formal

rtl/spi.sby

@@ -0,0 +1,14 @@
+[options]
+mode prove
+multiclock on
+depth 20
+
+[engines]
+smtbmc 
+
+[script]
+read_verilog -formal spi_client.v
+prep -top spi_client
+
+[files]
+spi_client.v

rtl/spi_client.v

@@ -34,12 +34,13 @@ module spi_client (
     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
             in_bit <= 0;
             first_byte <= 1;
         end else begin                      // receiving data
-            data_in[7-in_bit] <= i_mosi;
+            data_in[3'd7-in_bit] <= i_mosi;
             in_bit <= in_bit + 1;
             if(in_bit == 7)
                 first_byte <= 0;
@@ -50,7 +51,7 @@ module spi_client (
         if(i_spi_cs) begin                  // reset state
             out_bit <= 0;
         end else begin
-            o_miso <= data_out[7-out_bit];
+            o_miso <= data_out[3'd7-out_bit];
             out_bit <= out_bit + 1;
         end
     end
@@ -68,47 +69,130 @@ module spi_client (
 
     always @(posedge i_clock) begin
         if(i_reset) begin
-            data_in_state = DATA_IN_WAIT;
-            data_out_state = DATA_OUT_WAIT;
+            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
+        else begin
+
+            case(data_in_state)
+                DATA_IN_WAIT: begin
+                    start_status <= first_byte;
+                    o_data_in_valid <= 0;
+                    if(in_bit == 1)
+                        data_in_state <= DATA_IN_RX;
+                end
+                DATA_IN_RX: begin
+                    if(in_bit == 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;
+                    data_in_state <= DATA_IN_WAIT;
+                end
+            endcase
+
+            case(data_out_state)
+                DATA_OUT_WAIT: begin
+                    if(out_bit == 0)
+                        if(i_data_out_valid) begin
+                            data_out <= i_data_out_data;
+                            o_data_out_ready <= 1;
+                            data_out_state <= DATA_OUT_TX;
+                        end
+                end
+                DATA_OUT_TX: begin
+                    o_data_out_ready <= 0;
+                    if(out_bit == 7)
+                        data_out_state <= DATA_OUT_WAIT;
+                end
+
+            endcase
+        end
+    end
 
-        case(data_in_state)
-            DATA_IN_WAIT: begin
-                start_status <= first_byte;
-                o_data_in_valid <= 0;
-                if(in_bit == 1)
-                    data_in_state <= DATA_IN_RX;
-            end
-            DATA_IN_RX: begin
-                if(in_bit == 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;
-                data_in_state <= DATA_IN_WAIT;
-            end
-        endcase
-
-        case(data_out_state)
-            DATA_OUT_WAIT: begin
-                if(out_bit == 0)
-                    if(i_data_out_valid) begin
-                        data_out <= i_data_out_data;
-                        o_data_out_ready <= 1;
-                        data_out_state <= DATA_OUT_TX;
-                    end
+`ifdef FORMAL
+    reg [3:0] f_clk_counter;
+    initial f_clk_counter = 0;
+
+    initial restrict(i_reset);
+    initial restrict(i_spi_cs);
+
+    // past valid signal
+    reg f_past_valid = 0;
+    always @($global_clock)
+        f_past_valid <= 1'b1;
+
+    // stop reset from happening after start
+    always @($global_clock)
+        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]);
+    end
+
+    // check everything is zeroed on the reset signal
+    always @($global_clock)
+        if (f_past_valid)
+            if ($past(i_reset) && $rose(i_clock)) begin
+                assert(data_out_state == DATA_OUT_WAIT);
+                assert(data_in_state == DATA_IN_WAIT);
+                assert(o_data_in_start == 0);
             end
-            DATA_OUT_TX: begin
-                o_data_out_ready <= 0;
-                if(out_bit == 7)
-                    data_out_state <= DATA_OUT_WAIT;
+
+    // spi counters are reset on cs 
+    always @($global_clock)
+        if (f_past_valid)
+            if ($past(i_spi_cs) && $stable(i_spi_clk)) begin
+                assert(in_bit == 0);
+                assert(out_bit == 0);
+                assert(first_byte == 1);
             end
 
-        endcase
+    // counters increase
+    always @($global_clock) begin
+        if (f_past_valid) begin
+            if(!i_spi_cs && $rose(i_spi_clk))
+                assert(in_bit != $past(in_bit));
+            if(!i_spi_cs && $fell(i_spi_clk))
+                assert(out_bit != $past(out_bit));
+        end
+    end
+
+    // state machines: so simple just make sure they stay bounded
+    always @($global_clock) begin
+        assert(data_out_state < DATA_OUT_ENDSTATE);
+        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
+
+    // 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
+
+
+`endif
 endmodule

rtl/spi_formal.gtkw

@@ -0,0 +1,50 @@
+[*]
+[*] GTKWave Analyzer v3.3.86 (w)1999-2017 BSI
+[*] Sun Nov 18 20:11:52 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"
+[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
+[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]
+@1401200
+-group_end
+@28
+spi_client.i_clock
+spi_client.i_spi_clk
+spi_client.i_spi_cs
+spi_client.i_reset
+@200
+-
+@28
+spi_client.i_data_out_valid
+@24
+spi_client.out_bit[2:0]
+@28
+spi_client.data_out_state
+@200
+-
+@24
+spi_client.in_bit[2:0]
+@29
+spi_client.data_in_state[1:0]
+@28
+spi_client.o_data_in_start
+@22
+spi_client.bit_counter[7:0]
+[pattern_trace] 1
+[pattern_trace] 0