Closed programmerjake closed 2 years ago
note that this passes ci now
I would prefer if sby automatically does the right thing here instead of adding an option that removes the simcheck completely. Skipping the simcheck would allow using blackboxes to pass incomplete smtlib2 files to smtbmc and then on to the solvers. I think the way to do this instead would be extend hierarchy -simcheck
to have a mode where it allows blackboxes with an smtlib2_module
attribute and then to use that mode in sby's print_common_prep only when called for generating an smtlib2 output.
I think the way to do this instead would be extend
hierarchy -simcheck
to have a mode where it allows blackboxes with ansmtlib2_module
attribute and then to use that mode in sby's print_common_prep only when called for generating an smtlib2 output.
That sounds like a good idea, I'll work on it soon.
I think the way to do this instead would be extend
hierarchy -simcheck
to have a mode where it allows blackboxes with ansmtlib2_module
attribute and then to use that mode in sby's print_common_prep only when called for generating an smtlib2 output.That sounds like a good idea, I'll work on it soon.
I added -smtcheck
in https://github.com/YosysHQ/yosys/pull/3391
switch to using
hierarchy -smtcheck
for smtlib2 solvers, allowingsmtlib2_module
modulesFixes: https://github.com/YosysHQ/sby/issues/168
Depends on https://github.com/YosysHQ/yosys/pull/3391