Verilog: register-transfer level IR layer

[kroening]

This adds a new IR layer to the Verilog frontend that follows type checking and precedes synthesis.

Summary

The register-transfer level (RTL) representation (src/verilog/verilog_rtl.h) is a map from identifiers to a map of slices (lower and higher bit index) to the definition of the slice, plus the assert, assume and cover properties of the module. The slice definition indicates whether the slice is state-holding (a register) or a wire, and gives the defining expression: the next-state value for state-holding slices, and the current-state value for wires.

The construction pass (src/verilog/verilog_rtl.cpp) builds the representation from the type-checked module items. It supports:

• clocked and combinational always constructs, continuous assignments, and net declarations with a value
• bit- and part-select lvalues, concatenation lvalues, members of packed structs and unions, array elements, and nestings thereof; constant selects map to slices, and array elements with non-constant indices yield a with-expression over the whole array; slices that are partially out of range are clipped per 1800-2017 11.5.1
• if statements (branch values are merged per bit-fragment at slice boundaries)
• case, casex and casez statements, converted into if-then-else chains with the same pattern masking for ?, x, z as synthesis
• for loops, which are unrolled; break, continue and return use path-condition tracking, mirroring synthesis
• tasks and functions called as a statement, which are inlined; their locals are not part of the representation
• increment/decrement statements and compound assignment operators, lowered to plain assignments
• substitution of blocking assignments into subsequent right-hand sides, including reads after assignments to a part of a variable, which compose the value from the recorded fragments
• assert, assume and cover properties, recorded with their label when one is given: concurrent properties at module level, deferred assertions, and immediate and procedural concurrent assertions in always constructs (the path condition is applied as an implication)
• labeled statements

Constructs that synthesis also rejects (e.g. always_latch, guard-less always with assignments, procedural continuous assignments) produce a located error.

The new command-line option --show-rtl shows the representation, e.g.:

$root.main.q[3:0] register, next-state value: main.rst ? 0 : main.d[3:0]
$root.main.sum[7:0] wire, value: main.q + main.d
assert p1: main.q |-> main.d
cover c1: main.q == 15

Full designs

The RTL representation now covers full designs, so that a transition system can be constructed from it (see #2119):

• Module instances are included recursively; port connections and primitive gates become constraints, and interface ports connect the members of the bound interface instance.
• Initial constructs and variable declarations with an initializer yield initial values, recorded per slice.
• The declared variables are recorded; identifiers forced by port connections are tracked so that they can become wires.
• User-defined function calls in right-hand sides are inlined, including output arguments and return statements; elaboration-time constants, hierarchical identifiers, named property/sequence instances, and constant system functions such as $left are resolved during substitution.
• Properties carry their type-checker identifier and context, and the default disable iff clause is applied per module and generate block.

Testing

• New unit tests in unit/verilog/verilog_rtl.cpp (17 scenarios): slices, registers, wires, part selects, conditionals, case statements, for loops with and without break, task enables, concatenation lvalues, struct members, array elements, compound assignments, net declarations, increment/decrement, properties with and without labels, blocking-assignment substitution.
• Full unit suite passes (356 assertions in 62 test cases).
• regression/verilog and regression/ebmc suites pass.
• --show-rtl succeeds on all 746 tests in regression/verilog that reach RTL construction, except for 5 that deliberately provoke front-end errors.