Module Definition
dashboard | hierarchy | modlist | groups | tests | asserts



Module Instance : tb.dut.i_ping_timer.i_prim_lfsr

Instance :
SCORELINECONDTOGGLEFSMBRANCHASSERT
77.54 95.65 55.00 66.67 92.86


Instance's subtree :
SCORELINECONDTOGGLEFSMBRANCHASSERT
77.54 95.65 55.00 66.67 92.86


Parent :
SCORELINECONDTOGGLEFSMBRANCHASSERTNAME
94.57 100.00 100.00 80.00 92.86 100.00 i_ping_timer


Subtrees :
NAMESCORELINECONDTOGGLEFSMBRANCHASSERT
no children


Since this is the module's only instance, the coverage report is the same as for the module.
Line Coverage for Module : prim_lfsr
Line No.TotalCoveredPercent
TOTAL232295.65
CONT_ASSIGN31511100.00
CONT_ASSIGN31811100.00
CONT_ASSIGN36111100.00
CONT_ASSIGN36611100.00
ALWAYS36933100.00
ROUTINE3929888.89
CONT_ASSIGN46311100.00
CONT_ASSIGN46811100.00
ALWAYS47155100.00

314 // calculate next state using internal XOR feedback and entropy input 315 1/1 assign next_lfsr_state = LfsrDw'(entropy_i) ^ ({LfsrDw{lfsr_q[0]}} & coeffs) ^ (lfsr_q >> 1); 316 317 // lockup condition is all-zero 318 1/1 assign lockup = ~(|lfsr_q); 319 320 // check that seed is not all-zero 321 `ASSERT_INIT(DefaultSeedNzCheck_A, |DefaultSeed) 322 323 324 //////////////////// 325 // Fibonacci XNOR // 326 //////////////////// 327 end else if (64'(LfsrType) == "FIB_XNOR") begin : gen_fib_xnor 328 329 // if custom polynomial is provided 330 if (CustomCoeffs > 0) begin : gen_custom 331 assign coeffs = CustomCoeffs[LfsrDw-1:0]; 332 end else begin : gen_lut 333 assign coeffs = FIB_XNOR_COEFFS[LfsrDw-FIB_XNOR_LUT_OFF][LfsrDw-1:0]; 334 // check that the most significant bit of polynomial is 1 335 `ASSERT_INIT(MinLfsrWidth_A, LfsrDw >= $low(FIB_XNOR_COEFFS)+FIB_XNOR_LUT_OFF) 336 `ASSERT_INIT(MaxLfsrWidth_A, LfsrDw <= $high(FIB_XNOR_COEFFS)+FIB_XNOR_LUT_OFF) 337 end 338 339 // calculate next state using external XNOR feedback and entropy input 340 assign next_lfsr_state = LfsrDw'(entropy_i) ^ {lfsr_q[LfsrDw-2:0], ~(^(lfsr_q & coeffs))}; 341 342 // lockup condition is all-ones 343 assign lockup = &lfsr_q; 344 345 // check that seed is not all-ones 346 `ASSERT_INIT(DefaultSeedNzCheck_A, !(&DefaultSeed)) 347 348 349 ///////////// 350 // Unknown // 351 ///////////// 352 end else begin : gen_unknown_type 353 `ASSERT_INIT(UnknownLfsrType_A, 0) 354 end 355 356 357 ////////////////// 358 // Shared logic // 359 ////////////////// 360 361 1/1 assign lfsr_d = (seed_en_i) ? seed_i : 362 (lfsr_en_i && lockup) ? DefaultSeed : 363 (lfsr_en_i) ? next_lfsr_state : 364 lfsr_q; 365 366 1/1 assign state_o = lfsr_q[StateOutDw-1:0]; 367 368 always_ff @(posedge clk_i or negedge rst_ni) begin : p_reg 369 1/1 if (!rst_ni) begin 370 1/1 lfsr_q <= DefaultSeed; 371 end else begin 372 1/1 lfsr_q <= lfsr_d; 373 end 374 end 375 376 377 /////////////////////// 378 // shared assertions // 379 /////////////////////// 380 381 `ASSERT_KNOWN(DataKnownO_A, state_o) 382 383 // the code below is not meant to be synthesized, 384 // but it is intended to be used in simulation and FPV 385 `ifndef SYNTHESIS 386 function automatic logic[LfsrDw-1:0] compute_next_state(logic[LfsrDw-1:0] lfsrcoeffs, 387 logic[EntropyDw-1:0] entropy, 388 logic[LfsrDw-1:0] state); 389 logic state0; 390 391 // Galois XOR 392 1/1 if (64'(LfsrType) == 64'("GAL_XOR")) begin 393 1/1 if (state == 0) begin 394 0/1 ==> state = DefaultSeed; 395 end else begin 396 1/1 state0 = state[0]; 397 1/1 state = state >> 1; 398 2/2 if (state0) state ^= lfsrcoeffs; MISSING_ELSE 399 1/1 state ^= LfsrDw'(entropy); 400 end 401 // Fibonacci XNOR 402 unreachable end else if (64'(LfsrType) == "FIB_XNOR") begin 403 unreachable if (&state) begin 404 unreachable state = DefaultSeed; 405 end else begin 406 unreachable state0 = ~(^(state & lfsrcoeffs)); 407 unreachable state = state << 1; 408 unreachable state[0] = state0; 409 unreachable state ^= LfsrDw'(entropy); 410 end 411 end else begin 412 unreachable $error("unknown lfsr type"); 413 end 414 415 1/1 return state; 416 endfunction : compute_next_state 417 418 // check whether next state is computed correctly 419 `ASSERT(NextStateCheck_A, lfsr_en_i && !seed_en_i |=> lfsr_q == 420 compute_next_state(coeffs, $past(entropy_i,1), $past(lfsr_q,1))) 421 `endif 422 423 `ASSERT_INIT(InputWidth_A, LfsrDw >= EntropyDw) 424 `ASSERT_INIT(OutputWidth_A, LfsrDw >= StateOutDw) 425 426 // MSB must be one in any case 427 `ASSERT(CoeffCheck_A, coeffs[LfsrDw-1]) 428 429 // output check 430 `ASSERT_KNOWN(OutputKnown_A, state_o) 431 `ASSERT(OutputCheck_A, state_o == StateOutDw'(lfsr_q)) 432 433 // if no external input changes the lfsr state, a lockup must not occur (by design) 434 //`ASSERT(NoLockups_A, (!entropy_i) && (!seed_en_i) |=> !lockup, clk_i, !rst_ni) 435 `ASSERT(NoLockups_A, lfsr_en_i && !entropy_i && !seed_en_i |=> !lockup) 436 437 // this can be disabled if unused in order to not distort coverage 438 if (ExtSeedSVA) begin : gen_ext_seed_sva 439 // check that external seed is correctly loaded into the state 440 // rst_ni is used directly as part of the pre-condition since the usage of rst_ni 441 // in disable_iff is unsampled. See #1985 for more details 442 `ASSERT(ExtDefaultSeedInputCheck_A, (seed_en_i && rst_ni) |=> lfsr_q == $past(seed_i)) 443 end 444 445 // if the external seed mechanism is not used, 446 // there is theoretically no way we end up in a lockup condition 447 // in order to not distort coverage, this SVA can be disabled in such cases 448 if (LockupSVA) begin : gen_lockup_mechanism_sva 449 // check that a stuck LFSR is correctly reseeded 450 `ASSERT(LfsrLockupCheck_A, lfsr_en_i && lockup && !seed_en_i |=> !lockup) 451 end 452 453 if (MaxLenSVA) begin : gen_max_len_sva 454 455 `ifndef SYNTHESIS 456 // the code below is a workaround to enable long sequences to be checked. 457 // some simulators do not support SVA sequences longer than 2**32-1. 458 logic [LfsrDw-1:0] cnt_d, cnt_q; 459 logic perturbed_d, perturbed_q; 460 logic [LfsrDw-1:0] cmp_val; 461 462 assign cmp_val = {{(LfsrDw-1){1'b1}}, 1'b0}; // 2**LfsrDw-2 463 1/1 assign cnt_d = (lfsr_en_i && lockup) ? '0 : 464 (lfsr_en_i && (cnt_q == cmp_val)) ? '0 : 465 (lfsr_en_i) ? cnt_q + 1'b1 : 466 cnt_q; 467 468 1/1 assign perturbed_d = perturbed_q | (|entropy_i) | seed_en_i; 469 470 always_ff @(posedge clk_i or negedge rst_ni) begin : p_max_len 471 1/1 if (!rst_ni) begin 472 1/1 cnt_q <= '0; 473 1/1 perturbed_q <= 1'b0; 474 end else begin 475 1/1 cnt_q <= cnt_d; 476 1/1 perturbed_q <= perturbed_d;

