smt2: Add smtlib2_comb_expr attribute to allow user-selected smtlib2 expressions

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index ed6f3aff980cf4d0308b42701cccf2aa491e8a51..aa865e7fa66be9e30af4f963098f7f8d6fbcfbf0 100644 (file)
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -53,6 +53,8 @@ struct Smt2Worker
        std::map<int, int> bvsizes;
        dict<IdString, char*> ids;
 
+       bool is_smtlib2_module;
+
        const char *get_id(IdString n)
        {
                if (ids.count(n) == 0) {
@@ -112,9 +114,10 @@ struct Smt2Worker
        }
 
        Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose, bool statebv, bool statedt, bool forallmode,
-                       dict<IdString, int> &mod_stbv_width, dict<IdString, dict<IdString, pair<bool, bool>>> &mod_clk_cache) :
-                       ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode), wiresmode(wiresmode),
-                       verbose(verbose), statebv(statebv), statedt(statedt), forallmode(forallmode), mod_stbv_width(mod_stbv_width)
+                  dict<IdString, int> &mod_stbv_width, dict<IdString, dict<IdString, pair<bool, bool>>> &mod_clk_cache)
+           : ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode), wiresmode(wiresmode), verbose(verbose),
+             statebv(statebv), statedt(statedt), forallmode(forallmode), mod_stbv_width(mod_stbv_width),
+             is_smtlib2_module(module->has_attribute(ID::smtlib2_module))
        {
                pool<SigBit> noclock;
 
@@ -124,6 +127,9 @@ struct Smt2Worker
                memories = Mem::get_all_memories(module);
                for (auto &mem : memories)
                {
+                       if (is_smtlib2_module)
+                               log_error("Memory %s.%s not allowed in module with smtlib2_module attribute", get_id(module), mem.memid.c_str());
+
                        mem.narrow();
                        mem_dict[mem.memid] = &mem;
                        for (auto &port : mem.wr_ports)
@@ -893,10 +899,25 @@ struct Smt2Worker
                                log_id(cell->type), log_id(module), log_id(cell));
        }
 
+       void verify_smtlib2_module()
+       {
+               if (!module->get_blackbox_attribute())
+                       log_error("Module %s with smtlib2_module attribute must also have blackbox attribute.\n", log_id(module));
+               if (module->cells().size() > 0)
+                       log_error("Module %s with smtlib2_module attribute must not have any cells inside it.\n", log_id(module));
+               for (auto wire : module->wires())
+                       if (!wire->port_id)
+                               log_error("Wire %s.%s must be input or output since module has smtlib2_module attribute.\n", log_id(module),
+                                         log_id(wire));
+       }
+
        void run()
        {
                if (verbose) log("=> export logic driving outputs\n");
 
+               if (is_smtlib2_module)
+                       verify_smtlib2_module();
+
                pool<SigBit> reg_bits;
                for (auto cell : module->cells())
                        if (cell->type.in(ID($ff), ID($dff), ID($_FF_), ID($_DFF_P_), ID($_DFF_N_))) {
@@ -905,11 +926,24 @@ struct Smt2Worker
                                        reg_bits.insert(bit);
                        }
 
+               std::string smtlib2_inputs;
+               if (is_smtlib2_module) {
+                       for (auto wire : module->wires()) {
+                               if (!wire->port_input)
+                                       continue;
+                               smtlib2_inputs += stringf("(|%s| (|%s_n %s| state))\n", get_id(wire), get_id(module), get_id(wire));
+                       }
+               }
+
                for (auto wire : module->wires()) {
                        bool is_register = false;
                        for (auto bit : SigSpec(wire))
                                if (reg_bits.count(bit))
                                        is_register = true;
+                       bool is_smtlib2_comb_expr = wire->has_attribute(ID::smtlib2_comb_expr);
+                       if (is_smtlib2_comb_expr && !is_smtlib2_module)
+                               log_error("smtlib2_comb_expr is only valid in a module with the smtlib2_module attribute: wire %s.%s", log_id(module),
+                                         log_id(wire));
                        if (wire->port_id || is_register || wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name.isPublic())) {
                                RTLIL::SigSpec sig = sigmap(wire);
                                std::vector<std::string> comments;
@@ -924,8 +958,18 @@ struct Smt2Worker
                                if (GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig)))
                                        comments.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire),
                                                        clock_posedge.count(sig) ? " posedge" : "", clock_negedge.count(sig) ? " negedge" : ""));
