diff options
| author | Alberto Gonzalez <boqwxp@airmail.cc> | 2020-04-24 08:23:08 +0000 |
|---|---|---|
| committer | Alberto Gonzalez <boqwxp@airmail.cc> | 2020-07-01 19:51:46 +0000 |
| commit | ca3844d44e07a86d22d6026861cd405f80b0d321 (patch) | |
| tree | 346ecef15ece5fd8ea033749e9aff0599c3c61f2 /examples/smtbmc/glift/mux2.ys | |
| parent | 72cebef279357435cde115851bc095375763108c (diff) | |
| download | yosys-ca3844d44e07a86d22d6026861cd405f80b0d321.tar.gz yosys-ca3844d44e07a86d22d6026861cd405f80b0d321.tar.bz2 yosys-ca3844d44e07a86d22d6026861cd405f80b0d321.zip | |
glift: Add examples, including a number of benchmarks used in some academic works.
Diffstat (limited to 'examples/smtbmc/glift/mux2.ys')
| -rw-r--r-- | examples/smtbmc/glift/mux2.ys | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/examples/smtbmc/glift/mux2.ys b/examples/smtbmc/glift/mux2.ys new file mode 100644 index 000000000..6b2b98c89 --- /dev/null +++ b/examples/smtbmc/glift/mux2.ys @@ -0,0 +1,39 @@ +logger -expect log "SAT proof finished - no model found: SUCCESS!" 1 +logger -expect log "Number of cells:.*[\t ]12" 1 +logger -expect log "Number of cells:.*[\t ]20" 1 +logger -expect log "Problem is satisfiable with \\gate.__glift_weight = 11." 1 +logger -expect log "Problem is NOT satisfiable with \\gate.__glift_weight <= 10." 1 +logger -expect log "Wire \\gate.__glift_weight is minimized at 11." 1 +logger -expect log "Specializing .* from file with .* = 1." 2 +logger -expect log "Specializing .* from file with .* = 0." 4 +read_verilog <<EOT +module mux2(a, b, s, y); + input a, b, s; + output y; + + wire s_n = ~s; + wire t0 = s & a; + wire t1 = s_n & b; + assign y = t0 | t1; +endmodule +EOT +techmap +copy mux2 uut +copy mux2 spec +delete mux2 +glift -optimize-precise uut +glift -create-precise spec +design -push-copy +miter -equiv spec uut qbfmiter +flatten +delete spec uut +qbfsat -assume-outputs -assume-negative-polarity -write-solution mux2.soln qbfmiter +design -pop +copy uut solved +qbfsat -specialize-from-file mux2.soln solved +opt +miter -equiv spec solved proofmiter +flatten proofmiter +sat -prove trigger 0 proofmiter +delete proofmiter +stat solved spec |