Parameterized Construction and Constraint-Driven Validation of Formal Hardware Specifications for Efficient Code Generation

Abstract:
Hardware construction and code generation have been introduced to hardware development processes to cope with the increasing complexity of modern integrated circuits. Additionally, to maximize the reusability of such code generators, the Universal Specification Format (USF) provides a general formalism for high-level system specifications. USF models arbitrary hardware systems by their internal state and function set using a domain-specific expression language. However, it is this general modeling capacity of the USF formalism that also results in complex formal specifications, which can become tedious to write and prone to errors. Addressing these challenges, we present a specification workflow to simplify and harden the construction of valid USF models. It consists of two pillars: first, the parameterized construction of USF models simplifies system specification, and second, a novel constraint definition validates that the constructed specifications are correct. Moreover, we show that these constraints enable sweeping over a range of compliant configurations to automatically generate valid specification variants. Demonstrating the benefits of our workflow, we apply it to a selection of industrial hardware designs.