diff --git a/Makefile b/Makefile index 2539d5caa..35290fbd8 100644 --- a/Makefile +++ b/Makefile @@ -165,7 +165,7 @@ bumpversion: # is just a symlink to your actual ABC working directory, as 'make mrproper' # will remove the 'abc' directory and you do not want to accidentally # delete your work on ABC.. -ABCREV = 896e5e7 +ABCREV = 0cd90d0 ABCPULL = 1 ABCURL ?= https://github.com/YosysHQ/abc ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 ABC_USE_NAMESPACE=abc VERBOSE=$(Q) diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index fe4f7681d..f2cb5d9bc 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -67,6 +67,8 @@ struct AigerWriter int initstate_ff = 0; dict ywmap_clocks; + vector ywmap_asserts; + vector ywmap_assumes; int mkgate(int a0, int a1) { @@ -269,6 +271,7 @@ struct AigerWriter unused_bits.erase(A); unused_bits.erase(EN); asserts.push_back(make_pair(A, EN)); + ywmap_asserts.push_back(cell); continue; } @@ -279,6 +282,7 @@ struct AigerWriter unused_bits.erase(A); unused_bits.erase(EN); assumes.push_back(make_pair(A, EN)); + ywmap_assumes.push_back(cell); continue; } @@ -852,6 +856,19 @@ struct AigerWriter for (auto &it : init_lines) json.value(it.second); json.end_array(); + + json.name("asserts"); + json.begin_array(); + for (Cell *cell : ywmap_asserts) + json.value(witness_path(cell)); + json.end_array(); + + json.name("assumes"); + json.begin_array(); + for (Cell *cell : ywmap_assumes) + json.value(witness_path(cell)); + json.end_array(); + json.end_object(); } diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 5e63e6237..c702d5e7e 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -1117,7 +1117,18 @@ struct Smt2Worker string name_a = get_bool(cell->getPort(ID::A)); string name_en = get_bool(cell->getPort(ID::EN)); - if (cell->name[0] == '$' && cell->attributes.count(ID::src)) + bool private_name = cell->name[0] == '$'; + + if (!private_name && cell->has_attribute(ID::hdlname)) { + for (auto const &part : cell->get_hdlname_attribute()) { + if (part == "_witness_") { + private_name = true; + break; + } + } + } + + if (private_name && cell->attributes.count(ID::src)) decls.push_back(stringf("; yosys-smt2-%s %d %s %s\n", cell->type.c_str() + 1, id, get_id(cell), cell->attributes.at(ID::src).decode_string().c_str())); else decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, get_id(cell))); diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 34657be26..cc47bc376 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -649,14 +649,20 @@ if aimfile is not None: num_steps = max(num_steps, step+2) step += 1 +ywfile_hierwitness_cache = None + def ywfile_constraints(inywfile, constr_assumes, map_steps=None, skip_x=False): + global ywfile_hierwitness_cache if map_steps is None: map_steps = {} with open(inywfile, "r") as f: inyw = ReadWitness(f) - inits, seqs, clocks, mems = smt.hierwitness(topmod, allregs=True, blackbox=True) + if ywfile_hierwitness_cache is None: + ywfile_hierwitness_cache = smt.hierwitness(topmod, allregs=True, blackbox=True) + + inits, seqs, clocks, mems = ywfile_hierwitness_cache smt_wires = defaultdict(list) smt_mems = defaultdict(list) diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index ebf364f06..c904aea95 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -79,6 +79,20 @@ def except_hook(exctype, value, traceback): sys.excepthook = except_hook +def recursion_helper(iteration, *request): + stack = [iteration(*request)] + + while stack: + top = stack.pop() + try: + request = next(top) + except StopIteration: + continue + + stack.append(top) + stack.append(iteration(*request)) + + hex_dict = { "0": "0000", "1": "0001", "2": "0010", "3": "0011", "4": "0100", "5": "0101", "6": "0110", "7": "0111", @@ -298,10 +312,22 @@ class SmtIo: return stmt def unroll_stmt(self, stmt): - if not isinstance(stmt, list): - return stmt + result = [] + recursion_helper(self._unroll_stmt_into, stmt, result) + return result.pop() - stmt = [self.unroll_stmt(s) for s in stmt] + def _unroll_stmt_into(self, stmt, output, depth=128): + if not isinstance(stmt, list): + output.append(stmt) + return + + new_stmt = [] + for s in stmt: + if depth: + yield from self._unroll_stmt_into(s, new_stmt, depth - 1) + else: + yield s, new_stmt + stmt = new_stmt if len(stmt) >= 2 and not isinstance(stmt[0], list) and stmt[0] in self.unroll_decls: assert stmt[1] in self.unroll_objs @@ -330,12 +356,19 @@ class SmtIo: decl[2] = list() if len(decl) > 0: - decl = self.unroll_stmt(decl) + tmp = [] + if depth: + yield from self._unroll_stmt_into(decl, tmp, depth - 1) + else: + yield decl, tmp + + decl = tmp.pop() self.write(self.unparse(decl), unroll=False) - return self.unroll_cache[key] + output.append(self.unroll_cache[key]) + return - return stmt + output.append(stmt) def p_thread_main(self): while True: diff --git a/passes/cmds/rename.cc b/passes/cmds/rename.cc index da4ba2f17..3f8d807b3 100644 --- a/passes/cmds/rename.cc +++ b/passes/cmds/rename.cc @@ -134,7 +134,6 @@ static bool rename_witness(RTLIL::Design *design, dict &ca cell->set_hdlname_attribute({ "_witness_", strstr(new_id.c_str(), ".") + 1 }); renames.emplace_back(cell, new_id); } - break; } if (cell->type.in(ID($anyconst), ID($anyseq), ID($anyinit), ID($allconst), ID($allseq))) { @@ -165,6 +164,20 @@ static bool rename_witness(RTLIL::Design *design, dict &ca } } } + + + if (cell->type.in(ID($assert), ID($assume), ID($cover), ID($live), ID($fair), ID($check))) { + has_witness_signals = true; + if (cell->name.isPublic()) + continue; + std::string name = stringf("%s_%s", cell->type.c_str() + 1, cell->name.c_str() + 1); + for (auto &c : name) + if ((c < 'a' || c > 'z') && (c < 'A' || c > 'Z') && (c < '0' || c > '9') && c != '_') + c = '_'; + auto new_id = module->uniquify("\\_witness_." + name); + renames.emplace_back(cell, new_id); + cell->set_hdlname_attribute({ "_witness_", strstr(new_id.c_str(), ".") + 1 }); + } } for (auto rename : renames) { module->rename(rename.first, rename.second); diff --git a/tests/sva/runtest.sh b/tests/sva/runtest.sh index 84e797390..7692a5f9a 100644 --- a/tests/sva/runtest.sh +++ b/tests/sva/runtest.sh @@ -1,6 +1,6 @@ #!/usr/bin/env bash -set -ex +set -e prefix=${1%.ok} prefix=${prefix%.sv} @@ -58,16 +58,33 @@ generate_sby() { } if [ -f $prefix.ys ]; then + set -x $PWD/../../yosys -q -e "Assert .* failed." -s $prefix.ys elif [ -f $prefix.sv ]; then generate_sby pass > ${prefix}_pass.sby generate_sby fail > ${prefix}_fail.sby - sby --yosys $PWD/../../yosys -f ${prefix}_pass.sby - sby --yosys $PWD/../../yosys -f ${prefix}_fail.sby + + # Check that SBY is up to date enough for this yosys version + if sby --help | grep -q -e '--status'; then + set -x + sby --yosys $PWD/../../yosys -f ${prefix}_pass.sby + sby --yosys $PWD/../../yosys -f ${prefix}_fail.sby + else + echo "sva test '${prefix}' requires an up to date SBY, skipping" + fi else generate_sby pass > ${prefix}.sby - sby --yosys $PWD/../../yosys -f ${prefix}.sby + + # Check that SBY is up to date enough for this yosys version + if sby --help | grep -q -e '--status'; then + set -x + sby --yosys $PWD/../../yosys -f ${prefix}.sby + else + echo "sva test '${prefix}' requires an up to date SBY, skipping" + fi fi +{ set +x; } &>/dev/null + touch $prefix.ok