Add simple VAI register file as base to try to formal verify FSM designs

vai_reg/Makefile

@@ -0,0 +1,6 @@
+vai_reg: vai_reg.vhd properties.sv symbiyosys.sby
+	sby -f -d work symbiyosys.sby
+
+
+clean:
+	rm -rf work

vai_reg/properties.sv

@@ -0,0 +1,167 @@
+module properties (
+    input       Reset_n_i,
+    input       Clk_i,
+    input [7:0] Din_i,
+    input       DinValid_i,
+    input       DinStart_i,
+    input       DinStop_i,
+    input       DinAccept_o,
+    input [7:0] Dout_o,
+    input       DoutValid_o,
+    input       DoutStart_o,
+    input       DoutStop_o,
+    input       DoutAccept_i,
+    // Internals
+    input [2:0] s_fsm_state,
+    input [7:0] s_header
+);
+
+
+
+  `define READ 0
+  `define WRITE 1
+
+
+  reg init_state = 1;
+
+  // Initial reset
+  always @(*) begin
+    if (init_state) assume (!Reset_n_i);
+    if (!init_state) assume (Reset_n_i);
+  end
+
+  always @(posedge Clk_i)
+    init_state = 0;
+
+
+  // Constraints
+
+  assume property (@(posedge Clk_i)
+    DinValid_i && !DinAccept_o |=>
+    $stable(Din_i)
+  );
+
+  assume property (@(posedge Clk_i)
+    DinValid_i && !DinAccept_o |=>
+    $stable(DinStart_i)
+  );
+
+  assume property (@(posedge Clk_i)
+    DinValid_i && !DinAccept_o |=>
+    $stable(DinStop_i)
+  );
+
+
+  // Asserts
+
+  assert property (@(posedge Clk_i)
+    s_fsm_state >= 0 && s_fsm_state <= 6
+  );
+
+  assert property (@(posedge Clk_i)
+    DoutStart_o |->
+    DoutValid_o
+  );
+
+  assert property (@(posedge Clk_i)
+    DoutStart_o && DoutAccept_i |=>
+    !DoutStart_o
+  );
+
+  assert property (@(posedge Clk_i)
+    DoutStop_o |->
+    DoutValid_o
+  );
+
+  assert property (@(posedge Clk_i)
+    DoutStop_o && DoutAccept_i |=>
+    !DoutStop_o
+  );
+
+  assert property (@(posedge Clk_i)
+    s_fsm_state == 1 && DinValid_i && DinStart_i && DinAccept_o |=>
+    s_header == $past(Din_i)
+  );
+
+
+  // State changes
+
+  assert property (@(posedge Clk_i) disable iff (!Reset_n_i)
+    s_fsm_state == 0 |=> s_fsm_state == 1
+  );
+
+  assert property (@(posedge Clk_i) disable iff (!Reset_n_i)
+    s_fsm_state == 1 && DinValid_i && DinStart_i && DinStop_i && Din_i[3:0] == `READ |=>
+    s_fsm_state == 2
+  );
+
+  assert property (@(posedge Clk_i) disable iff (!Reset_n_i)
+    s_fsm_state == 1 && DinValid_i && DinStart_i && !DinStop_i && Din_i[3:0] == `WRITE |=>
+    s_fsm_state == 3
+  );
+
+  assert property (@(posedge Clk_i) disable iff (!Reset_n_i)
+    s_fsm_state == 2 |=> s_fsm_state == 4
+  );
+
+  assert property (@(posedge Clk_i) disable iff (!Reset_n_i)
+    s_fsm_state == 4 && DoutValid_o && DoutAccept_i && s_header[3:0] == `READ |=> s_fsm_state == 5
+  );
+
+  assert property (@(posedge Clk_i) disable iff (!Reset_n_i)
+    s_fsm_state == 4 && DoutValid_o && DoutAccept_i && s_header[3:0] != `READ |=> s_fsm_state == 6
+  );
+
+  assert property (@(posedge Clk_i) disable iff (!Reset_n_i)
+    s_fsm_state == 6 && DoutValid_o && DoutAccept_i |=> s_fsm_state == 0
+  );
+
+
+  // Protocol checks
+
+  assert property (@(posedge Clk_i)
+    s_fsm_state > 1 |->
+    s_header[3:0] == `READ || s_header[3:0] == `WRITE
+  );
+
+  assert property (@(posedge Clk_i)
+    DoutStart_o && DoutValid_o |->
+    Dout_o[3:0] == s_header[3:0]
+  );
+
+  assert property (@(posedge Clk_i)
+    DoutValid_o && !DoutAccept_i |=>
+    $stable(Dout_o)
+  );
+
+  assert property (@(posedge Clk_i)
+    DoutValid_o && !DoutAccept_i |=>
+    $stable(DoutStart_o)
+  );
+
+  assert property (@(posedge Clk_i)
+    DoutValid_o && !DoutAccept_i |=>
+    $stable(DoutStop_o)
+  );
+
+  assert property (@(posedge Clk_i)
+    DoutValid_o |-> !(DoutStart_o && DoutStop_o)
+  );
+
+  assert property (@(posedge Clk_i)
+    DoutStart_o |-> s_fsm_state == 4
+  );
+
+  assert property (@(posedge Clk_i)
+    DoutStop_o |-> s_fsm_state == 6
+  );
+
+  assert property (@(posedge Clk_i)
+    DoutValid_o |-> s_fsm_state >= 4 && s_fsm_state <= 6
+  );
+
+
+endmodule
+
+
+bind vai_reg properties properties (.*);

vai_reg/symbiyosys.sby

@@ -0,0 +1,19 @@
+[options]
+depth 30
+wait on
+mode prove
+#mode bmc
+
+[engines]
+smtbmc
+#abc pdr
+
+[script]
+verific -vhdl vai_reg.vhd
+verific -formal properties.sv
+verific -import -extnets -all vai_reg
+prep -top vai_reg
+
+[files]
+vai_reg.vhd
+properties.sv

vai_reg/vai_reg.vhd

@@ -0,0 +1,163 @@
+library ieee;
+use ieee.std_logic_1164.all;
+use ieee.numeric_std.all;
+
+
+
+entity vai_reg is
+  port (
+    Reset_n_i    : in  std_logic;
+    Clk_i        : in  std_logic;
+    -- req
+    Din_i        : in  std_logic_vector(7 downto 0);
+    DinValid_i   : in  std_logic;
+    DinStart_i   : in  std_logic;
+    DinStop_i    : in  std_logic;
+    DinAccept_o  : out std_logic;
+    -- ack
+    Dout_o       : out std_logic_vector(7 downto 0);
+    DoutValid_o  : out std_logic;
+    DoutStart_o  : out std_logic;
+    DoutStop_o   : out std_logic;
+    DoutAccept_i : in  std_logic
+  );
+end entity vai_reg;
+
+
+
+architecture rtl of vai_reg is
+
+
+  constant C_READ  : std_logic_vector(3 downto 0) := x"0";
+  constant C_WRITE : std_logic_vector(3 downto 0) := x"1";
+
+  type t_fsm_state is (IDLE, GET_HEADER, GET_DATA,
+                       SET_DATA, SEND_HEADER, SEND_DATA, SEND_FOOTER);
+  signal s_fsm_state : t_fsm_state;
+
+  type t_register is array(0 to 7) of std_logic_vector(7 downto 0);
+  signal s_register : t_register;
+
+  signal s_header : std_logic_vector(7 downto 0);
+  signal s_data   : std_logic_vector(7 downto 0);
+
+  signal s_error : boolean;
+
+  alias a_addr : std_logic_vector(3 downto 0) is s_header(7 downto 4);
+
+
+begin
+
+
+  process (Reset_n_i, Clk_i) is
+  begin
+    if (Reset_n_i = '0') then
+      DinAccept_o <= '0';
+      DoutStart_o <= '0';
+      DoutStop_o  <= '0';
+      DoutValid_o <= '0';
+      Dout_o      <= (others => '0');
+      s_header    <= (others => '0');
+      s_data      <= (others => '0');
+      s_register  <= (others => (others => '0'));
+      s_error     <= false;
+      s_fsm_state <= IDLE;
+    elsif (rising_edge(Clk_i)) then
+      case s_fsm_state is
+
+        when IDLE =>
+          DinAccept_o <= '0';
+          DoutStart_o <= '0';
+          DoutStop_o  <= '0';
+          DoutValid_o <= '0';
+          Dout_o      <= (others => '0');
+          s_header    <= (others => '0');
+          s_data      <= (others => '0');
+          s_error     <= false;
+          s_fsm_state <= GET_HEADER;
+
+        when GET_HEADER =>
+          DinAccept_o <= '1';
+          if (DinValid_i = '1' and DinStart_i = '1') then
+            DinAccept_o <= '0';
+            s_header    <= Din_i;
+            if (Din_i(3 downto 0) = C_READ and DinStop_i = '1') then
+              s_fsm_state <= GET_DATA;
+            elsif (Din_i(3 downto 0) = C_WRITE and DinStop_i = '0') then
+              s_fsm_state <= SET_DATA;
+            else
+              s_fsm_state <= IDLE;
+            end if;
+          end if;
+
+        when GET_DATA =>
+          if (unsigned(a_addr) <= 7) then
+            s_data <= s_register(to_integer(unsigned(a_addr)));
+          else
+            s_error <= true;
+            s_data  <= (others => '0');
+          end if;
+          s_fsm_state <= SEND_HEADER;
+
+        when SET_DATA =>
+          DinAccept_o <= '1';
+          if (DinValid_i = '1') then
+            DinAccept_o <= '0';
+            if (DinStop_i = '1') then
+              if (unsigned(a_addr) <= 7) then
+                -- Following line results in a Segmentation Fault
+                s_register(to_integer(unsigned(a_addr))) <= Din_i;
+                -- Following line results in following error:
+                -- ERROR: Unsupported cell type $dlatchsr for cell $verific$wide_dlatchrs_8.$verific$i1$172.
+                s_register(0) <= Din_i;
+              else
+                s_error <= true;
+              end if;
+              s_fsm_state <= SEND_HEADER;
+            else
+              s_fsm_state <= IDLE;
+            end if;
+          end if;
+
+        when SEND_HEADER =>
+          DoutValid_o <= '1';
+          DoutStart_o <= '1';
+          Dout_o      <= s_header;
+          if (DoutAccept_i = '1') then
+            DoutValid_o <= '0';
+            DoutStart_o <= '0';
+            if (s_header(3 downto 0) = C_WRITE) then
+              s_fsm_state <= SEND_FOOTER;
+            else
+              s_fsm_state <= SEND_DATA;
+            end if;
+          end if;
+
+        when SEND_DATA =>
+          DoutValid_o <= '1';
+          Dout_o      <= s_data;
+          if (DoutAccept_i = '1') then
+            DoutValid_o <= '0';
+            s_fsm_state <= SEND_FOOTER;
+          end if;
+
+        when SEND_FOOTER =>
+          DoutValid_o <= '1';
+          DoutStop_o  <= '1';
+          Dout_o      <= x"01" when s_error else x"00";
+          if (DoutAccept_i = '1') then
+            Dout_o      <= (others => '0');
+            DoutValid_o <= '0';
+            DoutStop_o  <= '0';
+            s_fsm_state <= IDLE;
+          end if;
+
+        when others => null;
+
+      end case;
+    end if;
+  end process;
+
+
+end architecture rtl;
+