From: Alberto Gonzalez Date: Tue, 9 Jun 2020 22:56:57 +0000 (+0000) Subject: glift: Change command names to better represent their functions. X-Git-Tag: yosys-0.15~29^2~11 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bc207d5426c5c41e103ca54dbb31cab573d66df2;p=yosys.git glift: Change command names to better represent their functions. --- diff --git a/examples/smtbmc/glift/C7552.ys b/examples/smtbmc/glift/C7552.ys index 139b0df43..c1fdf244e 100644 --- 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 93f929c89..9a5e7bdcd 100644 --- 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 72cdaceba..f79c33ca5 100644 --- 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 b4337e699..3fc2112d6 100644 --- 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 c6670d741..a8e99912b 100644 --- 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 249a9eb71..282e723af 100644 --- 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 2bb6105ea..05b9fa5dc 100644 --- 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 62054a86c..beba8b102 100644 --- 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 b010fe9ee..e48a4e6ce 100644 --- 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 8296e7194..1ed5de76a 100644 --- 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 args; std::vector::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(opt_create_precise) + static_cast(opt_create_imprecise) + static_cast(opt_create_sketch) != 1) + if(static_cast(opt_create_precise_model) + static_cast(opt_create_imprecise_model) + static_cast(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");