Draft
Conversation
kroening
force-pushed
the
kroening/root-module-instance
branch
2 times, most recently
from
6669f27 to
e7fcf46
Compare
Create a $root module instance that contains an instance of the top-level module, per IEEE 1800-2017. The $root module is synthesized via verilog_synthesis, which expands the top-level module into $root's namespace. The main_symbol now points to $root. The $root module's type is copied from the top-level module (including ports), and its module field is set to the instance identifier for expression resolution (used by -p, --reset, etc.). Pretty names and expression output strip the $root prefix since it is implicit in SystemVerilog.
kroening
force-pushed
the
kroening/root-module-instance
branch
from
e7fcf46 to
ee8b061
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Create a $root module instance that contains an instance of the top-level module, per IEEE 1800-2017.
Changes
$root module creation: After typechecking the top-level module, a synthetic $root module is created with a
verilog_insttthat instantiates the top-level module.verilog_synthesisexpands this, copying all symbols into $root's namespace.main_symbol points to $root: The transition system's
main_symbolnow points toVerilog::$root. The $root module's type is copied from the top-level module (including ports). Itsmodulefield is set to the instance identifier for expression resolution (-p,--reset, etc.).Display: Pretty names and the expression printer strip the $root prefix since it is implicit in SystemVerilog. Internal identifiers retain $root for correct lookups.
EBMC core fixes:
instrument_past,liveness_to_safety, andlive_signalnow usemain_symbol->name(notmain_symbol->module) when registering new symbols, since these need to appear in thesymbol_module_mapunder $root.Regression tests: Updated 7 test descriptors to reflect $root in hierarchy display, internal identifiers, and VCD/SMV netlist output.