add pin photos

fsm-tut4/rtl/clk_gen.v

@@ -5,7 +5,25 @@ module clk_gen(
    output wire o_clk
 );
 
-assign o_clk = i_clk;
+// assign o_clk = i_clk;
+reg [31:0] counter;
+reg buf_clk;
+parameter CLK_RATE_HZ = 12_000_000;
+
+initial  begin
+   counter = 0;
+   buf_clk = 0;
+end
+assign o_clk = buf_clk;
+
+always @(posedge i_clk) begin
+   if (counter >= CLK_RATE_HZ/2 - 1) begin
+      counter <= 0;
+      buf_clk <= ~buf_clk; 
+   end
+   else
+      counter <= counter + 1;
+end
 
 endmodule
 // Local Variables:

fsm-tut4/rtl/top.v

@@ -8,18 +8,17 @@ module top(i_clk, o_led, o_led_row_0, i_request, o_busy);
    input wire i_request;
    output wire o_busy;
 
-   wire clk_12MHz;
+   wire clk_1Hz;
 
    clk_gen clk_gen_0 (/*autoinst*/
       // Outputs
-      .o_clk                 (clk_12MHz),
+      .o_clk                 (clk_1Hz),
       // Inputs
       .i_clk                 (i_clk));
 
    reg [WIDTH-1:0] counter;
    reg [3:0] state;
    reg [5:0] led_buf; // output buffer, take into account the icefun use active low LED
-   reg strobe;
    reg busy_buf;
    wire req_buf;
 
@@ -30,41 +29,36 @@ module top(i_clk, o_led, o_led_row_0, i_request, o_busy);
 
    initial begin
       led_buf = 6'h0;
-      {strobe, counter} = 0;
-      // counter = 0;
+      counter = 0;
       state = 0;
       busy_buf = 0;
    end
 
