Unified Coverage Report :: Module :: prim_lfsr

Module : prim_lfsr

SCORE	LINE	COND	TOGGLE	FSM	BRANCH	ASSERT
98.31	100.00	96.55	100.00		100.00	95.00

Source File(s) :
/workspaces/repo/scratch/os_regression_2024_08_31/prim_lfsr-sim-vcs/prim_lfsr_dw_8_gal/sim-vcs/../src/lowrisc_prim_lfsr_0.1/rtl/prim_lfsr.sv

Module self-instances :

NAME	SCORE	LINE	COND	TOGGLE	FSM	BRANCH	ASSERT
prim_lfsr_tb.gen_duts[8].i_prim_lfsr	98.31	100.00	96.55	100.00		100.00	95.00

---

Module Instance : prim_lfsr_tb.gen_duts[8].i_prim_lfsr

Instance :

SCORE	LINE	COND	TOGGLE	FSM	BRANCH	ASSERT
98.31	100.00	96.55	100.00		100.00	95.00

Instance's subtree :

SCORE	LINE	COND	TOGGLE	FSM	BRANCH	ASSERT
98.31	100.00	96.55	100.00		100.00	95.00

Parent :

SCORE	LINE	COND	TOGGLE	FSM	BRANCH	ASSERT	NAME
							prim_lfsr_tb

Subtrees :

NAME	SCORE	LINE	COND	TOGGLE	FSM	BRANCH	ASSERT
no children

Line Coverage for Module : prim_lfsr

	Line No.	Total	Covered	Percent
TOTAL		32	32	100.00
CONT_ASSIGN	296	1	1	100.00
CONT_ASSIGN	299	1	1	100.00
CONT_ASSIGN	345	1	1	100.00
CONT_ASSIGN	465	1	1	100.00
CONT_ASSIGN	472	1	1	100.00
CONT_ASSIGN	472	1	1	100.00
CONT_ASSIGN	472	1	1	100.00
CONT_ASSIGN	472	1	1	100.00
CONT_ASSIGN	472	1	1	100.00
CONT_ASSIGN	472	1	1	100.00
CONT_ASSIGN	472	1	1	100.00
CONT_ASSIGN	472	1	1	100.00
ALWAYS	487	3	3	100.00
ROUTINE	510	10	10	100.00
CONT_ASSIGN	610	1	1	100.00
CONT_ASSIGN	615	1	1	100.00
ALWAYS	618	5	5	100.00

295                         // calculate next state using internal XOR feedback and entropy input
296        1/1              assign next_lfsr_state = LfsrDw'(entropy_i) ^ ({LfsrDw{lfsr_q[0]}} & coeffs) ^ (lfsr_q >> 1);
           Tests:       T1 T2 T3 
297                     
298                         // lockup condition is all-zero
299        1/1              assign lockup = ~(|lfsr_q);
           Tests:       T1 T2 T3 
