glift: Change command names to better represent their functions.

diff --git a/examples/smtbmc/glift/C7552.ys b/examples/smtbmc/glift/C7552.ys
index 139b0df4329c05c1a0d49e3dc4034297e85c6497..c1fdf244e0037db97cf6a53d8844524449be0669 100644 (file)
--- a/examples/smtbmc/glift/C7552.ys
+++ b/examples/smtbmc/glift/C7552.ys
@@ -2,7 +2,7 @@ read_verilog C7552.v
 techmap
 flatten
 select C7552_lev2
-glift -create-sketch
+glift -create-instrumented-model
 techmap
 opt
 rename C7552_lev2 uut
@@ -12,7 +12,7 @@ read_verilog C7552.v
 techmap
 flatten
 select C7552_lev2
-glift -create-precise
+glift -create-precise-model
 techmap
 opt
 rename C7552_lev2 spec
@@ -30,7 +30,7 @@ abc -script +print_stats;strash;print_stats;drwsat;print_stats;print_stats;fraig
 techmap
 opt
 stat
-qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution C7552.soln -show-smtbmc -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter 
+qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution C7552.soln -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter
 design -pop
 stat
 

diff --git a/examples/smtbmc/glift/C880.ys b/examples/smtbmc/glift/C880.ys
index 93f929c8957a45082cb7c24176116b2b99d2f86c..9a5e7bdcd08d918923f46ea37d129053c4fbd8d1 100644 (file)
--- a/examples/smtbmc/glift/C880.ys
+++ b/examples/smtbmc/glift/C880.ys
@@ -2,7 +2,7 @@ read_verilog C880.v
 techmap
 flatten
 select C880_lev2
-glift -create-sketch
+glift -create-instrumented-model
 techmap
 opt
 rename C880_lev2 uut
@@ -12,7 +12,7 @@ read_verilog C880.v
 techmap
 flatten
 select C880_lev2
-glift -create-precise
+glift -create-precise-model
 techmap
 opt
 rename C880_lev2 spec
@@ -30,7 +30,7 @@ abc -script +print_stats;strash;print_stats;drwsat;print_stats;print_stats;fraig
 techmap
 opt
 stat
-qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution C880.soln -show-smtbmc -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter 
+qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution C880.soln -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter
 design -pop
 stat
 

diff --git a/examples/smtbmc/glift/alu2.ys b/examples/smtbmc/glift/alu2.ys
index 72cdaceba9f6a0aef860d8a934bbeaa7afebc55c..f79c33ca5bc2a6a9dccceb043fbc9f071d8b4432 100644 (file)
--- a/examples/smtbmc/glift/alu2.ys
+++ b/examples/smtbmc/glift/alu2.ys
@@ -2,7 +2,7 @@ read_verilog alu2.v
 techmap
 flatten
 select alu2_lev2
-glift -create-sketch
+glift -create-instrumented-model
 techmap
 opt
 rename alu2_lev2 uut
@@ -12,7 +12,7 @@ read_verilog alu2.v
 techmap
 flatten
 select alu2_lev2
-glift -create-precise
+glift -create-precise-model
 techmap
 opt
 rename alu2_lev2 spec
@@ -30,7 +30,7 @@ abc -script +print_stats;strash;print_stats;drwsat;print_stats;print_stats;fraig
 techmap
 opt
 stat
-qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution alu2.soln -show-smtbmc -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter 
+qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution alu2.soln -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter
 design -pop
 stat
 

diff --git a/examples/smtbmc/glift/alu4.ys b/examples/smtbmc/glift/alu4.ys
index b4337e69927323789ea375d9b7f6fd69bf902f69..3fc2112d6212737babbb4401aa44593ab2990e7a 100644 (file)
--- a/examples/smtbmc/glift/alu4.ys
+++ b/examples/smtbmc/glift/alu4.ys
@@ -2,7 +2,7 @@ read_verilog alu4.v
 techmap
 flatten
 select alu4_lev2
