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/too_large.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/too_large.ys')
| -rw-r--r-- | examples/smtbmc/glift/too_large.ys | 45 |
1 files changed, 45 insertions, 0 deletions
diff --git a/examples/smtbmc/glift/too_large.ys b/examples/smtbmc/glift/too_large.ys new file mode 100644 index 000000000..e14c2b7b6 --- /dev/null +++ b/examples/smtbmc/glift/too_large.ys @@ -0,0 +1,45 @@ +read_verilog too_large.v +techmap +flatten +select too_large_lev2 +glift -optimize-precise +techmap +opt +rename too_large_lev2 uut +cd .. +delete [AIONX][NVXR]2 +read_verilog too_large.v +techmap +flatten +select too_large_lev2 +glift -create-precise +techmap +opt +rename too_large_lev2 spec +cd .. +delete [AIONX][NVXR]2 + +design -push-copy +miter -equiv spec uut miter +flatten +delete uut spec +techmap +opt +stat miter +abc -script +print_stats;strash;print_stats;drwsat;print_stats;print_stats;fraig;print_stats;dc2,-l,-b;print_stats;irw,-l,-z;print_stats;refactor,-N,15,-z;print_stats;dch,-S,50000,-C,10000;print_stats;dc2,-l;print_stats;fraig,-C,10000;print_stats miter +techmap +opt +stat +qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution too_large.soln -show-smtbmc -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter +design -pop +stat + +copy uut solved +qbfsat -specialize-from-file too_large.soln solved +opt solved +miter -equiv spec solved satmiter +flatten +sat -prove trigger 0 satmiter +delete satmiter +stat +shell |