riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Merge pull request #3510 from jix/ff_witness_fixes 

smt2/smtbmc: Fix FF witness data for fine grained or multi chunk FFs
This commit is contained in:
Jannis Harder 2022-10-12 20:50:00 +02:00 committed by GitHub
parent f35c062354 4d334fd3e3
commit 33a2773de0
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 29 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
backends/smt2/smt2.cc
View File

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

5
backends/smt2/smtbmc.py
View File

@ -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()

9
backends/smt2/smtio.py
View File

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

14
tests/various/smtlib2_module-expected.smt2
View File

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