-glift -create-sketch
+glift -create-instrumented-model
 techmap
 opt
 rename alu4_lev2 uut
@@ -12,7 +12,7 @@ read_verilog alu4.v
 techmap
 flatten
 select alu4_lev2
-glift -create-precise
+glift -create-precise-model
 techmap
 opt
 rename alu4_lev2 spec
@@ -30,7 +30,7 @@ abc -script +print_stats;strash;print_stats;drwsat;print_stats;print_stats;fraig
 techmap
 opt
 stat
-qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution alu4.soln -show-smtbmc -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter 
+qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution alu4.soln -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter
 design -pop
 stat
 

diff --git a/examples/smtbmc/glift/mux2.ys b/examples/smtbmc/glift/mux2.ys
index c6670d74172254d82cee7a3bbfd7dd2c0ea75b05..a8e99912b26e20c15d4fbdcaf9dedf3ab1607f7f 100644 (file)
--- a/examples/smtbmc/glift/mux2.ys
+++ b/examples/smtbmc/glift/mux2.ys
@@ -22,9 +22,9 @@ copy mux2 spec
 copy mux2 uut
 copy mux2 solved
 delete mux2
-glift -create-precise spec
-glift -create-sketch uut
-glift -create-sketch -no-cost-model solved
+glift -create-precise-model spec
+glift -create-instrumented-model uut
+glift -create-instrumented-model -no-cost-model solved
 design -push-copy
 miter -equiv spec uut qbfmiter
 flatten

diff --git a/examples/smtbmc/glift/t481.ys b/examples/smtbmc/glift/t481.ys
index 249a9eb7165154c58d6843fbba605c3ac42f9fb3..282e723af9ec45dddfab18e0264b2f592934769f 100644 (file)
--- a/examples/smtbmc/glift/t481.ys
+++ b/examples/smtbmc/glift/t481.ys
@@ -2,7 +2,7 @@ read_verilog t481.v
 techmap
 flatten
 select t481_lev2
-glift -create-sketch
+glift -create-instrumented-model
 techmap
 opt
 rename t481_lev2 uut
@@ -12,7 +12,7 @@ read_verilog t481.v
 techmap
 flatten
 select t481_lev2
-glift -create-precise
+glift -create-precise-model
 techmap
 opt
 rename t481_lev2 spec
@@ -30,7 +30,7 @@ abc -script +print_stats;strash;print_stats;drwsat;print_stats;print_stats;fraig
 techmap
 opt
 stat
-qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution t481.soln -show-smtbmc -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter 
+qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution t481.soln -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter
 design -pop
 stat
 

diff --git a/examples/smtbmc/glift/too_large.ys b/examples/smtbmc/glift/too_large.ys
index 2bb6105ea9ec54c226879dda9341c74c56d3c1fa..05b9fa5dc54d2bf80dc84b2f608ad43d4ce81db0 100644 (file)
--- a/examples/smtbmc/glift/too_large.ys
+++ b/examples/smtbmc/glift/too_large.ys
@@ -2,7 +2,7 @@ read_verilog too_large.v
 techmap
 flatten
 select too_large_lev2
-glift -create-sketch
+glift -create-instrumented-model
 techmap
 opt
 rename too_large_lev2 uut
@@ -12,7 +12,7 @@ read_verilog too_large.v
 techmap
 flatten
 select too_large_lev2
-glift -create-precise
+glift -create-precise-model
 techmap
 opt
 rename too_large_lev2 spec
@@ -30,7 +30,7 @@ abc -script +print_stats;strash;print_stats;drwsat;print_stats;print_stats;fraig
 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 
+qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution too_large.soln -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter
 design -pop
 stat
 

diff --git a/examples/smtbmc/glift/ttt2.ys b/examples/smtbmc/glift/ttt2.ys
index 62054a86c2bb7d24d979686e5fbb295dc9917fbf..beba8b1026b4f1446ad03ab2d46970929db89d02 100644 (file)
--- a/examples/smtbmc/glift/ttt2.ys
+++ b/examples/smtbmc/glift/ttt2.ys
@@ -2,7 +2,7 @@ read_verilog ttt2.v
 techmap
 flatten
 select ttt2_lev2