300                     
301                         // check that seed is not all-zero
302                         `ASSERT_INIT(DefaultSeedNzCheck_A, |DefaultSeedLocal)
303                     
304                     
305                       ////////////////////
306                       // Fibonacci XNOR //
307                       ////////////////////
308                       end else if (64'(LfsrType) == "FIB_XNOR") begin : gen_fib_xnor
309                     
310                         // if custom polynomial is provided
311                         if (CustomCoeffs > 0) begin : gen_custom
312                           assign coeffs = CustomCoeffs[LfsrDw-1:0];
313                         end else begin : gen_lut
314                           assign coeffs = LFSR_COEFFS[LfsrDw-LUT_OFF][LfsrDw-1:0];
315                           // check that the most significant bit of polynomial is 1
316                           `ASSERT_INIT(MinLfsrWidth_A, LfsrDw >= $low(LFSR_COEFFS)+LUT_OFF)
317                           `ASSERT_INIT(MaxLfsrWidth_A, LfsrDw <= $high(LFSR_COEFFS)+LUT_OFF)
318                         end
319                     
320                         // calculate next state using external XNOR feedback and entropy input
321                         assign next_lfsr_state = LfsrDw'(entropy_i) ^ {lfsr_q[LfsrDw-2:0], ~(^(lfsr_q & coeffs))};
322                     
323                         // lockup condition is all-ones
324                         assign lockup = &lfsr_q;
325                     
326                         // check that seed is not all-ones
327                         `ASSERT_INIT(DefaultSeedNzCheck_A, !(&DefaultSeedLocal))
328                     
329                     
330                       /////////////
331                       // Unknown //
332                       /////////////
333                       end else begin : gen_unknown_type
334                         assign coeffs = '0;
335                         assign next_lfsr_state = '0;
336                         assign lockup = 1'b0;
337                         `ASSERT_INIT(UnknownLfsrType_A, 0)
338                       end
339                     
340                     
341                       //////////////////
342                       // Shared logic //
343                       //////////////////
344                     
345        1/1            assign lfsr_d = (seed_en_i)           ? seed_i          :
           Tests:       T1 T2 T3 
346                                       (lfsr_en_i && lockup) ? DefaultSeedLocal     :
347                                       (lfsr_en_i)           ? next_lfsr_state :
348                                                               lfsr_q;
349                     
350                       logic [LfsrDw-1:0] sbox_out;
351                       if (NonLinearOut) begin : gen_out_non_linear
352                         // The "aligned" permutation ensures that adjacent bits do not go into the same SBox. It is
353                         // different from the state permutation that can be specified via the StatePerm parameter. The
354                         // permutation taps out 4 SBox input bits at regular stride intervals. E.g., for a 16bit
355                         // vector, the input assignment looks as follows:
356                         //
357                         // SBox0: 0,  4,  8, 12
358                         // SBox1: 1,  5,  9, 13
359                         // SBox2: 2,  6, 10, 14
360                         // SBox3: 3,  7, 11, 15
361                         //
362                         // Note that this permutation can be produced by filling the input vector into matrix columns
363                         // and reading out the SBox inputs as matrix rows.
364                         localparam int NumSboxes = LfsrDw / 4;
365                         // Fill in the input vector in col-major order.
366                         logic [3:0][NumSboxes-1:0][LfsrIdxDw-1:0] matrix_indices;
367                         for (genvar j = 0; j < LfsrDw; j++) begin : gen_input_idx_map
368                           assign matrix_indices[j / NumSboxes][j % NumSboxes] = j;
369                         end
370                         // Due to the LFSR shifting pattern, the above permutation has the property that the output of
371                         // SBox(n) is going to be equal to SBox(n+1) in the subsequent cycle (unless the LFSR polynomial
372                         // modifies some of the associated shifted bits via an XOR tap).
373                         // We therefore tweak this permutation by rotating and reversing some of the assignment matrix
374                         // columns. The rotation and reversion operations have been chosen such that this
375                         // generalizes to all power of two widths supported by the LFSR primitive. For 16bit, this
376                         // looks as follows:
377                         //
378                         // SBox0: 0,  6, 11, 14
379                         // SBox1: 1,  7, 10, 13
380                         // SBox2: 2,  4,  9, 12
381                         // SBox3: 3,  5,  8, 15
382                         //
383                         // This can be achieved by:
384                         //   1) down rotating the second column by NumSboxes/2
385                         //   2) reversing the third column
386                         //   3) down rotating the fourth column by 1 and reversing it
387                         //
388                         logic [3:0][NumSboxes-1:0][LfsrIdxDw-1:0] matrix_rotrev_indices;
389                         typedef logic [NumSboxes-1:0][LfsrIdxDw-1:0] matrix_col_t;
390                     
391                         // left-rotates a matrix column by the shift amount
392                         function automatic matrix_col_t lrotcol(matrix_col_t col, integer shift);
393                           matrix_col_t out;
394                           for (int k = 0; k < NumSboxes; k++) begin
395                             out[(k + shift) % NumSboxes] = col[k];
396                           end
397                           return out;
398                         endfunction : lrotcol
399                     
400                         // reverses a matrix column
401                         function automatic matrix_col_t revcol(matrix_col_t col);
402                           return {<<LfsrIdxDw{col}};
403                         endfunction : revcol
404                     
405                         always_comb begin : p_rotrev
406                           matrix_rotrev_indices[0] = matrix_indices[0];
407                           matrix_rotrev_indices[1] = lrotcol(matrix_indices[1], NumSboxes/2);
408                           matrix_rotrev_indices[2] = revcol(matrix_indices[2]);
409                           matrix_rotrev_indices[3] = revcol(lrotcol(matrix_indices[3], 1));
410                         end
411                     
412                         // Read out the matrix rows and linearize.
413                         logic [LfsrDw-1:0][LfsrIdxDw-1:0] sbox_in_indices;
414                         for (genvar k = 0; k < LfsrDw; k++) begin : gen_reverse_upper
415                           assign sbox_in_indices[k] = matrix_rotrev_indices[k % 4][k / 4];
416                         end
417                     
418                     `ifndef SYNTHESIS
419                           // Check that the permutation is indeed a permutation.
420                           logic [LfsrDw-1:0] sbox_perm_test;
421                           always_comb begin : p_perm_check
422                             sbox_perm_test = '0;
423                             for (int k = 0; k < LfsrDw; k++) begin
424                               sbox_perm_test[sbox_in_indices[k]] = 1'b1;
425                             end
426                           end
427                           // All bit positions must be marked with 1.
428                           `ASSERT(SboxPermutationCheck_A, &sbox_perm_test)
429                     `endif
430                     
431                     `ifdef FPV_ON
432                           // Verify that the permutation indeed breaks linear shifting patterns of 4bit input groups.
433                           // The symbolic variables let the FPV tool select all sbox index combinations and linear shift
434                           // offsets.
435                           int shift;
436                           int unsigned sk, sj;
437                           `ASSUME(SjSkRange_M, (sj < NumSboxes) && (sk < NumSboxes))
438                           `ASSUME(SjSkDifferent_M, sj != sk)
439                           `ASSUME(SjSkStable_M, ##1 $stable(sj) && $stable(sk) && $stable(shift))
440                           `ASSERT(SboxInputIndexGroupIsUnique_A,
441                               !((((sbox_in_indices[sj * 4 + 0] + shift) % LfsrDw) == sbox_in_indices[sk * 4 + 0]) &&
442                                 (((sbox_in_indices[sj * 4 + 1] + shift) % LfsrDw) == sbox_in_indices[sk * 4 + 1]) &&
443                                 (((sbox_in_indices[sj * 4 + 2] + shift) % LfsrDw) == sbox_in_indices[sk * 4 + 2]) &&
444                                 (((sbox_in_indices[sj * 4 + 3] + shift) % LfsrDw) == sbox_in_indices[sk * 4 + 3])))
445                     
446                           // this checks that the permutations does not preserve neighboring bit positions.
447                           // i.e. no two neighboring bits are mapped to neighboring bit positions.
448                           int y;
449                           int unsigned ik;
450                           `ASSUME(IkYRange_M, (ik < LfsrDw) && (y == 1 || y == -1))
451                           `ASSUME(IkStable_M, ##1 $stable(ik) && $stable(y))
452                           `ASSERT(IndicesNotAdjacent_A, (sbox_in_indices[ik] - sbox_in_indices[(ik + y) % LfsrDw]) != 1)
453                     `endif
454                     
455                         // Use the permutation indices to create the SBox layer
456                         for (genvar k = 0; k < NumSboxes; k++) begin : gen_sboxes
457                           logic [3:0] sbox_in;
458                           assign sbox_in = {lfsr_q[sbox_in_indices[k*4 + 3]],
459                                             lfsr_q[sbox_in_indices[k*4 + 2]],
460                                             lfsr_q[sbox_in_indices[k*4 + 1]],
461                                             lfsr_q[sbox_in_indices[k*4 + 0]]};
462                           assign sbox_out[k*4 +: 4] = prim_cipher_pkg::PRINCE_SBOX4[sbox_in];
463                         end
464                       end else begin : gen_out_passthru
465        1/1              assign sbox_out = lfsr_q;
           Tests:       T1 T2 T3 
466                       end
467                     
468                       // Random output permutation, defined at compile time
469                       if (StatePermEn) begin : gen_state_perm
470                     
471                         for (genvar k = 0; k < StateOutDw; k++) begin : gen_perm_loop
472        8/8                assign state_o[k] = sbox_out[StatePerm[k]];
           Tests:       T1 T2 T3  | T1 T2 T3  | T1 T2 T3  | T1 T2 T3  | T1 T2 T3  | T1 T2 T3  | T1 T2 T3  | T1 T2 T3 
473                         end
474                     
475                         // if lfsr width is greater than the output, then by definition
476                         // not every bit will be picked
477                         if (LfsrDw > StateOutDw) begin : gen_tieoff_unused
478                           logic unused_sbox_out;
479                           assign unused_sbox_out = ^sbox_out;
480                         end
481                     
482                       end else begin : gen_no_state_perm
483                         assign state_o = StateOutDw'(sbox_out);
484                       end
485                     
486                       always_ff @(posedge clk_i or negedge rst_ni) begin : p_reg
487        1/1              if (!rst_ni) begin
           Tests:       T1 T2 T3 
488        1/1                lfsr_q <= DefaultSeedLocal;
           Tests:       T1 T2 T3 
489                         end else begin
490        1/1                lfsr_q <= lfsr_d;
           Tests:       T1 T2 T3 
491                         end
492                       end
493                     
494                     
495                       ///////////////////////
496                       // shared assertions //
497                       ///////////////////////
498                     
499                       `ASSERT_KNOWN(DataKnownO_A, state_o)
500                     
501                     // the code below is not meant to be synthesized,
502                     // but it is intended to be used in simulation and FPV
503                     `ifndef SYNTHESIS
504                       function automatic logic [LfsrDw-1:0] compute_next_state(logic [LfsrDw-1:0]    lfsrcoeffs,
505                                                                                logic [EntropyDw-1:0] entropy,
506                                                                                logic [LfsrDw-1:0]    current_state);
507                         logic state0;
508                         logic [LfsrDw-1:0] next_state;
509                     
510        1/1              next_state = current_state;
           Tests:       T1 T2 T3 
511                     
512                         // Galois XOR
513        1/1              if (64'(LfsrType) == 64'("GAL_XOR")) begin
           Tests:       T1 T2 T3 
514        1/1                if (next_state == 0) begin
           Tests:       T1 T2 T3 
515        1/1                  next_state = DefaultSeedLocal;
           Tests:       T1 T2 T3 
516                           end else begin
517        1/1                  state0 = next_state[0];
           Tests:       T1 T2 T3 
518        1/1                  next_state = next_state >> 1;
           Tests:       T1 T2 T3 
519        2/2                  if (state0) next_state ^= lfsrcoeffs;
           Tests:       T1 T2 T3  | T1 T2 T3 
                        MISSING_ELSE
520        1/1                  next_state ^= LfsrDw'(entropy);
           Tests:       T1 T2 T3 
521                           end
522                         // Fibonacci XNOR
523        unreachable      end else if (64'(LfsrType) == "FIB_XNOR") begin
524        unreachable        if (&next_state) begin
525        unreachable          next_state = DefaultSeedLocal;
526                           end else begin
527        unreachable          state0 = ~(^(next_state & lfsrcoeffs));
528        unreachable          next_state = next_state << 1;
529        unreachable          next_state[0] = state0;
530        unreachable          next_state ^= LfsrDw'(entropy);
531                           end
532                         end else begin
533        unreachable        $error("unknown lfsr type");
534                         end
535                     
536        1/1              return next_state;
           Tests:       T1 T2 T3 
537                       endfunction : compute_next_state
538                     
539                       // check whether next state is computed correctly
540                       // we shift the assertion by one clock cycle (##1) in order to avoid
541                       // erroneous SVA triggers right after reset deassertion in cases where
542                       // the precondition is true throughout the reset.
543                       // this can happen since the disable_iff evaluates using unsampled values,
544                       // meaning that the assertion may already read rst_ni == 1 on an active
545                       // clock edge while the flops in the design have not yet changed state.
546                       `ASSERT(NextStateCheck_A, ##1 lfsr_en_i && !seed_en_i |=> lfsr_q ==
547                           compute_next_state(coeffs, $past(entropy_i), $past(lfsr_q)))
548                     
549                       // Only check this if enabled.
550                       if (StatePermEn) begin : gen_perm_check
551                         // Check that the supplied permutation is valid.
552                         logic [LfsrDw-1:0] lfsr_perm_test;
553                         initial begin : p_perm_check
554                           lfsr_perm_test = '0;
555                           for (int k = 0; k < LfsrDw; k++) begin
556                             lfsr_perm_test[StatePerm[k]] = 1'b1;
557                           end
558                           // All bit positions must be marked with 1.
559                           `ASSERT_I(PermutationCheck_A, &lfsr_perm_test)
560                         end
561                       end
562                     
563                     `endif
564                     
565                       `ASSERT_INIT(InputWidth_A, LfsrDw >= EntropyDw)
566                       `ASSERT_INIT(OutputWidth_A, LfsrDw >= StateOutDw)
567                     
568                       // MSB must be one in any case
569                       `ASSERT(CoeffCheck_A, coeffs[LfsrDw-1])
570                     
571                       // output check
572                       `ASSERT_KNOWN(OutputKnown_A, state_o)
573                       if (!StatePermEn && !NonLinearOut) begin : gen_output_sva
574                         `ASSERT(OutputCheck_A, state_o == StateOutDw'(lfsr_q))
575                       end
576                       // if no external input changes the lfsr state, a lockup must not occur (by design)
577                       //`ASSERT(NoLockups_A, (!entropy_i) && (!seed_en_i) |=> !lockup, clk_i, !rst_ni)
578                       `ASSERT(NoLockups_A, lfsr_en_i && !entropy_i && !seed_en_i |=> !lockup)
579                     
580                       // this can be disabled if unused in order to not distort coverage
581                       if (ExtSeedSVA) begin : gen_ext_seed_sva
582                         // check that external seed is correctly loaded into the state
583                         // rst_ni is used directly as part of the pre-condition since the usage of rst_ni
584                         // in disable_iff is unsampled.  See #1985 for more details
585                         `ASSERT(ExtDefaultSeedInputCheck_A, (seed_en_i && rst_ni) |=> lfsr_q == $past(seed_i))
586                       end
587                     
588                       // if the external seed mechanism is not used,
589                       // there is theoretically no way we end up in a lockup condition
590                       // in order to not distort coverage, this SVA can be disabled in such cases
591                       if (LockupSVA) begin : gen_lockup_mechanism_sva
592                         // check that a stuck LFSR is correctly reseeded
593                         `ASSERT(LfsrLockupCheck_A, lfsr_en_i && lockup && !seed_en_i |=> !lockup)
594                       end
595                     
596                       // If non-linear output requested, the LFSR width must be a power of 2 and greater than 16.
597                       if(NonLinearOut) begin : gen_nonlinear_align_check_sva
598                         `ASSERT_INIT(SboxByteAlign_A, 2**$clog2(LfsrDw) == LfsrDw && LfsrDw >= 16)
599                       end
600                     
601                       if (MaxLenSVA) begin : gen_max_len_sva
602                     `ifndef SYNTHESIS
603                         // the code below is a workaround to enable long sequences to be checked.
604                         // some simulators do not support SVA sequences longer than 2**32-1.
605                         logic [LfsrDw-1:0] cnt_d, cnt_q;
606                         logic perturbed_d, perturbed_q;
607                         logic [LfsrDw-1:0] cmp_val;
608                     
609                         assign cmp_val = {{(LfsrDw-1){1'b1}}, 1'b0}; // 2**LfsrDw-2
610        1/1              assign cnt_d = (lfsr_en_i && lockup)             ? '0           :
           Tests:       T1 T2 T3 
611                                        (lfsr_en_i && (cnt_q == cmp_val)) ? '0           :
612                                        (lfsr_en_i)                       ? cnt_q + 1'b1 :
613                                                                            cnt_q;
614                     
615        1/1              assign perturbed_d = perturbed_q | (|entropy_i) | seed_en_i;
           Tests:       T1 T2 T3 
616                     
617                         always_ff @(posedge clk_i or negedge rst_ni) begin : p_max_len
618        1/1                if (!rst_ni) begin
           Tests:       T1 T2 T3 
619        1/1                  cnt_q       <= '0;
           Tests:       T1 T2 T3 
620        1/1                  perturbed_q <= 1'b0;
           Tests:       T1 T2 T3 
621                           end else begin
622        1/1                  cnt_q       <= cnt_d;
           Tests:       T1 T2 T3 
623        1/1                  perturbed_q <= perturbed_d;
           Tests:       T1 T2 T3 

---

Cond Coverage for Module : prim_lfsr

	Total	Covered	Percent
Conditions	29	28	96.55
Logical	29	28	96.55
Non-Logical	0	0
Event	0	0

 LINE       345
 EXPRESSION (seed_en_i ? seed_i : ((lfsr_en_i && lockup) ? DefaultSeedLocal : (lfsr_en_i ? next_lfsr_state : lfsr_q)))
             ----1----

-1-	Status	Tests
0	Covered	T1,T2,T3
1	Covered	T1,T2,T3

 LINE       345
 SUB-EXPRESSION ((lfsr_en_i && lockup) ? DefaultSeedLocal : (lfsr_en_i ? next_lfsr_state : lfsr_q))
                 ----------1----------

-1-	Status	Tests
0	Covered	T1,T2,T3
1	Covered	T1,T2,T3

 LINE       345
 SUB-EXPRESSION (lfsr_en_i && lockup)
                 ----1----    ---2--

-1-	-2-	Status	Tests
0	1	Covered	T1,T2,T3
1	0	Covered	T1,T2,T3
1	1	Covered	T1,T2,T3

 LINE       345
 SUB-EXPRESSION (lfsr_en_i ? next_lfsr_state : lfsr_q)
                 ----1----

-1-	Status	Tests
0	Covered	T1,T2,T3
1	Covered	T1,T2,T3

 LINE       514
 EXPRESSION (next_state == 8'b0)
            ----------1---------

-1-	Status	Tests
0	Covered	T1,T2,T3
1	Covered	T1,T2,T3

 LINE       610
 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	Tests
0	Covered	T1,T2,T3
1	Covered	T1,T2,T3

 LINE       610
 SUB-EXPRESSION (lfsr_en_i && lockup)
                 ----1----    ---2--

-1-	-2-	Status	Tests
0	1	Covered	T1,T2,T3
1	0	Covered	T1,T2,T3
1	1	Covered	T1,T2,T3

 LINE       610
 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	Tests
0	Covered	T1,T2,T3
1	Covered	T1,T2,T3

 LINE       610
 SUB-EXPRESSION (lfsr_en_i && (gen_max_len_sva.cnt_q == gen_max_len_sva.cmp_val))
                 ----1----    -------------------------2------------------------

-1-	-2-	Status	Tests
0	1	Not Covered
1	0	Covered	T1,T2,T3
1	1	Covered	T1,T2,T3

 LINE       610
 SUB-EXPRESSION (gen_max_len_sva.cnt_q == gen_max_len_sva.cmp_val)
                -------------------------1------------------------

-1-	Status	Tests
0	Covered	T1,T2,T3
1	Covered	T1,T2,T3

 LINE       610
 SUB-EXPRESSION (lfsr_en_i ? ((gen_max_len_sva.cnt_q + 1'b1)) : gen_max_len_sva.cnt_q)
                 ----1----

-1-	Status	Tests
0	Covered	T1,T2,T3
1	Covered	T1,T2,T3

 LINE       615
 EXPRESSION (gen_max_len_sva.perturbed_q | ((|entropy_i)) | seed_en_i)
             -------------1-------------   -------2------   ----3----

-1-	-2-	-3-	Status	Tests
0	0	0	Covered	T1,T2,T3
0	0	1	Covered	T1,T2,T3
0	1	0	Covered	T1,T2,T3
1	0	0	Covered	T1,T2,T3

---

Toggle Coverage for Module : prim_lfsr

	Total	Covered	Percent
Totals	7	7	100.00
Total Bits	56	56	100.00
Total Bits 0->1	28	28	100.00
Total Bits 1->0	28	28	100.00

Ports	7	7	100.00
Port Bits	56	56	100.00
Port Bits 0->1	28	28	100.00
Port Bits 1->0	28	28	100.00

Port Details

Name	Toggle	Toggle 1->0	Tests	Toggle 0->1	Tests	Direction
clk_i	Yes	Yes	T1,T2,T3	Yes	T1,T2,T3	INPUT
rst_ni	Yes	Yes	T1,T2,T3	Yes	T1,T2,T3	INPUT
seed_en_i	Yes	Yes	T1,T2,T3	Yes	T1,T2,T3	INPUT
seed_i[7:0]	Yes	Yes	T1,T2,T3	Yes	T1,T2,T3	INPUT
lfsr_en_i	Yes	Yes	T1,T2,T3	Yes	T1,T2,T3	INPUT
entropy_i[7:0]	Yes	Yes	T1,T2,T3	Yes	T1,T2,T3	INPUT
state_o[7:0]	Yes	Yes	T1,T2,T3	Yes	T1,T2,T3	OUTPUT

---

Branch Coverage for Module : prim_lfsr

	Line No.	Total	Covered	Percent
Branches		15	15	100.00
TERNARY	345	4	4	100.00
TERNARY	610	4	4	100.00
IF	487	2	2	100.00
IF	618	2	2	100.00
IF	513	3	3	100.00

345          assign lfsr_d = (seed_en_i)           ? seed_i          :
                                                   -1-  
                                                   ==>  
346                          (lfsr_en_i && lockup) ? DefaultSeedLocal     :
                                                   -2-  
                                                   ==>  
347                          (lfsr_en_i)           ? next_lfsr_state :
                                                   -3-  
                                                   ==>  
                                                   ==>  

Branches:

-1-	-2-	-3-	Status	Tests
1	-	-	Covered	T1,T2,T3
0	1	-	Covered	T1,T2,T3
0	0	1	Covered	T1,T2,T3
0	0	0	Covered	T1,T2,T3

610            assign cnt_d = (lfsr_en_i && lockup)             ? '0           :
                                                                -1-  
                                                                ==>  
611                           (lfsr_en_i && (cnt_q == cmp_val)) ? '0           :
                                                                -2-  
                                                                ==>  
612                           (lfsr_en_i)                       ? cnt_q + 1'b1 :
                                                                -3-  
                                                                ==>  
                                                                ==>  

Branches:

-1-	-2-	-3-	Status	Tests
1	-	-	Covered	T1,T2,T3
0	1	-	Covered	T1,T2,T3
0	0	1	Covered	T1,T2,T3
0	0	0	Covered	T1,T2,T3

487            if (!rst_ni) begin
               -1-  
488              lfsr_q <= DefaultSeedLocal;
                 ==>
489            end else begin
490              lfsr_q <= lfsr_d;
                 ==>

Branches:

-1-	Status	Tests
1	Covered	T1,T2,T3
0	Covered	T1,T2,T3

618              if (!rst_ni) begin
                 -1-  
619                cnt_q       <= '0;
                   ==>
620                perturbed_q <= 1'b0;
621              end else begin
622                cnt_q       <= cnt_d;
                   ==>

Branches:

-1-	Status	Tests
1	Covered	T1,T2,T3
0	Covered	T1,T2,T3

513            if (64'(LfsrType) == 64'("GAL_XOR")) begin
               -1-  
514              if (next_state == 0) begin
                 -2-  
515                next_state = DefaultSeedLocal;
                   ==>
516              end else begin
517                state0 = next_state[0];
518                next_state = next_state >> 1;
519                if (state0) next_state ^= lfsrcoeffs;
                   -3-  
                   ==>
                   MISSING_ELSE
                   ==>
520                next_state ^= LfsrDw'(entropy);
521              end
522            // Fibonacci XNOR
523            end else if (64'(LfsrType) == "FIB_XNOR") begin
                        -4-  
524              if (&next_state) begin
                 -5-  
525                next_state = DefaultSeedLocal;
                   ==> (Unreachable)
526              end else begin
527                state0 = ~(^(next_state & lfsrcoeffs));
                   ==> (Unreachable)
528                next_state = next_state << 1;
529                next_state[0] = state0;
530                next_state ^= LfsrDw'(entropy);
531              end
532            end else begin
533              $error("unknown lfsr type");
                 ==> (Unreachable)

Branches:

-1-	-2-	-3-	-4-	-5-	Status	Tests
1	1	-	-	-	Covered	T1,T2,T3
1	0	1	-	-	Covered	T1,T2,T3
1	0	0	-	-	Covered	T1,T2,T3
0	-	-	1	1	Unreachable	T4,T5,T6
0	-	-	1	0	Unreachable	T4,T5,T6
0	-	-	0	-	Unreachable

---

Assert Coverage for Module : prim_lfsr

	Total	Attempted	Percent	Succeeded/Matched	Percent
Assertions	20	19	95.00	19	95.00
Cover properties	0	0		0
Cover sequences	0	0		0
Total	20	19	95.00	19	95.00

---

Assertion Details

Name	Attempts	Real Successes	Failures	Incomplete
CoeffCheck_A	1695548588	1680055435	0	0
DataKnownO_A	1695548588	1680055435	0	0
InputWidth_A	300	300	0	0
NextStateCheck_A	1695548588	1678242317	0	300
NoLockups_A	1695548588	1677774158	0	0
OutputKnown_A	1695548588	1680055435	0	0
OutputWidth_A	300	300	0	0
gen_ext_seed_sva.ExtDefaultSeedInputCheck_A	1695548588	1032260	0	0
gen_fib_xnor.DefaultSeedNzCheck_A	150	150	0	0
gen_fib_xnor.gen_lut.MaxLfsrWidth_A	150	150	0	0
gen_fib_xnor.gen_lut.MinLfsrWidth_A	150	150	0	0
gen_gal_xor.DefaultSeedNzCheck_A	150	150	0	0
gen_gal_xor.gen_lut.MaxLfsrWidth_A	150	150	0	0
gen_gal_xor.gen_lut.MinLfsrWidth_A	150	150	0	0
gen_lockup_mechanism_sva.LfsrLockupCheck_A	1695548588	1502	0	0
gen_max_len_sva.MaximalLengthCheck0_A	1695548588	6756	0	0
gen_max_len_sva.MaximalLengthCheck1_A	1695548588	1677772203	0	0
gen_perm_check.p_perm_check.PermutationCheck_A	300	300	0	0
p_randomize_default_seed.DefaultSeedLocalRandomizeCheck_A	300	300	0	0
p_randomize_default_seed.UseDefaultSeedRandomizeCheck_A	0	0	0	0

CoeffCheck_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	1695548588	1680055435	0	0
T1	44759	5831	0	0
T2	55634	6842	0	0
T3	40373	5478	0	0
T7	50195	6575	0	0
T8	42718	5580	0	0
T9	70915	9789	0	0
T10	67600	8916	0	0
T11	71447	9719	0	0
T12	55213	7281	0	0
T13	72768	9848	0	0
T14	168258	167836	0	0
T15	168264	167835	0	0
T16	168292	167838	0	0
T17	168284	167839	0	0
T18	168309	167840	0	0
T19	168377	167850	0	0
T20	168176	167823	0	0
T21	168227	167833	0	0
T22	168446	167860	0	0
T23	168235	167830	0	0

DataKnownO_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	1695548588	1680055435	0	0
T1	44759	5831	0	0
T2	55634	6842	0	0
T3	40373	5478	0	0
T7	50195	6575	0	0
T8	42718	5580	0	0
T9	70915	9789	0	0
T10	67600	8916	0	0
T11	71447	9719	0	0
T12	55213	7281	0	0
T13	72768	9848	0	0
T14	168258	167836	0	0
T15	168264	167835	0	0
T16	168292	167838	0	0
T17	168284	167839	0	0
T18	168309	167840	0	0
T19	168377	167850	0	0
T20	168176	167823	0	0
T21	168227	167833	0	0
T22	168446	167860	0	0
T23	168235	167830	0	0

InputWidth_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	300	300	0	0
T1	1	1	0	0
T2	1	1	0	0
T3	1	1	0	0
T7	1	1	0	0
T8	1	1	0	0
T9	1	1	0	0
T10	1	1	0	0
T11	1	1	0	0
T12	1	1	0	0
T13	1	1	0	0
T14	1	1	0	0
T15	1	1	0	0
T16	1	1	0	0
T17	1	1	0	0
T18	1	1	0	0
T19	1	1	0	0
T20	1	1	0	0
T21	1	1	0	0
T22	1	1	0	0
T23	1	1	0	0

NextStateCheck_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	1695548588	1678242317	0	300
T1	44759	1414	0	1
T2	55634	1642	0	1
T3	40373	1353	0	1
T7	50195	1518	0	1
T8	42718	1336	0	1
T9	70915	2234	0	1
T10	67600	2035	0	1
T11	71447	2172	0	1
T12	55213	1658	0	1
T13	72768	2308	0	1
T14	168258	167785	0	1
T15	168264	167785	0	1
T16	168292	167786	0	1
T17	168284	167786	0	1
T18	168309	167786	0	1
T19	168377	167788	0	1
T20	168176	167782	0	1
T21	168227	167785	0	1
T22	168446	167790	0	1
T23	168235	167784	0	1

NoLockups_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	1695548588	1677774158	0	0
T1	44759	261	0	0
T2	55634	265	0	0
T3	40373	261	0	0
T7	50195	266	0	0
T8	42718	261	0	0
T9	70915	271	0	0
T10	67600	261	0	0
T11	71447	264	0	0
T12	55213	265	0	0
T13	72768	264	0	0
T14	168258	167772	0	0
T15	168264	167772	0	0
T16	168292	167772	0	0
T17	168284	167772	0	0
T18	168309	167772	0	0
T19	168377	167772	0	0
T20	168176	167772	0	0
T21	168227	167772	0	0
T22	168446	167772	0	0
T23	168235	167772	0	0

OutputKnown_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	1695548588	1680055435	0	0
T1	44759	5831	0	0
T2	55634	6842	0	0
T3	40373	5478	0	0
T7	50195	6575	0	0
T8	42718	5580	0	0
T9	70915	9789	0	0
T10	67600	8916	0	0
T11	71447	9719	0	0
T12	55213	7281	0	0
T13	72768	9848	0	0
T14	168258	167836	0	0
T15	168264	167835	0	0
T16	168292	167838	0	0
T17	168284	167839	0	0
T18	168309	167840	0	0
T19	168377	167850	0	0
T20	168176	167823	0	0
T21	168227	167833	0	0
T22	168446	167860	0	0
T23	168235	167830	0	0

OutputWidth_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	300	300	0	0
T1	1	1	0	0
T2	1	1	0	0
T3	1	1	0	0
T7	1	1	0	0
T8	1	1	0	0
T9	1	1	0	0
T10	1	1	0	0
T11	1	1	0	0
T12	1	1	0	0
T13	1	1	0	0
T14	1	1	0	0
T15	1	1	0	0
T16	1	1	0	0
T17	1	1	0	0
T18	1	1	0	0
T19	1	1	0	0
T20	1	1	0	0
T21	1	1	0	0
T22	1	1	0	0
T23	1	1	0	0

gen_ext_seed_sva.ExtDefaultSeedInputCheck_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	1695548588	1032260	0	0
T1	44759	2494	0	0
T2	55634	2915	0	0
T3	40373	2353	0	0
T7	50195	2880	0	0
T8	42718	2346	0	0
T9	70915	4363	0	0
T10	67600	3953	0	0
T11	71447	4392	0	0
T12	55213	3230	0	0
T13	72768	4308	0	0
T14	168258	2946	0	0
T15	168264	2860	0	0
T16	168292	2945	0	0
T17	168284	3056	0	0
T18	168309	3052	0	0
T19	168377	3498	0	0
T20	168176	2327	0	0
T21	168227	2846	0	0
T22	168446	4028	0	0
T23	168235	2611	0	0

gen_fib_xnor.DefaultSeedNzCheck_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	150	150	0	0
T4	1	1	0	0
T5	1	1	0	0
T6	1	1	0	0
T24	1	1	0	0
T25	1	1	0	0
T26	1	1	0	0
T27	1	1	0	0
T28	1	1	0	0
T29	1	1	0	0
T30	1	1	0	0
T31	1	1	0	0
T32	1	1	0	0
T33	1	1	0	0
T34	1	1	0	0
T35	1	1	0	0
T36	1	1	0	0
T37	1	1	0	0
T38	1	1	0	0
T39	1	1	0	0
T40	1	1	0	0

gen_fib_xnor.gen_lut.MaxLfsrWidth_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	150	150	0	0
T4	1	1	0	0
T5	1	1	0	0
T6	1	1	0	0
T24	1	1	0	0
T25	1	1	0	0
T26	1	1	0	0
T27	1	1	0	0
T28	1	1	0	0
T29	1	1	0	0
T30	1	1	0	0
T31	1	1	0	0
T32	1	1	0	0
T33	1	1	0	0
T34	1	1	0	0
T35	1	1	0	0
T36	1	1	0	0
T37	1	1	0	0
T38	1	1	0	0
T39	1	1	0	0
T40	1	1	0	0

gen_fib_xnor.gen_lut.MinLfsrWidth_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	150	150	0	0
T4	1	1	0	0
T5	1	1	0	0
T6	1	1	0	0
T24	1	1	0	0
T25	1	1	0	0
T26	1	1	0	0
T27	1	1	0	0
T28	1	1	0	0
T29	1	1	0	0
T30	1	1	0	0
T31	1	1	0	0
T32	1	1	0	0
T33	1	1	0	0
T34	1	1	0	0
T35	1	1	0	0
T36	1	1	0	0
T37	1	1	0	0
T38	1	1	0	0
T39	1	1	0	0
T40	1	1	0	0

gen_gal_xor.DefaultSeedNzCheck_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	150	150	0	0
T1	1	1	0	0
T2	1	1	0	0
T3	1	1	0	0
T7	1	1	0	0
T8	1	1	0	0
T9	1	1	0	0
T10	1	1	0	0
T11	1	1	0	0
T12	1	1	0	0
T13	1	1	0	0
T14	1	1	0	0
T15	1	1	0	0
T16	1	1	0	0
T17	1	1	0	0
T18	1	1	0	0
T19	1	1	0	0
T20	1	1	0	0
T21	1	1	0	0
T22	1	1	0	0
T23	1	1	0	0

gen_gal_xor.gen_lut.MaxLfsrWidth_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	150	150	0	0
T1	1	1	0	0
T2	1	1	0	0
T3	1	1	0	0
T7	1	1	0	0
T8	1	1	0	0
T9	1	1	0	0
T10	1	1	0	0
T11	1	1	0	0
T12	1	1	0	0
T13	1	1	0	0
T14	1	1	0	0
T15	1	1	0	0
T16	1	1	0	0
T17	1	1	0	0
T18	1	1	0	0
T19	1	1	0	0
T20	1	1	0	0
T21	1	1	0	0
T22	1	1	0	0
T23	1	1	0	0

gen_gal_xor.gen_lut.MinLfsrWidth_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	150	150	0	0
T1	1	1	0	0
T2	1	1	0	0
T3	1	1	0	0
T7	1	1	0	0
T8	1	1	0	0
T9	1	1	0	0
T10	1	1	0	0
T11	1	1	0	0
T12	1	1	0	0
T13	1	1	0	0
T14	1	1	0	0
T15	1	1	0	0
T16	1	1	0	0
T17	1	1	0	0
T18	1	1	0	0
T19	1	1	0	0
T20	1	1	0	0
T21	1	1	0	0
T22	1	1	0	0
T23	1	1	0	0

gen_lockup_mechanism_sva.LfsrLockupCheck_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	1695548588	1502	0	0
T1	44759	4	0	0
T2	55634	7	0	0
T3	40373	6	0	0
T7	50195	8	0	0
T8	42718	3	0	0
T9	70915	7	0	0
T10	67600	6	0	0
T11	71447	12	0	0
T12	55213	6	0	0
T13	72768	7	0	0
T14	168258	1	0	0
T15	168264	1	0	0
T16	168292	1	0	0
T17	168284	1	0	0
T18	168309	1	0	0
T19	168377	1	0	0
T20	168176	1	0	0
T21	168227	1	0	0
T22	168446	1	0	0
T23	168235	1	0	0

gen_max_len_sva.MaximalLengthCheck0_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	1695548588	6756	0	0
T1	44759	28	0	0
T2	55634	17	0	0
T3	40373	24	0	0
T7	50195	32	0	0
T8	42718	28	0	0
T9	70915	19	0	0
T10	67600	17	0	0
T11	71447	31	0	0
T12	55213	24	0	0
T13	72768	34	0	0
T14	168258	17	0	0
T15	168264	22	0	0
T16	168292	21	0	0
T17	168284	13	0	0
T18	168309	24	0	0
T19	168377	14	0	0
T20	168176	20	0	0
T21	168227	14	0	0
T22	168446	15	0	0
T23	168235	14	0	0

gen_max_len_sva.MaximalLengthCheck1_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	1695548588	1677772203	0	0
T1	44759	254	0	0
T2	55634	254	0	0
T3	40373	254	0	0
T7	50195	254	0	0
T8	42718	254	0	0
T9	70915	254	0	0
T10	67600	254	0	0
T11	71447	254	0	0
T12	55213	254	0	0
T13	72768	254	0	0
T14	168258	167772	0	0
T15	168264	167772	0	0
T16	168292	167772	0	0
T17	168284	167772	0	0
T18	168309	167772	0	0
T19	168377	167772	0	0
T20	168176	167772	0	0
T21	168227	167772	0	0
T22	168446	167772	0	0
T23	168235	167772	0	0

gen_perm_check.p_perm_check.PermutationCheck_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	300	300	0	0
T1	1	1	0	0
T2	1	1	0	0
T3	1	1	0	0
T7	1	1	0	0
T8	1	1	0	0
T9	1	1	0	0
T10	1	1	0	0
T11	1	1	0	0
T12	1	1	0	0
T13	1	1	0	0
T14	1	1	0	0
T15	1	1	0	0
T16	1	1	0	0
T17	1	1	0	0
T18	1	1	0	0
T19	1	1	0	0
T20	1	1	0	0
T21	1	1	0	0
T22	1	1	0	0
T23	1	1	0	0

p_randomize_default_seed.DefaultSeedLocalRandomizeCheck_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	300	300	0	0
T1	1	1	0	0
T2	1	1	0	0
T3	1	1	0	0
T7	1	1	0	0
T8	1	1	0	0
T9	1	1	0	0
T10	1	1	0	0
T11	1	1	0	0
T12	1	1	0	0
T13	1	1	0	0
T14	1	1	0	0
T15	1	1	0	0
T16	1	1	0	0
T17	1	1	0	0
T18	1	1	0	0
T19	1	1	0	0
T20	1	1	0	0
T21	1	1	0	0
T22	1	1	0	0
T23	1	1	0	0

Line Coverage for Instance : prim_lfsr_tb.gen_duts[8].i_prim_lfsr

	Line No.	Total	Covered	Percent
TOTAL		32	32	100.00
CONT_ASSIGN	296	1	1	100.00
CONT_ASSIGN	299	1	1	100.00
CONT_ASSIGN	345	1	1	100.00
CONT_ASSIGN	465	1	1	100.00
CONT_ASSIGN	472	1	1	100.00
CONT_ASSIGN	472	1	1	100.00
CONT_ASSIGN	472	1	1	100.00
CONT_ASSIGN	472	1	1	100.00
CONT_ASSIGN	472	1	1	100.00
CONT_ASSIGN	472	1	1	100.00
CONT_ASSIGN	472	1	1	100.00
CONT_ASSIGN	472	1	1	100.00
ALWAYS	487	3	3	100.00
ROUTINE	510	10	10	100.00
CONT_ASSIGN	610	1	1	100.00
CONT_ASSIGN	615	1	1	100.00
ALWAYS	618	5	5	100.00

295                         // calculate next state using internal XOR feedback and entropy input
296        1/1              assign next_lfsr_state = LfsrDw'(entropy_i) ^ ({LfsrDw{lfsr_q[0]}} & coeffs) ^ (lfsr_q >> 1);
           Tests:       T1 T2 T3 
297                     
298                         // lockup condition is all-zero
299        1/1              assign lockup = ~(|lfsr_q);
           Tests:       T1 T2 T3 
300                     
301                         // check that seed is not all-zero
302                         `ASSERT_INIT(DefaultSeedNzCheck_A, |DefaultSeedLocal)
303                     
304                     
305                       ////////////////////
306                       // Fibonacci XNOR //
307                       ////////////////////
308                       end else if (64'(LfsrType) == "FIB_XNOR") begin : gen_fib_xnor
309                     
310                         // if custom polynomial is provided
311                         if (CustomCoeffs > 0) begin : gen_custom
312                           assign coeffs = CustomCoeffs[LfsrDw-1:0];
313                         end else begin : gen_lut
314                           assign coeffs = LFSR_COEFFS[LfsrDw-LUT_OFF][LfsrDw-1:0];
315                           // check that the most significant bit of polynomial is 1
316                           `ASSERT_INIT(MinLfsrWidth_A, LfsrDw >= $low(LFSR_COEFFS)+LUT_OFF)
317                           `ASSERT_INIT(MaxLfsrWidth_A, LfsrDw <= $high(LFSR_COEFFS)+LUT_OFF)
318                         end
319                     
320                         // calculate next state using external XNOR feedback and entropy input
321                         assign next_lfsr_state = LfsrDw'(entropy_i) ^ {lfsr_q[LfsrDw-2:0], ~(^(lfsr_q & coeffs))};
322                     
323                         // lockup condition is all-ones
324                         assign lockup = &lfsr_q;
325                     
326                         // check that seed is not all-ones
327                         `ASSERT_INIT(DefaultSeedNzCheck_A, !(&DefaultSeedLocal))
328                     
329                     
330                       /////////////
331                       // Unknown //
332                       /////////////
333                       end else begin : gen_unknown_type
334                         assign coeffs = '0;
335                         assign next_lfsr_state = '0;
336                         assign lockup = 1'b0;
337                         `ASSERT_INIT(UnknownLfsrType_A, 0)
338                       end
339                     
340                     
341                       //////////////////
342                       // Shared logic //
343                       //////////////////
344                     
345        1/1            assign lfsr_d = (seed_en_i)           ? seed_i          :
           Tests:       T1 T2 T3 
346                                       (lfsr_en_i && lockup) ? DefaultSeedLocal     :
347                                       (lfsr_en_i)           ? next_lfsr_state :
348                                                               lfsr_q;
349                     
350                       logic [LfsrDw-1:0] sbox_out;
351                       if (NonLinearOut) begin : gen_out_non_linear
352                         // The "aligned" permutation ensures that adjacent bits do not go into the same SBox. It is
353                         // different from the state permutation that can be specified via the StatePerm parameter. The
354                         // permutation taps out 4 SBox input bits at regular stride intervals. E.g., for a 16bit
355                         // vector, the input assignment looks as follows:
356                         //
357                         // SBox0: 0,  4,  8, 12
358                         // SBox1: 1,  5,  9, 13
359                         // SBox2: 2,  6, 10, 14
360                         // SBox3: 3,  7, 11, 15
361                         //
362                         // Note that this permutation can be produced by filling the input vector into matrix columns
363                         // and reading out the SBox inputs as matrix rows.
364                         localparam int NumSboxes = LfsrDw / 4;
365                         // Fill in the input vector in col-major order.
366                         logic [3:0][NumSboxes-1:0][LfsrIdxDw-1:0] matrix_indices;
367                         for (genvar j = 0; j < LfsrDw; j++) begin : gen_input_idx_map
368                           assign matrix_indices[j / NumSboxes][j % NumSboxes] = j;
369                         end
370                         // Due to the LFSR shifting pattern, the above permutation has the property that the output of
371                         // SBox(n) is going to be equal to SBox(n+1) in the subsequent cycle (unless the LFSR polynomial
372                         // modifies some of the associated shifted bits via an XOR tap).
373                         // We therefore tweak this permutation by rotating and reversing some of the assignment matrix
374                         // columns. The rotation and reversion operations have been chosen such that this
375                         // generalizes to all power of two widths supported by the LFSR primitive. For 16bit, this
376                         // looks as follows:
377                         //
378                         // SBox0: 0,  6, 11, 14
379                         // SBox1: 1,  7, 10, 13
380                         // SBox2: 2,  4,  9, 12
381                         // SBox3: 3,  5,  8, 15
382                         //
383                         // This can be achieved by:
384                         //   1) down rotating the second column by NumSboxes/2
385                         //   2) reversing the third column
386                         //   3) down rotating the fourth column by 1 and reversing it
387                         //
388                         logic [3:0][NumSboxes-1:0][LfsrIdxDw-1:0] matrix_rotrev_indices;
389                         typedef logic [NumSboxes-1:0][LfsrIdxDw-1:0] matrix_col_t;
390                     
391                         // left-rotates a matrix column by the shift amount
392                         function automatic matrix_col_t lrotcol(matrix_col_t col, integer shift);
393                           matrix_col_t out;
394                           for (int k = 0; k < NumSboxes; k++) begin
395                             out[(k + shift) % NumSboxes] = col[k];
396                           end
397                           return out;
398                         endfunction : lrotcol
399                     
400                         // reverses a matrix column
401                         function automatic matrix_col_t revcol(matrix_col_t col);
402                           return {<<LfsrIdxDw{col}};
403                         endfunction : revcol
404                     
405                         always_comb begin : p_rotrev
406                           matrix_rotrev_indices[0] = matrix_indices[0];
407                           matrix_rotrev_indices[1] = lrotcol(matrix_indices[1], NumSboxes/2);
408                           matrix_rotrev_indices[2] = revcol(matrix_indices[2]);
409                           matrix_rotrev_indices[3] = revcol(lrotcol(matrix_indices[3], 1));
410                         end
411                     
412                         // Read out the matrix rows and linearize.
413                         logic [LfsrDw-1:0][LfsrIdxDw-1:0] sbox_in_indices;
414                         for (genvar k = 0; k < LfsrDw; k++) begin : gen_reverse_upper
415                           assign sbox_in_indices[k] = matrix_rotrev_indices[k % 4][k / 4];
416                         end
417                     
418                     `ifndef SYNTHESIS
419                           // Check that the permutation is indeed a permutation.
420                           logic [LfsrDw-1:0] sbox_perm_test;
421                           always_comb begin : p_perm_check
422                             sbox_perm_test = '0;
423                             for (int k = 0; k < LfsrDw; k++) begin
424                               sbox_perm_test[sbox_in_indices[k]] = 1'b1;
425                             end
426                           end
427                           // All bit positions must be marked with 1.
428                           `ASSERT(SboxPermutationCheck_A, &sbox_perm_test)
429                     `endif
430                     
431                     `ifdef FPV_ON
432                           // Verify that the permutation indeed breaks linear shifting patterns of 4bit input groups.
433                           // The symbolic variables let the FPV tool select all sbox index combinations and linear shift
434                           // offsets.
435                           int shift;
436                           int unsigned sk, sj;
437                           `ASSUME(SjSkRange_M, (sj < NumSboxes) && (sk < NumSboxes))
438                           `ASSUME(SjSkDifferent_M, sj != sk)
439                           `ASSUME(SjSkStable_M, ##1 $stable(sj) && $stable(sk) && $stable(shift))
440                           `ASSERT(SboxInputIndexGroupIsUnique_A,
441                               !((((sbox_in_indices[sj * 4 + 0] + shift) % LfsrDw) == sbox_in_indices[sk * 4 + 0]) &&
442                                 (((sbox_in_indices[sj * 4 + 1] + shift) % LfsrDw) == sbox_in_indices[sk * 4 + 1]) &&
443                                 (((sbox_in_indices[sj * 4 + 2] + shift) % LfsrDw) == sbox_in_indices[sk * 4 + 2]) &&
444                                 (((sbox_in_indices[sj * 4 + 3] + shift) % LfsrDw) == sbox_in_indices[sk * 4 + 3])))
445                     
446                           // this checks that the permutations does not preserve neighboring bit positions.
447                           // i.e. no two neighboring bits are mapped to neighboring bit positions.
448                           int y;
449                           int unsigned ik;
450                           `ASSUME(IkYRange_M, (ik < LfsrDw) && (y == 1 || y == -1))
451                           `ASSUME(IkStable_M, ##1 $stable(ik) && $stable(y))
452                           `ASSERT(IndicesNotAdjacent_A, (sbox_in_indices[ik] - sbox_in_indices[(ik + y) % LfsrDw]) != 1)
453                     `endif
454                     
455                         // Use the permutation indices to create the SBox layer
456                         for (genvar k = 0; k < NumSboxes; k++) begin : gen_sboxes
457                           logic [3:0] sbox_in;
458                           assign sbox_in = {lfsr_q[sbox_in_indices[k*4 + 3]],
459                                             lfsr_q[sbox_in_indices[k*4 + 2]],
460                                             lfsr_q[sbox_in_indices[k*4 + 1]],
461                                             lfsr_q[sbox_in_indices[k*4 + 0]]};
462                           assign sbox_out[k*4 +: 4] = prim_cipher_pkg::PRINCE_SBOX4[sbox_in];
463                         end
464                       end else begin : gen_out_passthru
465        1/1              assign sbox_out = lfsr_q;
           Tests:       T1 T2 T3 
466                       end
467                     
468                       // Random output permutation, defined at compile time
469                       if (StatePermEn) begin : gen_state_perm
470                     
471                         for (genvar k = 0; k < StateOutDw; k++) begin : gen_perm_loop
472        8/8                assign state_o[k] = sbox_out[StatePerm[k]];
           Tests:       T1 T2 T3  | T1 T2 T3  | T1 T2 T3  | T1 T2 T3  | T1 T2 T3  | T1 T2 T3  | T1 T2 T3  | T1 T2 T3 
473                         end
474                     
475                         // if lfsr width is greater than the output, then by definition
476                         // not every bit will be picked
477                         if (LfsrDw > StateOutDw) begin : gen_tieoff_unused
478                           logic unused_sbox_out;
479                           assign unused_sbox_out = ^sbox_out;
480                         end
481                     
482                       end else begin : gen_no_state_perm
483                         assign state_o = StateOutDw'(sbox_out);
484                       end
485                     
486                       always_ff @(posedge clk_i or negedge rst_ni) begin : p_reg
487        1/1              if (!rst_ni) begin
           Tests:       T1 T2 T3 
488        1/1                lfsr_q <= DefaultSeedLocal;
           Tests:       T1 T2 T3 
489                         end else begin
490        1/1                lfsr_q <= lfsr_d;
           Tests:       T1 T2 T3 
491                         end
492                       end
493                     
494                     
495                       ///////////////////////
496                       // shared assertions //
497                       ///////////////////////
498                     
499                       `ASSERT_KNOWN(DataKnownO_A, state_o)
500                     
501                     // the code below is not meant to be synthesized,
502                     // but it is intended to be used in simulation and FPV
503                     `ifndef SYNTHESIS
504                       function automatic logic [LfsrDw-1:0] compute_next_state(logic [LfsrDw-1:0]    lfsrcoeffs,
505                                                                                logic [EntropyDw-1:0] entropy,
506                                                                                logic [LfsrDw-1:0]    current_state);
507                         logic state0;
508                         logic [LfsrDw-1:0] next_state;
509                     
510        1/1              next_state = current_state;
           Tests:       T1 T2 T3 
511                     
512                         // Galois XOR
513        1/1              if (64'(LfsrType) == 64'("GAL_XOR")) begin
           Tests:       T1 T2 T3 
514        1/1                if (next_state == 0) begin
           Tests:       T1 T2 T3 
515        1/1                  next_state = DefaultSeedLocal;
           Tests:       T1 T2 T3 
516                           end else begin
517        1/1                  state0 = next_state[0];
           Tests:       T1 T2 T3 
518        1/1                  next_state = next_state >> 1;
           Tests:       T1 T2 T3 
519        2/2                  if (state0) next_state ^= lfsrcoeffs;
           Tests:       T1 T2 T3  | T1 T2 T3 
                        MISSING_ELSE
520        1/1                  next_state ^= LfsrDw'(entropy);
           Tests:       T1 T2 T3 
521                           end
522                         // Fibonacci XNOR
523        unreachable      end else if (64'(LfsrType) == "FIB_XNOR") begin
524        unreachable        if (&next_state) begin
525        unreachable          next_state = DefaultSeedLocal;
526                           end else begin
527        unreachable          state0 = ~(^(next_state & lfsrcoeffs));
528        unreachable          next_state = next_state << 1;
529        unreachable          next_state[0] = state0;
530        unreachable          next_state ^= LfsrDw'(entropy);
531                           end
532                         end else begin
533        unreachable        $error("unknown lfsr type");
534                         end
535                     
536        1/1              return next_state;
           Tests:       T1 T2 T3 
537                       endfunction : compute_next_state
538                     
539                       // check whether next state is computed correctly
540                       // we shift the assertion by one clock cycle (##1) in order to avoid
541                       // erroneous SVA triggers right after reset deassertion in cases where
542                       // the precondition is true throughout the reset.
543                       // this can happen since the disable_iff evaluates using unsampled values,
544                       // meaning that the assertion may already read rst_ni == 1 on an active
545                       // clock edge while the flops in the design have not yet changed state.
546                       `ASSERT(NextStateCheck_A, ##1 lfsr_en_i && !seed_en_i |=> lfsr_q ==
547                           compute_next_state(coeffs, $past(entropy_i), $past(lfsr_q)))
548                     
549                       // Only check this if enabled.
550                       if (StatePermEn) begin : gen_perm_check
551                         // Check that the supplied permutation is valid.
552                         logic [LfsrDw-1:0] lfsr_perm_test;
553                         initial begin : p_perm_check
554                           lfsr_perm_test = '0;
555                           for (int k = 0; k < LfsrDw; k++) begin
556                             lfsr_perm_test[StatePerm[k]] = 1'b1;
557                           end
558                           // All bit positions must be marked with 1.
559                           `ASSERT_I(PermutationCheck_A, &lfsr_perm_test)
560                         end
561                       end
562                     
563                     `endif
564                     
565                       `ASSERT_INIT(InputWidth_A, LfsrDw >= EntropyDw)
566                       `ASSERT_INIT(OutputWidth_A, LfsrDw >= StateOutDw)
567                     
568                       // MSB must be one in any case
569                       `ASSERT(CoeffCheck_A, coeffs[LfsrDw-1])
570                     
571                       // output check
572                       `ASSERT_KNOWN(OutputKnown_A, state_o)
573                       if (!StatePermEn && !NonLinearOut) begin : gen_output_sva
574                         `ASSERT(OutputCheck_A, state_o == StateOutDw'(lfsr_q))
575                       end
576                       // if no external input changes the lfsr state, a lockup must not occur (by design)
577                       //`ASSERT(NoLockups_A, (!entropy_i) && (!seed_en_i) |=> !lockup, clk_i, !rst_ni)
578                       `ASSERT(NoLockups_A, lfsr_en_i && !entropy_i && !seed_en_i |=> !lockup)
579                     
580                       // this can be disabled if unused in order to not distort coverage
581                       if (ExtSeedSVA) begin : gen_ext_seed_sva
582                         // check that external seed is correctly loaded into the state
583                         // rst_ni is used directly as part of the pre-condition since the usage of rst_ni
584                         // in disable_iff is unsampled.  See #1985 for more details
585                         `ASSERT(ExtDefaultSeedInputCheck_A, (seed_en_i && rst_ni) |=> lfsr_q == $past(seed_i))
586                       end
587                     
588                       // if the external seed mechanism is not used,
589                       // there is theoretically no way we end up in a lockup condition
590                       // in order to not distort coverage, this SVA can be disabled in such cases
591                       if (LockupSVA) begin : gen_lockup_mechanism_sva
592                         // check that a stuck LFSR is correctly reseeded
593                         `ASSERT(LfsrLockupCheck_A, lfsr_en_i && lockup && !seed_en_i |=> !lockup)
594                       end
595                     
596                       // If non-linear output requested, the LFSR width must be a power of 2 and greater than 16.
597                       if(NonLinearOut) begin : gen_nonlinear_align_check_sva
598                         `ASSERT_INIT(SboxByteAlign_A, 2**$clog2(LfsrDw) == LfsrDw && LfsrDw >= 16)
599                       end
600                     
601                       if (MaxLenSVA) begin : gen_max_len_sva
602                     `ifndef SYNTHESIS
603                         // the code below is a workaround to enable long sequences to be checked.
604                         // some simulators do not support SVA sequences longer than 2**32-1.
605                         logic [LfsrDw-1:0] cnt_d, cnt_q;
606                         logic perturbed_d, perturbed_q;
607                         logic [LfsrDw-1:0] cmp_val;
608                     
609                         assign cmp_val = {{(LfsrDw-1){1'b1}}, 1'b0}; // 2**LfsrDw-2
610        1/1              assign cnt_d = (lfsr_en_i && lockup)             ? '0           :
           Tests:       T1 T2 T3 
611                                        (lfsr_en_i && (cnt_q == cmp_val)) ? '0           :
612                                        (lfsr_en_i)                       ? cnt_q + 1'b1 :
613                                                                            cnt_q;
614                     
615        1/1              assign perturbed_d = perturbed_q | (|entropy_i) | seed_en_i;
           Tests:       T1 T2 T3 
616                     
617                         always_ff @(posedge clk_i or negedge rst_ni) begin : p_max_len
618        1/1                if (!rst_ni) begin
           Tests:       T1 T2 T3 
619        1/1                  cnt_q       <= '0;
           Tests:       T1 T2 T3 
620        1/1                  perturbed_q <= 1'b0;
           Tests:       T1 T2 T3 
621                           end else begin
622        1/1                  cnt_q       <= cnt_d;
           Tests:       T1 T2 T3 
623        1/1                  perturbed_q <= perturbed_d;
           Tests:       T1 T2 T3 

---

Cond Coverage for Instance : prim_lfsr_tb.gen_duts[8].i_prim_lfsr

	Total	Covered	Percent
Conditions	29	28	96.55
Logical	29	28	96.55
Non-Logical	0	0
Event	0	0

 LINE       345
 EXPRESSION (seed_en_i ? seed_i : ((lfsr_en_i && lockup) ? DefaultSeedLocal : (lfsr_en_i ? next_lfsr_state : lfsr_q)))
             ----1----

-1-	Status	Tests
0	Covered	T1,T2,T3
1	Covered	T1,T2,T3

 LINE       345
 SUB-EXPRESSION ((lfsr_en_i && lockup) ? DefaultSeedLocal : (lfsr_en_i ? next_lfsr_state : lfsr_q))
                 ----------1----------

-1-	Status	Tests
0	Covered	T1,T2,T3
1	Covered	T1,T2,T3

 LINE       345
 SUB-EXPRESSION (lfsr_en_i && lockup)
                 ----1----    ---2--

-1-	-2-	Status	Tests
0	1	Covered	T1,T2,T3
1	0	Covered	T1,T2,T3
1	1	Covered	T1,T2,T3

 LINE       345
 SUB-EXPRESSION (lfsr_en_i ? next_lfsr_state : lfsr_q)
                 ----1----

-1-	Status	Tests
0	Covered	T1,T2,T3
1	Covered	T1,T2,T3

 LINE       514
 EXPRESSION (next_state == 8'b0)
            ----------1---------

-1-	Status	Tests
0	Covered	T1,T2,T3
1	Covered	T1,T2,T3

 LINE       610
 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	Tests
0	Covered	T1,T2,T3
1	Covered	T1,T2,T3

 LINE       610
 SUB-EXPRESSION (lfsr_en_i && lockup)
                 ----1----    ---2--

-1-	-2-	Status	Tests
0	1	Covered	T1,T2,T3
1	0	Covered	T1,T2,T3
1	1	Covered	T1,T2,T3

 LINE       610
 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	Tests
0	Covered	T1,T2,T3
1	Covered	T1,T2,T3

 LINE       610
 SUB-EXPRESSION (lfsr_en_i && (gen_max_len_sva.cnt_q == gen_max_len_sva.cmp_val))
                 ----1----    -------------------------2------------------------

-1-	-2-	Status	Tests
0	1	Not Covered
1	0	Covered	T1,T2,T3
1	1	Covered	T1,T2,T3

 LINE       610
 SUB-EXPRESSION (gen_max_len_sva.cnt_q == gen_max_len_sva.cmp_val)
                -------------------------1------------------------

-1-	Status	Tests
0	Covered	T1,T2,T3
1	Covered	T1,T2,T3

 LINE       610
 SUB-EXPRESSION (lfsr_en_i ? ((gen_max_len_sva.cnt_q + 1'b1)) : gen_max_len_sva.cnt_q)
                 ----1----

-1-	Status	Tests
0	Covered	T1,T2,T3
1	Covered	T1,T2,T3

 LINE       615
 EXPRESSION (gen_max_len_sva.perturbed_q | ((|entropy_i)) | seed_en_i)
             -------------1-------------   -------2------   ----3----

-1-	-2-	-3-	Status	Tests
0	0	0	Covered	T1,T2,T3
0	0	1	Covered	T1,T2,T3
0	1	0	Covered	T1,T2,T3
1	0	0	Covered	T1,T2,T3

---

Toggle Coverage for Instance : prim_lfsr_tb.gen_duts[8].i_prim_lfsr

	Total	Covered	Percent
Totals	7	7	100.00
Total Bits	56	56	100.00
Total Bits 0->1	28	28	100.00
Total Bits 1->0	28	28	100.00

Ports	7	7	100.00
Port Bits	56	56	100.00
Port Bits 0->1	28	28	100.00
Port Bits 1->0	28	28	100.00

Port Details

Name	Toggle	Toggle 1->0	Tests	Toggle 0->1	Tests	Direction
clk_i	Yes	Yes	T1,T2,T3	Yes	T1,T2,T3	INPUT
rst_ni	Yes	Yes	T1,T2,T3	Yes	T1,T2,T3	INPUT
seed_en_i	Yes	Yes	T1,T2,T3	Yes	T1,T2,T3	INPUT
seed_i[7:0]	Yes	Yes	T1,T2,T3	Yes	T1,T2,T3	INPUT
lfsr_en_i	Yes	Yes	T1,T2,T3	Yes	T1,T2,T3	INPUT
entropy_i[7:0]	Yes	Yes	T1,T2,T3	Yes	T1,T2,T3	INPUT
state_o[7:0]	Yes	Yes	T1,T2,T3	Yes	T1,T2,T3	OUTPUT

---

Branch Coverage for Instance : prim_lfsr_tb.gen_duts[8].i_prim_lfsr

	Line No.	Total	Covered	Percent
Branches		15	15	100.00
TERNARY	345	4	4	100.00
TERNARY	610	4	4	100.00
IF	487	2	2	100.00
IF	618	2	2	100.00
IF	513	3	3	100.00

345          assign lfsr_d = (seed_en_i)           ? seed_i          :
                                                   -1-  
                                                   ==>  
346                          (lfsr_en_i && lockup) ? DefaultSeedLocal     :
                                                   -2-  
                                                   ==>  
347                          (lfsr_en_i)           ? next_lfsr_state :
                                                   -3-  
                                                   ==>  
                                                   ==>  

Branches:

-1-	-2-	-3-	Status	Tests
1	-	-	Covered	T1,T2,T3
0	1	-	Covered	T1,T2,T3
0	0	1	Covered	T1,T2,T3
0	0	0	Covered	T1,T2,T3

610            assign cnt_d = (lfsr_en_i && lockup)             ? '0           :
                                                                -1-  
                                                                ==>  
611                           (lfsr_en_i && (cnt_q == cmp_val)) ? '0           :
                                                                -2-  
                                                                ==>  
612                           (lfsr_en_i)                       ? cnt_q + 1'b1 :
                                                                -3-  
                                                                ==>  
                                                                ==>  

Branches:

-1-	-2-	-3-	Status	Tests
1	-	-	Covered	T1,T2,T3
0	1	-	Covered	T1,T2,T3
0	0	1	Covered	T1,T2,T3
0	0	0	Covered	T1,T2,T3

487            if (!rst_ni) begin
               -1-  
488              lfsr_q <= DefaultSeedLocal;
                 ==>
489            end else begin
490              lfsr_q <= lfsr_d;
                 ==>

Branches:

-1-	Status	Tests
1	Covered	T1,T2,T3
0	Covered	T1,T2,T3

618              if (!rst_ni) begin
                 -1-  
619                cnt_q       <= '0;
                   ==>
620                perturbed_q <= 1'b0;
621              end else begin
622                cnt_q       <= cnt_d;
                   ==>

Branches:

-1-	Status	Tests
1	Covered	T1,T2,T3
0	Covered	T1,T2,T3

513            if (64'(LfsrType) == 64'("GAL_XOR")) begin
               -1-  
514              if (next_state == 0) begin
                 -2-  
515                next_state = DefaultSeedLocal;
                   ==>
516              end else begin
517                state0 = next_state[0];
518                next_state = next_state >> 1;
519                if (state0) next_state ^= lfsrcoeffs;
                   -3-  
                   ==>
                   MISSING_ELSE
                   ==>
520                next_state ^= LfsrDw'(entropy);
521              end
522            // Fibonacci XNOR
523            end else if (64'(LfsrType) == "FIB_XNOR") begin
                        -4-  
524              if (&next_state) begin
                 -5-  
525                next_state = DefaultSeedLocal;
                   ==> (Unreachable)
526              end else begin
527                state0 = ~(^(next_state & lfsrcoeffs));
                   ==> (Unreachable)
528                next_state = next_state << 1;
529                next_state[0] = state0;
530                next_state ^= LfsrDw'(entropy);
531              end
532            end else begin
533              $error("unknown lfsr type");
                 ==> (Unreachable)

Branches:

-1-	-2-	-3-	-4-	-5-	Status	Tests
1	1	-	-	-	Covered	T1,T2,T3
1	0	1	-	-	Covered	T1,T2,T3
1	0	0	-	-	Covered	T1,T2,T3
0	-	-	1	1	Unreachable	T4,T5,T6
0	-	-	1	0	Unreachable	T4,T5,T6
0	-	-	0	-	Unreachable

---

Assert Coverage for Instance : prim_lfsr_tb.gen_duts[8].i_prim_lfsr

	Total	Attempted	Percent	Succeeded/Matched	Percent
Assertions	20	19	95.00	19	95.00
Cover properties	0	0		0
Cover sequences	0	0		0
Total	20	19	95.00	19	95.00

---

Assertion Details

Name	Attempts	Real Successes	Failures	Incomplete
CoeffCheck_A	11872804	1569181	0	0
DataKnownO_A	11872804	1569181	0	0
InputWidth_A	200	200	0	0
NextStateCheck_A	11872804	363341	0	200
NoLockups_A	11872804	52558	0	0
OutputKnown_A	11872804	1569181	0	0
OutputWidth_A	200	200	0	0
gen_ext_seed_sva.ExtDefaultSeedInputCheck_A	11872804	686225	0	0
gen_fib_xnor.DefaultSeedNzCheck_A	100	100	0	0
gen_fib_xnor.gen_lut.MaxLfsrWidth_A	100	100	0	0
gen_fib_xnor.gen_lut.MinLfsrWidth_A	100	100	0	0
gen_gal_xor.DefaultSeedNzCheck_A	100	100	0	0
gen_gal_xor.gen_lut.MaxLfsrWidth_A	100	100	0	0
gen_gal_xor.gen_lut.MinLfsrWidth_A	100	100	0	0
gen_lockup_mechanism_sva.LfsrLockupCheck_A	11872804	1402	0	0
gen_max_len_sva.MaximalLengthCheck0_A	11872804	4572	0	0
gen_max_len_sva.MaximalLengthCheck1_A	11872804	50803	0	0
gen_perm_check.p_perm_check.PermutationCheck_A	200	200	0	0
p_randomize_default_seed.DefaultSeedLocalRandomizeCheck_A	200	200	0	0
p_randomize_default_seed.UseDefaultSeedRandomizeCheck_A	0	0	0	0

CoeffCheck_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	11872804	1569181	0	0
T1	44759	5831	0	0
T2	55634	6842	0	0
T3	40373	5478	0	0
T7	50195	6575	0	0
T8	42718	5580	0	0
T9	70915	9789	0	0
T10	67600	8916	0	0
T11	71447	9719	0	0
T12	55213	7281	0	0
T13	72768	9848	0	0

DataKnownO_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	11872804	1569181	0	0
T1	44759	5831	0	0
T2	55634	6842	0	0
T3	40373	5478	0	0
T7	50195	6575	0	0
T8	42718	5580	0	0
T9	70915	9789	0	0
T10	67600	8916	0	0
T11	71447	9719	0	0
T12	55213	7281	0	0
T13	72768	9848	0	0

InputWidth_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	200	200	0	0
T1	1	1	0	0
T2	1	1	0	0
T3	1	1	0	0
T7	1	1	0	0
T8	1	1	0	0
T9	1	1	0	0
T10	1	1	0	0
T11	1	1	0	0
T12	1	1	0	0
T13	1	1	0	0

NextStateCheck_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	11872804	363341	0	200
T1	44759	1414	0	1
T2	55634	1642	0	1
T3	40373	1353	0	1
T7	50195	1518	0	1
T8	42718	1336	0	1
T9	70915	2234	0	1
T10	67600	2035	0	1
T11	71447	2172	0	1
T12	55213	1658	0	1
T13	72768	2308	0	1

NoLockups_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	11872804	52558	0	0
T1	44759	261	0	0
T2	55634	265	0	0
T3	40373	261	0	0
T7	50195	266	0	0
T8	42718	261	0	0
T9	70915	271	0	0
T10	67600	261	0	0
T11	71447	264	0	0
T12	55213	265	0	0
T13	72768	264	0	0

OutputKnown_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	11872804	1569181	0	0
T1	44759	5831	0	0
T2	55634	6842	0	0
T3	40373	5478	0	0
T7	50195	6575	0	0
T8	42718	5580	0	0
T9	70915	9789	0	0
T10	67600	8916	0	0
T11	71447	9719	0	0
T12	55213	7281	0	0
T13	72768	9848	0	0

OutputWidth_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	200	200	0	0
T1	1	1	0	0
T2	1	1	0	0
T3	1	1	0	0
T7	1	1	0	0
T8	1	1	0	0
T9	1	1	0	0
T10	1	1	0	0
T11	1	1	0	0
T12	1	1	0	0
T13	1	1	0	0

gen_ext_seed_sva.ExtDefaultSeedInputCheck_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	11872804	686225	0	0
T1	44759	2494	0	0
T2	55634	2915	0	0
T3	40373	2353	0	0
T7	50195	2880	0	0
T8	42718	2346	0	0
T9	70915	4363	0	0
T10	67600	3953	0	0
T11	71447	4392	0	0
T12	55213	3230	0	0
T13	72768	4308	0	0

gen_fib_xnor.DefaultSeedNzCheck_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	100	100	0	0
T4	1	1	0	0
T5	1	1	0	0
T6	1	1	0	0
T24	1	1	0	0
T25	1	1	0	0
T26	1	1	0	0
T27	1	1	0	0
T28	1	1	0	0
T29	1	1	0	0
T30	1	1	0	0

gen_fib_xnor.gen_lut.MaxLfsrWidth_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	100	100	0	0
T4	1	1	0	0
T5	1	1	0	0
T6	1	1	0	0
T24	1	1	0	0
T25	1	1	0	0
T26	1	1	0	0
T27	1	1	0	0
T28	1	1	0	0
T29	1	1	0	0
T30	1	1	0	0

gen_fib_xnor.gen_lut.MinLfsrWidth_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	100	100	0	0
T4	1	1	0	0
T5	1	1	0	0
T6	1	1	0	0
T24	1	1	0	0
T25	1	1	0	0
T26	1	1	0	0
T27	1	1	0	0
T28	1	1	0	0
T29	1	1	0	0
T30	1	1	0	0

gen_gal_xor.DefaultSeedNzCheck_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	100	100	0	0
T1	1	1	0	0
T2	1	1	0	0
T3	1	1	0	0
T7	1	1	0	0
T8	1	1	0	0
T9	1	1	0	0
T10	1	1	0	0
T11	1	1	0	0
T12	1	1	0	0
T13	1	1	0	0

gen_gal_xor.gen_lut.MaxLfsrWidth_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	100	100	0	0
T1	1	1	0	0
T2	1	1	0	0
T3	1	1	0	0
T7	1	1	0	0
T8	1	1	0	0
T9	1	1	0	0
T10	1	1	0	0
T11	1	1	0	0
T12	1	1	0	0
T13	1	1	0	0

gen_gal_xor.gen_lut.MinLfsrWidth_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	100	100	0	0
T1	1	1	0	0
T2	1	1	0	0
T3	1	1	0	0
T7	1	1	0	0
T8	1	1	0	0
T9	1	1	0	0
T10	1	1	0	0
T11	1	1	0	0
T12	1	1	0	0
T13	1	1	0	0

gen_lockup_mechanism_sva.LfsrLockupCheck_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	11872804	1402	0	0
T1	44759	4	0	0
T2	55634	7	0	0
T3	40373	6	0	0
T7	50195	8	0	0
T8	42718	3	0	0
T9	70915	7	0	0
T10	67600	6	0	0
T11	71447	12	0	0
T12	55213	6	0	0
T13	72768	7	0	0

gen_max_len_sva.MaximalLengthCheck0_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	11872804	4572	0	0
T1	44759	28	0	0
T2	55634	17	0	0
T3	40373	24	0	0
T7	50195	32	0	0
T8	42718	28	0	0
T9	70915	19	0	0
T10	67600	17	0	0
T11	71447	31	0	0
T12	55213	24	0	0
T13	72768	34	0	0

gen_max_len_sva.MaximalLengthCheck1_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	11872804	50803	0	0
T1	44759	254	0	0
T2	55634	254	0	0
T3	40373	254	0	0
T7	50195	254	0	0
T8	42718	254	0	0
T9	70915	254	0	0
T10	67600	254	0	0
T11	71447	254	0	0
T12	55213	254	0	0
T13	72768	254	0	0

gen_perm_check.p_perm_check.PermutationCheck_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	200	200	0	0
T1	1	1	0	0
T2	1	1	0	0
T3	1	1	0	0
T7	1	1	0	0
T8	1	1	0	0
T9	1	1	0	0
T10	1	1	0	0
T11	1	1	0	0
T12	1	1	0	0
T13	1	1	0	0

p_randomize_default_seed.DefaultSeedLocalRandomizeCheck_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	200	200	0	0
T1	1	1	0	0
T2	1	1	0	0
T3	1	1	0	0
T7	1	1	0	0
T8	1	1	0	0
T9	1	1	0	0
T10	1	1	0	0
T11	1	1	0	0
T12	1	1	0	0
T13	1	1	0	0