-   always @(posedge clk_12MHz) begin
+   always @(posedge clk_1Hz) begin
       if (!busy_buf && req_buf)
          busy_buf <= 1;
       else
          busy_buf <= (state != 4'h0);
    end
    // counter and strobe run only during busy signal is High
-   always @(posedge clk_12MHz) begin
+   always @(posedge clk_1Hz) begin
       if (busy_buf)
-         // counter <= counter + 1'b1;
-         {strobe, counter} <= counter + 1'b1;
+         counter <= counter + 1'b1;
       else
-         {strobe, counter} <= 0;
-         // counter <= 0;
+         counter <= 0;
    end
 
-   // state change once strobe starts
-   always @(posedge clk_12MHz) begin
+   always @(posedge clk_1Hz) begin
       if (!busy_buf && req_buf)
          state <= 4'h1;
-      else if (state >= 4'hB && strobe)
+      else if (state >= 4'hB)
          state <= 4'h0;
-      else if (state != 0 && strobe)
+      else if (state != 0)
          state <= state + 1'b1;
    end
 
    // fsm for led_buf
-   always @(posedge clk_12MHz) begin
-      if (strobe)
+   always @(posedge clk_1Hz) begin
       case (state)
          4'h1: led_buf <= 6'b00_0001;
          4'h2: led_buf <= 6'b00_0010;
@@ -81,7 +75,7 @@ module top(i_clk, o_led, o_led_row_0, i_request, o_busy);
       endcase
    end
 
-`ifdef	FORMAL
+   `ifdef	FORMAL
       // state should never go beyond 13
       always @(*)
          assert(state <= 4'hd);
@@ -118,7 +112,7 @@ module top(i_clk, o_led, o_led_row_0, i_request, o_busy);
          // assert($onehot(o_led));
          // and avoided this case statement entirely.
       end
-`endif
+   `endif
 
 endmodule
 

tdc/Makefile

@@ -1,10 +1,12 @@
 SIM_TARGET = build/top
 BIN_TARGET = build/top.bin
-PCF = iceFUN.pcf
+PCF = constraints/iceFUN.pcf
+TIMING = constraints/timing.py
 YOSYS = yosys
 PNR = nextpnr-ice40
 IPACK = icepack
 BURN = iceFUNprog
+SBY = sby
 
 VERILATOR=verilator
 VERILATOR_ROOT ?= $(shell bash -c 'verilator -V|grep VERILATOR_ROOT | head -1 | sed -e "s/^.*=\s*//"')
@@ -12,43 +14,59 @@ VINC := $(VERILATOR_ROOT)/include
 
 RTL_SRC := $(wildcard rtl/*.v)
 SIM_SRC := $(wildcard sim/*.cc)
+FV_SRC := sim/top.sby
+
 BUILD_DIR := ./build
 
-.PHONY: all burn
+define colorecho
+      @tput setaf 6
+      @echo $1
+      @tput sgr0
+endef
+
+.PHONY: all burn fv clean sim
 all: $(SIM_TARGET)  $(BIN_TARGET)
 
-# -GWIDTH=5 allows passing parameter to verilog module
 $(BUILD_DIR)/Vtop.cc: $(RTL_SRC)
-	@echo "Running verilator"
-	@mkdir -p $(BUILD_DIR)
-	@$(VERILATOR) --trace -Wall -GWIDTH=10 -cc $^ --top-module top\
+	$(call colorecho, "Running verilator")
+	mkdir -p $(BUILD_DIR)
+	$(VERILATOR) --trace -Wall -cc $^ --top-module top -GWIDTH=10\
 		--Mdir $(BUILD_DIR) --timescale-override 10ns/1ns
 
 $(BUILD_DIR)/Vtop__ALL.a: $(BUILD_DIR)/Vtop.cc
-	@make --no-print-directory -C $(BUILD_DIR) -f Vtop.mk
+	make --no-print-directory -C $(BUILD_DIR) -f Vtop.mk
 
 # std=c++11 flag is needed as of verilator v4.100
 $(SIM_TARGET): $(SIM_SRC) $(BUILD_DIR)/Vtop__ALL.a
-	@echo "Compiling simulation executable"
-	@g++ -I$(VINC) -I$(BUILD_DIR) -std=c++14 $(VINC)/verilated.cpp\
+	$(call colorecho, "Compiling simulation executable")
+	g++ -I$(VINC) -I$(BUILD_DIR) -std=c++14 $(VINC)/verilated.cpp\
 		$(VINC)/verilated_vcd_c.cpp $^ -o $@
-	@echo "Run simulation with ./$(SIM_TARGET)"
+	echo "Run simulation with ./$(SIM_TARGET)"
 
 $(BUILD_DIR)/top.json: $(RTL_SRC)
-	@echo "Synthesizing ..."
-	@mkdir -p $(BUILD_DIR)
-	@$(YOSYS) -p "synth_ice40 -top top -json build/top.json" -q $^
+	$(call colorecho, "Synthesizing ...")
+	mkdir -p $(BUILD_DIR)
+	$(YOSYS) -p "synth_ice40 -top top -json build/top.json" -q $^
 
-$(BIN_TARGET): $(BUILD_DIR)/top.json $(PCF)
-	@echo "Routing and building binary stream ..."
-	@$(PNR) -r --hx8k --json $< --package cb132 \
-		--asc $(BUILD_DIR)/top.asc --opt-timing --pcf $(PCF) -q
-	@$(IPACK) $(BUILD_DIR)/top.asc $@
-	@echo "Done!"
+$(BIN_TARGET): $(BUILD_DIR)/top.json $(PCF) $(TIMING)
+	$(call colorecho, "Routing and building binary stream ...") 
+	$(PNR) -r --hx8k --json $< --package cb132 \
+		--asc $(BUILD_DIR)/top.asc --opt-timing --pcf $(PCF) \
+		--pre-pack $(TIMING) -l $(BUILD_DIR)/pnr_report.txt -q 
+	$(IPACK) $(BUILD_DIR)/top.asc $@
+	$(call colorecho, "Done!")
+
+sim: $(SIM_TARGET)
+	$(call colorecho, "Running simulation")
+	$(SIM_TARGET) && open $(BUILD_DIR)/waveform.vcd
 
 burn: $(BIN_TARGET)
-	@$(BURN) $<
+	$(BURN) $<
+
+fv:
+	$(SBY) -f $(FV_SRC) -d $(BUILD_DIR)/fv
 
-.PHONY: clean
 clean:
 	rm -rf $(BUILD_DIR)
+
+$V.SILENT:

tdc/constraints/iceFUN.pcf

@@ -0,0 +1,17 @@
+# For iceFUN board
+
+set_io --warn-no-port i_clk  	P7
+set_io --warn-no-port i_startN 	C11
+set_io --warn-no-port i_stopN 	A11
+set_io --warn-no-port i_resetN 	C6
+
+set_io --warn-no-port o_led_row_0	A12
+set_io --warn-no-port o_dataN[0] 	C10
+set_io --warn-no-port o_dataN[1] 	A10
+set_io --warn-no-port o_dataN[2] 	D7
+set_io --warn-no-port o_dataN[3] 	D6
+set_io --warn-no-port o_dataN[4] 	A7
+set_io --warn-no-port o_dataN[5] 	C7
+
+set_io --warn-no-port o_ledN 	A4
+set_io --warn-no-port o_readyN 	C4

tdc/constraints/timing.py

@@ -0,0 +1 @@
+ctx.addClock("i_clk", 100)

tdc/iceFUN.pcf

@@ -1,5 +0,0 @@
-# For iceFUN board
-
-set_io --warn-no-port o_led 	C10
-set_io --warn-no-port i_clk  	P7
-set_io --warn-no-port lcol1	A12

tdc/rtl/clk_gen.v

@@ -1,11 +1,17 @@
 `default_nettype none
 // dummy clock generator, should be replaced by a PLL clock gen eventually
-module clk_gen(
+module clk_gen #(parameter DIVISION=22)(
    input wire i_clk,
    output wire o_clk
 );
 
-assign o_clk = i_clk;
+reg [DIVISION-1:0] counter = 0;
+
+always @(posedge i_clk) begin
+   counter <= counter + 1;
+end
+
+assign o_clk = counter[DIVISION-1];
 
 endmodule
 // Local Variables:

tdc/rtl/tdc.v

@@ -0,0 +1,81 @@
+`default_nettype none
+
+module tdc #(parameter COUNTER_WIDTH=16)(
+   input wire i_clk,
+   input wire i_start,
+   input wire i_stop,
+   input wire i_reset,
+   output wire o_ready,
+   output wire [COUNTER_WIDTH-1:0] o_data
+);
+
+reg [COUNTER_WIDTH-1:0] counter;
+assign o_data = counter;
+
+// states
+localparam state_idle = 2'b00;
+localparam state_started = 2'b01;
+localparam state_running = 2'b10;
+localparam state_stopped = 2'b11;
+reg [1:0] current_state, next_state;
+
+// ensure that state changes each clock
+always @(posedge i_clk) begin
+   if (i_reset) begin
+      current_state <= state_idle;
+   end else begin
+      current_state <= next_state;
+   end
+end
+
+// state logic
+/* verilator lint_off COMBDLY */
+always @(*) begin
+   case (current_state)
+      state_idle: begin
+         if (i_start && (~i_stop))
+            next_state <= state_started;
+         else
+            next_state <= state_idle;
+      end
+      state_started: begin
+         if (~i_start && (~i_stop))
+            next_state <= state_running;
+         else
+            next_state <= state_started;
+      end
+      state_running: begin
+         if (~i_start && (i_stop))
+            next_state <= state_stopped;
+         else
+            next_state <= state_running;
+      end
+      state_stopped: begin
+         if (i_reset)
+            next_state <= state_idle;
+         else
+            next_state <= state_stopped;
+      end
+
+      default : next_state <= current_state;
+   endcase
+end
+/* verilator lint_on COMBDLY */
+
+// counter runs during running state only
+always @(posedge i_clk) begin
+   case (current_state)
+      state_idle: counter <= 0;
+      state_started: counter <= 0;
+      state_running: counter <= counter + 1;
+      state_stopped: counter <= counter;
+      default : counter <= 0;
+   endcase
+end
+
+assign o_ready = (current_state == state_stopped);
+
+endmodule
+// Local Variables:
+// verilog-library-directories:(".." "./rtl" ".")
+// End:

tdc/rtl/top.v

@@ -1,26 +1,44 @@
 `default_nettype  none
 
-module top(i_clk, o_led, lcol1);
-   parameter WIDTH = 24;
-   input wire i_clk;
-   output wire o_led;
-   output wire lcol1;
+module top #(parameter WIDTH=24)(
+   input wire i_clk,
+   input wire i_startN,
+   input wire i_stopN,
+   input wire i_resetN,
+   output wire o_ledN,
+   output wire o_readyN,
+   output wire [5:0] o_dataN,
+   output wire o_led_row_0
+);
+   wire clk_3Hz;
+   reg buf_led = 0;
+   wire buf_ready;
+   wire [5:0] buf_data;
+   assign o_readyN = ~buf_ready;
+   assign o_dataN = ~buf_data;
 
-   wire clk_12MHz;
-
-   clk_gen clk_gen_0 (/*autoinst*/
+   clk_gen #(.DIVISION(22)) clk_gen0 (/*autoinst*/
                       // Outputs
-      .o_clk                 (clk_12MHz),
+                      .o_clk            (clk_3Hz),
                       // Inputs
                       .i_clk            (i_clk));
 
-   reg [WIDTH-1:0] counter;
+   tdc #(.COUNTER_WIDTH(6)) tdc0 (/*autoinst*/
+            // Outputs
+            .o_ready                    (buf_ready),
+            .o_data                     (buf_data),
+            // Inputs
+            .i_clk                      (clk_3Hz),
+            .i_start                    (~i_startN),
+            .i_stop                     (~i_stopN),
+            .i_reset                   (~i_resetN));
 
-   always @(posedge clk_12MHz)
-      counter <= counter + 1'b1;
+   always @(posedge clk_3Hz) begin
+      buf_led <= ~buf_led;
+   end
 
-   assign o_led = counter[WIDTH-1];
-   assign lcol1 = 1'b0;
+   assign o_ledN = ~buf_led;
+   assign o_led_row_0 = 1'b0;
 endmodule
 
 // Local Variables:

tdc/sim/top.cc

@@ -32,16 +32,38 @@ int main(int argc, char **argv) {
    tb->trace(tfp, 00);
    tfp->open("build/waveform.vcd");
 
+   tb->i_resetN = 1;
+   tb->i_startN = 1;
+   tb->i_stopN = 1;
    unsigned tickcount = 0;
-  int last_led = tb->o_led;
-
-	for(int k=0; k<(1 << 12); k++) {
+   for (int k = 0; k < 2; k++) 
       tick(++tickcount, tb, tfp);
 
-    if (last_led != tb->o_led) {
-      printf("k = %7d, led = %d\n", k, tb->o_led);
-    }
+   tb->i_resetN = 0;
+   tick(++tickcount, tb, tfp);
+   tb->i_resetN = 1;
 
-    last_led = tb->o_led;
-	}
+   for (int k = 0; k < 3; k++) 
+      tick(++tickcount, tb, tfp);
+
+   tb->i_startN = 0;
+   tick(++tickcount, tb, tfp);
+   tb->i_startN = 1;
+
+   for (int k = 0; k < 15; k++) 
+      tick(++tickcount, tb, tfp);
+
+   tb->i_stopN = 0;
+   tick(++tickcount, tb, tfp);
+   tb->i_stopN = 1;
+
+   for (int k = 0; k < 3; k++) 
+      tick(++tickcount, tb, tfp);
+
+   tb->i_resetN = 0;
+   tick(++tickcount, tb, tfp);
+   tb->i_resetN = 1;
+
+   for (int k = 0; k < 3; k++) 
+      tick(++tickcount, tb, tfp);
 }

wb-tut4/Makefile

@@ -0,0 +1,68 @@
+SIM_TARGET = build/top
+BIN_TARGET = build/top.bin
+PCF = constraints/iceFUN.pcf
+TIMING = constraints/timing.py
+YOSYS = yosys
+PNR = nextpnr-ice40
+IPACK = icepack
+BURN = iceFUNprog
+SBY = sby
+
+VERILATOR=verilator
+VERILATOR_ROOT ?= $(shell bash -c 'verilator -V|grep VERILATOR_ROOT | head -1 | sed -e "s/^.*=\s*//"')
+VINC := $(VERILATOR_ROOT)/include
+
+RTL_SRC := $(wildcard rtl/*.v)
+SIM_SRC := $(wildcard sim/*.cc)
+FV_SRC := sim/top.sby
+
+BUILD_DIR := ./build
+
+define colorecho
+      @tput setaf 6
+      @echo $1
+      @tput sgr0
+endef
+
+.PHONY: all burn fv clean
+all: $(SIM_TARGET)  $(BIN_TARGET)
+
+$(BUILD_DIR)/Vtop.cc: $(RTL_SRC)
+	$(call colorecho, "Running verilator")
+	mkdir -p $(BUILD_DIR)
+	$(VERILATOR) --trace -Wall -cc $^ --top-module top\
+		--Mdir $(BUILD_DIR) --timescale-override 10ns/1ns
+
+$(BUILD_DIR)/Vtop__ALL.a: $(BUILD_DIR)/Vtop.cc
+	make --no-print-directory -C $(BUILD_DIR) -f Vtop.mk
+
+# std=c++11 flag is needed as of verilator v4.100
+$(SIM_TARGET): $(SIM_SRC) $(BUILD_DIR)/Vtop__ALL.a
+	$(call colorecho, "Compiling simulation executable")
+	g++ -I$(VINC) -I$(BUILD_DIR) -std=c++14 $(VINC)/verilated.cpp\
+		$(VINC)/verilated_vcd_c.cpp $^ -o $@
+	echo "Run simulation with ./$(SIM_TARGET)"
+
+$(BUILD_DIR)/top.json: $(RTL_SRC)
+	$(call colorecho, "Synthesizing ...")
+	mkdir -p $(BUILD_DIR)
+	$(YOSYS) -p "synth_ice40 -top top -json build/top.json" -q $^
+
+$(BIN_TARGET): $(BUILD_DIR)/top.json $(PCF) $(TIMING)
+	$(call colorecho, "Routing and building binary stream ...") 
+	$(PNR) -r --hx8k --json $< --package cb132 \
+		--asc $(BUILD_DIR)/top.asc --opt-timing --pcf $(PCF) \
+		--pre-pack $(TIMING) -l $(BUILD_DIR)/pnr_report.txt -q 
+	$(IPACK) $(BUILD_DIR)/top.asc $@
+	$(call colorecho, "Done!")
+
+burn: $(BIN_TARGET)
+	$(BURN) $<
+
+fv:
+	$(SBY) -f $(FV_SRC) -d $(BUILD_DIR)/fv
+
+clean:
+	rm -rf $(BUILD_DIR)
+
+$V.SILENT:

wb-tut4/constraints/iceFUN.pcf

@@ -0,0 +1,14 @@
+# For iceFUN board
+
+set_io --warn-no-port i_clk  	P7
+set_io --warn-no-port i_request 	A5
+
+set_io --warn-no-port o_led_row_0	A12
+set_io --warn-no-port o_led[0] 	C10
+set_io --warn-no-port o_led[1] 	A10
+set_io --warn-no-port o_led[2] 	D7
+set_io --warn-no-port o_led[3] 	D6
+set_io --warn-no-port o_led[4] 	A7
+set_io --warn-no-port o_led[5] 	C7
+# set_io --warn-no-port o_led[6] 	A4
+set_io --warn-no-port o_busy 	C4

wb-tut4/constraints/timing.py

@@ -0,0 +1 @@
+ctx.addClock("i_clk", 100)

wb-tut4/rtl/clk_gen.v

@@ -0,0 +1,13 @@
+`default_nettype none
+// dummy clock generator, should be replaced by a PLL clock gen eventually
+module clk_gen(
+   input wire i_clk,
+   output wire o_clk
+);
+
+assign o_clk = i_clk;
+
+endmodule
+// Local Variables:
+// verilog-library-directories:(".." "./rtl" ".")
+// End:

wb-tut4/rtl/top.v

@@ -0,0 +1,70 @@
+`default_nettype  none
+
+module top(i_clk,
+   i_cyc, i_stb, i_we, i_addr, i_data,
+   o_stall, o_ack, o_data,
+   o_led, o_led_row_0);
+input	wire		i_clk;
+//
+// Our wishbone bus interface
+input	wire		i_cyc, i_stb, i_we;
+input	wire		i_addr;
+input	wire	[31:0]	i_data;
+//
+output	wire		o_stall;
+output	reg		o_ack;
+output	wire	[31:0]	o_data;
+//
+// The output LED
+output wire o_led_row_0;
+output	reg	[5:0]	o_led;
+
+wire		busy;
+reg	[3:0]	state;
+
+initial	state = 0;
+always @(posedge i_clk) begin
+   if ((i_stb)&&(i_we)&&(!o_stall))
+      state <= 4'h1;
+   else if (state >= 4'd11)
+      state <= 4'h0;
+   else if (state != 0)
+      state <= state + 1'b1;
+end
+
+always @(posedge i_clk) begin
+   case(state)
+      4'h1: o_led <= 6'b00_0001;
+      4'h2: o_led <= 6'b00_0010;
+      4'h3: o_led <= 6'b00_0100;
+      4'h4: o_led <= 6'b00_1000;
+      4'h5: o_led <= 6'b01_0000;
+      4'h6: o_led <= 6'b10_0000;
+      4'h7: o_led <= 6'b01_0000;
+      4'h8: o_led <= 6'b00_1000;
+      4'h9: o_led <= 6'b00_0100;
+      4'ha: o_led <= 6'b00_0010;
+      4'hb: o_led <= 6'b00_0001;
+      default: o_led <= 6'b00_0000;
+   endcase
+end
+
+assign	busy = (state != 0);
+
+initial	o_ack = 1'b0;
+always @(posedge i_clk)
+   o_ack <= (i_stb)&&(!o_stall);
+
+assign	o_stall = (busy)&&(i_we);
+assign	o_data = { 28'h0, state };
+assign o_led_row_0 = 0;
+
+// Verilator lint_off UNUSED
+wire	[33:0]	unused;
+assign	unused = { i_cyc, i_addr, i_data };
+// Verilator lint_on  UNUSED
+//
+endmodule
+// Local Variables:
+// verilog-library-directories:(".." "./rtl" ".")
+// End:

wb-tut4/sim/top.cc

@@ -0,0 +1,118 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include "Vtop.h"
+#include "verilated.h"
+#include "verilated_vcd_c.h"
+
+int	tickcount = 0;
+Vtop	*tb;
+VerilatedVcdC	*tfp;
+
+void	tick(void) {
+   tickcount++;
+
+   tb->eval();
+   if (tfp)
+      tfp->dump(tickcount * 10 - 2);
+   tb->i_clk = 1;
+   tb->eval();
+   if (tfp)
+      tfp->dump(tickcount * 10);
+   tb->i_clk = 0;
+   tb->eval();
+   if (tfp) {
+      tfp->dump(tickcount * 10 + 5);
+      tfp->flush();
+   }
+}
+
+unsigned wb_read(unsigned a) {
+   tb->i_cyc = tb->i_stb = 1;
+   tb->i_we  = 0;
+   tb->eval();
+   tb->i_addr= a;
+   // Make the request
+   while(tb->o_stall)
+      tick();
+   tick();
+   tb->i_stb = 0;
+   // Wait for the ACK
+   while(!tb->o_ack)
+      tick();
+   // Idle the bus, and read the response
+   tb->i_cyc = 0;
+   return tb->o_data;
+}
+
+void wb_write(unsigned a, unsigned v) {
+   tb->i_cyc = tb->i_stb = 1;
+   tb->i_we  = 1;
+   tb->eval();
+   tb->i_addr= a;
+   tb->i_data= v;
+   // if busy, keep ticking
+   while(tb->o_stall)
+      tick();
+   // Then, make the bus request 
+   tick();
+   // and pull stb down
+   tb->i_stb = 0;
+   // Wait for the acknowledgement
+   while(!tb->o_ack)
+      tick();
+   // Idle the bus and return
+   tb->i_cyc = tb->i_stb = 0;
+}
+
+int main(int argc, char **argv) {
+   int	last_led, last_state = 0, state = 0;
+
+   // Call commandArgs first!
+   Verilated::commandArgs(argc, argv);
+
+   // Instantiate our design
+   tb = new Vtop;
+
+   // Generate a trace
+   Verilated::traceEverOn(true);
+   tfp = new VerilatedVcdC;
+   tb->trace(tfp, 99);
+   tfp->open("build/waveform.vcd");
+
+   last_led = tb->o_led;
+
+   // Read from the current state
+   printf("Initial state is: 0x%02x\n",
+         wb_read(0));
+
+   for(int cycle=0; cycle<2; cycle++) {
+      // Wait five clocks
+      for(int i=0; i<5; i++)
+         tick();
+
+      // Start the LEDs cycling
+      wb_write(0,0);
+      tick();
+
+      while((state = wb_read(0))!=0) {
+         if ((state != last_state)
+               ||(tb->o_led != last_led)) {
+            printf("%6d: State #%2d ",
+                  tickcount, state);
+            for(int j=0; j<6; j++) {
+               if(tb->o_led & (1<<j))
+                  printf("O");
+               else
+                  printf("-");
+            } printf("\n");
+         } tick();
+
+         last_state = state;
+         last_led = tb->o_led;
+      }
+   }
+
+   tfp->close();
+   delete tfp;
+   delete tb;
+}

wb-tut4/sim/top.sby

@@ -0,0 +1,13 @@
+[options]
+mode prove
+
+[engines]
+smtbmc
+
+[script]
+read -formal *.v
+prep -top top
+
+[files]
+rtl/top.v
+rtl/clk_gen.v