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_10_11/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	464	1	1	100.00
CONT_ASSIGN	471	1	1	100.00
CONT_ASSIGN	471	1	1	100.00
CONT_ASSIGN	471	1	1	100.00
CONT_ASSIGN	471	1	1	100.00
CONT_ASSIGN	471	1	1	100.00
CONT_ASSIGN	471	1	1	100.00
CONT_ASSIGN	471	1	1	100.00
CONT_ASSIGN	471	1	1	100.00
ALWAYS	486	3	3	100.00
ROUTINE	509	10	10	100.00
CONT_ASSIGN	609	1	1	100.00
CONT_ASSIGN	614	1	1	100.00
ALWAYS	617	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                             for (int k = 0; k < LfsrDw; k++) begin
423                               sbox_perm_test[sbox_in_indices[k]] = 1'b1;
424                             end
425                           end
426                           // All bit positions must be marked with 1.
427                           `ASSERT(SboxPermutationCheck_A, &sbox_perm_test)
428                     `endif
429                     
430                     `ifdef FPV_ON
431                           // Verify that the permutation indeed breaks linear shifting patterns of 4bit input groups.
432                           // The symbolic variables let the FPV tool select all sbox index combinations and linear shift
433                           // offsets.
434                           int shift;
435                           int unsigned sk, sj;
436                           `ASSUME(SjSkRange_M, (sj < NumSboxes) && (sk < NumSboxes))
437                           `ASSUME(SjSkDifferent_M, sj != sk)
438                           `ASSUME(SjSkStable_M, ##1 $stable(sj) && $stable(sk) && $stable(shift))
439                           `ASSERT(SboxInputIndexGroupIsUnique_A,
440                               !((((sbox_in_indices[sj * 4 + 0] + shift) % LfsrDw) == sbox_in_indices[sk * 4 + 0]) &&
441                                 (((sbox_in_indices[sj * 4 + 1] + shift) % LfsrDw) == sbox_in_indices[sk * 4 + 1]) &&
442                                 (((sbox_in_indices[sj * 4 + 2] + shift) % LfsrDw) == sbox_in_indices[sk * 4 + 2]) &&
443                                 (((sbox_in_indices[sj * 4 + 3] + shift) % LfsrDw) == sbox_in_indices[sk * 4 + 3])))
444                     
445                           // this checks that the permutations does not preserve neighboring bit positions.
446                           // i.e. no two neighboring bits are mapped to neighboring bit positions.
447                           int y;
448                           int unsigned ik;
449                           `ASSUME(IkYRange_M, (ik < LfsrDw) && (y == 1 || y == -1))
450                           `ASSUME(IkStable_M, ##1 $stable(ik) && $stable(y))
451                           `ASSERT(IndicesNotAdjacent_A, (sbox_in_indices[ik] - sbox_in_indices[(ik + y) % LfsrDw]) != 1)
452                     `endif
453                     
454                         // Use the permutation indices to create the SBox layer
455                         for (genvar k = 0; k < NumSboxes; k++) begin : gen_sboxes
456                           logic [3:0] sbox_in;
457                           assign sbox_in = {lfsr_q[sbox_in_indices[k*4 + 3]],
458                                             lfsr_q[sbox_in_indices[k*4 + 2]],
459                                             lfsr_q[sbox_in_indices[k*4 + 1]],
460                                             lfsr_q[sbox_in_indices[k*4 + 0]]};
461                           assign sbox_out[k*4 +: 4] = prim_cipher_pkg::PRINCE_SBOX4[sbox_in];
462                         end
463                       end else begin : gen_out_passthru
464        1/1              assign sbox_out = lfsr_q;
           Tests:       T1 T2 T3 
465                       end
466                     
467                       // Random output permutation, defined at compile time
468                       if (StatePermEn) begin : gen_state_perm
469                     
470                         for (genvar k = 0; k < StateOutDw; k++) begin : gen_perm_loop
471        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 
472                         end
473                     
474                         // if lfsr width is greater than the output, then by definition
475                         // not every bit will be picked
476                         if (LfsrDw > StateOutDw) begin : gen_tieoff_unused
477                           logic unused_sbox_out;
478                           assign unused_sbox_out = ^sbox_out;
479                         end
480                     
481                       end else begin : gen_no_state_perm
482                         assign state_o = StateOutDw'(sbox_out);
483                       end
484                     
485                       always_ff @(posedge clk_i or negedge rst_ni) begin : p_reg
486        1/1              if (!rst_ni) begin
           Tests:       T1 T2 T3 
487        1/1                lfsr_q <= DefaultSeedLocal;
           Tests:       T1 T2 T3 
488                         end else begin
489        1/1                lfsr_q <= lfsr_d;
           Tests:       T1 T2 T3 
490                         end
491                       end
492                     
493                     
494                       ///////////////////////
495                       // shared assertions //
496                       ///////////////////////
497                     
498                       `ASSERT_KNOWN(DataKnownO_A, state_o)
499                     
500                     // the code below is not meant to be synthesized,
501                     // but it is intended to be used in simulation and FPV
502                     `ifndef SYNTHESIS
503                       function automatic logic [LfsrDw-1:0] compute_next_state(logic [LfsrDw-1:0]    lfsrcoeffs,
504                                                                                logic [EntropyDw-1:0] entropy,
505                                                                                logic [LfsrDw-1:0]    current_state);
506                         logic state0;
507                         logic [LfsrDw-1:0] next_state;
508                     
509        1/1              next_state = current_state;
           Tests:       T1 T2 T3 
510                     
511                         // Galois XOR
512        1/1              if (64'(LfsrType) == 64'("GAL_XOR")) begin
           Tests:       T1 T2 T3 
513        1/1                if (next_state == 0) begin
           Tests:       T1 T2 T3 
514        1/1                  next_state = DefaultSeedLocal;
           Tests:       T1 T2 T3 
515                           end else begin
516        1/1                  state0 = next_state[0];
           Tests:       T1 T2 T3 
517        1/1                  next_state = next_state >> 1;
           Tests:       T1 T2 T3 
518        2/2                  if (state0) next_state ^= lfsrcoeffs;
           Tests:       T1 T2 T3  | T1 T2 T3 
                        MISSING_ELSE
519        1/1                  next_state ^= LfsrDw'(entropy);
           Tests:       T1 T2 T3 
520                           end
521                         // Fibonacci XNOR
522        unreachable      end else if (64'(LfsrType) == "FIB_XNOR") begin
523        unreachable        if (&next_state) begin
524        unreachable          next_state = DefaultSeedLocal;
525                           end else begin
526        unreachable          state0 = ~(^(next_state & lfsrcoeffs));
527        unreachable          next_state = next_state << 1;
528        unreachable          next_state[0] = state0;
529        unreachable          next_state ^= LfsrDw'(entropy);
530                           end
531                         end else begin
532        unreachable        $error("unknown lfsr type");
533                         end
534                     
535        1/1              return next_state;
           Tests:       T1 T2 T3 
536                       endfunction : compute_next_state
537                     
538                       // check whether next state is computed correctly
539                       // we shift the assertion by one clock cycle (##1) in order to avoid
540                       // erroneous SVA triggers right after reset deassertion in cases where
541                       // the precondition is true throughout the reset.
542                       // this can happen since the disable_iff evaluates using unsampled values,
543                       // meaning that the assertion may already read rst_ni == 1 on an active
544                       // clock edge while the flops in the design have not yet changed state.
545                       `ASSERT(NextStateCheck_A, ##1 lfsr_en_i && !seed_en_i |=> lfsr_q ==
546                           compute_next_state(coeffs, $past(entropy_i), $past(lfsr_q)))
547                     
548                       // Only check this if enabled.
549                       if (StatePermEn) begin : gen_perm_check
550                         // Check that the supplied permutation is valid.
551                         logic [LfsrDw-1:0] lfsr_perm_test;
552                         initial begin : p_perm_check
553                           lfsr_perm_test = '0;
554                           for (int k = 0; k < LfsrDw; k++) begin
555                             lfsr_perm_test[StatePerm[k]] = 1'b1;
556                           end
557                           // All bit positions must be marked with 1.
558                           `ASSERT_I(PermutationCheck_A, &lfsr_perm_test)
559                         end
560                       end
561                     
562                     `endif
563                     
564                       `ASSERT_INIT(InputWidth_A, LfsrDw >= EntropyDw)
565                       `ASSERT_INIT(OutputWidth_A, LfsrDw >= StateOutDw)
566                     
567                       // MSB must be one in any case
568                       `ASSERT(CoeffCheck_A, coeffs[LfsrDw-1])
569                     
570                       // output check
571                       `ASSERT_KNOWN(OutputKnown_A, state_o)
572                       if (!StatePermEn && !NonLinearOut) begin : gen_output_sva
573                         `ASSERT(OutputCheck_A, state_o == StateOutDw'(lfsr_q))
574                       end
575                       // if no external input changes the lfsr state, a lockup must not occur (by design)
576                       //`ASSERT(NoLockups_A, (!entropy_i) && (!seed_en_i) |=> !lockup, clk_i, !rst_ni)
577                       `ASSERT(NoLockups_A, lfsr_en_i && !entropy_i && !seed_en_i |=> !lockup)
578                     
579                       // this can be disabled if unused in order to not distort coverage
580                       if (ExtSeedSVA) begin : gen_ext_seed_sva
581                         // check that external seed is correctly loaded into the state
582                         // rst_ni is used directly as part of the pre-condition since the usage of rst_ni
583                         // in disable_iff is unsampled.  See #1985 for more details
584                         `ASSERT(ExtDefaultSeedInputCheck_A, (seed_en_i && rst_ni) |=> lfsr_q == $past(seed_i))
585                       end
586                     
587                       // if the external seed mechanism is not used,
588                       // there is theoretically no way we end up in a lockup condition
589                       // in order to not distort coverage, this SVA can be disabled in such cases
590                       if (LockupSVA) begin : gen_lockup_mechanism_sva
591                         // check that a stuck LFSR is correctly reseeded
592                         `ASSERT(LfsrLockupCheck_A, lfsr_en_i && lockup && !seed_en_i |=> !lockup)
593                       end
594                     
595                       // If non-linear output requested, the LFSR width must be a power of 2 and greater than 16.
596                       if(NonLinearOut) begin : gen_nonlinear_align_check_sva
597                         `ASSERT_INIT(SboxByteAlign_A, 2**$clog2(LfsrDw) == LfsrDw && LfsrDw >= 16)
598                       end
599                     
600                       if (MaxLenSVA) begin : gen_max_len_sva
601                     `ifndef SYNTHESIS
602                         // the code below is a workaround to enable long sequences to be checked.
603                         // some simulators do not support SVA sequences longer than 2**32-1.
604                         logic [LfsrDw-1:0] cnt_d, cnt_q;
605                         logic perturbed_d, perturbed_q;
606                         logic [LfsrDw-1:0] cmp_val;
607                     
608                         assign cmp_val = {{(LfsrDw-1){1'b1}}, 1'b0}; // 2**LfsrDw-2
609        1/1              assign cnt_d = (lfsr_en_i && lockup)             ? '0           :
           Tests:       T1 T2 T3 
610                                        (lfsr_en_i && (cnt_q == cmp_val)) ? '0           :
611                                        (lfsr_en_i)                       ? cnt_q + 1'b1 :
612                                                                            cnt_q;
613                     
614        1/1              assign perturbed_d = perturbed_q | (|entropy_i) | seed_en_i;
           Tests:       T1 T2 T3 
615                     
616                         always_ff @(posedge clk_i or negedge rst_ni) begin : p_max_len
617        1/1                if (!rst_ni) begin
           Tests:       T1 T2 T3 
618        1/1                  cnt_q       <= '0;
           Tests:       T1 T2 T3 
619        1/1                  perturbed_q <= 1'b0;
           Tests:       T1 T2 T3 
620                           end else begin
621        1/1                  cnt_q       <= cnt_d;
           Tests:       T1 T2 T3 
622        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       513
 EXPRESSION (next_state == 8'b0)
            ----------1---------

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

 LINE       609
 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       609
 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       609
 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       609
 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       609
 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       609
 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       614
 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	609	4	4	100.00
IF	486	2	2	100.00
IF	617	2	2	100.00
IF	512	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

609            assign cnt_d = (lfsr_en_i && lockup)             ? '0           :
                                                                -1-  
                                                                ==>  
610                           (lfsr_en_i && (cnt_q == cmp_val)) ? '0           :
                                                                -2-  
                                                                ==>  
611                           (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

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

Branches:

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

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

Branches:

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

512            if (64'(LfsrType) == 64'("GAL_XOR")) begin
               -1-  
513              if (next_state == 0) begin
                 -2-  
514                next_state = DefaultSeedLocal;
                   ==>
515              end else begin
516                state0 = next_state[0];
517                next_state = next_state >> 1;
518                if (state0) next_state ^= lfsrcoeffs;
                   -3-  
                   ==>
                   MISSING_ELSE
                   ==>
519                next_state ^= LfsrDw'(entropy);
520              end
521            // Fibonacci XNOR
522            end else if (64'(LfsrType) == "FIB_XNOR") begin
                        -4-  
523              if (&next_state) begin
                 -5-  
524                next_state = DefaultSeedLocal;
                   ==> (Unreachable)
525              end else begin
526                state0 = ~(^(next_state & lfsrcoeffs));
                   ==> (Unreachable)
527                next_state = next_state << 1;
528                next_state[0] = state0;
529                next_state ^= LfsrDw'(entropy);
530              end
531            end else begin
532              $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	1695344172	1680019075	0	0
DataKnownO_A	1695344172	1680019075	0	0
InputWidth_A	300	300	0	0
NextStateCheck_A	1695344172	1678233463	0	300
NoLockups_A	1695344172	1677774171	0	0
OutputKnown_A	1695344172	1680019075	0	0
OutputWidth_A	300	300	0	0
gen_ext_seed_sva.ExtDefaultSeedInputCheck_A	1695344172	1014412	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	1695344172	1478	0	0
gen_max_len_sva.MaximalLengthCheck0_A	1695344172	6733	0	0
gen_max_len_sva.MaximalLengthCheck1_A	1695344172	1677772200	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	1695344172	1680019075	0	0
T1	62133	8389	0	0
T2	57594	7464	0	0
T3	67887	8760	0	0
T7	46164	5937	0	0
T8	50361	7180	0	0
T9	75162	9896	0	0
T10	55026	7203	0	0
T11	57519	7549	0	0
T12	51060	6401	0	0
T13	36200	5304	0	0
T14	168288	167837	0	0
T15	168323	167841	0	0
T16	168194	167826	0	0
T17	168271	167836	0	0
T18	168259	167833	0	0
T19	168156	167823	0	0
T20	168189	167826	0	0
T21	168425	167858	0	0
T22	168245	167833	0	0
T23	168422	167855	0	0

DataKnownO_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	1695344172	1680019075	0	0
T1	62133	8389	0	0
T2	57594	7464	0	0
T3	67887	8760	0	0
T7	46164	5937	0	0
T8	50361	7180	0	0
T9	75162	9896	0	0
T10	55026	7203	0	0
T11	57519	7549	0	0
T12	51060	6401	0	0
T13	36200	5304	0	0
T14	168288	167837	0	0
T15	168323	167841	0	0
T16	168194	167826	0	0
T17	168271	167836	0	0
T18	168259	167833	0	0
T19	168156	167823	0	0
T20	168189	167826	0	0
T21	168425	167858	0	0
T22	168245	167833	0	0
T23	168422	167855	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	1695344172	1678233463	0	300
T1	62133	1947	0	1
T2	57594	1705	0	1
T3	67887	2080	0	1
T7	46164	1461	0	1
T8	50361	1672	0	1
T9	75162	2265	0	1
T10	55026	1663	0	1
T11	57519	1779	0	1
T12	51060	1487	0	1
T13	36200	1284	0	1
T14	168288	167785	0	1
T15	168323	167786	0	1
T16	168194	167783	0	1
T17	168271	167785	0	1
T18	168259	167784	0	1
T19	168156	167782	0	1
T20	168189	167782	0	1
T21	168425	167789	0	1
T22	168245	167784	0	1
T23	168422	167789	0	1

NoLockups_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	1695344172	1677774171	0	0
T1	62133	268	0	0
T2	57594	263	0	0
T3	67887	268	0	0
T7	46164	263	0	0
T8	50361	262	0	0
T9	75162	265	0	0
T10	55026	261	0	0
T11	57519	266	0	0
T12	51060	257	0	0
T13	36200	261	0	0
T14	168288	167772	0	0
T15	168323	167772	0	0
T16	168194	167772	0	0
T17	168271	167772	0	0
T18	168259	167772	0	0
T19	168156	167772	0	0
T20	168189	167772	0	0
T21	168425	167772	0	0
T22	168245	167772	0	0
T23	168422	167772	0	0

OutputKnown_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	1695344172	1680019075	0	0
T1	62133	8389	0	0
T2	57594	7464	0	0
T3	67887	8760	0	0
T7	46164	5937	0	0
T8	50361	7180	0	0
T9	75162	9896	0	0
T10	55026	7203	0	0
T11	57519	7549	0	0
T12	51060	6401	0	0
T13	36200	5304	0	0
T14	168288	167837	0	0
T15	168323	167841	0	0
T16	168194	167826	0	0
T17	168271	167836	0	0
T18	168259	167833	0	0
T19	168156	167823	0	0
T20	168189	167826	0	0
T21	168425	167858	0	0
T22	168245	167833	0	0
T23	168422	167855	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	1695344172	1014412	0	0
T1	62133	3614	0	0
T2	57594	3231	0	0
T3	67887	3821	0	0
T7	46164	2464	0	0
T8	50361	3167	0	0
T9	75162	4398	0	0
T10	55026	3173	0	0
T11	57519	3275	0	0
T12	51060	2783	0	0
T13	36200	2342	0	0
T14	168288	2953	0	0
T15	168323	3189	0	0
T16	168194	2426	0	0
T17	168271	2874	0	0
T18	168259	2696	0	0
T19	168156	2284	0	0
T20	168189	2427	0	0
T21	168425	3958	0	0
T22	168245	2789	0	0
T23	168422	3721	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	1695344172	1478	0	0
T1	62133	4	0	0
T2	57594	10	0	0
T3	67887	5	0	0
T7	46164	5	0	0
T8	50361	2	0	0
T9	75162	10	0	0
T10	55026	8	0	0
T11	57519	6	0	0
T12	51060	5	0	0
T13	36200	6	0	0
T14	168288	1	0	0
T15	168323	1	0	0
T16	168194	1	0	0
T17	168271	1	0	0
T18	168259	1	0	0
T19	168156	1	0	0
T20	168189	1	0	0
T21	168425	1	0	0
T22	168245	1	0	0
T23	168422	1	0	0

gen_max_len_sva.MaximalLengthCheck0_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	1695344172	6733	0	0
T1	62133	25	0	0
T2	57594	24	0	0
T3	67887	27	0	0
T7	46164	15	0	0
T8	50361	33	0	0
T9	75162	17	0	0
T10	55026	23	0	0
T11	57519	27	0	0
T12	51060	20	0	0
T13	36200	16	0	0
T14	168288	22	0	0
T15	168323	25	0	0
T16	168194	19	0	0
T17	168271	20	0	0
T18	168259	25	0	0
T19	168156	13	0	0
T20	168189	29	0	0
T21	168425	29	0	0
T22	168245	15	0	0
T23	168422	24	0	0

gen_max_len_sva.MaximalLengthCheck1_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	1695344172	1677772200	0	0
T1	62133	254	0	0
T2	57594	254	0	0
T3	67887	254	0	0
T7	46164	254	0	0
T8	50361	254	0	0
T9	75162	254	0	0
T10	55026	254	0	0
T11	57519	254	0	0
T12	51060	254	0	0
T13	36200	254	0	0
T14	168288	167772	0	0
T15	168323	167772	0	0
T16	168194	167772	0	0
T17	168271	167772	0	0
T18	168259	167772	0	0
T19	168156	167772	0	0
T20	168189	167772	0	0
T21	168425	167772	0	0
T22	168245	167772	0	0
T23	168422	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	464	1	1	100.00
CONT_ASSIGN	471	1	1	100.00
CONT_ASSIGN	471	1	1	100.00
CONT_ASSIGN	471	1	1	100.00
CONT_ASSIGN	471	1	1	100.00
CONT_ASSIGN	471	1	1	100.00
CONT_ASSIGN	471	1	1	100.00
CONT_ASSIGN	471	1	1	100.00
CONT_ASSIGN	471	1	1	100.00
ALWAYS	486	3	3	100.00
ROUTINE	509	10	10	100.00
CONT_ASSIGN	609	1	1	100.00
CONT_ASSIGN	614	1	1	100.00
ALWAYS	617	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                             for (int k = 0; k < LfsrDw; k++) begin
423                               sbox_perm_test[sbox_in_indices[k]] = 1'b1;
424                             end
425                           end
426                           // All bit positions must be marked with 1.
427                           `ASSERT(SboxPermutationCheck_A, &sbox_perm_test)
428                     `endif
429                     
430                     `ifdef FPV_ON
431                           // Verify that the permutation indeed breaks linear shifting patterns of 4bit input groups.
432                           // The symbolic variables let the FPV tool select all sbox index combinations and linear shift
433                           // offsets.
434                           int shift;
435                           int unsigned sk, sj;
436                           `ASSUME(SjSkRange_M, (sj < NumSboxes) && (sk < NumSboxes))
437                           `ASSUME(SjSkDifferent_M, sj != sk)
438                           `ASSUME(SjSkStable_M, ##1 $stable(sj) && $stable(sk) && $stable(shift))
439                           `ASSERT(SboxInputIndexGroupIsUnique_A,
440                               !((((sbox_in_indices[sj * 4 + 0] + shift) % LfsrDw) == sbox_in_indices[sk * 4 + 0]) &&
441                                 (((sbox_in_indices[sj * 4 + 1] + shift) % LfsrDw) == sbox_in_indices[sk * 4 + 1]) &&
442                                 (((sbox_in_indices[sj * 4 + 2] + shift) % LfsrDw) == sbox_in_indices[sk * 4 + 2]) &&
443                                 (((sbox_in_indices[sj * 4 + 3] + shift) % LfsrDw) == sbox_in_indices[sk * 4 + 3])))
444                     
445                           // this checks that the permutations does not preserve neighboring bit positions.
446                           // i.e. no two neighboring bits are mapped to neighboring bit positions.
447                           int y;
448                           int unsigned ik;
449                           `ASSUME(IkYRange_M, (ik < LfsrDw) && (y == 1 || y == -1))
450                           `ASSUME(IkStable_M, ##1 $stable(ik) && $stable(y))
451                           `ASSERT(IndicesNotAdjacent_A, (sbox_in_indices[ik] - sbox_in_indices[(ik + y) % LfsrDw]) != 1)
452                     `endif
453                     
454                         // Use the permutation indices to create the SBox layer
455                         for (genvar k = 0; k < NumSboxes; k++) begin : gen_sboxes
456                           logic [3:0] sbox_in;
457                           assign sbox_in = {lfsr_q[sbox_in_indices[k*4 + 3]],
458                                             lfsr_q[sbox_in_indices[k*4 + 2]],
459                                             lfsr_q[sbox_in_indices[k*4 + 1]],
460                                             lfsr_q[sbox_in_indices[k*4 + 0]]};
461                           assign sbox_out[k*4 +: 4] = prim_cipher_pkg::PRINCE_SBOX4[sbox_in];
462                         end
463                       end else begin : gen_out_passthru
464        1/1              assign sbox_out = lfsr_q;
           Tests:       T1 T2 T3 
465                       end
466                     
467                       // Random output permutation, defined at compile time
468                       if (StatePermEn) begin : gen_state_perm
469                     
470                         for (genvar k = 0; k < StateOutDw; k++) begin : gen_perm_loop
471        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 
472                         end
473                     
474                         // if lfsr width is greater than the output, then by definition
475                         // not every bit will be picked
476                         if (LfsrDw > StateOutDw) begin : gen_tieoff_unused
477                           logic unused_sbox_out;
478                           assign unused_sbox_out = ^sbox_out;
479                         end
480                     
481                       end else begin : gen_no_state_perm
482                         assign state_o = StateOutDw'(sbox_out);
483                       end
484                     
485                       always_ff @(posedge clk_i or negedge rst_ni) begin : p_reg
486        1/1              if (!rst_ni) begin
           Tests:       T1 T2 T3 
487        1/1                lfsr_q <= DefaultSeedLocal;
           Tests:       T1 T2 T3 
488                         end else begin
489        1/1                lfsr_q <= lfsr_d;
           Tests:       T1 T2 T3 
490                         end
491                       end
492                     
493                     
494                       ///////////////////////
495                       // shared assertions //
496                       ///////////////////////
497                     
498                       `ASSERT_KNOWN(DataKnownO_A, state_o)
499                     
500                     // the code below is not meant to be synthesized,
501                     // but it is intended to be used in simulation and FPV
502                     `ifndef SYNTHESIS
503                       function automatic logic [LfsrDw-1:0] compute_next_state(logic [LfsrDw-1:0]    lfsrcoeffs,
504                                                                                logic [EntropyDw-1:0] entropy,
505                                                                                logic [LfsrDw-1:0]    current_state);
506                         logic state0;
507                         logic [LfsrDw-1:0] next_state;
508                     
509        1/1              next_state = current_state;
           Tests:       T1 T2 T3 
510                     
511                         // Galois XOR
512        1/1              if (64'(LfsrType) == 64'("GAL_XOR")) begin
           Tests:       T1 T2 T3 
513        1/1                if (next_state == 0) begin
           Tests:       T1 T2 T3 
514        1/1                  next_state = DefaultSeedLocal;
           Tests:       T1 T2 T3 
515                           end else begin
516        1/1                  state0 = next_state[0];
           Tests:       T1 T2 T3 
517        1/1                  next_state = next_state >> 1;
           Tests:       T1 T2 T3 
518        2/2                  if (state0) next_state ^= lfsrcoeffs;
           Tests:       T1 T2 T3  | T1 T2 T3 
                        MISSING_ELSE
519        1/1                  next_state ^= LfsrDw'(entropy);
           Tests:       T1 T2 T3 
520                           end
521                         // Fibonacci XNOR
522        unreachable      end else if (64'(LfsrType) == "FIB_XNOR") begin
523        unreachable        if (&next_state) begin
524        unreachable          next_state = DefaultSeedLocal;
525                           end else begin
526        unreachable          state0 = ~(^(next_state & lfsrcoeffs));
527        unreachable          next_state = next_state << 1;
528        unreachable          next_state[0] = state0;
529        unreachable          next_state ^= LfsrDw'(entropy);
530                           end
531                         end else begin
532        unreachable        $error("unknown lfsr type");
533                         end
534                     
535        1/1              return next_state;
           Tests:       T1 T2 T3 
536                       endfunction : compute_next_state
537                     
538                       // check whether next state is computed correctly
539                       // we shift the assertion by one clock cycle (##1) in order to avoid
540                       // erroneous SVA triggers right after reset deassertion in cases where
541                       // the precondition is true throughout the reset.
542                       // this can happen since the disable_iff evaluates using unsampled values,
543                       // meaning that the assertion may already read rst_ni == 1 on an active
544                       // clock edge while the flops in the design have not yet changed state.
545                       `ASSERT(NextStateCheck_A, ##1 lfsr_en_i && !seed_en_i |=> lfsr_q ==
546                           compute_next_state(coeffs, $past(entropy_i), $past(lfsr_q)))
547                     
548                       // Only check this if enabled.
549                       if (StatePermEn) begin : gen_perm_check
550                         // Check that the supplied permutation is valid.
551                         logic [LfsrDw-1:0] lfsr_perm_test;
552                         initial begin : p_perm_check
553                           lfsr_perm_test = '0;
554                           for (int k = 0; k < LfsrDw; k++) begin
555                             lfsr_perm_test[StatePerm[k]] = 1'b1;
556                           end
557                           // All bit positions must be marked with 1.
558                           `ASSERT_I(PermutationCheck_A, &lfsr_perm_test)
559                         end
560                       end
561                     
562                     `endif
563                     
564                       `ASSERT_INIT(InputWidth_A, LfsrDw >= EntropyDw)
565                       `ASSERT_INIT(OutputWidth_A, LfsrDw >= StateOutDw)
566                     
567                       // MSB must be one in any case
568                       `ASSERT(CoeffCheck_A, coeffs[LfsrDw-1])
569                     
570                       // output check
571                       `ASSERT_KNOWN(OutputKnown_A, state_o)
572                       if (!StatePermEn && !NonLinearOut) begin : gen_output_sva
573                         `ASSERT(OutputCheck_A, state_o == StateOutDw'(lfsr_q))
574                       end
575                       // if no external input changes the lfsr state, a lockup must not occur (by design)
576                       //`ASSERT(NoLockups_A, (!entropy_i) && (!seed_en_i) |=> !lockup, clk_i, !rst_ni)
577                       `ASSERT(NoLockups_A, lfsr_en_i && !entropy_i && !seed_en_i |=> !lockup)
578                     
579                       // this can be disabled if unused in order to not distort coverage
580                       if (ExtSeedSVA) begin : gen_ext_seed_sva
581                         // check that external seed is correctly loaded into the state
582                         // rst_ni is used directly as part of the pre-condition since the usage of rst_ni
583                         // in disable_iff is unsampled.  See #1985 for more details
584                         `ASSERT(ExtDefaultSeedInputCheck_A, (seed_en_i && rst_ni) |=> lfsr_q == $past(seed_i))
585                       end
586                     
587                       // if the external seed mechanism is not used,
588                       // there is theoretically no way we end up in a lockup condition
589                       // in order to not distort coverage, this SVA can be disabled in such cases
590                       if (LockupSVA) begin : gen_lockup_mechanism_sva
591                         // check that a stuck LFSR is correctly reseeded
592                         `ASSERT(LfsrLockupCheck_A, lfsr_en_i && lockup && !seed_en_i |=> !lockup)
593                       end
594                     
595                       // If non-linear output requested, the LFSR width must be a power of 2 and greater than 16.
596                       if(NonLinearOut) begin : gen_nonlinear_align_check_sva
597                         `ASSERT_INIT(SboxByteAlign_A, 2**$clog2(LfsrDw) == LfsrDw && LfsrDw >= 16)
598                       end
599                     
600                       if (MaxLenSVA) begin : gen_max_len_sva
601                     `ifndef SYNTHESIS
602                         // the code below is a workaround to enable long sequences to be checked.
603                         // some simulators do not support SVA sequences longer than 2**32-1.
604                         logic [LfsrDw-1:0] cnt_d, cnt_q;
605                         logic perturbed_d, perturbed_q;
606                         logic [LfsrDw-1:0] cmp_val;
607                     
608                         assign cmp_val = {{(LfsrDw-1){1'b1}}, 1'b0}; // 2**LfsrDw-2
609        1/1              assign cnt_d = (lfsr_en_i && lockup)             ? '0           :
           Tests:       T1 T2 T3 
610                                        (lfsr_en_i && (cnt_q == cmp_val)) ? '0           :
611                                        (lfsr_en_i)                       ? cnt_q + 1'b1 :
612                                                                            cnt_q;
613                     
614        1/1              assign perturbed_d = perturbed_q | (|entropy_i) | seed_en_i;
           Tests:       T1 T2 T3 
615                     
616                         always_ff @(posedge clk_i or negedge rst_ni) begin : p_max_len
617        1/1                if (!rst_ni) begin
           Tests:       T1 T2 T3 
618        1/1                  cnt_q       <= '0;
           Tests:       T1 T2 T3 
619        1/1                  perturbed_q <= 1'b0;
           Tests:       T1 T2 T3 
620                           end else begin
621        1/1                  cnt_q       <= cnt_d;
           Tests:       T1 T2 T3 
622        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       513
 EXPRESSION (next_state == 8'b0)
            ----------1---------

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

 LINE       609
 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       609
 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       609
 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       609
 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       609
 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       609
 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       614
 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	609	4	4	100.00
IF	486	2	2	100.00
IF	617	2	2	100.00
IF	512	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

609            assign cnt_d = (lfsr_en_i && lockup)             ? '0           :
                                                                -1-  
                                                                ==>  
610                           (lfsr_en_i && (cnt_q == cmp_val)) ? '0           :
                                                                -2-  
                                                                ==>  
611                           (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

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

Branches:

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

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

Branches:

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

512            if (64'(LfsrType) == 64'("GAL_XOR")) begin
               -1-  
513              if (next_state == 0) begin
                 -2-  
514                next_state = DefaultSeedLocal;
                   ==>
515              end else begin
516                state0 = next_state[0];
517                next_state = next_state >> 1;
518                if (state0) next_state ^= lfsrcoeffs;
                   -3-  
                   ==>
                   MISSING_ELSE
                   ==>
519                next_state ^= LfsrDw'(entropy);
520              end
521            // Fibonacci XNOR
522            end else if (64'(LfsrType) == "FIB_XNOR") begin
                        -4-  
523              if (&next_state) begin
                 -5-  
524                next_state = DefaultSeedLocal;
                   ==> (Unreachable)
525              end else begin
526                state0 = ~(^(next_state & lfsrcoeffs));
                   ==> (Unreachable)
527                next_state = next_state << 1;
528                next_state[0] = state0;
529                next_state ^= LfsrDw'(entropy);
530              end
531            end else begin
532              $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	11788683	1550799	0	0
DataKnownO_A	11788683	1550799	0	0
InputWidth_A	200	200	0	0
NextStateCheck_A	11788683	358764	0	200
NoLockups_A	11788683	52571	0	0
OutputKnown_A	11788683	1550799	0	0
OutputWidth_A	200	200	0	0
gen_ext_seed_sva.ExtDefaultSeedInputCheck_A	11788683	676973	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	11788683	1378	0	0
gen_max_len_sva.MaximalLengthCheck0_A	11788683	4561	0	0
gen_max_len_sva.MaximalLengthCheck1_A	11788683	50800	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	11788683	1550799	0	0
T1	62133	8389	0	0
T2	57594	7464	0	0
T3	67887	8760	0	0
T7	46164	5937	0	0
T8	50361	7180	0	0
T9	75162	9896	0	0
T10	55026	7203	0	0
T11	57519	7549	0	0
T12	51060	6401	0	0
T13	36200	5304	0	0

DataKnownO_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	11788683	1550799	0	0
T1	62133	8389	0	0
T2	57594	7464	0	0
T3	67887	8760	0	0
T7	46164	5937	0	0
T8	50361	7180	0	0
T9	75162	9896	0	0
T10	55026	7203	0	0
T11	57519	7549	0	0
T12	51060	6401	0	0
T13	36200	5304	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	11788683	358764	0	200
T1	62133	1947	0	1
T2	57594	1705	0	1
T3	67887	2080	0	1
T7	46164	1461	0	1
T8	50361	1672	0	1
T9	75162	2265	0	1
T10	55026	1663	0	1
T11	57519	1779	0	1
T12	51060	1487	0	1
T13	36200	1284	0	1

NoLockups_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	11788683	52571	0	0
T1	62133	268	0	0
T2	57594	263	0	0
T3	67887	268	0	0
T7	46164	263	0	0
T8	50361	262	0	0
T9	75162	265	0	0
T10	55026	261	0	0
T11	57519	266	0	0
T12	51060	257	0	0
T13	36200	261	0	0

OutputKnown_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	11788683	1550799	0	0
T1	62133	8389	0	0
T2	57594	7464	0	0
T3	67887	8760	0	0
T7	46164	5937	0	0
T8	50361	7180	0	0
T9	75162	9896	0	0
T10	55026	7203	0	0
T11	57519	7549	0	0
T12	51060	6401	0	0
T13	36200	5304	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	11788683	676973	0	0
T1	62133	3614	0	0
T2	57594	3231	0	0
T3	67887	3821	0	0
T7	46164	2464	0	0
T8	50361	3167	0	0
T9	75162	4398	0	0
T10	55026	3173	0	0
T11	57519	3275	0	0
T12	51060	2783	0	0
T13	36200	2342	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	11788683	1378	0	0
T1	62133	4	0	0
T2	57594	10	0	0
T3	67887	5	0	0
T7	46164	5	0	0
T8	50361	2	0	0
T9	75162	10	0	0
T10	55026	8	0	0
T11	57519	6	0	0
T12	51060	5	0	0
T13	36200	6	0	0

gen_max_len_sva.MaximalLengthCheck0_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	11788683	4561	0	0
T1	62133	25	0	0
T2	57594	24	0	0
T3	67887	27	0	0
T7	46164	15	0	0
T8	50361	33	0	0
T9	75162	17	0	0
T10	55026	23	0	0
T11	57519	27	0	0
T12	51060	20	0	0
T13	36200	16	0	0

gen_max_len_sva.MaximalLengthCheck1_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	11788683	50800	0	0
T1	62133	254	0	0
T2	57594	254	0	0
T3	67887	254	0	0
T7	46164	254	0	0
T8	50361	254	0	0
T9	75162	254	0	0
T10	55026	254	0	0
T11	57519	254	0	0
T12	51060	254	0	0
T13	36200	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