From: Jacob Lifshay <programmerjake@gmail.com>
Date: Wed, 18 May 2022 04:29:58 +0000 (-0700)
Subject: add $smtlib2_expr
X-Git-Tag: smtlib2-expr-support-old~3
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4bf43c5ee227c0b64c6fff8276afa9b17bf36b94;p=yosys.git

add $smtlib2_expr
---

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index a3628197e..ed7e17951 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -436,6 +436,28 @@ struct Smt2Worker
 		recursive_cells.erase(cell);
 	}
 
+	void export_smtlib2_expr(RTLIL::Cell *cell)
+	{
+		RTLIL::SigSpec sig_a = cell->getPort(ID::A);
+		RTLIL::SigSpec sig_y = sigmap(cell->getPort(ID::Y));
+		string expr = cell->getParam(ID::EXPR).decode_string();
+
+		string a_bv = get_bv(sig_a);
+
+		if (verbose)
+			log("%*s-> import cell: %s\n", 2 + 2 * GetSize(recursive_cells), "", log_id(cell));
+
+		int expr_idcounter = idcounter++;
+
+		decls.push_back(stringf("(define-fun |%s#%d| ((A (_ BitVec %d))) (_ BitVec %d) ; %s\n  %s\n)\n", get_id(module), expr_idcounter,
+					GetSize(sig_a), GetSize(sig_y), log_signal(sig_y), expr.c_str()));
+		decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) (|%s#%d| %s)) ; %s\n", get_id(module), idcounter,
+					get_id(module), GetSize(sig_y), get_id(module), expr_idcounter, a_bv.c_str(), log_signal(sig_y)));
+		register_bv(sig_y, idcounter++);
+
+		recursive_cells.erase(cell);
+	}
+
 	void export_bvop(RTLIL::Cell *cell, std::string expr, char type = 0)
 	{
 		RTLIL::SigSpec sig_a, sig_b;
@@ -692,6 +714,10 @@ struct Smt2Worker
 				return;
 			}
 
+			if (cell->type == ID($smtlib2_expr)) {
+				return export_smtlib2_expr(cell);
+			}
+
 			// FIXME: $slice $concat
 		}
 
diff --git a/kernel/celltypes.h b/kernel/celltypes.h
index 7e9cfb38d..7a9eff1fc 100644
--- a/kernel/celltypes.h
+++ b/kernel/celltypes.h
@@ -176,6 +176,7 @@ struct CellTypes
 		setup_stdcells_eval();
 
 		setup_type(ID($_TBUF_), {ID::A, ID::E}, {ID::Y}, true);
+		setup_type(ID($smtlib2_expr), {ID::A}, {ID::Y});
 	}
 
 	void setup_stdcells_eval()
diff --git a/kernel/constids.inc b/kernel/constids.inc
index 566b76217..d6202663d 100644
--- a/kernel/constids.inc
+++ b/kernel/constids.inc
@@ -82,6 +82,7 @@ X(enum_base_type)
 X(enum_type)
 X(equiv_merged)
 X(equiv_region)
+X(EXPR)
 X(extract_order)
 X(F)
 X(force_downto)
diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc
index 72dcb89af..c91b2bb71 100644
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -1626,6 +1626,14 @@ namespace {
 				return;
 			}
 
