Abstract

Mainstream Hardware Description Languages (HDL) have not significantly improved since their introduction despite the continuous increase in the size and complexity of circuits being designed. As a result hardware design has become harder and harder. Our work is a step toward alleviating this problem by enhancing the Verilog Hardware Description Language. Static synthesizability and wire consistency checking for circuit families is one area where a large room for improvement is available.

Circuit families can be concisely described using existing Verilog’s generative constructs (parameterized modules, loops, and conditionals). These constructs are eliminated during the elaboration phase and replaced by simpler Verilog code. By treating Verilog as a statically typed two-level language and using indexed types, we can formalize the elaboration phase while providing static guarantees on the properties of the generated circuits. This formalization allows us to statically detect: 1) Non Synthesizable circuits, 2) Wire width mismatches, 3) Array bounds violations, and 4) Unreachable code. It also allows us to statically provide bounded parametric estimates of the number of gates required to realize a particular circuit.