From 68233baa1f3d6e3dcfec20583b0f37202035a589 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 25 Dec 2014 17:52:31 +0100 Subject: [PATCH] Various fixes and improvements in write_smt2 --- backends/smt2/smt2.cc | 75 +++++++++++++++++++++---------------- backends/smt2/test_cells.sh | 45 ++++++++++++++++++++++ 2 files changed, 88 insertions(+), 32 deletions(-) create mode 100644 backends/smt2/test_cells.sh diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index a5c015918..c383bbab9 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -133,7 +133,7 @@ struct Smt2Worker export_cell(bit_driver.at(bit)); sigmap.apply(sig); - for (int i = 0, j = 1; i < GetSize(sig); i += j) + for (int i = 0, j = 1; i < GetSize(sig); i += j, j = 1) { if (sig[i].wire == nullptr) { while (i+j < GetSize(sig) && sig[i+j].wire == nullptr) j++; @@ -167,7 +167,10 @@ struct Smt2Worker continue; } - while (i+j < GetSize(sig) && sig[i+j].wire && !fcache.count(sig[i+j])) j++; + std::set seen_bits = { sig[i] }; + while (i+j < GetSize(sig) && sig[i+j].wire && !fcache.count(sig[i+j]) && !seen_bits.count(sig[i+j])) + seen_bits.insert(sig[i+j]), j++; + decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n", log_id(module), idcounter, log_id(module), j, log_signal(sig.extract(i, j)))); subexpr.push_back(stringf("(|%s#%d| state)", log_id(module), idcounter)); @@ -205,14 +208,14 @@ struct Smt2Worker return; } - void export_bvop(RTLIL::Cell *cell, std::string expr, bool shift_op = false) + void export_bvop(RTLIL::Cell *cell, std::string expr, char type = 0) { RTLIL::SigSpec sig_a, sig_b; RTLIL::SigSpec sig_y = sigmap(cell->getPort("\\Y")); bool is_signed = cell->getParam("\\A_SIGNED").as_bool(); int width = GetSize(sig_y); - if (shift_op) { + if (type == 's') { width = std::max(width, GetSize(sig_a)); width = std::max(width, GetSize(sig_b)); } @@ -224,7 +227,7 @@ struct Smt2Worker if (cell->hasPort("\\B")) { sig_b = cell->getPort("\\B"); - sig_b.extend_u0(width, is_signed && !shift_op); + sig_b.extend_u0(width, is_signed && !(type == 's')); } std::string processed_expr; @@ -233,20 +236,26 @@ struct Smt2Worker if (ch == 'A') processed_expr += get_bv(sig_a); else if (ch == 'B') processed_expr += get_bv(sig_b); else if (ch == 'L') processed_expr += is_signed ? "a" : "l"; - else if (ch == 'U') processed_expr += is_signed ? "" : "u"; + else if (ch == 'U') processed_expr += is_signed ? "s" : "u"; else processed_expr += ch; } if (width != GetSize(sig_y)) processed_expr = stringf("((_ extract %d 0) %s)", GetSize(sig_y)-1, processed_expr.c_str()); - decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", - log_id(module), idcounter, log_id(module), GetSize(sig_y), processed_expr.c_str(), log_signal(sig_y))); - register_bv(sig_y, idcounter++); + if (type == 'b') { + decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n", + log_id(module), idcounter, log_id(module), processed_expr.c_str(), log_signal(sig_y))); + register_boolvec(sig_y, idcounter++); + } else { + decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", + log_id(module), idcounter, log_id(module), GetSize(sig_y), processed_expr.c_str(), log_signal(sig_y))); + register_bv(sig_y, idcounter++); + } return; } - void export_reduce(RTLIL::Cell *cell, std::string expr) + void export_reduce(RTLIL::Cell *cell, std::string expr, bool identity_val) { RTLIL::SigSpec sig_y = sigmap(cell->getPort("\\Y")); std::string processed_expr; @@ -256,6 +265,8 @@ struct Smt2Worker RTLIL::SigSpec sig = sigmap(cell->getPort(stringf("\\%c", ch))); for (auto bit : sig) processed_expr += " " + get_bool(bit); + if (GetSize(sig) == 1) + processed_expr += identity_val ? " true" : " false"; } else processed_expr += ch; @@ -312,22 +323,22 @@ struct Smt2Worker if (cell->type == "$xor") return export_bvop(cell, "(bvxor A B)"); if (cell->type == "$xnor") return export_bvop(cell, "(bvxnor A B)"); - if (cell->type == "$shl") return export_bvop(cell, "(bvshl A B)", true); - if (cell->type == "$shr") return export_bvop(cell, "(bvlshr A B)", true); - if (cell->type == "$sshl") return export_bvop(cell, "(bvshl A B)", true); - if (cell->type == "$sshr") return export_bvop(cell, "(bvLshr A B)", true); + if (cell->type == "$shl") return export_bvop(cell, "(bvshl A B)", 's'); + if (cell->type == "$shr") return export_bvop(cell, "(bvlshr A B)", 's'); + if (cell->type == "$sshl") return export_bvop(cell, "(bvshl A B)", 's'); + if (cell->type == "$sshr") return export_bvop(cell, "(bvLshr A B)", 's'); // FIXME: $shift $shiftx - if (cell->type == "$lt") return export_bvop(cell, "(bvUlt A B)"); - if (cell->type == "$le") return export_bvop(cell, "(bvUle A B)"); - if (cell->type == "$ge") return export_bvop(cell, "(bvUge A B)"); - if (cell->type == "$gt") return export_bvop(cell, "(bvUgt A B)"); + if (cell->type == "$lt") return export_bvop(cell, "(bvUlt A B)", 'b'); + if (cell->type == "$le") return export_bvop(cell, "(bvUle A B)", 'b'); + if (cell->type == "$ge") return export_bvop(cell, "(bvUge A B)", 'b'); + if (cell->type == "$gt") return export_bvop(cell, "(bvUgt A B)", 'b'); - if (cell->type == "$ne") return export_bvop(cell, "(distinct A B)"); - if (cell->type == "$nex") return export_bvop(cell, "(distinct A B)"); - if (cell->type == "$eq") return export_bvop(cell, "(= A B)"); - if (cell->type == "$eqx") return export_bvop(cell, "(= A B)"); + if (cell->type == "$ne") return export_bvop(cell, "(distinct A B)", 'b'); + if (cell->type == "$nex") return export_bvop(cell, "(distinct A B)", 'b'); + if (cell->type == "$eq") return export_bvop(cell, "(= A B)", 'b'); + if (cell->type == "$eqx") return export_bvop(cell, "(= A B)", 'b'); if (cell->type == "$not") return export_bvop(cell, "(bvnot A)"); if (cell->type == "$pos") return export_bvop(cell, "A"); @@ -339,15 +350,15 @@ struct Smt2Worker if (cell->type == "$div") return export_bvop(cell, "(bvUdiv A B)"); if (cell->type == "$mod") return export_bvop(cell, "(bvUrem A B)"); - if (cell->type == "$reduce_and") return export_reduce(cell, "(and A)"); - if (cell->type == "$reduce_or") return export_reduce(cell, "(or A)"); - if (cell->type == "$reduce_xor") return export_reduce(cell, "(xor A)"); - if (cell->type == "$reduce_xnor") return export_reduce(cell, "(not (xor A))"); - if (cell->type == "$reduce_bool") return export_reduce(cell, "(or A)"); + if (cell->type == "$reduce_and") return export_reduce(cell, "(and A)", true); + if (cell->type == "$reduce_or") return export_reduce(cell, "(or A)", false); + if (cell->type == "$reduce_xor") return export_reduce(cell, "(xor A)", false); + if (cell->type == "$reduce_xnor") return export_reduce(cell, "(not (xor A))", false); + if (cell->type == "$reduce_bool") return export_reduce(cell, "(or A)", false); - if (cell->type == "$logic_not") return export_reduce(cell, "(not (or A))"); - if (cell->type == "$logic_and") return export_reduce(cell, "(and (or A) (or B))"); - if (cell->type == "$logic_or") return export_reduce(cell, "(or A B)"); + if (cell->type == "$logic_not") return export_reduce(cell, "(not (or A))", false); + if (cell->type == "$logic_and") return export_reduce(cell, "(and (or A) (or B))", false); + if (cell->type == "$logic_or") return export_reduce(cell, "(or A B)", false); // FIXME: $slice $concat $mux $pmux @@ -407,8 +418,8 @@ struct Smt2Backend : public Backend { log("'' this will declare the sort '_s' (state of the module) and the the\n"); log("function '_t' (state transition function).\n"); log("\n"); - log("The '_s' sort represents the a module state. Additional '_n' functions\n"); - log("are provided that can be used to access the values of all signals in the module.\n"); + log("The '_s' sort represents a module state. Additional '_n' functions\n"); + log("are provided that can be used to access the values of the signals in the module.\n"); log("Only ports, and signals with the 'keep' attribute set are made available via\n"); log("such functions. Without the -bv option, multi-bit wires are exported as\n"); log("separate functions of type Bool for the individual bits. With the -bv option\n"); diff --git a/backends/smt2/test_cells.sh b/backends/smt2/test_cells.sh new file mode 100644 index 000000000..28d5c57f5 --- /dev/null +++ b/backends/smt2/test_cells.sh @@ -0,0 +1,45 @@ +#!/bin/bash + +set -ex + +rm -rf test_cells +mkdir test_cells +cd test_cells + +../../../yosys -p 'test_cell -n 2 -w test all /$alu /$macc /$fa /$lcu /$lut /$shift /$shiftx /$div /$mod' + +cat > miter.tpl <<- EOT +; #model# (set-option :produce-models true) +(set-logic QF_UFBV) +%% +(declare-fun s () miter_s) +(assert (|miter_n trigger| s)) +(check-sat) +; #model# (get-value ((|miter_n in_A| s) (|miter_n in_B| s) (|miter_n gold_Y| s) (|miter_n gate_Y| s) (|miter_n trigger| s))) +EOT + +for x in test_*.il; do + x=${x%.il} + cat > $x.ys <<- EOT + read_ilang $x.il + copy gold gate + + cd gate + techmap; opt; abc;; + cd .. + + miter -equiv -flatten -make_outputs gold gate miter + hierarchy -check -top miter + + dump + write_smt2 -bv -tpl miter.tpl $x.smt2 + EOT + ../../../yosys $x.ys + cvc4 $x.smt2 > $x.result + if ! grep unsat $x.result; then + echo "Proof failed! Extracting model..." + sed -i 's/^; #model# //' $x.smt2 + cvc4 $x.smt2 + exit 1 + fi +done -- 2.30.2