diff options
Diffstat (limited to 'backends/smt2/smt2.cc')
-rw-r--r-- | backends/smt2/smt2.cc | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 02d6f3fb6..584a1df1a 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -49,6 +49,7 @@ struct Smt2Worker regsmode(regsmode), wiresmode(wiresmode), verbose(verbose), idcounter(0) { decls.push_back(stringf("(declare-sort |%s_s| 0)\n", log_id(module))); + decls.push_back(stringf("(declare-fun |%s_is| (|%s_s|) Bool)\n", log_id(module), log_id(module))); for (auto cell : module->cells()) for (auto &conn : cell->connections()) { @@ -324,6 +325,16 @@ struct Smt2Worker exported_cells.insert(cell); recursive_cells.insert(cell); + if (cell->type == "$initstate") + { + SigBit bit = sigmap(cell->getPort("\\Y").as_bit()); + decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (|%s_is| state)) ; %s\n", + log_id(module), idcounter, log_id(module), log_id(module), log_signal(bit))); + register_bool(bit, idcounter++); + recursive_cells.erase(cell); + return; + } + if (cell->type == "$_DFF_P_" || cell->type == "$_DFF_N_") { registers.insert(cell); @@ -755,7 +766,9 @@ struct Smt2Backend : public Backend { log("the assumptions in the module.\n"); log("\n"); log("The '<mod>_i' function evaluates to 'true' when the given state conforms\n"); - log("to the initial state.\n"); + log("to the initial state. Furthermore the '<mod>_is' function should be asserted\n"); + log("to be true for initial states in addition to '<mod>_i', and should be\n"); + log("asserted to be false for non-initial states.\n"); log("\n"); log("For hierarchical designs, the '<mod>_h' function must be asserted for each\n"); log("state to establish the design hierarchy. The '<mod>_h <cellname>' function\n"); |