formally verified with CDC

rtl/Makefile

@@ -5,6 +5,13 @@ all: testbench
 	sed '/^TRACE/ ! d; s/^[^:]*: //;' < testbench.log > testbench.trace
 	cmp ../sim/demo.trace testbench.trace
 
+formal_spi: spi_client.v
+	sby -f spi.sby
+
+testbench_simple: testbench_simple.v top.v memory.v sequencer.v compute.v spi_client.v
+	iverilog -DTRACE -s testbench -o testbench_simple testbench_simple.v top.v memory.v sequencer.v compute.v spi_client.v $(shell yosys-config --datdir/ice40/cells_sim.v)
+	vvp -N testbench_simple
+
 testbench: testbench.v top.v memory.v sequencer.v compute.v spi_client.v
 	iverilog -DTRACE -s testbench -o testbench testbench.v top.v memory.v sequencer.v compute.v spi_client.v $(shell yosys-config --datdir/ice40/cells_sim.v)
 

rtl/spi_client.v

@@ -5,7 +5,7 @@ module spi_client (
     output              o_active,           // high whenever chip selected
 
     input               i_spi_clk,          // spi clock
-    input               i_spi_cs,           // spi chip select, low to select
+    input               i_spi_cs_n,         // spi chip select, low to select
 
     output reg          o_miso,             // output to master
     input               i_mosi,             // input from master
@@ -20,7 +20,7 @@ module spi_client (
 );
 
 
-    assign o_active = !i_spi_cs;
+    assign o_active = !i_spi_cs_n;
 
     // data coming from master goes here
     reg [2:0] in_bit = 0;
@@ -29,29 +29,36 @@ module spi_client (
     // data to send goes here
     reg [2:0] out_bit = 0;
     reg [7:0] data_out = 0;
+    // copy of data_out for the spi_clock domain
+    reg [7:0] data_out_spi = 0;
+    reg [7:0] data_in_spi = 0;
 
 
     reg first_byte = 0;
     reg start_status = 0; // registers data_in_start
 
 
-    always @(posedge i_spi_clk, posedge i_spi_cs) begin
-        if(i_spi_cs) begin                  // reset state
+    always @(posedge i_spi_clk, posedge i_spi_cs_n) begin
+        if(i_spi_cs_n) begin                  // reset state
             in_bit <= 0;
             first_byte <= 1;
         end else begin                      // receiving data
             data_in[3'd7-in_bit] <= i_mosi;
             in_bit <= in_bit + 1;
-            if(in_bit == 7)
+            if(in_bit == 7) begin
+                data_in_spi <= { data_in[7:1], i_mosi };
                 first_byte <= 0;
+            end
         end
     end
 
-    always @(negedge i_spi_clk, posedge i_spi_cs) begin
-        if(i_spi_cs) begin                  // reset state
+    always @(negedge i_spi_clk, posedge i_spi_cs_n) begin
+        if(i_spi_cs_n) begin                  // reset state
             out_bit <= 0;
         end else begin
-            o_miso <= data_out[3'd7-out_bit];
+            if(out_bit == 7)                  // get a local copy of the data to send out - guaranteed stable
+                data_out_spi <= data_out;
+            o_miso <= data_out_spi[3'd7-out_bit];
             out_bit <= out_bit + 1;
         end
     end
@@ -67,6 +74,31 @@ module spi_client (
     localparam DATA_OUT_ENDSTATE = 2;
     reg [$clog2(DATA_OUT_ENDSTATE)-1:0] data_out_state = DATA_OUT_WAIT;
 
+    // clock domain crossing with 2 flip flops and one for what happened one clock ago
+    reg out_bit_clock, out_bit_clock_past, out_bit_clock_pipe;
+    reg in_bit_clock, in_bit_clock_past, in_bit_clock_pipe;
+    reg fb_clock, fb_clock_past, fb_clock_pipe;
+
+    initial begin
+        { out_bit_clock_past, out_bit_clock, out_bit_clock_pipe } = 0;
+        { in_bit_clock_past, in_bit_clock, in_bit_clock_pipe } = 0;
+        { fb_clock, fb_clock_past, fb_clock_pipe } = 3'b111;
+    end
+
+    always @(posedge i_clock) begin
+        { out_bit_clock_past, out_bit_clock, out_bit_clock_pipe } <= { out_bit_clock, out_bit_clock_pipe, out_bit[2] };
+        { in_bit_clock_past, in_bit_clock, in_bit_clock_pipe } <= { in_bit_clock, in_bit_clock_pipe, in_bit == 7 };
+        { fb_clock_past, fb_clock, fb_clock_pipe } <= { fb_clock, fb_clock_pipe, first_byte };
+    end
+
+    initial begin
+        data_in_state <= DATA_IN_WAIT;
+        data_out_state <= DATA_OUT_WAIT;
+        o_data_in_start <= 0;
+        o_data_out_ready <= 0;
+        start_status <= 0;
+    end
+
     always @(posedge i_clock) begin
         if(i_reset) begin
             data_in_state <= DATA_IN_WAIT;
@@ -79,26 +111,26 @@ module spi_client (
 
             case(data_in_state)
                 DATA_IN_WAIT: begin
-                    start_status <= first_byte;
+                    start_status <= fb_clock;
                     o_data_in_valid <= 0;
-                    if(in_bit == 1)
+                    if(in_bit_clock == 1)
                         data_in_state <= DATA_IN_RX;
                 end
                 DATA_IN_RX: begin
-                    if(in_bit == 0)
+                    if(in_bit_clock == 0)
                         data_in_state <= DATA_IN_READY;
                 end 
                 DATA_IN_READY: begin
                     o_data_in_valid <= 1;
                     o_data_in_start <= start_status;
-                    o_data_in_data <= data_in;
+                    o_data_in_data <= data_in_spi;
                     data_in_state <= DATA_IN_WAIT;
                 end
             endcase
 
             case(data_out_state)
                 DATA_OUT_WAIT: begin
-                    if(out_bit == 0)
+                    if({out_bit_clock, out_bit_clock_past} == 2'b10)
                         if(i_data_out_valid) begin
                             data_out <= i_data_out_data;
                             o_data_out_ready <= 1;
@@ -107,7 +139,7 @@ module spi_client (
                 end
                 DATA_OUT_TX: begin
                     o_data_out_ready <= 0;
-                    if(out_bit == 7)
+                    if({out_bit_clock, out_bit_clock_past} == 2'b01)
                         data_out_state <= DATA_OUT_WAIT;
                 end
 
@@ -119,8 +151,10 @@ module spi_client (
     reg [3:0] f_clk_counter;
     initial f_clk_counter = 0;
 
-    initial restrict(i_reset);
-    initial restrict(i_spi_cs);
+    // ASSUMPTIONS
+
+    initial assume(i_reset);
+    initial assume(i_spi_cs_n);
 
     // past valid signal
     reg f_past_valid = 0;
@@ -132,15 +166,79 @@ module spi_client (
         if(f_past_valid)
             assume(i_reset == 0);
 
-    // clock pairing
-    always @($global_clock)
-    begin
-        f_clk_counter <= f_clk_counter + 1'b1;
-        assume(i_clock == f_clk_counter[0]);
-        assume(i_spi_clk == f_clk_counter[1]);
+    // fix sys clock
+    wire [7:0] f_sys_step = 8'h40;
+    reg [7:0] f_sys_counter;
+    reg [7:0] f_spi_counter;
+
+    // system clock
+    always @($global_clock) begin
+        f_sys_counter <= f_sys_counter + f_sys_step;
+        assume ( i_clock == f_sys_counter [7]);
+    end
+
+    // spi clock
+    // allow spi clock to be around 1/4 sys clock
+    (* anyconst *) wire [7:0] f_spi_step;
+    always @(*)
+        assume ((f_spi_step > 8'h05) && (f_spi_step <= 8'h15));
+
+    // spi clock if spi_cs_n
+    always @($global_clock) begin
+        f_spi_counter <= f_spi_counter + f_spi_step;
+        assume ( i_spi_cs_n || i_spi_clk == f_spi_counter [7]);
     end
 
-    // check everything is zeroed on the reset signal
+    // inputs only can change on system clock
+    always @($global_clock) 
+        if(f_past_valid && !$rose(i_clock)) begin
+            assume($stable(i_data_out_valid));
+            assume($stable(i_data_out_data));
+            assume($stable(i_reset));
+        end
+
+    // SPI assumptions
+    // mosi is stable as spi clock rises
+    always @($global_clock) 
+        if(f_past_valid && i_spi_clk) begin
+            assume($stable(i_mosi));
+        end
+
+    // if no clock, no chip select
+    always @(*)
+        if(!i_spi_clk)
+            assume(!i_spi_cs_n);
+
+    // no chip select, no clock
+    always @($global_clock)
+        if(f_past_valid)
+            if($rose(i_spi_cs_n) || $fell(i_spi_cs_n))
+                assume($stable(i_spi_clk) && i_spi_clk);
+
+    // controller behaves by keeping valid line high and not changing data until we are ready
+    always @(posedge i_clock)
+        if(f_past_valid)
+            if($past(i_data_out_valid) && $past(!o_data_out_ready))
+                assume($stable(i_data_out_data) && i_data_out_valid);
+
+    // ensure chip select is held long enough to be effective
+    reg [2:0] chip_select_count = 0;
+    always @($global_clock) 
+        if(i_spi_cs_n == 1 && chip_select_count < 7)
+            chip_select_count <= chip_select_count + 1;
+        else if(i_spi_cs_n == 0)
+            chip_select_count <= 0;
+
+    always @($global_clock)
+        if(f_past_valid)
+            if(chip_select_count < 3)
+                assume(!$fell(i_spi_cs_n));
+
+
+    // ASSERTIONS
+
+
+    // assert everything is zeroed on the reset signal
     always @($global_clock)
         if (f_past_valid)
             if ($past(i_reset) && $rose(i_clock)) begin
@@ -149,10 +247,10 @@ module spi_client (
                 assert(o_data_in_start == 0);
             end
 
-    // spi counters are reset on cs 
+    // spi counters are reset on cs_n
     always @($global_clock)
         if (f_past_valid)
-            if ($past(i_spi_cs) && $stable(i_spi_clk)) begin
+            if ($past(i_spi_cs_n) && $stable(i_spi_clk)) begin
                 assert(in_bit == 0);
                 assert(out_bit == 0);
                 assert(first_byte == 1);
@@ -161,9 +259,9 @@ module spi_client (
     // counters increase
     always @($global_clock) begin
         if (f_past_valid) begin
-            if(!i_spi_cs && $rose(i_spi_clk))
+            if(!i_spi_cs_n && $rose(i_spi_clk))
                 assert(in_bit != $past(in_bit));
-            if(!i_spi_cs && $fell(i_spi_clk))
+            if(!i_spi_cs_n && $fell(i_spi_clk))
                 assert(out_bit != $past(out_bit));
         end
     end
@@ -174,25 +272,17 @@ module spi_client (
         assert(data_in_state < DATA_IN_ENDSTATE);
     end
 
-    // start bit - should be low, go high on first valid byte received, then
-    // go low as second received byte is registered
-    always @(posedge i_clock) begin
-        if(bit_counter > 7 && bit_counter < 16)
-            assert(o_data_in_start);
-    end
+    // CDC ensure data_out doesn't change while it's being copied to data_out_spi
+    always @($global_clock)
+        if(f_past_valid)
+            if(out_bit == 6 || out_bit == 7)
+                assert($stable(data_out));
 
-    // count bits received
-    reg [7:0] bit_counter = 0;
-    always @($global_clock) begin
-        assume(bit_counter < 128);
-        if(i_reset)
-            bit_counter <= 0;
-        if($rose(i_spi_clk))
-            bit_counter <= bit_counter + 1;
-        if($rose(i_spi_cs))
-            bit_counter <= 0;
-    end
+    // CDC: capturing data from mosi and putting into controller's clock domain
+    always @($global_clock) 
+        if(f_past_valid)
+            if($rose(i_clock) && data_in_state == DATA_IN_READY)
+                assert($stable(data_in_spi));
 
-
 `endif
 endmodule

rtl/spi_formal.gtkw

@@ -1,50 +1,54 @@
 [*]
-[*] GTKWave Analyzer v3.3.86 (w)1999-2017 BSI
-[*] Sun Nov 18 20:11:52 2018
+[*] GTKWave Analyzer v3.3.66 (w)1999-2015 BSI
+[*] Mon Nov 19 16:36:01 2018
 [*]
-[dumpfile] "/home/matt/fpga/mlaccel/rtl/spi/engine_0/trace_induct.vcd"
-[dumpfile_mtime] "Sun Nov 18 20:10:39 2018"
-[dumpfile_size] 6172
-[savefile] "/home/matt/fpga/mlaccel/rtl/spi_formal.gtkw"
+[dumpfile] "/home/matt/work/fpga/mlaccel/rtl/spi/engine_0/trace_induct.vcd"
+[dumpfile_mtime] "Mon Nov 19 16:31:51 2018"
+[dumpfile_size] 8257
+[savefile] "/home/matt/work/fpga/mlaccel/rtl/spi_formal.gtkw"
 [timestart] 0
-[size] 1000 600
-[pos] -1 -1
-*-7.258204 190 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
-[sst_width] 223
-[signals_width] 243
+[size] 1774 1134
+[pos] -295 114
+*-6.258204 190 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
+[sst_width] 253
+[signals_width] 519
 [sst_expanded] 1
-[sst_vpaned_height] 152
-@c00022
-spi_client.f_clk_counter[3:0]
-@28
-(0)spi_client.f_clk_counter[3:0]
-(1)spi_client.f_clk_counter[3:0]
-(2)spi_client.f_clk_counter[3:0]
-(3)spi_client.f_clk_counter[3:0]
+[sst_vpaned_height] 332
+@c00200
+-spi_client.f_clk_counter
 @1401200
 -group_end
 @28
 spi_client.i_clock
 spi_client.i_spi_clk
-spi_client.i_spi_cs
+spi_client.i_mosi
 spi_client.i_reset
+spi_client.i_spi_cs_n
+@24
+spi_client.chip_select_count[2:0]
 @200
 -
+@22
+spi_client.i_data_out_data[7:0]
 @28
 spi_client.i_data_out_valid
 @24
 spi_client.out_bit[2:0]
+@22
+spi_client.data_out[7:0]
 @28
 spi_client.data_out_state
 @200
 -
+@23
+spi_client.data_in[7:0]
 @24
 spi_client.in_bit[2:0]
-@29
-spi_client.data_in_state[1:0]
 @28
+spi_client.data_in_state[1:0]
 spi_client.o_data_in_start
-@22
-spi_client.bit_counter[7:0]
+spi_client.i_spi_cs_n
+spi_client.spi_cs_n_clock_pipe
+spi_client.spi_cs_n_clock
 [pattern_trace] 1
 [pattern_trace] 0

rtl/top.v

@@ -81,7 +81,7 @@ module mlaccel_top (
 		.i_reset      (reset     ),
 		.o_active     (spi_active),
 
-		.i_spi_cs   (spi_csb),
+		.i_spi_cs_n (spi_csb),
 		.i_spi_clk  (spi_clk),
 
 		.o_miso   (spi_miso ),