diff options
Diffstat (limited to 'machxo2/examples/blinky.v')
| -rw-r--r-- | machxo2/examples/blinky.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/machxo2/examples/blinky.v b/machxo2/examples/blinky.v index 2137ad58..57bad543 100644 --- a/machxo2/examples/blinky.v +++ b/machxo2/examples/blinky.v @@ -1,6 +1,10 @@ module top(input clk, rst, output [7:0] leds); -// TODO: Test miter circuit without reset value. +// TODO: Test miter circuit without reset value. SAT and SMT diverge without +// reset value (SAT succeeds, SMT fails). I haven't figured out the correct +// init set of options to make SAT fail. +// "sat -verify -prove-asserts -set-init-def -seq 1 miter" causes assertion +// failure in yosys. reg [7:0] ctr = 8'h00; always @(posedge clk) if (rst) |