FV: updates on RTL changes (#493)

* fv ecc updates * fv sha256, wntz updates * fv sha512_masked updates --------- Co-authored-by: Rohith Babu Batthineni <[email protected]>
chipsalliance · Apr 9, 2024 · eb5393f · eb5393f
1 parent 9c815c3
commit eb5393f
Show file tree

Hide file tree

Showing 24 changed files with 3,309 additions and 1,114 deletions.
diff --git a/src/ecc/formal/fv_ecc_block_overview.pdf b/src/ecc/formal/fv_ecc_block_overview.pdf
diff --git a/src/ecc/formal/properties/coverpoints/fv_ecc_montgomerymultiplier_coverpoints.sv b/src/ecc/formal/properties/coverpoints/fv_ecc_montgomerymultiplier_coverpoints.sv
@@ -28,8 +28,8 @@ module fv_ecc_montgomerymultiplier_coverpoints_m(
     cover_zeroize: cover property(disable iff(!reset_n) ecc_montgomerymultiplier.zeroize );
     cover_prime_p: cover property(disable iff(!reset_n || zeroize) (ecc_montgomerymultiplier.n_i==384'hfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000ffffffff));
     cover_group_order: cover property(disable iff(!reset_n || zeroize)(ecc_montgomerymultiplier.n_i==384'hffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52973));
-    cover_n_prime_i_prime_mu : cover property(disable iff(!reset_n|| zeroize) ecc_montgomerymultiplier.n_prime_i == 32'h00000001);
-    cover_n_prime_i_group_order_mu : cover property(disable iff(!reset_n|| zeroize) ecc_montgomerymultiplier.n_prime_i == 32'he88fdc45);
+    cover_n_prime_i_prime_mu : cover property(disable iff(!reset_n|| zeroize) ecc_montgomerymultiplier.n_prime_i == 48'h100000001);
+    cover_n_prime_i_group_order_mu : cover property(disable iff(!reset_n|| zeroize) ecc_montgomerymultiplier.n_prime_i == 48'h6089e88fdc45);
     cover_opa_i_0 : cover property(disable iff(!reset_n|| zeroize) (ecc_montgomerymultiplier.opa_i == '0)&&(ecc_montgomerymultiplier.opb_i == '0 || ecc_montgomerymultiplier.opb_i == (ecc_montgomerymultiplier.n_i-1)) );
     cover_opa_i_prime_minus_1 : cover property(disable iff(!reset_n|| zeroize) (ecc_montgomerymultiplier.opa_i == (ecc_montgomerymultiplier.n_i-1))&&(ecc_montgomerymultiplier.opb_i == '0 || ecc_montgomerymultiplier.opb_i == (ecc_montgomerymultiplier.n_i-1)) );
     cover_opb_i_0 : cover property(disable iff(!reset_n|| zeroize) (ecc_montgomerymultiplier.opb_i == '0)&&(ecc_montgomerymultiplier.opa_i == '0 || ecc_montgomerymultiplier.opa_i == (ecc_montgomerymultiplier.n_i-1)) );

diff --git a/src/ecc/formal/properties/ecc_reduced_instantiations.sv b/src/ecc/formal/properties/ecc_reduced_instantiations.sv
@@ -51,8 +51,8 @@ module ecc_reduced_instantiations #(
 );
 
 ecc_montgomerymultiplier #(
-        .REG_SIZE(48),
-        .RADIX(4)
+        .REG_SIZE(16),
+        .RADIX(2)
         )
         ecc_montmult_reduced (
         // Clock and reset.

diff --git a/src/ecc/formal/properties/fv_dsa_ctrl_constraints.sv b/src/ecc/formal/properties/fv_dsa_ctrl_constraints.sv
@@ -101,12 +101,12 @@ end
 
 
     property no_cmd_when_not_ready_p;
-        !fv_new_inp 
+        (ecc_dsa_ctrl.prog_cntr < DSA_NOP)
         |->
         hwif_out.ECC_CTRL.CTRL.value == '0;
     endproperty
 
-    no_cmd: assume property(no_cmd_when_not_ready_p);
+    no_cmd_a: assume property(no_cmd_when_not_ready_p);
 
 `ifndef TOP
 

diff --git a/src/ecc/formal/properties/fv_ecc_dsa_ctrl.sv b/src/ecc/formal/properties/fv_ecc_dsa_ctrl.sv
@@ -916,7 +916,7 @@ module fv_ecc_dsa_ctrl_m
     //-------------------------------------------------------//
 
 
-    logic [REG_NUM_DWORDS-1 : 0][RADIX-1:0] privkey_reg;
+    logic [REG_NUM_DWORDS-1 : 0][DATA_WIDTH-1:0] privkey_reg;
     for(genvar i=0;i< REG_NUM_DWORDS;i++) begin
         assign privkey_reg[i] = hwif_out.ECC_PRIVKEY_IN[(REG_NUM_DWORDS-1)-i].PRIVKEY_IN.value;
     end

diff --git a/src/ecc/formal/properties/fv_ecc_fau.sv b/src/ecc/formal/properties/fv_ecc_fau.sv
@@ -75,15 +75,15 @@ module fv_ecc_fau_m #(
 
         mult_pulse_a: assert property(disable iff(!rst_n) mult_pulse_p);
 
-
+     `ifdef TOP
     //Once edge triggered from next cycle on it stays out until there is an another mult cmd    
          property no_mult_edge_p;
             ecc_fau.mult_start_edge
             |=>
             !ecc_fau.mult_start_edge s_until_with mult_en_i;
         endproperty
         no_mult_edge_a: assert property(disable iff(!rst_n)no_mult_edge_p);
-
+     `endif 
 
     //When ever add_en_i is triggered, it would just generate one pulse
          property add_pulse_p;
@@ -97,14 +97,15 @@ module fv_ecc_fau_m #(
         add_pulse_a: assert property(disable iff(!rst_n) add_pulse_p);
 
 
+    `ifdef TOP
     //Once edge triggered from next cycle on it stays out until there is an another add cmd
         property no_add_edge_p;
             ecc_fau.add_start_edge
             |=>
             !ecc_fau.add_start_edge s_until_with add_en_i;
         endproperty
         no_add_edge_a: assert property(disable iff(!rst_n)no_add_edge_p);
-
+    `endif
 
      //Primary outputs connected to primary outputs of submodules
         property outputs_p;

diff --git a/src/ecc/formal/properties/fv_ecc_hmac_drbg_interface.sv b/src/ecc/formal/properties/fv_ecc_hmac_drbg_interface.sv
@@ -23,7 +23,7 @@
 module fv_ecc_hmac_drbg_interface_m#(
     parameter                  REG_SIZE       = 384,
     parameter [REG_SIZE-1 : 0] GROUP_ORDER    = 384'hffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52973,
-    parameter [147 : 0]        LFSR_INIT_SEED = 148'h6_04E7_A407_54F1_4487_A021_11AC_D0DF_8C55_57A0   // a random value
+    parameter [REG_SIZE-1 : 0]        LFSR_INIT_SEED = 384'hc48555929cd58779f4819c1e6570c2ef20bccd503284e2d366f3273a66e9719b07ac999c80740d6277af88ceb4c3029c   // a random value
     )
     (
     // Clock and reset.
@@ -73,17 +73,18 @@ module fv_ecc_hmac_drbg_interface_m#(
  // Helper logic for lfsr_seed
  ///////////////////////////////////////////
 
-            logic [147 : 0]         fv_lfsr_seed_reg; 
+            logic [383 : 0]         fv_lfsr_seed_reg; 
             logic [383:0]           fv_hmac_drbg_result_reg;
             logic                   fv_hmac_drbg_valid_reg;
         always_ff @(posedge clk, negedge rst_n) begin
-            if(!rst_n)
+            if(!rst_n )
                 fv_lfsr_seed_reg <= LFSR_INIT_SEED;
             else begin
+
                 fv_hmac_drbg_valid_reg <= `hiearchy.hmac_drbg_valid;
                 fv_hmac_drbg_result_reg <= `hiearchy.hmac_drbg_result;
-                if(`hiearchy.state_reg == LFSR_ST && `hiearchy.hmac_drbg_valid && !fv_hmac_drbg_valid_reg) begin
-                    fv_lfsr_seed_reg <= `hiearchy.hmac_drbg_result[147 : 0];
+                 if(`hiearchy.state_reg == LFSR_ST && `hiearchy.hmac_drbg_valid && !fv_hmac_drbg_valid_reg) begin
+                    fv_lfsr_seed_reg <= `hiearchy.hmac_drbg_result;
                 end
             end
         end
@@ -117,14 +118,14 @@ module fv_ecc_hmac_drbg_interface_m#(
             `hiearchy.hmac_drbg_init == 1 &&
             `hiearchy.hmac_drbg_next == 0 &&
             `hiearchy.hmac_drbg_entropy == IV &&
-            `hiearchy.hmac_lfsr_seed == (fv_lfsr_seed_reg) ^ `hiearchy.counter_nonce[147:0] &&
+            `hiearchy.hmac_lfsr_seed == (fv_lfsr_seed_reg) ^ `hiearchy.counter_nonce &&
             `hiearchy.hmac_drbg_nonce == $past(`hiearchy.counter_nonce) &&
              ready == 0 &&
             lambda == $past(lambda) &&
             scalar_rnd == $past(scalar_rnd) &&
             masking_rnd == $past(masking_rnd) &&
-            drbg == $past(drbg)
-            ;
+            drbg == $past(drbg);
+
 
         endproperty
 
@@ -141,7 +142,7 @@ module fv_ecc_hmac_drbg_interface_m#(
             `hiearchy.hmac_drbg_init == 0 &&
             `hiearchy.hmac_drbg_next == 0 &&
             `hiearchy.hmac_drbg_entropy == '0 &&
-            `hiearchy.hmac_lfsr_seed == (fv_lfsr_seed_reg) ^ `hiearchy.counter_nonce[147:0] &&
+            `hiearchy.hmac_lfsr_seed == (fv_lfsr_seed_reg) ^ `hiearchy.counter_nonce &&
             `hiearchy.hmac_drbg_nonce == (`hiearchy.counter_nonce_reg) &&
             lambda == $past(lambda) &&
             scalar_rnd == $past(scalar_rnd) &&
@@ -163,7 +164,7 @@ module fv_ecc_hmac_drbg_interface_m#(
             `hiearchy.hmac_drbg_entropy == IV &&
             ready == 0 &&
             `hiearchy.hmac_drbg_nonce == `hiearchy.counter_nonce_reg &&
-            `hiearchy.hmac_lfsr_seed == $past(`hiearchy.hmac_drbg_result[147 : 0]) ^ `hiearchy.counter_nonce[147 : 0] &&
+            `hiearchy.hmac_lfsr_seed == $past(`hiearchy.hmac_drbg_result) ^ `hiearchy.counter_nonce &&
             lambda == $past(lambda) &&
             scalar_rnd == $past(scalar_rnd) &&
             masking_rnd == $past(masking_rnd) &&
@@ -184,7 +185,7 @@ module fv_ecc_hmac_drbg_interface_m#(
             `hiearchy.hmac_drbg_entropy == IV &&
             ready == 0 &&
             `hiearchy.hmac_drbg_nonce == `hiearchy.counter_nonce_reg &&
-            `hiearchy.hmac_lfsr_seed == (fv_lfsr_seed_reg) ^ `hiearchy.counter_nonce[147:0] &&
+            `hiearchy.hmac_lfsr_seed == (fv_lfsr_seed_reg) ^ `hiearchy.counter_nonce &&
             lambda == $past(lambda) &&
             scalar_rnd == $past(scalar_rnd) &&
             masking_rnd == $past(masking_rnd) &&
@@ -205,7 +206,7 @@ module fv_ecc_hmac_drbg_interface_m#(
             `hiearchy.hmac_drbg_entropy == IV &&
             ready == 0 &&
             `hiearchy.hmac_drbg_nonce == `hiearchy.counter_nonce_reg &&
-            `hiearchy.hmac_lfsr_seed == fv_lfsr_seed_reg ^ `hiearchy.counter_nonce[147 : 0] &&
+            `hiearchy.hmac_lfsr_seed == fv_lfsr_seed_reg ^ `hiearchy.counter_nonce &&
             lambda == $past(`hiearchy.hmac_drbg_result) &&
             scalar_rnd == $past(scalar_rnd) &&
             masking_rnd == $past(masking_rnd) &&
@@ -226,7 +227,7 @@ module fv_ecc_hmac_drbg_interface_m#(
             `hiearchy.hmac_drbg_entropy == IV &&
             ready == 0 &&
             `hiearchy.hmac_drbg_nonce == `hiearchy.counter_nonce_reg &&
-            `hiearchy.hmac_lfsr_seed == (fv_lfsr_seed_reg) ^ `hiearchy.counter_nonce[147:0] &&
+            `hiearchy.hmac_lfsr_seed == (fv_lfsr_seed_reg) ^ `hiearchy.counter_nonce &&
             lambda == $past(lambda) &&
             scalar_rnd == $past(scalar_rnd) &&
             masking_rnd == $past(masking_rnd) &&
@@ -246,7 +247,7 @@ module fv_ecc_hmac_drbg_interface_m#(
             `hiearchy.hmac_drbg_entropy == '0 &&
             ready == 0 &&
             `hiearchy.hmac_drbg_nonce == `hiearchy.counter_nonce_reg &&
-            `hiearchy.hmac_lfsr_seed == (fv_lfsr_seed_reg) ^ `hiearchy.counter_nonce[147:0] &&
+            `hiearchy.hmac_lfsr_seed == (fv_lfsr_seed_reg) ^ `hiearchy.counter_nonce &&
             lambda == $past(lambda) &&
             scalar_rnd == $past(`hiearchy.hmac_drbg_result) &&
             masking_rnd == $past(masking_rnd) &&
@@ -267,7 +268,7 @@ module fv_ecc_hmac_drbg_interface_m#(
             `hiearchy.hmac_drbg_entropy == IV &&
             ready == 0 &&
             `hiearchy.hmac_drbg_nonce == `hiearchy.counter_nonce_reg &&
-            `hiearchy.hmac_lfsr_seed == (fv_lfsr_seed_reg) ^ `hiearchy.counter_nonce[147:0] &&
+            `hiearchy.hmac_lfsr_seed == (fv_lfsr_seed_reg) ^ `hiearchy.counter_nonce &&
             lambda == $past(lambda) &&
             scalar_rnd == $past(scalar_rnd) &&
             masking_rnd == $past(masking_rnd) &&
@@ -286,7 +287,7 @@ module fv_ecc_hmac_drbg_interface_m#(
             `hiearchy.hmac_drbg_next == 1 &&
             `hiearchy.hmac_drbg_entropy == IV &&
             ready == 0 &&
-            `hiearchy.hmac_lfsr_seed == fv_lfsr_seed_reg ^ `hiearchy.counter_nonce[147 : 0] &&
+            `hiearchy.hmac_lfsr_seed == fv_lfsr_seed_reg ^ `hiearchy.counter_nonce &&
             `hiearchy.hmac_drbg_nonce == `hiearchy.counter_nonce_reg &&
              lambda == $past(lambda) &&
             scalar_rnd == $past(scalar_rnd) &&
@@ -306,7 +307,7 @@ module fv_ecc_hmac_drbg_interface_m#(
             `hiearchy.hmac_drbg_next == 0 &&
             ready == 0 &&
             `hiearchy.hmac_drbg_entropy == keygen_seed &&
-            `hiearchy.hmac_lfsr_seed == fv_lfsr_seed_reg ^ `hiearchy.counter_nonce[147 : 0] &&
+            `hiearchy.hmac_lfsr_seed == fv_lfsr_seed_reg ^ `hiearchy.counter_nonce &&
             `hiearchy.hmac_drbg_nonce == keygen_nonce &&
              lambda == $past(lambda) &&
             scalar_rnd == $past(scalar_rnd) &&
@@ -327,7 +328,7 @@ module fv_ecc_hmac_drbg_interface_m#(
             `hiearchy.hmac_drbg_entropy == privKey  &&
             ready == 0 &&
             `hiearchy.hmac_drbg_nonce == hashed_msg &&
-            `hiearchy.hmac_lfsr_seed == fv_lfsr_seed_reg ^ `hiearchy.counter_nonce[147 : 0] &&
+            `hiearchy.hmac_lfsr_seed == fv_lfsr_seed_reg ^ `hiearchy.counter_nonce &&
             masking_rnd == $past(`hiearchy.hmac_drbg_result) &&
              lambda == $past(lambda) &&
             scalar_rnd == $past(scalar_rnd) &&
@@ -347,7 +348,7 @@ module fv_ecc_hmac_drbg_interface_m#(
             `hiearchy.hmac_drbg_entropy == IV &&
             ready == 0 &&
             `hiearchy.hmac_drbg_nonce == `hiearchy.counter_nonce_reg &&
-            `hiearchy.hmac_lfsr_seed == (fv_lfsr_seed_reg) ^ `hiearchy.counter_nonce[147:0] &&
+            `hiearchy.hmac_lfsr_seed == (fv_lfsr_seed_reg) ^ `hiearchy.counter_nonce &&
             lambda == $past(lambda) &&
             scalar_rnd == $past(scalar_rnd) &&
             masking_rnd == $past(masking_rnd) &&
@@ -367,7 +368,7 @@ module fv_ecc_hmac_drbg_interface_m#(
             `hiearchy.hmac_drbg_entropy == '0 &&
             ready == 0 &&
             `hiearchy.hmac_drbg_nonce == `hiearchy.counter_nonce_reg &&
-            `hiearchy.hmac_lfsr_seed == (fv_lfsr_seed_reg) ^ `hiearchy.counter_nonce[147:0] &&
+            `hiearchy.hmac_lfsr_seed == (fv_lfsr_seed_reg) ^ `hiearchy.counter_nonce &&
             lambda == $past(lambda) &&
             scalar_rnd == $past(scalar_rnd) &&
             masking_rnd == $past(masking_rnd) &&
@@ -386,7 +387,7 @@ module fv_ecc_hmac_drbg_interface_m#(
             `hiearchy.hmac_drbg_entropy ==  keygen_seed &&
             ready == 0 &&
             `hiearchy.hmac_drbg_nonce == keygen_nonce &&
-            `hiearchy.hmac_lfsr_seed == (fv_lfsr_seed_reg) ^ `hiearchy.counter_nonce[147:0] &&
+            `hiearchy.hmac_lfsr_seed == (fv_lfsr_seed_reg) ^ `hiearchy.counter_nonce &&
             lambda == $past(lambda) &&
             scalar_rnd == $past(scalar_rnd) &&
             masking_rnd == $past(masking_rnd) &&
@@ -408,7 +409,7 @@ module fv_ecc_hmac_drbg_interface_m#(
             `hiearchy.hmac_drbg_entropy == '0 &&
             ready == 0 &&
             `hiearchy.hmac_drbg_nonce == `hiearchy.counter_nonce_reg &&
-            `hiearchy.hmac_lfsr_seed == (fv_lfsr_seed_reg) ^ `hiearchy.counter_nonce[147:0] &&
+            `hiearchy.hmac_lfsr_seed == (fv_lfsr_seed_reg) ^ `hiearchy.counter_nonce &&
              lambda == $past(lambda) &&
             scalar_rnd == $past(scalar_rnd) &&
             masking_rnd == $past(masking_rnd) &&
@@ -428,7 +429,7 @@ module fv_ecc_hmac_drbg_interface_m#(
             `hiearchy.hmac_drbg_entropy == privKey &&
             ready == 0 &&
             `hiearchy.hmac_drbg_nonce == hashed_msg &&
-            `hiearchy.hmac_lfsr_seed == (fv_lfsr_seed_reg) ^ `hiearchy.counter_nonce[147:0] &&
+            `hiearchy.hmac_lfsr_seed == (fv_lfsr_seed_reg) ^ `hiearchy.counter_nonce &&
             lambda == $past(lambda) &&
             scalar_rnd == $past(scalar_rnd) &&
             masking_rnd == $past(masking_rnd) &&
@@ -447,7 +448,7 @@ module fv_ecc_hmac_drbg_interface_m#(
             `hiearchy.hmac_drbg_entropy == '0 &&
             ready == 1 &&
             `hiearchy.hmac_drbg_nonce == `hiearchy.counter_nonce_reg &&
-            `hiearchy.hmac_lfsr_seed == (fv_lfsr_seed_reg) ^ `hiearchy.counter_nonce[147:0] &&
+            `hiearchy.hmac_lfsr_seed == (fv_lfsr_seed_reg) ^ `hiearchy.counter_nonce &&
             lambda == $past(lambda) &&
             scalar_rnd == $past(scalar_rnd) &&
             masking_rnd == $past(masking_rnd) &&
@@ -518,7 +519,8 @@ endmodule
 
 bind ecc_hmac_drbg_interface fv_ecc_hmac_drbg_interface_m#(
         .REG_SIZE(REG_SIZE),
-        .GROUP_ORDER(GROUP_ORDER)
+        .GROUP_ORDER(GROUP_ORDER),
+        .LFSR_INIT_SEED(LFSR_INIT_SEED)
         )    
         fv_ecc_hmac_drbg_interface (
         .clk(clk),

diff --git a/src/ecc/formal/properties/fv_montmultiplier.sv b/src/ecc/formal/properties/fv_montmultiplier.sv
@@ -46,7 +46,7 @@ default clocking default_clk @(posedge clk); endclocking
 //-------------------------------------------------------//
 
 
-localparam MULT_DLY = 40; // Defines after start how many cycles ready would stay deasserted.
+localparam MULT_DLY = 28; // Defines after start how many cycles ready would stay deasserted.
 
 
 localparam  int unsigned S_NUM =  ((REG_SIZE + RADIX - 1) / RADIX) + 1; 
@@ -113,11 +113,12 @@ property multi_0_p(prime_i, mu_i,r_inv);
     opb_i <= 4'hf &&
     start_i
     ##0 (1'b1, temp = (48'(32'(opa_i*opb_i)*r_inv)%n_i)) 
+    ##1 ready_o[->1]  
     |->
-    ##16 
-    (p_o == temp) &&
-    ready_o;
-    endproperty
+
+    p_o == temp; 
+endproperty
+
 
 
 /********For inp value less than 8 bits ******/
@@ -131,12 +132,12 @@ property multi_1_p(prime_i, mu_i,r_inv);
     opb_i > 4'hf &&
      start_i
     ##0 (1'b1, temp = (48'(32'(opa_i*opb_i)*r_inv)%n_i))  
-
+     ##1 ready_o[->1]  
     |->
-    ##16 
-    (p_o == temp) &&
-    ready_o;
-    endproperty
+
+    p_o == temp; 
+endproperty
+
 
 
 /********For inp value less than 12 bits ******/
@@ -150,31 +151,31 @@ property multi_2_p(prime_i, mu_i,r_inv);
     opb_i > 8'hff &&
      start_i
     ##0 (1'b1, temp = (48'(32'(opa_i*opb_i)*r_inv)%n_i))  
+    ##1 ready_o[->1]  
     |->
-    ##16 //for 16 bit just gave a slack
-    (p_o[0] == temp[0]) &&
-    ready_o;
-    endproperty
-
+
+    p_o == temp; 
+endproperty
 /********For inp value all bits ******/
 property multi_p(prime_i, mu_i,r_inv);
     logic [REG_SIZE-1:0] temp; 
     n_i == prime_i &&
     n_prime_i == mu_i &&
     start_i
     ##0 (1'b1, temp = (48'(32'(opa_i*opb_i)*r_inv)%n_i))  
+
+    ##1 ready_o[->1]  
     |->
-    ##16 //for 16 bit just gave a slack
-    p_o == temp &&
-    ready_o;
-    endproperty
+
+    p_o == temp; 
+endproperty
 
 logic [4:0][REG_SIZE-1:0] prime;
 logic [4:0][RADIX-1:0] mu_word;
 logic [4:0][REG_SIZE-1:0] rinv;
 assign prime ={16'hfceb,16'hfcfb,16'hfd0d,16'hfd0f,16'hfd19};
-assign mu_word = {4'hd,4'hd,4'hb,4'h1,4'h7};
-assign rinv ={16'hc0ea,16'he269,16'hcc03,16'h1a92,16'h4e28};
+assign mu_word = {2'd1,2'd1,2'd3,2'd1,2'd3};
+assign rinv ={16'hce7,16'h92b3,16'h38e5,16'h6a48,16'h3b87};
 
 genvar i;
 for(i=0;i<5;i++) begin
@@ -192,7 +193,7 @@ end
 property no_ready_p;
     start_i
     |=>
-    !ready_o[*15];
+    !ready_o[*MULT_DLY-1];
 endproperty
 
 no_ready_a: assert property(disable iff(!rst_n)no_ready_p);