+                               std::string smtlib2_comb_expr;
+                               if (is_smtlib2_comb_expr) {
+                                       smtlib2_comb_expr =
+                                         "(let (\n" + smtlib2_inputs + ")\n" + wire->get_string_attribute(ID::smtlib2_comb_expr) + "\n)";
+                                       if (wire->port_input || !wire->port_output)
+                                               log_error("smtlib2_comb_expr is only valid on output: wire %s.%s", log_id(module), log_id(wire));
+                                       if (!bvmode && GetSize(sig) > 1)
+                                               log_error("smtlib2_comb_expr is unsupported on multi-bit wires when -nobv is specified: wire %s.%s",
+                                                         log_id(module), log_id(wire));
+                               }
                                if (bvmode && GetSize(sig) > 1) {
-                                       std::string sig_bv = get_bv(sig);
+                                       std::string sig_bv = is_smtlib2_comb_expr ? smtlib2_comb_expr : get_bv(sig);
                                        if (!comments.empty())
                                                decls.insert(decls.end(), comments.begin(), comments.end());
                                        decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n",
@@ -936,7 +980,7 @@ struct Smt2Worker
                                } else {
                                        std::vector<std::string> sig_bool;
                                        for (int i = 0; i < GetSize(sig); i++) {
-                                               sig_bool.push_back(get_bool(sig[i]));
+                                               sig_bool.push_back(is_smtlib2_comb_expr ? smtlib2_comb_expr : get_bool(sig[i]));
                                        }
                                        if (!comments.empty())
                                                decls.insert(decls.end(), comments.begin(), comments.end());
@@ -964,6 +1008,10 @@ struct Smt2Worker
                vector<string> init_list;
                for (auto wire : module->wires())
                        if (wire->attributes.count(ID::init)) {
+                               if (is_smtlib2_module)
+                                       log_error("init attribute not allowed on wires in module with smtlib2_module attribute: wire %s.%s",
+                                                 log_id(module), log_id(wire));
+
                                RTLIL::SigSpec sig = sigmap(wire);
                                Const val = wire->attributes.at(ID::init);
                                val.bits.resize(GetSize(sig), State::Sx);
@@ -1687,7 +1735,10 @@ struct Smt2Backend : public Backend {
 
                for (auto module : sorted_modules)
                {
-                       if (module->get_blackbox_attribute() || module->has_processes_warn())
+                       if (module->get_blackbox_attribute() && !module->has_attribute(ID::smtlib2_module))
+                               continue;
+
+                       if (module->has_processes_warn())
                                continue;
 
                        log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module));

diff --git a/kernel/constids.inc b/kernel/constids.inc
index 443ac3bcb19c1cdb44a256e12909d544d5afb96a..0f6dfc29bac4135c1f6749adec0fd3c3b27bf5c0 100644 (file)
--- a/kernel/constids.inc
+++ b/kernel/constids.inc
@@ -196,6 +196,8 @@ X(STATE_NUM)
 X(STATE_NUM_LOG2)
 X(STATE_RST)
 X(STATE_TABLE)
+X(smtlib2_module)
+X(smtlib2_comb_expr)
 X(submod)
 X(syn_ramstyle)
 X(syn_romstyle)

diff --git a/tests/various/.gitignore b/tests/various/.gitignore
index c6373468a25438da8d77e03ea170b1943d0d19d5..da78b6ec59de1e179f5ab2e2d41535ccfe6df366 100644 (file)
--- a/tests/various/.gitignore
+++ b/tests/various/.gitignore
@@ -6,3 +6,4 @@
 /plugin.so
 /plugin.so.dSYM
 /temp
+/smtlib2_module.smt2

diff --git a/tests/various/smtlib2_module-expected.smt2 b/tests/various/smtlib2_module-expected.smt2
new file mode 100644 (file)
index 0000000..bb869c0
--- /dev/null
+++ b/tests/various/smtlib2_module-expected.smt2
@@ -0,0 +1,88 @@
+; SMT-LIBv2 description generated by Yosys $VERSION
+; yosys-smt2-module smtlib2
+(declare-sort |smtlib2_s| 0)
+(declare-fun |smtlib2_is| (|smtlib2_s|) Bool)
+(declare-fun |smtlib2#0| (|smtlib2_s|) (_ BitVec 8)) ; \a
+; yosys-smt2-input a 8
+(define-fun |smtlib2_n a| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#0| state))
+; yosys-smt2-output add 8
+(define-fun |smtlib2_n add| ((state |smtlib2_s|)) (_ BitVec 8) (let (
+(|a| (|smtlib2_n a| state))
+(|b| (|smtlib2_n b| state))
+)
+(bvadd a b)
+))
+(declare-fun |smtlib2#1| (|smtlib2_s|) (_ BitVec 8)) ; \b
+; yosys-smt2-input b 8
+(define-fun |smtlib2_n b| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#1| state))
+; yosys-smt2-output eq 1
+(define-fun |smtlib2_n eq| ((state |smtlib2_s|)) Bool (let (
+(|a| (|smtlib2_n a| state))
+(|b| (|smtlib2_n b| state))
+)
+(= a b)
+))
+; yosys-smt2-output sub 8
+(define-fun |smtlib2_n sub| ((state |smtlib2_s|)) (_ BitVec 8) (let (
+(|a| (|smtlib2_n a| state))
+(|b| (|smtlib2_n b| state))
+)
+(bvadd a (bvneg b))
+))
+(define-fun |smtlib2_a| ((state |smtlib2_s|)) Bool true)
+(define-fun |smtlib2_u| ((state |smtlib2_s|)) Bool true)
+(define-fun |smtlib2_i| ((state |smtlib2_s|)) Bool true)
+(define-fun |smtlib2_h| ((state |smtlib2_s|)) Bool true)
+(define-fun |smtlib2_t| ((state |smtlib2_s|) (next_state |smtlib2_s|)) Bool true) ; end of module smtlib2
+; yosys-smt2-module uut
+(declare-sort |uut_s| 0)
+(declare-fun |uut_is| (|uut_s|) Bool)
+; yosys-smt2-cell smtlib2 s
+(declare-fun |uut#0| (|uut_s|) (_ BitVec 8)) ; \add
+(declare-fun |uut#1| (|uut_s|) Bool) ; \eq
+(declare-fun |uut#2| (|uut_s|) (_ BitVec 8)) ; \sub
+(declare-fun |uut_h s| (|uut_s|) |smtlib2_s|)
+; yosys-smt2-anyconst uut#3 8 smtlib2_module.v:14.17-14.26
+(declare-fun |uut#3| (|uut_s|) (_ BitVec 8)) ; \a
+; yosys-smt2-anyconst uut#4 8 smtlib2_module.v:14.32-14.41
+(declare-fun |uut#4| (|uut_s|) (_ BitVec 8)) ; \b
+(define-fun |uut#5| ((state |uut_s|)) (_ BitVec 8) (bvadd (|uut#3| state) (|uut#4| state))) ; \add2
+(define-fun |uut#6| ((state |uut_s|)) Bool (= (|uut#0| state) (|uut#5| state))) ; $0$formal$smtlib2_module.v:28$1_CHECK[0:0]$9
+; yosys-smt2-assert 0 $assert$smtlib2_module.v:28$19 smtlib2_module.v:28.17-29.22
+(define-fun |uut_a 0| ((state |uut_s|)) Bool (or (|uut#6| state) (not true))) ; $assert$smtlib2_module.v:28$19
+(define-fun |uut#7| ((state |uut_s|)) (_ BitVec 8) (bvsub (|uut#3| state) (|uut#4| state))) ; \sub2
+(define-fun |uut#8| ((state |uut_s|)) Bool (= (|uut#2| state) (|uut#7| state))) ; $0$formal$smtlib2_module.v:29$2_CHECK[0:0]$11
+; yosys-smt2-assert 1 $assert$smtlib2_module.v:29$20 smtlib2_module.v:29.23-30.22
+(define-fun |uut_a 1| ((state |uut_s|)) Bool (or (|uut#8| state) (not true))) ; $assert$smtlib2_module.v:29$20
+(define-fun |uut#9| ((state |uut_s|)) Bool (= (|uut#3| state) (|uut#4| state))) ; $eq$smtlib2_module.v:31$17_Y
+(define-fun |uut#10| ((state |uut_s|)) Bool (= (ite (|uut#1| state) #b1 #b0) (ite (|uut#9| state) #b1 #b0))) ; $0$formal$smtlib2_module.v:30$3_CHECK[0:0]$13
+; yosys-smt2-assert 2 $assert$smtlib2_module.v:30$21 smtlib2_module.v:30.23-31.25
+(define-fun |uut_a 2| ((state |uut_s|)) Bool (or (|uut#10| state) (not true))) ; $assert$smtlib2_module.v:30$21
+(define-fun |uut_a| ((state |uut_s|)) Bool (and
+  (|uut_a 0| state)
+  (|uut_a 1| state)
+  (|uut_a 2| state)
+  (|smtlib2_a| (|uut_h s| state))
+))
+(define-fun |uut_u| ((state |uut_s|)) Bool 
+  (|smtlib2_u| (|uut_h s| state))
+)
+(define-fun |uut_i| ((state |uut_s|)) Bool 
+  (|smtlib2_i| (|uut_h s| state))
+)
+(define-fun |uut_h| ((state |uut_s|)) Bool (and
+  (= (|uut_is| state) (|smtlib2_is| (|uut_h s| state)))
+  (= (|uut#3| state) (|smtlib2_n a| (|uut_h s| state))) ; smtlib2.a
+  (= (|uut#0| state) (|smtlib2_n add| (|uut_h s| state))) ; smtlib2.add
+  (= (|uut#4| state) (|smtlib2_n b| (|uut_h s| state))) ; smtlib2.b
+  (= (|uut#1| state) (|smtlib2_n eq| (|uut_h s| state))) ; smtlib2.eq
+  (= (|uut#2| state) (|smtlib2_n sub| (|uut_h s| state))) ; smtlib2.sub
+  (|smtlib2_h| (|uut_h s| state))
+))
+(define-fun |uut_t| ((state |uut_s|) (next_state |uut_s|)) Bool (and
+  (= (|uut#4| state) (|uut#4| next_state)) ; $anyconst$5 \b
+  (= (|uut#3| state) (|uut#3| next_state)) ; $anyconst$4 \a
+  (|smtlib2_t| (|uut_h s| state) (|uut_h s| next_state))
+)) ; end of module uut
+; yosys-smt2-topmod uut
+; end of yosys output

diff --git a/tests/various/smtlib2_module.sh b/tests/various/smtlib2_module.sh
new file mode 100755 (executable)
index 0000000..2dbd664
--- /dev/null
+++ b/tests/various/smtlib2_module.sh
@@ -0,0 +1,5 @@
+#!/bin/bash
+set -ex
+../../yosys -q -p 'read_verilog -formal smtlib2_module.v; prep; write_smt2 smtlib2_module.smt2'
+sed -i 's/; SMT-LIBv2 description generated by Yosys .*/; SMT-LIBv2 description generated by Yosys $VERSION/' smtlib2_module.smt2
+diff -auN smtlib2_module-expected.smt2 smtlib2_module.smt2

diff --git a/tests/various/smtlib2_module.v b/tests/various/smtlib2_module.v
new file mode 100644 (file)
index 0000000..4aad869
--- /dev/null
+++ b/tests/various/smtlib2_module.v
@@ -0,0 +1,33 @@
+(* smtlib2_module *)
+module smtlib2(a, b, add, sub, eq);
+       input [7:0] a, b;
+       (* smtlib2_comb_expr = "(bvadd a b)" *)
+       output [7:0] add;
+       (* smtlib2_comb_expr = "(bvadd a (bvneg b))" *)
+       output [7:0] sub;
+       (* smtlib2_comb_expr = "(= a b)" *)
+       output eq;
+endmodule
+
+(* top *)
+module uut;
+       wire [7:0] a = $anyconst, b = $anyconst, add, sub, add2, sub2;
+       wire eq;
+
+       assign add2 = a + b;
+       assign sub2 = a - b;
+
+       smtlib2 s (
+               .a(a),
+               .b(b),
+               .add(add),
+               .sub(sub),
+               .eq(eq)
+       );
+
+       always @* begin
+               assert(add == add2);
+               assert(sub == sub2);
+               assert(eq == (a == b));
+       end
+endmodule