adds formal tests to workflow, adds a harden script, more tests

.github/workflows/formal.yaml

@@ -0,0 +1,23 @@
+name: formal
+
+on:
+  [push, workflow_dispatch]
+
+jobs:
+  formal:
+    runs-on: ubuntu-latest
+    steps:
+      - name: checkout repo
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: install oss-cad-suite
+        uses: YosysHQ/setup-oss-cad-suite@v3
+
+      - name: Run formal tests
+        working-directory: ./src
+        shell: bash
+        run: |
+          ./formal.sh
+

.gitignore

@@ -16,3 +16,4 @@ src/formal/
 src/formal_bmc/
 src/formal_cover/
 src/formal_prove/
+~

README.md

@@ -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/formal/badge.svg) ![](../../workflows/fpga/badge.svg)
 
 # Tiny Tapeout Verilog Project Template
 

harden.sh

@@ -0,0 +1 @@
+tt/tt_tool.py --create-user-config --harden --openlane2

src/formal.sby

@@ -19,7 +19,11 @@ cover: smtbmc z3
 read -formal jtag.v
 prep -top jtag
 memory_map -rom-only
+# use this to help track down PREUNSAT, only works on a single module at a time.
+# hierarchy -check; proc; opt
+# sat -prove-asserts -set-assumes
 
 [files]
 jtag.v
-byte_transmitter.v
+byte_transmitter.v
+mux_2_1.v

src/jtag.v

@@ -5,6 +5,7 @@
 `timescale 1us / 100 ns
 
 `include "byte_transmitter.v"
+`include "mux_2_1.v"
 
 // Ensures that the first_state happens before the second_state.
 // We use a label as a breadcrumb in case an invalid state is asserted
@@ -19,14 +20,15 @@ module jtag (
     input wire tdi,
     output wire tdo,
     input wire tms,
-    input wire trst,
+    input wire trst_n,
     input wire reset, // comes from main domain clock.
     output in_reset
 );
 
-  // IDCODE of our jtag device.
-  localparam [31:0] IDCODE = 32'hFAF0;
+  wire trst;
+  assign trst = ~trst_n;
 
+  // TAP controller state
   localparam [4:0] TestLogicReset = 5'h0;
   localparam [4:0] RunTestOrIdle = 5'h1;
   localparam [4:0] SelectDrScan = 5'h2;
@@ -45,11 +47,24 @@ module jtag (
   localparam [4:0] UpdateIr = 5'h15;
 
   reg [4:0] current_state;
+
+  // IR Instruction values
+  localparam [3:0] Abort  = 4'b1000;
+  localparam [3:0] IdCode = 4'b1110;
+  localparam [3:0] Bypass = 4'b1111;
+
+  reg [3:0] current_ir_instruction;
+
+  // DR Register containing the IDCODE of our jtag device.
+  localparam [31:0] IdCodeDrRegister = 32'hFAF0;
+
   reg r_in_reset;
-  //
+  // whether a reset in the main design has been seen.
   wire r_in_reset_from_main_clk;
   assign in_reset = r_in_reset;
+
   // for checking that the TAP state machine is in reset at the right time.
+  // TODO: move this behind an `ifdef FORMAL and prefix with `f_`
   reg [4:0] tms_reset_check;
   reg [7:0] cycles;
 
