yosys/passes/sat/example.ys


read_verilog example.v
proc; opt_clean
echo on

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 -ignore_unknown_cells example004
sat -show rst,counter -set-at 3 y 1'b1 -seq 4 example004

sat -prove y 1'b0 -show rst,counter,y -ignore_unknown_cells example004
sat -prove y 1'b0 -tempinduct -show rst,counter,y -set-at 1 rst 1'b1 -seq 1 example004
Implemented temporal induction proofs in sat_solve 2013-06-09 18:07:05 +02:00
Added SAT generator and simple sat_solve command 2013-06-07 13:59:13 +02:00			`read_verilog example.v`
Various improvements in sat_solve pass and SAT generator 2013-06-08 14:11:50 +02:00			`proc; opt_clean`
Fixes in old SAT example.ys 2014-09-01 11:45:47 +02:00			`echo on`
Implemented temporal induction proofs in sat_solve 2013-06-09 18:07:05 +02:00
Renamed "sat_solve" pass to "sat" 2013-06-09 21:55:53 +02:00			`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`
Fixes in old SAT example.ys 2014-09-01 11:45:47 +02:00			`sat -set y 1'b1 -ignore_unknown_cells example004`
Renamed "sat_solve" pass to "sat" 2013-06-09 21:55:53 +02:00			`sat -show rst,counter -set-at 3 y 1'b1 -seq 4 example004`

Fixes in old SAT example.ys 2014-09-01 11:45:47 +02:00			`sat -prove y 1'b0 -show rst,counter,y -ignore_unknown_cells example004`
			`sat -prove y 1'b0 -tempinduct -show rst,counter,y -set-at 1 rst 1'b1 -seq 1 example004`
Added support for non-temporal proofs to sat_solve 2013-06-09 16:30:37 +02:00