+			if (cell->type == ID($smtlib2_expr)) {
+				param(ID::EXPR);
+				port(ID::A, param(ID::A_WIDTH));
+				port(ID::Y, param(ID::Y_WIDTH));
+				check_expected();
+				return;
+			}
+
 			if (cell->type.in(ID($assert), ID($assume), ID($live), ID($fair), ID($cover))) {
 				port(ID::A, 1);
 				port(ID::EN, 1);
diff --git a/manual/CHAPTER_CellLib.tex b/manual/CHAPTER_CellLib.tex
index 3c9fb31cc..2727e4dc4 100644
--- a/manual/CHAPTER_CellLib.tex
+++ b/manual/CHAPTER_CellLib.tex
@@ -1005,3 +1005,7 @@ Add information about {\tt \$lut} and {\tt \$sop} cells.
 \begin{fixme}
 Add information about {\tt \$alu}, {\tt \$macc}, {\tt \$fa}, and {\tt \$lcu} cells.
 \end{fixme}
+
+\begin{fixme}
+Add information about {\tt \$smtlib2_expr} cell.
+\end{fixme}
diff --git a/techlibs/common/simlib.v b/techlibs/common/simlib.v
index b14488ff4..789b97a5f 100644
--- a/techlibs/common/simlib.v
+++ b/techlibs/common/simlib.v
@@ -2591,3 +2591,24 @@ endmodule
 `endif
 
 // --------------------------------------------------------
+
+module \$smtlib2_expr (A, Y);
+
+parameter EXPR = "";
+parameter A_WIDTH = 0;
+parameter Y_WIDTH = 0;
+
+input [A_WIDTH-1:0] A;
+output [Y_WIDTH-1:0] Y;
+
+initial begin
+	// inside if to not break tests
+	if (EXPR != "") begin
+		$display("ERROR: $smtlib2_expr is non-simulatable!");
+		$finish;
+	end
+end
+
+endmodule
+
+// --------------------------------------------------------
diff --git a/techlibs/common/techmap.v b/techlibs/common/techmap.v
index 91d385b80..45c90f897 100644
--- a/techlibs/common/techmap.v
+++ b/techlibs/common/techmap.v
@@ -646,3 +646,12 @@ module _90_lut;
 endmodule
 `endif
 
+(* techmap_celltype = "$smtlib2_expr" *)
+module _90_smtlib2_expr (A, Y);
+	parameter EXPR = "";
+	parameter A_WIDTH = 0;
+	parameter Y_WIDTH = 0;
+
+	input [A_WIDTH-1:0] A;
+	output [Y_WIDTH-1:0] Y;
+endmodule
diff --git a/tests/various/.gitignore b/tests/various/.gitignore
index c6373468a..bc7f447ae 100644
--- a/tests/various/.gitignore
+++ b/tests/various/.gitignore
@@ -6,3 +6,5 @@
 /plugin.so
 /plugin.so.dSYM
 /temp
+/smtlib2_expr.smt2
+/smtlib2_expr.vcd
diff --git a/tests/various/smtlib2_expr.sh b/tests/various/smtlib2_expr.sh
new file mode 100755
index 000000000..dc0cc3ead
--- /dev/null
+++ b/tests/various/smtlib2_expr.sh
@@ -0,0 +1,4 @@
+#!/bin/bash
+set -ex
+../../yosys -q -p 'read_verilog -icells -formal smtlib2_expr.v; prep; write_smt2 -wires smtlib2_expr.smt2'
+../../yosys-smtbmc -s cvc4 --dump-vcd smtlib2_expr.vcd smtlib2_expr.smt2
diff --git a/tests/various/smtlib2_expr.v b/tests/various/smtlib2_expr.v
new file mode 100644
index 000000000..45b5b1ccc
--- /dev/null
+++ b/tests/various/smtlib2_expr.v
@@ -0,0 +1,28 @@
+module uut;
+    wire [7:0] a = $anyconst, b = $anyconst, add, add2, sub, sub2;
+    assign add2 = a + b;
+    assign sub2 = a - b;
+
+    \$smtlib2_expr #(
+        .A_WIDTH(16),
+        .Y_WIDTH(8),
+        .EXPR("(bvadd ((_ extract 15 8) A) ((_ extract 7 0) A))")
+    ) add_expr (
+        .A({a, b}),
+        .Y(add)
+    );
+
+    \$smtlib2_expr #(
+        .A_WIDTH(16),
+        .Y_WIDTH(8),
+        .EXPR("(bvadd ((_ extract 15 8) A) (bvneg ((_ extract 7 0) A)))")
+    ) sub_expr (
+        .A({a, b}),
+        .Y(sub)
+    );
+
+    always @* begin
+        assert(add == add2);
+        assert(sub == sub2);
+    end
+endmodule