commit 71d29ea84afa6384d059b8a0f3a4da628e8af7b6
author Canberk Topal <ctopal@lowrisc.org> Thu Aug 18 15:40:11 2022 +0100
committer Greg Chadwick <mail@gregchadwick.co.uk> Fri Sep 09 15:21:25 2022 +0100
tree 0e2b588c3e81b82367a51732053573f0a6074216
parent 06154a58679aec61f7cbc79948d08bee8406665f

[otbn,dv] Blanking assertions

Signed-off-by: Canberk Topal <ctopal@lowrisc.org>

hw/ip/otbn/rtl/otbn_alu_bignum.sv

diff --git a/hw/ip/otbn/rtl/otbn_alu_bignum.sv b/hw/ip/otbn/rtl/otbn_alu_bignum.sv
index 980b95d..3298975 100644
--- a/hw/ip/otbn/rtl/otbn_alu_bignum.sv
+++ b/hw/ip/otbn/rtl/otbn_alu_bignum.sv
@@ -844,4 +844,60 @@
   assign reg_intg_violation_err_o = mod_used & |(mod_intg_err);
   `ASSERT_KNOWN(RegIntgErrKnown_A, reg_intg_violation_err_o)
 
+  // Blanking Assertions
+  // adder_x_res related blanking
+  `ASSERT(BlankingBignumAluXOp_A,
+          !expected_adder_x_en |-> {adder_x_op_a_blanked, adder_x_op_b_blanked,adder_x_res} == '0,
+          clk_i, !rst_ni)
+
+  // adder_y_res related blanking
+  `ASSERT(BlankingBignumAluYOpA_A,
+          !expected_adder_y_op_a_en |-> adder_y_op_a_blanked == '0,
+          clk_i, !rst_ni)
+  `ASSERT(BlankingBignumAluYOpShft_A,
+          !expected_adder_y_op_shifter_en |-> adder_y_op_shifter_res_blanked == '0,
+          clk_i, !rst_ni)
+
+  `ASSERT(BlankingBignumAluYResUsed_A,
+          !adder_y_res_used |-> {x_res_operand_a_mux_out, adder_y_op_b} == '0,
+          clk_i, !rst_ni)
+
+  // shifter_res related blanking
+  `ASSERT(BlankingBignumAluShftA_A,
+          !expected_shifter_a_en |-> shifter_operand_a_blanked == '0,
+          clk_i, !rst_ni)
+
+  `ASSERT(BlankingBignumAluShftB_A,
+          !expected_shifter_b_en |-> shifter_operand_b_blanked == '0,
+          clk_i, !rst_ni)
+
+  `ASSERT(BlankingBignumAluShftRes_A,
+          !(expected_shifter_a_en || expected_shifter_b_en) |-> shifter_res == '0,
+          clk_i, !rst_ni)
+
+  // logical_res related blanking
+  `ASSERT(BlankingBignumAluLogicOpA_A,
+          !expected_logic_a_en |-> logical_op_a_blanked == '0,
+          clk_i, !rst_ni)
+
+  `ASSERT(BlankingBignumAluLogicShft_A,
+          !expected_logic_shifter_en |-> logical_op_shifter_res_blanked == '0,
+          clk_i, !rst_ni)
+
+  `ASSERT(BlankingBignumAluLogicRes_A,
+          !(expected_logic_a_en || expected_logic_shifter_en) |-> logical_res == '0,
+          clk_i, !rst_ni)
+
+
+  // MOD ISPR Blanking
+  `ASSERT(BlankingIsprMod_A,
+          !(|mod_wr_en) |-> ispr_mod_bignum_wdata_intg_blanked == '0,
+          clk_i, !rst_ni)
+
+  // ACC ISPR Blanking
+  `ASSERT(BlankingIsprACC_A,
+          !(|ispr_acc_wr_en_o) |-> ispr_acc_bignum_wdata_intg_blanked == '0,
+          clk_i, !rst_ni)
+
+
 endmodule

hw/ip/otbn/rtl/otbn_rf_bignum.sv

diff --git a/hw/ip/otbn/rtl/otbn_rf_bignum.sv b/hw/ip/otbn/rtl/otbn_rf_bignum.sv
index ddb5f32..ebfb10c 100644
--- a/hw/ip/otbn/rtl/otbn_rf_bignum.sv
+++ b/hw/ip/otbn/rtl/otbn_rf_bignum.sv
@@ -163,6 +163,14 @@
   assign intg_err_o = ((|rd_data_a_err) & rd_en_a_i) |
                       ((|rd_data_b_err) & rd_en_b_i);
 
+  `ASSERT(BlankingBignumRegReadA_A,
+          !rd_en_a_i |->  rd_data_a_intg_o == '0,
+          clk_i, !rst_ni)
+
+  `ASSERT(BlankingBignumRegReadB_A,
+          !rd_en_b_i |->  rd_data_b_intg_o == '0,
+          clk_i, !rst_ni)
+
   // Make sure we're not outputting X. This indicates that something went wrong during the initial
   // secure wipe.
   `ASSERT(OtbnRfBignumRdAKnown, rd_en_a_i && !rd_en_a_mismatch |-> !$isunknown(rd_data_a_intg_o))

hw/ip/otbn/rtl/otbn_rf_bignum_ff.sv

diff --git a/hw/ip/otbn/rtl/otbn_rf_bignum_ff.sv b/hw/ip/otbn/rtl/otbn_rf_bignum_ff.sv
index 540b299..29058de 100644
--- a/hw/ip/otbn/rtl/otbn_rf_bignum_ff.sv
+++ b/hw/ip/otbn/rtl/otbn_rf_bignum_ff.sv
@@ -62,6 +62,8 @@
         rf[i][ExtWLEN/2+:ExtWLEN/2] <= wr_data_blanked[ExtWLEN/2+:ExtWLEN/2];
       end
     end
+
+  `ASSERT(BlankingBignumRegWData_A, !(|we_onehot[i]) |-> wr_data_blanked inside {'0, 'x})
   end
 
   // SEC_CM: DATA_REG_SW.SCA