Verilog: synthesize the module instance hierarchy monolithically

[kroening]

Summary

Synthesis used to be modular: synth_module_instance recursively invoked a fresh verilog_synthesist object per instantiated module, generating that module's constraints (synth_assignments) before folding the result into its parent. Because the assignment bookkeeping (assignments, local_symbols) was scoped to each of these separate objects, an assignment reaching across an instance boundary via a hierarchical identifier (in either direction) was invisible to whichever module's constraints had already been finalized. This silently produced an over-constrained transition system (e.g. a spurious self-hold alongside the real next-state equation) rather than an error — in the worst case making the transition relation UNSAT beyond the initial state, so every safety property is vacuously, wrongly "proved".

• synth_module_items now recursively expands the entire instance hierarchy in place, using one shared verilog_synthesist object, so assignments/local_symbols accumulate across the whole design.
• synth_assignments (which generates the actual constraints) now runs exactly once, after the whole hierarchy has been visited.
• default_disable_iff is explicitly saved/restored per module, since it's no longer implicitly scoped by a fresh object per module.
• The existing shortcut for a module that's already been independently synthesized (top-level modules pre-synthesized under typecheck_module, later wrapped under $root) is preserved.

Test plan

• regression/verilog/interface/instance4.desc: promoted from KNOWNBUG to CORE (this is exactly the bug — an interface's counter driven both by its own always block and a hierarchical identifier from the enclosing module; previously stayed vacuously PROVED even at bound 20). Bound corrected from 10 to 11 to match the counter's actual dynamics.
• Added regression/verilog/hierarchical_identifiers/hierarchical_identifiers5.{sv,desc}: same shape using a plain module instance rather than an interface. Verified it reports the wrong PROVED/EXIT=0 on the old code and the correct REFUTED/EXIT=10 with this change.
• regression/verilog/modules/ref_port1.desc moved to KNOWNBUG: making synthesis monolithic exposes a pre-existing gap in how ref ports are modeled (as a driven/continuous connection rather than a true alias for the bound variable), which now surfaces as a conversion error instead of silently working by accident. Deferred to a follow-up change; the comment in the .desc documents the cause.
• Full regression/verilog suite (917 tests, all levels) passes.
• Full regression/ebmc suite passes.

[tautschnig]

It's a somewhat hidden invariant that those need to be cleaned first. Maybe the should actually become local variables and be passed to synth_module_items and synth_assignments? Though I also wonder whether invars is necessary at all - couldn't trans.invar() be populated directly?