From f2f433b16583e67b6e862f514e5963e5f97e353c Mon Sep 17 00:00:00 2001 From: tmeissner Date: Mon, 8 Jun 2020 13:12:30 +0200 Subject: [PATCH] Use PSL functions instead of workarounds; add forgotten always to asserts in alu --- alu/alu.vhd | 43 +++++++++++++++++-------------------------- counter/counter.vhd | 17 +++-------------- vai_reg/vai_reg.vhd | 33 ++++++++++----------------------- 3 files changed, 30 insertions(+), 63 deletions(-) diff --git a/alu/alu.vhd b/alu/alu.vhd index 7b701b0..52a8a12 100644 --- a/alu/alu.vhd +++ b/alu/alu.vhd @@ -51,8 +51,8 @@ begin when c_sub => v_result := std_logic_vector(unsigned('0' & DinA_i) - unsigned('0' & DinB_i)); - when c_and => v_result := DinA_i and DinB_i; - when c_or => v_result := DinA_i or DinB_i; + when c_and => v_result := ('0', DinA_i and DinB_i); + when c_or => v_result := ('0', DinA_i or DinB_i); when others => null; end case; Dout_o <= v_result(Width-1 downto 0); @@ -63,9 +63,6 @@ begin FormalG : if Formal generate - signal s_dina : std_logic_vector(DinA_i'range); - signal s_dinb : std_logic_vector(DinB_i'range); - function max(a, b: std_logic_vector) return unsigned is begin if unsigned(a) > unsigned(b) then @@ -77,42 +74,36 @@ begin begin - -- VHDL helper logic - process is - begin - wait until rising_edge(Clk_i); - s_dina <= DinA_i; - s_dinb <= DinB_i; - end process; - - default clock is rising_edge(Clk_i); + -- 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'; - ADD_OP : assert Reset_n_i and Opc_i = c_add -> - next unsigned(Dout_o) = unsigned(s_dina) + unsigned(s_dinb) abort not Reset_n_i; + 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; - SUB_OP : assert Reset_n_i and Opc_i = c_sub -> - next unsigned(Dout_o) = unsigned(s_dina) - unsigned(s_dinb) abort not Reset_n_i; + SUB_OP : assert always Reset_n_i and Opc_i = c_sub -> + next unsigned(Dout_o) = unsigned(prev(DinA_i)) - unsigned(prev(DinB_i)) abort not Reset_n_i; - AND_OP : assert Reset_n_i and Opc_i = c_and -> - next Dout_o = (s_dina and s_dinb) abort not Reset_n_i; + AND_OP : assert always Reset_n_i and Opc_i = c_and -> + next Dout_o = (prev(DinA_i) and prev(DinB_i)) abort not Reset_n_i; - OR_OP : assert Reset_n_i and Opc_i = c_or -> - next Dout_o = (s_dina or s_dinb) abort not Reset_n_i; + OR_OP : assert always Reset_n_i and Opc_i = c_or -> + next Dout_o = (prev(DinA_i) or prev(DinB_i)) abort not Reset_n_i; - OVERFLOW_ADD : assert Reset_n_i and Opc_i = c_add and (unsigned(DinA_i) + unsigned(DinB_i)) < max(DinA_i, DinB_i) -> + OVERFLOW_ADD : assert always Reset_n_i and Opc_i = c_add and (unsigned(DinA_i) + unsigned(DinB_i)) < max(DinA_i, DinB_i) -> next OverFlow_o abort not Reset_n_i; - NOT_OVERFLOW_ADD : assert Reset_n_i and Opc_i = c_add and (unsigned(DinA_i) + unsigned(DinB_i)) >= max(DinA_i, DinB_i) -> + NOT_OVERFLOW_ADD : assert always Reset_n_i and Opc_i = c_add and (unsigned(DinA_i) + unsigned(DinB_i)) >= max(DinA_i, DinB_i) -> next not OverFlow_o abort not Reset_n_i; - OVERFLOW_SUB : assert Reset_n_i and Opc_i = c_sub and (unsigned(DinA_i) - unsigned(DinB_i)) > unsigned(DinA_i) -> + OVERFLOW_SUB : assert always Reset_n_i and Opc_i = c_sub and (unsigned(DinA_i) - unsigned(DinB_i)) > unsigned(DinA_i) -> next OverFlow_o abort not Reset_n_i; - NOT_OVERFLOW_SUB : assert Reset_n_i and Opc_i = c_sub and (unsigned(DinA_i) - unsigned(DinB_i)) <= unsigned(DinA_i) -> + NOT_OVERFLOW_SUB : assert always Reset_n_i and Opc_i = c_sub and (unsigned(DinA_i) - unsigned(DinB_i)) <= unsigned(DinA_i) -> next not OverFlow_o abort not Reset_n_i; end generate FormalG; diff --git a/counter/counter.vhd b/counter/counter.vhd index 1f7ef49..9a986e8 100644 --- a/counter/counter.vhd +++ b/counter/counter.vhd @@ -39,30 +39,19 @@ begin FormalG : if Formal generate - signal s_data : unsigned(Data_o'range); - - begin - - -- VHDL helper logic - process is - begin - wait until rising_edge(Clk_i); - s_data <= unsigned(Data_o); - end process; - default clock is rising_edge(Clk_i); -- Initial reset - INITIAL_RESET : restrict {Reset_n_i = '0'[*2]; Reset_n_i = '1'[+]}[*1]; + 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'); COUNT_UP : assert always - Reset_n_i and unsigned(Data_o) < to_unsigned(EndVal, 32) -> next unsigned(Data_o) = s_data + 1; + Reset_n_i and unsigned(Data_o) < to_unsigned(EndVal, 32) -> next unsigned(Data_o) = unsigned(prev(Data_o)) + 1; END_VALUE : assert always - unsigned(Data_o) = to_unsigned(EndVal, 32) -> next unsigned(Data_o) = s_data; + unsigned(Data_o) = to_unsigned(EndVal, 32) -> next Data_o = prev(Data_o); VALID_RANGE : assert always unsigned(Data_o) >= to_unsigned(InitVal, 32) and diff --git a/vai_reg/vai_reg.vhd b/vai_reg/vai_reg.vhd index 1542aea..252539a 100644 --- a/vai_reg/vai_reg.vhd +++ b/vai_reg/vai_reg.vhd @@ -171,17 +171,6 @@ begin 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; - begin @@ -190,8 +179,6 @@ begin 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 @@ -208,26 +195,26 @@ begin -- RESTRICTIONS -- Initial reset - INITIAL_RESET : restrict {Reset_n_i = '0'[*2]; Reset_n_i = '1'[+]}[*1]; + INITIAL_RESET : restrict {not Reset_n_i[*2]; Reset_n_i[+]}[*1]; -- CONSTRAINTS -- Valid stable until accepted JOB_REQ_VALID_STABLE : assume always - DinValid_i and not DinAccept_o -> next (DinValid_i until_ DinAccept_o); + DinValid_i and not DinAccept_o -> next (stable(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); + DinValid_i and not DinAccept_o -> next (stable(DinStart_i) 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); + DinValid_i and not DinAccept_o -> next (stable(DinStop_i) 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); + DinValid_i and not DinAccept_o -> next (stable(Din_i) until_ DinAccept_o); -- ASSERTIONS @@ -315,19 +302,19 @@ begin -- 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); + DoutValid_o and not DoutAccept_i -> next (stable(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); + DoutValid_o and not DoutAccept_i -> next (stable(DoutStart_o) 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); + DoutValid_o and not DoutAccept_i -> next (stable(DoutStop_o) 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); + DoutValid_o and not DoutAccept_i -> next (stable(Dout_o) until_ DoutAccept_i); -- Data from selected address has to be read READ_DATA : assert always @@ -352,7 +339,7 @@ begin 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}; + {s_register(s_addr) = prev(Din_i)}; -- FUNCTIONAL COVERAGE