From: Jacob Lifshay Date: Fri, 3 Jun 2022 05:37:29 +0000 (-0700) Subject: smt2: Add smtlib2_comb_expr attribute to allow user-selected smtlib2 expressions X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cd57c5adb39d2343e81ed1024cb2848983bfede2;p=yosys.git 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 ed6f3aff9..aa865e7fa 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -53,6 +53,8 @@ struct Smt2Worker std::map bvsizes; dict 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 &mod_stbv_width, dict>> &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 &mod_stbv_width, dict>> &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 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 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 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 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 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 443ac3bcb..0f6dfc29b 100644 --- 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 c6373468a..da78b6ec5 100644 --- 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 index 000000000..bb869c08a --- /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 index 000000000..2dbd664fa --- /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 index 000000000..4aad86905 --- /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