diff options
| author | William D. Jones <thor0505@comcast.net> | 2020-11-28 21:08:09 -0500 |
|---|---|---|
| committer | gatecat <gatecat@ds0.me> | 2021-02-12 10:36:59 +0000 |
| commit | 4f042eac5338c789ad90ac10dc2a9d8e92ce1acd (patch) | |
| tree | fa859afdf47733863088d42facf04560d351224d /machxo2/examples/blinky.v | |
| parent | 5838662b2f8a06aef52eac8218175f59547b5f09 (diff) | |
| download | nextpnr-4f042eac5338c789ad90ac10dc2a9d8e92ce1acd.tar.gz nextpnr-4f042eac5338c789ad90ac10dc2a9d8e92ce1acd.tar.bz2 nextpnr-4f042eac5338c789ad90ac10dc2a9d8e92ce1acd.zip | |
machxo2: Rework examples to test pack, place, and route phases.
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) |