riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

glift: Change command names to better represent their functions.

This commit is contained in:
Alberto Gonzalez 2020-06-09 22:56:57 +00:00
parent ddfb9f08e2
commit bc207d5426
No known key found for this signature in database
GPG Key ID: 8395A8BA109708B2
10 changed files with 49 additions and 49 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
examples/smtbmc/glift/C7552.ys
View File

@ -2,7 +2,7 @@ read_verilog C7552.v
techmap techmap
flatten flatten
select C7552_lev2 select C7552_lev2
glift -create-sketch glift -create-instrumented-model
techmap techmap
opt opt
rename C7552_lev2 uut rename C7552_lev2 uut
@ -12,7 +12,7 @@ read_verilog C7552.v
techmap techmap
flatten flatten
select C7552_lev2 select C7552_lev2
glift -create-precise glift -create-precise-model
techmap techmap
opt opt
rename C7552_lev2 spec rename C7552_lev2 spec
@ -30,7 +30,7 @@ abc -script +print_stats;strash;print_stats;drwsat;print_stats;print_stats;fraig
techmap techmap
opt opt
stat 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 design -pop
stat stat

6
examples/smtbmc/glift/C880.ys
View File

@ -2,7 +2,7 @@ read_verilog C880.v
techmap techmap
flatten flatten
select C880_lev2 select C880_lev2
glift -create-sketch glift -create-instrumented-model
techmap techmap
opt opt
rename C880_lev2 uut rename C880_lev2 uut
@ -12,7 +12,7 @@ read_verilog C880.v
techmap techmap
flatten flatten
select C880_lev2 select C880_lev2
glift -create-precise glift -create-precise-model
techmap techmap
opt opt
rename C880_lev2 spec rename C880_lev2 spec
@ -30,7 +30,7 @@ abc -script +print_stats;strash;print_stats;drwsat;print_stats;print_stats;fraig
techmap techmap
opt opt
stat 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 design -pop
stat stat

6
examples/smtbmc/glift/alu2.ys
View File

@ -2,7 +2,7 @@ read_verilog alu2.v
techmap techmap
flatten flatten
select alu2_lev2 select alu2_lev2
glift -create-sketch glift -create-instrumented-model
techmap techmap
opt opt
rename alu2_lev2 uut rename alu2_lev2 uut
@ -12,7 +12,7 @@ read_verilog alu2.v
techmap techmap
flatten flatten
select alu2_lev2 select alu2_lev2
glift -create-precise glift -create-precise-model
techmap techmap
opt opt
rename alu2_lev2 spec rename alu2_lev2 spec
@ -30,7 +30,7 @@ abc -script +print_stats;strash;print_stats;drwsat;print_stats;print_stats;fraig
techmap techmap
opt opt
stat 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 design -pop
stat stat

6
examples/smtbmc/glift/alu4.ys
View File

@ -2,7 +2,7 @@ read_verilog alu4.v
techmap techmap
flatten flatten
select alu4_lev2 select alu4_lev2
glift -create-sketch glift -create-instrumented-model
techmap techmap
opt opt
rename alu4_lev2 uut rename alu4_lev2 uut
@ -12,7 +12,7 @@ read_verilog alu4.v
techmap techmap
flatten flatten
select alu4_lev2 select alu4_lev2
glift -create-precise glift -create-precise-model
techmap techmap
opt opt
rename alu4_lev2 spec rename alu4_lev2 spec
@ -30,7 +30,7 @@ abc -script +print_stats;strash;print_stats;drwsat;print_stats;print_stats;fraig
techmap techmap
opt opt
stat 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 design -pop
stat stat

6
examples/smtbmc/glift/mux2.ys
View File

@ -22,9 +22,9 @@ copy mux2 spec
copy mux2 uut copy mux2 uut
copy mux2 solved copy mux2 solved
delete mux2 delete mux2
glift -create-precise spec glift -create-precise-model spec
glift -create-sketch uut glift -create-instrumented-model uut
glift -create-sketch -no-cost-model solved glift -create-instrumented-model -no-cost-model solved
design -push-copy design -push-copy
miter -equiv spec uut qbfmiter miter -equiv spec uut qbfmiter
flatten flatten

6
examples/smtbmc/glift/t481.ys
View File

@ -2,7 +2,7 @@ read_verilog t481.v
techmap techmap
flatten flatten
select t481_lev2 select t481_lev2
glift -create-sketch glift -create-instrumented-model
techmap techmap
opt opt
rename t481_lev2 uut rename t481_lev2 uut
@ -12,7 +12,7 @@ read_verilog t481.v
techmap techmap
flatten flatten
select t481_lev2 select t481_lev2
glift -create-precise glift -create-precise-model
techmap techmap
opt opt
rename t481_lev2 spec rename t481_lev2 spec
@ -30,7 +30,7 @@ abc -script +print_stats;strash;print_stats;drwsat;print_stats;print_stats;fraig
techmap techmap
opt opt
stat 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 design -pop
stat stat

6
examples/smtbmc/glift/too_large.ys
View File

@ -2,7 +2,7 @@ read_verilog too_large.v
techmap techmap
flatten flatten
select too_large_lev2 select too_large_lev2
glift -create-sketch glift -create-instrumented-model
techmap techmap
opt opt
rename too_large_lev2 uut rename too_large_lev2 uut
@ -12,7 +12,7 @@ read_verilog too_large.v
techmap techmap
flatten flatten
select too_large_lev2 select too_large_lev2
glift -create-precise glift -create-precise-model
techmap techmap
opt opt
rename too_large_lev2 spec rename too_large_lev2 spec
@ -30,7 +30,7 @@ abc -script +print_stats;strash;print_stats;drwsat;print_stats;print_stats;fraig
techmap techmap
opt opt
stat 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 design -pop
stat stat

