From 3d57fff226eed011ed526b19576bf1545ea14f4b Mon Sep 17 00:00:00 2001 From: tmeissner Date: Tue, 16 Feb 2021 23:16:43 +0100 Subject: [PATCH] Replace reset checks by async VHDL asserts; Add assumptions about inputs --- alu/alu.vhd | 10 ++- counter/counter.vhd | 21 +++-- counter/symbiyosys.sby | 2 +- vai_reg/vai_reg.psl | 195 +++++++++++++++++++++++++++++++++++++++++ vai_reg/vai_reg.vhd | 30 ++++--- 5 files changed, 239 insertions(+), 19 deletions(-) create mode 100644 vai_reg/vai_reg.psl diff --git a/alu/alu.vhd b/alu/alu.vhd index 52a8a12..b9bacb2 100644 --- a/alu/alu.vhd +++ b/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; diff --git a/counter/counter.vhd b/counter/counter.vhd index 9a986e8..cc3e89c 100644 --- a/counter/counter.vhd +++ b/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; diff --git a/counter/symbiyosys.sby b/counter/symbiyosys.sby index b05f40b..bf49a6e 100644 --- a/counter/symbiyosys.sby +++ b/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] diff --git a/vai_reg/vai_reg.psl b/vai_reg/vai_reg.psl new file mode 100644 index 0000000..fbde0cf --- /dev/null +++ b/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"}; + +} diff --git a/vai_reg/vai_reg.vhd b/vai_reg/vai_reg.vhd index 252539a..f256fb1 100644 --- a/vai_reg/vai_reg.vhd +++ b/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