aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--backends/smt2/smt2.cc13
-rw-r--r--backends/smt2/smtbmc.py5
-rw-r--r--backends/smt2/smtio.py9
-rw-r--r--tests/various/smtlib2_module-expected.smt214
4 files changed, 29 insertions, 12 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 54783cf1b..7434b13da 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -559,6 +559,9 @@ struct Smt2Worker
if (cell->type.in(ID($_FF_), ID($_DFF_P_), ID($_DFF_N_)))
{
registers.insert(cell);
+ SigBit q_bit = cell->getPort(ID::Q);
+ if (q_bit.is_wire())
+ decls.push_back(witness_signal("reg", 1, 0, "", idcounter, q_bit.wire));
makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(cell->getPort(ID::Q)));
register_bool(cell->getPort(ID::Q), idcounter++);
recursive_cells.erase(cell);
@@ -589,9 +592,12 @@ struct Smt2Worker
if (cell->type.in(ID($ff), ID($dff)))
{
registers.insert(cell);
- for (auto chunk : cell->getPort(ID::Q).chunks())
+ int smtoffset = 0;
+ for (auto chunk : cell->getPort(ID::Q).chunks()) {
if (chunk.is_wire())
- decls.push_back(witness_signal("reg", chunk.width, chunk.offset, "", idcounter, chunk.wire));
+ decls.push_back(witness_signal("reg", chunk.width, chunk.offset, "", idcounter, chunk.wire, smtoffset));
+ smtoffset += chunk.width;
+ }
makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(ID::Q)), log_signal(cell->getPort(ID::Q)));
register_bv(cell->getPort(ID::Q), idcounter++);
recursive_cells.erase(cell);
@@ -1490,7 +1496,7 @@ struct Smt2Worker
return path;
}
- std::string witness_signal(const char *type, int width, int offset, const std::string &smtname, int smtid, RTLIL::Wire *wire)
+ std::string witness_signal(const char *type, int width, int offset, const std::string &smtname, int smtid, RTLIL::Wire *wire, int smtoffset = 0)
{
std::vector<std::string> hiername;
const char *wire_name = wire->name.c_str();
@@ -1508,6 +1514,7 @@ struct Smt2Worker
{ "offset", offset },
{ "width", width },
{ "smtname", smtname.empty() ? json11::Json(smtid) : json11::Json(smtname) },
+ { "smtoffset", smtoffset },
{ "path", witness_path(wire) },
}}).dump(line);
line += "\n";
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 5f05287de..ac329053f 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -669,7 +669,7 @@ if inywfile is not None:
if common_end <= common_offset:
continue
- smt_expr = smt.net_expr(topmod, f"s{t}", wire["smtpath"])
+ smt_expr = smt.witness_net_expr(topmod, f"s{t}", wire)
if not smt_bool:
slice_high = common_end - offset - 1
@@ -1267,7 +1267,8 @@ def write_yw_trace(steps_start, steps_stop, index, allregs=False):
sigs = seqs
for sig in sigs:
- step_values[sig["sig"]] = smt.bv2bin(smt.get(smt.net_expr(topmod, f"s{k}", sig["smtpath"])))
+ value = smt.bv2bin(smt.get(smt.witness_net_expr(topmod, f"s{k}", sig)))
+ step_values[sig["sig"]] = value
yw.step(step_values)
yw.end_trace()
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 9af454cca..f5cfe436d 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -958,6 +958,15 @@ class SmtIo:
nextbase = "(|%s_h %s| %s)" % (mod, path[0], base)
return self.net_expr(nextmod, nextbase, path[1:])
+ def witness_net_expr(self, mod, base, witness):
+ net = self.net_expr(mod, base, witness["smtpath"])
+ is_bool = self.net_width(mod, witness["smtpath"]) == 1
+ if is_bool:
+ assert witness["width"] == 1
+ assert witness["smtoffset"] == 0
+ return net
+ return "((_ extract %d %d) %s)" % (witness["smtoffset"] + witness["width"] - 1, witness["smtoffset"], net)
+
def net_width(self, mod, net_path):
for i in range(len(net_path)-1):
assert mod in self.modinfo
diff --git a/tests/various/smtlib2_module-expected.smt2 b/tests/various/smtlib2_module-expected.smt2
index 74e2f3fca..494e7cda0 100644
--- a/tests/various/smtlib2_module-expected.smt2
+++ b/tests/various/smtlib2_module-expected.smt2
@@ -4,14 +4,14 @@
(declare-fun |smtlib2_is| (|smtlib2_s|) Bool)
(declare-fun |smtlib2#0| (|smtlib2_s|) (_ BitVec 8)) ; \a
; yosys-smt2-input a 8
-; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": "a", "type": "input", "width": 8}
+; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": "a", "smtoffset": 0, "type": "input", "width": 8}
(define-fun |smtlib2_n a| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#0| state))
(declare-fun |smtlib2#1| (|smtlib2_s|) (_ BitVec 8)) ; \b
; yosys-smt2-input b 8
-; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": "b", "type": "input", "width": 8}
+; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": "b", "smtoffset": 0, "type": "input", "width": 8}
(define-fun |smtlib2_n b| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#1| state))
; yosys-smt2-output add 8
-; yosys-smt2-witness {"offset": 0, "path": ["\\add"], "smtname": "add", "type": "blackbox", "width": 8}
+; yosys-smt2-witness {"offset": 0, "path": ["\\add"], "smtname": "add", "smtoffset": 0, "type": "blackbox", "width": 8}
(define-fun |smtlib2_n add| ((state |smtlib2_s|)) (_ BitVec 8) (let (
(|a| (|smtlib2_n a| state))
(|b| (|smtlib2_n b| state))
@@ -19,7 +19,7 @@
(bvadd a b)
))
; yosys-smt2-output eq 1
-; yosys-smt2-witness {"offset": 0, "path": ["\\eq"], "smtname": "eq", "type": "blackbox", "width": 1}
+; yosys-smt2-witness {"offset": 0, "path": ["\\eq"], "smtname": "eq", "smtoffset": 0, "type": "blackbox", "width": 1}
(define-fun |smtlib2_n eq| ((state |smtlib2_s|)) Bool (let (
(|a| (|smtlib2_n a| state))
(|b| (|smtlib2_n b| state))
@@ -27,7 +27,7 @@
(= a b)
))
; yosys-smt2-output sub 8
-; yosys-smt2-witness {"offset": 0, "path": ["\\sub"], "smtname": "sub", "type": "blackbox", "width": 8}
+; yosys-smt2-witness {"offset": 0, "path": ["\\sub"], "smtname": "sub", "smtoffset": 0, "type": "blackbox", "width": 8}
(define-fun |smtlib2_n sub| ((state |smtlib2_s|)) (_ BitVec 8) (let (
(|a| (|smtlib2_n a| state))
(|b| (|smtlib2_n b| state))
@@ -49,10 +49,10 @@
(declare-fun |uut#2| (|uut_s|) (_ BitVec 8)) ; \sub
(declare-fun |uut_h s| (|uut_s|) |smtlib2_s|)
; yosys-smt2-anyconst uut#3 8 smtlib2_module.v:14.17-14.26
-; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": 3, "type": "init", "width": 8}
+; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": 3, "smtoffset": 0, "type": "init", "width": 8}
(declare-fun |uut#3| (|uut_s|) (_ BitVec 8)) ; \a
; yosys-smt2-anyconst uut#4 8 smtlib2_module.v:14.32-14.41
-; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": 4, "type": "init", "width": 8}
+; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": 4, "smtoffset": 0, "type": "init", "width": 8}
(declare-fun |uut#4| (|uut_s|) (_ BitVec 8)) ; \b
(define-fun |uut#5| ((state |uut_s|)) (_ BitVec 8) (bvadd (|uut#3| state) (|uut#4| state))) ; \add2
(define-fun |uut#6| ((state |uut_s|)) Bool (= (|uut#0| state) (|uut#5| state))) ; $0$formal$smtlib2_module.v:28$1_CHECK[0:0]$9
generated by cgit v1.2.3 (git 2.25.1) at 2025-02-25 01:59:03 +0000