6
examples/smtbmc/glift/ttt2.ys
View File

@ -2,7 +2,7 @@ read_verilog ttt2.v
techmap techmap
flatten flatten
select ttt2_lev2 select ttt2_lev2
glift -create-sketch glift -create-instrumented-model
techmap techmap
opt opt
rename ttt2_lev2 uut rename ttt2_lev2 uut
@ -12,7 +12,7 @@ read_verilog ttt2.v
techmap techmap
flatten flatten
select ttt2_lev2 select ttt2_lev2
glift -create-precise glift -create-precise-model
techmap techmap
opt opt
rename ttt2_lev2 spec rename ttt2_lev2 spec
@ -30,7 +30,7 @@ abc -script +print_stats;strash;print_stats;drwsat;print_stats;print_stats;fraig
techmap techmap
opt opt
stat 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 design -pop
stat stat

6
examples/smtbmc/glift/x1.ys
View File

@ -2,7 +2,7 @@ read_verilog x1.v
techmap techmap
flatten flatten
select x1_lev2 select x1_lev2
glift -create-sketch glift -create-instrumented-model
techmap techmap
opt opt
rename x1_lev2 uut rename x1_lev2 uut
@ -12,7 +12,7 @@ read_verilog x1.v
techmap techmap
flatten flatten
select x1_lev2 select x1_lev2
glift -create-precise glift -create-precise-model
techmap techmap
opt opt
rename x1_lev2 spec rename x1_lev2 spec
@ -30,7 +30,7 @@ abc -script +print_stats;strash;print_stats;drwsat;print_stats;print_stats;fraig
techmap techmap
opt opt
stat 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 design -pop
stat stat

44
passes/cmds/glift.cc
View File

@ -27,7 +27,7 @@ PRIVATE_NAMESPACE_BEGIN
struct GliftPass : public Pass { struct GliftPass : public Pass {
private: 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; bool opt_taintconstants, opt_keepoutputs, opt_nocostmodel;
std::vector<std::string> args; std::vector<std::string> args;
std::vector<std::string>::size_type argidx; std::vector<std::string>::size_type argidx;
@ -39,16 +39,16 @@ struct GliftPass : public Pass {
void parse_args() { void parse_args() {
for (argidx = 1; argidx < args.size(); argidx++) { for (argidx = 1; argidx < args.size(); argidx++) {
if (args[argidx] == "-create-precise") { if (args[argidx] == "-create-precise-model") {
opt_create_precise = true; opt_create_precise_model = true;
continue; continue;
} }
if (args[argidx] == "-create-imprecise") { if (args[argidx] == "-create-imprecise-model") {
opt_create_imprecise = true; opt_create_imprecise_model = true;
continue; continue;
} }
if (args[argidx] == "-create-sketch") { if (args[argidx] == "-create-instrumented-model") {
opt_create_sketch = true; opt_create_instrumented_model = true;
continue; continue;
} }
if (args[argidx] == "-taint-constants") { if (args[argidx] == "-taint-constants") {
@ -65,9 +65,9 @@ struct GliftPass : public Pass {
} }
break; 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"); 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"); 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) for (unsigned int i = 0; i < NUM_PORTS; ++i)
port_taints[i] = get_corresponding_taint_signal(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]); 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]); 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)), RTLIL::SigSpec precise_y(module->addWire(cell->name.str() + "_y1", 1)),
imprecise_1_y(module->addWire(cell->name.str() + "_y2", 1)), imprecise_1_y(module->addWire(cell->name.str() + "_y2", 1)),
imprecise_2_y(module->addWire(cell->name.str() + "_y3", 1)), imprecise_2_y(module->addWire(cell->name.str() + "_y3", 1)),
@ -259,9 +259,9 @@ struct GliftPass : public Pass {
} }
void reset() { void reset() {
opt_create_precise = false; opt_create_precise_model = false;
opt_create_imprecise = false; opt_create_imprecise_model = false;
opt_create_sketch = false; opt_create_instrumented_model = false;
opt_taintconstants = false; opt_taintconstants = false;
opt_keepoutputs = false; opt_keepoutputs = false;
opt_nocostmodel = false; opt_nocostmodel = false;
@ -274,7 +274,7 @@ struct GliftPass : public Pass {
public: 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 void help() YS_OVERRIDE
{ {
@ -290,17 +290,17 @@ struct GliftPass : public Pass {
log("\n"); log("\n");
log("Commands:\n"); log("Commands:\n");
log("\n"); log("\n");
log(" -create-precise\n"); log(" -create-precise-model\n");
log(" Replaces the current or specified module with one that has additional \"taint\"\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(" inputs, outputs, and internal nets along with precise taint-tracking logic.\n");
log("\n"); log("\n");
log(" -create-imprecise\n"); log(" -create-imprecise-model\n");
log(" Replaces the current or specified module with one that has additional \"taint\"\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(" inputs, outputs, and internal nets along with imprecise \"All OR\" taint-tracking\n");
log(" logic.\n"); log(" logic.\n");
log("\n"); log("\n");
log(" -create-sketch\n"); log(" -create-instrumented-model\n");
log(" Replaces the current or specified module with one that has additional \"taint\"\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(" 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(" 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"); log(" by a MUX selected by an $anyconst cell. By default, unless the `-no-cost-model`\n");