tmeissner
/
formal_hw_verification
1
0
Fork 0
Code Issues 0 Pull Requests 0 Releases 6 Wiki Activity
Browse Source

Use PSL functions instead of workarounds; add forgotten always to asserts in alu

master
T. Meissner 4 years ago
parent
3da2f2df9e
commit
f2f433b165
3 changed files with 30 additions and 63 deletions
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. +17
    -26
      alu/alu.vhd
  2. +3
    -14
      counter/counter.vhd
  3. +10
    -23
      vai_reg/vai_reg.vhd

+ 17
- 26
alu/alu.vhd View File

@ -51,8 +51,8 @@ begin
when c_sub => when c_sub =>
v_result := std_logic_vector(unsigned('0' & DinA_i) - v_result := std_logic_vector(unsigned('0' & DinA_i) -
unsigned('0' & DinB_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; when others => null;
end case; end case;
Dout_o <= v_result(Width-1 downto 0); Dout_o <= v_result(Width-1 downto 0);
@ -63,9 +63,6 @@ begin
FormalG : if Formal generate 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 function max(a, b: std_logic_vector) return unsigned is
begin begin
if unsigned(a) > unsigned(b) then if unsigned(a) > unsigned(b) then
@ -77,42 +74,36 @@ begin
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); 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 AFTER_RESET : assert always
not Reset_n_i -> Dout_o = (Dout_o'range => '0') and OverFlow_o = '0'; 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; 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; 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; 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; next not OverFlow_o abort not Reset_n_i;
end generate FormalG; end generate FormalG;


+ 3
- 14
counter/counter.vhd View File

@ -39,30 +39,19 @@ begin
FormalG : if Formal generate 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); default clock is rising_edge(Clk_i);
-- Initial reset -- 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 AFTER_RESET : assert always
not Reset_n_i -> Data_o = (Data_o'range => '0'); not Reset_n_i -> Data_o = (Data_o'range => '0');
COUNT_UP : assert always 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 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 VALID_RANGE : assert always
unsigned(Data_o) >= to_unsigned(InitVal, 32) and unsigned(Data_o) >= to_unsigned(InitVal, 32) and


+ 10
- 23
vai_reg/vai_reg.vhd View File

@ -171,17 +171,6 @@ begin
type t_cmd is (READ, WRITE, NOP); type t_cmd is (READ, WRITE, NOP);
signal s_cmd : t_cmd; 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 begin
@ -190,8 +179,6 @@ begin
process is process is
begin begin
wait until rising_edge(Clk_i); 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 (s_fsm_state = GET_HEADER) then
if (DinValid_i = '1' and DinStart_i = '1') then if (DinValid_i = '1' and DinStart_i = '1') then
s_cmd <= READ when Din_i(3 downto 0) = x"0" else s_cmd <= READ when Din_i(3 downto 0) = x"0" else
@ -208,26 +195,26 @@ begin
-- RESTRICTIONS -- RESTRICTIONS
-- Initial reset -- 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 -- CONSTRAINTS
-- Valid stable until accepted -- Valid stable until accepted
JOB_REQ_VALID_STABLE : assume always 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 -- Start stable until accepted
JOB_REQ_START_STABLE : assume always 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 -- Stop stable until accepted
JOB_REQ_STOP_STABLE : assume always 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 -- Data stable until accepted
JOB_REQ_DIN_STABLE : assume always 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 -- ASSERTIONS
@ -315,19 +302,19 @@ begin
-- Valid has to be stable until accepted -- Valid has to be stable until accepted
JOB_ACK_VALID_STABLE : assert always 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 -- Start has to be stable until accepted
JOB_ACK_START_STABLE : assert always 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 -- Stop has to be stable until accepted
JOB_ACK_STOP_STABLE : assert always 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 -- Data has to be stable until accepted
JOB_ACK_DOUT_STABLE : assert always 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 -- Data from selected address has to be read
READ_DATA : assert always 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 not DinAccept_o [*];
DinValid_i and not DinStart_i and DinStop_i and 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 -- FUNCTIONAL COVERAGE


Write Preview
Loading…
Cancel
Save