diff options
| author | Clifford Wolf <clifford@clifford.at> | 2013-06-09 16:30:37 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2013-06-09 16:30:37 +0200 |
| commit | b210234612beb3e20d5338d03debf084c9b6c7b9 (patch) | |
| tree | 430c539d3db2f9811e1178701456ff5c7b237b40 /passes/sat/example.ys | |
| parent | 1349b845e3c6508fada52f58919cffad069ceb13 (diff) | |
Added support for non-temporal proofs to sat_solve
Diffstat (limited to 'passes/sat/example.ys')
| -rw-r--r-- | passes/sat/example.ys | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/passes/sat/example.ys b/passes/sat/example.ys index dd1a117f..19f8f50e 100644 --- a/passes/sat/example.ys +++ b/passes/sat/example.ys @@ -5,3 +5,7 @@ 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 example001 +# sat_solve -show rst,counter -prove y 1'b0 -set-at 1 rst 1'b1 -seq 1 example004 + |