-glift -create-sketch
+glift -create-instrumented-model
 techmap
 opt
 rename ttt2_lev2 uut
@@ -12,7 +12,7 @@ read_verilog ttt2.v
 techmap
 flatten
 select ttt2_lev2
-glift -create-precise
+glift -create-precise-model
 techmap
 opt
 rename ttt2_lev2 spec
@@ -30,7 +30,7 @@ abc -script +print_stats;strash;print_stats;drwsat;print_stats;print_stats;fraig
 techmap
 opt
 stat
-qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution ttt2.soln -show-smtbmc -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter 
+qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution ttt2.soln -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter
 design -pop
 stat
 

diff --git a/examples/smtbmc/glift/x1.ys b/examples/smtbmc/glift/x1.ys
index b010fe9ee6666be7366e72cdcf60a84709c17e82..e48a4e6ce91db816d98273ea786257459afe40c1 100644 (file)
--- a/examples/smtbmc/glift/x1.ys
+++ b/examples/smtbmc/glift/x1.ys
@@ -2,7 +2,7 @@ read_verilog x1.v
 techmap
 flatten
 select x1_lev2
-glift -create-sketch
+glift -create-instrumented-model
 techmap
 opt
 rename x1_lev2 uut
@@ -12,7 +12,7 @@ read_verilog x1.v
 techmap
 flatten
 select x1_lev2
-glift -create-precise
+glift -create-precise-model
 techmap
 opt
 rename x1_lev2 spec
@@ -30,7 +30,7 @@ abc -script +print_stats;strash;print_stats;drwsat;print_stats;print_stats;fraig
 techmap
 opt
 stat
-qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution x1.soln -show-smtbmc -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter 
+qbfsat -dump-final-smt2 /tmp/test.smt2 -write-solution x1.soln -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity -specialize miter
 design -pop
 stat
 

