fixing formal workflow and adding tests with pat

Author: stevej

.github/workflows/formal.sh renamed to .github/workflows/formal.yaml

@@ -1,4 +1,4 @@
-![](../../workflows/gds/badge.svg) ![](../../workflows/docs/badge.svg) ![](../../workflows/test/badge.svg) ![](../../workflows/fpga/badge.svg)
+![](../../workflows/gds/badge.svg) ![](../../workflows/docs/badge.svg) ![](../../workflows/test/badge.svg) ![](../../workflows/fpga/badge.svg) ![](../../workflows/docs/formal.svg)
 
 # TinyQV Full Peripheral Template for Tiny Tapeout
 

README.md

@@ -35,50 +35,45 @@ module tqvp_stevej_watchdog (
     reg [31:0] window_start;
     reg [31:0] window_close;
     reg watchdog_enabled; // has the user enabled the design
-    reg pat; // has the user patted the watchdog this window?
     reg saw_pat; // destination is an output pin, driving high means the watchdog was pat and reset.
 
     always @(posedge clk) begin
         if (!rst_n) begin
             window_start <= 32'b0;
             window_close <= 32'b0;
             watchdog_enabled <= 1'b0;
-            pat <= 1'b0;
             saw_pat <= 1'b0;
             timer <= 32'b0;
         end else begin
+            watchdog_enabled <= watchdog_enabled;
+            timer <= timer;
+            window_start <= window_start;
+            window_close <= window_close;
+            saw_pat <= saw_pat;
+            
             if (address == 6'h0) begin // Address 0 is ENABLE
                 if (data_write_n != 2'b11) begin
-                    watchdog_enabled <= data_in[0];
+                    watchdog_enabled <= 1;
                     timer <= 32'b0;
                 end
-            end
-
-            if (address == 6'h1) begin // Address 1 is WINDOW_START
+            end else if (address == 6'h1) begin // Address 1 is WINDOW_START
                 if (data_write_n != 2'b11) begin
                     window_start <= data_in;
                 end
-            end
-
-            if (address == 6'h2) begin // Address 2 is WINDOW_CLOSE
+            end else if (address == 6'h2) begin // Address 2 is WINDOW_CLOSE
                 if (data_write_n != 2'b11) begin
                     window_close <= data_in;
                 end
-            end
-
-            if (address == 6'h3) begin // Address 3 is PAT
+            end else if (address == 6'h3) begin // Address 3 is PAT
                 if (data_write_n != 2'b11) begin
                     saw_pat <= 1'b1;
                     timer <= 32'b0;
                 end
-            end else begin
-                saw_pat <= 1'b0;
             end
 
             if (!timer_expired) begin
                 timer <= timer + 32'b1;
             end
-
         end
     end
 
@@ -95,9 +90,11 @@ module tqvp_stevej_watchdog (
     assign after_window_close = timer > window_close;
 
     assign timer_expired = watchdog_enabled && after_window_start && after_window_close;
+
     assign interrupt_high = timer_expired;
     assign interrupt_low = !timer_expired;
     assign user_interrupt = interrupt_high;
+
     assign uo_out = {interrupt_high, interrupt_low, saw_pat, watchdog_enabled, after_window_start, after_window_close, 2'b00};
 
     // Addresses

src/peripheral.v

@@ -58,19 +58,27 @@ async def test_enabled_with_window_close(dut):
 
     dut._log.info("Test project behavior")
     # Test writing 10 to WATCHDOG_CLOSE register
-    await tqv.write_word_reg(2, 0xA)
-    assert await tqv.read_word_reg(2) == 0xA
+    await tqv.write_word_reg(2, 0xAAA)
+    assert await tqv.read_word_reg(2) == 0xAAA
 
     # Test enabling watchdog timer by writing to interrupt.
     await tqv.write_word_reg(0, 0x1)
+    assert await tqv.read_word_reg(0) == 0x1
+
+    # Send pat immediately
+    await tqv.write_word_reg(3, 0x1)
+    assert await tqv.read_word_reg(3) == 0x1
 
-    await ClockCycles(dut.clk, 5)
-    # no interrupts, no pat seen, watchdog has been enabled, timer not expired
-    assert dut.uo_out.value == 0b01010000
+    await ClockCycles(dut.clk, 0xAA)
+    assert dut.uo_out.value != 0b10111100 # we should not trigger at this point.
+
+    # Checking that the watchdog does eventually fire
+    await ClockCycles(dut.clk, 0xAAA)
+    assert dut.uo_out.value == 0b10111100
 
 # Test that enabling the watchdog timer with a WINDOW_CLOSE of 10 results in an expired timer in 10 cycles.
 @cocotb.test()
-async def test_enabled_with_window_close(dut):
+async def test_enabled_with_window_close2_and_immediate_pat(dut):
     dut._log.info("Start")
 
     # Set the clock period to 100 ns (10 MHz)
@@ -89,84 +97,47 @@ async def test_enabled_with_window_close(dut):
     dut._log.info("Test project behavior")
     # Set WINDOW_CLOSE
     await tqv.write_word_reg(2, 0xAAA) # 2730 cycles
+    assert await tqv.read_word_reg(2) == 0xAAA
 
     # Test enabling watchdog timer by writing to interrupt.
     await tqv.write_word_reg(0, 0x1)
 
+    # Send pat immediately
+    await tqv.write_word_reg(3, 0x1)
+    assert await tqv.read_word_reg(3) == 0x1
+
     await ClockCycles(dut.clk, 1)
     # watchdog has been enabled, no pat seen, timer expired
     # no interrupt, no pat seen, watchdog enabled, after_window_start, window has not closed.
-    assert dut.uo_out.value == 0b01011000 # this is actually 0b10011100 so the timer has expired after 1 clock cycle.
+    assert dut.uo_out.value != 0b10011100 # we should not have triggered.
+    assert dut.uo_out.value == 0b01111000
 
     # Check that the watchdog is enabled but not triggered for 10 cycles.
     for _ in range(10):
       await ClockCycles(dut.clk, 1)
       # watchdog has been enabled, no pat seen, timer expired
       # no interrupt, no pat seen, watchdog enabled, after_window_start, window has not closed.
-      assert dut.uo_out.value == 0b01011000
+      assert dut.uo_out.value == 0b01111000
 
     # TODO: Mystery! For some unknown reason we only need 101, and not (2730 - already used) cycles, for the watchdog to trigger.
-    await ClockCycles(dut.clk, 101)
+    await ClockCycles(dut.clk, 0xAAA)
     # interrupt, watchdog enabled, after_window_start, after_window_close
-    assert dut.uo_out.value == 0b1001_1100
+    assert dut.uo_out.value == 0b1011_1100
 
     # interrupts, no pat seen, watchdog enabled, after_window_start
     # After enough clock cycles, this should be 0b10011000 which indicates the watchdog has been triggered.
     timer_elapsed = 0
     for _ in range(10):
-        if dut.uo_out.value != 0b0101_1000:
-            assert dut.uo_out.value == 0b1001_1100
-        if dut.uo_out.value == 0b1001_1100:
+        if dut.uo_out.value != 0b0111_1000:
+            assert dut.uo_out.value == 0b1011_1100
+        if dut.uo_out.value == 0b1011_1100:
             timer_elapsed = 1
     assert timer_elapsed
 
 
   # Test that enabling the watchdog timer with a WINDOW_OPEN of 5 and a WINDOW_CLOSE of 10 doesn't 
   # trigger outside the window but does trigger inside the window.
 
-# Test that enabling the watchdog timer with a WINDOW_CLOSE of 10 results in an expired timer in 10 cycles.
-@cocotb.test()
-async def test_enabled_with_window_start_and_close_no_pat(dut):
-    dut._log.info("Start")
-
-    # Set the clock period to 100 ns (10 MHz)
-    clock = Clock(dut.clk, 100, units="ns")
-    cocotb.start_soon(clock.start())
-
-    # Interact with your design's registers through this TinyQV class.
-    # This will allow the same test to be run when your design is integrated
-    # with TinyQV - the implementation of this class will be replaces with a
-    # different version that uses Risc-V instructions instead of the SPI 
-    # interface to read and write the registers.
-    tqv = TinyQV(dut)
-    # Reset
-    await tqv.reset()
-
-    dut._log.info("Test project behavior")
-    # Writing 5 to WATCHDOG_START register
-    await tqv.write_word_reg(1, 0x5)
-    # Writing 10 to WATCHDOG_CLOSE register
-    await tqv.write_word_reg(2, 0xBBB)
-    # Enabling watchdog timer
-    await tqv.write_word_reg(0, 0x1)
-
-    await ClockCycles(dut.clk, 1)
-    # watchdog should not have tripped after 1 cycle when configured for 0xBBB cycles
-    assert dut.uo_out.value != 0b10011000
-    assert dut.uo_out.value == 0b01011100
-
-    # The watchdog should not trigger in less cycles than configured.
-    await ClockCycles(dut.clk, 0xAA)
-    # If this assertion fails, the watchdog triggered too quickly from our perspective.
-    assert dut.uo_out.value != 0b10011100
-
-    await ClockCycles(dut.clk, 0xA00)
-    assert dut.uo_out.value == 0b01111000
-
-    await ClockCycles(dut.clk, 0xBBB)
-    assert dut.uo_out.value == 0b10111100
-
-
 
 # Test that enabling the watchdog timer with a WINDOW_CLOSE of 10 results in an expired timer in 10 cycles.
 @cocotb.test()
@@ -194,7 +165,7 @@ async def test_enabled_with_window_start_and_close_early_pat(dut):
     # Enabling watchdog timer
     await tqv.write_word_reg(0, 0x1)
 
-    # immediately patting
+    # immediately patting to reset the timer.
     await tqv.write_word_reg(3, 0x1)