From 098067fa17f6d88c05b462b0877c539dd85b3124 Mon Sep 17 00:00:00 2001 From: advaith_sreevalsan Date: Thu, 23 Nov 2023 18:43:18 +0100 Subject: [PATCH 1/2] sha_masked property suite added to folder --- .../formal/properties/fv_constraints.sv | 85 ++ .../formal/properties/fv_coverpoints.sv | 50 + .../formal/properties/fv_sha512_masked.sv | 919 ++++++++++++++++++ .../formal/properties/fv_sha512_masked_pkg.sv | 197 ++++ src/sha512_masked/formal/readme.md | 66 ++ 5 files changed, 1317 insertions(+) create mode 100644 src/sha512_masked/formal/properties/fv_constraints.sv create mode 100644 src/sha512_masked/formal/properties/fv_coverpoints.sv create mode 100644 src/sha512_masked/formal/properties/fv_sha512_masked.sv create mode 100644 src/sha512_masked/formal/properties/fv_sha512_masked_pkg.sv create mode 100644 src/sha512_masked/formal/readme.md diff --git a/src/sha512_masked/formal/properties/fv_constraints.sv b/src/sha512_masked/formal/properties/fv_constraints.sv new file mode 100644 index 000000000..f3534f5ef --- /dev/null +++ b/src/sha512_masked/formal/properties/fv_constraints.sv @@ -0,0 +1,85 @@ +// ------------------------------------------------- +// 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_constraints_m( + input logic init_cmd, + input logic next_cmd, + input logic reset_n, + input logic clk, + input logic zeroize, + input logic ready, + input logic digest_valid, + input logic [1023 : 0] block_msg, + input logic [73 : 0] lfsr_seed, + input logic [511 : 0] digest, + input logic [1 : 0] mode + ); + + default clocking default_clk @(posedge clk); endclocking + + logic fv_init_reg; + + always @ (posedge clk or negedge reset_n) + begin : init_reg_order + if (!reset_n || zeroize) + fv_init_reg <= 1'b0; + else if (init_cmd) + fv_init_reg <= 1'b1; + end + + + property mode_values; + (sha512_masked_core.mode == 0) || + (sha512_masked_core.mode == 1) || + (sha512_masked_core.mode == 2) || + (sha512_masked_core.mode == 3); + endproperty + assume_mode_values: assume property (disable iff(!reset_n || zeroize) mode_values); + + property inputs_stay_stable; + !(sha512_masked_core.ready) |-> $stable(block_msg) && $stable(sha512_masked_core.mode); + endproperty + assume_inputs_stay_stable: assume property (disable iff(!reset_n || zeroize) inputs_stay_stable); + + property remove_init_next_together; + !(init_cmd && next_cmd); + endproperty + assume_remove_init_next_together: assume property (disable iff(!reset_n || zeroize) remove_init_next_together); + + property init_next_order; + !fv_init_reg |-> !next_cmd; + endproperty + assume_init_next_order: assume property (disable iff(!reset_n || zeroize) init_next_order); + + +endmodule + +bind sha512_masked_core fv_constraints_m fv_constraints( + .init_cmd(init_cmd), + .next_cmd(next_cmd), + .reset_n(reset_n), + .ready(ready), + .digest_valid(digest_valid), + .clk(clk), + .mode(mode), + .block_msg(block_msg), + .zeroize(zeroize), + .lfsr_seed(lfsr_seed), + .digest(digest) +); diff --git a/src/sha512_masked/formal/properties/fv_coverpoints.sv b/src/sha512_masked/formal/properties/fv_coverpoints.sv new file mode 100644 index 000000000..99fc818e4 --- /dev/null +++ b/src/sha512_masked/formal/properties/fv_coverpoints.sv @@ -0,0 +1,50 @@ +// ------------------------------------------------- +// 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_coverpoints_m( + input logic clk, + input logic reset_n, + input logic zeroize +); + + default clocking default_clk @(posedge clk); endclocking + + //Cover zeroize: + //Assert zeroize input and check the status of all registers. All registers/internal memories should be cleared. + cover_zeroize: cover property(disable iff(!reset_n) sha512_masked_core.zeroize ); + cover_zeroize_after_next: cover property(disable iff(!reset_n) sha512_masked_core.zeroize && sha512_masked_core.next_cmd ); + + cover_multiple_next: cover property(disable iff(!reset_n || zeroize) + sha512_masked_core.next_cmd && sha512_masked_core.ready ##1 (sha512_masked_core.next_cmd && sha512_masked_core.ready)[->1] + ); + + //Cover modes: + //Cover all 4 different modes for SHA512 + cover_mode_224: cover property(disable iff(!reset_n) sha512_masked_core.mode == 0 && sha512_masked_core.init_cmd ); + cover_mode_256: cover property(disable iff(!reset_n) sha512_masked_core.mode == 1 && sha512_masked_core.init_cmd ); + cover_mode_384: cover property(disable iff(!reset_n) sha512_masked_core.mode == 2 && sha512_masked_core.init_cmd ); + cover_mode_512: cover property(disable iff(!reset_n) sha512_masked_core.mode == 3 && sha512_masked_core.init_cmd ); + + +endmodule +bind sha512_masked_core fv_coverpoints_m fv_coverpoints( + .clk(clk), + .reset_n(reset_n), + .zeroize(zeroize) +); \ No newline at end of file diff --git a/src/sha512_masked/formal/properties/fv_sha512_masked.sv b/src/sha512_masked/formal/properties/fv_sha512_masked.sv new file mode 100644 index 000000000..a7b0ef598 --- /dev/null +++ b/src/sha512_masked/formal/properties/fv_sha512_masked.sv @@ -0,0 +1,919 @@ +// ------------------------------------------------- +// 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. +// + +import sha512_masked_pkg::*; + + +module fv_sha512_masked_m( + input bit rst, + input bit clk, + + // Inputs + input st_SHA_Args sha_in_struct, + input bit unsigned [73:0] lfsr_in, + + // Outputs + input bit unsigned [511:0] digest_out, + + // Valid signals + input bit block_in_valid, + input bit digest_valid, + + // Ready signals + input bit block_in_ready, + + // Registers + input a_sc_big_unsigned_64_8 H, + input bit signed [31:0] block_sha_mode, + input a_sc_big_unsigned_64_16 W, + input st_masked_reg_t a, + input st_masked_reg_t b, + input bit unsigned [1023:0] block_in, + input st_masked_reg_t c, + input st_masked_reg_t d, + input st_masked_reg_t e, + input st_masked_reg_t f, + input st_masked_reg_t g, + input st_masked_reg_t h, + input bit signed [31:0] i, + input bit block_init, + input bit unsigned [73:0] lfsr_rnd, + input bit signed [31:0] rnd_cnt_reg, + input a_sc_big_unsigned_64_8 rh_masking_rnd, + + // States + input bit IDLE, + input bit CTRL_RND, + input bit SHA_Rounds, + input bit DONE +); + + +default clocking default_clk @(posedge clk); endclocking + + +a_sc_big_unsigned_64_8 H_0 = '{ + 0: 64'd0, + 1: 64'd0, + 2: 64'd0, + 3: 64'd0, + 4: 64'd0, + 5: 64'd0, + 6: 64'd0, + 7: 64'd0 +}; + +a_sc_big_unsigned_64_16 W_0 = '{ + 0: 64'd0, + 1: 64'd0, + 2: 64'd0, + 3: 64'd0, + 4: 64'd0, + 5: 64'd0, + 6: 64'd0, + 7: 64'd0, + 8: 64'd0, + 9: 64'd0, + 10: 64'd0, + 11: 64'd0, + 12: 64'd0, + 13: 64'd0, + 14: 64'd0, + 15: 64'd0 +}; + +st_masked_reg_t a_0 = '{ + masked: 64'd0, + random: 64'd0 +}; + +a_sc_big_unsigned_64_8 rh_masking_rnd_0 = '{ + 0: ((rnd_cnt_reg == 'sd0) ? lfsr_in : rh_masking_rnd['sd0]), + 1: ((rnd_cnt_reg == 'sd1) ? lfsr_in : rh_masking_rnd['sd1]), + 2: ((rnd_cnt_reg == 'sd2) ? lfsr_in : rh_masking_rnd['sd2]), + 3: ((rnd_cnt_reg == 'sd3) ? lfsr_in : rh_masking_rnd['sd3]), + 4: ((rnd_cnt_reg == 'sd4) ? lfsr_in : rh_masking_rnd['sd4]), + 5: ((rnd_cnt_reg == 'sd5) ? lfsr_in : rh_masking_rnd['sd5]), + 6: ((rnd_cnt_reg == 'sd6) ? lfsr_in : rh_masking_rnd['sd6]), + 7: ((rnd_cnt_reg == 'sd7) ? lfsr_in : rh_masking_rnd['sd7]) +}; + +a_sc_big_unsigned_64_8 H_1 = '{ + 0: 64'h8C3D37C819544DA2, + 1: 64'h73E1996689DCD4D6, + 2: 64'h1DFAB7AE32FF9C82, + 3: 64'h679DD514582F9FCF, + 4: 64'hF6D2B697BD44DA8, + 5: 64'h77E36F7304C48942, + 6: 64'h3F9D85A86A1D36C8, + 7: 64'h1112E6AD91D692A1 +}; + +a_sc_big_unsigned_64_16 W_1 = '{ + 0: slicer(block_in, 'sd15), + 1: slicer(block_in, 'sd14), + 2: slicer(block_in, 'sd13), + 3: slicer(block_in, 'sd12), + 4: slicer(block_in, 'sd11), + 5: slicer(block_in, 'sd10), + 6: slicer(block_in, 'sd9), + 7: slicer(block_in, 'sd8), + 8: slicer(block_in, 'sd7), + 9: slicer(block_in, 'sd6), + 10: slicer(block_in, 'sd5), + 11: slicer(block_in, 'sd4), + 12: slicer(block_in, 'sd3), + 13: slicer(block_in, 'sd2), + 14: slicer(block_in, 'sd1), + 15: slicer(block_in, 'sd0) +}; + +st_masked_reg_t a_1 = '{ + masked: (64'h8C3D37C819544DA2 ^ (0 ? lfsr_in : rh_masking_rnd['sd0])), + random: (0 ? lfsr_in : rh_masking_rnd['sd0]) +}; + +st_masked_reg_t b_0 = '{ + masked: (64'h73E1996689DCD4D6 ^ (0 ? lfsr_in : rh_masking_rnd['sd1])), + random: (0 ? lfsr_in : rh_masking_rnd['sd1]) +}; + +st_masked_reg_t c_0 = '{ + masked: (64'h1DFAB7AE32FF9C82 ^ (0 ? lfsr_in : rh_masking_rnd['sd2])), + random: (0 ? lfsr_in : rh_masking_rnd['sd2]) +}; + +st_masked_reg_t d_0 = '{ + masked: (64'h679DD514582F9FCF ^ (0 ? lfsr_in : rh_masking_rnd['sd3])), + random: (0 ? lfsr_in : rh_masking_rnd['sd3]) +}; + +st_masked_reg_t e_0 = '{ + masked: (64'hF6D2B697BD44DA8 ^ (0 ? lfsr_in : rh_masking_rnd['sd4])), + random: (0 ? lfsr_in : rh_masking_rnd['sd4]) +}; + +st_masked_reg_t f_0 = '{ + masked: (64'h77E36F7304C48942 ^ (0 ? lfsr_in : rh_masking_rnd['sd5])), + random: (0 ? lfsr_in : rh_masking_rnd['sd5]) +}; + +st_masked_reg_t g_0 = '{ + masked: (64'h3F9D85A86A1D36C8 ^ (0 ? lfsr_in : rh_masking_rnd['sd6])), + random: (0 ? lfsr_in : rh_masking_rnd['sd6]) +}; + +st_masked_reg_t h_0 = '{ + masked: (64'h1112E6AD91D692A1 ^ (0 ? lfsr_in : rh_masking_rnd['sd7])), + random: (0 ? lfsr_in : rh_masking_rnd['sd7]) +}; + +a_sc_big_unsigned_64_8 rh_masking_rnd_1 = '{ + 0: lfsr_in, + 1: rh_masking_rnd['sd1], + 2: rh_masking_rnd['sd2], + 3: rh_masking_rnd['sd3], + 4: rh_masking_rnd['sd4], + 5: rh_masking_rnd['sd5], + 6: rh_masking_rnd['sd6], + 7: rh_masking_rnd['sd7] +}; + +a_sc_big_unsigned_64_8 H_2 = '{ + 0: 64'h22312194FC2BF72C, + 1: 64'h9F555FA3C84C64C2, + 2: 64'h2393B86B6F53B151, + 3: 64'h963877195940EABD, + 4: 64'h96283EE2A88EFFE3, + 5: 64'hBE5E1E2553863992, + 6: 64'h2B0199FC2C85B8AA, + 7: 64'hEB72DDC81C52CA2 +}; + +st_masked_reg_t a_2 = '{ + masked: (64'h22312194FC2BF72C ^ (0 ? lfsr_in : rh_masking_rnd['sd0])), + random: (0 ? lfsr_in : rh_masking_rnd['sd0]) +}; + +st_masked_reg_t b_1 = '{ + masked: (64'h9F555FA3C84C64C2 ^ (0 ? lfsr_in : rh_masking_rnd['sd1])), + random: (0 ? lfsr_in : rh_masking_rnd['sd1]) +}; + +st_masked_reg_t c_1 = '{ + masked: (64'h2393B86B6F53B151 ^ (0 ? lfsr_in : rh_masking_rnd['sd2])), + random: (0 ? lfsr_in : rh_masking_rnd['sd2]) +}; + +st_masked_reg_t d_1 = '{ + masked: (64'h963877195940EABD ^ (0 ? lfsr_in : rh_masking_rnd['sd3])), + random: (0 ? lfsr_in : rh_masking_rnd['sd3]) +}; + +st_masked_reg_t e_1 = '{ + masked: (64'h96283EE2A88EFFE3 ^ (0 ? lfsr_in : rh_masking_rnd['sd4])), + random: (0 ? lfsr_in : rh_masking_rnd['sd4]) +}; + +st_masked_reg_t f_1 = '{ + masked: (64'hBE5E1E2553863992 ^ (0 ? lfsr_in : rh_masking_rnd['sd5])), + random: (0 ? lfsr_in : rh_masking_rnd['sd5]) +}; + +st_masked_reg_t g_1 = '{ + masked: (64'h2B0199FC2C85B8AA ^ (0 ? lfsr_in : rh_masking_rnd['sd6])), + random: (0 ? lfsr_in : rh_masking_rnd['sd6]) +}; + +st_masked_reg_t h_1 = '{ + masked: (64'hEB72DDC81C52CA2 ^ (0 ? lfsr_in : rh_masking_rnd['sd7])), + random: (0 ? lfsr_in : rh_masking_rnd['sd7]) +}; + +a_sc_big_unsigned_64_8 H_3 = '{ + 0: 64'h6A09E667F3BCC908, + 1: 64'hBB67AE8584CAA73B, + 2: 64'h3C6EF372FE94F82B, + 3: 64'hA54FF53A5F1D36F1, + 4: 64'h510E527FADE682D1, + 5: 64'h9B05688C2B3E6C1F, + 6: 64'h1F83D9ABFB41BD6B, + 7: 64'h5BE0CD19137E2179 +}; + +st_masked_reg_t a_3 = '{ + masked: (64'h6A09E667F3BCC908 ^ (0 ? lfsr_in : rh_masking_rnd['sd0])), + random: (0 ? lfsr_in : rh_masking_rnd['sd0]) +}; + +st_masked_reg_t b_2 = '{ + masked: (64'hBB67AE8584CAA73B ^ (0 ? lfsr_in : rh_masking_rnd['sd1])), + random: (0 ? lfsr_in : rh_masking_rnd['sd1]) +}; + +st_masked_reg_t c_2 = '{ + masked: (64'h3C6EF372FE94F82B ^ (0 ? lfsr_in : rh_masking_rnd['sd2])), + random: (0 ? lfsr_in : rh_masking_rnd['sd2]) +}; + +st_masked_reg_t d_2 = '{ + masked: (64'hA54FF53A5F1D36F1 ^ (0 ? lfsr_in : rh_masking_rnd['sd3])), + random: (0 ? lfsr_in : rh_masking_rnd['sd3]) +}; + +st_masked_reg_t e_2 = '{ + masked: (64'h510E527FADE682D1 ^ (0 ? lfsr_in : rh_masking_rnd['sd4])), + random: (0 ? lfsr_in : rh_masking_rnd['sd4]) +}; + +st_masked_reg_t f_2 = '{ + masked: (64'h9B05688C2B3E6C1F ^ (0 ? lfsr_in : rh_masking_rnd['sd5])), + random: (0 ? lfsr_in : rh_masking_rnd['sd5]) +}; + +st_masked_reg_t g_2 = '{ + masked: (64'h1F83D9ABFB41BD6B ^ (0 ? lfsr_in : rh_masking_rnd['sd6])), + random: (0 ? lfsr_in : rh_masking_rnd['sd6]) +}; + +st_masked_reg_t h_2 = '{ + masked: (64'h5BE0CD19137E2179 ^ (0 ? lfsr_in : rh_masking_rnd['sd7])), + random: (0 ? lfsr_in : rh_masking_rnd['sd7]) +}; + +a_sc_big_unsigned_64_8 H_4 = '{ + 0: 64'hCBBB9D5DC1059ED8, + 1: 64'h629A292A367CD507, + 2: 64'h9159015A3070DD17, + 3: 64'h152FECD8F70E5939, + 4: 64'h67332667FFC00B31, + 5: 64'h8EB44A8768581511, + 6: 64'hDB0C2E0D64F98FA7, + 7: 64'h47B5481DBEFA4FA4 +}; + +st_masked_reg_t a_4 = '{ + masked: (64'hCBBB9D5DC1059ED8 ^ (0 ? lfsr_in : rh_masking_rnd['sd0])), + random: (0 ? lfsr_in : rh_masking_rnd['sd0]) +}; + +st_masked_reg_t b_3 = '{ + masked: (64'h629A292A367CD507 ^ (0 ? lfsr_in : rh_masking_rnd['sd1])), + random: (0 ? lfsr_in : rh_masking_rnd['sd1]) +}; + +st_masked_reg_t c_3 = '{ + masked: (64'h9159015A3070DD17 ^ (0 ? lfsr_in : rh_masking_rnd['sd2])), + random: (0 ? lfsr_in : rh_masking_rnd['sd2]) +}; + +st_masked_reg_t d_3 = '{ + masked: (64'h152FECD8F70E5939 ^ (0 ? lfsr_in : rh_masking_rnd['sd3])), + random: (0 ? lfsr_in : rh_masking_rnd['sd3]) +}; + +st_masked_reg_t e_3 = '{ + masked: (64'h67332667FFC00B31 ^ (0 ? lfsr_in : rh_masking_rnd['sd4])), + random: (0 ? lfsr_in : rh_masking_rnd['sd4]) +}; + +st_masked_reg_t f_3 = '{ + masked: (64'h8EB44A8768581511 ^ (0 ? lfsr_in : rh_masking_rnd['sd5])), + random: (0 ? lfsr_in : rh_masking_rnd['sd5]) +}; + +st_masked_reg_t g_3 = '{ + masked: (64'hDB0C2E0D64F98FA7 ^ (0 ? lfsr_in : rh_masking_rnd['sd6])), + random: (0 ? lfsr_in : rh_masking_rnd['sd6]) +}; + +st_masked_reg_t h_3 = '{ + masked: (64'h47B5481DBEFA4FA4 ^ (0 ? lfsr_in : rh_masking_rnd['sd7])), + random: (0 ? lfsr_in : rh_masking_rnd['sd7]) +}; + +st_masked_reg_t a_5 = '{ + masked: (H[64'd0] ^ (0 ? lfsr_in : rh_masking_rnd['sd0])), + random: (0 ? lfsr_in : rh_masking_rnd['sd0]) +}; + +st_masked_reg_t b_4 = '{ + masked: (H[64'd1] ^ (0 ? lfsr_in : rh_masking_rnd['sd1])), + random: (0 ? lfsr_in : rh_masking_rnd['sd1]) +}; + +st_masked_reg_t c_4 = '{ + masked: (H[64'd2] ^ (0 ? lfsr_in : rh_masking_rnd['sd2])), + random: (0 ? lfsr_in : rh_masking_rnd['sd2]) +}; + +st_masked_reg_t d_4 = '{ + masked: (H[64'd3] ^ (0 ? lfsr_in : rh_masking_rnd['sd3])), + random: (0 ? lfsr_in : rh_masking_rnd['sd3]) +}; + +st_masked_reg_t e_4 = '{ + masked: (H[64'd4] ^ (0 ? lfsr_in : rh_masking_rnd['sd4])), + random: (0 ? lfsr_in : rh_masking_rnd['sd4]) +}; + +st_masked_reg_t f_4 = '{ + masked: (H[64'd5] ^ (0 ? lfsr_in : rh_masking_rnd['sd5])), + random: (0 ? lfsr_in : rh_masking_rnd['sd5]) +}; + +st_masked_reg_t g_4 = '{ + masked: (H[64'd6] ^ (0 ? lfsr_in : rh_masking_rnd['sd6])), + random: (0 ? lfsr_in : rh_masking_rnd['sd6]) +}; + +st_masked_reg_t h_4 = '{ + masked: (H[64'd7] ^ (0 ? lfsr_in : rh_masking_rnd['sd7])), + random: (0 ? lfsr_in : rh_masking_rnd['sd7]) +}; + +st_masked_reg_t a_6 = '{ + masked: A2B_conv(64'((T1_m(e.masked, e.random, f.masked, f.random, g.masked, g.random, h.masked, h.random, K[i], (W[i] ^ 64'(lfsr_rnd)), 64'(lfsr_rnd), 0, 128'd0, 64'd0, (((lfsr_rnd >> 74'd64) & 74'h1) == 74'd1), ((((lfsr_rnd >> 74'd64) >> 74'd1) & 74'h1) == 74'd1), (((((lfsr_rnd >> 74'd64) >> 74'd1) >> 74'd1) & 74'h1) == 74'd1), ((((((lfsr_rnd >> 74'd64) >> 74'd1) >> 74'd1) >> 74'd1) & 74'h1) == 74'd1), (((((((lfsr_rnd >> 74'd64) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) & 74'h1) == 74'd1), 'sd10) + T2_m(a.masked, a.random, b.masked, b.random, c.masked, c.random, 0, 128'd0, 64'd0, ((((((((lfsr_rnd >> 74'd64) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) & 74'h1) == 74'd1), (((((((((lfsr_rnd >> 74'd64) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) & 74'h1) == 74'd1), 'sd10))), 64'((T1_r(e.random, g.random, h.random, 64'(lfsr_rnd)) + T2_r(a.random, b.random))), (((((((((((lfsr_rnd >> 74'd64) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) & 74'h1) == 74'd1), 0, 128'd0, 64'd0, 'sd10), + random: (T1_r(e.random, g.random, h.random, 64'(lfsr_rnd)) + T2_r(a.random, b.random)) +}; + +st_masked_reg_t e_5 = '{ + masked: A2B_conv(64'((B2A_conv(d.masked, d.random, ((((((((((lfsr_rnd >> 74'd64) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) & 74'h1) == 74'd1), 0, 128'd0, 64'd0, 'sd10) + T1_m(e.masked, e.random, f.masked, f.random, g.masked, g.random, h.masked, h.random, K[i], (W[i] ^ 64'(lfsr_rnd)), 64'(lfsr_rnd), 0, 128'd0, 64'd0, (((lfsr_rnd >> 74'd64) & 74'h1) == 74'd1), ((((lfsr_rnd >> 74'd64) >> 74'd1) & 74'h1) == 74'd1), (((((lfsr_rnd >> 74'd64) >> 74'd1) >> 74'd1) & 74'h1) == 74'd1), ((((((lfsr_rnd >> 74'd64) >> 74'd1) >> 74'd1) >> 74'd1) & 74'h1) == 74'd1), (((((((lfsr_rnd >> 74'd64) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) & 74'h1) == 74'd1), 'sd10))), 64'((d.random + T1_r(e.random, g.random, h.random, 64'(lfsr_rnd)))), ((((((((((((lfsr_rnd >> 74'd64) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) & 74'h1) == 74'd1), 0, 128'd0, 64'd0, 'sd10), + random: (d.random + T1_r(e.random, g.random, h.random, 64'(lfsr_rnd))) +}; + +a_sc_big_unsigned_64_16 W_2 = '{ + 0: W['sd1], + 1: W['sd2], + 2: W['sd3], + 3: W['sd4], + 4: W['sd5], + 5: W['sd6], + 6: W['sd7], + 7: W['sd8], + 8: W['sd9], + 9: W['sd10], + 10: W['sd11], + 11: W['sd12], + 12: W['sd13], + 13: W['sd14], + 14: W['sd15], + 15: compute_w(W[64'd14], W[64'd9], W[64'd1], W[64'd0]) +}; + +st_masked_reg_t a_7 = '{ + masked: A2B_conv(64'((T1_m(e.masked, e.random, f.masked, f.random, g.masked, g.random, h.masked, h.random, K[i], (compute_w(W[64'd14], W[64'd9], W[64'd1], W[64'd0]) ^ 64'(lfsr_rnd)), 64'(lfsr_rnd), 0, 128'd0, 64'd0, (((lfsr_rnd >> 74'd64) & 74'h1) == 74'd1), ((((lfsr_rnd >> 74'd64) >> 74'd1) & 74'h1) == 74'd1), (((((lfsr_rnd >> 74'd64) >> 74'd1) >> 74'd1) & 74'h1) == 74'd1), ((((((lfsr_rnd >> 74'd64) >> 74'd1) >> 74'd1) >> 74'd1) & 74'h1) == 74'd1), (((((((lfsr_rnd >> 74'd64) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) & 74'h1) == 74'd1), 'sd10) + T2_m(a.masked, a.random, b.masked, b.random, c.masked, c.random, 0, 128'd0, 64'd0, ((((((((lfsr_rnd >> 74'd64) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) & 74'h1) == 74'd1), (((((((((lfsr_rnd >> 74'd64) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) & 74'h1) == 74'd1), 'sd10))), 64'((T1_r(e.random, g.random, h.random, 64'(lfsr_rnd)) + T2_r(a.random, b.random))), (((((((((((lfsr_rnd >> 74'd64) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) & 74'h1) == 74'd1), 0, 128'd0, 64'd0, 'sd10), + random: (T1_r(e.random, g.random, h.random, 64'(lfsr_rnd)) + T2_r(a.random, b.random)) +}; + +st_masked_reg_t e_6 = '{ + masked: A2B_conv(64'((B2A_conv(d.masked, d.random, ((((((((((lfsr_rnd >> 74'd64) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) & 74'h1) == 74'd1), 0, 128'd0, 64'd0, 'sd10) + T1_m(e.masked, e.random, f.masked, f.random, g.masked, g.random, h.masked, h.random, K[i], (compute_w(W[64'd14], W[64'd9], W[64'd1], W[64'd0]) ^ 64'(lfsr_rnd)), 64'(lfsr_rnd), 0, 128'd0, 64'd0, (((lfsr_rnd >> 74'd64) & 74'h1) == 74'd1), ((((lfsr_rnd >> 74'd64) >> 74'd1) & 74'h1) == 74'd1), (((((lfsr_rnd >> 74'd64) >> 74'd1) >> 74'd1) & 74'h1) == 74'd1), ((((((lfsr_rnd >> 74'd64) >> 74'd1) >> 74'd1) >> 74'd1) & 74'h1) == 74'd1), (((((((lfsr_rnd >> 74'd64) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) & 74'h1) == 74'd1), 'sd10))), 64'((d.random + T1_r(e.random, g.random, h.random, 64'(lfsr_rnd)))), ((((((((((((lfsr_rnd >> 74'd64) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) >> 74'd1) & 74'h1) == 74'd1), 0, 128'd0, 64'd0, 'sd10), + random: (d.random + T1_r(e.random, g.random, h.random, 64'(lfsr_rnd))) +}; + +a_sc_big_unsigned_64_8 H_5 = '{ + 0: (H[64'd0] + (a.masked ^ a.random)), + 1: (H['sd1] + (b.masked ^ b.random)), + 2: (H['sd2] + (c.masked ^ c.random)), + 3: (H['sd3] + (d.masked ^ d.random)), + 4: (H['sd4] + (e.masked ^ e.random)), + 5: (H['sd5] + (f.masked ^ f.random)), + 6: (H['sd6] + (g.masked ^ g.random)), + 7: (H['sd7] + (h.masked ^ h.random)) +}; + + +sequence reset_sequence; + !rst ##1 rst; +endsequence + + +reset_a: assert property (reset_p); +property reset_p; + $past(!rst) && rst |-> + IDLE && + H == H_0 && + W == W_0 && + a == a_0 && + b == a_0 && + c == a_0 && + d == a_0 && + e == a_0 && + f == a_0 && + g == a_0 && + h == a_0 && + i == 'sd0 && + rnd_cnt_reg == 'sd0 && + rh_masking_rnd == H_0 && + block_in_ready == 1 && + digest_valid == 0; +endproperty + + +CTRL_RND_to_CTRL_RND_a: assert property (disable iff(!rst) CTRL_RND_to_CTRL_RND_p); +property CTRL_RND_to_CTRL_RND_p; + CTRL_RND && + (('sd1 + rnd_cnt_reg) < 'sd9) +|-> + ##1 (block_in_ready == 0) and + ##1 (digest_valid == 0) and + ##1 + CTRL_RND && + H == $past(H, 1) && + W == $past(W, 1) && + a == $past(a, 1) && + b == $past(b, 1) && + c == $past(c, 1) && + d == $past(d, 1) && + e == $past(e, 1) && + f == $past(f, 1) && + g == $past(g, 1) && + h == $past(h, 1) && + i == $past(i, 1) && + rnd_cnt_reg == ('sd1 + $past(rnd_cnt_reg, 1)) && + rh_masking_rnd == $past(rh_masking_rnd_0, 1); +endproperty + + +CTRL_RND_to_SHA_Rounds_224_a: assert property (disable iff(!rst) CTRL_RND_to_SHA_Rounds_224_p); +property CTRL_RND_to_SHA_Rounds_224_p; + CTRL_RND && + (('sd1 + rnd_cnt_reg) >= 'sd9) && + block_init && + (block_sha_mode == 'sd0) +|-> + ##1 (block_in_ready == 0) and + ##1 (digest_valid == 0) and + ##1 + SHA_Rounds && + H == $past(H_1, 1) && + W == $past(W_1, 1) && + a == $past(a_1, 1) && + b == $past(b_0, 1) && + c == $past(c_0, 1) && + d == $past(d_0, 1) && + e == $past(e_0, 1) && + f == $past(f_0, 1) && + g == $past(g_0, 1) && + h == $past(h_0, 1) && + i == 'sd0 && + rnd_cnt_reg == ('sd1 + $past(rnd_cnt_reg, 1)) && + rh_masking_rnd == $past(rh_masking_rnd_1, 1); +endproperty + + +CTRL_RND_to_SHA_Rounds_256_a: assert property (disable iff(!rst) CTRL_RND_to_SHA_Rounds_256_p); +property CTRL_RND_to_SHA_Rounds_256_p; + CTRL_RND && + (('sd1 + rnd_cnt_reg) >= 'sd9) && + block_init && + (block_sha_mode == 'sd1) +|-> + ##1 (block_in_ready == 0) and + ##1 (digest_valid == 0) and + ##1 + SHA_Rounds && + H == $past(H_2, 1) && + W == $past(W_1, 1) && + a == $past(a_2, 1) && + b == $past(b_1, 1) && + c == $past(c_1, 1) && + d == $past(d_1, 1) && + e == $past(e_1, 1) && + f == $past(f_1, 1) && + g == $past(g_1, 1) && + h == $past(h_1, 1) && + i == 'sd0 && + rnd_cnt_reg == ('sd1 + $past(rnd_cnt_reg, 1)) && + rh_masking_rnd == $past(rh_masking_rnd_1, 1); +endproperty + + +CTRL_RND_to_SHA_Rounds_512_a: assert property (disable iff(!rst) CTRL_RND_to_SHA_Rounds_512_p); +property CTRL_RND_to_SHA_Rounds_512_p; + CTRL_RND && + (('sd1 + rnd_cnt_reg) >= 'sd9) && + block_init && + (block_sha_mode == 'sd3) +|-> + ##1 (block_in_ready == 0) and + ##1 (digest_valid == 0) and + ##1 + SHA_Rounds && + H == $past(H_3, 1) && + W == $past(W_1, 1) && + a == $past(a_3, 1) && + b == $past(b_2, 1) && + c == $past(c_2, 1) && + d == $past(d_2, 1) && + e == $past(e_2, 1) && + f == $past(f_2, 1) && + g == $past(g_2, 1) && + h == $past(h_2, 1) && + i == 'sd0 && + rnd_cnt_reg == ('sd1 + $past(rnd_cnt_reg, 1)) && + rh_masking_rnd == $past(rh_masking_rnd_1, 1); +endproperty + + +CTRL_RND_to_SHA_Rounds_384_a: assert property (disable iff(!rst) CTRL_RND_to_SHA_Rounds_384_p); +property CTRL_RND_to_SHA_Rounds_384_p; + CTRL_RND && + (('sd1 + rnd_cnt_reg) >= 'sd9) && + block_init && + (block_sha_mode != 'sd0) && + (block_sha_mode != 'sd1) && + (block_sha_mode != 'sd3) +|-> + ##1 (block_in_ready == 0) and + ##1 (digest_valid == 0) and + ##1 + SHA_Rounds && + H == $past(H_4, 1) && + W == $past(W_1, 1) && + a == $past(a_4, 1) && + b == $past(b_3, 1) && + c == $past(c_3, 1) && + d == $past(d_3, 1) && + e == $past(e_3, 1) && + f == $past(f_3, 1) && + g == $past(g_3, 1) && + h == $past(h_3, 1) && + i == 'sd0 && + rnd_cnt_reg == ('sd1 + $past(rnd_cnt_reg, 1)) && + rh_masking_rnd == $past(rh_masking_rnd_1, 1); +endproperty + + +CTRL_RND_to_SHA_Rounds_next_a: assert property (disable iff(!rst) CTRL_RND_to_SHA_Rounds_next_p); +property CTRL_RND_to_SHA_Rounds_next_p; + CTRL_RND && + (('sd1 + rnd_cnt_reg) >= 'sd9) && + !block_init +|-> + ##1 (block_in_ready == 0) and + ##1 (digest_valid == 0) and + ##1 + SHA_Rounds && + H == $past(H, 1) && + W == $past(W_1, 1) && + a == $past(a_5, 1) && + b == $past(b_4, 1) && + c == $past(c_4, 1) && + d == $past(d_4, 1) && + e == $past(e_4, 1) && + f == $past(f_4, 1) && + g == $past(g_4, 1) && + h == $past(h_4, 1) && + i == 'sd0 && + rnd_cnt_reg == ('sd1 + $past(rnd_cnt_reg, 1)) && + rh_masking_rnd == $past(rh_masking_rnd_1, 1); +endproperty + + +DONE_to_IDLE_a: assert property (disable iff(!rst) DONE_to_IDLE_p); +property DONE_to_IDLE_p; + DONE +|-> + ##1 + IDLE && + H == $past(H_5, 1) && + W == $past(W, 1) && + a == $past(a, 1) && + b == $past(b, 1) && + c == $past(c, 1) && + d == $past(d, 1) && + e == $past(e, 1) && + f == $past(f, 1) && + g == $past(g, 1) && + h == $past(h, 1) && + i == $past(i, 1) && + digest_out == $past(compute_digest(H[64'd7], h.masked, h.random, H[64'd6], g.masked, g.random, H[64'd5], f.masked, f.random, H[64'd4], e.masked, e.random, H[64'd3], d.masked, d.random, H[64'd2], c.masked, c.random, H[64'd1], b.masked, b.random, H[64'd0], a.masked, a.random)) && + rnd_cnt_reg == $past(rnd_cnt_reg, 1) && + rh_masking_rnd == $past(rh_masking_rnd, 1) && + block_in_ready == 1 && + digest_valid == 1; +endproperty + + +IDLE_to_CTRL_RND_a: assert property (disable iff(!rst) IDLE_to_CTRL_RND_p); +property IDLE_to_CTRL_RND_p; + IDLE && + block_in_valid +|-> + ##1 (block_in_ready == 0) and + ##1 (digest_valid == 0) and + ##1 + CTRL_RND && + H == $past(H, 1) && + W == $past(W, 1) && + a == $past(a, 1) && + b == $past(b, 1) && + c == $past(c, 1) && + d == $past(d, 1) && + e == $past(e, 1) && + f == $past(f, 1) && + g == $past(g, 1) && + h == $past(h, 1) && + i == $past(i, 1) && + rnd_cnt_reg == 'sd0 && + rh_masking_rnd == $past(rh_masking_rnd, 1); +endproperty + + +SHA_Rounds_to_DONE_a: assert property (disable iff(!rst) SHA_Rounds_to_DONE_p); +property SHA_Rounds_to_DONE_p; + SHA_Rounds && + (i >= 'sd16) && + (('sd1 + i) >= 'sd80) +|-> + ##1 (block_in_ready == 0) and + ##1 (digest_valid == 0) and + ##1 + DONE && + H == $past(H, 1) && + W == $past(W_2, 1) && + a == $past(a_7, 1) && + b == $past(a, 1) && + c == $past(b, 1) && + d == $past(c, 1) && + e == $past(e_6, 1) && + f == $past(e, 1) && + g == $past(f, 1) && + h == $past(g, 1) && + i == ('sd1 + $past(i, 1)) && + rnd_cnt_reg == $past(rnd_cnt_reg, 1) && + rh_masking_rnd == $past(rh_masking_rnd, 1); +endproperty + + +SHA_Rounds_to_SHA_Rounds_before_16_a: assert property (disable iff(!rst) SHA_Rounds_to_SHA_Rounds_before_16_p); +property SHA_Rounds_to_SHA_Rounds_before_16_p; + SHA_Rounds && + (i < 'sd16) && + (('sd1 + i) < 'sd80) +|-> + ##1 (block_in_ready == 0) and + ##1 (digest_valid == 0) and + ##1 + SHA_Rounds && + H == $past(H, 1) && + W == $past(W, 1) && + a == $past(a_6, 1) && + b == $past(a, 1) && + c == $past(b, 1) && + d == $past(c, 1) && + e == $past(e_5, 1) && + f == $past(e, 1) && + g == $past(f, 1) && + h == $past(g, 1) && + i == ('sd1 + $past(i, 1)) && + rnd_cnt_reg == $past(rnd_cnt_reg, 1) && + rh_masking_rnd == $past(rh_masking_rnd, 1); +endproperty + + +SHA_Rounds_to_SHA_Rounds_after_16_a: assert property (disable iff(!rst) SHA_Rounds_to_SHA_Rounds_after_16_p); +property SHA_Rounds_to_SHA_Rounds_after_16_p; + SHA_Rounds && + (i >= 'sd16) && + (('sd1 + i) < 'sd80) +|-> + ##1 (block_in_ready == 0) and + ##1 (digest_valid == 0) and + ##1 + SHA_Rounds && + H == $past(H, 1) && + W == $past(W_2, 1) && + a == $past(a_7, 1) && + b == $past(a, 1) && + c == $past(b, 1) && + d == $past(c, 1) && + e == $past(e_6, 1) && + f == $past(e, 1) && + g == $past(f, 1) && + h == $past(g, 1) && + i == ('sd1 + $past(i, 1)) && + rnd_cnt_reg == $past(rnd_cnt_reg, 1) && + rh_masking_rnd == $past(rh_masking_rnd, 1); +endproperty + + +IDLE_wait_a: assert property (disable iff(!rst) IDLE_wait_p); +property IDLE_wait_p; + IDLE && + !block_in_valid +|-> + ##1 + IDLE && + H == $past(H, 1) && + W == $past(W, 1) && + a == $past(a, 1) && + b == $past(b, 1) && + c == $past(c, 1) && + d == $past(d, 1) && + e == $past(e, 1) && + f == $past(f, 1) && + g == $past(g, 1) && + h == $past(h, 1) && + i == $past(i, 1) && + rnd_cnt_reg == $past(rnd_cnt_reg, 1) && + rh_masking_rnd == $past(rh_masking_rnd, 1) && + block_in_ready == 1 && + digest_valid == $past(digest_valid); +endproperty + + +endmodule + + +module fv_SHA512_masked_wrapper_m; + + +default clocking default_clk @(posedge (sha512_masked_core.clk)); endclocking + + +st_SHA_Args sha_in_struct = '{ + in: (sha512_masked_core.block_msg), + SHA_Mode: (sha512_masked_core.mode), + init_cmd: (sha512_masked_core.init_cmd), + next_cmd: (sha512_masked_core.next_cmd), + zeroize: (sha512_masked_core.zeroize) +}; +a_sc_big_unsigned_64_8 H = '{ + 0: (sha512_masked_core.H0_reg), + 1: (sha512_masked_core.H1_reg), + 2: (sha512_masked_core.H2_reg), + 3: (sha512_masked_core.H3_reg), + 4: (sha512_masked_core.H4_reg), + 5: (sha512_masked_core.H5_reg), + 6: (sha512_masked_core.H6_reg), + 7: (sha512_masked_core.H7_reg) +}; +a_sc_big_unsigned_64_16 W = '{ + 0: (sha512_masked_core.w_mem_inst.w_mem[00]), + 1: (sha512_masked_core.w_mem_inst.w_mem[01]), + 2: (sha512_masked_core.w_mem_inst.w_mem[02]), + 3: (sha512_masked_core.w_mem_inst.w_mem[03]), + 4: (sha512_masked_core.w_mem_inst.w_mem[04]), + 5: (sha512_masked_core.w_mem_inst.w_mem[05]), + 6: (sha512_masked_core.w_mem_inst.w_mem[06]), + 7: (sha512_masked_core.w_mem_inst.w_mem[07]), + 8: (sha512_masked_core.w_mem_inst.w_mem[08]), + 9: (sha512_masked_core.w_mem_inst.w_mem[09]), + 10: (sha512_masked_core.w_mem_inst.w_mem[10]), + 11: (sha512_masked_core.w_mem_inst.w_mem[11]), + 12: (sha512_masked_core.w_mem_inst.w_mem[12]), + 13: (sha512_masked_core.w_mem_inst.w_mem[13]), + 14: (sha512_masked_core.w_mem_inst.w_mem[14]), + 15: (sha512_masked_core.w_mem_inst.w_mem[15]) +}; +st_masked_reg_t a = '{ + masked: (sha512_masked_core.a_reg.masked), + random: (sha512_masked_core.a_reg.random) +}; +st_masked_reg_t b = '{ + masked: (sha512_masked_core.b_reg.masked), + random: (sha512_masked_core.b_reg.random) +}; +st_masked_reg_t c = '{ + masked: (sha512_masked_core.c_reg.masked), + random: (sha512_masked_core.c_reg.random) +}; +st_masked_reg_t d = '{ + masked: (sha512_masked_core.d_reg.masked), + random: (sha512_masked_core.d_reg.random) +}; +st_masked_reg_t e = '{ + masked: (sha512_masked_core.e_reg.masked), + random: (sha512_masked_core.e_reg.random) +}; +st_masked_reg_t f = '{ + masked: (sha512_masked_core.f_reg.masked), + random: (sha512_masked_core.f_reg.random) +}; +st_masked_reg_t g = '{ + masked: (sha512_masked_core.g_reg.masked), + random: (sha512_masked_core.g_reg.random) +}; +st_masked_reg_t h = '{ + masked: (sha512_masked_core.h_reg.masked), + random: (sha512_masked_core.h_reg.random) +}; +a_sc_big_unsigned_64_8 rh_masking_rnd = '{ + 0: (sha512_masked_core.rh_masking_rnd[0]), + 1: (sha512_masked_core.rh_masking_rnd[1]), + 2: (sha512_masked_core.rh_masking_rnd[2]), + 3: (sha512_masked_core.rh_masking_rnd[3]), + 4: (sha512_masked_core.rh_masking_rnd[4]), + 5: (sha512_masked_core.rh_masking_rnd[5]), + 6: (sha512_masked_core.rh_masking_rnd[6]), + 7: (sha512_masked_core.rh_masking_rnd[7]) +}; + + +fv_sha512_masked_m fv_sha512_masked( + .rst((sha512_masked_core.reset_n) && !(sha512_masked_core.zeroize)), + .clk(sha512_masked_core.clk), + + // Inputs + .sha_in_struct(sha_in_struct), + .lfsr_in(sha512_masked_core.lfsr_inst.rnd), + + // Outputs + .digest_out(sha512_masked_core.digest), + + // Valid signals + .block_in_valid(((sha512_masked_core.init_cmd) || (sha512_masked_core.next_cmd))), + .digest_valid(sha512_masked_core.digest_valid), + + // Ready signals + .block_in_ready(sha512_masked_core.ready), + + // Registers + .H(H), + .block_sha_mode(sha512_masked_core.mode), + .W(W), + .a(a), + .b(b), + .block_in(sha512_masked_core.block_msg), + .c(c), + .d(d), + .e(e), + .f(f), + .g(g), + .h(h), + .i(sha512_masked_core.round_ctr_reg), + .block_init(sha512_masked_core.init_reg), + .lfsr_rnd(sha512_masked_core.lfsr_rnd), + .rnd_cnt_reg(sha512_masked_core.rnd_ctr_reg), + .rh_masking_rnd(rh_masking_rnd), + + // States + .IDLE(sha512_masked_core.sha512_ctrl_reg==2'h0), + .CTRL_RND(sha512_masked_core.sha512_ctrl_reg==2'h1), + .SHA_Rounds(sha512_masked_core.sha512_ctrl_reg==2'h2), + .DONE(sha512_masked_core.sha512_ctrl_reg==2'h3) +); + + +endmodule + + +bind sha512_masked_core fv_SHA512_masked_wrapper_m fv_SHA512_masked_wrapper(); diff --git a/src/sha512_masked/formal/properties/fv_sha512_masked_pkg.sv b/src/sha512_masked/formal/properties/fv_sha512_masked_pkg.sv new file mode 100644 index 000000000..9479c5ebc --- /dev/null +++ b/src/sha512_masked/formal/properties/fv_sha512_masked_pkg.sv @@ -0,0 +1,197 @@ +// ------------------------------------------------- +// 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. +// + +package sha512_masked_pkg; + + +typedef struct { + bit unsigned [1023:0] in; + bit signed [31:0] SHA_Mode; + bit init_cmd; + bit next_cmd; + bit zeroize; +} st_SHA_Args; + +typedef struct { + bit unsigned [63:0] masked; + bit unsigned [63:0] random; +} st_masked_reg_t; + +typedef bit a_bool_10 [9:0]; + +typedef bit unsigned [63:0] a_sc_big_unsigned_64_16 [15:0]; + +typedef bit unsigned [63:0] a_sc_big_unsigned_64_8 [7:0]; + +typedef bit unsigned [63:0] a_sc_big_unsigned_64_80 [79:0]; + + +// Constants + +parameter a_sc_big_unsigned_64_80 K = '{ 0: 64'h428A2F98D728AE22, 1: 64'h7137449123EF65CD, 2: 64'hB5C0FBCFEC4D3B2F, 3: 64'hE9B5DBA58189DBBC, 4: 64'h3956C25BF348B538, 5: 64'h59F111F1B605D019, 6: 64'h923F82A4AF194F9B, 7: 64'hAB1C5ED5DA6D8118, 8: 64'hD807AA98A3030242, 9: 64'h12835B0145706FBE, 10: 64'h243185BE4EE4B28C, 11: 64'h550C7DC3D5FFB4E2, 12: 64'h72BE5D74F27B896F, 13: 64'h80DEB1FE3B1696B1, 14: 64'h9BDC06A725C71235, 15: 64'hC19BF174CF692694, 16: 64'hE49B69C19EF14AD2, 17: 64'hEFBE4786384F25E3, 18: 64'hFC19DC68B8CD5B5, 19: 64'h240CA1CC77AC9C65, 20: 64'h2DE92C6F592B0275, 21: 64'h4A7484AA6EA6E483, 22: 64'h5CB0A9DCBD41FBD4, 23: 64'h76F988DA831153B5, 24: 64'h983E5152EE66DFAB, 25: 64'hA831C66D2DB43210, 26: 64'hB00327C898FB213F, 27: 64'hBF597FC7BEEF0EE4, 28: 64'hC6E00BF33DA88FC2, 29: 64'hD5A79147930AA725, 30: 64'h6CA6351E003826F, 31: 64'h142929670A0E6E70, 32: 64'h27B70A8546D22FFC, 33: 64'h2E1B21385C26C926, 34: 64'h4D2C6DFC5AC42AED, 35: 64'h53380D139D95B3DF, 36: 64'h650A73548BAF63DE, 37: 64'h766A0ABB3C77B2A8, 38: 64'h81C2C92E47EDAEE6, 39: 64'h92722C851482353B, 40: 64'hA2BFE8A14CF10364, 41: 64'hA81A664BBC423001, 42: 64'hC24B8B70D0F89791, 43: 64'hC76C51A30654BE30, 44: 64'hD192E819D6EF5218, 45: 64'hD69906245565A910, 46: 64'hF40E35855771202A, 47: 64'h106AA07032BBD1B8, 48: 64'h19A4C116B8D2D0C8, 49: 64'h1E376C085141AB53, 50: 64'h2748774CDF8EEB99, 51: 64'h34B0BCB5E19B48A8, 52: 64'h391C0CB3C5C95A63, 53: 64'h4ED8AA4AE3418ACB, 54: 64'h5B9CCA4F7763E373, 55: 64'h682E6FF3D6B2B8A3, 56: 64'h748F82EE5DEFB2FC, 57: 64'h78A5636F43172F60, 58: 64'h84C87814A1F0AB72, 59: 64'h8CC702081A6439EC, 60: 64'h90BEFFFA23631E28, 61: 64'hA4506CEBDE82BDE9, 62: 64'hBEF9A3F7B2C67915, 63: 64'hC67178F2E372532B, 64: 64'hCA273ECEEA26619C, 65: 64'hD186B8C721C0C207, 66: 64'hEADA7DD6CDE0EB1E, 67: 64'hF57D4F7FEE6ED178, 68: 64'h6F067AA72176FBA, 69: 64'hA637DC5A2C898A6, 70: 64'h113F9804BEF90DAE, 71: 64'h1B710B35131C471B, 72: 64'h28DB77F523047D84, 73: 64'h32CAAB7B40C72493, 74: 64'h3C9EBE0A15C9BEBC, 75: 64'h431D67C49C100D4C, 76: 64'h4CC5D4BECB3E42B6, 77: 64'h597F299CFC657E2A, 78: 64'h5FCB6FAB3AD6FAEC, 79: 64'h6C44198C4A475817 }; + + +// Functions + +function bit unsigned [63:0] A2B_conv(bit unsigned [63:0] x_masked, bit unsigned [63:0] x_random, bit q, bit masked_carr, bit unsigned [127:0] x_m, bit unsigned [63:0] mask, bit signed [31:0] j); + + reg [63 : 0] masked_carry; + for (int j = 0; j < 64 ; j++) begin + if (j == 0) begin + masked_carry[j] = (~x_masked[0] & x_random[0]) ^ q; + x_masked[j] = x_masked[j]; + end + else begin + masked_carry[j] = (x_masked[j] ^ x_random[j]) & (x_random[j] ^ q) | (~x_masked[j] ^ x_random[j]) & masked_carry[j-1]; + x_masked[j] = (x_masked[j] ^ masked_carry[j-1]) ^ q; + + end + end + return x_masked; +endfunction + +function bit unsigned [63:0] B2A_conv(bit unsigned [63:0] x_masked, bit unsigned [63:0] x_random, bit q, bit masked_carr, bit unsigned [127:0] x_prime, bit unsigned [63:0] mask, bit signed [31:0] j); +reg [63 : 0] masked_carry; + for (int j = 0; j < 64 ; j++) begin + if (j == 0) begin + masked_carry[j] = ~x_masked[j] & (x_random[j] ^ q) | (x_masked[j] & q); + x_prime[j] = x_masked[j]; + end + else begin + x_prime[j] = (x_masked[j] ^ masked_carry[j-1]) ^ q; + masked_carry[j] = ~x_masked[j] & (x_random[j] ^ q) | x_masked[j] & masked_carry[j-1]; + end + end + return x_prime; +endfunction + +function bit unsigned [63:0] T1_m(bit unsigned [63:0] e_masked, bit unsigned [63:0] e_random, bit unsigned [63:0] f_masked, bit unsigned [63:0] f_random, bit unsigned [63:0] g_masked, bit unsigned [63:0] g_random, bit unsigned [63:0] h_masked, bit unsigned [63:0] h_random, bit unsigned [63:0] k, bit unsigned [63:0] w_masked, bit unsigned [63:0] w_random, bit masked_carry, bit unsigned [127:0] x_prime, bit unsigned [63:0] mask, bit q_masking_rnd_0, bit q_masking_rnd_1, bit q_masking_rnd_2, bit q_masking_rnd_3, bit q_masking_rnd_4, bit signed [31:0] j); + return 64'(((((B2A_conv(h_masked, h_random, q_masking_rnd_0, masked_carry, x_prime, mask, j) + B2A_conv(sigma1(e_masked), sigma1(e_random), q_masking_rnd_1, masked_carry, x_prime, mask, j)) + B2A_conv(masked_Ch_m(e_masked, e_random, f_masked, f_random, g_masked, g_random), (e_random ^ g_random), q_masking_rnd_2, masked_carry, x_prime, mask, j)) + B2A_conv(k, 64'h0, q_masking_rnd_3, masked_carry, x_prime, mask, j)) + B2A_conv(w_masked, w_random, q_masking_rnd_4, masked_carry, x_prime, mask, j))); +endfunction + +function bit unsigned [63:0] T1_r(bit unsigned [63:0] e_random, bit unsigned [63:0] g_random, bit unsigned [63:0] h_random, bit unsigned [63:0] w_random); + return 64'((((h_random + sigma1(e_random)) + (e_random ^ g_random)) + w_random)); +endfunction + +function bit unsigned [63:0] T2_m(bit unsigned [63:0] a_masked, bit unsigned [63:0] a_random, bit unsigned [63:0] b_masked, bit unsigned [63:0] b_random, bit unsigned [63:0] c_masked, bit unsigned [63:0] c_random, bit masked_carry, bit unsigned [127:0] x_prime, bit unsigned [63:0] mask, bit q_masking_rnd_5, bit q_masking_rnd_6, bit signed [31:0] j); + return 64'((B2A_conv(sigma0(a_masked), sigma0(a_random), q_masking_rnd_5, masked_carry, x_prime, mask, j) + B2A_conv(masked_Maj(a_masked, a_random, b_masked, b_random, c_masked, c_random), b_random, q_masking_rnd_6, masked_carry, x_prime, mask, j))); +endfunction + +function bit unsigned [63:0] T2_r(bit unsigned [63:0] a_random, bit unsigned [63:0] b_random); + return 64'((sigma0(a_random) + b_random)); +endfunction + +function bit unsigned [63:0] compute_w(bit unsigned [63:0] w14, bit unsigned [63:0] w9, bit unsigned [63:0] w1, bit unsigned [63:0] w0); + return 64'((((delta1(w14) + w9) + delta0(w1)) + w0)); +endfunction + +function bit unsigned [63:0] delta0(bit unsigned [63:0] x); + return ((rotr1(x) ^ rotr8(x)) ^ shr7(x)); +endfunction + +function bit unsigned [63:0] delta1(bit unsigned [63:0] x); + return ((rotr19(x) ^ rotr61(x)) ^ shr6(x)); +endfunction + +function bit unsigned [63:0] masked_Ch_m(bit unsigned [63:0] e_masked, bit unsigned [63:0] e_random, bit unsigned [63:0] f_masked, bit unsigned [63:0] f_random, bit unsigned [63:0] g_masked, bit unsigned [63:0] g_random); + return (masked_and(e_masked, e_random, f_masked, f_random) ^ masked_and(g_masked, g_random, ~e_masked, e_random)); +endfunction + +function bit unsigned [63:0] masked_Maj(bit unsigned [63:0] a_masked, bit unsigned [63:0] a_random, bit unsigned [63:0] b_masked, bit unsigned [63:0] b_random, bit unsigned [63:0] c_masked, bit unsigned [63:0] c_random); + return ((masked_and(a_masked, a_random, b_masked, b_random) ^ masked_and(a_masked, a_random, c_masked, c_random)) ^ masked_and(b_masked, b_random, c_masked, c_random)); +endfunction + +function bit unsigned [63:0] masked_and(bit unsigned [63:0] x_masked, bit unsigned [63:0] x_random, bit unsigned [63:0] y_masked, bit unsigned [63:0] y_random); + return ((~y_masked & ((~y_random & x_random) | (y_random & x_masked))) | (y_masked & ((y_random & x_random) | (~y_random & x_masked)))); +endfunction + +function bit unsigned [63:0] rotr1(bit unsigned [63:0] n); + return 64'(((n >> 64'd1) | (n << 64'd63))); +endfunction + +function bit unsigned [63:0] rotr14(bit unsigned [63:0] n); + return 64'(((n >> 64'd14) | (n << 64'd50))); +endfunction + +function bit unsigned [63:0] rotr18(bit unsigned [63:0] n); + return 64'(((n >> 64'd18) | (n << 64'd46))); +endfunction + +function bit unsigned [63:0] rotr19(bit unsigned [63:0] n); + return 64'(((n >> 64'd19) | (n << 64'd45))); +endfunction + +function bit unsigned [63:0] rotr28(bit unsigned [63:0] n); + return 64'(((n >> 64'd28) | (n << 64'd36))); +endfunction + +function bit unsigned [63:0] rotr34(bit unsigned [63:0] n); + return 64'(((n >> 64'd34) | (n << 64'd30))); +endfunction + +function bit unsigned [63:0] rotr39(bit unsigned [63:0] n); + return 64'(((n >> 64'd39) | (n << 64'd25))); +endfunction + +function bit unsigned [63:0] rotr41(bit unsigned [63:0] n); + return 64'(((n >> 64'd41) | (n << 64'd23))); +endfunction + +function bit unsigned [63:0] rotr61(bit unsigned [63:0] n); + return 64'(((n >> 64'd61) | (n << 64'd3))); +endfunction + +function bit unsigned [63:0] rotr8(bit unsigned [63:0] n); + return 64'(((n >> 64'd8) | (n << 64'd56))); +endfunction + +function bit unsigned [63:0] shr6(bit unsigned [63:0] n); + return (n >> 64'd6); +endfunction + +function bit unsigned [63:0] shr7(bit unsigned [63:0] n); + return (n >> 64'd7); +endfunction + +function bit unsigned [63:0] sigma0(bit unsigned [63:0] x); + return ((rotr28(x) ^ rotr34(x)) ^ rotr39(x)); +endfunction + +function bit unsigned [63:0] sigma1(bit unsigned [63:0] x); + return ((rotr14(x) ^ rotr18(x)) ^ rotr41(x)); +endfunction + +function bit unsigned [63:0] slicer(bit unsigned [1023:0] block, bit signed [31:0] index); + return(block[(64*index)+:64]); +endfunction + +function bit unsigned [511:0] compute_digest(bit unsigned [63:0] H_7, bit unsigned [63:0] h_random , bit unsigned [63:0] h_masked, bit unsigned [63:0] H_6, bit unsigned [63:0] g_random , bit unsigned [63:0] g_masked, bit unsigned [63:0] H_5, bit unsigned [63:0] f_random , bit unsigned [63:0] f_masked, bit unsigned [63:0] H_4, bit unsigned [63:0] e_random , bit unsigned [63:0] e_masked, bit unsigned [63:0] H_3, bit unsigned [63:0] d_random , bit unsigned [63:0] d_masked, bit unsigned [63:0] H_2, bit unsigned [63:0] c_random , bit unsigned [63:0] c_masked, bit unsigned [63:0] H_1, bit unsigned [63:0] b_random , bit unsigned [63:0] b_masked, bit unsigned [63:0] H_0, bit unsigned [63:0] a_random , bit unsigned [63:0] a_masked); + bit unsigned [511:0] temp; + temp[63:0] = 64'(H_7 + (h_masked ^ h_random)); + temp[127:64] = 64'(H_6 + (g_masked ^ g_random)); + temp[191:128] = 64'(H_5 + (f_masked ^ f_random)); + temp[255:192] = 64'(H_4 + (e_masked ^ e_random)); + temp[319:256] = 64'(H_3 + (d_masked ^ d_random)); + temp[383:320] = 64'(H_2 + (c_masked ^ c_random)); + temp[447:384] = 64'(H_1 + (b_masked ^ b_random)); + temp[511:448] = 64'(H_0 + (a_masked ^ a_random)); + return temp; + endfunction + +endpackage diff --git a/src/sha512_masked/formal/readme.md b/src/sha512_masked/formal/readme.md new file mode 100644 index 000000000..64b5d78d2 --- /dev/null +++ b/src/sha512_masked/formal/readme.md @@ -0,0 +1,66 @@ +# SHA512_MASKED +Date: 28-06-2023 +Author: LUBIS EDA + +## Folder Structure +The following subdirectories are part of the main directory **formal** + +- properties: Contains the assertion IP(AIP) named as **fv_sha512_masked.sv** and the constraints in place for the respective AIP **fv_constraints.sv** + + +## DUT Overview + +The DUT sha512_core has the primary inputs and primary outputs as shown below. + +| S.No | Port | Direction | Description | +| ---- | -------------------| --------- | --------------------------------------------------------------------------------- | +| 1 | clk | input | The positive edge of the clk is used for all the signals | +| 2 | reset_n | input | The reset signal is active low and resets the core | +| 3 | zeroize | input | The core is reseted when this signal is triggered. | +| 4 | init_cmd | input | The core is initialised with respective mode constants and processes the message. | +| 5 | next_cmd | input | The core processes the message block with the previously computed results | +| 6 | mode[1:0] | input | Define which hash function: SHA512,SHA384,SHA224,SHA256 | +| 7 | block_msg[1023:0] | input | The padded block message | +| 8 | lfsr_seed[73:0] | input | random bit vectors that are left shifted and rotated | +| 9 | ready | output | When triggered indicates that the core is ready | +| 10 | digest[511:0] | output | The hashed value of the given message block | +| 11 | digest_valid | output | When triggered indicates that the computed digest is ready | + +When the respective mode is selected and initalised the core iterates for 80 rounds to process the hash value with random lfsr seed value so as a countermeasure for single channel side-attacks. if the next is triggered then the previous values of the **H** registers are in place for processing the hash value. The digest is always generated of 512 bits, in which if the mode changes to 384 then from MSB 384 bits is a valid output and rest is garbage value. +## Assertion IP Overview + +The Assertion IP signals are bound with the respective signals in the dut, where for the **rst** in binded with the DUT (reset_n && !zeroize), which ensures the reset functionality. And another AIP signal block_in_valid is triggered whenever the init or next is high. + +- reset_a: Checks that all the resgiters are resetted and the state is idle, with the ready to high. + +- DONE_to_IDLE_a: Checks the necessary registers, outputs holds the values when state transits from Done to idle. + +- IDLE_to_CTRL_RND_a: Checks if the state is in idle, if there is an init_cmd or next_cmd, state transists to CTRL_RND and checks if the state registers are unchanged and round counter remains zero. + +- CTRL_RND_TO_CTRL_RND: State transition remains CTRL_RND as long as the round_counter values is less than 9 and checks the necessary registers, masking register holds corrcet value. + +- CTRL_RND_to_SHA_Rounds_224_a: Checks if the state is in ctrl_rnd ,the mode choosen as 224,the init is triggered then the registers should be initialised with the respective constants of 224. + +- CTRL_RND_to_SHA_Rounds_256_a: Checks if the state is in ctrl_rnd ,the mode choosen as 256,the init is triggered then the registers should be initialised with the respective constants of 256. + +- CTRL_RND_to_SHA_Rounds_512_a: Checks if the state is in ctrl_rnd ,the mode choosen as 512,the init is triggered then the registers should be initialised with the respective constants of 512. + +- CTRL_RND_to_SHA_Rounds_384_a: Checks if the state is in ctrl_rnd ,the mode choosen is neither 512,256 nor 224,the init is triggered then the registers should be initialised with the respective constants of default, which covers 384 mode also. + +- CTRL_RND_to_SHA_Rounds_next_a: Checks if the state is in ctrl_rnd and there is no init signal and the next signal asserts then the register holds the past values. + +- SHA_Rounds_to_DONE_a: Checks if the rounds are done then the registers are updated correctly. + +- SHA_Rounds_to_SHA_Rounds_before_16_a: Checks if the the rounds less than 16 then the necessary registers are updated correctly and the round increments. + +- SHA_Rounds_to_SHA_Rounds_after_16_a: Checks if the rounds are greater than 16 and less than 80 then the respective registers are updated correctly and the round increments. + +- IDLE_wait_a: Checks if there isn't either init or next signal triggered in idle state then the state stays in idle and holds the past values and the core is ready. + + +## Reproduce results +For reproducing the results: Load the AIP, sha512_masked_core and fv_constraints together in your formal tool. To ensure converging proves cut the following signals: + +- cut the respective signal **lfsr_inst.rnd** in formal tool. By cutting the signal model complexity is drastically reduced. + +Feel free to reach out to contact@lubis-eda.com to request the loadscripts. From de0e2196ff56baa2f2c25db2a28d84aaf9ff3682 Mon Sep 17 00:00:00 2001 From: advaith_sreevalsan Date: Fri, 24 Nov 2023 11:48:35 +0100 Subject: [PATCH 2/2] updated readme file --- src/sha512_masked/formal/readme.md | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/sha512_masked/formal/readme.md b/src/sha512_masked/formal/readme.md index 64b5d78d2..0a23239e2 100644 --- a/src/sha512_masked/formal/readme.md +++ b/src/sha512_masked/formal/readme.md @@ -59,8 +59,6 @@ The Assertion IP signals are bound with the respective signals in the dut, where ## Reproduce results -For reproducing the results: Load the AIP, sha512_masked_core and fv_constraints together in your formal tool. To ensure converging proves cut the following signals: - -- cut the respective signal **lfsr_inst.rnd** in formal tool. By cutting the signal model complexity is drastically reduced. +For reproducing the results: Load the AIP, sha512_masked_core and fv_constraints together in your formal tool. Feel free to reach out to contact@lubis-eda.com to request the loadscripts.