Merged PR 118346: added SVA and coverage for modular operations

added SVA and coverage for modular operations Related work items: #520637
nquarton · Aug 14, 2023 · 3c8ae28 · 3c8ae28
1 parent 9aa732e
commit 3c8ae28
Show file tree

Hide file tree

Showing 2 changed files with 68 additions and 1 deletion.
diff --git a/src/ecc/coverage/ecc_top_cov_if.sv b/src/ecc/coverage/ecc_top_cov_if.sv
@@ -41,6 +41,42 @@ interface ecc_top_cov_if
     logic pubkey_input_invalid;
     logic signing_process;
     logic verifying_process;
+
+
+    logic mod_p_q;
+    logic add_en;
+    logic add_sub_i;
+    logic [383 : 0] add_res0;
+    logic add_cout0;
+    logic add_cout1;
+    logic add_res_less_than_prime;
+    logic add_res_greater_than_prime;
+    logic add_res_greater_than_384_bit;
+
+    logic PE_UNITS;
+    logic mult_final_subtraction;
+
+    assign mod_p_q = ecc_top.ecc_dsa_ctrl_i.ecc_arith_unit_i.mod_p_q;
+    assign add_en = ecc_top.ecc_dsa_ctrl_i.ecc_arith_unit_i.ecc_fau_i.add_en_i;
+    assign add_sub_i = ecc_top.ecc_dsa_ctrl_i.ecc_arith_unit_i.ecc_fau_i.sub_i;
+    assign add_res0 = ecc_top.ecc_dsa_ctrl_i.ecc_arith_unit_i.ecc_fau_i.i_ADDER_SUBTRACTOR.r0_reg;
+    assign add_cout0 = ecc_top.ecc_dsa_ctrl_i.ecc_arith_unit_i.ecc_fau_i.i_ADDER_SUBTRACTOR.carry0_reg;
+    assign add_cout1 = ecc_top.ecc_dsa_ctrl_i.ecc_arith_unit_i.ecc_fau_i.i_ADDER_SUBTRACTOR.carry1;
+    assign add_res_less_than_prime = ((add_cout0 == 1'b0) & (add_res0 < ecc_top.ecc_dsa_ctrl_i.ecc_arith_unit_i.ecc_fau_i.prime_i));
+    assign add_res_greater_than_prime = ((add_cout0 == 1'b0) & (add_res0 >= ecc_top.ecc_dsa_ctrl_i.ecc_arith_unit_i.ecc_fau_i.prime_i));
+    assign add_res_greater_than_384_bit = (add_cout0 == 1'b1);
+
+    assign PE_UNITS = ecc_top.ecc_dsa_ctrl_i.ecc_arith_unit_i.ecc_fau_i.i_MULTIPLIER.PE_UNITS;
+    always_ff @(posedge clk) begin
+        if (!reset_n) begin
+            mult_final_subtraction <= '0;
+        end
+        else if (ecc_top.ecc_dsa_ctrl_i.ecc_arith_unit_i.ecc_fau_i.i_MULTIPLIER.ready_o) begin
+            mult_final_subtraction <= ecc_top.ecc_dsa_ctrl_i.ecc_arith_unit_i.ecc_fau_i.i_MULTIPLIER.sub_b_o[2*(PE_UNITS+1)];
+        end
+    end
+
+
 
     assign ecc_cmd = ecc_top.ecc_dsa_ctrl_i.cmd_reg;
     assign pcr_sign_mode = ecc_top.ecc_dsa_ctrl_i.pcr_sign_mode;
@@ -102,6 +138,14 @@ interface ecc_top_cov_if
         error_signing_cp: cross error_flag, signing_process;
         error_verifying_cp: cross error_flag, verifying_process;
 
+        // modular operation
+        mult_final_subtraction_cp: coverpoint mult_final_subtraction;
+        add_carry_cp: cross mod_p_q, add_sub_i, add_cout0, add_cout1;
+        add_result_less_than_prime_cp: cross mod_p_q, add_sub_i, add_res_less_than_prime;
+        add_result_greater_than_prime_cp: cross mod_p_q, add_sub_i, add_res_greater_than_prime;
+        add_result_greater_than_384_bit_cp: cross mod_p_q, add_sub_i, add_res_greater_than_384_bit;
+
+
     endgroup
 
     ecc_top_cov_grp ecc_top_cov_grp1 = new();

diff --git a/src/integration/asserts/caliptra_top_sva.sv b/src/integration/asserts/caliptra_top_sva.sv
@@ -501,8 +501,31 @@ module caliptra_top_sva
                                     @(posedge `SVA_RDC_CLK)
                                     `ECC_PATH.dsa_valid_reg |-> `ECC_PATH.dsa_ready_reg 
                                     )
-                        else $display("SVA ERROR: ECC VALID flag mismatch!");                         
+                        else $display("SVA ERROR: ECC VALID flag mismatch!");      
 
+  //SVA for modular operations
+  ecc_opa_input:        assert property (
+                                      @(posedge `SVA_RDC_CLK)
+                                      (`ECC_PATH.ecc_arith_unit_i.ecc_fau_i.add_en_i | `ECC_PATH.ecc_arith_unit_i.ecc_fau_i.mult_en_i) |-> (`ECC_PATH.ecc_arith_unit_i.ecc_fau_i.opa_i < `ECC_PATH.ecc_arith_unit_i.ecc_fau_i.prime_i)
+                                      )
+                          else $display("SVA ERROR: ECC opa input is not valid!"); 
+
+  ecc_opb_input:        assert property (
+                                      @(posedge `SVA_RDC_CLK)
+                                      (`ECC_PATH.ecc_arith_unit_i.ecc_fau_i.add_en_i | `ECC_PATH.ecc_arith_unit_i.ecc_fau_i.mult_en_i) |-> (`ECC_PATH.ecc_arith_unit_i.ecc_fau_i.opb_i < `ECC_PATH.ecc_arith_unit_i.ecc_fau_i.prime_i)
+                                      )
+                          else $display("SVA ERROR: ECC opb input is not valid!"); 
 
+  ecc_add_result:       assert property (
+                                      @(posedge `SVA_RDC_CLK)
+                                      `ECC_PATH.ecc_arith_unit_i.ecc_instr_s.opcode.add_we |-> (`ECC_PATH.ecc_arith_unit_i.add_res_s < `ECC_PATH.ecc_arith_unit_i.adder_prime)
+                                      )
+                          else $display("SVA ERROR: ECC adder result is not valid!"); 
+
+  ecc_mult_result:       assert property (
+                                      @(posedge `SVA_RDC_CLK)
+                                      `ECC_PATH.ecc_arith_unit_i.ecc_instr_s.opcode.mult_we |-> (`ECC_PATH.ecc_arith_unit_i.mult_res_s < `ECC_PATH.ecc_arith_unit_i.adder_prime)
+                                      )
+                          else $display("SVA ERROR: ECC multiplier result is not valid!"); 
 endmodule