Merge pull request #4222 from jix/pdr-X

write_aiger: Include `$assert` and `$assume` cells in -ywmap output

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)

backends/aiger/aiger.cc

@@ -67,6 +67,8 @@ struct AigerWriter
 	int initstate_ff = 0;
 
 	dict<SigBit, int> ywmap_clocks;
+	vector<Cell *> ywmap_asserts;
+	vector<Cell *> 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();
 	}
 

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

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)

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):
+        result = []
-            return stmt
+        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:

passes/cmds/rename.cc

@@ -134,7 +134,6 @@ static bool rename_witness(RTLIL::Design *design, dict<RTLIL::Module *, int> &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<RTLIL::Module *, int> &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);

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