From 8edb03c011ccb700a35de82db3d2d3b0a5300155 Mon Sep 17 00:00:00 2001 From: tmeissner Date: Wed, 2 Jan 2019 11:30:03 +0100 Subject: [PATCH] Add a bunch of new properties; name all assert directives --- vai_reg/properties.sv | 151 +++++++++++++++++++++++++++++++----------- 1 file changed, 114 insertions(+), 37 deletions(-) diff --git a/vai_reg/properties.sv b/vai_reg/properties.sv index 10853fd..723fc20 100644 --- a/vai_reg/properties.sv +++ b/vai_reg/properties.sv @@ -14,6 +14,7 @@ module properties ( // Internals input [2:0] s_fsm_state, input [7:0] s_header, + input [7:0] s_data, input s_error, input [7:0] s_register [0:7] ); @@ -69,31 +70,31 @@ module properties ( // Asserts - assert property ( + fsm_state_valid_a : assert property ( s_fsm_state >= 0 && s_fsm_state <= 6 ); - assert property ( + valid_when_start_a : assert property ( DoutStart_o |-> DoutValid_o ); - assert property ( + start_off_when_acked_a : assert property ( DoutStart_o && DoutAccept_i |=> !DoutStart_o ); - assert property ( + valid_when_stop_a : assert property ( DoutStop_o |-> DoutValid_o ); - assert property ( + stop_off_when_acked_a : assert property ( DoutStop_o && DoutAccept_i |=> !DoutStop_o ); - assert property ( + store_header_a : assert property ( s_fsm_state == 1 && DinValid_i && DinStart_i && DinAccept_o |=> s_header == $past(Din_i) ); @@ -101,109 +102,136 @@ module properties ( // State changes - assert property ( + // IDLE -> GET_HEADER + fsm_idle_to_get_header_a : assert property ( s_fsm_state == 0 |=> s_fsm_state == 1 ); - assert property ( + // GET_HEADER -> GET_DATA + fsm_get_header_to_get_data_a : assert property ( s_fsm_state == 1 && DinValid_i && DinStart_i && DinStop_i && Din_i[3:0] == `READ |=> s_fsm_state == 2 ); - assert property ( + // GET_HEADER -> SET_DATA + fsm_get_header_to_set_data_a : assert property ( s_fsm_state == 1 && DinValid_i && DinStart_i && !DinStop_i && Din_i[3:0] == `WRITE |=> s_fsm_state == 3 ); - assert property ( + // GET_DATA -> SEND_HEADER + fsm_get_data_to_send_header_a : assert property ( s_fsm_state == 2 |=> s_fsm_state == 4 ); - assert property ( + // SET_DATA -> IDLE + fsm_set_data_to_idle_a : assert property ( + s_fsm_state == 3 && DinValid_i && !DinStop_i |=> s_fsm_state == 0 + ); + + // SET_DATA -> SEND_HEADER + fsm_set_data_to_send_header_a : assert property ( + s_fsm_state == 3 && DinValid_i && DinStop_i |=> s_fsm_state == 4 + ); + + // SEND_HEADER -> SEND_DATA + fsm_send_header_to_send_data_a : assert property ( s_fsm_state == 4 && DoutValid_o && DoutAccept_i && s_header[3:0] == `READ |=> s_fsm_state == 5 ); - assert property ( - s_fsm_state == 4 && DoutValid_o && DoutAccept_i && s_header[3:0] != `READ |=> s_fsm_state == 6 + // SEND_HEADER -> SEND_FOOTER + fsm_send_header_to_send_footer_a : assert property ( + s_fsm_state == 4 && DoutValid_o && DoutAccept_i && s_header[3:0] == `WRITE |=> s_fsm_state == 6 ); - assert property ( + // SEND_DATA -> SEND_FOOTER + fsm_send_data_to_send_footer_a : assert property ( + s_fsm_state == 5 && DoutValid_o && DoutAccept_i |=> s_fsm_state == 6 + ); + + // SEND_FOOTER -> IDLE + fsm_send_footer_to_idle_a : assert property ( s_fsm_state == 6 && DoutValid_o && DoutAccept_i |=> s_fsm_state == 0 ); // Protocol checks - assert property ( + header_in_valid_range_a : assert property ( s_fsm_state > 1 |-> s_header[3:0] inside {`READ, `WRITE} ); - assert property ( + header_stable_a : assert property ( s_fsm_state > 1 |=> $stable(s_header) ); - assert property ( + header_dout_valid_a : assert property ( DoutStart_o && DoutValid_o |-> - Dout_o[3:0] == s_header[3:0] + Dout_o == s_header ); - assert property ( + error_flag_initial_false_a : assert property ( s_fsm_state inside {1, 2, 3} |-> !s_error ); - assert property ( + error_flag_set_invalid_addr_a : assert property ( s_fsm_state >= 4 |-> s_error == !(s_header[7:4] <= 7) ); - assert property ( + footer_dout_valid_a :assert property ( DoutStop_o && DoutValid_o |-> Dout_o == s_error ); - assert property ( + doutvalid_stable_until_acked_a : assert property ( + DoutValid_o && !DoutAccept_i |=> + $stable(DoutValid_o) + ); + + dout_stable_until_acked_a : assert property ( DoutValid_o && !DoutAccept_i |=> $stable(Dout_o) ); - assert property ( + doutstart_stable_until_acked_a : assert property ( DoutValid_o && !DoutAccept_i |=> $stable(DoutStart_o) ); - assert property ( + doutstop_stable_until_acked_a : assert property ( DoutValid_o && !DoutAccept_i |=> $stable(DoutStop_o) ); - assert property ( - DoutValid_o |-> !(DoutStart_o && DoutStop_o) + onehot_doutstart_doutstop_a : assert property ( + DoutValid_o |-> $onehot0({DoutStart_o, DoutStop_o}) ); - assert property ( + doutstart_in_valid_fsm_state_a : assert property ( DoutStart_o |-> s_fsm_state == 4 ); - assert property ( + doutstop_in_valid_fsm_state_a : assert property ( DoutStop_o |-> s_fsm_state == 6 ); - assert property ( + doutvalid_in_valid_fsm_states_a : assert property ( DoutValid_o |-> s_fsm_state >= 4 && s_fsm_state <= 6 ); // Write ack frame - assert property ( + write_frame_a : assert property ( DoutValid_o && DoutStart_o && DoutAccept_i && Dout_o[3:0] == `WRITE |=> !DoutValid_o ##1 DoutValid_o && DoutStop_o ); // Read ack frame - assert property ( + read_frame_a : assert property ( DoutValid_o && DoutStart_o && DoutAccept_i && Dout_o[3:0] == `READ |=> !DoutValid_o ##1 DoutValid_o && !DoutStart_o && !DoutStop_o && !DoutAccept_i [*] ##1 @@ -212,15 +240,64 @@ module properties ( DoutValid_o && DoutStop_o ); - // Can only be proven with abc at the moment - // smtbmc fails with unbounded proof - assert property ( - s_fsm_state == 1 && DinValid_i && DinStart_i && !DinStop_i && DinAccept_o && Din_i[3:0] == `WRITE && Din_i[7:4] <= 7 ##1 - !DinValid_i [*] ##1 - s_fsm_state == 3 && DinValid_i && DinAccept_o && DinStop_i |=> + // Register read in GET_DATA if valid adress was given + get_data_valid_a : assert property ( + s_fsm_state > 2 && s_header[7:4] <= 7 && s_header[3:0] == `READ |-> + s_data == s_register[s_header[7:4]] + ); + + // Error flag set & no register read in GET_DATA if invalid adress was given + get_data_invalid_a : assert property ( + s_fsm_state > 2 && s_header[7:4] > 7 && s_header[3:0] == `READ |=> + s_data == 0 && s_error + ); + + // register stable if read request + reg_stable_during_read_a : assert property ( + s_fsm_state > 1 && s_header[3:0] == `READ |=> + $stable(s_register) + ); + + // Read ack data correct if address is valid + read_ack_data_valid_a : assert property ( + DoutValid_o && DoutStart_o && DoutAccept_i && Dout_o[3:0] == `READ && s_header[7:4] <= 7 |=> + !DoutValid_o ##1 + DoutValid_o && !DoutStart_o && !DoutStop_o && Dout_o == s_data + ); + + // Read ack data zero if address is invalid + read_ack_data_invalid_a : assert property ( + DoutValid_o && DoutStart_o && DoutAccept_i && Dout_o[3:0] == `READ && s_header[7:4] > 7 |=> + !DoutValid_o ##1 + DoutValid_o && !DoutStart_o && !DoutStop_o && Dout_o == 0 + ); + + // Register write in SET_DATA if valid adress was given + set_data_valid_a : assert property ( + s_fsm_state == 3 && DinValid_i && DinAccept_o && DinStop_i && s_header[7:4] <= 7 |=> s_register[s_header[7:4]] == $past(Din_i) ); + // Error flag set & no register write in SET_DATA if invalid adress was given + set_data_invalid_a : assert property ( + s_fsm_state == 3 && DinValid_i && DinAccept_o && DinStop_i && s_header[7:4] > 7 |=> + $stable(s_register) && s_error + ); + + // No register write in SET_DATA if stop don't active + set_data_discard_a : assert property ( + s_fsm_state == 3 && DinValid_i && DinAccept_o && !DinStop_i |=> + $stable(s_register) + ); + + fsm_read_req_when_get_data_a : assert property ( + s_fsm_state == 2 |-> s_header[3:0] == `READ + ); + + fsm_write_req_when_set_data_a : assert property ( + s_fsm_state == 3 |-> s_header[3:0] == `WRITE + ); + endmodule