Add a bunch of new properties; name all assert directives

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