diff options
Diffstat (limited to 'examples/smtbmc/glift/alu4.ys')
| -rw-r--r-- | examples/smtbmc/glift/alu4.ys | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/examples/smtbmc/glift/alu4.ys b/examples/smtbmc/glift/alu4.ys new file mode 100644 index 000000000..8e8d14225 --- /dev/null +++ b/examples/smtbmc/glift/alu4.ys @@ -0,0 +1,41 @@ +read_verilog alu4.v +techmap +flatten +select alu4_lev2 +glift -create-instrumented-model +techmap +opt +rename alu4_lev2 uut +cd .. +delete [AIONX][NVXR]2 +read_verilog alu4.v +techmap +flatten +select alu4_lev2 +glift -create-precise-model +techmap +opt +rename alu4_lev2 spec +cd .. +delete [AIONX][NVXR]2 + +design -push-copy +miter -equiv spec uut miter +flatten +delete uut spec +techmap +opt +stat miter +qbfsat -O2 -write-solution alu4.soln -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity miter +design -pop +stat + +copy uut solved +qbfsat -specialize-from-file alu4.soln solved +opt solved +miter -equiv spec solved satmiter +flatten +sat -prove trigger 0 satmiter +delete satmiter +stat +shell |