[ci] Add a formal trace text target

Makefile

@@ -1,8 +1,9 @@
 #   make MOD=sync_fifo           		    compile rtl/ + that tb, run; a test FAIL exits nonzero
 #   make wave MOD=sync_fifo        			same, then open the waveform in surfer (opens even on FAIL)
 #   make view MOD=sync_fifo         		open testbench waveform in surfer (no rerun); error if .vcd missing
-#   make view-formal MOD=async_fifo_cover   open formal waveform; error if .vcd missing
 #   make formal MOD=async_fifo   		    run every SymbiYosys task in formal/$(MOD).sby; a FAIL exits nonzero
+#   make trace MOD=async_fifo    		    print a formal counterexample as text
+#   make view-formal MOD=async_fifo   		open a formal waveform in surfer; error if .vcd missing
 #   make clean                  		    delete build artifacts (build/, *.vcd)
 
 RTL := $(wildcard rtl/*.sv)
@@ -34,14 +35,38 @@ view:
 	@test -f "$$(ls tb/*.vcd 2>/dev/null | head -1)" || { echo "Error: no .vcd found in tb/"; exit 1; }
 	surfer $$(ls tb/*.vcd 2>/dev/null | head -1) -s tb/$(MOD).ron &
 
+# Echoes MOD's run directory, prompting when the .sby split into several tasks
+define pick_run
+	test -n "$(MOD)" || { echo "usage: make $@ MOD=<module>  (e.g. MOD=async_fifo)" >&2; exit 1; }; \
+	runs=$$(for d in formal/$(MOD)/ formal/$(MOD)_*/; do [ -f "$$d/status" ] && echo "$${d%/}"; done); \
+	[ -n "$$runs" ] || { echo "No runs for $(MOD), try: make formal MOD=$(MOD)" >&2; exit 1; }; \
+	if [ $$(echo "$$runs" | wc -l) -eq 1 ]; then echo "$$runs"; else \
+	  i=0; for d in $$runs; do i=$$((i+1)); \
+	    printf '  %d) %-12s %-6s%s\n' $$i "$$(basename $$d | sed 's/^$(MOD)_//')" \
+	      "$$(cut -d' ' -f1 $$d/status)" \
+	      "$$(find $$d -name trace.yw 2>/dev/null | head -1 | sed 's/.*/counterexample/')" >&2; \
+	  done; \
+	  printf 'Select task: ' >&2; read n; \
+	  sel=$$(echo "$$runs" | sed -n "$${n}p" 2>/dev/null); \
+	  [ -d "$$sel" ] || { echo "No task $$n" >&2; exit 1; }; \
+	  echo "$$sel"; fi
+endef
+
+trace:
+	@dir=$$($(pick_run)); test -n "$$dir" || exit 1; \
+	yw=$$(find $$dir -name 'trace.yw' 2>/dev/null | head -1); \
+	test -n "$$yw" || { echo "Error: no trace.yw in $$dir/, that run has no counterexample"; exit 1; }; \
+	yosys-witness display $$yw
+
 view-formal:
-	@test -n "$(MOD)" || { echo "usage: make view-formal MOD=<module>  (e.g. MOD=async_fifo_cover)"; exit 1; }
-	@test -f "formal/$(MOD).ron" || { echo "Error: formal/$(MOD).ron not found"; exit 1; }
-	@test -f "$$(find formal/$(MOD) -name '*.vcd' 2>/dev/null | head -1)" || { echo "Error: no .vcd found in formal/$(MOD)/"; exit 1; }
-	surfer $$(find formal/$(MOD) -name '*.vcd' 2>/dev/null | head -1) -s formal/$(MOD).ron &
+	@dir=$$($(pick_run)); test -n "$$dir" || exit 1; \
+	vcd=$$(find $$dir -name '*.vcd' 2>/dev/null | head -1); \
+	test -n "$$vcd" || { echo "Error: no .vcd found in $$dir/"; exit 1; }; \
+	echo "surfer $$vcd"; \
+	surfer $$vcd $$(test -f $$dir.ron && echo "-s $$dir.ron") &
 
 clean:
 	rm -rf build *.vcd sim_build results.xml
 
 .DEFAULT_GOAL := run
-.PHONY: run wave formal view view-formal clean
+.PHONY: run wave formal view trace view-formal clean

README.md

@@ -46,6 +46,8 @@ Synthesized for the Xilinx Artix-7 XC7A35T through Yosys and nextpnr-xilinx.
 make MOD=sync_fifo                                  # run a module's testbench
 make wave MOD=sync_fifo                             # run the testbench and open the waveform in Surfer
 make formal MOD=async_fifo                          # run the module's SymbiYosys proof
+make trace MOD=async_fifo                           # print a formal counterexample as text
+make view-formal MOD=async_fifo                     # open a formal waveform in Surfer
 ./synth_stats.sh sync_fifo                          # report a module's synthesis cost
 ./fmax.sh async_fifo tt_async_fifo wr_clk rd_clk    # fmax and utilization
 ```