summaryrefslogtreecommitdiff
path: root/backends/smt2
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-12-25 20:28:16 +0100
committerClifford Wolf <clifford@clifford.at>2014-12-25 20:28:34 +0100
commite8c12e5f0c49cca4dd54da12003bd010a488aee3 (patch)
tree008aecff3e87a644babb64e02a6a01af52962bb4 /backends/smt2
parentb748622a7f482cebc44c93ee065f36b159bb2a6c (diff)
Various fixes and improvements in "write_smt2 -bv"
Diffstat (limited to 'backends/smt2')
-rw-r--r--backends/smt2/.gitignore1
-rw-r--r--backends/smt2/smt2.cc35
-rw-r--r--backends/smt2/test_cells.sh18
3 files changed, 43 insertions, 11 deletions
diff --git a/backends/smt2/.gitignore b/backends/smt2/.gitignore
new file mode 100644
index 00000000..313ea0a1
--- /dev/null
+++ b/backends/smt2/.gitignore
@@ -0,0 +1 @@
+test_cells
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index c383bbab..8451eff4 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -215,9 +215,9 @@ struct Smt2Worker
bool is_signed = cell->getParam("\\A_SIGNED").as_bool();
int width = GetSize(sig_y);
- if (type == 's') {
- width = std::max(width, GetSize(sig_a));
- width = std::max(width, GetSize(sig_b));
+ if (type == 's' || type == 'd' || type == 'b') {
+ width = std::max(width, GetSize(cell->getPort("\\A")));
+ width = std::max(width, GetSize(cell->getPort("\\B")));
}
if (cell->hasPort("\\A")) {
@@ -240,7 +240,7 @@ struct Smt2Worker
else processed_expr += ch;
}
- if (width != GetSize(sig_y))
+ if (width != GetSize(sig_y) && type != 'b')
processed_expr = stringf("((_ extract %d 0) %s)", GetSize(sig_y)-1, processed_expr.c_str());
if (type == 'b') {
@@ -347,8 +347,8 @@ struct Smt2Worker
if (cell->type == "$add") return export_bvop(cell, "(bvadd A B)");
if (cell->type == "$sub") return export_bvop(cell, "(bvsub A B)");
if (cell->type == "$mul") return export_bvop(cell, "(bvmul A B)");
- 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 == "$div") return export_bvop(cell, "(bvUdiv A B)", 'd');
+ if (cell->type == "$mod") return export_bvop(cell, "(bvUrem A B)", 'd');
if (cell->type == "$reduce_and") return export_reduce(cell, "(and A)", true);
if (cell->type == "$reduce_or") return export_reduce(cell, "(or A)", false);
@@ -360,7 +360,28 @@ struct Smt2Worker
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
+ if (cell->type == "$mux" || cell->type == "$pmux")
+ {
+ int width = GetSize(cell->getPort("\\Y"));
+ std::string processed_expr = get_bv(cell->getPort("\\A"));
+
+ RTLIL::SigSpec sig_b = cell->getPort("\\B");
+ RTLIL::SigSpec sig_s = cell->getPort("\\S");
+ get_bv(sig_b);
+ get_bv(sig_s);
+
+ for (int i = 0; i < GetSize(sig_s); i++)
+ processed_expr = stringf("(ite %s %s %s)", get_bool(sig_s[i]).c_str(),
+ get_bv(sig_b.extract(i*width, width)).c_str(), processed_expr.c_str());
+
+ RTLIL::SigSpec sig = sigmap(cell->getPort("\\Y"));
+ decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
+ log_id(module), idcounter, log_id(module), width, processed_expr.c_str(), log_signal(sig)));
+ register_bv(sig, idcounter++);
+ return;
+ }
+
+ // FIXME: $slice $concat
log_error("Unsupported cell type %s for cell %s.%s.\n",
log_id(cell->type), log_id(module), log_id(cell));
diff --git a/backends/smt2/test_cells.sh b/backends/smt2/test_cells.sh
index 28d5c57f..34adb7af 100644
--- a/backends/smt2/test_cells.sh
+++ b/backends/smt2/test_cells.sh
@@ -6,7 +6,7 @@ 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'
+../../../yosys -p 'test_cell -muxdiv -w test all /$alu /$macc /$fa /$lcu /$lut /$shift /$shiftx'
cat > miter.tpl <<- EOT
; #model# (set-option :produce-models true)
@@ -18,7 +18,7 @@ cat > miter.tpl <<- EOT
; #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
+for x in $(set +x; ls test_*.il | sort -R); do
x=${x%.il}
cat > $x.ys <<- EOT
read_ilang $x.il
@@ -34,8 +34,11 @@ for x in test_*.il; do
dump
write_smt2 -bv -tpl miter.tpl $x.smt2
EOT
- ../../../yosys $x.ys
- cvc4 $x.smt2 > $x.result
+ ../../../yosys -q $x.ys
+ if ! cvc4 $x.smt2 > $x.result; then
+ cat $x.result
+ exit 1
+ fi
if ! grep unsat $x.result; then
echo "Proof failed! Extracting model..."
sed -i 's/^; #model# //' $x.smt2
@@ -43,3 +46,10 @@ for x in test_*.il; do
exit 1
fi
done
+
+set +x
+echo ""
+echo " All tests passed."
+echo ""
+exit 0
+