Cond Coverage for Module : prim_lfsr
TotalCoveredPercent
Conditions201155.00
Logical201155.00
Non-Logical00
Event00

 LINE       361
 EXPRESSION (seed_en_i ? seed_i : ((lfsr_en_i && lockup) ? DefaultSeed : (lfsr_en_i ? next_lfsr_state : lfsr_q)))
             ----1----
-1-Status
0Covered
1Unreachable

 LINE       361
 SUB-EXPRESSION ((lfsr_en_i && lockup) ? DefaultSeed : (lfsr_en_i ? next_lfsr_state : lfsr_q))
                 ----------1----------
-1-Status
0Covered
1Not Covered

 LINE       361
 SUB-EXPRESSION (lfsr_en_i && lockup)
                 ----1----    ---2--
-1--2-Status
01Not Covered
10Covered
11Not Covered

 LINE       361
 SUB-EXPRESSION (lfsr_en_i ? next_lfsr_state : lfsr_q)
                 ----1----
-1-Status
0Covered
1Covered

 LINE       463
 EXPRESSION 
 Number  Term
      1  (lfsr_en_i && lockup) ? '0 : ((lfsr_en_i && (gen_max_len_sva.cnt_q == gen_max_len_sva.cmp_val)) ? '0 : (lfsr_en_i ? ((gen_max_len_sva.cnt_q + 1'b1)) : gen_max_len_sva.cnt_q)))
-1-Status
0Covered
1Not Covered

 LINE       463
 SUB-EXPRESSION (lfsr_en_i && lockup)
                 ----1----    ---2--
-1--2-Status
01Not Covered
10Covered
11Not Covered

 LINE       463
 SUB-EXPRESSION ((lfsr_en_i && (gen_max_len_sva.cnt_q == gen_max_len_sva.cmp_val)) ? '0 : (lfsr_en_i ? ((gen_max_len_sva.cnt_q + 1'b1)) : gen_max_len_sva.cnt_q))
                 --------------------------------1--------------------------------