diff --git a/passes/cmds/glift.cc b/passes/cmds/glift.cc
index 8296e719422e53c724c424fb5bac911ac6f66aad..1ed5de76a2f404b7411133e0e9f057557486c2c3 100644 (file)
--- a/passes/cmds/glift.cc
+++ b/passes/cmds/glift.cc
@@ -27,7 +27,7 @@ PRIVATE_NAMESPACE_BEGIN
 struct GliftPass : public Pass {
        private:
 
-       bool opt_create_precise, opt_create_imprecise, opt_create_sketch;
+       bool opt_create_precise_model, opt_create_imprecise_model, opt_create_instrumented_model;
        bool opt_taintconstants, opt_keepoutputs, opt_nocostmodel;
        std::vector<std::string> args;
        std::vector<std::string>::size_type argidx;
@@ -39,16 +39,16 @@ struct GliftPass : public Pass {
 
        void parse_args() {
                for (argidx = 1; argidx < args.size(); argidx++) {
-                       if (args[argidx] == "-create-precise") {
-                               opt_create_precise = true;
+                       if (args[argidx] == "-create-precise-model") {
+                               opt_create_precise_model = true;
                                continue;
                        }
-                       if (args[argidx] == "-create-imprecise") {
-                               opt_create_imprecise = true;
+                       if (args[argidx] == "-create-imprecise-model") {
+                               opt_create_imprecise_model = true;
                                continue;
                        }
-                       if (args[argidx] == "-create-sketch") {
-                               opt_create_sketch = true;
+                       if (args[argidx] == "-create-instrumented-model") {
+                               opt_create_instrumented_model = true;
                                continue;
                        }
                        if (args[argidx] == "-taint-constants") {
@@ -65,9 +65,9 @@ struct GliftPass : public Pass {
                        }
                        break;
                }
-               if(!opt_create_precise && !opt_create_imprecise && !opt_create_sketch)
+               if(!opt_create_precise_model && !opt_create_imprecise_model && !opt_create_instrumented_model)
                        log_cmd_error("No command provided.  See help for usage.\n");
-               if(static_cast<int>(opt_create_precise) + static_cast<int>(opt_create_imprecise) + static_cast<int>(opt_create_sketch) != 1)
+               if(static_cast<int>(opt_create_precise_model) + static_cast<int>(opt_create_imprecise_model) + static_cast<int>(opt_create_instrumented_model) != 1)
                        log_cmd_error("Only one command may be specified.  See help for usage.\n");
        }
 
@@ -165,11 +165,11 @@ struct GliftPass : public Pass {
                                for (unsigned int i = 0; i < NUM_PORTS; ++i)
                                        port_taints[i] = get_corresponding_taint_signal(ports[i]);
 
-                               if (opt_create_precise)
+                               if (opt_create_precise_model)
                                        add_precise_GLIFT_logic(cell, ports[A], port_taints[A], ports[B], port_taints[B], port_taints[Y]);
-                               else if (opt_create_imprecise)
+                               else if (opt_create_imprecise_model)
                                        add_imprecise_GLIFT_logic_3(cell, port_taints[A], port_taints[B], port_taints[Y]);
-                               else if (opt_create_sketch) {
+                               else if (opt_create_instrumented_model) {
                                        RTLIL::SigSpec precise_y(module->addWire(cell->name.str() + "_y1", 1)),
                                                        imprecise_1_y(module->addWire(cell->name.str() + "_y2", 1)),
                                                        imprecise_2_y(module->addWire(cell->name.str() + "_y3", 1)),
@@ -259,9 +259,9 @@ struct GliftPass : public Pass {
        }
 
        void reset() {
-               opt_create_precise = false;
-               opt_create_imprecise = false;
-               opt_create_sketch = false;
+               opt_create_precise_model = false;
+               opt_create_imprecise_model = false;
+               opt_create_instrumented_model = false;
                opt_taintconstants = false;
                opt_keepoutputs = false;
                opt_nocostmodel = false;
@@ -274,7 +274,7 @@ struct GliftPass : public Pass {
 
        public:
 
-       GliftPass() : Pass("glift", "create GLIFT models and optimization problems"), opt_create_precise(false), opt_create_imprecise(false), opt_create_sketch(false), opt_taintconstants(false), opt_keepoutputs(false), opt_nocostmodel(false), module(nullptr) { }
+       GliftPass() : Pass("glift", "create GLIFT models and optimization problems"), opt_create_precise_model(false), opt_create_imprecise_model(false), opt_create_instrumented_model(false), opt_taintconstants(false), opt_keepoutputs(false), opt_nocostmodel(false), module(nullptr) { }
 
        void help() YS_OVERRIDE
        {
@@ -290,17 +290,17 @@ struct GliftPass : public Pass {
                log("\n");
                log("Commands:\n");
                log("\n");
-               log("  -create-precise\n");
-               log("    Replaces the current or specified module with one that has additional \"taint\"\n");
+               log("  -create-precise-model\n");
+               log("    Replaces the current or specified module with one that has corresponding \"taint\"\n");
                log("    inputs, outputs, and internal nets along with precise taint-tracking logic.\n");
                log("\n");
-               log("  -create-imprecise\n");
-               log("    Replaces the current or specified module with one that has additional \"taint\"\n");
+               log("  -create-imprecise-model\n");
+               log("    Replaces the current or specified module with one that has corresponding \"taint\"\n");
                log("    inputs, outputs, and internal nets along with imprecise \"All OR\" taint-tracking\n");
                log("    logic.\n");
                log("\n");
-               log("  -create-sketch\n");
-               log("    Replaces the current or specified module with one that has additional \"taint\"\n");
+               log("  -create-instrumented-model\n");
+               log("    Replaces the current or specified module with one that has corresponding \"taint\"\n");
                log("    inputs, outputs, and internal nets along with varying-precision taint-tracking\n");
                log("    logic.  Which version of taint tracking logic is used at a given cell is determined\n");
                log("    by a MUX selected by an $anyconst cell.  By default, unless the `-no-cost-model`\n");