Browse Source

Replace integer coded FSM states by symbolic state names

T. Meissner 7 months ago
parent
commit
9cb4b7d291
1 changed files with 50 additions and 31 deletions
  1. 50
    31
      vai_reg/properties.sv

+ 50
- 31
vai_reg/properties.sv View File

@@ -20,9 +20,18 @@ module properties (
20 20
 );
21 21
 
22 22
 
23
+  // commands
24
+  `define READ      0
25
+  `define WRITE     1
23 26
 
24
-  `define READ 0
25
-  `define WRITE 1
27
+  // FSM states
28
+  `define IDLE        0
29
+  `define GET_HEADER  1
30
+  `define GET_DATA    2
31
+  `define SET_DATA    3
32
+  `define SEND_HEADER 4
33
+  `define SEND_DATA   5
34
+  `define SEND_FOOTER 6
26 35
 
27 36
 
28 37
   reg init_state = 1;
@@ -71,7 +80,7 @@ module properties (
71 80
   // Asserts
72 81
 
73 82
   fsm_state_valid_a : assert property (
74
-    s_fsm_state >= 0 && s_fsm_state <= 6
83
+    s_fsm_state >= `IDLE && s_fsm_state <= `SEND_FOOTER
75 84
   );
76 85
 
77 86
   valid_when_start_a : assert property (
@@ -95,7 +104,7 @@ module properties (
95 104
   );
96 105
 
97 106
   store_header_a : assert property (
98
-    s_fsm_state == 1 && DinValid_i && DinStart_i && DinAccept_o |=>
107
+    s_fsm_state == `GET_HEADER && DinValid_i && DinStart_i && DinAccept_o |=>
99 108
     s_header == $past(Din_i)
100 109
   );
101 110
 