-1-Status
0Covered
1Not Covered

 LINE       463
 SUB-EXPRESSION (lfsr_en_i && (gen_max_len_sva.cnt_q == gen_max_len_sva.cmp_val))
                 ----1----    -------------------------2------------------------
-1--2-Status
01Not Covered
10Covered
11Not Covered

 LINE       463
 SUB-EXPRESSION (lfsr_en_i ? ((gen_max_len_sva.cnt_q + 1'b1)) : gen_max_len_sva.cnt_q)
                 ----1----
-1-Status
0Covered
1Covered

Branch Coverage for Module : prim_lfsr
Line No.TotalCoveredPercent
Branches 12 8 66.67
TERNARY 361 4 2 50.00
TERNARY 463 4 2 50.00
IF 369 2 2 100.00
IF 471 2 2 100.00


361 assign lfsr_d = (seed_en_i) ? seed_i : -1- ==> 362 (lfsr_en_i && lockup) ? DefaultSeed : -2- ==> 363 (lfsr_en_i) ? next_lfsr_state : -3- ==> ==>

Branches:
-1--2--3-Status
1 - - Not Covered
0 1 - Not Covered
0 0 1 Covered
0 0 0 Covered


463 assign cnt_d = (lfsr_en_i && lockup) ? '0 : -1- ==> 464 (lfsr_en_i && (cnt_q == cmp_val)) ? '0 : -2- ==> 465 (lfsr_en_i) ? cnt_q + 1'b1 : -3- ==> ==>

Branches:
-1--2--3-Status
1 - - Not Covered
0 1 - Not Covered
0 0 1 Covered
0 0 0 Covered


369 if (!rst_ni) begin -1- 370 lfsr_q <= DefaultSeed; ==> 371 end else begin 372 lfsr_q <= lfsr_d; ==>

Branches:
-1-Status
1 Covered
0 Covered


471 if (!rst_ni) begin -1- 472 cnt_q <= '0; ==> 473 perturbed_q <= 1'b0; 474 end else begin 475 cnt_q <= cnt_d; ==>

Branches:
-1-Status
1 Covered
0 Covered


Assert Coverage for Module : prim_lfsr
TotalAttemptedPercentSucceeded/MatchedPercent
Assertions 14 14 100.00 13 92.86
Cover properties 0 0 0
Cover sequences 0 0 0
Total 14 14 100.00 13 92.86




Assertion Details

NameAttemptsReal SuccessesFailuresIncomplete
CoeffCheck_A 2147483647 2147483647 0 0
DataKnownO_A 2147483647 2147483647 0 0
InputWidth_A 919 919 0 0
NextStateCheck_A 2147483647 1035 0 0
NoLockups_A 2147483647 508 0 0
OutputCheck_A 2147483647 2147483647 0 0
OutputKnown_A 2147483647 2147483647 0 0
OutputWidth_A 919 919 0 0
gen_gal_xor.DefaultSeedNzCheck_A 919 919 0 0
gen_gal_xor.gen_lut.MaxLfsrWidth_A 919 919 0 0
gen_gal_xor.gen_lut.MinLfsrWidth_A 919 919 0 0
gen_lockup_mechanism_sva.LfsrLockupCheck_A 2147483647 0 0 0
gen_max_len_sva.MaximalLengthCheck0_A 2147483647 84350249 0 0
gen_max_len_sva.MaximalLengthCheck1_A 2147483647 179304 0 0

0% 10% 20% 30% 40% 50% 60% 70% 80% 90% 100%