Go
back
125 // Indication for CSRs
126 1/1 assign ext_clock_switched_o = lc_tx_test_true_strict(lc_clk_byp_ack[3]);
Tests: T1 T2 T3
127
128 // We have multiple response channels for this signal since the RMA wiping requests can go to
129 // multiple modules that perform wiping in parallel. For security reasons, this signal is not
130 // daisy-chained - see #19136 for context. Synchronize ACK signals separately, combine with
131 // bitwise LC AND function and feed into FSM.
132 lc_tx_t [NumRmaAckSigs-1:0] lc_flash_rma_ack;
133 for (genvar k = 0; k < NumRmaAckSigs; k++) begin : gen_syncs
134 prim_lc_sync #(
135 .NumCopies(1)
136 ) u_prim_lc_sync_flash_rma_ack(
137 .clk_i,
138 .rst_ni,
139 .lc_en_i(lc_flash_rma_ack_i[k]),
140 .lc_en_o({lc_flash_rma_ack[k]})
141 );
142 end
143
144 lc_tx_t lc_flash_rma_ack_combined;
145 always_comb begin
146 1/1 lc_flash_rma_ack_combined = On;
Tests: T1 T2 T3
147 1/1 for (int k = 0; k < NumRmaAckSigs; k++) begin
Tests: T1 T2 T3
148 1/1 lc_flash_rma_ack_combined = lc_tx_and_hi(lc_flash_rma_ack_combined, lc_flash_rma_ack[k]);
Tests: T1 T2 T3
149 end
150 end
151
152 // Make buffered copies for consumption in the FSM below.
153 lc_tx_t [2:0] lc_flash_rma_ack_buf;
154 prim_lc_sync #(
155 .NumCopies(3),
156 .AsyncOn(0)
157 ) u_prim_lc_sync_flash_rma_ack_buf (
158 .clk_i,
159 .rst_ni,
160 .lc_en_i(lc_flash_rma_ack_combined),
161 .lc_en_o(lc_flash_rma_ack_buf)
162 );
163
164 ///////////////
165 // FSM Logic //
166 ///////////////
167 fsm_state_e fsm_state_d, fsm_state_q;
168
169 // Continuously feed in valid signal for LC state.
170 logic lc_state_valid_d, lc_state_valid_q;
171 1/1 assign lc_state_valid_d = lc_state_valid_i;
Tests: T12 T29 T41
172
173 // Encoded state vector.
174 lc_state_e lc_state_d, lc_state_q, next_lc_state;
175 lc_cnt_e lc_cnt_d, lc_cnt_q, next_lc_cnt;
176
177 // Feed the next lc state reg back to the programming interface of OTP.
178 1/1 assign otp_prog_lc_state_o = next_lc_state;
Tests: T1 T2 T3
179 1/1 assign otp_prog_lc_cnt_o = next_lc_cnt;
Tests: T1 T2 T3
180
181 // Conditional LC signal outputs
182 lc_tx_t lc_clk_byp_req, lc_flash_rma_req, lc_check_byp_en;
183
184 `ASSERT_KNOWN(LcStateKnown_A, lc_state_q )
185 `ASSERT_KNOWN(LcCntKnown_A, lc_cnt_q )
186 `ASSERT_KNOWN(FsmStateKnown_A, fsm_state_q )
187
188 // Hashed token to compare against.
189 logic [1:0] hashed_token_valid_mux;
190 lc_token_t hashed_token_mux;
191
192 // Multibit state error from state decoder
193 logic [5:0] state_invalid_error;
194
195 // Strap sample override signal.
196 logic set_strap_en_override;
197
198 // Registers whether volatile unlock has been successful
199 prim_mubi_pkg::mubi8_t volatile_raw_unlock_success_d, volatile_raw_unlock_success_q;
200
201 // SEC_CM: MAIN.CTRL_FLOW.CONSISTENCY
202 always_comb begin : p_fsm
203 // FSM default state assignments.
204 1/1 fsm_state_d = fsm_state_q;
Tests: T1 T2 T3
205 1/1 lc_state_d = lc_state_q;
Tests: T1 T2 T3
206 1/1 lc_cnt_d = lc_cnt_q;
Tests: T1 T2 T3
207
208 // Token hashing.
209 1/1 token_hash_req_o = 1'b0;
Tests: T1 T2 T3
210 1/1 token_hash_req_chk_o = 1'b1;
Tests: T1 T2 T3
211
212 // OTP Interface
213 1/1 otp_prog_req_o = 1'b0;
Tests: T1 T2 T3
214
215 // Defaults for status/error signals.
216 1/1 token_invalid_error_o = 1'b0;
Tests: T1 T2 T3
217 1/1 otp_prog_error_o = 1'b0;
Tests: T1 T2 T3
218 1/1 flash_rma_error_o = 1'b0;
Tests: T1 T2 T3
219 1/1 trans_success_o = 1'b0;
Tests: T1 T2 T3
220 1/1 state_invalid_error_o = 1'b0;
Tests: T1 T2 T3
221
222 // Status indication going to power manager.
223 1/1 init_done_o = 1'b1;
Tests: T1 T2 T3
224 1/1 idle_o = 1'b0;
Tests: T1 T2 T3
225
226 // ---------- VOLATILE_TEST_UNLOCKED CODE SECTION START ----------
227 // NOTE THAT THIS IS A FEATURE FOR TEST CHIPS ONLY TO MITIGATE
228 // THE RISK OF A BROKEN OTP MACRO. THIS WILL BE DISABLED VIA
229 // SecVolatileRawUnlockEn AT COMPILETIME FOR PRODUCTION DEVICES.
230 // ---------------------------------------------------------------
231 1/1 set_strap_en_override = 1'b0;
Tests: T1 T2 T3
232 1/1 volatile_raw_unlock_success_d = volatile_raw_unlock_success_q;
Tests: T1 T2 T3
233 // ----------- VOLATILE_TEST_UNLOCKED CODE SECTION END -----------
234
235 // These signals remain asserted once set to On.
236 // Note that the remaining life cycle signals are decoded in
237 // the lc_ctrl_signal_decode submodule.
238 1/1 lc_clk_byp_req = lc_clk_byp_req_o;
Tests: T1 T2 T3
239 1/1 lc_flash_rma_req = lc_flash_rma_req_o;
Tests: T1 T2 T3
240 1/1 lc_check_byp_en = lc_check_byp_en_o;
Tests: T1 T2 T3
241
242 1/1 unique case (fsm_state_q)
Tests: T1 T2 T3
243 ///////////////////////////////////////////////////////////////////
244 // Wait here until OTP has initialized and the
245 // power manager sends an initialization request.
246 ResetSt: begin
247 1/1 init_done_o = 1'b0;
Tests: T1 T2 T3
248 1/1 lc_clk_byp_req = Off;
Tests: T1 T2 T3
249 1/1 lc_flash_rma_req = Off;
Tests: T1 T2 T3
250 1/1 lc_check_byp_en = Off;
Tests: T1 T2 T3
251 1/1 if (init_req_i && lc_state_valid_q) begin
Tests: T1 T2 T3
252 1/1 fsm_state_d = IdleSt;
Tests: T1 T2 T3
253 // Fetch LC state vector from OTP.
254 1/1 lc_state_d = lc_state_i;
Tests: T1 T2 T3
255 1/1 lc_cnt_d = lc_cnt_i;
Tests: T1 T2 T3
256 end
MISSING_ELSE
257 end
258 ///////////////////////////////////////////////////////////////////
259 // Idle state where life cycle control signals are broadcast.
260 // Note that the life cycle signals are decoded and broadcast
261 // in the lc_ctrl_signal_decode submodule.
262 IdleSt: begin
263 1/1 idle_o = 1'b1;
Tests: T1 T2 T3
264
265 // ---------- VOLATILE_TEST_UNLOCKED CODE SECTION START ----------
266 // NOTE THAT THIS IS A FEATURE FOR TEST CHIPS ONLY TO MITIGATE
267 // THE RISK OF A BROKEN OTP MACRO. THIS WILL BE DISABLED VIA
268 // SecVolatileRawUnlockEn AT COMPILETIME FOR PRODUCTION DEVICES.
269 // ---------------------------------------------------------------
270 // Note that if the volatile unlock mechanism is available,
271 // we have to stop fetching the OTP value after a volatile unlock has succeeded.
272 // Otherwise we unconditionally fetch from OTP in this state.
273 1/1 if (!(SecVolatileRawUnlockEn && lc_state_q == LcStTestUnlocked0 && lc_cnt_q != LcCnt0) ||
Tests: T1 T2 T3
274 prim_mubi_pkg::mubi8_test_false_loose(volatile_raw_unlock_success_q)) begin
275 // Continuously fetch LC state vector from OTP.
276 // The state is locked in once a transition is started.
277 1/1 lc_state_d = lc_state_i;
Tests: T1 T2 T3
278 1/1 lc_cnt_d = lc_cnt_i;
Tests: T1 T2 T3
279 end
==> MISSING_ELSE
280 // ----------- VOLATILE_TEST_UNLOCKED CODE SECTION END -----------
281
282 // If the life cycle state is SCRAP, we move the FSM into a terminal
283 // SCRAP state that does not allow any transitions to be initiated anymore.
284 1/1 if (lc_state_q == LcStScrap) begin
Tests: T1 T2 T3
285 1/1 fsm_state_d = ScrapSt;
Tests: T1 T14 T5
286
287 // ---------- VOLATILE_TEST_UNLOCKED CODE SECTION START ----------
288 // NOTE THAT THIS IS A FEATURE FOR TEST CHIPS ONLY TO MITIGATE
289 // THE RISK OF A BROKEN OTP MACRO. THIS WILL BE DISABLED VIA
290 // SecVolatileRawUnlockEn AT COMPILETIME FOR PRODUCTION DEVICES.
291 // ---------------------------------------------------------------
292 // Only enter here if volatile RAW unlock is available and enabled.
293 1/1 end else if (SecVolatileRawUnlockEn && volatile_raw_unlock_i && trans_cmd_i) begin
Tests: T1 T2 T3
294 // We only allow transitions from RAW -> TEST_UNLOCKED0
295 unreachable if (lc_state_q == LcStRaw &&
296 trans_target_i == {DecLcStateNumRep{DecLcStTestUnlocked0}} &&
297 !trans_invalid_error_o) begin
298 // 128bit token check (without passing it through the KMAC)
299 unreachable if (unhashed_token_i == RndCnstRawUnlockTokenHashed) begin
300 // We stay in Idle, but update the life cycle state register (volatile).
301 unreachable lc_state_d = LcStTestUnlocked0;
302 // If the count is 0, we set it to 1 - otherwise we just leave it as is so that the
303 // register value is in sync with what has been programmed to OTP already (there may
304 // have been unsuccessul raw unlock attempts before that already incremented it).
305 unreachable lc_cnt_d = (lc_cnt_q == LcCnt0) ? LcCnt1 : lc_cnt_q;
306 // Re-sample the DFT straps in the pinmux.
307 // This signal will be delayed by several cycles so that the LC_CTRL signals
308 // have time to propagate.
309 unreachable set_strap_en_override = 1'b1;
310 // We have to remember that the transition was successful in order to correctly
311 // disable the continuos sampling of the life cycle state vector coming from OTP.
312 unreachable volatile_raw_unlock_success_d = prim_mubi_pkg::MuBi8True;
313 // Indicate that the transition was successful.
314 unreachable trans_success_o = 1'b1;
315 end else begin
316 unreachable token_invalid_error_o = 1'b1;
317 unreachable fsm_state_d = PostTransSt;
318 end
319 end else begin
320 // Transition invalid error is set by lc_ctrl_state_transition module.
321 unreachable fsm_state_d = PostTransSt;
322 end
323 // ----------- VOLATILE_TEST_UNLOCKED CODE SECTION END -----------
324 // Initiate a transition. This will first increment the
325 // life cycle counter before hashing and checking the token.
326 1/1 end else if (trans_cmd_i) begin
Tests: T1 T2 T3
327 1/1 fsm_state_d = ClkMuxSt;
Tests: T1 T2 T3
328 end
MISSING_ELSE
329 // If we are in a non-PROD life cycle state, steer the clock mux if requested. This
330 // action is available in IdleSt so that the mux can be steered without having to initiate
331 // a life cycle transition. If a transition is initiated however, the life cycle controller
332 // will wait for the clock mux acknowledgement in the ClkMuxSt state before proceeding.
333 1/1 if (lc_state_q inside {LcStRaw,
Tests: T1 T2 T3
334 LcStTestLocked0,
335 LcStTestLocked1,
336 LcStTestLocked2,
337 LcStTestLocked3,
338 LcStTestLocked4,
339 LcStTestLocked5,
340 LcStTestLocked6,
341 LcStTestUnlocked0,
342 LcStTestUnlocked1,
343 LcStTestUnlocked2,
344 LcStTestUnlocked3,
345 LcStTestUnlocked4,
346 LcStTestUnlocked5,
347 LcStTestUnlocked6,
348 LcStTestUnlocked7,
349 LcStRma}) begin
350 1/1 if (use_ext_clock_i) begin
Tests: T1 T2 T3
351 1/1 lc_clk_byp_req = On;
Tests: T1 T16 T8
352 end
MISSING_ELSE
353 end
MISSING_ELSE
354 end
355 ///////////////////////////////////////////////////////////////////
356 // Clock mux state. If we are in RAW, TEST* or RMA, it is permissible
357 // to switch to an external clock source. If the bypass request is
358 // asserted, we have to wait until the clock mux and clock manager
359 // have switched the mux and the clock divider. Also, we disable the
360 // life cycle partition checks at this point since we are going to
361 // alter the contents in the OTP memory array, which could lead to
362 // spurious escalations.
363 ClkMuxSt: begin
364 1/1 lc_check_byp_en = On;
Tests: T1 T2 T3
365 1/1 if (lc_state_q inside {LcStRaw,
Tests: T1 T2 T3
366 LcStTestLocked0,
367 LcStTestLocked1,
368 LcStTestLocked2,
369 LcStTestLocked3,
370 LcStTestLocked4,
371 LcStTestLocked5,
372 LcStTestLocked6,
373 LcStTestUnlocked0,
374 LcStTestUnlocked1,
375 LcStTestUnlocked2,
376 LcStTestUnlocked3,
377 LcStTestUnlocked4,
378 LcStTestUnlocked5,
379 LcStTestUnlocked6,
380 LcStTestUnlocked7,
381 LcStRma}) begin
382 1/1 if (use_ext_clock_i) begin
Tests: T1 T2 T3
383 1/1 lc_clk_byp_req = On;
Tests: T1 T16 T40
384 1/1 if (lc_tx_test_true_strict(lc_clk_byp_ack[0])) begin
Tests: T1 T16 T40
385 1/1 fsm_state_d = CntIncrSt;
Tests: T1 T16 T40
386 end
MISSING_ELSE
387 end else begin
388 1/1 fsm_state_d = CntIncrSt;
Tests: T1 T2 T3
389 end
390 end else begin
391 1/1 fsm_state_d = CntIncrSt;
Tests: T1 T4 T13
392 end
393 end
394 ///////////////////////////////////////////////////////////////////
395 // This increments the life cycle counter state.
396 CntIncrSt: begin
397 // If the counter has reached the maximum, bail out.
398 1/1 if (trans_cnt_oflw_error_o) begin
Tests: T1 T2 T3
399 1/1 fsm_state_d = PostTransSt;
Tests: T13 T22 T27
400 end else begin
401 1/1 fsm_state_d = CntProgSt;
Tests: T1 T2 T3
402 end
403 end
404 ///////////////////////////////////////////////////////////////////
405 // This programs the life cycle counter state.
406 CntProgSt: begin
407 1/1 otp_prog_req_o = 1'b1;
Tests: T1 T2 T3
408
409 // If the clock mux has been steered, double check that this is still the case.
410 // Otherwise abort the transition operation.
411 1/1 if (lc_clk_byp_req_o != lc_clk_byp_ack[1]) begin
Tests: T1 T2 T3
412 1/1 fsm_state_d = PostTransSt;
Tests: T13 T21 T22
413 1/1 otp_prog_error_o = 1'b1;
Tests: T13 T21 T22
414 end
MISSING_ELSE
415
416 // Check return value and abort if there
417 // was an error.
418 1/1 if (otp_prog_ack_i) begin
Tests: T1 T2 T3
419 1/1 if (otp_prog_err_i) begin
Tests: T1 T2 T3
420 1/1 fsm_state_d = PostTransSt;
Tests: T4 T7 T42
421 1/1 otp_prog_error_o = 1'b1;
Tests: T4 T7 T42
422 end else begin
423 1/1 fsm_state_d = TransCheckSt;
Tests: T1 T2 T3
424 end
425 end
MISSING_ELSE
426 end
427 ///////////////////////////////////////////////////////////////////
428 // First transition valid check. This will be repeated several
429 // times below.
430 TransCheckSt: begin
431 1/1 if (trans_invalid_error_o) begin
Tests: T1 T2 T3
432 1/1 fsm_state_d = PostTransSt;
Tests: T13 T20 T22
433 end else begin
434 1/1 fsm_state_d = TokenHashSt;
Tests: T1 T2 T3
435 end
436 end
437 ///////////////////////////////////////////////////////////////////
438 // Hash and compare the token, no matter whether this transition
439 // is conditional or not. Unconditional transitions just use a known
440 // all-zero token value. That way, we always compare a hashed token
441 // and guarantee that no other control flow path exists that could
442 // bypass the token check.
443 // SEC_CM: TOKEN.DIGEST
444 TokenHashSt: begin
445 1/1 token_hash_req_o = 1'b1;
Tests: T1 T2 T3
446 1/1 if (token_hash_ack_i) begin
Tests: T1 T2 T3
447 // This is the first comparison.
448 // The token is compared two more times further below.
449 // Also note that conditional transitions won't be possible if the
450 // corresponding token is not valid. This only applies to tokens stored in
451 // OTP. I.e., these tokens first have to be provisioned, before they can be used.
452 1/1 if (hashed_token_i == hashed_token_mux &&
Tests: T1 T2 T3
453 !token_hash_err_i &&
454 &hashed_token_valid_mux) begin
455 1/1 fsm_state_d = FlashRmaSt;
Tests: T1 T3 T13
456 end else begin
457 1/1 fsm_state_d = PostTransSt;
Tests: T2 T13 T20
458 1/1 token_invalid_error_o = 1'b1;
Tests: T2 T13 T20
459 end
460 end
MISSING_ELSE
461 end
462 ///////////////////////////////////////////////////////////////////
463 // Flash RMA state. Note that we check the flash response again
464 // two times later below.
465 FlashRmaSt: begin
466 1/1 if (trans_target_i == {DecLcStateNumRep{DecLcStRma}}) begin
Tests: T1 T3 T13
467 1/1 lc_flash_rma_req = On;
Tests: T1 T13 T14
468 1/1 if (lc_tx_test_true_strict(lc_flash_rma_ack_buf[0])) begin
Tests: T1 T13 T14
469 1/1 fsm_state_d = TokenCheck0St;
Tests: T1 T13 T14
470 end
MISSING_ELSE
471 end else begin
472 1/1 fsm_state_d = TokenCheck0St;
Tests: T1 T3 T13
473 end
474 end
475 ///////////////////////////////////////////////////////////////////
476 // Check again two times whether this transition and the hashed
477 // token are valid. Also check again whether the flash RMA
478 // response is valid.
479 // SEC_CM: TOKEN.DIGEST
480 TokenCheck0St,
481 TokenCheck1St: begin
482 1/1 if (trans_invalid_error_o) begin
Tests: T1 T3 T13
483 1/1 fsm_state_d = PostTransSt;
Tests: T20 T43 T44
484 end else begin
485 // If any of these RMA are conditions are true,
486 // all of them must be true at the same time.
487 1/1 if ((trans_target_i != {DecLcStateNumRep{DecLcStRma}} &&
Tests: T1 T3 T13
488 lc_tx_test_false_strict(lc_flash_rma_req_o) &&
489 lc_tx_test_false_strict(lc_flash_rma_ack_buf[1])) ||
490 (trans_target_i == {DecLcStateNumRep{DecLcStRma}} &&
491 lc_tx_test_true_strict(lc_flash_rma_req_o) &&
492 lc_tx_test_true_strict(lc_flash_rma_ack_buf[1]))) begin
493 1/1 if (hashed_token_i == hashed_token_mux &&
Tests: T1 T3 T13
494 !token_hash_err_i &&
495 &hashed_token_valid_mux) begin
496 1/1 if (fsm_state_q == TokenCheck1St) begin
Tests: T1 T3 T13
497 // This is the only way we can get into the
498 // programming state.
499 1/1 fsm_state_d = TransProgSt;
Tests: T1 T3 T13
500 end else begin
501 1/1 fsm_state_d = TokenCheck1St;
Tests: T1 T3 T13
502 end
503 end else begin
504 0/1 ==> fsm_state_d = PostTransSt;
505 0/1 ==> token_invalid_error_o = 1'b1;
506 end
507 // The flash RMA process failed.
508 end else begin
509 1/1 fsm_state_d = PostTransSt;
Tests: T13 T21 T22
510 1/1 flash_rma_error_o = 1'b1;
Tests: T13 T21 T22
511 end
512 end
513 end
514 ///////////////////////////////////////////////////////////////////
515 // Initiate OTP transaction. Note that the concurrent
516 // LC state check is continuously checking whether the
517 // new LC state remains valid. Once the ack returns we are
518 // done with the transition and can go into the terminal PosTransSt.
519 TransProgSt: begin
520 1/1 otp_prog_req_o = 1'b1;
Tests: T1 T3 T13
521
522 // If the clock mux has been steered, double check that this is still the case.
523 // Otherwise abort the transition operation.
524 1/1 if (lc_clk_byp_req_o != lc_clk_byp_ack[2]) begin
Tests: T1 T3 T13
525 1/1 fsm_state_d = PostTransSt;
Tests: T45 T46 T47
526 1/1 otp_prog_error_o = 1'b1;
Tests: T45 T46 T47
527 // Also double check that the RMA signals remain stable.
528 // Otherwise abort the transition operation.
529 1/1 end else if ((trans_target_i != {DecLcStateNumRep{DecLcStRma}} &&
Tests: T1 T3 T13
530 (lc_flash_rma_req_o != Off || lc_flash_rma_ack_buf[2] != Off)) ||
531 (trans_target_i == {DecLcStateNumRep{DecLcStRma}} &&
532 (lc_flash_rma_req_o != On || lc_flash_rma_ack_buf[2] != On))) begin
533 1/1 fsm_state_d = PostTransSt;
Tests: T21 T48 T49
534 1/1 flash_rma_error_o = 1'b1;
Tests: T21 T48 T49
535 1/1 end else if (otp_prog_ack_i) begin
Tests: T1 T3 T13
536 1/1 fsm_state_d = PostTransSt;
Tests: T1 T3 T13
537 1/1 otp_prog_error_o = otp_prog_err_i;
Tests: T1 T3 T13
538 1/1 trans_success_o = ~otp_prog_err_i;
Tests: T1 T3 T13
539 end
MISSING_ELSE
540 end
541 ///////////////////////////////////////////////////////////////////
542 // Terminal states.
543 ScrapSt,
544 1/1 PostTransSt: ;
Tests: T1 T2 T3
545
546
547 EscalateSt: begin
548 // During an escalation it is okay to de-assert token_hash_req without receivng ACK.
549 1/1 token_hash_req_chk_o = 1'b0;
Tests: T3 T4 T12
550 end
551
552 InvalidSt: begin
553 // During an escalation it is okay to de-assert token_hash_req without receivng ACK.
554 1/1 token_hash_req_chk_o = 1'b0;
Tests: T3 T12 T6
555 1/1 state_invalid_error_o = 1'b1;
Tests: T3 T12 T6
556 end
557 ///////////////////////////////////////////////////////////////////
558 // Go to terminal error state if we get here.
559 default: begin
560 fsm_state_d = InvalidSt;
561 state_invalid_error_o = 1'b1;
562 end
563 ///////////////////////////////////////////////////////////////////
564 endcase
565
566 // SEC_CM: MAIN.FSM.GLOBAL_ESC
567 1/1 if (esc_scrap_state0_i || esc_scrap_state1_i) begin
Tests: T1 T2 T3
568 1/1 fsm_state_d = EscalateSt;
Tests: T3 T4 T12
569 // SEC_CM: MAIN.FSM.LOCAL_ESC
570 // If at any time the life cycle state encoding or any other FSM state within this module
571 // is not valid, we jump into the terminal error state right away.
572 // Note that state_invalid_error is a multibit error signal
573 // with different error sources - need to reduce this to one bit here.
574 1/1 end else if ((|state_invalid_error | token_if_fsm_err_i) && (fsm_state_q != EscalateSt)) begin
Tests: T1 T2 T3
575 1/1 fsm_state_d = InvalidSt;
Tests: T3 T12 T6
576 1/1 state_invalid_error_o = 1'b1;
Tests: T3 T12 T6
577 end
MISSING_ELSE
578 end
579
580 /////////////////
581 // State Flops //
582 /////////////////
583
584 3/3 `PRIM_FLOP_SPARSE_FSM(u_fsm_state_regs, fsm_state_d, fsm_state_q, fsm_state_e, ResetSt)
Tests: T1 T2 T3 | T1 T2 T3 | T1 T2 T3
PRIM_FLOP_SPARSE_FSM(u_fsm_state_regs, fsm_state_d, fsm_state_q, fsm_state_e, ResetSt):
584.1 `ifdef SIMULATION
584.2 prim_sparse_fsm_flop #(
584.3 .StateEnumT(fsm_state_e),
584.4 .Width($bits(fsm_state_e)),
584.5 .ResetValue($bits(fsm_state_e)'(ResetSt)),
584.6 .EnableAlertTriggerSVA(1),
584.7 .CustomForceName("fsm_state_q")
584.8 ) u_fsm_state_regs (
584.9 .clk_i ( clk_i ),
584.10 .rst_ni ( rst_ni ),
584.11 .state_i ( fsm_state_d ),
584.12 .state_o ( )
584.13 );
584.14 always_ff @(posedge clk_i or negedge rst_ni) begin
584.15 1/1 if (!rst_ni) begin
Tests: T1 T2 T3
584.16 1/1 fsm_state_q <= ResetSt;
Tests: T1 T2 T3
584.17 end else begin
584.18 1/1 fsm_state_q <= fsm_state_d;
Tests: T1 T2 T3
584.19 end
584.20 end
584.21 u_fsm_state_regs_A: assert property (@(posedge clk_i) disable iff ((!rst_ni) !== '0) (fsm_state_q === u_fsm_state_regs.state_o))
584.22 else begin
584.23 `ifdef UVM
584.24 uvm_pkg::uvm_report_error("ASSERT FAILED", "u_fsm_state_regs_A", uvm_pkg::UVM_NONE,
584.25 "../src/lowrisc_ip_lc_ctrl_0.1/rtl/lc_ctrl_fsm.sv", 584, "", 1);
584.26 `else
584.27 $error("%0t: (%0s:%0d) [%m] [ASSERT FAILED] %0s", $time, `__FILE__, `__LINE__,
584.28 `PRIM_STRINGIFY(u_fsm_state_regs_A));
584.29 `endif
584.30 end
584.31 `else
584.32 prim_sparse_fsm_flop #(
584.33 .StateEnumT(fsm_state_e),
584.34 .Width($bits(fsm_state_e)),
584.35 .ResetValue($bits(fsm_state_e)'(ResetSt)),
584.36 .EnableAlertTriggerSVA(1)
584.37 ) u_fsm_state_regs (
584.38 .clk_i ( `PRIM_FLOP_CLK ),
584.39 .rst_ni ( `PRIM_FLOP_RST ),
584.40 .state_i ( fsm_state_d ),
584.41 .state_o ( fsm_state_q )
584.42 );
584.43 `endif585 3/3 `PRIM_FLOP_SPARSE_FSM(u_state_regs, lc_state_d, lc_state_q, lc_state_e, LcStScrap)
Tests: T1 T2 T3 | T1 T2 T3 | T1 T2 T3
PRIM_FLOP_SPARSE_FSM(u_state_regs, lc_state_d, lc_state_q, lc_state_e, LcStScrap):
585.1 `ifdef SIMULATION
585.2 prim_sparse_fsm_flop #(
585.3 .StateEnumT(lc_state_e),
585.4 .Width($bits(lc_state_e)),
585.5 .ResetValue($bits(lc_state_e)'(LcStScrap)),
585.6 .EnableAlertTriggerSVA(1),
585.7 .CustomForceName("lc_state_q")
585.8 ) u_state_regs (
585.9 .clk_i ( clk_i ),
585.10 .rst_ni ( rst_ni ),
585.11 .state_i ( lc_state_d ),
585.12 .state_o ( )
585.13 );
585.14 always_ff @(posedge clk_i or negedge rst_ni) begin
585.15 1/1 if (!rst_ni) begin
Tests: T1 T2 T3
585.16 1/1 lc_state_q <= LcStScrap;
Tests: T1 T2 T3
585.17 end else begin
585.18 1/1 lc_state_q <= lc_state_d;
Tests: T1 T2 T3
585.19 end
585.20 end
585.21 u_state_regs_A: assert property (@(posedge clk_i) disable iff ((!rst_ni) !== '0) (lc_state_q === u_state_regs.state_o))
585.22 else begin
585.23 `ifdef UVM
585.24 uvm_pkg::uvm_report_error("ASSERT FAILED", "u_state_regs_A", uvm_pkg::UVM_NONE,
585.25 "../src/lowrisc_ip_lc_ctrl_0.1/rtl/lc_ctrl_fsm.sv", 585, "", 1);
585.26 `else
585.27 $error("%0t: (%0s:%0d) [%m] [ASSERT FAILED] %0s", $time, `__FILE__, `__LINE__,
585.28 `PRIM_STRINGIFY(u_state_regs_A));
585.29 `endif
585.30 end
585.31 `else
585.32 prim_sparse_fsm_flop #(
585.33 .StateEnumT(lc_state_e),
585.34 .Width($bits(lc_state_e)),
585.35 .ResetValue($bits(lc_state_e)'(LcStScrap)),
585.36 .EnableAlertTriggerSVA(1)
585.37 ) u_state_regs (
585.38 .clk_i ( `PRIM_FLOP_CLK ),
585.39 .rst_ni ( `PRIM_FLOP_RST ),
585.40 .state_i ( lc_state_d ),
585.41 .state_o ( lc_state_q )
585.42 );
585.43 `endif586 3/3 `PRIM_FLOP_SPARSE_FSM(u_cnt_regs, lc_cnt_d, lc_cnt_q, lc_cnt_e, LcCnt24)
Tests: T1 T2 T3 | T1 T2 T3 | T1 T2 T3
PRIM_FLOP_SPARSE_FSM(u_cnt_regs, lc_cnt_d, lc_cnt_q, lc_cnt_e, LcCnt24):
586.1 `ifdef SIMULATION
586.2 prim_sparse_fsm_flop #(
586.3 .StateEnumT(lc_cnt_e),
586.4 .Width($bits(lc_cnt_e)),
586.5 .ResetValue($bits(lc_cnt_e)'(LcCnt24)),
586.6 .EnableAlertTriggerSVA(1),
586.7 .CustomForceName("lc_cnt_q")
586.8 ) u_cnt_regs (
586.9 .clk_i ( clk_i ),
586.10 .rst_ni ( rst_ni ),
586.11 .state_i ( lc_cnt_d ),
586.12 .state_o ( )
586.13 );
586.14 always_ff @(posedge clk_i or negedge rst_ni) begin
586.15 1/1 if (!rst_ni) begin
Tests: T1 T2 T3
586.16 1/1 lc_cnt_q <= LcCnt24;
Tests: T1 T2 T3
586.17 end else begin
586.18 1/1 lc_cnt_q <= lc_cnt_d;
Tests: T1 T2 T3
586.19 end
586.20 end
586.21 u_cnt_regs_A: assert property (@(posedge clk_i) disable iff ((!rst_ni) !== '0) (lc_cnt_q === u_cnt_regs.state_o))
586.22 else begin
586.23 `ifdef UVM
586.24 uvm_pkg::uvm_report_error("ASSERT FAILED", "u_cnt_regs_A", uvm_pkg::UVM_NONE,
586.25 "../src/lowrisc_ip_lc_ctrl_0.1/rtl/lc_ctrl_fsm.sv", 586, "", 1);
586.26 `else
586.27 $error("%0t: (%0s:%0d) [%m] [ASSERT FAILED] %0s", $time, `__FILE__, `__LINE__,
586.28 `PRIM_STRINGIFY(u_cnt_regs_A));
586.29 `endif
586.30 end
586.31 `else
586.32 prim_sparse_fsm_flop #(
586.33 .StateEnumT(lc_cnt_e),
586.34 .Width($bits(lc_cnt_e)),
586.35 .ResetValue($bits(lc_cnt_e)'(LcCnt24)),
586.36 .EnableAlertTriggerSVA(1)
586.37 ) u_cnt_regs (
586.38 .clk_i ( `PRIM_FLOP_CLK ),
586.39 .rst_ni ( `PRIM_FLOP_RST ),
586.40 .state_i ( lc_cnt_d ),
586.41 .state_o ( lc_cnt_q )
586.42 );
586.43 `endif587
588 always_ff @(posedge clk_i or negedge rst_ni) begin : p_regs
589 1/1 if (!rst_ni) begin
Tests: T1 T2 T3
590 1/1 lc_state_valid_q <= 1'b0;
Tests: T1 T2 T3
591 end else begin
592 1/1 lc_state_valid_q <= lc_state_valid_d;
Tests: T1 T2 T3
593 end
594 end
595
596 // ---------- VOLATILE_TEST_UNLOCKED CODE SECTION START ----------
597 // NOTE THAT THIS IS A FEATURE FOR TEST CHIPS ONLY TO MITIGATE
598 // THE RISK OF A BROKEN OTP MACRO. THIS WILL BE DISABLED VIA
599 // SecVolatileRawUnlockEn AT COMPILETIME FOR PRODUCTION DEVICES.
600 // ---------------------------------------------------------------
601 if (SecVolatileRawUnlockEn) begin : gen_strap_delay_regs
602 // The delay on the life cycle signals is 1 sender + 2 receiver domain
603 // cycles. We are delaying this cycle several cycles more than that so
604 // that the life cycle signals have time to propagate (for good measure).
605 localparam int NumStrapDelayRegs = 10;
606 logic [NumStrapDelayRegs-1:0] strap_en_override_q;
607 always_ff @(posedge clk_i or negedge rst_ni) begin : p_volatile_raw_unlock_reg
608 if(!rst_ni) begin
609 strap_en_override_q <= '0;
610 volatile_raw_unlock_success_q <= prim_mubi_pkg::MuBi8False;
611 end else begin
612 strap_en_override_q <= {strap_en_override_q[NumStrapDelayRegs-2:0],
613 // This is a set-reg that will stay high until the next reset.
614 set_strap_en_override || strap_en_override_q[0]};
615 volatile_raw_unlock_success_q <= volatile_raw_unlock_success_d;
616 end
617 end
618
619 assign strap_en_override_o = strap_en_override_q[NumStrapDelayRegs-1];
620 end else begin : gen_no_strap_delay_regs
621 // In this case we tie the strap sampling off.
622 logic unused_sigs;
623 0/1 ==> assign unused_sigs = ^{set_strap_en_override,
624 volatile_raw_unlock_success_d};
625 assign strap_en_override_o = 1'b0;
626 assign volatile_raw_unlock_success_q = prim_mubi_pkg::MuBi8False;
627 end
628 // ----------- VOLATILE_TEST_UNLOCKED CODE SECTION END -----------
629
630 ///////////////
631 // Token mux //
632 ///////////////
633
634 lc_ctrl_pkg::lc_tx_t [3:0] rma_token_valid;
635 prim_lc_sync #(
636 .NumCopies(4),
637 .AsyncOn(0),
638 .ResetValueIsOn(0)
639 ) u_prim_lc_sync_rma_token_valid (
640 .clk_i,
641 .rst_ni,
642 .lc_en_i(rma_token_valid_i),
643 .lc_en_o(rma_token_valid)
644 );
645
646 lc_ctrl_pkg::lc_tx_t [7:0] test_tokens_valid;
647 prim_lc_sync #(
648 .NumCopies(8),
649 .AsyncOn(0),
650 .ResetValueIsOn(0)
651 ) u_prim_lc_sync_test_token_valid (
652 .clk_i,
653 .rst_ni,
654 .lc_en_i(test_tokens_valid_i),
655 .lc_en_o(test_tokens_valid)
656 );
657
658 // SEC_CM: TOKEN_MUX.CTRL.REDUN
659 // The token mux is split into two halves for which we use separate mux select signals
660 // that have both been generated from separately buffered multibit lifecycle signals.
661 logic [2**TokenIdxWidth-1:0][LcTokenWidth/2-1:0] hashed_tokens_lower, hashed_tokens_upper;
662 // These helper signals are only there to increase readability of the mux code below.
663 logic [LcTokenWidth/2-1:0] test_unlock_token_lower, test_unlock_token_upper;
664 logic [LcTokenWidth/2-1:0] test_exit_token_lower, test_exit_token_upper;
665 logic [LcTokenWidth/2-1:0] rma_token_lower, rma_token_upper;
666 1/1 assign {test_unlock_token_lower, test_unlock_token_upper} = test_unlock_token_i;
Tests: T1 T3 T4
667 1/1 assign {test_exit_token_lower, test_exit_token_upper} = test_exit_token_i;
Tests: T1 T3 T4
668 1/1 assign {rma_token_lower, rma_token_upper} = rma_token_i;
Tests: T1 T3 T4
669
670 // SEC_CM: TOKEN.DIGEST
671 // This indexes the correct token, based on the transition arc.
672 // Note that we always perform a token comparison, even in case of
673 // unconditional transitions. In the case of unconditional tokens
674 // we just pass an all-zero constant through the hashing function.
675 always_comb begin : p_token_assign
676 // Set the invalid token indices to a random netlist constant, rather than all-zero.
677 1/1 {hashed_tokens_lower, hashed_tokens_upper} = RndCnstInvalidTokens;
Tests: T1 T3 T4
678 // All-zero token for unconditional transitions.
679 1/1 {hashed_tokens_lower[ZeroTokenIdx],
Tests: T1 T3 T4
680 hashed_tokens_upper[ZeroTokenIdx]} = AllZeroTokenHashed;
681 1/1 {hashed_tokens_lower[RawUnlockTokenIdx],
Tests: T1 T3 T4
682 hashed_tokens_upper[RawUnlockTokenIdx]} = RndCnstRawUnlockTokenHashed;
683 // This mux has two separate halves, steered with separately buffered life cycle signals.
684 1/1 if (lc_tx_test_true_strict(test_tokens_valid[0])) begin
Tests: T1 T3 T4
685 1/1 hashed_tokens_lower[TestUnlockTokenIdx] = test_unlock_token_lower;
Tests: T1 T3 T4
686 end
MISSING_ELSE
687 1/1 if (lc_tx_test_true_strict(test_tokens_valid[1])) begin
Tests: T1 T3 T4
688 1/1 hashed_tokens_upper[TestUnlockTokenIdx] = test_unlock_token_upper;
Tests: T1 T3 T4
689 end
MISSING_ELSE
690 // This mux has two separate halves, steered with separately buffered life cycle signals.
691 1/1 if (lc_tx_test_true_strict(test_tokens_valid[2])) begin
Tests: T1 T3 T4
692 1/1 hashed_tokens_lower[TestExitTokenIdx] = test_exit_token_lower;
Tests: T1 T3 T4
693 end
MISSING_ELSE
694 1/1 if (lc_tx_test_true_strict(test_tokens_valid[3])) begin
Tests: T1 T3 T4
695 1/1 hashed_tokens_upper[TestExitTokenIdx] = test_exit_token_upper;
Tests: T1 T3 T4
696 end
MISSING_ELSE
697 // This mux has two separate halves, steered with separately buffered life cycle signals.
698 1/1 if (lc_tx_test_true_strict(rma_token_valid[0])) begin
Tests: T1 T3 T4
699 1/1 hashed_tokens_lower[RmaTokenIdx] = rma_token_lower;
Tests: T1 T3 T4
700 end
MISSING_ELSE
701 1/1 if (lc_tx_test_true_strict(rma_token_valid[1])) begin
Tests: T1 T3 T4
702 1/1 hashed_tokens_upper[RmaTokenIdx] = rma_token_upper;
Tests: T1 T3 T4
703 end
MISSING_ELSE
704 end
705
706 // SEC_CM: TOKEN_VALID.MUX.REDUN
707 // The token valid mux is duplicated.
708 logic [TokenIdxWidth-1:0] token_idx0, token_idx1;
709 logic [2**TokenIdxWidth-1:0] hashed_tokens_valid0, hashed_tokens_valid1;
710 always_comb begin : p_token_valid_assign
711 // First mux
712 1/1 hashed_tokens_valid0 = '0;
Tests: T21 T50 T51
713 1/1 hashed_tokens_valid0[ZeroTokenIdx] = 1'b1; // always valid
Tests: T21 T50 T51
714 1/1 hashed_tokens_valid0[RawUnlockTokenIdx] = 1'b1; // always valid
Tests: T21 T50 T51
715 1/1 hashed_tokens_valid0[TestUnlockTokenIdx] = lc_tx_test_true_strict(test_tokens_valid[4]);
Tests: T21 T50 T51
716 1/1 hashed_tokens_valid0[TestExitTokenIdx] = lc_tx_test_true_strict(test_tokens_valid[5]);
Tests: T21 T50 T51
717 1/1 hashed_tokens_valid0[RmaTokenIdx] = lc_tx_test_true_strict(rma_token_valid[2]);
Tests: T21 T50 T51
718 1/1 hashed_tokens_valid0[InvalidTokenIdx] = 1'b0; // always invalid
Tests: T21 T50 T51
719 // Second mux
720 1/1 hashed_tokens_valid1 = '0;
Tests: T21 T50 T51
721 1/1 hashed_tokens_valid1[ZeroTokenIdx] = 1'b1; // always valid
Tests: T21 T50 T51
722 1/1 hashed_tokens_valid1[RawUnlockTokenIdx] = 1'b1; // always valid
Tests: T21 T50 T51
723 1/1 hashed_tokens_valid1[TestUnlockTokenIdx] = lc_tx_test_true_strict(test_tokens_valid[6]);
Tests: T21 T50 T51
724 1/1 hashed_tokens_valid1[TestExitTokenIdx] = lc_tx_test_true_strict(test_tokens_valid[7]);
Tests: T21 T50 T51
725 1/1 hashed_tokens_valid1[RmaTokenIdx] = lc_tx_test_true_strict(rma_token_valid[3]);
Tests: T21 T50 T51
726 1/1 hashed_tokens_valid1[InvalidTokenIdx] = 1'b0; // always invalid
Tests: T21 T50 T51
727 end
728
729 // SEC_CM: STATE.CONFIG.SPARSE
730 // The trans_target_i signal comes from the CSR and uses a replication encoding,
731 // hence we can use different indices of the array.
732 1/1 assign token_idx0 = (int'(dec_lc_state_o[0]) < NumLcStates &&
Tests: T1 T2 T3
733 int'(trans_target_i[0]) < NumLcStates) ?
734 TransTokenIdxMatrix[dec_lc_state_o[0]][trans_target_i[0]] :
735 InvalidTokenIdx;
736 1/1 assign token_idx1 = (int'(dec_lc_state_o[1]) < NumLcStates &&
Tests: T1 T2 T3
737 int'(trans_target_i[1]) < NumLcStates) ?
738 TransTokenIdxMatrix[dec_lc_state_o[1]][trans_target_i[1]] :
739 InvalidTokenIdx;
740 1/1 assign hashed_token_mux = {hashed_tokens_lower[token_idx0],
Tests: T1 T2 T3
741 hashed_tokens_upper[token_idx1]};
742 1/1 assign hashed_token_valid_mux = {hashed_tokens_valid0[token_idx0],
Tests: T1 T2 T3
743 hashed_tokens_valid1[token_idx1]};
744
745 // If the indices are inconsistent, we also trigger a transition error.
746 // We do not trigger an alert right away if this happens, since it could
747 // be due to an invalid value programmed to the CSRs.
748 logic trans_invalid_error;
749 1/1 assign trans_invalid_error_o = trans_invalid_error || (token_idx0 != token_idx1);
Tests: T1 T2 T3
750
751 ////////////////////////////////////////////////////////////////////
752 // Decoding and transition logic for redundantly encoded LC state //
753 ////////////////////////////////////////////////////////////////////
754
755 // This decodes the state into a format that can be exposed in the CSRs,
756 // and flags any errors in the state encoding. Errors will move the
757 // main FSM into INVALID right away.
758 lc_ctrl_state_decode u_lc_ctrl_state_decode (
759 .lc_state_valid_i ( lc_state_valid_q ),
760 .lc_state_i ( lc_state_q ),
761 .lc_cnt_i ( lc_cnt_q ),
762 .secrets_valid_i,
763 .fsm_state_i ( fsm_state_q ),
764 .dec_lc_state_o,
765 .dec_lc_id_state_o,
766 .dec_lc_cnt_o,
767 .state_invalid_error_o (state_invalid_error)
768 );
769
770 // LC transition checker logic and next state generation.
771 lc_ctrl_state_transition #(
772 .SecVolatileRawUnlockEn(SecVolatileRawUnlockEn)
773 ) u_lc_ctrl_state_transition (
774 .lc_state_i ( lc_state_q ),
775 .lc_cnt_i ( lc_cnt_q ),
776 .dec_lc_state_i ( dec_lc_state_o ),
777 .fsm_state_i ( fsm_state_q ),
778 .trans_target_i,
779 .volatile_raw_unlock_i,
780 .trans_cmd_i,
781 .next_lc_state_o ( next_lc_state ),
782 .next_lc_cnt_o ( next_lc_cnt ),
783 .trans_cnt_oflw_error_o,
784 .trans_invalid_error_o ( trans_invalid_error )
785 );
786
787 // LC signal decoder and broadcasting logic.
788 lc_ctrl_signal_decode #(
789 .RndCnstLcKeymgrDivInvalid ( RndCnstLcKeymgrDivInvalid ),
790 .RndCnstLcKeymgrDivTestUnlocked( RndCnstLcKeymgrDivTestUnlocked ),
791 .RndCnstLcKeymgrDivDev ( RndCnstLcKeymgrDivDev ),
792 .RndCnstLcKeymgrDivProduction ( RndCnstLcKeymgrDivProduction ),
793 .RndCnstLcKeymgrDivRma ( RndCnstLcKeymgrDivRma )
794 ) u_lc_ctrl_signal_decode (
795 .clk_i,
796 .rst_ni,
797 .lc_state_valid_i ( lc_state_valid_q ),
798 .lc_state_i ( lc_state_q ),
799 .secrets_valid_i,
800 .fsm_state_i ( fsm_state_q ),
801 .lc_raw_test_rma_o,
802 .lc_dft_en_o,
803 .lc_nvm_debug_en_o,
804 .lc_hw_debug_en_o,
805 .lc_cpu_en_o,
806 .lc_creator_seed_sw_rw_en_o,
807 .lc_owner_seed_sw_rw_en_o,
808 .lc_iso_part_sw_rd_en_o,
809 .lc_iso_part_sw_wr_en_o,
810 .lc_seed_hw_rd_en_o,
811 .lc_keymgr_en_o,
812 .lc_escalate_en_o,
813 .lc_keymgr_div_o
814 );
815
816
817 // Conditional signals set by main FSM.
818 prim_lc_sender u_prim_lc_sender_clk_byp_req (
819 .clk_i,
820 .rst_ni,
821 .lc_en_i(lc_clk_byp_req),
822 .lc_en_o(lc_clk_byp_req_o)
823 );
824 prim_lc_sender u_prim_lc_sender_flash_rma_req (
825 .clk_i,
826 .rst_ni,
827 .lc_en_i(lc_flash_rma_req),
828 .lc_en_o(lc_flash_rma_req_o)
829 );
830 prim_lc_sender u_prim_lc_sender_check_byp_en (
831 .clk_i,
832 .rst_ni,
833 .lc_en_i(lc_check_byp_en),
834 .lc_en_o(lc_check_byp_en_o)
835 );
836
837 ////////////////
838 // Assertions //
839 ////////////////
840
841 `ASSERT(EscStaysOnOnceAsserted_A,
842 lc_tx_test_true_strict(lc_escalate_en_o)
843 |=>
844 lc_tx_test_true_strict(lc_escalate_en_o))
845
846 `ASSERT(ClkBypStaysOnOnceAsserted_A,
847 lc_tx_test_true_strict(lc_clk_byp_req_o)
848 |=>
849 lc_tx_test_true_strict(lc_clk_byp_req_o))
850
851 `ASSERT(FlashRmaStaysOnOnceAsserted_A,
852 lc_tx_test_true_strict(lc_flash_rma_req_o)
853 |=>
854 lc_tx_test_true_strict(lc_flash_rma_req_o))
855
856 `ASSERT(NoClkBypInProdStates_A,
857 lc_state_q inside {LcStProd, LcStProdEnd, LcStDev}
858 |=>
859 lc_tx_test_false_strict(lc_clk_byp_req_o))
860
861 `ASSERT(SecCmCFITerminal0_A,
862 fsm_state_q == PostTransSt
863 |=>
864 fsm_state_q inside {PostTransSt, InvalidSt, EscalateSt})
865
866 `ASSERT(SecCmCFITerminal1_A,
867 fsm_state_q == ScrapSt
868 |=>
869 fsm_state_q inside {ScrapSt, InvalidSt, EscalateSt})
870
871 `ASSERT(SecCmCFITerminal2_A,
872 fsm_state_q == EscalateSt
873 |=>
874 fsm_state_q == EscalateSt)
875
876 `ASSERT(SecCmCFITerminal3_A,
877 fsm_state_q == InvalidSt
878 |=>
879 fsm_state_q inside {InvalidSt, EscalateSt})
880
881 // Check that the FSM is linear and does not contain any loops
882 3/3 `ASSERT_FPV_LINEAR_FSM(SecCmCFILinear_A, fsm_state_q, fsm_state_e)
Tests: T1 T2 T3 | T1 T2 T3 | T1 T2 T3
ASSERT_FPV_LINEAR_FSM(SecCmCFILinear_A, fsm_state_q, fsm_state_e):
882.1 `ifdef INC_ASSERT
882.2 bit SecCmCFILinear_A_cond;
882.3 always_ff @(posedge clk_i or posedge !rst_ni) begin
882.4 1/1 if (!rst_ni) begin
Tests: T1 T2 T3
882.5 1/1 SecCmCFILinear_A_cond <= 0;
Tests: T1 T2 T3
882.6 end else begin
882.7 1/1 SecCmCFILinear_A_cond <= 1;
Tests: T1 T2 T3
882.8 end
882.9 end
882.10 property SecCmCFILinear_A_p;
882.11 fsm_state_e initial_state;
882.12 (!$stable(fsm_state_q) & SecCmCFILinear_A_cond, initial_state = $past(fsm_state_q)) |->
882.13 (fsm_state_q != initial_state) until (!rst_ni == 1'b1);
882.14 endproperty
882.15 SecCmCFILinear_A: assert property (@(posedge clk_i) disable iff ((0) !== '0) (SecCmCFILinear_A_p))
882.16 else begin
882.17 `ifdef UVM
882.18 uvm_pkg::uvm_report_error("ASSERT FAILED", "SecCmCFILinear_A", uvm_pkg::UVM_NONE,
882.19 "../src/lowrisc_ip_lc_ctrl_0.1/rtl/lc_ctrl_fsm.sv", 882, "", 1);
882.20 `else
882.21 $error("%0t: (%0s:%0d) [%m] [ASSERT FAILED] %0s", $time, `__FILE__, `__LINE__,
882.22 `PRIM_STRINGIFY(SecCmCFILinear_A));
882.23 `endif
882.24 end
882.25 `endif