diff options
| author | Clifford Wolf <clifford@clifford.at> | 2016-07-27 16:11:37 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2016-07-27 16:11:37 +0200 |
| commit | da56a5bbc60e58c305227105b68654264738c241 (patch) | |
| tree | bfae24cda2952ca3ed99f92d06dab0cf0849152a /backends | |
| parent | 8d88fcb27011a6f8f47a8615c30ab658fafab0f2 (diff) | |
| download | yosys-da56a5bbc60e58c305227105b68654264738c241.tar.gz yosys-da56a5bbc60e58c305227105b68654264738c241.tar.bz2 yosys-da56a5bbc60e58c305227105b68654264738c241.zip | |
Added $initstate support to smtbmc flow
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/smt2/smt2.cc | 15 | ||||
| -rw-r--r-- | backends/smt2/smtbmc.py | 3 |
2 files changed, 17 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"); diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index f74908f87..0e94a1675 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -130,6 +130,7 @@ if tempind: smt.write("(declare-fun s%d () %s_s)" % (step, topmod)) smt.write("(assert (%s_u s%d))" % (topmod, step)) smt.write("(assert (%s_h s%d))" % (topmod, step)) + smt.write("(assert (not (%s_is s%d)))" % (topmod, step)) if step == num_steps: smt.write("(assert (not (%s_a s%d)))" % (topmod, step)) @@ -172,9 +173,11 @@ else: # not tempind if step == 0: smt.write("(assert (%s_i s0))" % (topmod)) + smt.write("(assert (%s_is s0))" % (topmod)) else: smt.write("(assert (%s_t s%d s%d))" % (topmod, step-1, step)) + smt.write("(assert (not (%s_is s%d)))" % (topmod, step)) if step < skip_steps: if assume_skipped is not None and step >= assume_skipped: |