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

Renamed "sat_solve" pass to "sat"

This commit is contained in:
Clifford Wolf 2013-06-09 21:55:53 +02:00
parent a75b249427
commit 08e2fa978c
3 changed files with 12 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
passes/sat/Makefile.inc
View File

@ -1,3 +1,3 @@
OBJS += passes/sat/sat_solve.o OBJS += passes/sat/sat.o

14
passes/sat/example.ys
View File

@ -2,12 +2,12 @@
read_verilog example.v read_verilog example.v
proc; opt_clean proc; opt_clean
sat_solve -set y 1'b1 example001 sat -set y 1'b1 example001
sat_solve -set y 1'b1 example002 sat -set y 1'b1 example002
sat_solve -set y_sshl 8'hf0 -set y_sshr 8'hf0 -set sh 4'd3 example003 sat -set y_sshl 8'hf0 -set y_sshr 8'hf0 -set sh 4'd3 example003
sat_solve -set y 1'b1 example004 sat -set y 1'b1 example004
sat_solve -show rst,counter -set-at 3 y 1'b1 -seq 4 example004 sat -show rst,counter -set-at 3 y 1'b1 -seq 4 example004
sat_solve -prove y 1'b0 -show rst,counter,y example004 sat -prove y 1'b0 -show rst,counter,y example004
sat_solve -prove y 1'b0 -show rst,counter,y -set-at 1 rst 1'b1 -seq 1 example004 sat -prove y 1'b0 -show rst,counter,y -set-at 1 rst 1'b1 -seq 1 example004

8
passes/sat/sat_solve.cc → passes/sat/sat.cc
View File

@ -469,13 +469,13 @@ static void print_qed()
log("\n"); log("\n");
} }
struct SatSolvePass : public Pass { struct SatPass : public Pass {
SatSolvePass() : Pass("sat_solve", "solve a SAT problem in the circuit") { } SatPass() : Pass("sat", "solve a SAT problem in the circuit") { }
virtual void help() virtual void help()
{ {
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n"); log("\n");
log(" sat_solve [options] [selection]\n"); log(" sat [options] [selection]\n");
log("\n"); log("\n");
log("This command solves a SAT problem defined over the currently selected circuit\n"); log("This command solves a SAT problem defined over the currently selected circuit\n");
log("and additional constraints passed as parameters.\n"); log("and additional constraints passed as parameters.\n");
@ -749,5 +749,5 @@ struct SatSolvePass : public Pass {
} }
} }
} }
} SatSolvePass; } SatPass;