summaryrefslogtreecommitdiff
path: root/passes
diff options
context:
space:
mode:
Diffstat (limited to 'passes')
-rw-r--r--passes/sat/Makefile.inc2
-rw-r--r--passes/sat/example.ys16
-rw-r--r--passes/sat/sat.cc (renamed from passes/sat/sat_solve.cc)8
3 files changed, 13 insertions, 13 deletions
diff --git a/passes/sat/Makefile.inc b/passes/sat/Makefile.inc
index 873f9746..4a9094bf 100644
--- a/passes/sat/Makefile.inc
+++ b/passes/sat/Makefile.inc
@@ -1,3 +1,3 @@
-OBJS += passes/sat/sat_solve.o
+OBJS += passes/sat/sat.o
diff --git a/passes/sat/example.ys b/passes/sat/example.ys
index c532c1fb..11f5b924 100644
--- a/passes/sat/example.ys
+++ b/passes/sat/example.ys
@@ -2,12 +2,12 @@
read_verilog example.v
proc; opt_clean
-sat_solve -set y 1'b1 example001
-sat_solve -set y 1'b1 example002
-sat_solve -set y_sshl 8'hf0 -set y_sshr 8'hf0 -set sh 4'd3 example003
-sat_solve -set y 1'b1 example004
-sat_solve -show rst,counter -set-at 3 y 1'b1 -seq 4 example004
-
-sat_solve -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 -set y 1'b1 example001
+sat -set y 1'b1 example002
+sat -set y_sshl 8'hf0 -set y_sshr 8'hf0 -set sh 4'd3 example003
+sat -set y 1'b1 example004
+sat -show rst,counter -set-at 3 y 1'b1 -seq 4 example004
+
+sat -prove y 1'b0 -show rst,counter,y example004
+sat -prove y 1'b0 -show rst,counter,y -set-at 1 rst 1'b1 -seq 1 example004
diff --git a/passes/sat/sat_solve.cc b/passes/sat/sat.cc
index 6a548ae5..a13f8318 100644
--- a/passes/sat/sat_solve.cc
+++ b/passes/sat/sat.cc
@@ -469,13 +469,13 @@ static void print_qed()
log("\n");
}
-struct SatSolvePass : public Pass {
- SatSolvePass() : Pass("sat_solve", "solve a SAT problem in the circuit") { }
+struct SatPass : public Pass {
+ SatPass() : Pass("sat", "solve a SAT problem in the circuit") { }
virtual void help()
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
- log(" sat_solve [options] [selection]\n");
+ log(" sat [options] [selection]\n");
log("\n");
log("This command solves a SAT problem defined over the currently selected circuit\n");
log("and additional constraints passed as parameters.\n");
@@ -749,5 +749,5 @@ struct SatSolvePass : public Pass {
}
}
}
-} SatSolvePass;
+} SatPass;