@@ -104,66 +113,73 @@ module properties (
104 113
 
105 114
   // IDLE -> GET_HEADER
106 115
   fsm_idle_to_get_header_a : assert property (
107
-    s_fsm_state == 0 |=> s_fsm_state == 1
116
+    s_fsm_state == `IDLE |=>
117
+    s_fsm_state == `GET_HEADER
108 118
   );
109 119
 
110 120
   // GET_HEADER -> GET_DATA
111 121
   fsm_get_header_to_get_data_a : assert property (
112
-    s_fsm_state == 1 && DinValid_i && DinStart_i && DinStop_i && Din_i[3:0] == `READ |=>
113
-    s_fsm_state == 2
122
+    s_fsm_state == `GET_HEADER && DinValid_i && DinStart_i && DinStop_i && Din_i[3:0] == `READ |=>
123
+    s_fsm_state == `GET_DATA
114 124
   );
115 125
 
116 126
   // GET_HEADER -> SET_DATA
117 127
   fsm_get_header_to_set_data_a : assert property (
118
-    s_fsm_state == 1 && DinValid_i && DinStart_i && !DinStop_i && Din_i[3:0] == `WRITE |=>
119
-    s_fsm_state == 3
128
+    s_fsm_state == `GET_HEADER && DinValid_i && DinStart_i && !DinStop_i && Din_i[3:0] == `WRITE |=>
129
+    s_fsm_state == `SET_DATA
120 130
   );
121 131
 
122 132
   // GET_DATA -> SEND_HEADER
123 133
   fsm_get_data_to_send_header_a : assert property (
124
-    s_fsm_state == 2 |=> s_fsm_state == 4
134
+    s_fsm_state == `GET_DATA |=>
135
+    s_fsm_state == `SEND_HEADER
125 136
   );
126 137
 
127 138
   // SET_DATA -> IDLE
128 139
   fsm_set_data_to_idle_a : assert property (
129
-    s_fsm_state == 3 && DinValid_i && !DinStop_i |=> s_fsm_state == 0
140
+    s_fsm_state == `SET_DATA && DinValid_i && !DinStop_i |=>
141
+    s_fsm_state == `IDLE
130 142
   );
131 143
 
132 144
   // SET_DATA -> SEND_HEADER
133 145
   fsm_set_data_to_send_header_a : assert property (
134
-    s_fsm_state == 3 && DinValid_i && DinStop_i |=> s_fsm_state == 4
146
+    s_fsm_state == `SET_DATA && DinValid_i && DinStop_i |=> s_fsm_state == `SEND_HEADER
135 147
   );
136 148
 
137 149
   // SEND_HEADER -> SEND_DATA
138 150
   fsm_send_header_to_send_data_a : assert property (
139
-    s_fsm_state == 4 && DoutValid_o && DoutAccept_i && s_header[3:0] == `READ |=> s_fsm_state == 5
151
+    s_fsm_state == `SEND_HEADER && DoutValid_o && DoutAccept_i && s_header[3:0] == `READ |=>
152
+    s_fsm_state == `SEND_DATA
140 153
   );
141 154
 
142 155
   // SEND_HEADER -> SEND_FOOTER
143 156
   fsm_send_header_to_send_footer_a : assert property (
144
-    s_fsm_state == 4 && DoutValid_o && DoutAccept_i && s_header[3:0] == `WRITE |=> s_fsm_state == 6
157
+    s_fsm_state == `SEND_HEADER && DoutValid_o && DoutAccept_i && s_header[3:0] == `WRITE |=>
158
+    s_fsm_state == `SEND_FOOTER
145 159
   );
146 160
 
147 161
   // SEND_DATA -> SEND_FOOTER
148 162
   fsm_send_data_to_send_footer_a : assert property (
149
-    s_fsm_state == 5 && DoutValid_o && DoutAccept_i |=> s_fsm_state == 6
163
+    s_fsm_state == `SEND_DATA && DoutValid_o && DoutAccept_i |=>
164
+    s_fsm_state == `SEND_FOOTER
150 165
   );
151 166
 
152 167
   // SEND_FOOTER -> IDLE
153 168
   fsm_send_footer_to_idle_a : assert property (
154
-    s_fsm_state == 6 && DoutValid_o && DoutAccept_i |=> s_fsm_state == 0
169
+    s_fsm_state == `SEND_FOOTER && DoutValid_o && DoutAccept_i |=>
170
+    s_fsm_state == `IDLE
155 171
   );
156 172
 
157 173
 
158 174
   // Protocol checks
159 175
 
160 176
   header_in_valid_range_a : assert property (
161
-    s_fsm_state > 1 |->
177
+    s_fsm_state > `GET_HEADER |->
162 178
     s_header[3:0] inside {`READ, `WRITE}
163 179
   );
164 180
 
165 181
   header_stable_a : assert property (
166
-    s_fsm_state > 1 |=>
182
+    s_fsm_state > `GET_HEADER |=>
167 183
     $stable(s_header)
168 184
   );
169 185
 
@@ -173,12 +189,12 @@ module properties (
173 189
   );
174 190
 
175 191
   error_flag_initial_false_a : assert property (
176
-    s_fsm_state inside {1, 2, 3} |->
192
+    s_fsm_state inside {`GET_HEADER, `GET_DATA, `SET_DATA} |->
177 193
     !s_error
178 194
   );
179 195
 
180 196
   error_flag_set_invalid_addr_a : assert property (
181
-    s_fsm_state >= 4 |->
197
+    s_fsm_state >= `SEND_HEADER |->
182 198
     s_error == !(s_header[7:4] <= 7)
183 199
   );
184 200
 
@@ -212,15 +228,18 @@ module properties (
212 228
   );
213 229
 
214 230
   doutstart_in_valid_fsm_state_a : assert property (
215
-    DoutStart_o |-> s_fsm_state == 4
231
+    DoutStart_o |->
232
+    s_fsm_state == `SEND_HEADER
216 233
   );
217 234
 
218 235
   doutstop_in_valid_fsm_state_a : assert property (
219
-    DoutStop_o |-> s_fsm_state == 6
236
+    DoutStop_o |->
237
+    s_fsm_state == `SEND_FOOTER
220 238
   );
221 239
 
222 240
   doutvalid_in_valid_fsm_states_a : assert property (
223
-    DoutValid_o |-> s_fsm_state >= 4 && s_fsm_state <= 6
241
+    DoutValid_o |->
242
+    s_fsm_state inside {`SEND_HEADER, `SEND_DATA, `SEND_FOOTER}
224 243
   );
225 244
 
226 245
   // Write ack frame
@@ -242,19 +261,19 @@ module properties (
242 261
 
243 262
   // Register read in GET_DATA if valid adress was given
244 263
   get_data_valid_a : assert property (
245
-    s_fsm_state > 2 && s_header[7:4] <= 7 && s_header[3:0] == `READ |->
264
+    s_fsm_state > `GET_DATA && s_header[7:4] <= 7 && s_header[3:0] == `READ |->
246 265
     s_data == s_register[s_header[7:4]]
247 266
   );
248 267
 
249 268
   // Error flag set & no register read in GET_DATA if invalid adress was given
250 269
   get_data_invalid_a : assert property (
251
-    s_fsm_state > 2 && s_header[7:4] > 7 && s_header[3:0] == `READ |=>
270
+    s_fsm_state > `GET_DATA && s_header[7:4] > 7 && s_header[3:0] == `READ |=>
252 271
     s_data == 0 && s_error
253 272
   );
254 273
 
255 274
   // register stable if read request
256 275
   reg_stable_during_read_a : assert property (
257
-    s_fsm_state > 1 && s_header[3:0] == `READ |=>
276
+    s_fsm_state > `GET_HEADER && s_header[3:0] == `READ |=>
258 277
     $stable(s_register)
259 278
   );
260 279
 
@@ -274,28 +293,28 @@ module properties (
274 293
 
275 294
   // Register write in SET_DATA if valid adress was given
276 295
   set_data_valid_a : assert property (
277
-    s_fsm_state == 3 && DinValid_i && DinAccept_o && DinStop_i && s_header[7:4] <= 7 |=>
296
+    s_fsm_state == `SET_DATA && DinValid_i && DinAccept_o && DinStop_i && s_header[7:4] <= 7 |=>
278 297
     s_register[s_header[7:4]] == $past(Din_i)
279 298
   );
280 299
 
281 300
   // Error flag set & no register write in SET_DATA if invalid adress was given
282 301
   set_data_invalid_a : assert property (
283
-    s_fsm_state == 3 && DinValid_i && DinAccept_o && DinStop_i && s_header[7:4] > 7 |=>
302
+    s_fsm_state == `SET_DATA && DinValid_i && DinAccept_o && DinStop_i && s_header[7:4] > 7 |=>
284 303
     $stable(s_register) && s_error
285 304
   );
286 305
 
287 306
   // No register write in SET_DATA if stop don't active
288 307
   set_data_discard_a : assert property (
289
-    s_fsm_state == 3 && DinValid_i && DinAccept_o && !DinStop_i |=>
308
+    s_fsm_state == `SET_DATA && DinValid_i && DinAccept_o && !DinStop_i |=>
290 309
     $stable(s_register)
291 310
   );
292 311
 
293 312
   fsm_read_req_when_get_data_a : assert property (
294
-    s_fsm_state == 2 |-> s_header[3:0] == `READ
313
+    s_fsm_state == `GET_DATA |-> s_header[3:0] == `READ
295 314
   );
296 315
 
297 316
   fsm_write_req_when_set_data_a : assert property (
298
-    s_fsm_state == 3 |-> s_header[3:0] == `WRITE
317
+    s_fsm_state == `SET_DATA |-> s_header[3:0] == `WRITE
299 318
   );
300 319
 
301 320