add $smtlib2_expr

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index a3628197ec64a0b027331e8a0cdd2716284793e9..ed7e1795166d35b725f0aa8f5f3bd6f0dc28ddee 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 7e9cfb38d2d99f8a6a949acf712ed63bef23db52..7a9eff1fc0ed58b80366ef275568b4653c415589 100644 (file)
--- 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 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 72dcb89af22e51fae7f61229a34270373689b730..c91b2bb71be770da02c636918b038dbef79455f4 100644 (file)
--- 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 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 b14488ff44691e74771709e1054d3c78cd54d921..789b97a5f02193cd2fb3e0c96117407307a5705b 100644 (file)
--- 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 91d385b80a795219b685fc9fe38f2f89a8ea13bf..45c90f8979c9ab7f0a40eca75d651e2a0a86eb36 100644 (file)
--- 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 c6373468a25438da8d77e03ea170b1943d0d19d5..bc7f447aeeba573eac63280440a6ab45087fbc6e 100644 (file)
--- 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 (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