mirror of
https://github.com/YosysHQ/yosys
synced 2025-07-24 05:08:56 +00:00
Improved handling of SMT2 logics in yosys-smtbmc
This commit is contained in:
parent
13a03b84d4
commit
d009cdd6ee
3 changed files with 49 additions and 11 deletions
|
@ -998,7 +998,7 @@ struct Smt2Backend : public Backend {
|
|||
continue;
|
||||
}
|
||||
if (args[argidx] == "-nomem") {
|
||||
bvmode = false;
|
||||
memmode = false;
|
||||
continue;
|
||||
}
|
||||
if (args[argidx] == "-wires") {
|
||||
|
@ -1027,6 +1027,12 @@ struct Smt2Backend : public Backend {
|
|||
|
||||
*f << stringf("; SMT-LIBv2 description generated by %s\n", yosys_version_str);
|
||||
|
||||
if (!bvmode)
|
||||
*f << stringf("; yosys-smt2-nobv\n");
|
||||
|
||||
if (!memmode)
|
||||
*f << stringf("; yosys-smt2-nomem\n");
|
||||
|
||||
std::vector<RTLIL::Module*> sorted_modules;
|
||||
|
||||
// extract module dependencies
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue