Verilog: create the transition relation from the RTL representation

[kroening]

Stacked on #2117; only the top commit ("Verilog: create the transition relation from the RTL representation") is new relative to that PR.

Summary

This adds a new component, verilog_transition_relation (src/verilog/verilog_transition_relation.{h,cpp}), which replaces verilog_synthesis in the EBMC flow. It takes the register-transfer level (RTL) representation introduced in #2117 as input — which includes module instances recursively — and produces the transition relation for the design:

• State-holding slices become next-state equalities in the transition constraints, and wire slices become equalities in the state constraints. Slices are composed into whole-symbol values; unassigned fragments hold their value (registers) or remain unconstrained (wires). Variables that are only assigned combinationally become wires, as do variables forced by port connections.
• Declared variables without a next-state definition hold their value.
• The initial values yield the initial state constraints; reads of state-holding variables are replaced by their non-deterministic pre-initial value, and unused non-determinism is removed. --ignore-initial and --initial-zero are handled here.
• Constraints from port connections and primitive gates are added to the state constraints.
• Properties are wrapped as in synthesis (implicit always, assume/cover marking, sequence semantics) and set as the values of the property symbols.
• Expressions are lowered, and remaining system function calls, e.g. $past, are rewritten as in synthesis.

Unlike synthesis, the conversion does not introduce auxiliary wires (x_aux0 etc.); four regression test expectations are updated accordingly. verilog_synthesis remains in use by the hw-cbmc flow.

The RTL gaps found while making all tests pass were fixed in #2117 (module instances, initial values, declared-variable and forced-wire tracking, function call inlining with side effects, hierarchical identifiers, constant folding of type-dependent system functions, case pattern folding, and more).

Testing

With the new pipeline, all suites pass:

• unit (356 assertions in 62 test cases)
• regression/verilog (SAT and Z3)
• regression/ebmc (SAT and Z3)
• regression/smv (SAT and Z3)
• regression/vlindex