Various fixes and improvements in write_smt2

2 files changed, 88 insertions, 32 deletions

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index a5c015918..c383bbab9 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -133,7 +133,7 @@ struct Smt2Worker
 				export_cell(bit_driver.at(bit));
 		sigmap.apply(sig);
 
-		for (int i = 0, j = 1; i < GetSize(sig); i += j)
+		for (int i = 0, j = 1; i < GetSize(sig); i += j, j = 1)
 		{
 			if (sig[i].wire == nullptr) {
 				while (i+j < GetSize(sig) && sig[i+j].wire == nullptr) j++;
@@ -167,7 +167,10 @@ struct Smt2Worker
 				continue;
 			}
 
-			while (i+j < GetSize(sig) && sig[i+j].wire && !fcache.count(sig[i+j])) j++;
+			std::set<RTLIL::SigBit> seen_bits = { sig[i] };
+			while (i+j < GetSize(sig) && sig[i+j].wire && !fcache.count(sig[i+j]) && !seen_bits.count(sig[i+j]))
+				seen_bits.insert(sig[i+j]), j++;
+
 			decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n",
 					log_id(module), idcounter, log_id(module), j, log_signal(sig.extract(i, j))));
 			subexpr.push_back(stringf("(|%s#%d| state)", log_id(module), idcounter));
@@ -205,14 +208,14 @@ struct Smt2Worker
 		return;
 	}
 
-	void export_bvop(RTLIL::Cell *cell, std::string expr, bool shift_op = false)
+	void export_bvop(RTLIL::Cell *cell, std::string expr, char type = 0)
 	{
 		RTLIL::SigSpec sig_a, sig_b;
 		RTLIL::SigSpec sig_y = sigmap(cell->getPort("\\Y"));
 		bool is_signed = cell->getParam("\\A_SIGNED").as_bool();
 		int width = GetSize(sig_y);
 
-		if (shift_op) {
+		if (type == 's') {
 			width = std::max(width, GetSize(sig_a));
 			width = std::max(width, GetSize(sig_b));
 		}
@@ -224,7 +227,7 @@ struct Smt2Worker
 
 		if (cell->hasPort("\\B")) {
 			sig_b = cell->getPort("\\B");
-			sig_b.extend_u0(width, is_signed && !shift_op);
+			sig_b.extend_u0(width, is_signed && !(type == 's'));
 		}
 
 		std::string processed_expr;
@@ -233,20 +236,26 @@ struct Smt2Worker
 			if (ch == 'A') processed_expr += get_bv(sig_a);
 			else if (ch == 'B') processed_expr += get_bv(sig_b);
 			else if (ch == 'L') processed_expr += is_signed ? "a" : "l";
-			else if (ch == 'U') processed_expr += is_signed ? "" : "u";
+			else if (ch == 'U') processed_expr += is_signed ? "s" : "u";
 			else processed_expr += ch;
 		}
 
 		if (width != GetSize(sig_y))
 			processed_expr = stringf("((_ extract %d 0) %s)", GetSize(sig_y)-1, processed_expr.c_str());
 
-		decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
-				log_id(module), idcounter, log_id(module), GetSize(sig_y), processed_expr.c_str(), log_signal(sig_y)));
-		register_bv(sig_y, idcounter++);
+		if (type == 'b') {
+			decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n",
+					log_id(module), idcounter, log_id(module), processed_expr.c_str(), log_signal(sig_y)));
+			register_boolvec(sig_y, idcounter++);
+		} else {
+			decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
+					log_id(module), idcounter, log_id(module), GetSize(sig_y), processed_expr.c_str(), log_signal(sig_y)));
+			register_bv(sig_y, idcounter++);
+		}
 		return;
 	}
 
-	void export_reduce(RTLIL::Cell *cell, std::string expr)
+	void export_reduce(RTLIL::Cell *cell, std::string expr, bool identity_val)
 	{
 		RTLIL::SigSpec sig_y = sigmap(cell->getPort("\\Y"));
 		std::string processed_expr;
@@ -256,6 +265,8 @@ struct Smt2Worker
 				RTLIL::SigSpec sig = sigmap(cell->getPort(stringf("\\%c", ch)));
 				for (auto bit : sig)
 					processed_expr += " " + get_bool(bit);
+				if (GetSize(sig) == 1)
+					processed_expr += identity_val ? " true" : " false";
 			} else
 				processed_expr += ch;
 
@@ -312,22 +323,22 @@ struct Smt2Worker
 		if (cell->type == "$xor") return export_bvop(cell, "(bvxor A B)");
 		if (cell->type == "$xnor") return export_bvop(cell, "(bvxnor A B)");
 
-		if (cell->type == "$shl") return export_bvop(cell, "(bvshl A B)", true);
-		if (cell->type == "$shr") return export_bvop(cell, "(bvlshr A B)", true);
-		if (cell->type == "$sshl") return export_bvop(cell, "(bvshl A B)", true);
-		if (cell->type == "$sshr") return export_bvop(cell, "(bvLshr A B)", true);
+		if (cell->type == "$shl") return export_bvop(cell, "(bvshl A B)", 's');
+		if (cell->type == "$shr") return export_bvop(cell, "(bvlshr A B)", 's');
+		if (cell->type == "$sshl") return export_bvop(cell, "(bvshl A B)", 's');
+		if (cell->type == "$sshr") return export_bvop(cell, "(bvLshr A B)", 's');
 
 		// FIXME: $shift $shiftx
 
