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

Fixes in old SAT example.ys 2014-09-01 04:45:47 -05: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 09:30:37 -05:00