9 ..
/..
/..
/yosys
-p 'test_cell -muxdiv -w test all /$alu /$macc /$fa /$lcu /$lut /$shift /$shiftx'
11 cat > miter.tpl
<<- EOT
12 ; #model# (set-option :produce-models true)
15 (declare-fun s () miter_s)
16 (assert (|miter_n trigger| s))
18 ; #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)))
21 for x
in $
(set +x
; ls test_
*.il |
sort -R); do
31 miter -equiv -flatten -make_outputs gold gate miter
32 hierarchy -check -top miter
35 write_smt2 -bv -tpl miter.tpl $x.smt2
37 ..
/..
/..
/yosys
-q $x.ys
38 if ! cvc4
$x.smt2
> $x.result
; then
42 if ! grep unsat
$x.result
; then
43 echo "Proof failed! Extracting model..."
44 sed -i 's/^; #model# //' $x.smt2
52 echo " All tests passed."