-
Notifications
You must be signed in to change notification settings - Fork 31
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #3 from ludwigatlubis/ecc
Added formal folder with readme and pdf
- Loading branch information
Showing
26 changed files
with
9,593 additions
and
0 deletions.
There are no files selected for viewing
Binary file not shown.
45 changes: 45 additions & 0 deletions
45
src/ecc/formal/properties/coverpoints/fv_add_sub_alter_coverpoints.sv
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,45 @@ | ||
| // ------------------------------------------------- | ||
| // Contact: contact@lubis-eda.com | ||
| // Author: Tobias Ludwig, Michael Schwarz | ||
| // ------------------------------------------------- | ||
| // SPDX-License-Identifier: Apache-2.0 | ||
| // | ||
| // Licensed under the Apache License, Version 2.0 (the "License"); | ||
| // you may not use this file except in compliance with the License. | ||
| // You may obtain a copy of the License at | ||
| // | ||
| // http://www.apache.org/licenses/LICENSE-2.0 | ||
| // | ||
| // Unless required by applicable law or agreed to in writing, software | ||
| // distributed under the License is distributed on an "AS IS" BASIS, | ||
| // WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. | ||
| // See the License for the specific language governing permissions and | ||
| // limitations under the License. | ||
| // | ||
| module fv_add_sub_alter_coverpoints_m( | ||
| input logic clk, | ||
| input logic reset_n, | ||
| input logic zeroize | ||
| ); | ||
|
|
||
| default clocking default_clk @(posedge clk); endclocking | ||
|
|
||
| //Cover zeroize: | ||
| cover_zeroize: cover property(disable iff(!reset_n) ecc_add_sub_mod_alter.zeroize ); | ||
|
|
||
| cover_prime_p: cover property(disable iff(!reset_n) (ecc_add_sub_mod_alter.prime_i==384'hfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000ffffffff)); | ||
| cover_prime_q: cover property(disable iff(!reset_n)(ecc_add_sub_mod_alter.prime_i==384'hffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52973)); | ||
| cover_add_en: cover property(disable iff(!reset_n) ecc_add_sub_mod_alter.add_en_i==1); | ||
| cover_add_disable: cover property(disable iff(!reset_n) ecc_add_sub_mod_alter.add_en_i==0); | ||
| cover_r0_0: cover property(disable iff(!reset_n || zeroize) ecc_add_sub_mod_alter.r0=='0); | ||
| cover_r0_1: cover property(disable iff(!reset_n || zeroize) ecc_add_sub_mod_alter.r0=='1); | ||
| cover_r0_greater_prime: cover property(disable iff(!reset_n || zeroize) ecc_add_sub_mod_alter.r0 > ecc_add_sub_mod_alter.prime_i); | ||
|
|
||
|
|
||
| endmodule | ||
|
|
||
| bind ecc_add_sub_mod_alter fv_add_sub_alter_coverpoints_m fv_add_sub_alter_coverpoints( | ||
| .clk(clk), | ||
| .reset_n(reset_n), | ||
| .zeroize(zeroize) | ||
| ); |
86 changes: 86 additions & 0 deletions
86
src/ecc/formal/properties/coverpoints/fv_arith_unit_coverpoints.sv
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,86 @@ | ||
| // ------------------------------------------------- | ||
| // Contact: contact@lubis-eda.com | ||
| // Author: Tobias Ludwig, Michael Schwarz | ||
| // ------------------------------------------------- | ||
| // SPDX-License-Identifier: Apache-2.0 | ||
| // | ||
| // Licensed under the Apache License, Version 2.0 (the "License"); | ||
| // you may not use this file except in compliance with the License. | ||
| // You may obtain a copy of the License at | ||
| // | ||
| // http://www.apache.org/licenses/LICENSE-2.0 | ||
| // | ||
| // Unless required by applicable law or agreed to in writing, software | ||
| // distributed under the License is distributed on an "AS IS" BASIS, | ||
| // WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. | ||
| // See the License for the specific language governing permissions and | ||
| // limitations under the License. | ||
| // | ||
| module fv_ecc_arith_unit_coverpoints_m( | ||
| input logic clk, | ||
| input logic reset_n, | ||
| input logic zeroize | ||
| ); | ||
|
|
||
| default clocking default_clk @(posedge clk); endclocking | ||
|
|
||
| //Cover zeroize: | ||
| cover_zeroize: cover property(disable iff(!reset_n) ecc_arith_unit.zeroize ); | ||
|
|
||
| //cover wea | ||
| cover_wea: cover property(disable iff(!reset_n) ( | ||
| ecc_arith_unit.ecc_instr_s.opcode.add_en | ||
| ##3 | ||
| ecc_arith_unit.ram_tdp_file_i.wea)); | ||
|
|
||
| //cover web | ||
| cover_wem: cover property(disable iff(!reset_n) | ||
| ecc_arith_unit.ecc_instr_s.opcode.mult_en | ||
| ##41 | ||
| ecc_arith_unit.web_mux_s); | ||
|
|
||
| //cover req_digit when keygen cmd | ||
| cover_req_digit_keygen: cover property(disable iff(!reset_n) | ||
| ecc_arith_unit.ecc_cmd_i== 3'b001 //KEYGEN_CMD | ||
| ##1 | ||
| ecc_arith_unit.req_digit[->576]); | ||
|
|
||
| //cover req_digit when signing cmd | ||
| cover_req_digit_signing: cover property(disable iff(!reset_n) | ||
| ecc_arith_unit.ecc_cmd_i==3'b010 //SIGN_CMD | ||
| ##1 | ||
| ecc_arith_unit.req_digit[->576]); | ||
|
|
||
|
|
||
| //cover wr_op_sel_i when ecc_cmd_i is received | ||
| cover_wr_op_sel_i: cover property(disable iff(!reset_n) | ||
| (ecc_arith_unit.ecc_cmd_i!=3'b0 && !ecc_arith_unit.wr_op_sel_i)); | ||
|
|
||
| //cover wr_en_i when ecc_cmd_i is received | ||
| cover_wr_en_i: cover property(disable iff(!reset_n || zeroize) | ||
| (ecc_arith_unit.ecc_cmd_i!=3'b0 && !ecc_arith_unit.wr_en_i)); | ||
|
|
||
| //cover sca_en_i | ||
| cover_sca_en_always: cover property(disable iff(!reset_n || zeroize) | ||
| ecc_arith_unit.sca_en_i ==1); | ||
|
|
||
| //cover digit_in be the MSB bit of secret key | ||
| cover_digit_in_msb_secret_key: cover property(disable iff(!reset_n || zeroize) | ||
| ecc_arith_unit.req_digit | ||
| ##1 | ||
| ecc_arith_unit.digit_in == $past(ecc_arith_unit.secret_key[(ecc_arith_unit.REG_SIZE+ecc_arith_unit.RND_SIZE)-1])); | ||
|
|
||
| //cover secret key is shifted with req_digit | ||
| cover_req_digit_secret_key: cover property(disable iff(!reset_n || zeroize) | ||
| ecc_arith_unit.req_digit | ||
| ##1 | ||
| ecc_arith_unit.secret_key == $past({ecc_arith_unit.secret_key[(ecc_arith_unit.REG_SIZE+ecc_arith_unit.RND_SIZE)-2 : 0], ecc_arith_unit.secret_key[(ecc_arith_unit.REG_SIZE+ecc_arith_unit.RND_SIZE)-1]})); | ||
|
|
||
|
|
||
| endmodule | ||
|
|
||
| bind ecc_arith_unit fv_ecc_arith_unit_coverpoints_m fv_ecc_arith_unit_coverpoints( | ||
| .clk(clk), | ||
| .reset_n(reset_n), | ||
| .zeroize(zeroize) | ||
| ); |
130 changes: 130 additions & 0 deletions
130
src/ecc/formal/properties/coverpoints/fv_ecc_dsa_ctrl_coverpoints.sv
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,130 @@ | ||
| // ------------------------------------------------- | ||
| // Contact: contact@lubis-eda.com | ||
| // Author: Tobias Ludwig, Michael Schwarz | ||
| // ------------------------------------------------- | ||
| // SPDX-License-Identifier: Apache-2.0 | ||
| // | ||
| // Licensed under the Apache License, Version 2.0 (the "License"); | ||
| // you may not use this file except in compliance with the License. | ||
| // You may obtain a copy of the License at | ||
| // | ||
| // http://www.apache.org/licenses/LICENSE-2.0 | ||
| // | ||
| // Unless required by applicable law or agreed to in writing, software | ||
| // distributed under the License is distributed on an "AS IS" BASIS, | ||
| // WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. | ||
| // See the License for the specific language governing permissions and | ||
| // limitations under the License. | ||
| // | ||
| module fv_ecc_dsa_ctrl_coverpoints( | ||
| input logic clk, | ||
| input logic reset_n, | ||
| input logic zeroize | ||
| ); | ||
|
|
||
|
|
||
| default clocking default_clk @(posedge clk); endclocking | ||
|
|
||
| //cover zeroize | ||
| cover_zeroize: cover property(disable iff(!reset_n) ecc_dsa_ctrl.zeroize_reg ); | ||
|
|
||
| //cover seed_reg | ||
|
|
||
| cover_seed_reg_max: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.seed_reg == 384'hFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF); | ||
| cover_seed_reg_zero: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.seed_reg =='0); | ||
|
|
||
| //cover nonce_reg | ||
|
|
||
|
|
||
| cover_nonce_reg_max: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.nonce_reg== 384'hFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF); | ||
| cover_nonce_reg_zero: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.nonce_reg =='0); | ||
|
|
||
| //cover msg_reg | ||
|
|
||
| cover_msg_reg_max: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.msg_reg == 384'hFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF); | ||
| cover_msg_reg_zero: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.msg_reg =='0); | ||
|
|
||
|
|
||
| //cover privkey_reg | ||
|
|
||
| cover_privkey_reg_less_grp_order: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.privkey_reg < 384'hffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52973); | ||
| cover_privkey_reg_grt_zero: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.privkey_reg >'0); | ||
|
|
||
| //cover scalar_G_reg | ||
|
|
||
| cover_scalar_G_reg_less_grp_order: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.scalar_G_reg < 384'hffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52973); | ||
| cover_scalar_G_reg_grt_zero: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.scalar_G_reg >'0); | ||
| cover_scalar_G_reg_grp_order_1: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.scalar_G_reg == 384'hffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52972); | ||
| cover_scalar_G_reg_1: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.scalar_G_reg == 1); | ||
|
|
||
| //cover scalar_PK_reg | ||
|
|
||
| cover_scalar_PK_reg_less_grp_order: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.scalar_PK_reg < 384'hffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52973); | ||
| cover_scalar_PK_reg_grt_zero: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.scalar_PK_reg >'0); | ||
| cover_scalar_PK_reg_grp_order_1: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.scalar_PK_reg == 384'hffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52972); | ||
| cover_scalar_PK_reg_1: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.scalar_PK_reg == 1); | ||
|
|
||
| //cover r_reg | ||
|
|
||
| cover_r_reg_less_grp_order: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.r_reg < 384'hffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52973); | ||
| cover_r_reg_grt_zero: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.r_reg >'0); | ||
| cover_r_reg_grp_order_1: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.r_reg == 384'hffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52972); | ||
| cover_r_reg_1: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.r_reg == 1); | ||
|
|
||
| //cover s_reg | ||
| cover_s_reg_less_grp_order: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.s_reg < 384'hffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52973); | ||
| cover_s_reg_grt_zero: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.s_reg >'0); | ||
| cover_s_reg_grp_order_1: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.s_reg == 384'hffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52972); | ||
| cover_s_reg_1: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.s_reg == 1); | ||
|
|
||
|
|
||
| //cover IV_reg | ||
| cover_IV_reg_less_grp_order: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.IV_reg < 384'hffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52973); | ||
| cover_IV_reg_grt_zero: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.IV_reg >'0); | ||
| cover_IV_reg_grp_order_1: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.IV_reg == 384'hffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52972); | ||
| cover_IV_reg_1: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.IV_reg == 1); | ||
|
|
||
| //cover pubkeyx_reg | ||
| cover_pubkeyx_reg_less_prime: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.pubkeyx_reg < 384'hfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000ffffffff); | ||
| cover_pubkeyx_reg_zero: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.pubkeyx_reg =='0); | ||
| cover_pubkeyx_reg_prime_1: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.pubkeyx_reg == 384'hfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000fffffffe); | ||
| cover_pubkeyx_reg_grt_prime: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.pubkeyx_reg > 384'hfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000ffffffff); | ||
|
|
||
| //cover pubkeyy_reg | ||
| cover_pubkeyy_reg_less_prime: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.pubkeyy_reg < 384'hfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000ffffffff); | ||
| cover_pubkeyy_reg_zero: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.pubkeyy_reg =='0); | ||
| cover_pubkeyy_reg_prime_1: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.pubkeyy_reg == 384'hfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000fffffffe); | ||
| cover_pubkeyy_reg_grt_prime: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.pubkeyy_reg > 384'hfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000ffffffff); | ||
|
|
||
|
|
||
| //cover scalar_out_reg | ||
| cover_scalar_out_reg_eq_1: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.scalar_out_reg==1); | ||
| cover_scalar_out_reg_grp_order_1: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.scalar_out_reg==384'hffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52972); | ||
| cover_scalar_out_reg_grp_mult: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.scalar_out_reg==(1+((2**192)-1)*384'hffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52973) ); | ||
| cover_scalar_out_reg_grp_order_mult_1: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.scalar_out_reg==(384'hffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52972 +((2**192)-1)*384'hffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52973) ); | ||
|
|
||
|
|
||
|
|
||
| //cover lambda_reg | ||
|
|
||
| cover_lambda_reg_max: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.lambda_reg == 384'hFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF); | ||
| cover_lambda_reg_zero: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.lambda_reg =='0); | ||
|
|
||
|
|
||
|
|
||
| //cover masking_rnd_reg | ||
|
|
||
| cover_masking_rnd_reg_max: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.masking_rnd_reg == 384'hFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF); | ||
| cover_masking_rnd_reg_zero: cover property(disable iff(!reset_n || zeroize) ecc_dsa_ctrl.masking_rnd_reg =='0); | ||
|
|
||
|
|
||
|
|
||
|
|
||
|
|
||
| endmodule | ||
|
|
||
| bind ecc_dsa_ctrl fv_ecc_dsa_ctrl_coverpoints fv_ecc_dsa_ctrl_coverpoints_inst ( | ||
| .clk(clk), | ||
| .reset_n(reset_n), | ||
| .zeroize(ecc_dsa_ctrl.zeroize_reg) | ||
| ); |
49 changes: 49 additions & 0 deletions
49
src/ecc/formal/properties/coverpoints/fv_ecc_montgomerymultiplier_coverpoints.sv
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,49 @@ | ||
| // ------------------------------------------------- | ||
| // Contact: contact@lubis-eda.com | ||
| // Author: Tobias Ludwig, Michael Schwarz | ||
| // ------------------------------------------------- | ||
| // SPDX-License-Identifier: Apache-2.0 | ||
| // | ||
| // Licensed under the Apache License, Version 2.0 (the "License"); | ||
| // you may not use this file except in compliance with the License. | ||
| // You may obtain a copy of the License at | ||
| // | ||
| // http://www.apache.org/licenses/LICENSE-2.0 | ||
| // | ||
| // Unless required by applicable law or agreed to in writing, software | ||
| // distributed under the License is distributed on an "AS IS" BASIS, | ||
| // WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. | ||
| // See the License for the specific language governing permissions and | ||
| // limitations under the License. | ||
| // | ||
| module fv_ecc_montgomerymultiplier_coverpoints_m( | ||
| input logic clk, | ||
| input logic reset_n, | ||
| input logic zeroize | ||
| ); | ||
|
|
||
| default clocking default_clk @(posedge clk); endclocking | ||
|
|
||
| //Cover zeroize: | ||
| 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_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)) ); | ||
| cover_opb_i_prime_minus_1 : cover property(disable iff(!reset_n|| zeroize) (ecc_montgomerymultiplier.opb_i == (ecc_montgomerymultiplier.n_i-1))&&(ecc_montgomerymultiplier.opa_i == '0 || ecc_montgomerymultiplier.opa_i == (ecc_montgomerymultiplier.n_i-1)) ); | ||
| cover_sub_b_o_zero: cover property(disable iff(!reset_n || zeroize) ecc_montgomerymultiplier.ready_o && ecc_montgomerymultiplier.sub_b_o[2*(ecc_montgomerymultiplier.PE_UNITS+1)]==0); | ||
| cover_sub_b_o_one: cover property(disable iff(!reset_n || zeroize) ecc_montgomerymultiplier.ready_o && ecc_montgomerymultiplier.sub_b_o[2*(ecc_montgomerymultiplier.PE_UNITS+1)]== 1); | ||
| cover_p_sub_internal: cover property (disable iff(!reset_n || zeroize) !$past(!reset_n || zeroize) && ecc_montgomerymultiplier.ready_o && (ecc_montgomerymultiplier.p_subtracted_internal == ( ecc_montgomerymultiplier.p_internal - ecc_montgomerymultiplier.n_i))); | ||
|
|
||
|
|
||
|
|
||
| endmodule | ||
|
|
||
| bind ecc_montgomerymultiplier fv_ecc_montgomerymultiplier_coverpoints_m fv_ecc_montgomerymultiplier_coverpoints( | ||
| .clk(clk), | ||
| .reset_n(reset_n), | ||
| .zeroize(zeroize) | ||
| ); |
Oops, something went wrong.