-		if (cell->type == "$lt") return export_bvop(cell, "(bvUlt A B)");
-		if (cell->type == "$le") return export_bvop(cell, "(bvUle A B)");
-		if (cell->type == "$ge") return export_bvop(cell, "(bvUge A B)");
-		if (cell->type == "$gt") return export_bvop(cell, "(bvUgt A B)");
+		if (cell->type == "$lt") return export_bvop(cell, "(bvUlt A B)", 'b');
+		if (cell->type == "$le") return export_bvop(cell, "(bvUle A B)", 'b');
+		if (cell->type == "$ge") return export_bvop(cell, "(bvUge A B)", 'b');
+		if (cell->type == "$gt") return export_bvop(cell, "(bvUgt A B)", 'b');
 
-		if (cell->type == "$ne") return export_bvop(cell, "(distinct A B)");
-		if (cell->type == "$nex") return export_bvop(cell, "(distinct A B)");
-		if (cell->type == "$eq") return export_bvop(cell, "(= A B)");
-		if (cell->type == "$eqx") return export_bvop(cell, "(= A B)");
+		if (cell->type == "$ne") return export_bvop(cell, "(distinct A B)", 'b');
+		if (cell->type == "$nex") return export_bvop(cell, "(distinct A B)", 'b');
+		if (cell->type == "$eq") return export_bvop(cell, "(= A B)", 'b');
+		if (cell->type == "$eqx") return export_bvop(cell, "(= A B)", 'b');
 
 		if (cell->type == "$not") return export_bvop(cell, "(bvnot A)");
 		if (cell->type == "$pos") return export_bvop(cell, "A");
@@ -339,15 +350,15 @@ struct Smt2Worker
 		if (cell->type == "$div") return export_bvop(cell, "(bvUdiv A B)");
 		if (cell->type == "$mod") return export_bvop(cell, "(bvUrem A B)");
 
-		if (cell->type == "$reduce_and") return export_reduce(cell, "(and A)");
-		if (cell->type == "$reduce_or") return export_reduce(cell, "(or A)");
-		if (cell->type == "$reduce_xor") return export_reduce(cell, "(xor A)");
-		if (cell->type == "$reduce_xnor") return export_reduce(cell, "(not (xor A))");
-		if (cell->type == "$reduce_bool") return export_reduce(cell, "(or A)");
+		if (cell->type == "$reduce_and") return export_reduce(cell, "(and A)", true);
+		if (cell->type == "$reduce_or") return export_reduce(cell, "(or A)", false);
+		if (cell->type == "$reduce_xor") return export_reduce(cell, "(xor A)", false);
+		if (cell->type == "$reduce_xnor") return export_reduce(cell, "(not (xor A))", false);
+		if (cell->type == "$reduce_bool") return export_reduce(cell, "(or A)", false);
 
-		if (cell->type == "$logic_not") return export_reduce(cell, "(not (or A))");
-		if (cell->type == "$logic_and") return export_reduce(cell, "(and (or A) (or B))");
-		if (cell->type == "$logic_or") return export_reduce(cell, "(or A B)");
+		if (cell->type == "$logic_not") return export_reduce(cell, "(not (or A))", false);
+		if (cell->type == "$logic_and") return export_reduce(cell, "(and (or A) (or B))", false);
+		if (cell->type == "$logic_or") return export_reduce(cell, "(or A B)", false);
 
 		// FIXME: $slice $concat $mux $pmux
 
@@ -407,8 +418,8 @@ struct Smt2Backend : public Backend {
 		log("'<mod>' this will declare the sort '<mod>_s' (state of the module) and the the\n");
 		log("function '<mod>_t' (state transition function).\n");
 		log("\n");
-		log("The '<mod>_s' sort represents the a module state. Additional '<mod>_n' functions\n");
-		log("are provided that can be used to access the values of all signals in the module.\n");
+		log("The '<mod>_s' sort represents a module state. Additional '<mod>_n' functions\n");
+		log("are provided that can be used to access the values of the signals in the module.\n");
 		log("Only ports, and signals with the 'keep' attribute set are made available via\n");
 		log("such functions. Without the -bv option, multi-bit wires are exported as\n");
 		log("separate functions of type Bool for the individual bits. With the -bv option\n");
diff --git a/backends/smt2/test_cells.sh b/backends/smt2/test_cells.sh
new file mode 100644
index 000000000..28d5c57f5
--- /dev/null
+++ b/backends/smt2/test_cells.sh
@@ -0,0 +1,45 @@
+#!/bin/bash
+
+set -ex
+
+rm -rf test_cells
+mkdir test_cells
+cd test_cells
+
+../../../yosys -p 'test_cell -n 2 -w test all /$alu /$macc /$fa /$lcu /$lut /$shift /$shiftx /$div /$mod'
+
+cat > miter.tpl <<- EOT
+; #model# (set-option :produce-models true)
+(set-logic QF_UFBV)
+%%
+(declare-fun s () miter_s)
+(assert (|miter_n trigger| s))
+(check-sat)
+; #model# (get-value ((|miter_n in_A| s) (|miter_n in_B| s) (|miter_n gold_Y| s) (|miter_n gate_Y| s) (|miter_n trigger| s)))
+EOT
+
+for x in test_*.il; do
+	x=${x%.il}
+	cat > $x.ys <<- EOT
+		read_ilang $x.il
+		copy gold gate
+
+		cd gate
+		techmap; opt; abc;;
+		cd ..
+
+		miter -equiv -flatten -make_outputs gold gate miter
+		hierarchy -check -top miter
+
+		dump
+		write_smt2 -bv -tpl miter.tpl $x.smt2
+	EOT
+	../../../yosys $x.ys
+	cvc4 $x.smt2 > $x.result
+	if ! grep unsat $x.result; then
+		echo "Proof failed! Extracting model..."
+		sed -i 's/^; #model# //' $x.smt2
+		cvc4 $x.smt2
+		exit 1
+	fi
+done