add $smtlib2_expr

(cherry picked from commit 4bf43c5ee227c0b64c6fff8276afa9b17bf36b94)

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index f2fa003bcb665bc2d29409b1d0c711cb67121d24..547d85ae9eae764a4ff6902c34086f4f60e2e79e 100644 (file)
--- 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 879ac0edc0b34bb0bcdfb250b3d75614992f1c21..b3dad6dc7208815bb29c30fd06178f147749861b 100644 (file)
--- a/kernel/celltypes.h
+++ b/kernel/celltypes.h
@@ -173,6 +173,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 566b76217737c7bdea2a6e083fb8141a2658a298..d6202663d0e8a1f58b99dd141f3e41505e37e4e3 100644 (file)
--- 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 cd0f5ab1246c8cd6aed4a57cfe500326f45c82f1..7f55a798e4a6a7a67bec91ccdb98bc2bad31b1eb 100644 (file)
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -1605,6 +1605,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 3c9fb31ccc4c3575bfdf57239d321e30870b2eeb..2727e4dc4b78118e540119f77661fb51b07cea9e 100644 (file)
--- 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 e9129f690118e70be0e7dbf6e46f46c0c30b8b0d..dbea327bc1e9864f24292d94fc3514811f9f3cd5 100644 (file)
--- a/techlibs/common/simlib.v
+++ b/techlibs/common/simlib.v
@@ -2565,3 +2565,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 667773e1bfb9d6a352b289bf8ad1ffbdb59e918a..71e70ef40d0f783c6316346745f0000fedcac283 100644 (file)
--- a/techlibs/common/techmap.v
+++ b/techlibs/common/techmap.v
@@ -609,3 +609,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 2bb6c71793ce6e35e51c9eb94829acdf53226925..bc7f447aeeba573eac63280440a6ab45087fbc6e 100644 (file)
--- a/tests/various/.gitignore
+++ b/tests/various/.gitignore
@@ -5,3 +5,6 @@
 /run-test.mk
 /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 (executable)
index 0000000..dc0cc3e
--- /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 (file)
index 0000000..45b5b1c
--- /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