From 4f042eac5338c789ad90ac10dc2a9d8e92ce1acd Mon Sep 17 00:00:00 2001
From: "William D. Jones" <thor0505@comcast.net>
Date: Sat, 28 Nov 2020 21:08:09 -0500
Subject: machxo2: Rework examples to test pack, place, and route phases.

---
 machxo2/examples/blinky.v | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'machxo2/examples/blinky.v')

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)
-- 
cgit v1.2.3