mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-24 01:25:33 +00:00
Code Activity

Merge branch 'master' of github.com:cliffordwolf/yosys

Browse source
This commit is contained in:
Clifford Wolf 2016-07-30 12:50:39 +02:00
commit 21e1bac084
16 changed files with 162 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

15
backends/smt2/smt2.cc
View file

@ -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");

3
backends/smt2/smtbmc.py
View file

@ -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: