Replace reset checks by async VHDL asserts; Add assumptions about inputs

alu/alu.vhd

@@ -79,8 +79,14 @@ begin
     -- Initial reset
     INITIAL_RESET : restrict {not Reset_n_i[*2]; Reset_n_i[+]}[*1];
 
-    AFTER_RESET : assert always
-      not Reset_n_i -> Dout_o = (Dout_o'range => '0') and OverFlow_o = '0';
+    -- Asynchronous (unclocked) Reset asserts
+    AFTER_RESET : process (all) is
+    begin
+      if (not Reset_n_i) then
+        RESET_DOUT : assert Dout_o = (Dout_o'range => '0');
+        RESET_OVFL : assert OverFlow_o = '0';
+      end if;
+    end process AFTER_RESET;
 
     ADD_OP : assert always Reset_n_i and Opc_i = c_add ->
       next unsigned(Dout_o) = unsigned(prev(DinA_i)) + unsigned(prev(DinB_i)) abort not Reset_n_i;

counter/counter.vhd

@@ -44,18 +44,27 @@ begin
     -- Initial reset
     INITIAL_RESET : restrict {not Reset_n_i[*2]; Reset_n_i[+]}[*1];
 
-    AFTER_RESET : assert always
-      not Reset_n_i -> Data_o = (Data_o'range => '0');
+    -- Asynchronous (unclocked) Reset asserts
+    AFTER_RESET : process (all) is
+    begin
+      if (not Reset_n_i) then
+        RESET_DATA : assert unsigned(Data_o) = to_unsigned(InitVal, Data_o'length);
+      end if;
+    end process AFTER_RESET;
 
     COUNT_UP : assert always
-      Reset_n_i and unsigned(Data_o) < to_unsigned(EndVal, 32) -> next unsigned(Data_o) = unsigned(prev(Data_o)) + 1;
+      Reset_n_i and unsigned(Data_o) < to_unsigned(EndVal, Data_o'length)
+      ->
+      next unsigned(Data_o) = unsigned(prev(Data_o)) + 1;
 
     END_VALUE : assert always
-      unsigned(Data_o) = to_unsigned(EndVal, 32) -> next Data_o = prev(Data_o);
+      unsigned(Data_o) = to_unsigned(EndVal, Data_o'length)
+      ->
+      next Data_o = prev(Data_o);
 
     VALID_RANGE : assert always
-      unsigned(Data_o) >= to_unsigned(InitVal, 32) and
-      unsigned(Data_o) <= to_unsigned(EndVal, 32);
+      unsigned(Data_o) >= to_unsigned(InitVal, Data_o'length) and
+      unsigned(Data_o) <= to_unsigned(EndVal, Data_o'length);
 
   end generate FormalG;
 

counter/symbiyosys.sby

@@ -15,7 +15,7 @@ bmc: smtbmc z3
 prove: smtbmc z3
 
 [script]
-ghdl --std=08 -fpsl counter.vhd -e counter
+ghdl --std=08 -gInitVal=23 -gEndVal=42 -fpsl counter.vhd -e counter
 prep -auto-top
 
 [files]

vai_reg/vai_reg.psl

@@ -0,0 +1,195 @@
+vunit formal (vai_reg(rtl)) {
+
+
+    signal s_addr : natural range 0 to 15;
+
+    type t_cmd is (READ, WRITE, NOP);
+    signal s_cmd : t_cmd;
+
+    type t_vai is record
+      Start  : std_logic;
+      Stop   : std_logic;
+      Data   : std_logic_vector(7 downto 0);
+      Valid  : std_logic;
+      Accept : std_logic;
+    end record t_vai;
+
+    signal s_job_req : t_vai;
+    signal s_job_ack : t_vai;
+
+
+    -- VHDL helper logic
+    process is
+    begin
+      wait until rising_edge(Clk_i);
+      s_job_req <= (DinStart_i, DinStop_i, Din_i, DinValid_i, DinAccept_o);
+      s_job_ack <= (DoutStart_o, DoutStop_o, Dout_o, DoutValid_o, DoutAccept_i);
+      if (s_fsm_state = GET_HEADER) then
+        if (DinValid_i = '1' and DinStart_i = '1') then
+          s_cmd  <= READ  when Din_i(3 downto 0) = x"0" else
+                    WRITE when Din_i(3 downto 0) = x"1" else
+                    NOP;
+          s_addr <= to_integer(unsigned(Din_i(7 downto 4)));
+        end if;
+      end if;
+    end process;
+
+
+    default clock is rising_edge(Clk_i);
+
+    -- RESTRICTIONS
+
+    -- Initial reset
+    INITIAL_RESET : restrict {Reset_n_i = '0'[*2]; Reset_n_i = '1'[+]}[*1];
+
+
+    -- CONSTRAINTS
+
+    -- Valid stable until accepted
+    JOB_REQ_VALID_STABLE : assume always
+      DinValid_i and not DinAccept_o -> next (DinValid_i until_ DinAccept_o);
+
+    -- Start stable until accepted
+    JOB_REQ_START_STABLE : assume always
+      DinValid_i and not DinAccept_o -> next (DinStart_i = s_job_req.Start until_ DinAccept_o);
+
+    -- Stop stable until accepted
+    JOB_REQ_STOP_STABLE : assume always
+      DinValid_i and not DinAccept_o -> next (DinStop_i = s_job_req.Stop until_ DinAccept_o);
+
+    -- Data stable until accepted
+    JOB_REQ_DIN_STABLE : assume always
+      DinValid_i and not DinAccept_o -> next (Din_i = s_job_req.Data until_ DinAccept_o);
+
+
+    -- ASSERTIONS
+
+    -- Reset values
+    AFTER_RESET : assert always
+      not Reset_n_i
+      ->
+      s_fsm_state = IDLE and
+      not DinAccept_o and
+      not DoutStart_o and
+      not DoutStop_o  and
+      not DoutValid_o and
+      s_register = (0 to 7 => x"00");
+
+    -- FSM states in valid range
+    FSM_STATES_VALID : assert always
+      s_fsm_state = IDLE or s_fsm_state = GET_HEADER or
+      s_fsm_state = GET_DATA or s_fsm_state = SET_DATA or
+      s_fsm_state = SEND_HEADER or s_fsm_state = SEND_DATA or
+      s_fsm_state = SEND_FOOTER;
+
+    -- Discard jobs with invalid command
+    INV_CMD_DISCARD : assert always
+      s_fsm_state = GET_HEADER and DinValid_i = '1' and DinStart_i = '1' and
+      Din_i(3 downto 0) /= x"0" and Din_i(3 downto 0) /= x"1"
+      ->
+      next s_fsm_state = IDLE;
+
+    -- Discard read job with invalid stop flags
+    READ_INV_FLAGS_DISCARD : assert always
+      s_fsm_state = GET_HEADER and DinValid_i = '1' and DinStart_i = '1' and
+      Din_i(3 downto 0) = x"0" and DinStop_i = '0'
+      ->
+      next s_fsm_state = IDLE;
+
+    -- Discard write job with invalid stop flags
+    WRITE_INV_FLAGS_DISCARD : assert always
+      s_fsm_state = GET_HEADER and DinValid_i = '1' and DinStart_i = '1' and
+      Din_i(3 downto 0) = x"1" and DinStop_i = '1'
+      ->
+      next s_fsm_state = IDLE;
+
+    -- After a valid job read request,
+    -- a job read acknowledge has to follow
+    READ_VALID_ACK : assert always
+      {s_fsm_state = GET_HEADER and DinValid_i = '1' and DinStart_i = '1' and
+       Din_i(3 downto 0) = x"0" and DinStop_i = '1'}
+      |=>
+      {-- Job ack header cycle
+       not DoutValid_o [*];
+       DoutValid_o and DoutStart_o and not DoutAccept_i [*];
+       DoutValid_o and DoutStart_o and DoutAccept_i;
+       -- Job ack data cycle
+       not DoutValid_o [*];
+       DoutValid_o and not DoutStart_o and not DoutStop_o and not DoutAccept_i [*];
+       DoutValid_o and not DoutStart_o and not DoutStop_o and DoutAccept_i;
+       -- Job ack footer cycle
+       not DoutValid_o [*];
+       DoutValid_o and DoutStop_o};
+
+    -- After a valid job write request,
+    -- a job read acknowledge has to follow
+    WRITE_VALID_ACK : assert always
+      {s_fsm_state = GET_HEADER and DinValid_i = '1' and DinStart_i = '1' and
+       Din_i(3 downto 0) = x"1" and DinStop_i = '0';
+       not DinValid_i [*];
+       DinValid_i and DinStop_i}
+      |=>
+      {-- Job ack header cycle
+       not DoutValid_o [*];
+       DoutValid_o and DoutStart_o and not DoutAccept_i [*];
+       DoutValid_o and DoutStart_o and DoutAccept_i;
+       -- Job ack footer cycle
+       not DoutValid_o [*];
+       DoutValid_o and DoutStop_o};
+
+     -- Start & stop flag have to be exclusive
+     JOB_ACK_NEVER_START_STOP : assert never
+       DoutStart_o and DoutStop_o;
+
+     -- Start & Stop have to be active together with valid
+     JOB_ACK_START_STOP_VALID : assert always
+       DoutStart_o or DoutStop_o -> DoutValid_o;
+
+     -- Valid has to be stable until accepted
+     JOB_ACK_VALID_STABLE : assert always
+       DoutValid_o and not DoutAccept_i -> next (DoutValid_o until_ DoutAccept_i);
+
+     -- Start has to be stable until accepted
+     JOB_ACK_START_STABLE : assert always
+       DoutValid_o and not DoutAccept_i -> next (DoutStart_o = s_job_ack.Start until_ DoutAccept_i);
+
+     -- Stop has to be stable until accepted
+     JOB_ACK_STOP_STABLE : assert always
+       DoutValid_o and not DoutAccept_i -> next (DoutStop_o = s_job_ack.Stop until_ DoutAccept_i);
+
+     -- Data has to be stable until accepted
+     JOB_ACK_DOUT_STABLE : assert always
+       DoutValid_o and not DoutAccept_i -> next (Dout_o = s_job_ack.Data until_ DoutAccept_i);
+
+    -- Data from selected address has to be read
+    READ_DATA : assert always
+      DoutValid_o and not DoutStart_o and not DoutStop_o and s_addr <= 7
+      ->
+      Dout_o = s_register(s_addr);
+
+    -- 0 has to be read when invalid address is given
+    READ_DATA_INV_ADDR : assert always
+      DoutValid_o and not DoutStart_o and not DoutStop_o and s_addr > 7
+      ->
+      Dout_o = x"00";
+
+    -- Register has to be written at given address with given data
+    -- when correct job req write occurs
+    WRITE_DATA : assert always
+      -- Job req header cycle
+      {s_fsm_state = GET_HEADER and DinValid_i = '1' and DinStart_i = '1' and
+       Din_i(3 downto 0) = x"1" and unsigned(Din_i(7 downto 4)) <= 7 and DinStop_i = '0';
+       -- Job req data / footer cycle
+       not DinValid_i [*];
+       DinValid_i and not DinStart_i and DinStop_i and not DinAccept_o [*];
+       DinValid_i and not DinStart_i and DinStop_i and DinAccept_o}
+      |=>
+      {s_register(s_addr) = s_job_req.Data};
+
+
+    -- FUNCTIONAL COVERAGE
+
+    FOOTER_VALID : cover {DoutValid_o = '1' and DoutStop_o = '1' and Dout_o = 8x"0"};
+    FOOTER_ERR   : cover {DoutValid_o = '1' and DoutStop_o = '1' and Dout_o = 8x"1"};
+
+}

vai_reg/vai_reg.vhd

@@ -200,6 +200,14 @@ begin
 
     -- CONSTRAINTS
 
+    -- Inputs are low during reset for simplicity
+    ASSUME_INPUTS_DURING_RESET : assume always
+      not Reset_n_i ->
+      not DinValid_i and
+      not DinStart_i and
+      not DinStop_i  and
+      not DoutAccept_i;
+
     -- Valid stable until accepted
     JOB_REQ_VALID_STABLE : assume always
       DinValid_i and not DinAccept_o -> next (stable(DinValid_i) until_ DinAccept_o);
@@ -219,16 +227,18 @@ begin
 
     -- ASSERTIONS
 
-    -- Reset values
-    AFTER_RESET : assert always
-      not Reset_n_i
-      ->
-      s_fsm_state = IDLE and
-      not DinAccept_o and
-      not DoutStart_o and
-      not DoutStop_o  and
-      not DoutValid_o and
-      s_register = (0 to 7 => x"00");
+    -- Asynchronous (unclocked) Reset asserts
+    AFTER_RESET : process (all) is
+    begin
+      if (not Reset_n_i) then
+        RESET_STATE  : assert s_fsm_state = IDLE;
+        RESET_ACCEPT : assert DinAccept_o = '0';
+        RESET_START  : assert DoutStart_o = '0';
+        RESET_STOP   : assert DoutStop_o = '0';
+        RESET_VALID  : assert DoutValid_o = '0';
+        RESET_REG    : assert s_register = (0 to 7 => x"00");
+      end if;
+    end process AFTER_RESET;
 
     -- FSM states in valid range
     FSM_STATES_VALID : assert always