From ac22f1764d5a9f8dbe70f70b1acf6b7dc65c1ced Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 7 Jun 2022 17:37:04 +0200 Subject: [PATCH] smt2: emit smtlib2_comb_expr outputs after all inputs --- backends/smt2/smt2.cc | 14 +++++++++----- tests/various/smtlib2_module-expected.smt2 | 10 +++++----- tests/various/smtlib2_module.sh | 2 +- 3 files changed, 15 insertions(+), 11 deletions(-) diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index aa865e7fa..7481e0510 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -927,6 +927,7 @@ struct Smt2Worker } std::string smtlib2_inputs; + std::vector smtlib2_decls; if (is_smtlib2_module) { for (auto wire : module->wires()) { if (!wire->port_input) @@ -968,11 +969,12 @@ struct Smt2Worker log_error("smtlib2_comb_expr is unsupported on multi-bit wires when -nobv is specified: wire %s.%s", log_id(module), log_id(wire)); } + auto &out_decls = is_smtlib2_comb_expr ? smtlib2_decls : decls; if (bvmode && GetSize(sig) > 1) { 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", + out_decls.insert(out_decls.end(), comments.begin(), comments.end()); + out_decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n", get_id(module), get_id(wire), get_id(module), GetSize(sig), sig_bv.c_str())); if (wire->port_input) ex_input_eq.push_back(stringf(" (= (|%s_n %s| state) (|%s_n %s| other_state))", @@ -983,16 +985,16 @@ struct Smt2Worker 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()); + out_decls.insert(out_decls.end(), comments.begin(), comments.end()); for (int i = 0; i < GetSize(sig); i++) { if (GetSize(sig) > 1) { - decls.push_back(stringf("(define-fun |%s_n %s %d| ((state |%s_s|)) Bool %s)\n", + out_decls.push_back(stringf("(define-fun |%s_n %s %d| ((state |%s_s|)) Bool %s)\n", get_id(module), get_id(wire), i, get_id(module), sig_bool[i].c_str())); if (wire->port_input) ex_input_eq.push_back(stringf(" (= (|%s_n %s %d| state) (|%s_n %s %d| other_state))", get_id(module), get_id(wire), i, get_id(module), get_id(wire), i)); } else { - decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) Bool %s)\n", + out_decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) Bool %s)\n", get_id(module), get_id(wire), get_id(module), sig_bool[i].c_str())); if (wire->port_input) ex_input_eq.push_back(stringf(" (= (|%s_n %s| state) (|%s_n %s| other_state))", @@ -1003,6 +1005,8 @@ struct Smt2Worker } } + decls.insert(decls.end(), smtlib2_decls.begin(), smtlib2_decls.end()); + if (verbose) log("=> export logic associated with the initial state\n"); vector init_list; diff --git a/tests/various/smtlib2_module-expected.smt2 b/tests/various/smtlib2_module-expected.smt2 index bb869c08a..ace858ca8 100644 --- a/tests/various/smtlib2_module-expected.smt2 +++ b/tests/various/smtlib2_module-expected.smt2 @@ -5,6 +5,9 @@ (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)) +(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 add 8 (define-fun |smtlib2_n add| ((state |smtlib2_s|)) (_ BitVec 8) (let ( (|a| (|smtlib2_n a| state)) @@ -12,9 +15,6 @@ ) (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)) @@ -64,10 +64,10 @@ (|uut_a 2| state) (|smtlib2_a| (|uut_h s| state)) )) -(define-fun |uut_u| ((state |uut_s|)) Bool +(define-fun |uut_u| ((state |uut_s|)) Bool (|smtlib2_u| (|uut_h s| state)) ) -(define-fun |uut_i| ((state |uut_s|)) Bool +(define-fun |uut_i| ((state |uut_s|)) Bool (|smtlib2_i| (|uut_h s| state)) ) (define-fun |uut_h| ((state |uut_s|)) Bool (and diff --git a/tests/various/smtlib2_module.sh b/tests/various/smtlib2_module.sh index 9b2f24f9f..491f65148 100755 --- a/tests/various/smtlib2_module.sh +++ b/tests/various/smtlib2_module.sh @@ -1,5 +1,5 @@ #!/bin/bash set -ex ../../yosys -q -p 'read_verilog -formal smtlib2_module.v; prep; write_smt2 smtlib2_module.smt2' -sed 's/; SMT-LIBv2 description generated by Yosys .*/; SMT-LIBv2 description generated by Yosys $VERSION/' smtlib2_module.smt2 > smtlib2_module-filtered.smt2 +sed 's/; SMT-LIBv2 description generated by Yosys .*/; SMT-LIBv2 description generated by Yosys $VERSION/;s/ *$//' smtlib2_module.smt2 > smtlib2_module-filtered.smt2 diff -au smtlib2_module-expected.smt2 smtlib2_module-filtered.smt2 -- 2.30.2