Making Concurrent Hardware Verification Sequential

Compared to familiar hardware-description languages like Verilog, rule-based languages like Bluespec offer opportunities to import modularity features from software programming. While Verilog modules are about connecting wires between submodules, Bluespec modules resemble objects in object-oriented programming, where interactions with a module occur only through calls to its methods. However, while software objects can typically be characterized one method at a time, the concurrent nature of hardware makes it essential to consider the repercussions of invoking multiple methods simultaneously. Prior formalizations of rule-based languages conceptualized modules by describing their semantics considering arbitrary sets of simultaneous method calls. This internalized concurrency significantly complicates correctness proofs. Rather than analyzing methods one-at-a-time, as is done when verifying software object methods, validating the correctness of rule-based modules necessitated simultaneous consideration of arbitrary subsets of method calls. The result was a number of proof cases that grew exponentially in the size of the module’s API. In this work, we side-step the exponential blowup through a set of judicious language restrictions. We introduce a new Bluespec-inspired formal language, Fjf j, that supports sequential characterization of modules, while preserving the concurrent hardware nature of the language. We evaluated Fjf j by implementing it in Coq, proving the key framework principle: the refinement theorem. We demonstrated Fjf j’s expressivity via implementation and verification of three examples: a pipelined processor, a parameterized crossbar, and a network switch.