diff options
| author | Alberto Gonzalez <boqwxp@airmail.cc> | 2020-04-28 06:13:12 +0000 |
|---|---|---|
| committer | Alberto Gonzalez <boqwxp@airmail.cc> | 2020-07-01 19:51:46 +0000 |
| commit | ddfb9f08e20557ab434017a053f14067992b0ea9 (patch) | |
| tree | 75dabcbf4130d791a3785f17137f33e5a50ecc08 /examples/smtbmc/glift/mux2.ys | |
| parent | ca3844d44e07a86d22d6026861cd405f80b0d321 (diff) | |
| download | yosys-ddfb9f08e20557ab434017a053f14067992b0ea9.tar.gz yosys-ddfb9f08e20557ab434017a053f14067992b0ea9.tar.bz2 yosys-ddfb9f08e20557ab434017a053f14067992b0ea9.zip | |
glift: Add `-create-imprecise` command, rename other commands, and re-work the help text.
Diffstat (limited to 'examples/smtbmc/glift/mux2.ys')
| -rw-r--r-- | examples/smtbmc/glift/mux2.ys | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/examples/smtbmc/glift/mux2.ys b/examples/smtbmc/glift/mux2.ys index 6b2b98c89..c6670d741 100644 --- a/examples/smtbmc/glift/mux2.ys +++ b/examples/smtbmc/glift/mux2.ys @@ -18,18 +18,19 @@ module mux2(a, b, s, y); endmodule EOT techmap -copy mux2 uut copy mux2 spec +copy mux2 uut +copy mux2 solved delete mux2 -glift -optimize-precise uut glift -create-precise spec +glift -create-sketch uut +glift -create-sketch -no-cost-model solved design -push-copy miter -equiv spec uut qbfmiter flatten -delete spec uut +delete spec uut solved 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 |