riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Merge pull request #3367 from jix/smtlib2-module-fixes 

smt2: emit smtlib2_comb_expr outputs after all inputs
This commit is contained in:
Jannis Harder 2022-06-07 19:45:47 +02:00 committed by GitHub
parent 5f9a97d234 ac22f1764d
commit d9bb10ba5f
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 15 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
backends/smt2/smt2.cc
View File

@ -927,6 +927,7 @@ struct Smt2Worker
} }
std::string smtlib2_inputs; std::string smtlib2_inputs;
std::vector<std::string> smtlib2_decls;
if (is_smtlib2_module) { if (is_smtlib2_module) {
for (auto wire : module->wires()) { for (auto wire : module->wires()) {
if (!wire->port_input) 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_error("smtlib2_comb_expr is unsupported on multi-bit wires when -nobv is specified: wire %s.%s",
log_id(module), log_id(wire)); log_id(module), log_id(wire));
} }
auto &out_decls = is_smtlib2_comb_expr ? smtlib2_decls : decls;
if (bvmode && GetSize(sig) > 1) { if (bvmode && GetSize(sig) > 1) {
std::string sig_bv = is_smtlib2_comb_expr ? smtlib2_comb_expr : get_bv(sig); std::string sig_bv = is_smtlib2_comb_expr ? smtlib2_comb_expr : get_bv(sig);
if (!comments.empty()) if (!comments.empty())
decls.insert(decls.end(), comments.begin(), comments.end()); out_decls.insert(out_decls.end(), comments.begin(), comments.end());
decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n", 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())); get_id(module), get_id(wire), get_id(module), GetSize(sig), sig_bv.c_str()));
if (wire->port_input) if (wire->port_input)
ex_input_eq.push_back(stringf(" (= (|%s_n %s| state) (|%s_n %s| other_state))", 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])); sig_bool.push_back(is_smtlib2_comb_expr ? smtlib2_comb_expr : get_bool(sig[i]));
} }
if (!comments.empty()) 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++) { for (int i = 0; i < GetSize(sig); i++) {
if (GetSize(sig) > 1) { 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())); get_id(module), get_id(wire), i, get_id(module), sig_bool[i].c_str()));
if (wire->port_input) if (wire->port_input)
ex_input_eq.push_back(stringf(" (= (|%s_n %s %d| state) (|%s_n %s %d| other_state))", 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)); get_id(module), get_id(wire), i, get_id(module), get_id(wire), i));
} else { } 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())); get_id(module), get_id(wire), get_id(module), sig_bool[i].c_str()));
if (wire->port_input) if (wire->port_input)
ex_input_eq.push_back(stringf(" (= (|%s_n %s| state) (|%s_n %s| other_state))", 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"); if (verbose) log("=> export logic associated with the initial state\n");
vector<string> init_list; vector<string> init_list;

10
tests/various/smtlib2_module-expected.smt2
View File

@ -5,6 +5,9 @@
(declare-fun |smtlib2#0| (|smtlib2_s|) (_ BitVec 8)) ; \a (declare-fun |smtlib2#0| (|smtlib2_s|) (_ BitVec 8)) ; \a
; yosys-smt2-input a 8 ; yosys-smt2-input a 8
(define-fun |smtlib2_n a| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#0| state)) (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 ; yosys-smt2-output add 8
(define-fun |smtlib2_n add| ((state |smtlib2_s|)) (_ BitVec 8) (let ( (define-fun |smtlib2_n add| ((state |smtlib2_s|)) (_ BitVec 8) (let (
(|a| (|smtlib2_n a| state)) (|a| (|smtlib2_n a| state))
@ -12,9 +15,6 @@
) )
(bvadd a b) (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 ; yosys-smt2-output eq 1
(define-fun |smtlib2_n eq| ((state |smtlib2_s|)) Bool (let ( (define-fun |smtlib2_n eq| ((state |smtlib2_s|)) Bool (let (
(|a| (|smtlib2_n a| state)) (|a| (|smtlib2_n a| state))
@ -64,10 +64,10 @@
(|uut_a 2| state) (|uut_a 2| state)
(|smtlib2_a| (|uut_h s| 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)) (|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)) (|smtlib2_i| (|uut_h s| state))
) )
(define-fun |uut_h| ((state |uut_s|)) Bool (and (define-fun |uut_h| ((state |uut_s|)) Bool (and

2
tests/various/smtlib2_module.sh
View File

@ -1,5 +1,5 @@
#!/bin/bash #!/bin/bash
set -ex set -ex
../../yosys -q -p 'read_verilog -formal smtlib2_module.v; prep; write_smt2 smtlib2_module.smt2' ../../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 diff -au smtlib2_module-expected.smt2 smtlib2_module-filtered.smt2