@@ -59,12 +74,15 @@ module jtag (
 
   byte_transmitter id_byte_transmitter(
     .clk(tck),
-    .reset(~trst),
+    .reset(trst), // TODO: is TRST is active low so always high?
     .enable(1'b1), // TODO: this is where mux goes.
-    .in(IDCODE),
+    .in(IdCodeDrRegister),
     .out(transmitter_channel), // make this another wire.
     .done(idcode_out_done));
 
+  wire reset_;
+  assign reset_ = ~trst;
+
 reg r_output_selector_transmitter;  // 1 means TAP controller, 0 means byte transmitter
 mux_2_1 output_mux (
     .one(tap_channel),
@@ -77,15 +95,18 @@ mux_2_1 output_mux (
   // a small synchronizer.
   // A single cycle pulse on output for each pulse on input:
   (* ASYNC_REG = "TRUE" *) reg [2:0] sync;
-  always @(posedge tck) sync <= (sync << 1) | {1'b0, 1'b0, reset};
+  always @(posedge tck) begin
+    sync <= (sync << 1) | {1'b0, 1'b0, reset};
+  end
   assign r_in_reset_from_main_clk = sync[1] & !sync[2];
 
   always @(posedge tck) begin
-    if (trst | r_in_reset_from_main_clk) begin
-      current_state <= TestLogicReset;  // 0
+    if (trst) begin
+      current_state <= TestLogicReset;  // State 0
       tms_reset_check <= 5'b0_0000;
       cycles <= 0;
       r_in_reset <= 1;
+      current_ir_instruction <= 4'b1110; // IDCODE is the default instruction.
       r_output_selector_transmitter <= 1; // by default the tap controller writes
       tap_channel <= 0;
     end else begin
@@ -99,7 +120,6 @@ mux_2_1 output_mux (
           r_in_reset <= 1;
           tms_reset_check <= 5'b0_0000;
           tap_channel <= 0;
-
           case (tms)
             1: current_state <= TestLogicReset;
             default: current_state <= RunTestOrIdle;
@@ -131,15 +151,25 @@ mux_2_1 output_mux (
           default: current_state <= ShiftIr;
         endcase
         ShiftDr:  // 6
+        // in the Shift-DR state, this data is shifted out, least significant bit first
         // Pretty sure this means connect a shift register to TDO and drain it
         case (tms)
           1: current_state <= Exit1Dr;
-          default: begin
-            // place the byte transmitter with the IDCODE register and start to shift it onto TDO. 
-            if (!idcode_out_done) begin
-            end else begin
+          default: begin /*
+            case (current_ir_instruction)
+              IdCode:  begin
+                // enable the idcode byte transmitter
+                // place the byte transmitter with the IDCODE register and start to shift it onto TDO. 
+              if (!idcode_out_done) begin
+                current_state <= ShiftDr;
+              end else begin
+                current_state <= Exit1Dr; // Not sure if this is correct.
+                end
+              end
+            default: begin
               current_state <= ShiftDr;
             end
+            endcase */
           end
         endcase
         ShiftIr:  // 7

src/project.v

@@ -37,7 +37,7 @@ module tt_um_jtag_example_stevej (
     .tck(ui_in[0]),
     .tdi(ui_in[1]),
     .tms(ui_in[2]),
-    .trst(ui_in[3]),
+    .trst_n(ui_in[3]),
     .tdo(tdo),
     .reset(reset),
     .in_reset(jtag_in_reset));
@@ -57,7 +57,6 @@ minipit minipit0 (
     .interrupting(interrupting)
 );
 
-
   // Set unused wires
   assign uio_out[7:1] = 7'b000_0000;
 

test/test.py

@@ -5,16 +5,17 @@
 from cocotb.clock import Clock
 from cocotb.triggers import ClockCycles
 
+# For reference, the pinout is:
 #    .tck(ui_in[0]),
 #    .tdi(ui_in[1]),
 #    .tms(ui_in[2]),
 #    .trst(ui_in[3]),
 @cocotb.test()
-async def test_rms_five_high_for_reset(dut):
+async def test_tms_five_high_for_reset(dut):
         dut._log.info("Start")
         clock = Clock(dut.clk, 3, units="us")
         cocotb.start_soon(clock.start())
-        dut._log.info("Reset")
+        dut._log.info("Reset the interrupt timer")
         dut.ena.value = 1
         dut.ui_in.value = 0
         dut.uio_in.value = 0
@@ -23,16 +24,21 @@ async def test_rms_five_high_for_reset(dut):
         dut.rst_n.value = 0
         await ClockCycles(dut.clk, 1)
         dut.rst_n.value = 1
+        dut.ui_in.value = 0b0000_1000
         await ClockCycles(dut.clk, 1)
 
-        # Drive TRST and TCK high then low to reset the design.
-        dut.ui_in.value = 0b0000_1001
+        # Drive TRST low and TCK high then low to reset tap controller
+        dut._log.info("Reset the jtag tap controller")
+        dut.ui_in.value = 0b0000_0001
         await ClockCycles(dut.clk, 1)
-        dut.ui_in.value = 0b0000_0000
+        dut.ui_in.value = 0b0000_1000
         await ClockCycles(dut.clk, 1)
         assert dut.uo_out.value == 0x0
 
+        # Drive TCK high/low enough times to see 0xFAF01
+
         # Drive TMS high then low for five cycles to put us into reset.
+        dut._log.info("TMS high for five pulses to reset TAP controller")
         dut.ui_in.value = 0b0000_0111
         await ClockCycles(dut.clk, 1)
         dut.ui_in.value = 0b0000_0110
@@ -63,3 +69,35 @@ async def test_rms_five_high_for_reset(dut):
         await ClockCycles(dut.clk, 1)
         assert dut.uo_out.value == 0x0
 
+# Ensure that IDCODE is returned when asked for
+cocotb.test()
+async def test_idcode(dut):
+        dut._log.info("Start")
+        clock = Clock(dut.clk, 3, units="us")
+        cocotb.start_soon(clock.start())
+        dut._log.info("Reset the interrupt timer")
+        dut.ena.value = 1
+        dut.ui_in.value = 0
+        dut.uio_in.value = 0
+        dut.rst_n.value = 1
+        await ClockCycles(dut.clk, 1)
+        dut.rst_n.value = 0
+        await ClockCycles(dut.clk, 1)
+        dut.rst_n.value = 1
+        await ClockCycles(dut.clk, 1)
+
+        # Drive TRST and TCK high then low to reset tap controller
+        dut._log.info("Reset the jtag tap controller")
+        dut.ui_in.value = 0b0000_1001
+        await ClockCycles(dut.clk, 1)
+        dut.ui_in.value = 0b0000_0000
+        await ClockCycles(dut.clk, 1)
+        assert dut.uo_out.value == 0x0
+
+        # Drive TCK and TMS into ShiftDr state
+        # TMS: 0 1 0 0 to get into ShiftDr
+
+        # Drive TCK high/low enough times to see 0xFAF01
+        for i in range(32):
+        # Code to execute in each iteration
+                print(i)