diff --git a/src/ecc/formal/fv_ecc_block_overview.pdf b/src/ecc/formal/fv_ecc_block_overview.pdf index 5454274fd..0effbcd67 100644 Binary files a/src/ecc/formal/fv_ecc_block_overview.pdf and b/src/ecc/formal/fv_ecc_block_overview.pdf differ diff --git a/src/ecc/formal/properties/coverpoints/fv_ecc_montgomerymultiplier_coverpoints.sv b/src/ecc/formal/properties/coverpoints/fv_ecc_montgomerymultiplier_coverpoints.sv index feaf4d2a7..717d4f00f 100644 --- 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 index c292f3430..6cd4fa0a8 100644 --- 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 index 09d962409..81afaf79e 100644 --- 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 index cf0a85a76..c689ac5b4 100644 --- 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 index b1f85eb10..cd77668be 100644 --- a/src/ecc/formal/properties/fv_ecc_fau.sv +++ b/src/ecc/formal/properties/fv_ecc_fau.sv @@ -75,7 +75,7 @@ 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 @@ -83,7 +83,7 @@ module fv_ecc_fau_m #( !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,6 +97,7 @@ 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 @@ -104,7 +105,7 @@ module fv_ecc_fau_m #( !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 index 3a4c45390..bf25df6dd 100644 --- 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 index 42011dd95..2a2d53775 100644 --- 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,12 +151,11 @@ 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; @@ -163,18 +163,19 @@ property multi_p(prime_i, mu_i,r_inv); 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); diff --git a/src/ecc/formal/properties/fv_montmultiplier_glue.sv b/src/ecc/formal/properties/fv_montmultiplier_glue.sv index ad8573f5c..650501e82 100644 --- a/src/ecc/formal/properties/fv_montmultiplier_glue.sv +++ b/src/ecc/formal/properties/fv_montmultiplier_glue.sv @@ -45,10 +45,10 @@ localparam [(FULL_REG_SIZE-REG_SIZE)-1 : 0] fv_zero_pad = '0; localparam prime_p = 384'hfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000ffffffff; localparam prime_q = 384'hffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52973; -localparam p_mu = 32'h00000001; -localparam q_mu = 32'he88fdc45; -localparam MULT_DLY = 40; -localparam DLY_CONCAT = MULT_DLY - (2*(PE_UNITS+1))-1; //27 +localparam p_mu = 48'h100000001; +localparam q_mu = 48'h6089e88fdc45; +localparam MULT_DLY = 28; +localparam DLY_CONCAT = MULT_DLY - (2*(PE_UNITS+1))-1; //17 ///////////////////////////////////////////////// @@ -116,13 +116,9 @@ logic [FULL_REG_SIZE-1:0] fv_reg; ##1 (1'b1, fv_reg[4*RADIX-1:3*RADIX] = (ecc_montgomerymultiplier.gen_PE[1].box_i.s_out)) ##1 (1'b1, fv_reg[5*RADIX-1:4*RADIX] = (ecc_montgomerymultiplier.gen_PE[2].box_i.s_out)) ##1 (1'b1, fv_reg[6*RADIX-1:5*RADIX] = (ecc_montgomerymultiplier.gen_PE[2].box_i.s_out)) - ##1 (1'b1, fv_reg[7*RADIX-1:6*RADIX] = (ecc_montgomerymultiplier.gen_PE[3].box_i.s_out)) - ##1 (1'b1, fv_reg[8*RADIX-1:7*RADIX] = (ecc_montgomerymultiplier.gen_PE[3].box_i.s_out)) - ##1 (1'b1, fv_reg[9*RADIX-1:8*RADIX] = (ecc_montgomerymultiplier.gen_PE[4].box_i.s_out)) - ##1 (1'b1, fv_reg[10*RADIX-1:9*RADIX] = (ecc_montgomerymultiplier.gen_PE[4].box_i.s_out)) - ##1 (1'b1, fv_reg[11*RADIX-1:10*RADIX] = (ecc_montgomerymultiplier.final_box.s_out)) - ##1 (1'b1, fv_reg[12*RADIX-1:11*RADIX] = (ecc_montgomerymultiplier.final_box.s_out)) - ##0 (1'b1, fv_reg[13*RADIX-1:12*RADIX] = (ecc_montgomerymultiplier.final_box.c_out[RADIX-1:0])) + ##1 (1'b1, fv_reg[7*RADIX-1:6*RADIX]= (ecc_montgomerymultiplier.final_box.s_out)) + ##1 (1'b1, fv_reg[8*RADIX-1:7*RADIX] = (ecc_montgomerymultiplier.final_box.s_out)) + ##0 (1'b1, fv_reg[9*RADIX-1:8*RADIX] = (ecc_montgomerymultiplier.final_box.c_out[RADIX-1:0])) ##0 (1'b1, fv_result = reduction_prime(fv_reg, prime)) |=> ##1 diff --git a/src/ecc/formal/properties/fv_pe_final.sv b/src/ecc/formal/properties/fv_pe_final.sv index 7e739e310..a639c25e3 100644 --- a/src/ecc/formal/properties/fv_pe_final.sv +++ b/src/ecc/formal/properties/fv_pe_final.sv @@ -58,7 +58,7 @@ property s_out_odd_p; odd && !start_in |=> - s_out == $past(32'(64'(a_in * b_in) + 64'(p_in * m_in)+ c_out + s_in)); + s_out == $past(48'(96'(a_in * b_in) + 96'(p_in * m_in)+ c_out + s_in)); endproperty s_out_odd_a : assert property (disable iff(!rst_n) s_out_odd_p); @@ -71,7 +71,7 @@ property s_out_noodd_p; !odd && !start_in |=> - s_out == $past(32'(64'(a_in * b_in) + 64'(p_in * m_in)+ c_in + s_out)); + s_out == $past(48'(96'(a_in * b_in) + 96'(p_in * m_in)+ c_in + s_out)); endproperty s_out_noodd_a : assert property (disable iff(!rst_n) s_out_noodd_p); @@ -83,7 +83,7 @@ property c_out_odd_p; logic [2*RADIX : 0] temp; odd && !start_in - ##0 (1'b1, temp = (64'(a_in * b_in) + 64'(p_in * m_in)+ c_out + s_in)) + ##0 (1'b1, temp = (96'(a_in * b_in) + 96'(p_in * m_in)+ c_out + s_in)) |=> //c_out == $past(33'((64'(a_in * b_in) + 64'(p_in * m_in)+ c_out + s_in)>>32)); c_out == temp[2*RADIX:RADIX]; @@ -98,7 +98,7 @@ property c_out_noodd_p; logic [2*RADIX : 0] temp; !odd && !start_in - ##0 (1'b1, temp = (64'(a_in * b_in) + 64'(p_in * m_in)+ c_in + s_out)) + ##0 (1'b1, temp = (96'(a_in * b_in) + 96'(p_in * m_in)+ c_in + s_out)) |=> //c_out == $past(33'((64'(a_in * b_in) + 64'(p_in * m_in)+ c_in + s_out)>>32)); c_out == temp[2*RADIX:RADIX]; diff --git a/src/ecc/formal/readme.md b/src/ecc/formal/readme.md index cdba90718..2dc10c983 100644 --- a/src/ecc/formal/readme.md +++ b/src/ecc/formal/readme.md @@ -1,5 +1,5 @@ -# Reproduce results - +# Reproducing results and Notable changes from caliptra 1.0 +The description of the proofs, is provided in the caliptra 1.0 version which are still valid. **MACROS :** TOP @@ -9,7 +9,20 @@ TOP FOR48 -- This macro is used for fv_montmultiplier.sv as the montgomery multiplier shorter version end-to-end checkers. Due to the restriction of the formal tool overmultiplication this file is used for only reduced version of the design. Further details are in the ECC_block_overview. +- This macro is used for fv_montmultiplier.sv as the montgomery multiplier shorter version end-to-end checkers. Due to the restriction of the formal tool overmultiplication this file is used for only reduced version of the design. This macro is for 48 bit version and radix as 4 which reproduces the same number of processing elements instantiations in the original version(384 bit and radix 48 bit). If this macro isn't enabled then 16 bit version of the multiplier proofs are set (16bit and Radix as 2) + +## Notable changes from caliptra 1.0 + +- The following sections for each module depicts the changes occurred + # Montgomery Multiplier + - Reduced version proofs for REG_SIZE 16 and 48 with RADIX 2 and 4 respectively + - Created a set of five different primes, p_mu, q_mu, r_inv to run the proofs + - Adapted the proofs for ecc_pe, ecc_pe_first and ecc_pe_final for RADIX 48 bit + - Similary the proofs were adjusted for the fv_montmultiplier_glue.sv for the RADIX 48bit + # HMAC_DRBG interface + - The interface has the lfsr_seed input previously of 148 bit wide in the latest version adopted the changes to 384 bit in the proofs + - For hmac_drbg and hmac_core can have the same AIP as the caliptra 1.0 as verifying those modules we would cut out the outputs from sha_masked and lfsr_seed is only fed to sha_masked as entropy. + ## Proving the submodules @@ -29,7 +42,7 @@ FOR48 If the following modules are chossen as a task then the respective signals need to be cut. - + # ecc_add_sub_mod_alter - cut the signals add_en_i, sub_i @@ -55,17 +68,17 @@ FOR48 - cut the signal ecc_cmd_i # ecc_hmac_drbg_interface - + - updates from previous version included the LFSR_SEED of 384 bit version into the proofs. - cut the signal counter_nonce, keygen_sign, hmac_drbg_i.drbg, hmac_drbg_i.ready,hmac_drbg_i.valid, internal signal counter_nonce. Constraints do the work by reducing the timing. # hmac_drbg - cut the signals init_cmd,next_cmd,nonce, entropy,u_sha512_core_h1.digest, - u_sha512_core_h2.digest,HMAC_K.tag,hmac_drbg_lfsr.rnd + u_sha512_core_h2.digest,HMAC_K.tag,HMAC_K.lfsr_inst_i.rnd # sha512_masked - - cut the signals init_cmd,next_cmd,mode,block_msg,sha_masked_lfsr.rnd + - cut the signals init_cmd,next_cmd,mode,block_msg,entropy # reduced versions - For montgomerymultiplier, scalar_blinding and ecc_pe_first modules, a reduced diff --git a/src/sha256/formal/model/sha256.h b/src/sha256/formal/model/sha256.h new file mode 100644 index 000000000..d1184d3f0 --- /dev/null +++ b/src/sha256/formal/model/sha256.h @@ -0,0 +1,369 @@ +// ------------------------------------------------- +// 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. +// + + +#ifndef SHA256_H +#define SHA256_H + +#include "systemc.h" +#include "Interfaces.h" +#include + +// Declare some constants to make the code easier to read +constexpr uint16_t DATA_WIDTH = 32; +constexpr uint16_t NUMBER_OF_MESSAGE_BLOCKS = 512 / DATA_WIDTH; +constexpr uint16_t NUMBER_OF_DIGEST_BLOCKS = 8; +const sc_uint<8> SHA256_ENDING = 0x80; + +// Declare some type aliases to make the code easier to read +using MessageBlockType = std::array; +using DigestBlockType = std::array; + +// Datatypes used for the communitcation with the environment +struct Sha256Request { + bool is_init; + bool is_next; + bool is_sha256_mode; + bool is_winternitz; + bool winternitz_n_mode; + uint8_t winternitz_w; + uint8_t winternitz_loop_init; + bool zerorize; + MessageBlockType message_block; +}; + +struct Sha256Response { + DigestBlockType digest_block; +}; + +// Datatypes used for the communication with the SHA256 core +// Using different datatypes/ports for the same hardware interface allows to write more abstract code +// and makes the code significantly easier to read, because a large amount of bitmanipulations can be +// moved from the code to the ESL to RTL mapping. +// ... for the regular SHA256 computation +struct Sha256CoreRequest { + bool init_command; + bool next_command; + bool is_sha256_mode; + bool zerorize; + MessageBlockType message_block; +}; +struct Sha256CoreResponse { + DigestBlockType digest_block; +}; + + +// ... for the winternitz computation in 256bit mode +using Tmp256Type = std::array; +struct Winternitz256BlockType { + sc_biguint<128> I; + sc_uint< 32> q; + sc_uint< 16> i; + sc_uint< 8> j; + Tmp256Type tmp; + sc_biguint< 72> padding; +}; +struct Sha256CoreWinternitz256Request { + bool init_command; + bool next_command; + bool is_sha256_mode; + bool zerorize; + Winternitz256BlockType message_block; +}; +struct Sha256CoreWinternitz256Response { + Tmp256Type tmp; +}; + +// ... for the winternitz computation in 192bit mode +using Tmp192Type = std::array; +struct Winternitz192BlockType { + sc_biguint<128> I; + sc_uint< 32> q; + sc_uint< 16> i; + sc_uint< 8> j; + Tmp192Type tmp; + sc_biguint<136> padding; +}; +struct Sha256CoreWinternitz192Request { + bool init_command; + bool next_command; + bool is_sha256_mode; + bool zerorize; + Winternitz192BlockType message_block; +}; +struct Sha256CoreWinternitz192Response { + Tmp192Type tmp; +}; + + +SC_MODULE(sha256) { + public: + // Interface to the environment + Sha256Request sha_request; + blocking_in sha_request_port; + shared_in sha_shared_request_port; + Sha256Response sha_response; + master_out sha_response_port; + + // Interface to the sha256 core submodule for regular sha256 computation + Sha256CoreRequest sha_core_request; + master_out sha_core_request_port; + Sha256CoreResponse sha_core_response; + blocking_in sha_core_response_port; + + // Interface to the sha256 core submodule for winternitz computations modes + Sha256CoreWinternitz256Request sha_core_winternitz256_request; + master_out sha_core_winternitz256_request_port; + Sha256CoreWinternitz256Response sha_core_winternitz256_response; + blocking_in sha_core_winternitz256_response_port; + + Sha256CoreWinternitz192Request sha_core_winternitz192_request; + master_out sha_core_winternitz192_request_port; + Sha256CoreWinternitz192Response sha_core_winternitz192_response; + blocking_in sha_core_winternitz192_response_port; + + // Constructor + SC_CTOR(sha256) { + SC_THREAD(sha); + } + + private: + // The number of loop iterations to compute a key candidate are: 2^w - 1 + // Without the first iteration it is 2^w - 2 + uint8_t compute_winternitz_iterations(uint8_t winternitz_w) const { + switch (winternitz_w) { + case 0: + return 0; + break; + + case 2: + return 2; + break; + + case 4: + return 14; + break; + + case 8: + return 254; + break; + + default: + return 0; + break; + } + } + + bool invalid_winternitz_w(uint8_t winternitz_w) const { + return (winternitz_w != 1 && + winternitz_w != 2 && + winternitz_w != 4 && + winternitz_w != 8); + } + + bool invalid_winternitz_j(uint8_t winternitz_loop_init, uint8_t loop_iterations) const { + return (winternitz_loop_init > loop_iterations); + } + + bool invalid_winternitz_mode(bool is_sha256_mode) const { + return !is_sha256_mode; + } + + bool is_winternitz_valid = false; + bool winternitz_error = false; + bool winternitz_error_w = false; + bool winternitz_error_j = false; + bool winternitz_error_mode = false; + + sc_biguint<128> winternitz_I = 0; + sc_uint<32> winternitz_q = 0; + sc_uint<16> winternitz_i = 0; + + uint8_t loop_counter = 0; + uint8_t loop_boundary; + uint8_t loop_iterations; + + bool pending_sha_request = false; + + void sha() { + pending_sha_request = false; + while (true) { + + sha_request_port->read(sha_request, "idle"); + + // Check if the request is for a valid winternitz computation + loop_iterations = + compute_winternitz_iterations(sha_request.winternitz_w); + + is_winternitz_valid = + sha_request.is_init && + sha_request.winternitz_loop_init <= loop_iterations; + if (sha_request.is_winternitz && is_winternitz_valid) { + + // winternitz_error_w = ( + // sha_request.winternitz_w != 1 && + // sha_request.winternitz_w != 2 && + // sha_request.winternitz_w != 4 && + // sha_request.winternitz_w != 8); + + // winternitz_error_j = + // (sha_request.winternitz_loop_init > loop_iterations); + + // winternitz_error_mode = !sha_request.is_sha256_mode; + + // winternitz_error = + // winternitz_error_w || + // winternitz_error_j || + // winternitz_error_mode; + + // sha_error.winternitz_error = winternitz_error; + // sha_error_port->set(sha_error); + + // Step1: Perform regular SHA256 computation + sha_core_request.init_command = true; + sha_core_request.next_command = false; + sha_core_request.is_sha256_mode = sha_request.is_sha256_mode; + sha_core_request.message_block = sha_request.message_block; + sha_core_request.zerorize = sha_request.zerorize; + sha_core_request_port->master_write(sha_core_request); + + loop_counter = sha_request.winternitz_loop_init; + loop_boundary = loop_iterations; + + winternitz_I = + (sc_biguint<128>(sha_request.message_block[0]) << 96) + + (sc_biguint<128>(sha_request.message_block[1]) << 64) + + (sc_biguint<128>(sha_request.message_block[2]) << 32) + + (sc_biguint<128>(sha_request.message_block[3]) ); + winternitz_q = + sc_uint<32>(sha_request.message_block[4]); + winternitz_i = + sc_uint<16>(sha_request.message_block[5] >> 16); + + if(sha_request.winternitz_n_mode) { + + sha_core_winternitz256_response_port->read(sha_core_winternitz256_response, "lms_1st_256"); + sha_response.digest_block = sha_core_winternitz256_response.tmp; + while (loop_counter < loop_boundary) { + loop_counter += 1; + + // Next stop: Perform 256 bit winternitz computation + sha_core_winternitz256_request.init_command = true; + sha_core_winternitz256_request.next_command = false; + sha_core_winternitz256_request.is_sha256_mode = true; + sha_core_winternitz256_request.message_block.I = winternitz_I; + sha_core_winternitz256_request.message_block.q = winternitz_q; + sha_core_winternitz256_request.message_block.i = winternitz_i; + sha_core_winternitz256_request.message_block.j = + static_cast>(loop_counter); + sha_core_winternitz256_request.message_block.tmp = + sha_core_winternitz256_response.tmp; + sha_core_winternitz256_request.message_block.padding = + (sc_biguint<72>(SHA256_ENDING) << 64) + + //(sc_biguint<72>(0x80) << 64) + + (sc_biguint<72>(0x01b8)); + sha_core_winternitz256_request.zerorize = sha_request.zerorize; + sha_core_winternitz256_request_port->master_write(sha_core_winternitz256_request); + + sha_core_winternitz256_response_port->read(sha_core_winternitz256_response, "lms_others_256"); + sha_response.digest_block = sha_core_winternitz256_response.tmp; + } + + } else { + + sha_core_winternitz192_response_port->read(sha_core_winternitz192_response, "lms_1st_192"); + sha_response.digest_block[0] = sha_core_winternitz192_response.tmp[0]; + sha_response.digest_block[1] = sha_core_winternitz192_response.tmp[1]; + sha_response.digest_block[2] = sha_core_winternitz192_response.tmp[2]; + sha_response.digest_block[3] = sha_core_winternitz192_response.tmp[3]; + sha_response.digest_block[4] = sha_core_winternitz192_response.tmp[4]; + sha_response.digest_block[5] = sha_core_winternitz192_response.tmp[5]; + sha_response.digest_block[6] = 0; + sha_response.digest_block[7] = 0; + while (loop_counter < loop_boundary) { + loop_counter += 1; + + // Next stop: Perform 192 bit winternitz computation + sha_core_winternitz192_request.init_command = true; + sha_core_winternitz192_request.next_command = false; + sha_core_winternitz192_request.is_sha256_mode = true; + sha_core_winternitz192_request.message_block.I = winternitz_I; + sha_core_winternitz192_request.message_block.q = winternitz_q; + sha_core_winternitz192_request.message_block.i = winternitz_i; + sha_core_winternitz192_request.message_block.j = + static_cast>(loop_counter); + sha_core_winternitz192_request.message_block.tmp = + sha_core_winternitz192_response.tmp; + sha_core_winternitz192_request.message_block.padding = + (sc_biguint<136>(SHA256_ENDING) << 128) + + //(sc_biguint<136>(0x80) << 128) + + (sc_biguint<136>(0x0178)); + sha_core_winternitz192_request.zerorize = sha_request.zerorize; + sha_core_winternitz192_request_port->master_write(sha_core_winternitz192_request); + + sha_core_winternitz192_response_port->read(sha_core_winternitz192_response, "lms_others_192"); + sha_response.digest_block[0] = sha_core_winternitz192_response.tmp[0]; + sha_response.digest_block[1] = sha_core_winternitz192_response.tmp[1]; + sha_response.digest_block[2] = sha_core_winternitz192_response.tmp[2]; + sha_response.digest_block[3] = sha_core_winternitz192_response.tmp[3]; + sha_response.digest_block[4] = sha_core_winternitz192_response.tmp[4]; + sha_response.digest_block[5] = sha_core_winternitz192_response.tmp[5]; + sha_response.digest_block[6] = 0; + sha_response.digest_block[7] = 0; + } + } + + // Send out the computed result + sha_response_port->master_write(sha_response); + + } else { + + // sha_error.winternitz_error = false; + + while(sha_request.is_init || sha_request.is_next) { + //do { + // Perform regular SHA operation + sha_core_request.init_command = sha_request.is_init; + sha_core_request.next_command = sha_request.is_next; + sha_core_request.is_sha256_mode = sha_request.is_sha256_mode; + sha_core_request.message_block = sha_request.message_block; + sha_core_request.zerorize = sha_request.zerorize; + sha_core_request_port->master_write(sha_core_request); + + sha_core_response_port->read(sha_core_response, "sha"); + + sha_response.digest_block = sha_core_response.digest_block; + sha_response.digest_block[7] = sha_request.is_sha256_mode ? sha_response.digest_block[7] : 0; + //if (!sha_request.is_sha256_mode) { + // sha_response.digest_block[7] = 0; + //} + + // Send out the computed result + sha_response_port->master_write(sha_response); + + // Check if the next request is already there + sha_shared_request_port->get(sha_request); + } + //} while(true); + } + } + } +}; + +#endif \ No newline at end of file diff --git a/src/sha256/formal/properties/fv_sha256.sv b/src/sha256/formal/properties/fv_sha256.sv index 356e51c80..79bb8650d 100644 --- a/src/sha256/formal/properties/fv_sha256.sv +++ b/src/sha256/formal/properties/fv_sha256.sv @@ -16,585 +16,1037 @@ // See the License for the specific language governing permissions and // limitations under the License. // +import sha256_package::*; -import fv_sha256_pkg::*; - -module fv_sha_256_m( - input bit rst, - input bit clk, - input bit unsigned [31:0] digest_out_0, - input bit unsigned [31:0] digest_out_1, - input bit unsigned [31:0] digest_out_2, - input bit unsigned [31:0] digest_out_3, - input bit unsigned [31:0] digest_out_4, - input bit unsigned [31:0] digest_out_5, - input bit unsigned [31:0] digest_out_6, - input bit unsigned [31:0] digest_out_7, - input bit block_init, - input bit block_mode, - input bit block_next, - input bit unsigned [31:0] block_in_0, - input bit unsigned [31:0] block_in_1, - input bit unsigned [31:0] block_in_2, - input bit unsigned [31:0] block_in_3, - input bit unsigned [31:0] block_in_4, - input bit unsigned [31:0] block_in_5, - input bit unsigned [31:0] block_in_6, - input bit unsigned [31:0] block_in_7, - input bit unsigned [31:0] block_in_8, - input bit unsigned [31:0] block_in_9, - input bit unsigned [31:0] block_in_10, - input bit unsigned [31:0] block_in_11, - input bit unsigned [31:0] block_in_12, - input bit unsigned [31:0] block_in_13, - input bit unsigned [31:0] block_in_14, - input bit unsigned [31:0] block_in_15, - input bit block_zeroize, - input bit block_in_valid, - input bit digest_valid, - input bit block_in_ready, - input bit unsigned [5:0] i, - input bit unsigned [31:0] W_0, - input bit unsigned [31:0] W_1, - input bit unsigned [31:0] W_2, - input bit unsigned [31:0] W_3, - input bit unsigned [31:0] W_4, - input bit unsigned [31:0] W_5, - input bit unsigned [31:0] W_6, - input bit unsigned [31:0] W_7, - input bit unsigned [31:0] W_8, - input bit unsigned [31:0] W_9, - input bit unsigned [31:0] W_10, - input bit unsigned [31:0] W_11, - input bit unsigned [31:0] W_12, - input bit unsigned [31:0] W_13, - input bit unsigned [31:0] W_14, - input bit unsigned [31:0] W_15, - input bit unsigned [31:0] H_0, - input bit unsigned [31:0] H_1, - input bit unsigned [31:0] H_2, - input bit unsigned [31:0] H_3, - input bit unsigned [31:0] H_4, - input bit unsigned [31:0] H_5, - input bit unsigned [31:0] H_6, - input bit unsigned [31:0] H_7, - input bit unsigned [31:0] a, - input bit unsigned [31:0] b, - input bit unsigned [31:0] c, - input bit unsigned [31:0] d, - input bit unsigned [31:0] e, - input bit unsigned [31:0] f, - input bit unsigned [31:0] g, - input bit unsigned [31:0] h, - input bit idle, - input bit ctrl_rotationss, - input bit ctrl_done + +// Functions + +function logic unsigned [7:0] compute_winternitz_iterations(logic unsigned [7:0] winternitz_w); + if ((winternitz_w == 8'd0)) + return 8'd0; + else if ((winternitz_w == 8'd2)) + return 8'd2; + else if ((winternitz_w == 8'd4)) + return 8'd14; + else if ((winternitz_w == 8'd8)) + return 8'd254; + else + return 8'd0; +endfunction + +function logic invalid_winternitz_j(logic unsigned [7:0] winternitz_loop_init, logic unsigned [7:0] loop_iterations); + return (winternitz_loop_init > loop_iterations); +endfunction + +function logic invalid_winternitz_mode(logic is_sha256_mode); + return !is_sha256_mode; +endfunction + +function logic invalid_winternitz_w(logic unsigned [7:0] winternitz_w); + return ((((winternitz_w != 8'd1) && (winternitz_w != 8'd2)) && (winternitz_w != 8'd4)) && (winternitz_w != 8'd8)); +endfunction + + +module fv_sha256 ( + input logic reset_n, + input logic top_reset_n, + input logic clk, + + // Ports + input logic sha_core_response_port_vld, + input logic sha_core_response_port_rdy, + input st_Sha256CoreResponse sha_core_response_port, + + input logic sha_core_winternitz192_response_port_vld, + input logic sha_core_winternitz192_response_port_rdy, + input st_Sha256CoreWinternitz192Response sha_core_winternitz192_response_port, + + input logic sha_core_winternitz256_response_port_vld, + input logic sha_core_winternitz256_response_port_rdy, + input st_Sha256CoreWinternitz256Response sha_core_winternitz256_response_port, + + input logic sha_request_port_vld, + input logic sha_request_port_rdy, + input st_Sha256Request sha_request_port, + + input st_Sha256Request sha_shared_request_port, + + input logic sha_core_request_port_vld, + input st_Sha256CoreRequest sha_core_request_port, + + input logic sha_core_winternitz192_request_port_vld, + input st_Sha256CoreWinternitz192Request sha_core_winternitz192_request_port, + + input logic sha_core_winternitz256_request_port_vld, + input st_Sha256CoreWinternitz256Request sha_core_winternitz256_request_port, + + input logic sha_response_port_vld, + input st_Sha256Response sha_response_port, + + // Registers + input logic unsigned [7:0] loop_boundary, + input logic unsigned [7:0] loop_counter, + input st_Sha256Request sha_request, + input logic unsigned [127:0] winternitz_I, + input logic unsigned [15:0] winternitz_i, + input logic unsigned [31:0] winternitz_q, + + // States + input logic idle, + input logic lms_1st_256, + input logic lms_others_256, + input logic lms_1st_192, + input logic lms_others_192, + input logic sha, + + // Manual + input logic hwif_in_register_error_reset, + input logic hwif_in_winternitz_error, + input logic hwif_in_sha_operation_error, + input logic hwif_in_error2, + input logic hwif_in_error3, + input logic hwif_in_command_done, + input logic [31:0] hwif_in_name0, + input logic [31:0] hwif_in_name1, + input logic [31:0] hwif_in_version0, + input logic [31:0] hwif_in_version1, + input logic hwif_in_valid, + input logic hwif_in_ready, + input logic hwif_in_wntz_busy, + input logic hwif_in_digest_clear, + input logic hwif_in_block_clear, + input logic hwif_in_control_zeroize, + input logic hwif_in_register_error_interrupt, + input logic hwif_in_register_notification_interrupt, + input logic error_interrupt, + input logic notification_interrupt, + input logic error, + input logic powergood, + input logic register_read_error, + input logic register_write_error, + input logic valid_register, + input logic ready_register, + input logic [2:0] wntz_fsm_next, + input logic [2:0] wntz_fsm, + input logic wntz_busy_register, + input logic core_init, + input logic core_next, + input logic core_digest_valid, + input logic debug_scan_switch, + input logic ready_flag_register, + input logic [0 : 7][31 : 0] digest_register, + input logic valid_flag_register, + input logic zeroize_register ); default clocking default_clk @(posedge clk); endclocking -logic [15:0][31:0] w; -logic [3:0] j; -assign j = i[3:0]; -assign w = {W_15,W_14,W_13,W_12,W_11,W_10,W_9,W_8,W_7,W_6,W_5,W_4,W_3,W_2,W_1,W_0}; -sequence reset_sequence; - !rst ##1 rst; -endsequence +// Define a SHA state for the DUV +logic sha_next; +logic sha_state; + +assign sha_next = + ((core_init || core_next) && wntz_fsm_next == WNTZ_IDLE) || + (!core_digest_valid && sha_state); + +always @(posedge clk or negedge reset_n) begin + if(!reset_n) + sha_state <= 1'b0; + else + sha_state <= sha_next; +end + + +// Define instances of data we receive from the ports +st_Sha256CoreResponse sha_core_response_0_i; +assign sha_core_response_0_i = '{ + digest_block: '{ 0: 0, 1: 0, 2: 0, 3: 0, 4: 0, 5: 0, 6: 0, 7: 0 } +}; + +st_Sha256Request sha_request_0_i; +assign sha_request_0_i = '{ + is_init: 0, + is_next: 0, + is_sha256_mode: 0, + is_winternitz: 0, + winternitz_n_mode: 0, + winternitz_w: 8'd0, + winternitz_loop_init: 8'd0, + zeroize: 0, + message_block: '{ + 0: 0, + 1: 0, + 2: 0, + 3: 0, + 4: 0, + 5: 0, + 6: 0, + 7: 0, + 8: 0, + 9: 0, + 10: 0, + 11: 0, + 12: 0, + 13: 0, + 14: 0, + 15: 0 + } +}; + +st_Sha256CoreRequest sha_core_request_1_i; +assign sha_core_request_1_i = '{ + init_command: 1, + next_command: 0, + is_sha256_mode: sha_request_port.is_sha256_mode, + zeroize: sha_request_port.zeroize, + message_block: sha_request_port.message_block +}; + +st_Sha256CoreRequest sha_core_request_2_i; +assign sha_core_request_2_i = '{ + init_command: sha_request_port.is_init, + next_command: sha_request_port.is_next, + is_sha256_mode: sha_request_port.is_sha256_mode, + zeroize: sha_request_port.zeroize, + message_block: sha_request_port.message_block +}; + +st_Sha256CoreWinternitz256Request sha_core_winternitz256_request_1_i; +assign sha_core_winternitz256_request_1_i = '{ + init_command: 1, + next_command: 0, + is_sha256_mode: 1, + zeroize: sha_request.zeroize, + message_block: '{ + I: winternitz_I, + q: winternitz_q, + i: winternitz_i, + j: 8'((loop_counter + 8'd1)), + tmp: sha_core_winternitz256_response_port.tmp, + padding: ((SHA256_ENDING << 72'd64) + 72'h1B8) + } +}; +st_Sha256Response sha_response_1_i; +assign sha_response_1_i = '{ + digest_block: sha_core_winternitz256_response_port.tmp +}; + +st_Sha256CoreWinternitz192Request sha_core_winternitz192_request_1_i; +assign sha_core_winternitz192_request_1_i = '{ + init_command: 1, + next_command: 0, + is_sha256_mode: 1, + zeroize: sha_request.zeroize, + message_block: '{ + I: winternitz_I, + q: winternitz_q, + i: winternitz_i, + j: 8'((loop_counter + 8'd1)), + tmp: sha_core_winternitz192_response_port.tmp, + padding: ((SHA256_ENDING << 136'd128) + 136'h178) + } +}; + +st_Sha256Response sha_response_2_i; +assign sha_response_2_i = '{ + digest_block: '{ + 0: sha_core_winternitz192_response_port.tmp[64'd0], + 1: sha_core_winternitz192_response_port.tmp[64'd1], + 2: sha_core_winternitz192_response_port.tmp[64'd2], + 3: sha_core_winternitz192_response_port.tmp[64'd3], + 4: sha_core_winternitz192_response_port.tmp[64'd4], + 5: sha_core_winternitz192_response_port.tmp[64'd5], + 6: 0, + 7: 0 + } +}; + +st_Sha256CoreRequest sha_core_request_3_i; +assign sha_core_request_3_i = '{ + init_command: sha_shared_request_port.is_init, + next_command: sha_shared_request_port.is_next, + is_sha256_mode: sha_shared_request_port.is_sha256_mode, + zeroize: sha_shared_request_port.zeroize, + message_block: sha_shared_request_port.message_block +}; + +st_Sha256Response sha_response_3_i; +assign sha_response_3_i = '{ + digest_block: '{ + 0: sha_core_response_port.digest_block['sd0], + 1: sha_core_response_port.digest_block['sd1], + 2: sha_core_response_port.digest_block['sd2], + 3: sha_core_response_port.digest_block['sd3], + 4: sha_core_response_port.digest_block['sd4], + 5: sha_core_response_port.digest_block['sd5], + 6: sha_core_response_port.digest_block['sd6], + 7: (sha_request.is_sha256_mode ? sha_core_response_port.digest_block[64'd7] : 0) + } +}; + + +assert_reset_zeroize: assert property( + ##0 (hwif_in_control_zeroize || debug_scan_switch) +|-> + ##1 ready_register == 1'b0 + && digest_register == 1'b0 + && valid_flag_register == 1'b0 +); -reset_a: assert property (reset_p); -property reset_p; - reset_sequence |-> +assert_reset_n: assert property (property_reset_n); +property property_reset_n; + !top_reset_n +|-> + ##1 idle && + loop_boundary == 8'd0 && + loop_counter == 8'd0 && + winternitz_I == 128'd0 && + winternitz_i == 16'd0 && + winternitz_q == 0; +endproperty + + +assert_winternitz_error: assert property( + disable iff(!reset_n) + + hwif_in_winternitz_error == ( + ( + (lms_1st_256 || lms_others_256 || lms_1st_192 || lms_others_192) && + (invalid_winternitz_mode(sha_request.is_sha256_mode) || + invalid_winternitz_w(sha_request.winternitz_w)) + ) || ( + sha_request_port.is_winternitz && + invalid_winternitz_j( + sha_request_port.winternitz_loop_init, + compute_winternitz_iterations(sha_request_port.winternitz_w) + ) + ) + ) +); + +assert_sha_operation_error: assert property( + disable iff(!reset_n) + + hwif_in_sha_operation_error == ( + sha_request.is_init && + sha_request.is_next + ) +); + +assert_error2: assert property( + disable iff(!reset_n) + hwif_in_error2 == 1'b0 +); + +assert_error3: assert property( + disable iff(!reset_n) + hwif_in_error3 == 1'b0 +); + +assert_connectivity_interrupts: assert property( + (error_interrupt == hwif_in_register_error_interrupt) && + (notification_interrupt == hwif_in_register_notification_interrupt) && + (error == register_read_error | register_write_error) +); + +assert_connectivity_name_version: assert property( + (hwif_in_name0 == sha256_params_pkg::SHA256_CORE_NAME0) && + (hwif_in_name1 == sha256_params_pkg::SHA256_CORE_NAME1) && + (hwif_in_version0 == sha256_params_pkg::SHA256_CORE_VERSION0) && + (hwif_in_version1 == sha256_params_pkg::SHA256_CORE_VERSION1) +); + +assert_connectivity_status: assert property( + hwif_in_ready == ready_register && + hwif_in_valid == valid_register && + hwif_in_wntz_busy == wntz_busy_register +); + +assert_connectivity_powergood: assert property( + powergood == hwif_in_register_error_reset +); + +assert_connectivity_zeroize: assert property( + (hwif_in_digest_clear == zeroize_register) && + (hwif_in_block_clear == zeroize_register) +); + +assert_command_done: assert property( + hwif_in_command_done == ( + (wntz_fsm == WNTZ_IDLE) & core_digest_valid & ($past(!core_digest_valid) | $past(wntz_fsm != WNTZ_IDLE)) + ) +); + + +assert_idle_to_lms_1st_192: assert property (disable iff(!reset_n) property_idle_to_lms_1st_192); +property property_idle_to_lms_1st_192; idle && - i == 'sd0 && - W_0 == 0 && - W_10 == 0 && - W_11 == 0 && - W_12 == 0 && - W_13 == 0 && - W_14 == 0 && - W_15 == 0 && - W_1 == 0 && - W_2 == 0 && - W_3 == 0 && - W_4 == 0 && - W_5 == 0 && - W_6 == 0 && - W_7 == 0 && - W_8 == 0 && - W_9 == 0 && - H_0 == 0 && - H_1 == 0 && - H_2 == 0 && - H_3 == 0 && - H_4 == 0 && - H_5 == 0 && - H_6 == 0 && - H_7 == 0 && - a == 0 && - b == 0 && - c == 0 && - d == 0 && - e == 0 && - f == 0 && - g == 0 && - h == 0 && - digest_valid == 0 && - block_in_ready == 1; + sha_request_port_vld && + sha_request_port.is_winternitz && + sha_request_port.is_init && + (sha_request_port.winternitz_loop_init <= compute_winternitz_iterations(sha_request_port.winternitz_w)) && + !sha_request_port.winternitz_n_mode +|-> + sha_core_request_port == sha_core_request_1_i + ##1 + lms_1st_192 && + loop_boundary == compute_winternitz_iterations($past(sha_request_port.winternitz_w, 1)) && + loop_counter == $past(sha_request_port.winternitz_loop_init, 1) && + winternitz_I == 128'( + (((($past(sha_request_port.message_block[64'd0], 1) << 128'd96) + + ($past(sha_request_port.message_block[64'd1], 1) << 128'd64)) + + ($past(sha_request_port.message_block[64'd2], 1) << 128'd32)) + + $past(sha_request_port.message_block[64'd3], 1)) + ) && + winternitz_i == 16'(($past(sha_request_port.message_block[64'd5], 1) >> 16)) && + winternitz_q == $past(sha_request_port.message_block[64'd4], 1); endproperty -DONE_to_IDLE_a: assert property (disable iff(!rst) DONE_to_IDLE_p); -property DONE_to_IDLE_p; - ctrl_done +assert_idle_to_lms_1st_256: assert property (disable iff(!reset_n) property_idle_to_lms_1st_256); +property property_idle_to_lms_1st_256; + idle && + sha_request_port_vld && + sha_request_port.is_winternitz && + sha_request_port.is_init && + (sha_request_port.winternitz_loop_init <= compute_winternitz_iterations(sha_request_port.winternitz_w)) && + sha_request_port.winternitz_n_mode |-> + sha_core_request_port == sha_core_request_1_i ##1 + lms_1st_256 && + loop_boundary == compute_winternitz_iterations($past(sha_request_port.winternitz_w, 1)) && + loop_counter == $past(sha_request_port.winternitz_loop_init, 1) && + winternitz_I == 128'( + (((($past(sha_request_port.message_block[64'd0], 1) << 128'd96) + + ($past(sha_request_port.message_block[64'd1], 1) << 128'd64)) + + ($past(sha_request_port.message_block[64'd2], 1) << 128'd32)) + + $past(sha_request_port.message_block[64'd3], 1)) + ) && + winternitz_i == 16'(($past(sha_request_port.message_block[64'd5], 1) >> 16)) && + winternitz_q == $past(sha_request_port.message_block[64'd4], 1); +endproperty + + +assert_idle_to_sha: assert property (disable iff(!reset_n) property_idle_to_sha); +property property_idle_to_sha; idle && - digest_out_0 == ($past(a, 1) + $past(H_0, 1)) && - digest_out_1 == ($past(b, 1) + $past(H_1, 1)) && - digest_out_2 == ($past(c, 1) + $past(H_2, 1)) && - digest_out_3 == ($past(d, 1) + $past(H_3, 1)) && - digest_out_4 == ($past(e, 1) + $past(H_4, 1)) && - digest_out_5 == ($past(f, 1) + $past(H_5, 1)) && - digest_out_6 == ($past(g, 1) + $past(H_6, 1)) && - digest_out_7 == ($past(h, 1) + $past(H_7, 1)) && - i == $past(i, 1) && - W_0 == $past(W_0, 1) && - W_10 == $past(W_10, 1) && - W_11 == $past(W_11, 1) && - W_12 == $past(W_12, 1) && - W_13 == $past(W_13, 1) && - W_14 == $past(W_14, 1) && - W_15 == $past(W_15, 1) && - W_1 == $past(W_1, 1) && - W_2 == $past(W_2, 1) && - W_3 == $past(W_3, 1) && - W_4 == $past(W_4, 1) && - W_5 == $past(W_5, 1) && - W_6 == $past(W_6, 1) && - W_7 == $past(W_7, 1) && - W_8 == $past(W_8, 1) && - W_9 == $past(W_9, 1) && - H_0 == ($past(a, 1) + $past(H_0, 1)) && - H_1 == ($past(b, 1) + $past(H_1, 1)) && - H_2 == ($past(c, 1) + $past(H_2, 1)) && - H_3 == ($past(d, 1) + $past(H_3, 1)) && - H_4 == ($past(e, 1) + $past(H_4, 1)) && - H_5 == ($past(f, 1) + $past(H_5, 1)) && - H_6 == ($past(g, 1) + $past(H_6, 1)) && - H_7 == ($past(h, 1) + $past(H_7, 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) && - digest_valid == 1 && - block_in_ready == 1; + sha_request_port_vld && + !((sha_request_port.is_winternitz && sha_request_port.is_init) && (sha_request_port.winternitz_loop_init <= compute_winternitz_iterations(sha_request_port.winternitz_w))) && + (sha_request_port.is_init || sha_request_port.is_next) +|-> + sha_core_request_port == sha_core_request_2_i + ##1 + sha_state && + loop_boundary == $past(loop_boundary, 1) && + loop_counter == $past(loop_counter, 1) && + winternitz_I == $past(winternitz_I, 1) && + winternitz_i == $past(winternitz_i, 1) && + winternitz_q == $past(winternitz_q, 1); endproperty +assert_lms_1st_192_to_idle: assert property (disable iff(!reset_n) property_lms_1st_192_to_idle); +property property_lms_1st_192_to_idle; + lms_1st_192 && + sha_core_winternitz192_response_port_vld && + (loop_boundary <= loop_counter) +|-> + ##1 + idle && + loop_boundary == $past(loop_boundary, 1) && + loop_counter == $past(loop_counter, 1) && + sha_response_port == $past(sha_response_2_i, 1) && + winternitz_I == $past(winternitz_I, 1) && + winternitz_i == $past(winternitz_i, 1) && + winternitz_q == $past(winternitz_q, 1); +endproperty -SHA_Rounds_to_DONE_a: assert property (disable iff(!rst) SHA_Rounds_to_DONE_p); -property SHA_Rounds_to_DONE_p; - ctrl_rotationss && - (i >= 'sd16) && - (('sd1 + i) >= 'sd64) + + +assert_lms_1st_192_to_lms_others_192: assert property (disable iff(!reset_n) property_lms_1st_192_to_lms_others_192); +property property_lms_1st_192_to_lms_others_192; + lms_1st_192 && + sha_core_winternitz192_response_port_vld && + (loop_boundary > loop_counter) |-> - ##1 (digest_valid == 0) and - ##1 (block_in_ready == 0) and ##1 - ctrl_done && - i == 'sd0 && - W_0 == $past(W_1, 1) && - W_10 == $past(W_11, 1) && - W_11 == $past(W_12, 1) && - W_12 == $past(W_13, 1) && - W_13 == $past(W_14, 1) && - W_14 == $past(W_15, 1) && - W_15 == $past(compute_w(W_14,W_9,W_1,W_0)) && - W_1 == $past(W_2, 1) && - W_2 == $past(W_3, 1) && - W_3 == $past(W_4, 1) && - W_4 == $past(W_5, 1) && - W_5 == $past(W_6, 1) && - W_6 == $past(W_7, 1) && - W_7 == $past(W_8, 1) && - W_8 == $past(W_9, 1) && - W_9 == $past(W_10, 1) && - H_0 == $past(H_0, 1) && - H_1 == $past(H_1, 1) && - H_2 == $past(H_2, 1) && - H_3 == $past(H_3, 1) && - H_4 == $past(H_4, 1) && - H_5 == $past(H_5, 1) && - H_6 == $past(H_6, 1) && - H_7 == $past(H_7, 1) && - a == $past(newa(mult_xor(a, 2, 13, 22),majority(a,b,c),Summ(compute_w(W_14,W_9,W_1,W_0),K[i],h,choose(e,f,g),mult_xor(e, 6, 11, 25)))) && - b == $past(a, 1) && - c == $past(b, 1) && - d == $past(c, 1) && - e == $past(newe(d,Summ(compute_w(W_14,W_9,W_1,W_0),K[i],h,choose(e,f,g),mult_xor(e,6,11,25)))) && - f == $past(e, 1) && - g == $past(f, 1) && - h == $past(g, 1); + lms_others_192 && + loop_boundary == $past(loop_boundary, 1) && + loop_counter == 8'((1 + $past(loop_counter, 1))) && + sha_core_winternitz192_request_port.init_command == $past(sha_core_winternitz192_request_1_i.init_command, 1) && + sha_core_winternitz192_request_port.next_command == $past(sha_core_winternitz192_request_1_i.next_command, 1) && + sha_core_winternitz192_request_port.is_sha256_mode == $past(sha_core_winternitz192_request_1_i.is_sha256_mode, 1) && + sha_core_winternitz192_request_port.zeroize == sha_core_winternitz192_request_1_i.zeroize && + sha_core_winternitz192_request_port.message_block == $past(sha_core_winternitz192_request_1_i.message_block, 1) && + winternitz_I == $past(winternitz_I, 1) && + winternitz_i == $past(winternitz_i, 1) && + winternitz_q == $past(winternitz_q, 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; - ctrl_rotationss && - (i < 'sd16) +assert_lms_1st_256_to_idle: assert property (disable iff(!reset_n) property_lms_1st_256_to_idle); +property property_lms_1st_256_to_idle; + lms_1st_256 && + sha_core_winternitz256_response_port_vld && + (loop_boundary <= loop_counter) |-> - ##1 (digest_valid == 0) and - ##1 (block_in_ready == 0) and ##1 - ctrl_rotationss && - i == ('sd1 + $past(i, 1)) && - W_0 == $past(W_0, 1) && - W_10 == $past(W_10, 1) && - W_11 == $past(W_11, 1) && - W_12 == $past(W_12, 1) && - W_13 == $past(W_13, 1) && - W_14 == $past(W_14, 1) && - W_15 == $past(W_15, 1) && - W_1 == $past(W_1, 1) && - W_2 == $past(W_2, 1) && - W_3 == $past(W_3, 1) && - W_4 == $past(W_4, 1) && - W_5 == $past(W_5, 1) && - W_6 == $past(W_6, 1) && - W_7 == $past(W_7, 1) && - W_8 == $past(W_8, 1) && - W_9 == $past(W_9, 1) && - H_0 == $past(H_0, 1) && - H_1 == $past(H_1, 1) && - H_2 == $past(H_2, 1) && - H_3 == $past(H_3, 1) && - H_4 == $past(H_4, 1) && - H_5 == $past(H_5, 1) && - H_6 == $past(H_6, 1) && - H_7 == $past(H_7, 1) && - a == $past(newa(mult_xor(a, 2, 13, 22),majority(a,b,c),Summ(w[j],K[i],h,choose(e,f,g),mult_xor(e, 6, 11, 25)))) && - b == $past(a, 1) && - c == $past(b, 1) && - d == $past(c, 1) && - e == $past(newe(d,Summ(w[j],K[i],h,choose(e,f,g),mult_xor(e,6,11,25)))) && - f == $past(e, 1) && - g == $past(f, 1) && - h == $past(g, 1); + idle && + loop_boundary == $past(loop_boundary, 1) && + loop_counter == $past(loop_counter, 1) && + sha_response_port == $past(sha_response_1_i, 1) && + winternitz_I == $past(winternitz_I, 1) && + winternitz_i == $past(winternitz_i, 1) && + winternitz_q == $past(winternitz_q, 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; - ctrl_rotationss && - (i >= 'sd16) && - (('sd1 + i) < 'sd64) +assert_lms_1st_256_to_lms_others_256: assert property (disable iff(!reset_n) property_lms_1st_256_to_lms_others_256); +property property_lms_1st_256_to_lms_others_256; + lms_1st_256 && + sha_core_winternitz256_response_port_vld && + (loop_boundary > loop_counter) |-> - ##1 (digest_valid == 0) and - ##1 (block_in_ready == 0) and ##1 - ctrl_rotationss && - i == ('sd1 + $past(i, 1)) && - W_0 == $past(W_1, 1) && - W_10 == $past(W_11, 1) && - W_11 == $past(W_12, 1) && - W_12 == $past(W_13, 1) && - W_13 == $past(W_14, 1) && - W_14 == $past(W_15, 1) && - W_15 == $past(compute_w(W_14,W_9,W_1,W_0)) && - W_1 == $past(W_2, 1) && - W_2 == $past(W_3, 1) && - W_3 == $past(W_4, 1) && - W_4 == $past(W_5, 1) && - W_5 == $past(W_6, 1) && - W_6 == $past(W_7, 1) && - W_7 == $past(W_8, 1) && - W_8 == $past(W_9, 1) && - W_9 == $past(W_10, 1) && - H_0 == $past(H_0, 1) && - H_1 == $past(H_1, 1) && - H_2 == $past(H_2, 1) && - H_3 == $past(H_3, 1) && - H_4 == $past(H_4, 1) && - H_5 == $past(H_5, 1) && - H_6 == $past(H_6, 1) && - H_7 == $past(H_7, 1) && - a == $past(newa(mult_xor(a, 2, 13, 22),majority(a,b,c),Summ(compute_w(W_14,W_9,W_1,W_0),K[i],h,choose(e,f,g),mult_xor(e, 6, 11, 25)))) && - b == $past(a, 1) && - c == $past(b, 1) && - d == $past(c, 1) && - e == $past(newe(d,Summ(compute_w(W_14,W_9,W_1,W_0),K[i],h,choose(e,f,g),mult_xor(e,6,11,25)))) && - f == $past(e, 1) && - g == $past(f, 1) && - h == $past(g, 1); + lms_others_256 && + loop_boundary == $past(loop_boundary, 1) && + loop_counter == 8'((1 + $past(loop_counter, 1))) && + sha_core_winternitz256_request_port.init_command == $past(sha_core_winternitz256_request_1_i.init_command, 1) && + sha_core_winternitz256_request_port.next_command == $past(sha_core_winternitz256_request_1_i.next_command, 1) && + sha_core_winternitz256_request_port.is_sha256_mode == $past(sha_core_winternitz256_request_1_i.is_sha256_mode, 1) && + sha_core_winternitz256_request_port.zeroize == sha_core_winternitz256_request_1_i.zeroize && + sha_core_winternitz256_request_port.message_block == $past(sha_core_winternitz256_request_1_i.message_block, 1) && + winternitz_I == $past(winternitz_I, 1) && + winternitz_i == $past(winternitz_i, 1) && + winternitz_q == $past(winternitz_q, 1); endproperty -IDLE_to_SHA_Rounds_224_a: assert property (disable iff(!rst) IDLE_to_SHA_Rounds_224_p); -property IDLE_to_SHA_Rounds_224_p; +assert_lms_others_192_to_idle: assert property (disable iff(!reset_n) property_lms_others_192_to_idle); +property property_lms_others_192_to_idle; + lms_others_192 && + sha_core_winternitz192_response_port_vld && + (loop_boundary <= loop_counter) +|-> + ##1 idle && - block_in_valid && - block_init && - !block_mode + loop_boundary == $past(loop_boundary, 1) && + loop_counter == $past(loop_counter, 1) && + sha_response_port == $past(sha_response_2_i, 1) && + winternitz_I == $past(winternitz_I, 1) && + winternitz_i == $past(winternitz_i, 1) && + winternitz_q == $past(winternitz_q, 1); +endproperty + + +assert_lms_others_192_to_lms_others_192: assert property (disable iff(!reset_n) property_lms_others_192_to_lms_others_192); +property property_lms_others_192_to_lms_others_192; + lms_others_192 && + sha_core_winternitz192_response_port_vld && + (loop_boundary > loop_counter) |-> - ##1 (digest_valid == 0) and - ##1 (block_in_ready == 0) and ##1 - ctrl_rotationss && - i == 'sd0 && - W_0 == $past(block_in_15, 1) && - W_10 == $past(block_in_5, 1) && - W_11 == $past(block_in_4, 1) && - W_12 == $past(block_in_3, 1) && - W_13 == $past(block_in_2, 1) && - W_14 == $past(block_in_1, 1) && - W_15 == $past(block_in_0, 1) && - W_1 == $past(block_in_14, 1) && - W_2 == $past(block_in_13, 1) && - W_3 == $past(block_in_12, 1) && - W_4 == $past(block_in_11, 1) && - W_5 == $past(block_in_10, 1) && - W_6 == $past(block_in_9, 1) && - W_7 == $past(block_in_8, 1) && - W_8 == $past(block_in_7, 1) && - W_9 == $past(block_in_6, 1) && - H_0 == 32'd3238371032 && - H_1 == 32'd914150663 && - H_2 == 32'd812702999 && - H_3 == 32'd4144912697 && - H_4 == 32'd4290775857 && - H_5 == 32'd1750603025 && - H_6 == 32'd1694076839 && - H_7 == 32'd3204075428 && - a == 32'd3238371032 && - b == 32'd914150663 && - c == 32'd812702999 && - d == 32'd4144912697 && - e == 32'd4290775857 && - f == 32'd1750603025 && - g == 32'd1694076839 && - h == 32'd3204075428; + lms_others_192 && + loop_boundary == $past(loop_boundary, 1) && + loop_counter == 8'((1 + $past(loop_counter, 1))) && + sha_core_winternitz192_request_port.init_command == $past(sha_core_winternitz192_request_1_i.init_command, 1) && + sha_core_winternitz192_request_port.next_command == $past(sha_core_winternitz192_request_1_i.next_command, 1) && + sha_core_winternitz192_request_port.is_sha256_mode == $past(sha_core_winternitz192_request_1_i.is_sha256_mode, 1) && + sha_core_winternitz192_request_port.zeroize == sha_core_winternitz192_request_1_i.zeroize && + sha_core_winternitz192_request_port.message_block == $past(sha_core_winternitz192_request_1_i.message_block, 1) && + winternitz_I == $past(winternitz_I, 1) && + winternitz_i == $past(winternitz_i, 1) && + winternitz_q == $past(winternitz_q, 1); endproperty -IDLE_to_SHA_Rounds_256_a: assert property (disable iff(!rst) IDLE_to_SHA_Rounds_256_p); -property IDLE_to_SHA_Rounds_256_p; +assert_lms_others_256_to_idle: assert property (disable iff(!reset_n) property_lms_others_256_to_idle); +property property_lms_others_256_to_idle; + lms_others_256 && + sha_core_winternitz256_response_port_vld && + (loop_boundary <= loop_counter) +|-> + ##1 idle && - block_in_valid && - block_init && - block_mode + loop_boundary == $past(loop_boundary, 1) && + loop_counter == $past(loop_counter, 1) && + sha_response_port == $past(sha_response_1_i, 1) && + winternitz_I == $past(winternitz_I, 1) && + winternitz_i == $past(winternitz_i, 1) && + winternitz_q == $past(winternitz_q, 1); +endproperty + + +assert_lms_others_256_to_lms_others_256: assert property (disable iff(!reset_n) property_lms_others_256_to_lms_others_256); +property property_lms_others_256_to_lms_others_256; + lms_others_256 && + sha_core_winternitz256_response_port_vld && + (loop_boundary > loop_counter) |-> - ##1 (digest_valid == 0) and - ##1 (block_in_ready == 0) and ##1 - ctrl_rotationss && - i == 'sd0 && - W_0 == $past(block_in_15, 1) && - W_10 == $past(block_in_5, 1) && - W_11 == $past(block_in_4, 1) && - W_12 == $past(block_in_3, 1) && - W_13 == $past(block_in_2, 1) && - W_14 == $past(block_in_1, 1) && - W_15 == $past(block_in_0, 1) && - W_1 == $past(block_in_14, 1) && - W_2 == $past(block_in_13, 1) && - W_3 == $past(block_in_12, 1) && - W_4 == $past(block_in_11, 1) && - W_5 == $past(block_in_10, 1) && - W_6 == $past(block_in_9, 1) && - W_7 == $past(block_in_8, 1) && - W_8 == $past(block_in_7, 1) && - W_9 == $past(block_in_6, 1) && - H_0 == 32'd1779033703 && - H_1 == 32'd3144134277 && - H_2 == 32'd1013904242 && - H_3 == 32'd2773480762 && - H_4 == 32'd1359893119 && - H_5 == 32'd2600822924 && - H_6 == 32'd528734635 && - H_7 == 32'd1541459225 && - a == 32'd1779033703 && - b == 32'd3144134277 && - c == 32'd1013904242 && - d == 32'd2773480762 && - e == 32'd1359893119 && - f == 32'd2600822924 && - g == 32'd528734635 && - h == 32'd1541459225; + lms_others_256 && + loop_boundary == $past(loop_boundary, 1) && + loop_counter == 8'((1 + $past(loop_counter, 1))) && + sha_core_winternitz256_request_port.init_command == $past(sha_core_winternitz256_request_1_i.init_command, 1) && + sha_core_winternitz256_request_port.next_command == $past(sha_core_winternitz256_request_1_i.next_command, 1) && + sha_core_winternitz256_request_port.is_sha256_mode == $past(sha_core_winternitz256_request_1_i.is_sha256_mode, 1) && + sha_core_winternitz256_request_port.zeroize == sha_core_winternitz256_request_1_i.zeroize && + sha_core_winternitz256_request_port.message_block == $past(sha_core_winternitz256_request_1_i.message_block, 1) && + winternitz_I == $past(winternitz_I, 1) && + winternitz_i == $past(winternitz_i, 1) && + winternitz_q == $past(winternitz_q, 1); endproperty -IDLE_to_SHA_Rounds_next_a: assert property (disable iff(!rst) IDLE_to_SHA_Rounds_next_p); -property IDLE_to_SHA_Rounds_next_p; +assert_sha_to_idle: assert property (disable iff(!reset_n) property_sha_to_idle); +property property_sha_to_idle; + sha_state && + sha_core_response_port_vld && + !sha_shared_request_port.is_init && + !sha_shared_request_port.is_next +|-> + ##1 idle && - block_in_valid && - !block_init + loop_boundary == $past(loop_boundary, 1) && + loop_counter == $past(loop_counter, 1) && + sha_response_port == $past(sha_response_3_i, 1) && + winternitz_I == $past(winternitz_I, 1) && + winternitz_i == $past(winternitz_i, 1) && + winternitz_q == $past(winternitz_q, 1); +endproperty + + +assert_sha_to_sha: assert property (disable iff(!reset_n) property_sha_to_sha); +property property_sha_to_sha; + sha_state && + sha_core_response_port_vld && + (sha_shared_request_port.is_init || sha_shared_request_port.is_next) |-> - ##1 (digest_valid == 0) and - ##1 (block_in_ready == 0) and + sha_core_request_port == sha_core_request_3_i ##1 - ctrl_rotationss && - i == 'sd0 && - W_0 == $past(block_in_15, 1) && - W_10 == $past(block_in_5, 1) && - W_11 == $past(block_in_4, 1) && - W_12 == $past(block_in_3, 1) && - W_13 == $past(block_in_2, 1) && - W_14 == $past(block_in_1, 1) && - W_15 == $past(block_in_0, 1) && - W_1 == $past(block_in_14, 1) && - W_2 == $past(block_in_13, 1) && - W_3 == $past(block_in_12, 1) && - W_4 == $past(block_in_11, 1) && - W_5 == $past(block_in_10, 1) && - W_6 == $past(block_in_9, 1) && - W_7 == $past(block_in_8, 1) && - W_8 == $past(block_in_7, 1) && - W_9 == $past(block_in_6, 1) && - H_0 == $past(H_0, 1) && - H_1 == $past(H_1, 1) && - H_2 == $past(H_2, 1) && - H_3 == $past(H_3, 1) && - H_4 == $past(H_4, 1) && - H_5 == $past(H_5, 1) && - H_6 == $past(H_6, 1) && - H_7 == $past(H_7, 1) && - a == $past(H_0, 1) && - b == $past(H_1, 1) && - c == $past(H_2, 1) && - d == $past(H_3, 1) && - e == $past(H_4, 1) && - f == $past(H_5, 1) && - g == $past(H_6, 1) && - h == $past(H_7, 1); + sha_state && + loop_boundary == $past(loop_boundary, 1) && + loop_counter == $past(loop_counter, 1) && + sha_response_port == $past(sha_response_3_i, 1) && + winternitz_I == $past(winternitz_I, 1) && + winternitz_i == $past(winternitz_i, 1) && + winternitz_q == $past(winternitz_q, 1); endproperty -idle_wait_a: assert property (disable iff(!rst) idle_wait_p); -property idle_wait_p; +assert_idle_wait: assert property (disable iff(!reset_n) property_idle_wait); +property property_idle_wait; idle && - !block_in_valid + !sha_request_port_vld |-> ##1 idle && - i == $past(i, 1) && - W_0 == $past(W_0, 1) && - W_10 == $past(W_10, 1) && - W_11 == $past(W_11, 1) && - W_12 == $past(W_12, 1) && - W_13 == $past(W_13, 1) && - W_14 == $past(W_14, 1) && - W_15 == $past(W_15, 1) && - W_1 == $past(W_1, 1) && - W_2 == $past(W_2, 1) && - W_3 == $past(W_3, 1) && - W_4 == $past(W_4, 1) && - W_5 == $past(W_5, 1) && - W_6 == $past(W_6, 1) && - W_7 == $past(W_7, 1) && - W_8 == $past(W_8, 1) && - W_9 == $past(W_9, 1) && - H_0 == $past(H_0, 1) && - H_1 == $past(H_1, 1) && - H_2 == $past(H_2, 1) && - H_3 == $past(H_3, 1) && - H_4 == $past(H_4, 1) && - H_5 == $past(H_5, 1) && - H_6 == $past(H_6, 1) && - H_7 == $past(H_7, 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) && - digest_valid == $past(digest_valid) && - block_in_ready == 1; + loop_boundary == $past(loop_boundary, 1) && + loop_counter == $past(loop_counter, 1) && + winternitz_I == $past(winternitz_I, 1) && + winternitz_i == $past(winternitz_i, 1) && + winternitz_q == $past(winternitz_q, 1); +endproperty + + +assert_lms_1st_192_wait: assert property (disable iff(!reset_n) property_lms_1st_192_wait); +property property_lms_1st_192_wait; + lms_1st_192 && + !sha_core_winternitz192_response_port_vld +|-> + ##1 + lms_1st_192 && + loop_boundary == $past(loop_boundary, 1) && + loop_counter == $past(loop_counter, 1) && + winternitz_I == $past(winternitz_I, 1) && + winternitz_i == $past(winternitz_i, 1) && + winternitz_q == $past(winternitz_q, 1); +endproperty + + +assert_lms_1st_256_wait: assert property (disable iff(!reset_n) property_lms_1st_256_wait); +property property_lms_1st_256_wait; + lms_1st_256 && + !sha_core_winternitz256_response_port_vld +|-> + ##1 + lms_1st_256 && + loop_boundary == $past(loop_boundary, 1) && + loop_counter == $past(loop_counter, 1) && + winternitz_I == $past(winternitz_I, 1) && + winternitz_i == $past(winternitz_i, 1) && + winternitz_q == $past(winternitz_q, 1); +endproperty + + +assert_lms_others_192_wait: assert property (disable iff(!reset_n) property_lms_others_192_wait); +property property_lms_others_192_wait; + lms_others_192 && + !sha_core_winternitz192_response_port_vld +|-> + ##1 + lms_others_192 && + loop_boundary == $past(loop_boundary, 1) && + loop_counter == $past(loop_counter, 1) && + winternitz_I == $past(winternitz_I, 1) && + winternitz_i == $past(winternitz_i, 1) && + winternitz_q == $past(winternitz_q, 1); +endproperty + + +assert_lms_others_256_wait: assert property (disable iff(!reset_n) property_lms_others_256_wait); +property property_lms_others_256_wait; + lms_others_256 && + !sha_core_winternitz256_response_port_vld +|-> + ##1 + lms_others_256 && + loop_boundary == $past(loop_boundary, 1) && + loop_counter == $past(loop_counter, 1) && + winternitz_I == $past(winternitz_I, 1) && + winternitz_i == $past(winternitz_i, 1) && + winternitz_q == $past(winternitz_q, 1); +endproperty + + +assert_sha_wait: assert property (disable iff(!reset_n) property_sha_wait); +property property_sha_wait; + sha_state && + !sha_core_response_port_vld +|-> + ##1 + sha_state && + loop_boundary == $past(loop_boundary, 1) && + loop_counter == $past(loop_counter, 1) && + winternitz_I == $past(winternitz_I, 1) && + winternitz_i == $past(winternitz_i, 1) && + winternitz_q == $past(winternitz_q, 1); endproperty endmodule +module fv_sha256_ref_wrapper; + + +default clocking default_clk @(posedge (sha256.clk)); endclocking + -bind sha256_core fv_sha_256_m fv_sha256( - .rst(sha256_core.reset_n && !sha256_core.zeroize), - .clk(sha256_core.clk), - .digest_out_0(sha256_core.digest [255:224]), - .digest_out_1(sha256_core.digest [223:192]), - .digest_out_2(sha256_core.digest [191:160]), - .digest_out_3(sha256_core.digest [159:128]), - .digest_out_4(sha256_core.digest [127:96]), - .digest_out_5(sha256_core.digest [95:64]), - .digest_out_6(sha256_core.digest [63:32]), - .digest_out_7(sha256_core.digest [31:0]), - .block_init(sha256_core.init_cmd), - .block_mode(sha256_core.mode), - .block_next(sha256_core.next_cmd), - .block_in_0(sha256_core.block_msg[31:0]), - .block_in_1(sha256_core.block_msg[63:32]), - .block_in_2(sha256_core.block_msg[95:64]), - .block_in_3(sha256_core.block_msg[127:96]), - .block_in_4(sha256_core.block_msg[159:128]), - .block_in_5(sha256_core.block_msg[191:160]), - .block_in_6(sha256_core.block_msg[223:192]), - .block_in_7(sha256_core.block_msg[255:224]), - .block_in_8(sha256_core.block_msg[287:256]), - .block_in_9(sha256_core.block_msg[319:288]), - .block_in_10(sha256_core.block_msg[351:320]), - .block_in_11(sha256_core.block_msg[383:352]), - .block_in_12(sha256_core.block_msg[415:384]), - .block_in_13(sha256_core.block_msg[447:416]), - .block_in_14(sha256_core.block_msg[479:448]), - .block_in_15(sha256_core.block_msg[511:480]), - .block_zeroize(sha256_core.zeroize), - .block_in_valid((sha256_core.init_cmd) || (sha256_core.next_cmd)), - .digest_valid(sha256_core.digest_valid), - .block_in_ready(sha256_core.ready), - .i(sha256_core.t_ctr_reg), - .W_0(sha256_core.w_mem_inst.w_mem[00]), - .W_1(sha256_core.w_mem_inst.w_mem[01]), - .W_2(sha256_core.w_mem_inst.w_mem[02]), - .W_3(sha256_core.w_mem_inst.w_mem[03]), - .W_4(sha256_core.w_mem_inst.w_mem[04]), - .W_5(sha256_core.w_mem_inst.w_mem[05]), - .W_6(sha256_core.w_mem_inst.w_mem[06]), - .W_7(sha256_core.w_mem_inst.w_mem[07]), - .W_8(sha256_core.w_mem_inst.w_mem[08]), - .W_9(sha256_core.w_mem_inst.w_mem[09]), - .W_10(sha256_core.w_mem_inst.w_mem[10]), - .W_11(sha256_core.w_mem_inst.w_mem[11]), - .W_12(sha256_core.w_mem_inst.w_mem[12]), - .W_13(sha256_core.w_mem_inst.w_mem[13]), - .W_14(sha256_core.w_mem_inst.w_mem[14]), - .W_15(sha256_core.w_mem_inst.w_mem[15]), - .H_0(sha256_core.H0_reg), - .H_1(sha256_core.H1_reg), - .H_2(sha256_core.H2_reg), - .H_3(sha256_core.H3_reg), - .H_4(sha256_core.H4_reg), - .H_5(sha256_core.H5_reg), - .H_6(sha256_core.H6_reg), - .H_7(sha256_core.H7_reg), - .a(sha256_core.a_reg), - .b(sha256_core.b_reg), - .c(sha256_core.c_reg), - .d(sha256_core.d_reg), - .e(sha256_core.e_reg), - .f(sha256_core.f_reg), - .g(sha256_core.g_reg), - .h(sha256_core.h_reg), - .idle(sha256_core.sha256_ctrl_reg==2'h0), - .ctrl_rotationss(sha256_core.sha256_ctrl_reg==2'h1), - .ctrl_done(sha256_core.sha256_ctrl_reg==2'h2) +st_Sha256CoreRequest sha_core_request_port; +assign sha_core_request_port = '{ + init_command: (sha256.core_init), + next_command: (sha256.core_next), + is_sha256_mode: (sha256.core_mode), + zeroize: (sha256.zeroize_reg), + message_block: '{ + 0: (sha256.core_block[511:480]), + 1: (sha256.core_block[479:448]), + 2: (sha256.core_block[447:416]), + 3: (sha256.core_block[415:384]), + 4: (sha256.core_block[383:352]), + 5: (sha256.core_block[351:320]), + 6: (sha256.core_block[319:288]), + 7: (sha256.core_block[287:256]), + 8: (sha256.core_block[255:224]), + 9: (sha256.core_block[223:192]), + 10: (sha256.core_block[191:160]), + 11: (sha256.core_block[159:128]), + 12: (sha256.core_block[127:96]), + 13: (sha256.core_block[95:64]), + 14: (sha256.core_block[63:32]), + 15: (sha256.core_block[31:0]) + } +}; +st_Sha256CoreResponse sha_core_response_port; +assign sha_core_response_port = '{ + digest_block: '{ + 0: (sha256.core_digest[0]), + 1: (sha256.core_digest[1]), + 2: (sha256.core_digest[2]), + 3: (sha256.core_digest[3]), + 4: (sha256.core_digest[4]), + 5: (sha256.core_digest[5]), + 6: (sha256.core_digest[6]), + 7: (sha256.core_digest[7]) + } +}; +st_Sha256CoreWinternitz192Request sha_core_winternitz192_request_port; +assign sha_core_winternitz192_request_port = '{ + init_command: (sha256.core_init), + next_command: (sha256.core_next), + is_sha256_mode: (sha256.core_mode), + zeroize: (sha256.zeroize_reg), + message_block: '{ + I: (sha256.core_block[511:384]), + q: (sha256.core_block[383:352]), + i: (sha256.core_block[351:336]), + j: (sha256.core_block[335:328]), + tmp: '{ + 0: (sha256.core_block[327:296]), + 1: (sha256.core_block[295:264]), + 2: (sha256.core_block[263:232]), + 3: (sha256.core_block[231:200]), + 4: (sha256.core_block[199:168]), + 5: (sha256.core_block[167:136]) + }, + padding: (sha256.core_block[135:0]) + } +}; +st_Sha256CoreWinternitz192Response sha_core_winternitz192_response_port; +assign sha_core_winternitz192_response_port = '{ + tmp: '{ + 0: (sha256.core_digest[0]), + 1: (sha256.core_digest[1]), + 2: (sha256.core_digest[2]), + 3: (sha256.core_digest[3]), + 4: (sha256.core_digest[4]), + 5: (sha256.core_digest[5]) + } +}; +st_Sha256CoreWinternitz256Request sha_core_winternitz256_request_port; +assign sha_core_winternitz256_request_port = '{ + init_command: (sha256.core_init), + next_command: (sha256.core_next), + is_sha256_mode: (sha256.core_mode), + zeroize: (sha256.zeroize_reg), + message_block: '{ + I: (sha256.core_block[511:384]), + q: (sha256.core_block[383:352]), + i: (sha256.core_block[351:336]), + j: (sha256.core_block[335:328]), + tmp: '{ + 0: (sha256.core_block[327:296]), + 1: (sha256.core_block[295:264]), + 2: (sha256.core_block[263:232]), + 3: (sha256.core_block[231:200]), + 4: (sha256.core_block[199:168]), + 5: (sha256.core_block[167:136]), + 6: (sha256.core_block[135:104]), + 7: (sha256.core_block[103:72]) + }, + padding: (sha256.core_block[71:0]) + } +}; +st_Sha256CoreWinternitz256Response sha_core_winternitz256_response_port; +assign sha_core_winternitz256_response_port = '{ + tmp: '{ + 0: (sha256.core_digest[0]), + 1: (sha256.core_digest[1]), + 2: (sha256.core_digest[2]), + 3: (sha256.core_digest[3]), + 4: (sha256.core_digest[4]), + 5: (sha256.core_digest[5]), + 6: (sha256.core_digest[6]), + 7: (sha256.core_digest[7]) + } +}; +st_Sha256Request sha_request_port; +assign sha_request_port = '{ + is_init: (sha256.hwif_out.SHA256_CTRL.INIT.value), + is_next: (sha256.hwif_out.SHA256_CTRL.NEXT.value), + is_sha256_mode: (sha256.hwif_out.SHA256_CTRL.MODE.value), + is_winternitz: (sha256.hwif_out.SHA256_CTRL.WNTZ_MODE.value), + winternitz_n_mode: (sha256.hwif_out.SHA256_CTRL.WNTZ_N_MODE.value), + winternitz_w: (sha256.hwif_out.SHA256_CTRL.WNTZ_W.value), + winternitz_loop_init: (sha256.hwif_out.SHA256_BLOCK[5].BLOCK.value[15:8]), + zeroize: (sha256.hwif_out.SHA256_CTRL.ZEROIZE.value || sha256.debugUnlock_or_scan_mode_switch), + message_block: '{ + 0: (sha256.hwif_out.SHA256_BLOCK[0].BLOCK.value), + 1: (sha256.hwif_out.SHA256_BLOCK[1].BLOCK.value), + 2: (sha256.hwif_out.SHA256_BLOCK[2].BLOCK.value), + 3: (sha256.hwif_out.SHA256_BLOCK[3].BLOCK.value), + 4: (sha256.hwif_out.SHA256_BLOCK[4].BLOCK.value), + 5: (sha256.hwif_out.SHA256_BLOCK[5].BLOCK.value), + 6: (sha256.hwif_out.SHA256_BLOCK[6].BLOCK.value), + 7: (sha256.hwif_out.SHA256_BLOCK[7].BLOCK.value), + 8: (sha256.hwif_out.SHA256_BLOCK[8].BLOCK.value), + 9: (sha256.hwif_out.SHA256_BLOCK[9].BLOCK.value), + 10: (sha256.hwif_out.SHA256_BLOCK[10].BLOCK.value), + 11: (sha256.hwif_out.SHA256_BLOCK[11].BLOCK.value), + 12: (sha256.hwif_out.SHA256_BLOCK[12].BLOCK.value), + 13: (sha256.hwif_out.SHA256_BLOCK[13].BLOCK.value), + 14: (sha256.hwif_out.SHA256_BLOCK[14].BLOCK.value), + 15: (sha256.hwif_out.SHA256_BLOCK[15].BLOCK.value) + } +}; +st_Sha256Response sha_response_port; +assign sha_response_port = '{ + digest_block: '{ + 0: (sha256.hwif_in.SHA256_DIGEST[0].DIGEST.next), + 1: (sha256.hwif_in.SHA256_DIGEST[1].DIGEST.next), + 2: (sha256.hwif_in.SHA256_DIGEST[2].DIGEST.next), + 3: (sha256.hwif_in.SHA256_DIGEST[3].DIGEST.next), + 4: (sha256.hwif_in.SHA256_DIGEST[4].DIGEST.next), + 5: (sha256.hwif_in.SHA256_DIGEST[5].DIGEST.next), + 6: (sha256.hwif_in.SHA256_DIGEST[6].DIGEST.next), + 7: (sha256.hwif_in.SHA256_DIGEST[7].DIGEST.next) + } +}; +st_Sha256Request sha_shared_request_port; +assign sha_shared_request_port = '{ + is_init: (sha256.hwif_out.SHA256_CTRL.INIT.value), + is_next: (sha256.hwif_out.SHA256_CTRL.NEXT.value), + is_sha256_mode: (sha256.hwif_out.SHA256_CTRL.MODE.value), + is_winternitz: (sha256.hwif_out.SHA256_CTRL.WNTZ_MODE.value), + winternitz_n_mode: (sha256.hwif_out.SHA256_CTRL.WNTZ_N_MODE.value), + winternitz_w: (sha256.hwif_out.SHA256_CTRL.WNTZ_W.value), + winternitz_loop_init: (sha256.hwif_out.SHA256_BLOCK[5].BLOCK.value[15:8]), + zeroize: (sha256.hwif_out.SHA256_CTRL.ZEROIZE.value || sha256.debugUnlock_or_scan_mode_switch), + message_block: '{ + 0: (sha256.hwif_out.SHA256_BLOCK[0].BLOCK.value), + 1: (sha256.hwif_out.SHA256_BLOCK[1].BLOCK.value), + 2: (sha256.hwif_out.SHA256_BLOCK[2].BLOCK.value), + 3: (sha256.hwif_out.SHA256_BLOCK[3].BLOCK.value), + 4: (sha256.hwif_out.SHA256_BLOCK[4].BLOCK.value), + 5: (sha256.hwif_out.SHA256_BLOCK[5].BLOCK.value), + 6: (sha256.hwif_out.SHA256_BLOCK[6].BLOCK.value), + 7: (sha256.hwif_out.SHA256_BLOCK[7].BLOCK.value), + 8: (sha256.hwif_out.SHA256_BLOCK[8].BLOCK.value), + 9: (sha256.hwif_out.SHA256_BLOCK[9].BLOCK.value), + 10: (sha256.hwif_out.SHA256_BLOCK[10].BLOCK.value), + 11: (sha256.hwif_out.SHA256_BLOCK[11].BLOCK.value), + 12: (sha256.hwif_out.SHA256_BLOCK[12].BLOCK.value), + 13: (sha256.hwif_out.SHA256_BLOCK[13].BLOCK.value), + 14: (sha256.hwif_out.SHA256_BLOCK[14].BLOCK.value), + 15: (sha256.hwif_out.SHA256_BLOCK[15].BLOCK.value) + } +}; +st_Sha256Request sha_request; +assign sha_request = '{ + is_init: (sha256.init_reg), + is_next: (sha256.next_reg), + is_sha256_mode: (sha256.mode_reg), + is_winternitz: (sha256.wntz_mode), + winternitz_n_mode: (sha256.wntz_n_mode), + winternitz_w: (sha256.wntz_w_reg), + winternitz_loop_init: (sha256.wntz_iter), + zeroize: (sha256.zeroize_reg), + message_block: '{ + 0: (sha256.block_reg[0]), + 1: (sha256.block_reg[1]), + 2: (sha256.block_reg[2]), + 3: (sha256.block_reg[3]), + 4: (sha256.block_reg[4]), + 5: (sha256.block_reg[5]), + 6: (sha256.block_reg[6]), + 7: (sha256.block_reg[7]), + 8: (sha256.block_reg[8]), + 9: (sha256.block_reg[9]), + 10: (sha256.block_reg[10]), + 11: (sha256.block_reg[11]), + 12: (sha256.block_reg[12]), + 13: (sha256.block_reg[13]), + 14: (sha256.block_reg[14]), + 15: (sha256.block_reg[15]) + } +}; + +// Symbolic digest element +logic [$clog2(8)-1 : 0] digest_position; +assume_stable_digest_position: assume property(##1 $stable(digest_position)); + +// Symbolic block element +logic [$clog2(sha256.BLOCK_NO)-1 : 0] block_position; +assume_stable_block_position: assume property(##1 $stable(block_position)); + +fv_sha256 fv_sha256_i ( + .reset_n(sha256.reset_n && sha256.cptra_pwrgood && !$past(sha256.zeroize_reg)), + .top_reset_n(sha256.reset_n), + .clk(sha256.clk), + + // Ports + .sha_core_response_port_vld(sha256.core_digest_valid), + .sha_core_response_port_rdy(1'b1), + .sha_core_response_port(sha_core_response_port), + + .sha_core_winternitz192_response_port_vld(sha256.core_digest_valid && !sha256.core_init && !sha256.core_next), + .sha_core_winternitz192_response_port_rdy(1'b1), + .sha_core_winternitz192_response_port(sha_core_winternitz192_response_port), + + .sha_core_winternitz256_response_port_vld(sha256.core_digest_valid && !sha256.core_init && !sha256.core_next), + .sha_core_winternitz256_response_port_rdy(1'b1), + .sha_core_winternitz256_response_port(sha_core_winternitz256_response_port), + + .sha_request_port_vld(sha256.hwif_out.SHA256_CTRL.INIT.value || sha256.hwif_out.SHA256_CTRL.NEXT.value), + .sha_request_port_rdy($past(!sha256.reset_n) ? !sha256.hwif_in.SHA256_STATUS.READY.next : sha256.hwif_in.SHA256_STATUS.READY.next), + .sha_request_port(sha_request_port), + + .sha_shared_request_port(sha_shared_request_port), + + .sha_core_request_port_vld(sha256.core_init), + .sha_core_request_port(sha_core_request_port), + + .sha_core_winternitz192_request_port_vld(sha256.core_init), + .sha_core_winternitz192_request_port(sha_core_winternitz192_request_port), + + .sha_core_winternitz256_request_port_vld(sha256.core_init), + .sha_core_winternitz256_request_port(sha_core_winternitz256_request_port), + + .sha_response_port_vld(sha256.hwif_in.SHA256_STATUS.VALID.next), + .sha_response_port(sha_response_port), + + // Registers + .loop_boundary(sha256.wntz_iter_reg), + .loop_counter(sha256.wntz_j_reg), + .sha_request(sha_request), + .winternitz_I(sha256.wntz_prefix[175:48]), + .winternitz_i(sha256.wntz_prefix[15:0]), + .winternitz_q(sha256.wntz_prefix[47:16]), + + // States + .idle($past(sha256.core_ready) && sha256.core_ready && sha256.wntz_fsm == WNTZ_IDLE), + .lms_1st_256(sha256.wntz_fsm == WNTZ_1ST && sha256.wntz_n_mode_reg), + .lms_others_256(sha256.wntz_fsm == WNTZ_OTHERS && sha256.wntz_n_mode_reg), + .lms_1st_192(sha256.wntz_fsm == WNTZ_1ST && !sha256.wntz_n_mode_reg), + .lms_others_192(sha256.wntz_fsm == WNTZ_OTHERS && !sha256.wntz_n_mode_reg), + .sha(((sha256.core_init || sha256.core_next) && sha256.wntz_fsm_next == WNTZ_IDLE)), + + // Manually added signals for manually added assertions + .hwif_in_register_error_reset (sha256.hwif_in.error_reset_b), + .hwif_in_winternitz_error (sha256.hwif_in.intr_block_rf.error_internal_intr_r.error0_sts.hwset), + .hwif_in_sha_operation_error (sha256.hwif_in.intr_block_rf.error_internal_intr_r.error1_sts.hwset), + .hwif_in_error2 (sha256.hwif_in.intr_block_rf.error_internal_intr_r.error2_sts.hwset), + .hwif_in_error3 (sha256.hwif_in.intr_block_rf.error_internal_intr_r.error3_sts.hwset), + .hwif_in_command_done (sha256.hwif_in.intr_block_rf.notif_internal_intr_r.notif_cmd_done_sts.hwset), + .hwif_in_name0 (sha256.hwif_in.SHA256_NAME[0].NAME.next), + .hwif_in_name1 (sha256.hwif_in.SHA256_NAME[1].NAME.next), + .hwif_in_version0 (sha256.hwif_in.SHA256_VERSION[0].VERSION.next), + .hwif_in_version1 (sha256.hwif_in.SHA256_VERSION[1].VERSION.next), + .hwif_in_valid (sha256.hwif_in.SHA256_STATUS.READY.next), + .hwif_in_ready (sha256.hwif_in.SHA256_STATUS.VALID.next), + .hwif_in_wntz_busy (sha256.hwif_in.SHA256_STATUS.WNTZ_BUSY.next), + .hwif_in_digest_clear (sha256.hwif_in.SHA256_DIGEST[digest_position].DIGEST.hwclr), + .hwif_in_block_clear (sha256.hwif_in.SHA256_BLOCK[block_position].BLOCK.hwclr), + .hwif_in_control_zeroize (sha256.hwif_out.SHA256_CTRL.ZEROIZE.value), + .hwif_in_register_error_interrupt (sha256.hwif_out.intr_block_rf.error_global_intr_r.intr), + .hwif_in_register_notification_interrupt (sha256.hwif_out.intr_block_rf.notif_global_intr_r.intr), + .error_interrupt (sha256.error_intr), + .notification_interrupt (sha256.notif_intr), + .error (sha256.err), + .powergood (sha256.cptra_pwrgood), + .register_read_error (sha256.read_error), + .register_write_error (sha256.write_error), + .valid_register (sha256.ready_reg), + .ready_register (sha256.digest_valid_reg), + .wntz_fsm_next (sha256.wntz_fsm_next), + .wntz_fsm (sha256.wntz_fsm), + .wntz_busy_register (sha256.wntz_busy), + .core_init (sha256.core_init), + .core_next (sha256.core_next), + .core_digest_valid (sha256.core_digest_valid), + .debug_scan_switch (sha256.debugUnlock_or_scan_mode_switch), + .ready_flag_register (sha256.ready_flag_reg), + .digest_register (sha256.digest_reg), + .valid_flag_register (sha256.valid_flag_reg), + .zeroize_register (sha256.zeroize_reg) ); +endmodule + +bind sha256 fv_sha256_ref_wrapper fv_sha256_ref_wrapper_i(); diff --git a/src/sha256/formal/properties/fv_sha256_constraints.sv b/src/sha256/formal/properties/fv_sha256_constraints.sv new file mode 100644 index 000000000..5220dc554 --- /dev/null +++ b/src/sha256/formal/properties/fv_sha256_constraints.sv @@ -0,0 +1,96 @@ + +// ------------------------------------------------- +// 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_main + import sha256_reg_pkg::*; +#( + parameter ADDR_WIDTH = 32, + parameter DATA_WIDTH = 32 +)( + input wire clk, + input wire reset_n, + input wire cptra_pwrgood, + input wire cs, + input wire we, + input wire [ADDR_WIDTH-1 : 0] address, + input wire [DATA_WIDTH-1 : 0] write_data, + input logic debugUnlock_or_scan_mode_switch, + + // Design internal signals + input logic core_init, + input logic core_next, + input logic core_ready, + input logic winternitz_mode +); + + default clocking default_clk @(posedge clk); endclocking + + // Compute if there is an ongoing init computation + logic init_reg; + always @ (posedge clk or negedge reset_n) begin + if (!reset_n) + init_reg <= 1'b0; + else if (core_init && core_ready) + init_reg <= 1'b1; + else if (core_next && core_ready) + init_reg <= 1'b0; + end + + // There should not be a next command before an init command + assume_init_before_next: assume property( + !init_reg + |-> + !core_next + ); + + // When a winternitz computation is ongoing, then no core_next is allowed + assume_no_next_for_winternitz: assume property( + winternitz_mode + |-> + !core_next + ); + + // Since we cut the core digest signal we need to ensure that the output + // of the core is stable + assume_stable_digest_when_valid: assume property( + ##1 sha256.core_digest_valid + |-> + $stable(sha256.core_digest) + ); + +endmodule + +bind sha256 fv_constraints_main #( + .ADDR_WIDTH(ADDR_WIDTH), + .DATA_WIDTH(DATA_WIDTH) +) fv_constraints_i ( + .clk(clk), + .reset_n(reset_n), + .cptra_pwrgood(cptra_pwrgood), + .cs(cs), + .we(we), + .address(address), + .write_data(write_data), + .debugUnlock_or_scan_mode_switch(debugUnlock_or_scan_mode_switch), + .core_init(sha256.core_init), + .core_next(sha256.core_next), + .core_ready(sha256.core_ready), + .winternitz_mode(sha256.wntz_mode) +); diff --git a/src/sha256/formal/properties/fv_sha256_core.sv b/src/sha256/formal/properties/fv_sha256_core.sv new file mode 100644 index 000000000..3272fa58d --- /dev/null +++ b/src/sha256/formal/properties/fv_sha256_core.sv @@ -0,0 +1,597 @@ +// ------------------------------------------------- +// 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 fv_sha256_core_pkg::*; + +module fv_sha_256_core_m( + input bit rst, + input bit clk, + input bit unsigned [31:0] digest_out_0, + input bit unsigned [31:0] digest_out_1, + input bit unsigned [31:0] digest_out_2, + input bit unsigned [31:0] digest_out_3, + input bit unsigned [31:0] digest_out_4, + input bit unsigned [31:0] digest_out_5, + input bit unsigned [31:0] digest_out_6, + input bit unsigned [31:0] digest_out_7, + input bit block_init, + input bit block_mode, + input bit block_next, + input bit unsigned [31:0] block_in_0, + input bit unsigned [31:0] block_in_1, + input bit unsigned [31:0] block_in_2, + input bit unsigned [31:0] block_in_3, + input bit unsigned [31:0] block_in_4, + input bit unsigned [31:0] block_in_5, + input bit unsigned [31:0] block_in_6, + input bit unsigned [31:0] block_in_7, + input bit unsigned [31:0] block_in_8, + input bit unsigned [31:0] block_in_9, + input bit unsigned [31:0] block_in_10, + input bit unsigned [31:0] block_in_11, + input bit unsigned [31:0] block_in_12, + input bit unsigned [31:0] block_in_13, + input bit unsigned [31:0] block_in_14, + input bit unsigned [31:0] block_in_15, + input bit block_zeroize, + input bit block_in_valid, + input bit digest_valid, + input bit block_in_ready, + input bit unsigned [5:0] i, + input bit unsigned [31:0] W_0, + input bit unsigned [31:0] W_1, + input bit unsigned [31:0] W_2, + input bit unsigned [31:0] W_3, + input bit unsigned [31:0] W_4, + input bit unsigned [31:0] W_5, + input bit unsigned [31:0] W_6, + input bit unsigned [31:0] W_7, + input bit unsigned [31:0] W_8, + input bit unsigned [31:0] W_9, + input bit unsigned [31:0] W_10, + input bit unsigned [31:0] W_11, + input bit unsigned [31:0] W_12, + input bit unsigned [31:0] W_13, + input bit unsigned [31:0] W_14, + input bit unsigned [31:0] W_15, + input bit unsigned [31:0] H_0, + input bit unsigned [31:0] H_1, + input bit unsigned [31:0] H_2, + input bit unsigned [31:0] H_3, + input bit unsigned [31:0] H_4, + input bit unsigned [31:0] H_5, + input bit unsigned [31:0] H_6, + input bit unsigned [31:0] H_7, + input bit unsigned [31:0] a, + input bit unsigned [31:0] b, + input bit unsigned [31:0] c, + input bit unsigned [31:0] d, + input bit unsigned [31:0] e, + input bit unsigned [31:0] f, + input bit unsigned [31:0] g, + input bit unsigned [31:0] h, + input bit idle, + input bit ctrl_rotationss, + input bit ctrl_done +); + + +default clocking default_clk @(posedge clk); endclocking +logic [15:0][31:0] w; +logic [3:0] j; + +assign j = i[3:0]; +assign w = {W_15,W_14,W_13,W_12,W_11,W_10,W_9,W_8,W_7,W_6,W_5,W_4,W_3,W_2,W_1,W_0}; + +sequence reset_sequence; + !rst ##1 rst; +endsequence + + +reset_a: assert property (reset_p); +property reset_p; + reset_sequence |-> + idle && + i == 'sd0 && + W_0 == 0 && + W_10 == 0 && + W_11 == 0 && + W_12 == 0 && + W_13 == 0 && + W_14 == 0 && + W_15 == 0 && + W_1 == 0 && + W_2 == 0 && + W_3 == 0 && + W_4 == 0 && + W_5 == 0 && + W_6 == 0 && + W_7 == 0 && + W_8 == 0 && + W_9 == 0 && + H_0 == 0 && + H_1 == 0 && + H_2 == 0 && + H_3 == 0 && + H_4 == 0 && + H_5 == 0 && + H_6 == 0 && + H_7 == 0 && + a == 0 && + b == 0 && + c == 0 && + d == 0 && + e == 0 && + f == 0 && + g == 0 && + h == 0 && + digest_valid == 0 && + block_in_ready == 1; +endproperty + + +DONE_to_IDLE_a: assert property (disable iff(!rst) DONE_to_IDLE_p); +property DONE_to_IDLE_p; + ctrl_done +|-> + ##1 + idle && + digest_out_0 == ($past(a, 1) + $past(H_0, 1)) && + digest_out_1 == ($past(b, 1) + $past(H_1, 1)) && + digest_out_2 == ($past(c, 1) + $past(H_2, 1)) && + digest_out_3 == ($past(d, 1) + $past(H_3, 1)) && + digest_out_4 == ($past(e, 1) + $past(H_4, 1)) && + digest_out_5 == ($past(f, 1) + $past(H_5, 1)) && + digest_out_6 == ($past(g, 1) + $past(H_6, 1)) && + digest_out_7 == ($past(h, 1) + $past(H_7, 1)) && + i == $past(i, 1) && + W_0 == $past(W_0, 1) && + W_10 == $past(W_10, 1) && + W_11 == $past(W_11, 1) && + W_12 == $past(W_12, 1) && + W_13 == $past(W_13, 1) && + W_14 == $past(W_14, 1) && + W_15 == $past(W_15, 1) && + W_1 == $past(W_1, 1) && + W_2 == $past(W_2, 1) && + W_3 == $past(W_3, 1) && + W_4 == $past(W_4, 1) && + W_5 == $past(W_5, 1) && + W_6 == $past(W_6, 1) && + W_7 == $past(W_7, 1) && + W_8 == $past(W_8, 1) && + W_9 == $past(W_9, 1) && + H_0 == ($past(a, 1) + $past(H_0, 1)) && + H_1 == ($past(b, 1) + $past(H_1, 1)) && + H_2 == ($past(c, 1) + $past(H_2, 1)) && + H_3 == ($past(d, 1) + $past(H_3, 1)) && + H_4 == ($past(e, 1) + $past(H_4, 1)) && + H_5 == ($past(f, 1) + $past(H_5, 1)) && + H_6 == ($past(g, 1) + $past(H_6, 1)) && + H_7 == ($past(h, 1) + $past(H_7, 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) && + digest_valid == 1 && + block_in_ready == 1; +endproperty + + +SHA_Rounds_to_DONE_a: assert property (disable iff(!rst) SHA_Rounds_to_DONE_p); +property SHA_Rounds_to_DONE_p; + ctrl_rotationss && + (i >= 'sd16) && + (('sd1 + i) >= 'sd64) +|-> + ##1 (digest_valid == 0) and + ##1 (block_in_ready == 0) and + ##1 + ctrl_done && + i == 'sd0 && + W_0 == $past(W_1, 1) && + W_10 == $past(W_11, 1) && + W_11 == $past(W_12, 1) && + W_12 == $past(W_13, 1) && + W_13 == $past(W_14, 1) && + W_14 == $past(W_15, 1) && + W_15 == $past(compute_w(W_14,W_9,W_1,W_0)) && + W_1 == $past(W_2, 1) && + W_2 == $past(W_3, 1) && + W_3 == $past(W_4, 1) && + W_4 == $past(W_5, 1) && + W_5 == $past(W_6, 1) && + W_6 == $past(W_7, 1) && + W_7 == $past(W_8, 1) && + W_8 == $past(W_9, 1) && + W_9 == $past(W_10, 1) && + H_0 == $past(H_0, 1) && + H_1 == $past(H_1, 1) && + H_2 == $past(H_2, 1) && + H_3 == $past(H_3, 1) && + H_4 == $past(H_4, 1) && + H_5 == $past(H_5, 1) && + H_6 == $past(H_6, 1) && + H_7 == $past(H_7, 1) && + a == $past(newa(mult_xor(a, 2, 13, 22),majority(a,b,c),Summ(compute_w(W_14,W_9,W_1,W_0),K[i],h,choose(e,f,g),mult_xor(e, 6, 11, 25)))) && + b == $past(a, 1) && + c == $past(b, 1) && + d == $past(c, 1) && + e == $past(newe(d,Summ(compute_w(W_14,W_9,W_1,W_0),K[i],h,choose(e,f,g),mult_xor(e,6,11,25)))) && + f == $past(e, 1) && + g == $past(f, 1) && + h == $past(g, 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; + ctrl_rotationss && + (i < 'sd16) +|-> + ##1 (digest_valid == 0) and + ##1 (block_in_ready == 0) and + ##1 + ctrl_rotationss && + i == ('sd1 + $past(i, 1)) && + W_0 == $past(W_0, 1) && + W_10 == $past(W_10, 1) && + W_11 == $past(W_11, 1) && + W_12 == $past(W_12, 1) && + W_13 == $past(W_13, 1) && + W_14 == $past(W_14, 1) && + W_15 == $past(W_15, 1) && + W_1 == $past(W_1, 1) && + W_2 == $past(W_2, 1) && + W_3 == $past(W_3, 1) && + W_4 == $past(W_4, 1) && + W_5 == $past(W_5, 1) && + W_6 == $past(W_6, 1) && + W_7 == $past(W_7, 1) && + W_8 == $past(W_8, 1) && + W_9 == $past(W_9, 1) && + H_0 == $past(H_0, 1) && + H_1 == $past(H_1, 1) && + H_2 == $past(H_2, 1) && + H_3 == $past(H_3, 1) && + H_4 == $past(H_4, 1) && + H_5 == $past(H_5, 1) && + H_6 == $past(H_6, 1) && + H_7 == $past(H_7, 1) && + a == $past(newa(mult_xor(a, 2, 13, 22),majority(a,b,c),Summ(w[j],K[i],h,choose(e,f,g),mult_xor(e, 6, 11, 25)))) && + b == $past(a, 1) && + c == $past(b, 1) && + d == $past(c, 1) && + e == $past(newe(d,Summ(w[j],K[i],h,choose(e,f,g),mult_xor(e,6,11,25)))) && + f == $past(e, 1) && + g == $past(f, 1) && + h == $past(g, 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; + ctrl_rotationss && + (i >= 'sd16) && + (('sd1 + i) < 'sd64) +|-> + ##1 (digest_valid == 0) and + ##1 (block_in_ready == 0) and + ##1 + ctrl_rotationss && + i == ('sd1 + $past(i, 1)) && + W_0 == $past(W_1, 1) && + W_10 == $past(W_11, 1) && + W_11 == $past(W_12, 1) && + W_12 == $past(W_13, 1) && + W_13 == $past(W_14, 1) && + W_14 == $past(W_15, 1) && + W_15 == $past(compute_w(W_14,W_9,W_1,W_0)) && + W_1 == $past(W_2, 1) && + W_2 == $past(W_3, 1) && + W_3 == $past(W_4, 1) && + W_4 == $past(W_5, 1) && + W_5 == $past(W_6, 1) && + W_6 == $past(W_7, 1) && + W_7 == $past(W_8, 1) && + W_8 == $past(W_9, 1) && + W_9 == $past(W_10, 1) && + H_0 == $past(H_0, 1) && + H_1 == $past(H_1, 1) && + H_2 == $past(H_2, 1) && + H_3 == $past(H_3, 1) && + H_4 == $past(H_4, 1) && + H_5 == $past(H_5, 1) && + H_6 == $past(H_6, 1) && + H_7 == $past(H_7, 1) && + a == $past(newa(mult_xor(a, 2, 13, 22),majority(a,b,c),Summ(compute_w(W_14,W_9,W_1,W_0),K[i],h,choose(e,f,g),mult_xor(e, 6, 11, 25)))) && + b == $past(a, 1) && + c == $past(b, 1) && + d == $past(c, 1) && + e == $past(newe(d,Summ(compute_w(W_14,W_9,W_1,W_0),K[i],h,choose(e,f,g),mult_xor(e,6,11,25)))) && + f == $past(e, 1) && + g == $past(f, 1) && + h == $past(g, 1); +endproperty + + +IDLE_to_SHA_Rounds_224_a: assert property (disable iff(!rst) IDLE_to_SHA_Rounds_224_p); +property IDLE_to_SHA_Rounds_224_p; + idle && + block_in_valid && + block_init && + !block_mode +|-> + ##1 (digest_valid == 0) and + ##1 (block_in_ready == 0) and + ##1 + ctrl_rotationss && + i == 'sd0 && + W_0 == $past(block_in_15, 1) && + W_10 == $past(block_in_5, 1) && + W_11 == $past(block_in_4, 1) && + W_12 == $past(block_in_3, 1) && + W_13 == $past(block_in_2, 1) && + W_14 == $past(block_in_1, 1) && + W_15 == $past(block_in_0, 1) && + W_1 == $past(block_in_14, 1) && + W_2 == $past(block_in_13, 1) && + W_3 == $past(block_in_12, 1) && + W_4 == $past(block_in_11, 1) && + W_5 == $past(block_in_10, 1) && + W_6 == $past(block_in_9, 1) && + W_7 == $past(block_in_8, 1) && + W_8 == $past(block_in_7, 1) && + W_9 == $past(block_in_6, 1) && + H_0 == 32'd3238371032 && + H_1 == 32'd914150663 && + H_2 == 32'd812702999 && + H_3 == 32'd4144912697 && + H_4 == 32'd4290775857 && + H_5 == 32'd1750603025 && + H_6 == 32'd1694076839 && + H_7 == 32'd3204075428 && + a == 32'd3238371032 && + b == 32'd914150663 && + c == 32'd812702999 && + d == 32'd4144912697 && + e == 32'd4290775857 && + f == 32'd1750603025 && + g == 32'd1694076839 && + h == 32'd3204075428; +endproperty + + +IDLE_to_SHA_Rounds_256_a: assert property (disable iff(!rst) IDLE_to_SHA_Rounds_256_p); +property IDLE_to_SHA_Rounds_256_p; + idle && + block_in_valid && + block_init && + block_mode +|-> + ##1 (digest_valid == 0) and + ##1 (block_in_ready == 0) and + ##1 + ctrl_rotationss && + i == 'sd0 && + W_0 == $past(block_in_15, 1) && + W_10 == $past(block_in_5, 1) && + W_11 == $past(block_in_4, 1) && + W_12 == $past(block_in_3, 1) && + W_13 == $past(block_in_2, 1) && + W_14 == $past(block_in_1, 1) && + W_15 == $past(block_in_0, 1) && + W_1 == $past(block_in_14, 1) && + W_2 == $past(block_in_13, 1) && + W_3 == $past(block_in_12, 1) && + W_4 == $past(block_in_11, 1) && + W_5 == $past(block_in_10, 1) && + W_6 == $past(block_in_9, 1) && + W_7 == $past(block_in_8, 1) && + W_8 == $past(block_in_7, 1) && + W_9 == $past(block_in_6, 1) && + H_0 == 32'd1779033703 && + H_1 == 32'd3144134277 && + H_2 == 32'd1013904242 && + H_3 == 32'd2773480762 && + H_4 == 32'd1359893119 && + H_5 == 32'd2600822924 && + H_6 == 32'd528734635 && + H_7 == 32'd1541459225 && + a == 32'd1779033703 && + b == 32'd3144134277 && + c == 32'd1013904242 && + d == 32'd2773480762 && + e == 32'd1359893119 && + f == 32'd2600822924 && + g == 32'd528734635 && + h == 32'd1541459225; +endproperty + + +IDLE_to_SHA_Rounds_next_a: assert property (disable iff(!rst) IDLE_to_SHA_Rounds_next_p); +property IDLE_to_SHA_Rounds_next_p; + idle && + block_in_valid && + !block_init +|-> + ##1 (digest_valid == 0) and + ##1 (block_in_ready == 0) and + ##1 + ctrl_rotationss && + i == 'sd0 && + W_0 == $past(block_in_15, 1) && + W_10 == $past(block_in_5, 1) && + W_11 == $past(block_in_4, 1) && + W_12 == $past(block_in_3, 1) && + W_13 == $past(block_in_2, 1) && + W_14 == $past(block_in_1, 1) && + W_15 == $past(block_in_0, 1) && + W_1 == $past(block_in_14, 1) && + W_2 == $past(block_in_13, 1) && + W_3 == $past(block_in_12, 1) && + W_4 == $past(block_in_11, 1) && + W_5 == $past(block_in_10, 1) && + W_6 == $past(block_in_9, 1) && + W_7 == $past(block_in_8, 1) && + W_8 == $past(block_in_7, 1) && + W_9 == $past(block_in_6, 1) && + H_0 == $past(H_0, 1) && + H_1 == $past(H_1, 1) && + H_2 == $past(H_2, 1) && + H_3 == $past(H_3, 1) && + H_4 == $past(H_4, 1) && + H_5 == $past(H_5, 1) && + H_6 == $past(H_6, 1) && + H_7 == $past(H_7, 1) && + a == $past(H_0, 1) && + b == $past(H_1, 1) && + c == $past(H_2, 1) && + d == $past(H_3, 1) && + e == $past(H_4, 1) && + f == $past(H_5, 1) && + g == $past(H_6, 1) && + h == $past(H_7, 1); +endproperty + + +idle_wait_a: assert property (disable iff(!rst) idle_wait_p); +property idle_wait_p; + idle && + !block_in_valid +|-> + ##1 + idle && + i == $past(i, 1) && + W_0 == $past(W_0, 1) && + W_10 == $past(W_10, 1) && + W_11 == $past(W_11, 1) && + W_12 == $past(W_12, 1) && + W_13 == $past(W_13, 1) && + W_14 == $past(W_14, 1) && + W_15 == $past(W_15, 1) && + W_1 == $past(W_1, 1) && + W_2 == $past(W_2, 1) && + W_3 == $past(W_3, 1) && + W_4 == $past(W_4, 1) && + W_5 == $past(W_5, 1) && + W_6 == $past(W_6, 1) && + W_7 == $past(W_7, 1) && + W_8 == $past(W_8, 1) && + W_9 == $past(W_9, 1) && + H_0 == $past(H_0, 1) && + H_1 == $past(H_1, 1) && + H_2 == $past(H_2, 1) && + H_3 == $past(H_3, 1) && + H_4 == $past(H_4, 1) && + H_5 == $past(H_5, 1) && + H_6 == $past(H_6, 1) && + H_7 == $past(H_7, 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) && + digest_valid == $past(digest_valid) && + block_in_ready == 1; +endproperty + + +endmodule + + + +bind sha256_core fv_sha_256_core_m fv_sha256_core( + .rst(sha256_core.reset_n && !sha256_core.zeroize), + .clk(sha256_core.clk), + .digest_out_0(sha256_core.digest [255:224]), + .digest_out_1(sha256_core.digest [223:192]), + .digest_out_2(sha256_core.digest [191:160]), + .digest_out_3(sha256_core.digest [159:128]), + .digest_out_4(sha256_core.digest [127:96]), + .digest_out_5(sha256_core.digest [95:64]), + .digest_out_6(sha256_core.digest [63:32]), + .digest_out_7(sha256_core.digest [31:0]), + .block_init(sha256_core.init_cmd), + .block_mode(sha256_core.mode), + .block_next(sha256_core.next_cmd), + .block_in_0(sha256_core.block_msg[31:0]), + .block_in_1(sha256_core.block_msg[63:32]), + .block_in_2(sha256_core.block_msg[95:64]), + .block_in_3(sha256_core.block_msg[127:96]), + .block_in_4(sha256_core.block_msg[159:128]), + .block_in_5(sha256_core.block_msg[191:160]), + .block_in_6(sha256_core.block_msg[223:192]), + .block_in_7(sha256_core.block_msg[255:224]), + .block_in_8(sha256_core.block_msg[287:256]), + .block_in_9(sha256_core.block_msg[319:288]), + .block_in_10(sha256_core.block_msg[351:320]), + .block_in_11(sha256_core.block_msg[383:352]), + .block_in_12(sha256_core.block_msg[415:384]), + .block_in_13(sha256_core.block_msg[447:416]), + .block_in_14(sha256_core.block_msg[479:448]), + .block_in_15(sha256_core.block_msg[511:480]), + .block_zeroize(sha256_core.zeroize), + .block_in_valid((sha256_core.init_cmd) || (sha256_core.next_cmd)), + .digest_valid(sha256_core.digest_valid), + .block_in_ready(sha256_core.ready), + .i(sha256_core.t_ctr_reg), + .W_0(sha256_core.w_mem_inst.w_mem[00]), + .W_1(sha256_core.w_mem_inst.w_mem[01]), + .W_2(sha256_core.w_mem_inst.w_mem[02]), + .W_3(sha256_core.w_mem_inst.w_mem[03]), + .W_4(sha256_core.w_mem_inst.w_mem[04]), + .W_5(sha256_core.w_mem_inst.w_mem[05]), + .W_6(sha256_core.w_mem_inst.w_mem[06]), + .W_7(sha256_core.w_mem_inst.w_mem[07]), + .W_8(sha256_core.w_mem_inst.w_mem[08]), + .W_9(sha256_core.w_mem_inst.w_mem[09]), + .W_10(sha256_core.w_mem_inst.w_mem[10]), + .W_11(sha256_core.w_mem_inst.w_mem[11]), + .W_12(sha256_core.w_mem_inst.w_mem[12]), + .W_13(sha256_core.w_mem_inst.w_mem[13]), + .W_14(sha256_core.w_mem_inst.w_mem[14]), + .W_15(sha256_core.w_mem_inst.w_mem[15]), + .H_0(sha256_core.H0_reg), + .H_1(sha256_core.H1_reg), + .H_2(sha256_core.H2_reg), + .H_3(sha256_core.H3_reg), + .H_4(sha256_core.H4_reg), + .H_5(sha256_core.H5_reg), + .H_6(sha256_core.H6_reg), + .H_7(sha256_core.H7_reg), + .a(sha256_core.a_reg), + .b(sha256_core.b_reg), + .c(sha256_core.c_reg), + .d(sha256_core.d_reg), + .e(sha256_core.e_reg), + .f(sha256_core.f_reg), + .g(sha256_core.g_reg), + .h(sha256_core.h_reg), + .idle(sha256_core.sha256_ctrl_reg==2'h0), + .ctrl_rotationss(sha256_core.sha256_ctrl_reg==2'h1), + .ctrl_done(sha256_core.sha256_ctrl_reg==2'h2) +); diff --git a/src/sha256/formal/properties/fv_sha256_core_constraints.sv b/src/sha256/formal/properties/fv_sha256_core_constraints.sv new file mode 100644 index 000000000..1ae9c005a --- /dev/null +++ b/src/sha256/formal/properties/fv_sha256_core_constraints.sv @@ -0,0 +1,53 @@ +// ------------------------------------------------- +// 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_sha256_core_constraints(init, next, reset_n, clk, mode); + input bit init, next, reset_n, clk, mode; + reg init_reg; + + default clocking default_clk @(posedge clk); endclocking + remove_int_next_together_a: assume property (remove_int_next_together); + property remove_int_next_together; + !(init && next); + endproperty + + int_next_order_a: assume property (int_next_order); + property int_next_order; + !init_reg |-> !next; + endproperty + + + + always @ (posedge clk or negedge reset_n) + begin : init_reg_order + if (!reset_n) + init_reg <= 1'b0; + else if (init) + init_reg <= 1'b1; + end + +endmodule + +bind sha256_core fv_sha256_core_constraints fv_sha256_core_constraints_i( + .init(init_cmd), + .next(next_cmd), + .reset_n(reset_n), + .clk(clk), + .mode(mode) +); diff --git a/src/sha256/formal/properties/fv_sha256_core_coverpoints.sv b/src/sha256/formal/properties/fv_sha256_core_coverpoints.sv new file mode 100644 index 000000000..82b214809 --- /dev/null +++ b/src/sha256/formal/properties/fv_sha256_core_coverpoints.sv @@ -0,0 +1,48 @@ +// ------------------------------------------------- +// 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_sha256_core_coverpoints_m( + input logic clk, + input logic reset_n +); + + 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) sha256_core.zeroize ); + cover_zeroize_after_next: cover property(disable iff(!reset_n) sha256_core.zeroize && sha256_core.next_cmd ); + + //Cover modes: + //Cover all 4 different modes for SHA512 + cover_mode_224: cover property(disable iff(!reset_n) sha256_core.mode == 0 && sha256_core.init_cmd ); + cover_mode_256: cover property(disable iff(!reset_n) sha256_core.mode == 1 && sha256_core.init_cmd ); + + + //Cover: i>16 + cover_rnd_cnt_bigger_16: cover property(disable iff(!reset_n) sha256_core.t_ctr_reg == 17 ##1 sha256_core.t_ctr_reg == 17[->1] ); + + + + +endmodule +bind sha256_core fv_sha256_core_coverpoints_m fv_sha256_core_coverpoints( + .clk(clk), + .reset_n(reset_n) +); diff --git a/src/sha256/formal/properties/fv_sha256_core_pkg.sv b/src/sha256/formal/properties/fv_sha256_core_pkg.sv new file mode 100644 index 000000000..74d5a4a2f --- /dev/null +++ b/src/sha256/formal/properties/fv_sha256_core_pkg.sv @@ -0,0 +1,76 @@ +// ------------------------------------------------- +// 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 fv_sha256_core_pkg; + +typedef bit unsigned [31:0] a_unsigned_32_64 [63:0]; + +// Constants + +parameter a_unsigned_32_64 K = '{ 0:'h428A2F98, 1:'h71374491, 2:'hB5C0FBCF, 3:'hE9B5DBA5, 4:'h3956C25B, 5:'h59F111F1, 6:'h923F82A4, 7:'hAB1C5ED5, 8:'hD807AA98, 9:'h12835B01, 10:'h243185BE, 11:'h550C7DC3, 12:'h72BE5D74, 13:'h80DEB1FE, 14:'h9BDC06A7, 15:'hC19BF174, 16:'hE49B69C1, 17:'hEFBE4786, 18:'hFC19DC6, 19:'h240CA1CC, 20:'h2DE92C6F, 21:'h4A7484AA, 22:'h5CB0A9DC, 23:'h76F988DA, 24:'h983E5152, 25:'hA831C66D, 26:'hB00327C8, 27:'hBF597FC7, 28:'hC6E00BF3, 29:'hD5A79147, 30:'h6CA6351, 31:'h14292967, 32:'h27B70A85, 33:'h2E1B2138, 34:'h4D2C6DFC, 35:'h53380D13, 36:'h650A7354, 37:'h766A0ABB, 38:'h81C2C92E, 39:'h92722C85, 40:'hA2BFE8A1, 41:'hA81A664B, 42:'hC24B8B70, 43:'hC76C51A3, 44:'hD192E819, 45:'hD6990624, 46:'hF40E3585, 47:'h106AA070, 48:'h19A4C116, 49:'h1E376C08, 50:'h2748774C, 51:'h34B0BCB5, 52:'h391C0CB3, 53:'h4ED8AA4A, 54:'h5B9CCA4F, 55:'h682E6FF3, 56:'h748F82EE, 57:'h78A5636F, 58:'h84C87814, 59:'h8CC70208, 60:'h90BEFFFA, 61:'hA4506CEB, 62:'hBEF9A3F7, 63:'hC67178F2 }; + + +// Functions + +function bit unsigned [31:0] Summ(bit unsigned [31:0] x, bit unsigned [31:0] y, bit unsigned [31:0] z, bit unsigned [31:0] m, bit unsigned [31:0] e); + return ((((x + y) + z) + m) + e); +endfunction + +function bit unsigned [31:0] choose(bit unsigned [31:0] e, bit unsigned [31:0] f, bit unsigned [31:0] g); + return ((e & f) ^ (~e & g)); +endfunction + +function bit unsigned [31:0] compute_w(bit unsigned [31:0] m14, bit unsigned [31:0] m9, bit unsigned [31:0] m1, bit unsigned [31:0] m0); + return (((sig1(m14) + m9) + sig0(m1)) + m0); +endfunction + +function bit unsigned [31:0] majority(bit unsigned [31:0] a, bit unsigned [31:0] b, bit unsigned [31:0] c); + return ((a & (b | c)) | (b & c)); +endfunction + +function bit unsigned [31:0] mult_xor(bit unsigned [31:0] x, bit unsigned [31:0] a, bit unsigned [31:0] b, bit unsigned [31:0] c); + return ((rotr(x, a) ^ rotr(x, b)) ^ rotr(x, c)); +endfunction + +function bit unsigned [31:0] newa(bit unsigned [31:0] x, bit unsigned [31:0] y, bit unsigned [31:0] z); + return ((x + y) + z); +endfunction + +function bit unsigned [31:0] newe(bit unsigned [31:0] x, bit unsigned [31:0] y); + return (x + y); +endfunction + +function bit unsigned [31:0] past_m(bit unsigned [5:0]i,bit unsigned [31:0] m_0,bit unsigned [31:0] m_1,bit unsigned [31:0] m_2,bit unsigned [31:0] m_3,bit unsigned [31:0] m_4,bit unsigned [31:0] m_5,bit unsigned [31:0] m_6,bit unsigned [31:0] m_7,bit unsigned [31:0] m_8,bit unsigned [31:0] m_9,bit unsigned [31:0] m_10,bit unsigned [31:0] m_11,bit unsigned [31:0] m_12,bit unsigned [31:0] m_13,bit unsigned [31:0] m_14,bit unsigned [31:0] m_15); + return ((i == 'sd0 ? m_0 : (i == 'sd1) ? m_1 : (i == 'sd2) ? m_2 : (i == 'sd3) ? m_3 : (i == 'sd4) ? m_4 : (i == 'sd5) ? m_5 : (i == 'sd6) ? m_6 : (i == 'sd7) ? m_7 : (i == 'sd8) ? m_8 : (i == 'sd9) ? m_9 : (i == 'sd10) ? m_10 : (i == 'sd11) ? m_11 : (i == 'sd12) ? m_12 : (i == 'sd13) ? m_13 : (i == 'sd14) ? m_14 : m_15)); +endfunction + +function bit unsigned [31:0] rotr(bit unsigned [31:0] x, bit unsigned [31:0] n); + return ((x >> n) | (x << (32 - n))); +endfunction + +function bit unsigned [31:0] sig0(bit unsigned [31:0] x); + return ((rotr(x, 7) ^ rotr(x, 18)) ^ (x >> 3)); +endfunction + +function bit unsigned [31:0] sig1(bit unsigned [31:0] x); + return ((rotr(x, 17) ^ rotr(x, 19)) ^ (x >> 10)); +endfunction + + +endpackage diff --git a/src/sha256/formal/properties/fv_sha256_package.sv b/src/sha256/formal/properties/fv_sha256_package.sv new file mode 100644 index 000000000..e96e16065 --- /dev/null +++ b/src/sha256/formal/properties/fv_sha256_package.sv @@ -0,0 +1,105 @@ +// ------------------------------------------------- +// 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 sha256_package; + +typedef enum logic [2:0] {WNTZ_IDLE, WNTZ_1ST, WNTZ_OTHERS} wntz_fsm_t; + +typedef logic unsigned [31:0] a_unsigned_32_16 [15:0]; + +typedef struct { + logic init_command; + logic next_command; + logic is_sha256_mode; + logic zeroize; + a_unsigned_32_16 message_block; +} st_Sha256CoreRequest; + +typedef logic unsigned [31:0] a_unsigned_32_8 [7:0]; + +typedef struct { + a_unsigned_32_8 digest_block; +} st_Sha256CoreResponse; + +typedef logic unsigned [31:0] a_unsigned_32_6 [5:0]; + +typedef struct { + logic unsigned [127:0] I; + logic unsigned [31:0] q; + logic unsigned [15:0] i; + logic unsigned [7:0] j; + a_unsigned_32_6 tmp; + logic unsigned [135:0] padding; +} st_Winternitz192BlockType; + +typedef struct { + logic init_command; + logic next_command; + logic is_sha256_mode; + logic zeroize; + st_Winternitz192BlockType message_block; +} st_Sha256CoreWinternitz192Request; + +typedef struct { + a_unsigned_32_6 tmp; +} st_Sha256CoreWinternitz192Response; + +typedef struct { + logic unsigned [127:0] I; + logic unsigned [31:0] q; + logic unsigned [15:0] i; + logic unsigned [7:0] j; + a_unsigned_32_8 tmp; + logic unsigned [71:0] padding; +} st_Winternitz256BlockType; + +typedef struct { + logic init_command; + logic next_command; + logic is_sha256_mode; + logic zeroize; + st_Winternitz256BlockType message_block; +} st_Sha256CoreWinternitz256Request; + +typedef struct { + a_unsigned_32_8 tmp; +} st_Sha256CoreWinternitz256Response; + +typedef struct { + logic is_init; + logic is_next; + logic is_sha256_mode; + logic is_winternitz; + logic winternitz_n_mode; + logic unsigned [7:0] winternitz_w; + logic unsigned [7:0] winternitz_loop_init; + logic zeroize; + a_unsigned_32_16 message_block; +} st_Sha256Request; + +typedef struct { + a_unsigned_32_8 digest_block; +} st_Sha256Response; + + +// Constants + +parameter logic unsigned [7:0] SHA256_ENDING = 8'h80; + + +endpackage diff --git a/src/sha512_masked/formal/properties/fv_constraints.sv b/src/sha512_masked/formal/properties/fv_constraints.sv index f3534f5ef..87a5a0625 100644 --- a/src/sha512_masked/formal/properties/fv_constraints.sv +++ b/src/sha512_masked/formal/properties/fv_constraints.sv @@ -17,7 +17,7 @@ // limitations under the License. // -module fv_constraints_m( +module fv_constraints_sha_m( input logic init_cmd, input logic next_cmd, input logic reset_n, @@ -26,7 +26,7 @@ module fv_constraints_m( input logic ready, input logic digest_valid, input logic [1023 : 0] block_msg, - input logic [73 : 0] lfsr_seed, + input logic [191 : 0] entropy, input logic [511 : 0] digest, input logic [1 : 0] mode ); @@ -53,7 +53,7 @@ module fv_constraints_m( 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); + !(sha512_masked_core.ready) |-> $stable(entropy) && $stable(block_msg) && $stable(sha512_masked_core.mode); endproperty assume_inputs_stay_stable: assume property (disable iff(!reset_n || zeroize) inputs_stay_stable); @@ -67,10 +67,10 @@ module fv_constraints_m( 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( +bind sha512_masked_core fv_constraints_sha_m fv_constraints( .init_cmd(init_cmd), .next_cmd(next_cmd), .reset_n(reset_n), @@ -80,6 +80,6 @@ bind sha512_masked_core fv_constraints_m fv_constraints( .mode(mode), .block_msg(block_msg), .zeroize(zeroize), - .lfsr_seed(lfsr_seed), + .entropy(entropy), .digest(digest) ); diff --git a/src/sha512_masked/formal/properties/fv_coverpoints.sv b/src/sha512_masked/formal/properties/fv_coverpoints.sv index 99fc818e4..b78479fba 100644 --- a/src/sha512_masked/formal/properties/fv_coverpoints.sv +++ b/src/sha512_masked/formal/properties/fv_coverpoints.sv @@ -16,8 +16,8 @@ // See the License for the specific language governing permissions and // limitations under the License. // - -module fv_coverpoints_m( + +module fv_coverpoints_sha_m( input logic clk, input logic reset_n, input logic zeroize @@ -43,7 +43,7 @@ module fv_coverpoints_m( endmodule -bind sha512_masked_core fv_coverpoints_m fv_coverpoints( +bind sha512_masked_core fv_coverpoints_sha_m fv_coverpoints( .clk(clk), .reset_n(reset_n), .zeroize(zeroize) diff --git a/src/sha512_masked/formal/properties/fv_sha512_masked.sv b/src/sha512_masked/formal/properties/fv_sha512_masked.sv index a7b0ef598..b95e4620e 100644 --- a/src/sha512_masked/formal/properties/fv_sha512_masked.sv +++ b/src/sha512_masked/formal/properties/fv_sha512_masked.sv @@ -16,59 +16,54 @@ // 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, +import SHA512_masked_pkg::*; - // Inputs - input st_SHA_Args sha_in_struct, - input bit unsigned [73:0] lfsr_in, - // Outputs - input bit unsigned [511:0] digest_out, +module fv_sha512_masked_core_m( + input logic rst, + input logic clk, - // Valid signals - input bit block_in_valid, - input bit digest_valid, - - // Ready signals - input bit block_in_ready, + // Ports + input logic SHA_Input_sync, + input logic SHA_Input_notify, + input st_SHA_Args SHA_Input, + + input logic out_notify, + input logic unsigned [511:0] out, // 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 logic signed [31:0] SHA_Mode_in, + input st_SHA_Args SHA_in, + input a_st_masked_reg_t_16 W, input st_masked_reg_t a, input st_masked_reg_t b, - input bit unsigned [1023:0] block_in, + input logic 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, + input logic signed [31:0] i, + input logic init_cmd, + input a_sc_big_unsigned_64_24 masking_rnd, + input logic signed [31:0] p, // States - input bit IDLE, - input bit CTRL_RND, - input bit SHA_Rounds, - input bit DONE + input logic IDLE, + input logic CTRL_RND, + input logic SHA_Rounds, + input logic DONE ); default clocking default_clk @(posedge clk); endclocking -a_sc_big_unsigned_64_8 H_0 = '{ +a_sc_big_unsigned_64_8 H_0_i = '{ 0: 64'd0, 1: 64'd0, 2: 64'd0, @@ -79,7 +74,40 @@ a_sc_big_unsigned_64_8 H_0 = '{ 7: 64'd0 }; -a_sc_big_unsigned_64_16 W_0 = '{ +st_SHA_Args SHA_in_0_i = '{ + in: 1024'd0, + entropy: 192'd0, + SHA_Mode: 'sd0, + init_cmd: 0, + next_cmd: 0, + zeroize: 0 +}; + +a_st_masked_reg_t_16 W_0_i = '{ + 0: '{ masked: 64'd0, random: 64'd0 }, + 1: '{ masked: 64'd0, random: 64'd0 }, + 2: '{ masked: 64'd0, random: 64'd0 }, + 3: '{ masked: 64'd0, random: 64'd0 }, + 4: '{ masked: 64'd0, random: 64'd0 }, + 5: '{ masked: 64'd0, random: 64'd0 }, + 6: '{ masked: 64'd0, random: 64'd0 }, + 7: '{ masked: 64'd0, random: 64'd0 }, + 8: '{ masked: 64'd0, random: 64'd0 }, + 9: '{ masked: 64'd0, random: 64'd0 }, + 10: '{ masked: 64'd0, random: 64'd0 }, + 11: '{ masked: 64'd0, random: 64'd0 }, + 12: '{ masked: 64'd0, random: 64'd0 }, + 13: '{ masked: 64'd0, random: 64'd0 }, + 14: '{ masked: 64'd0, random: 64'd0 }, + 15: '{ masked: 64'd0, random: 64'd0 } +}; + +st_masked_reg_t a_0_i = '{ + masked: 64'd0, + random: 64'd0 +}; + +a_sc_big_unsigned_64_24 masking_rnd_0_i = '{ 0: 64'd0, 1: 64'd0, 2: 64'd0, @@ -95,26 +123,77 @@ a_sc_big_unsigned_64_16 W_0 = '{ 12: 64'd0, 13: 64'd0, 14: 64'd0, - 15: 64'd0 + 15: 64'd0, + 16: 64'd0, + 17: 64'd0, + 18: 64'd0, + 19: 64'd0, + 20: 64'd0, + 21: 64'd0, + 22: 64'd0, + 23: 64'd0 }; -st_masked_reg_t a_0 = '{ - masked: 64'd0, - random: 64'd0 +a_sc_big_unsigned_64_24 masking_rnd_1_i = '{ + 0: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd0) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd0) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd0) ? 64'(SHA_in.entropy) : masking_rnd['sd0]))), + 1: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd1) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd1) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd1) ? 64'(SHA_in.entropy) : masking_rnd['sd1]))), + 2: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd2) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd2) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd2) ? 64'(SHA_in.entropy) : masking_rnd['sd2]))), + 3: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd3) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd3) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd3) ? 64'(SHA_in.entropy) : masking_rnd['sd3]))), + 4: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd4) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd4) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd4) ? 64'(SHA_in.entropy) : masking_rnd['sd4]))), + 5: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd5) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd5) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd5) ? 64'(SHA_in.entropy) : masking_rnd['sd5]))), + 6: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd6) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd6) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd6) ? 64'(SHA_in.entropy) : masking_rnd['sd6]))), + 7: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd7) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd7) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd7) ? 64'(SHA_in.entropy) : masking_rnd['sd7]))), + 8: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd8) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd8) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd8) ? 64'(SHA_in.entropy) : masking_rnd['sd8]))), + 9: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd9) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd9) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd9) ? 64'(SHA_in.entropy) : masking_rnd['sd9]))), + 10: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd10) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd10) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd10) ? 64'(SHA_in.entropy) : masking_rnd['sd10]))), + 11: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd11) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd11) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd11) ? 64'(SHA_in.entropy) : masking_rnd['sd11]))), + 12: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd12) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd12) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd12) ? 64'(SHA_in.entropy) : masking_rnd['sd12]))), + 13: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd13) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd13) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd13) ? 64'(SHA_in.entropy) : masking_rnd['sd13]))), + 14: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd14) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd14) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd14) ? 64'(SHA_in.entropy) : masking_rnd['sd14]))), + 15: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd15) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd15) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd15) ? 64'(SHA_in.entropy) : masking_rnd['sd15]))), + 16: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd16) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd16) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd16) ? 64'(SHA_in.entropy) : masking_rnd['sd16]))), + 17: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd17) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd17) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd17) ? 64'(SHA_in.entropy) : masking_rnd['sd17]))), + 18: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd18) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd18) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd18) ? 64'(SHA_in.entropy) : masking_rnd['sd18]))), + 19: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd19) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd19) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd19) ? 64'(SHA_in.entropy) : masking_rnd['sd19]))), + 20: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd20) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd20) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd20) ? 64'(SHA_in.entropy) : masking_rnd['sd20]))), + 21: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd21) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd21) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd21) ? 64'(SHA_in.entropy) : masking_rnd['sd21]))), + 22: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd22) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd22) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd22) ? 64'(SHA_in.entropy) : masking_rnd['sd22]))), + 23: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd23) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd23) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd23) ? 64'(SHA_in.entropy) : masking_rnd['sd23]))) }; -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]) -}; +logic unsigned [63:0] slicer_0_i = slicer(block_in, 'sd0); + +logic unsigned [63:0] slicer_1_i = slicer(block_in, 'sd1); + +logic unsigned [63:0] slicer_2_i = slicer(block_in, 'sd2); + +logic unsigned [63:0] slicer_3_i = slicer(block_in, 'sd3); + +logic unsigned [63:0] slicer_4_i = slicer(block_in, 'sd4); + +logic unsigned [63:0] slicer_5_i = slicer(block_in, 'sd5); -a_sc_big_unsigned_64_8 H_1 = '{ +logic unsigned [63:0] slicer_6_i = slicer(block_in, 'sd6); + +logic unsigned [63:0] slicer_7_i = slicer(block_in, 'sd7); + +logic unsigned [63:0] slicer_8_i = slicer(block_in, 'sd8); + +logic unsigned [63:0] slicer_9_i = slicer(block_in, 'sd9); + +logic unsigned [63:0] slicer_10_i = slicer(block_in, 'sd10); + +logic unsigned [63:0] slicer_11_i = slicer(block_in, 'sd11); + +logic unsigned [63:0] slicer_12_i = slicer(block_in, 'sd12); + +logic unsigned [63:0] slicer_13_i = slicer(block_in, 'sd13); + +logic unsigned [63:0] slicer_14_i = slicer(block_in, 'sd14); + +logic unsigned [63:0] slicer_15_i = slicer(block_in, 'sd15); + +a_sc_big_unsigned_64_8 H_1_i = '{ 0: 64'h8C3D37C819544DA2, 1: 64'h73E1996689DCD4D6, 2: 64'h1DFAB7AE32FF9C82, @@ -125,77 +204,66 @@ a_sc_big_unsigned_64_8 H_1 = '{ 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]) +a_st_masked_reg_t_16 W_1_i = '{ + 0: '{ masked: (slicer_15_i ^ (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd8) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd8) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd8) ? 64'(SHA_in.entropy) : masking_rnd['sd8])))), random: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd8) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd8) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd8) ? 64'(SHA_in.entropy) : masking_rnd['sd8]))) }, + 1: '{ masked: (slicer_14_i ^ (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd9) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd9) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd9) ? 64'(SHA_in.entropy) : masking_rnd['sd9])))), random: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd9) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd9) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd9) ? 64'(SHA_in.entropy) : masking_rnd['sd9]))) }, + 2: '{ masked: (slicer_13_i ^ (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd10) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd10) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd10) ? 64'(SHA_in.entropy) : masking_rnd['sd10])))), random: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd10) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd10) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd10) ? 64'(SHA_in.entropy) : masking_rnd['sd10]))) }, + 3: '{ masked: (slicer_12_i ^ (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd11) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd11) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd11) ? 64'(SHA_in.entropy) : masking_rnd['sd11])))), random: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd11) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd11) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd11) ? 64'(SHA_in.entropy) : masking_rnd['sd11]))) }, + 4: '{ masked: (slicer_11_i ^ (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd12) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd12) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd12) ? 64'(SHA_in.entropy) : masking_rnd['sd12])))), random: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd12) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd12) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd12) ? 64'(SHA_in.entropy) : masking_rnd['sd12]))) }, + 5: '{ masked: (slicer_10_i ^ (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd13) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd13) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd13) ? 64'(SHA_in.entropy) : masking_rnd['sd13])))), random: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd13) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd13) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd13) ? 64'(SHA_in.entropy) : masking_rnd['sd13]))) }, + 6: '{ masked: (slicer_9_i ^ (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd14) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd14) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd14) ? 64'(SHA_in.entropy) : masking_rnd['sd14])))), random: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd14) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd14) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd14) ? 64'(SHA_in.entropy) : masking_rnd['sd14]))) }, + 7: '{ masked: (slicer_8_i ^ (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd15) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd15) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd15) ? 64'(SHA_in.entropy) : masking_rnd['sd15])))), random: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd15) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd15) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd15) ? 64'(SHA_in.entropy) : masking_rnd['sd15]))) }, + 8: '{ masked: (slicer_7_i ^ (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd16) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd16) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd16) ? 64'(SHA_in.entropy) : masking_rnd['sd16])))), random: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd16) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd16) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd16) ? 64'(SHA_in.entropy) : masking_rnd['sd16]))) }, + 9: '{ masked: (slicer_6_i ^ (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd17) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd17) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd17) ? 64'(SHA_in.entropy) : masking_rnd['sd17])))), random: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd17) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd17) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd17) ? 64'(SHA_in.entropy) : masking_rnd['sd17]))) }, + 10: '{ masked: (slicer_5_i ^ (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd18) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd18) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd18) ? 64'(SHA_in.entropy) : masking_rnd['sd18])))), random: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd18) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd18) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd18) ? 64'(SHA_in.entropy) : masking_rnd['sd18]))) }, + 11: '{ masked: (slicer_4_i ^ (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd19) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd19) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd19) ? 64'(SHA_in.entropy) : masking_rnd['sd19])))), random: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd19) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd19) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd19) ? 64'(SHA_in.entropy) : masking_rnd['sd19]))) }, + 12: '{ masked: (slicer_3_i ^ (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd20) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd20) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd20) ? 64'(SHA_in.entropy) : masking_rnd['sd20])))), random: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd20) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd20) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd20) ? 64'(SHA_in.entropy) : masking_rnd['sd20]))) }, + 13: '{ masked: (slicer_2_i ^ (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd21) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd21) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd21) ? 64'(SHA_in.entropy) : masking_rnd['sd21])))), random: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd21) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd21) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd21) ? 64'(SHA_in.entropy) : masking_rnd['sd21]))) }, + 14: '{ masked: (slicer_1_i ^ (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd22) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd22) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd22) ? 64'(SHA_in.entropy) : masking_rnd['sd22])))), random: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd22) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd22) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd22) ? 64'(SHA_in.entropy) : masking_rnd['sd22]))) }, + 15: '{ masked: (slicer_0_i ^ (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd23) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd23) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd23) ? 64'(SHA_in.entropy) : masking_rnd['sd23])))), random: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd23) ? 64'((SHA_in.entropy >> 192'd128)) : (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd23) ? 64'((SHA_in.entropy >> 192'd64)) : ((('sd3 * (p & 'sh7)) == 'sd23) ? 64'(SHA_in.entropy) : masking_rnd['sd23]))) } }; -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 a_1_i = '{ + masked: (64'h8C3D37C819544DA2 ^ ((('sd3 * (p & 'sh7)) == 'sd0) ? 64'(SHA_in.entropy) : masking_rnd['sd0])), + random: ((('sd3 * (p & 'sh7)) == 'sd0) ? 64'(SHA_in.entropy) : masking_rnd['sd0]) }; -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 b_0_i = '{ + masked: (64'h73E1996689DCD4D6 ^ (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd1) ? 64'((SHA_in.entropy >> 192'd64)) : masking_rnd['sd1])), + random: (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd1) ? 64'((SHA_in.entropy >> 192'd64)) : masking_rnd['sd1]) }; -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 c_0_i = '{ + masked: (64'h1DFAB7AE32FF9C82 ^ (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd2) ? 64'((SHA_in.entropy >> 192'd128)) : masking_rnd['sd2])), + random: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd2) ? 64'((SHA_in.entropy >> 192'd128)) : masking_rnd['sd2]) }; -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 d_0_i = '{ + masked: (64'h679DD514582F9FCF ^ ((('sd3 * (p & 'sh7)) == 'sd3) ? 64'(SHA_in.entropy) : masking_rnd['sd3])), + random: ((('sd3 * (p & 'sh7)) == 'sd3) ? 64'(SHA_in.entropy) : masking_rnd['sd3]) }; -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 e_0_i = '{ + masked: (64'hF6D2B697BD44DA8 ^ (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd4) ? 64'((SHA_in.entropy >> 192'd64)) : masking_rnd['sd4])), + random: (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd4) ? 64'((SHA_in.entropy >> 192'd64)) : masking_rnd['sd4]) }; -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 f_0_i = '{ + masked: (64'h77E36F7304C48942 ^ (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd5) ? 64'((SHA_in.entropy >> 192'd128)) : masking_rnd['sd5])), + random: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd5) ? 64'((SHA_in.entropy >> 192'd128)) : masking_rnd['sd5]) }; -st_masked_reg_t h_0 = '{ - masked: (64'h1112E6AD91D692A1 ^ (0 ? lfsr_in : rh_masking_rnd['sd7])), - random: (0 ? lfsr_in : rh_masking_rnd['sd7]) +st_masked_reg_t g_0_i = '{ + masked: (64'h3F9D85A86A1D36C8 ^ ((('sd3 * (p & 'sh7)) == 'sd6) ? 64'(SHA_in.entropy) : masking_rnd['sd6])), + random: ((('sd3 * (p & 'sh7)) == 'sd6) ? 64'(SHA_in.entropy) : masking_rnd['sd6]) }; -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] +st_masked_reg_t h_0_i = '{ + masked: (64'h1112E6AD91D692A1 ^ (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd7) ? 64'((SHA_in.entropy >> 192'd64)) : masking_rnd['sd7])), + random: (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd7) ? 64'((SHA_in.entropy >> 192'd64)) : masking_rnd['sd7]) }; -a_sc_big_unsigned_64_8 H_2 = '{ +a_sc_big_unsigned_64_8 H_2_i = '{ 0: 64'h22312194FC2BF72C, 1: 64'h9F555FA3C84C64C2, 2: 64'h2393B86B6F53B151, @@ -206,47 +274,47 @@ a_sc_big_unsigned_64_8 H_2 = '{ 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 a_2_i = '{ + masked: (64'h22312194FC2BF72C ^ ((('sd3 * (p & 'sh7)) == 'sd0) ? 64'(SHA_in.entropy) : masking_rnd['sd0])), + random: ((('sd3 * (p & 'sh7)) == 'sd0) ? 64'(SHA_in.entropy) : 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 b_1_i = '{ + masked: (64'h9F555FA3C84C64C2 ^ (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd1) ? 64'((SHA_in.entropy >> 192'd64)) : masking_rnd['sd1])), + random: (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd1) ? 64'((SHA_in.entropy >> 192'd64)) : 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 c_1_i = '{ + masked: (64'h2393B86B6F53B151 ^ (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd2) ? 64'((SHA_in.entropy >> 192'd128)) : masking_rnd['sd2])), + random: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd2) ? 64'((SHA_in.entropy >> 192'd128)) : 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 d_1_i = '{ + masked: (64'h963877195940EABD ^ ((('sd3 * (p & 'sh7)) == 'sd3) ? 64'(SHA_in.entropy) : masking_rnd['sd3])), + random: ((('sd3 * (p & 'sh7)) == 'sd3) ? 64'(SHA_in.entropy) : 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 e_1_i = '{ + masked: (64'h96283EE2A88EFFE3 ^ (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd4) ? 64'((SHA_in.entropy >> 192'd64)) : masking_rnd['sd4])), + random: (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd4) ? 64'((SHA_in.entropy >> 192'd64)) : 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 f_1_i = '{ + masked: (64'hBE5E1E2553863992 ^ (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd5) ? 64'((SHA_in.entropy >> 192'd128)) : masking_rnd['sd5])), + random: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd5) ? 64'((SHA_in.entropy >> 192'd128)) : 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 g_1_i = '{ + masked: (64'h2B0199FC2C85B8AA ^ ((('sd3 * (p & 'sh7)) == 'sd6) ? 64'(SHA_in.entropy) : masking_rnd['sd6])), + random: ((('sd3 * (p & 'sh7)) == 'sd6) ? 64'(SHA_in.entropy) : 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]) +st_masked_reg_t h_1_i = '{ + masked: (64'hEB72DDC81C52CA2 ^ (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd7) ? 64'((SHA_in.entropy >> 192'd64)) : masking_rnd['sd7])), + random: (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd7) ? 64'((SHA_in.entropy >> 192'd64)) : masking_rnd['sd7]) }; -a_sc_big_unsigned_64_8 H_3 = '{ +a_sc_big_unsigned_64_8 H_3_i = '{ 0: 64'h6A09E667F3BCC908, 1: 64'hBB67AE8584CAA73B, 2: 64'h3C6EF372FE94F82B, @@ -257,47 +325,47 @@ a_sc_big_unsigned_64_8 H_3 = '{ 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 a_3_i = '{ + masked: (64'h6A09E667F3BCC908 ^ ((('sd3 * (p & 'sh7)) == 'sd0) ? 64'(SHA_in.entropy) : masking_rnd['sd0])), + random: ((('sd3 * (p & 'sh7)) == 'sd0) ? 64'(SHA_in.entropy) : 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 b_2_i = '{ + masked: (64'hBB67AE8584CAA73B ^ (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd1) ? 64'((SHA_in.entropy >> 192'd64)) : masking_rnd['sd1])), + random: (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd1) ? 64'((SHA_in.entropy >> 192'd64)) : 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 c_2_i = '{ + masked: (64'h3C6EF372FE94F82B ^ (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd2) ? 64'((SHA_in.entropy >> 192'd128)) : masking_rnd['sd2])), + random: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd2) ? 64'((SHA_in.entropy >> 192'd128)) : 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 d_2_i = '{ + masked: (64'hA54FF53A5F1D36F1 ^ ((('sd3 * (p & 'sh7)) == 'sd3) ? 64'(SHA_in.entropy) : masking_rnd['sd3])), + random: ((('sd3 * (p & 'sh7)) == 'sd3) ? 64'(SHA_in.entropy) : 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 e_2_i = '{ + masked: (64'h510E527FADE682D1 ^ (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd4) ? 64'((SHA_in.entropy >> 192'd64)) : masking_rnd['sd4])), + random: (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd4) ? 64'((SHA_in.entropy >> 192'd64)) : 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 f_2_i = '{ + masked: (64'h9B05688C2B3E6C1F ^ (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd5) ? 64'((SHA_in.entropy >> 192'd128)) : masking_rnd['sd5])), + random: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd5) ? 64'((SHA_in.entropy >> 192'd128)) : 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 g_2_i = '{ + masked: (64'h1F83D9ABFB41BD6B ^ ((('sd3 * (p & 'sh7)) == 'sd6) ? 64'(SHA_in.entropy) : masking_rnd['sd6])), + random: ((('sd3 * (p & 'sh7)) == 'sd6) ? 64'(SHA_in.entropy) : 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]) +st_masked_reg_t h_2_i = '{ + masked: (64'h5BE0CD19137E2179 ^ (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd7) ? 64'((SHA_in.entropy >> 192'd64)) : masking_rnd['sd7])), + random: (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd7) ? 64'((SHA_in.entropy >> 192'd64)) : masking_rnd['sd7]) }; -a_sc_big_unsigned_64_8 H_4 = '{ +a_sc_big_unsigned_64_8 H_4_i = '{ 0: 64'hCBBB9D5DC1059ED8, 1: 64'h629A292A367CD507, 2: 64'h9159015A3070DD17, @@ -308,126 +376,164 @@ a_sc_big_unsigned_64_8 H_4 = '{ 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 a_4_i = '{ + masked: (64'hCBBB9D5DC1059ED8 ^ ((('sd3 * (p & 'sh7)) == 'sd0) ? 64'(SHA_in.entropy) : masking_rnd['sd0])), + random: ((('sd3 * (p & 'sh7)) == 'sd0) ? 64'(SHA_in.entropy) : 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 b_3_i = '{ + masked: (64'h629A292A367CD507 ^ (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd1) ? 64'((SHA_in.entropy >> 192'd64)) : masking_rnd['sd1])), + random: (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd1) ? 64'((SHA_in.entropy >> 192'd64)) : 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 c_3_i = '{ + masked: (64'h9159015A3070DD17 ^ (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd2) ? 64'((SHA_in.entropy >> 192'd128)) : masking_rnd['sd2])), + random: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd2) ? 64'((SHA_in.entropy >> 192'd128)) : 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 d_3_i = '{ + masked: (64'h152FECD8F70E5939 ^ ((('sd3 * (p & 'sh7)) == 'sd3) ? 64'(SHA_in.entropy) : masking_rnd['sd3])), + random: ((('sd3 * (p & 'sh7)) == 'sd3) ? 64'(SHA_in.entropy) : 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 e_3_i = '{ + masked: (64'h67332667FFC00B31 ^ (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd4) ? 64'((SHA_in.entropy >> 192'd64)) : masking_rnd['sd4])), + random: (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd4) ? 64'((SHA_in.entropy >> 192'd64)) : 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 f_3_i = '{ + masked: (64'h8EB44A8768581511 ^ (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd5) ? 64'((SHA_in.entropy >> 192'd128)) : masking_rnd['sd5])), + random: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd5) ? 64'((SHA_in.entropy >> 192'd128)) : 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 g_3_i = '{ + masked: (64'hDB0C2E0D64F98FA7 ^ ((('sd3 * (p & 'sh7)) == 'sd6) ? 64'(SHA_in.entropy) : masking_rnd['sd6])), + random: ((('sd3 * (p & 'sh7)) == 'sd6) ? 64'(SHA_in.entropy) : 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 h_3_i = '{ + masked: (64'h47B5481DBEFA4FA4 ^ (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd7) ? 64'((SHA_in.entropy >> 192'd64)) : masking_rnd['sd7])), + random: (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd7) ? 64'((SHA_in.entropy >> 192'd64)) : 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 a_5_i = '{ + masked: (H[64'd0] ^ ((('sd3 * (p & 'sh7)) == 'sd0) ? 64'(SHA_in.entropy) : masking_rnd['sd0])), + random: ((('sd3 * (p & 'sh7)) == 'sd0) ? 64'(SHA_in.entropy) : 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 b_4_i = '{ + masked: (H[64'd1] ^ (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd1) ? 64'((SHA_in.entropy >> 192'd64)) : masking_rnd['sd1])), + random: (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd1) ? 64'((SHA_in.entropy >> 192'd64)) : 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 c_4_i = '{ + masked: (H[64'd2] ^ (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd2) ? 64'((SHA_in.entropy >> 192'd128)) : masking_rnd['sd2])), + random: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd2) ? 64'((SHA_in.entropy >> 192'd128)) : 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 d_4_i = '{ + masked: (H[64'd3] ^ ((('sd3 * (p & 'sh7)) == 'sd3) ? 64'(SHA_in.entropy) : masking_rnd['sd3])), + random: ((('sd3 * (p & 'sh7)) == 'sd3) ? 64'(SHA_in.entropy) : 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 e_4_i = '{ + masked: (H[64'd4] ^ (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd4) ? 64'((SHA_in.entropy >> 192'd64)) : masking_rnd['sd4])), + random: (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd4) ? 64'((SHA_in.entropy >> 192'd64)) : 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 f_4_i = '{ + masked: (H[64'd5] ^ (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd5) ? 64'((SHA_in.entropy >> 192'd128)) : masking_rnd['sd5])), + random: (((('sd3 * (p & 'sh7)) + 'sd2) == 'sd5) ? 64'((SHA_in.entropy >> 192'd128)) : 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 g_4_i = '{ + masked: (H[64'd6] ^ ((('sd3 * (p & 'sh7)) == 'sd6) ? 64'(SHA_in.entropy) : masking_rnd['sd6])), + random: ((('sd3 * (p & 'sh7)) == 'sd6) ? 64'(SHA_in.entropy) : 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 h_4_i = '{ + masked: (H[64'd7] ^ (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd7) ? 64'((SHA_in.entropy >> 192'd64)) : masking_rnd['sd7])), + random: (((('sd3 * (p & 'sh7)) + 'sd1) == 'sd7) ? 64'((SHA_in.entropy >> 192'd64)) : 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)) +logic ent_shift_0_i = ent_shift(SHA_in.entropy, 192'd32); + +logic ent_shift_1_i = ent_shift(SHA_in.entropy, 192'd64); + +logic ent_shift_2_i = ent_shift(SHA_in.entropy, 192'd128); + +logic ent_shift_3_i = ent_shift(SHA_in.entropy, 192'd256); + +logic ent_shift_4_i = ent_shift(SHA_in.entropy, 192'd512); + +logic ent_shift_5_i = ent_shift(SHA_in.entropy, 192'd1024); + +logic ent_shift_6_i = ent_shift(SHA_in.entropy, 192'd2048); + +logic ent_shift_7_i = ent_shift(SHA_in.entropy, 192'd4096); + +logic ent_shift_8_i = ent_shift(SHA_in.entropy, 192'd8192); + +logic ent_shift_9_i = ent_shift(SHA_in.entropy, 192'd16384); + +logic unsigned [63:0] T1_m_0_i = T1_m(e.masked, e.random, f.masked, f.random, g.masked, g.random, h.masked, h.random, K[i], W[i].masked, W[i].random, 0, 128'd0, 64'd0, ent_shift_0_i, ent_shift_1_i, ent_shift_2_i, ent_shift_3_i, ent_shift_4_i, 'sd0); + +logic unsigned [63:0] T1_r_0_i = T1_r(e.random, g.random, h.random, W[i].random); + +logic unsigned [63:0] T2_m_0_i = T2_m(a.masked, a.random, b.masked, b.random, c.masked, c.random, 0, 128'd0, 64'd0, ent_shift_5_i, ent_shift_6_i, 'sd0); + +logic unsigned [63:0] T2_r_0_i = T2_r(a.random, b.random); + +logic unsigned [63:0] B2A_conv_0_i = B2A_conv(d.masked, d.random, ent_shift_7_i, 0, 128'd0, 64'd0, 'sd0); + +st_masked_reg_t a_6_i = '{ + masked: A2B_conv(64'((T1_m_0_i + T2_m_0_i)), 64'((T1_r_0_i + T2_r_0_i)), ent_shift_8_i, 0, 128'd0, 64'd0, 'sd0), + random: (T1_r_0_i + T2_r_0_i) }; -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))) +st_masked_reg_t e_5_i = '{ + masked: A2B_conv(64'((B2A_conv_0_i + T1_m_0_i)), 64'((d.random + T1_r_0_i)), ent_shift_9_i, 0, 128'd0, 64'd0, 'sd0), + random: (d.random + T1_r_0_i) }; -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]) +logic unsigned [63:0] compute_w_random_0_i = compute_w_random(W[64'd14].random, W[64'd9].random, W[64'd1].random, W[64'd0].random); + +logic unsigned [63:0] compute_w_masked_0_i = compute_w_masked(W[64'd14], W[64'd9], W[64'd1], W[64'd0], SHA_in.entropy, 0, 128'd0, 64'd0, 'sd0, compute_w_random_0_i); + +logic unsigned [63:0] T1_m_1_i = T1_m(e.masked, e.random, f.masked, f.random, g.masked, g.random, h.masked, h.random, K[i], compute_w_masked_0_i, compute_w_random_0_i, 0, 128'd0, 64'd0, ent_shift_0_i, ent_shift_1_i, ent_shift_2_i, ent_shift_3_i, ent_shift_4_i, 'sd0); + +logic unsigned [63:0] T1_r_1_i = T1_r(e.random, g.random, h.random, compute_w_random_0_i); + +a_st_masked_reg_t_16 W_2_i = '{ + 0: '{ masked: W['sd1].masked, random: W['sd1].random }, + 1: '{ masked: W['sd2].masked, random: W['sd2].random }, + 2: '{ masked: W['sd3].masked, random: W['sd3].random }, + 3: '{ masked: W['sd4].masked, random: W['sd4].random }, + 4: '{ masked: W['sd5].masked, random: W['sd5].random }, + 5: '{ masked: W['sd6].masked, random: W['sd6].random }, + 6: '{ masked: W['sd7].masked, random: W['sd7].random }, + 7: '{ masked: W['sd8].masked, random: W['sd8].random }, + 8: '{ masked: W['sd9].masked, random: W['sd9].random }, + 9: '{ masked: W['sd10].masked, random: W['sd10].random }, + 10: '{ masked: W['sd11].masked, random: W['sd11].random }, + 11: '{ masked: W['sd12].masked, random: W['sd12].random }, + 12: '{ masked: W['sd13].masked, random: W['sd13].random }, + 13: '{ masked: W['sd14].masked, random: W['sd14].random }, + 14: '{ masked: W['sd15].masked, random: W['sd15].random }, + 15: '{ masked: compute_w_masked(W[64'd14], W[64'd9], W[64'd1], W[64'd0], SHA_in.entropy, 0, 128'd0, 64'd0, 'sd0, compute_w_random_0_i), random: compute_w_random(W[64'd14].random, W[64'd9].random, W[64'd1].random, W[64'd0].random) } }; -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 a_7_i = '{ + masked: A2B_conv(64'((T1_m_1_i + T2_m_0_i)), 64'((T1_r_1_i + T2_r_0_i)), ent_shift_8_i, 0, 128'd0, 64'd0, 'sd0), + random: (T1_r_1_i + T2_r_0_i) }; -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))) +st_masked_reg_t e_6_i = '{ + masked: A2B_conv(64'((B2A_conv_0_i + T1_m_1_i)), 64'((d.random + T1_r_1_i)), ent_shift_9_i, 0, 128'd0, 64'd0, 'sd0), + random: (d.random + T1_r_1_i) }; -a_sc_big_unsigned_64_8 H_5 = '{ +a_sc_big_unsigned_64_8 H_5_i = '{ 0: (H[64'd0] + (a.masked ^ a.random)), 1: (H['sd1] + (b.masked ^ b.random)), 2: (H['sd2] + (c.masked ^ c.random)), @@ -446,33 +552,33 @@ endsequence reset_a: assert property (reset_p); property reset_p; - $past(!rst) && rst |-> + $past(!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 && + H == H_0_i && + W == W_0_i && + a == a_0_i && + b == a_0_i && + c == a_0_i && + d == a_0_i && + e == a_0_i && + f == a_0_i && + g == a_0_i && + h == a_0_i && i == 'sd0 && - rnd_cnt_reg == 'sd0 && - rh_masking_rnd == H_0 && - block_in_ready == 1 && - digest_valid == 0; + masking_rnd == masking_rnd_0_i && + p == 'sd0 && + SHA_Input_notify == 1 && + out_notify == 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) + (('sd1 + p) < 'sd9) |-> - ##1 (block_in_ready == 0) and - ##1 (digest_valid == 0) and + ##1 (SHA_Input_notify == 0) and + ##1 (out_notify == 0) and ##1 CTRL_RND && H == $past(H, 1) && @@ -486,144 +592,144 @@ property CTRL_RND_to_CTRL_RND_p; 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); + masking_rnd == $past(masking_rnd_1_i, 1) && + p == ('sd1 + $past(p, 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_to_SHA_Rounds_a: assert property (disable iff(!rst) CTRL_RND_to_SHA_Rounds_p); +property CTRL_RND_to_SHA_Rounds_p; CTRL_RND && - (('sd1 + rnd_cnt_reg) >= 'sd9) && - block_init && - (block_sha_mode == 'sd0) + (('sd1 + p) >= 'sd9) && + init_cmd && + (SHA_Mode_in == 'sd0) |-> - ##1 (block_in_ready == 0) and - ##1 (digest_valid == 0) and + ##1 (SHA_Input_notify == 0) and + ##1 (out_notify == 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) && + H == $past(H_1_i, 1) && + W == $past(W_1_i, 1) && + a == $past(a_1_i, 1) && + b == $past(b_0_i, 1) && + c == $past(c_0_i, 1) && + d == $past(d_0_i, 1) && + e == $past(e_0_i, 1) && + f == $past(f_0_i, 1) && + g == $past(g_0_i, 1) && + h == $past(h_0_i, 1) && i == 'sd0 && - rnd_cnt_reg == ('sd1 + $past(rnd_cnt_reg, 1)) && - rh_masking_rnd == $past(rh_masking_rnd_1, 1); + masking_rnd == $past(masking_rnd_1_i, 1) && + p == ('sd1 + $past(p, 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_to_SHA_Rounds_1_a: assert property (disable iff(!rst) CTRL_RND_to_SHA_Rounds_1_p); +property CTRL_RND_to_SHA_Rounds_1_p; CTRL_RND && - (('sd1 + rnd_cnt_reg) >= 'sd9) && - block_init && - (block_sha_mode == 'sd1) + (('sd1 + p) >= 'sd9) && + init_cmd && + (SHA_Mode_in == 'sd1) |-> - ##1 (block_in_ready == 0) and - ##1 (digest_valid == 0) and + ##1 (SHA_Input_notify == 0) and + ##1 (out_notify == 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) && + H == $past(H_2_i, 1) && + W == $past(W_1_i, 1) && + a == $past(a_2_i, 1) && + b == $past(b_1_i, 1) && + c == $past(c_1_i, 1) && + d == $past(d_1_i, 1) && + e == $past(e_1_i, 1) && + f == $past(f_1_i, 1) && + g == $past(g_1_i, 1) && + h == $past(h_1_i, 1) && i == 'sd0 && - rnd_cnt_reg == ('sd1 + $past(rnd_cnt_reg, 1)) && - rh_masking_rnd == $past(rh_masking_rnd_1, 1); + masking_rnd == $past(masking_rnd_1_i, 1) && + p == ('sd1 + $past(p, 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_to_SHA_Rounds_2_a: assert property (disable iff(!rst) CTRL_RND_to_SHA_Rounds_2_p); +property CTRL_RND_to_SHA_Rounds_2_p; CTRL_RND && - (('sd1 + rnd_cnt_reg) >= 'sd9) && - block_init && - (block_sha_mode == 'sd3) + (('sd1 + p) >= 'sd9) && + init_cmd && + (SHA_Mode_in == 'sd3) |-> - ##1 (block_in_ready == 0) and - ##1 (digest_valid == 0) and + ##1 (SHA_Input_notify == 0) and + ##1 (out_notify == 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) && + H == $past(H_3_i, 1) && + W == $past(W_1_i, 1) && + a == $past(a_3_i, 1) && + b == $past(b_2_i, 1) && + c == $past(c_2_i, 1) && + d == $past(d_2_i, 1) && + e == $past(e_2_i, 1) && + f == $past(f_2_i, 1) && + g == $past(g_2_i, 1) && + h == $past(h_2_i, 1) && i == 'sd0 && - rnd_cnt_reg == ('sd1 + $past(rnd_cnt_reg, 1)) && - rh_masking_rnd == $past(rh_masking_rnd_1, 1); + masking_rnd == $past(masking_rnd_1_i, 1) && + p == ('sd1 + $past(p, 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_to_SHA_Rounds_3_a: assert property (disable iff(!rst) CTRL_RND_to_SHA_Rounds_3_p); +property CTRL_RND_to_SHA_Rounds_3_p; CTRL_RND && - (('sd1 + rnd_cnt_reg) >= 'sd9) && - block_init && - (block_sha_mode != 'sd0) && - (block_sha_mode != 'sd1) && - (block_sha_mode != 'sd3) + (('sd1 + p) >= 'sd9) && + init_cmd && + (SHA_Mode_in != 'sd0) && + (SHA_Mode_in != 'sd1) && + (SHA_Mode_in != 'sd3) |-> - ##1 (block_in_ready == 0) and - ##1 (digest_valid == 0) and + ##1 (SHA_Input_notify == 0) and + ##1 (out_notify == 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) && + H == $past(H_4_i, 1) && + W == $past(W_1_i, 1) && + a == $past(a_4_i, 1) && + b == $past(b_3_i, 1) && + c == $past(c_3_i, 1) && + d == $past(d_3_i, 1) && + e == $past(e_3_i, 1) && + f == $past(f_3_i, 1) && + g == $past(g_3_i, 1) && + h == $past(h_3_i, 1) && i == 'sd0 && - rnd_cnt_reg == ('sd1 + $past(rnd_cnt_reg, 1)) && - rh_masking_rnd == $past(rh_masking_rnd_1, 1); + masking_rnd == $past(masking_rnd_1_i, 1) && + p == ('sd1 + $past(p, 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_to_SHA_Rounds_4_a: assert property (disable iff(!rst) CTRL_RND_to_SHA_Rounds_4_p); +property CTRL_RND_to_SHA_Rounds_4_p; CTRL_RND && - (('sd1 + rnd_cnt_reg) >= 'sd9) && - !block_init + (('sd1 + p) >= 'sd9) && + !init_cmd |-> - ##1 (block_in_ready == 0) and - ##1 (digest_valid == 0) and + ##1 (SHA_Input_notify == 0) and + ##1 (out_notify == 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) && + W == $past(W_1_i, 1) && + a == $past(a_5_i, 1) && + b == $past(b_4_i, 1) && + c == $past(c_4_i, 1) && + d == $past(d_4_i, 1) && + e == $past(e_4_i, 1) && + f == $past(f_4_i, 1) && + g == $past(g_4_i, 1) && + h == $past(h_4_i, 1) && i == 'sd0 && - rnd_cnt_reg == ('sd1 + $past(rnd_cnt_reg, 1)) && - rh_masking_rnd == $past(rh_masking_rnd_1, 1); + masking_rnd == $past(masking_rnd_1_i, 1) && + p == ('sd1 + $past(p, 1)); endproperty @@ -633,7 +739,7 @@ property DONE_to_IDLE_p; |-> ##1 IDLE && - H == $past(H_5, 1) && + H == $past(H_5_i, 1) && W == $past(W, 1) && a == $past(a, 1) && b == $past(b, 1) && @@ -644,21 +750,21 @@ property DONE_to_IDLE_p; 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; + masking_rnd == $past(masking_rnd, 1) && + out == 512'(((512'(((512'(((512'(((512'(((512'(((512'(((512'((($past(H['sd7], 1) + ($past(h.masked, 1) ^ $past(h.random, 1))) << 64'd448)) >> 512'd64) + (($past(H['sd6], 1) + ($past(g.masked, 1) ^ $past(g.random, 1))) << 64'd448))) >> 512'd64) + (($past(H['sd5], 1) + ($past(f.masked, 1) ^ $past(f.random, 1))) << 64'd448))) >> 512'd64) + (($past(H['sd4], 1) + ($past(e.masked, 1) ^ $past(e.random, 1))) << 64'd448))) >> 512'd64) + (($past(H['sd3], 1) + ($past(d.masked, 1) ^ $past(d.random, 1))) << 64'd448))) >> 512'd64) + (($past(H['sd2], 1) + ($past(c.masked, 1) ^ $past(c.random, 1))) << 64'd448))) >> 512'd64) + (($past(H['sd1], 1) + ($past(b.masked, 1) ^ $past(b.random, 1))) << 64'd448))) >> 512'd64) + (($past(H[64'd0], 1) + ($past(a.masked, 1) ^ $past(a.random, 1))) << 64'd448))) && + p == $past(p, 1) && + SHA_Input_notify == 1 && + out_notify == 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 + SHA_Input_sync |-> - ##1 (block_in_ready == 0) and - ##1 (digest_valid == 0) and + ##1 (SHA_Input_notify == 0) and + ##1 (out_notify == 0) and ##1 CTRL_RND && H == $past(H, 1) && @@ -672,8 +778,8 @@ property IDLE_to_CTRL_RND_p; g == $past(g, 1) && h == $past(h, 1) && i == $past(i, 1) && - rnd_cnt_reg == 'sd0 && - rh_masking_rnd == $past(rh_masking_rnd, 1); + masking_rnd == $past(masking_rnd, 1) && + p == 'sd0; endproperty @@ -683,82 +789,81 @@ property SHA_Rounds_to_DONE_p; (i >= 'sd16) && (('sd1 + i) >= 'sd80) |-> - ##1 (block_in_ready == 0) and - ##1 (digest_valid == 0) and + ##1 (SHA_Input_notify == 0) and + ##1 (out_notify == 0) and ##1 DONE && H == $past(H, 1) && - W == $past(W_2, 1) && - a == $past(a_7, 1) && + W == $past(W_2_i, 1) && + a == $past(a_7_i, 1) && b == $past(a, 1) && c == $past(b, 1) && d == $past(c, 1) && - e == $past(e_6, 1) && + e == $past(e_6_i, 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); + masking_rnd == $past(masking_rnd, 1) && + p == $past(p, 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_to_SHA_Rounds_a: assert property (disable iff(!rst) SHA_Rounds_to_SHA_Rounds_p); +property SHA_Rounds_to_SHA_Rounds_p; SHA_Rounds && - (i < 'sd16) && - (('sd1 + i) < 'sd80) + (i < 'sd16) |-> - ##1 (block_in_ready == 0) and - ##1 (digest_valid == 0) and + ##1 (SHA_Input_notify == 0) and + ##1 (out_notify == 0) and ##1 SHA_Rounds && H == $past(H, 1) && W == $past(W, 1) && - a == $past(a_6, 1) && + a == $past(a_6_i, 1) && b == $past(a, 1) && c == $past(b, 1) && d == $past(c, 1) && - e == $past(e_5, 1) && + e == $past(e_5_i, 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); + masking_rnd == $past(masking_rnd, 1) && + p == $past(p, 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_to_SHA_Rounds_1_a: assert property (disable iff(!rst) SHA_Rounds_to_SHA_Rounds_1_p); +property SHA_Rounds_to_SHA_Rounds_1_p; SHA_Rounds && (i >= 'sd16) && (('sd1 + i) < 'sd80) |-> - ##1 (block_in_ready == 0) and - ##1 (digest_valid == 0) and + ##1 (SHA_Input_notify == 0) and + ##1 (out_notify == 0) and ##1 SHA_Rounds && H == $past(H, 1) && - W == $past(W_2, 1) && - a == $past(a_7, 1) && + W == $past(W_2_i, 1) && + a == $past(a_7_i, 1) && b == $past(a, 1) && c == $past(b, 1) && d == $past(c, 1) && - e == $past(e_6, 1) && + e == $past(e_6_i, 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); + masking_rnd == $past(masking_rnd, 1) && + p == $past(p, 1); endproperty IDLE_wait_a: assert property (disable iff(!rst) IDLE_wait_p); property IDLE_wait_p; IDLE && - !block_in_valid + !SHA_Input_sync |-> ##1 IDLE && @@ -773,28 +878,29 @@ property IDLE_wait_p; 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); + masking_rnd == $past(masking_rnd, 1) && + p == $past(p, 1) && + SHA_Input_notify == 1 && + out_notify == 0; endproperty endmodule -module fv_SHA512_masked_wrapper_m; +module fv_sha512_masked_core_wrap_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) +st_SHA_Args SHA_Input = '{ + in: (sha512_masked_core.block_msg), + entropy: (sha512_masked_core.entropy), + 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), @@ -806,23 +912,79 @@ a_sc_big_unsigned_64_8 H = '{ 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_SHA_Args SHA_in = '{ + in: (sha512_masked_core.block_msg), + entropy: (sha512_masked_core.entropy), + 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_st_masked_reg_t_16 W = '{ + 0: '{ + masked: (sha512_masked_core.w_mem_inst.w_mem[00].masked), + random: (sha512_masked_core.w_mem_inst.w_mem[00].random) + }, + 1: '{ + masked: (sha512_masked_core.w_mem_inst.w_mem[01].masked), + random: (sha512_masked_core.w_mem_inst.w_mem[01].random) + }, + 2: '{ + masked: (sha512_masked_core.w_mem_inst.w_mem[2].masked), + random: (sha512_masked_core.w_mem_inst.w_mem[2].random) + }, + 3: '{ + masked: (sha512_masked_core.w_mem_inst.w_mem[3].masked), + random: (sha512_masked_core.w_mem_inst.w_mem[3].random) + }, + 4: '{ + masked: (sha512_masked_core.w_mem_inst.w_mem[4].masked), + random: (sha512_masked_core.w_mem_inst.w_mem[4].random) + }, + 5: '{ + masked: (sha512_masked_core.w_mem_inst.w_mem[5].masked), + random: (sha512_masked_core.w_mem_inst.w_mem[5].random) + }, + 6: '{ + masked: (sha512_masked_core.w_mem_inst.w_mem[6].masked), + random: (sha512_masked_core.w_mem_inst.w_mem[6].random) + }, + 7: '{ + masked: (sha512_masked_core.w_mem_inst.w_mem[7].masked), + random: (sha512_masked_core.w_mem_inst.w_mem[7].random) + }, + 8: '{ + masked: (sha512_masked_core.w_mem_inst.w_mem[8].masked), + random: (sha512_masked_core.w_mem_inst.w_mem[8].random) + }, + 9: '{ + masked: (sha512_masked_core.w_mem_inst.w_mem[9].masked), + random: (sha512_masked_core.w_mem_inst.w_mem[9].random) + }, + 10: '{ + masked: (sha512_masked_core.w_mem_inst.w_mem[10].masked), + random: (sha512_masked_core.w_mem_inst.w_mem[10].random) + }, + 11: '{ + masked: (sha512_masked_core.w_mem_inst.w_mem[11].masked), + random: (sha512_masked_core.w_mem_inst.w_mem[11].random) + }, + 12: '{ + masked: (sha512_masked_core.w_mem_inst.w_mem[12].masked), + random: (sha512_masked_core.w_mem_inst.w_mem[12].random) + }, + 13: '{ + masked: (sha512_masked_core.w_mem_inst.w_mem[13].masked), + random: (sha512_masked_core.w_mem_inst.w_mem[13].random) + }, + 14: '{ + masked: (sha512_masked_core.w_mem_inst.w_mem[14].masked), + random: (sha512_masked_core.w_mem_inst.w_mem[14].random) + }, + 15: '{ + masked: (sha512_masked_core.w_mem_inst.w_mem[15].masked), + random: (sha512_masked_core.w_mem_inst.w_mem[15].random) + } }; st_masked_reg_t a = '{ masked: (sha512_masked_core.a_reg.masked), @@ -856,39 +1018,50 @@ 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( +a_sc_big_unsigned_64_24 masking_rnd = '{ + 0: (sha512_masked_core.masking_rnd[0]), + 1: (sha512_masked_core.masking_rnd[1]), + 2: (sha512_masked_core.masking_rnd[2]), + 3: (sha512_masked_core.masking_rnd[3]), + 4: (sha512_masked_core.masking_rnd[4]), + 5: (sha512_masked_core.masking_rnd[5]), + 6: (sha512_masked_core.masking_rnd[6]), + 7: (sha512_masked_core.masking_rnd[7]), + 8: (sha512_masked_core.masking_rnd[8]), + 9: (sha512_masked_core.masking_rnd[9]), + 10: (sha512_masked_core.masking_rnd[10]), + 11: (sha512_masked_core.masking_rnd[11]), + 12: (sha512_masked_core.masking_rnd[12]), + 13: (sha512_masked_core.masking_rnd[13]), + 14: (sha512_masked_core.masking_rnd[14]), + 15: (sha512_masked_core.masking_rnd[15]), + 16: (sha512_masked_core.masking_rnd[16]), + 17: (sha512_masked_core.masking_rnd[17]), + 18: (sha512_masked_core.masking_rnd[18]), + 19: (sha512_masked_core.masking_rnd[19]), + 20: (sha512_masked_core.masking_rnd[20]), + 21: (sha512_masked_core.masking_rnd[21]), + 22: (sha512_masked_core.masking_rnd[22]), + 23: (sha512_masked_core.masking_rnd[23]) +}; + + +fv_sha512_masked_core_m fv_sha512_masked_core( .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), + // Ports + .SHA_Input_sync(((sha512_masked_core.init_cmd) || (sha512_masked_core.next_cmd))), + .SHA_Input_notify(sha512_masked_core.ready), + .SHA_Input(SHA_Input), - // Ready signals - .block_in_ready(sha512_masked_core.ready), + .out_notify((sha512_masked_core.digest_valid) && ((sha512_masked_core.sha512_ctrl_reg==2'h0) && $past(sha512_masked_core.sha512_ctrl_reg==2'h3) )), + .out(sha512_masked_core.digest), // Registers .H(H), - .block_sha_mode(sha512_masked_core.mode), + .SHA_Mode_in(sha512_masked_core.mode), + .SHA_in(SHA_in), .W(W), .a(a), .b(b), @@ -900,10 +1073,9 @@ fv_sha512_masked_m fv_sha512_masked( .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), + .init_cmd(sha512_masked_core.init_reg), + .masking_rnd(masking_rnd), + .p(sha512_masked_core.rnd_ctr_reg), // States .IDLE(sha512_masked_core.sha512_ctrl_reg==2'h0), @@ -916,4 +1088,4 @@ fv_sha512_masked_m fv_sha512_masked( endmodule -bind sha512_masked_core fv_SHA512_masked_wrapper_m fv_SHA512_masked_wrapper(); +bind sha512_masked_core fv_sha512_masked_core_wrap_m fv_sha512_masked_core_wrap(); diff --git a/src/sha512_masked/formal/properties/fv_sha512_masked_pkg.sv b/src/sha512_masked/formal/properties/fv_sha512_masked_pkg.sv index 9479c5ebc..048a7e857 100644 --- a/src/sha512_masked/formal/properties/fv_sha512_masked_pkg.sv +++ b/src/sha512_masked/formal/properties/fv_sha512_masked_pkg.sv @@ -16,30 +16,36 @@ // See the License for the specific language governing permissions and // limitations under the License. // - -package sha512_masked_pkg; + +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; + logic unsigned [1023:0] in; + logic unsigned [191:0] entropy; + logic signed [31:0] SHA_Mode; + logic init_cmd; + logic next_cmd; + logic zeroize; } st_SHA_Args; typedef struct { - bit unsigned [63:0] masked; - bit unsigned [63:0] random; + logic unsigned [63:0] masked; + logic unsigned [63:0] random; } st_masked_reg_t; -typedef bit a_bool_10 [9:0]; +typedef logic a_bool_10 [9:0]; + +typedef logic unsigned [63:0] a_sc_big_unsigned_64_16 [15:0]; -typedef bit unsigned [63:0] a_sc_big_unsigned_64_16 [15:0]; +typedef logic unsigned [63:0] a_sc_big_unsigned_64_23 [22:0]; +typedef logic unsigned [63:0] a_sc_big_unsigned_64_24 [23:0]; -typedef bit unsigned [63:0] a_sc_big_unsigned_64_8 [7:0]; +typedef logic unsigned [63:0] a_sc_big_unsigned_64_8 [7:0]; -typedef bit unsigned [63:0] a_sc_big_unsigned_64_80 [79:0]; +typedef logic unsigned [63:0] a_sc_big_unsigned_64_80 [79:0]; + +typedef st_masked_reg_t a_st_masked_reg_t_16 [15:0]; // Constants @@ -49,6 +55,15 @@ parameter a_sc_big_unsigned_64_80 K = '{ 0: 64'h428A2F98D728AE22, 1: 64'h7137449 // Functions +/* function logic unsigned [63:0] A2B_conv(logic unsigned [63:0] x_masked, logic unsigned [63:0] x_random, logic q, logic masked_carry, logic unsigned [127:0] x_m, logic unsigned [63:0] mask, logic signed [31:0] j); + return 64'((((x_masked & 64'h1) << 128'd64) >> 128'd1)); +endfunction + +function logic unsigned [63:0] B2A_conv(logic unsigned [63:0] x_masked, logic unsigned [63:0] x_random, logic q, logic masked_carry, logic unsigned [127:0] x_prime, logic unsigned [63:0] mask, logic signed [31:0] j); + return 64'd0; +endfunction */ + + 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; @@ -81,117 +96,315 @@ reg [63 : 0] masked_carry; 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))); + +function logic unsigned [63:0] T1_m(logic unsigned [63:0] e_masked, logic unsigned [63:0] e_random, logic unsigned [63:0] f_masked, logic unsigned [63:0] f_random, logic unsigned [63:0] g_masked, logic unsigned [63:0] g_random, logic unsigned [63:0] h_masked, logic unsigned [63:0] h_random, logic unsigned [63:0] k, logic unsigned [63:0] w_masked, logic unsigned [63:0] w_random, logic masked_carry, logic unsigned [127:0] x_prime, logic unsigned [63:0] mask, logic q_masking_rnd_0, logic q_masking_rnd_1, logic q_masking_rnd_2, logic q_masking_rnd_3, logic q_masking_rnd_4, logic signed [31:0] j); + logic unsigned [63:0] B2A_conv_0_i; + logic unsigned [63:0] sigma1_0_i; + logic unsigned [63:0] sigma1_1_i; + logic unsigned [63:0] B2A_conv_1_i; + logic unsigned [63:0] masked_Ch_m_0_i; + logic unsigned [63:0] B2A_conv_2_i; + logic unsigned [63:0] B2A_conv_3_i; + logic unsigned [63:0] B2A_conv_4_i; + B2A_conv_0_i = B2A_conv(h_masked, h_random, q_masking_rnd_0, masked_carry, x_prime, mask, j); + + sigma1_0_i = sigma1(e_masked); + + sigma1_1_i = sigma1(e_random); + + B2A_conv_1_i = B2A_conv(sigma1_0_i, sigma1_1_i, q_masking_rnd_1, masked_carry, x_prime, mask, j); + + masked_Ch_m_0_i = masked_Ch_m(e_masked, e_random, f_masked, f_random, g_masked, g_random); + + B2A_conv_2_i = B2A_conv(masked_Ch_m_0_i, (e_random ^ g_random), q_masking_rnd_2, masked_carry, x_prime, mask, j); + + B2A_conv_3_i = B2A_conv(k, 64'h0, q_masking_rnd_3, masked_carry, x_prime, mask, j); + + B2A_conv_4_i = B2A_conv(w_masked, w_random, q_masking_rnd_4, masked_carry, x_prime, mask, j); + + return 64'(((((B2A_conv_0_i + B2A_conv_1_i) + B2A_conv_2_i) + B2A_conv_3_i) + B2A_conv_4_i)); 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)); +function logic unsigned [63:0] T1_r(logic unsigned [63:0] e_random, logic unsigned [63:0] g_random, logic unsigned [63:0] h_random, logic unsigned [63:0] w_random); + logic unsigned [63:0] sigma1_0_i; + sigma1_0_i = sigma1(e_random); + + return 64'((((h_random + sigma1_0_i) + (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))); +function logic unsigned [63:0] T2_m(logic unsigned [63:0] a_masked, logic unsigned [63:0] a_random, logic unsigned [63:0] b_masked, logic unsigned [63:0] b_random, logic unsigned [63:0] c_masked, logic unsigned [63:0] c_random, logic masked_carry, logic unsigned [127:0] x_prime, logic unsigned [63:0] mask, logic q_masking_rnd_5, logic q_masking_rnd_6, logic signed [31:0] j); + logic unsigned [63:0] sigma0_0_i; + logic unsigned [63:0] sigma0_1_i; + logic unsigned [63:0] B2A_conv_0_i; + logic unsigned [63:0] masked_Maj_0_i; + logic unsigned [63:0] B2A_conv_1_i; + sigma0_0_i = sigma0(a_masked); + + sigma0_1_i = sigma0(a_random); + + B2A_conv_0_i = B2A_conv(sigma0_0_i, sigma0_1_i, q_masking_rnd_5, masked_carry, x_prime, mask, j); + + masked_Maj_0_i = masked_Maj(a_masked, a_random, b_masked, b_random, c_masked, c_random); + + B2A_conv_1_i = B2A_conv(masked_Maj_0_i, b_random, q_masking_rnd_6, masked_carry, x_prime, mask, j); + + return 64'((B2A_conv_0_i + B2A_conv_1_i)); 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)); +function logic unsigned [63:0] T2_r(logic unsigned [63:0] a_random, logic unsigned [63:0] b_random); + logic unsigned [63:0] sigma0_0_i; + sigma0_0_i = sigma0(a_random); + + return 64'((sigma0_0_i + b_random)); +endfunction + +function logic unsigned [63:0] compute_w_masked(st_masked_reg_t w14, st_masked_reg_t w9, st_masked_reg_t w1, st_masked_reg_t w0, logic unsigned [191:0] ent, logic masked_carry, logic unsigned [127:0] x_prime, logic unsigned [63:0] mask, logic signed [31:0] j, logic unsigned [63:0] m_rand); + logic ent_shift_0_i; + logic unsigned [63:0] B2A_conv_0_i; + logic unsigned [63:0] delta0_0_i; + logic unsigned [63:0] delta0_1_i; + logic ent_shift_1_i; + logic unsigned [63:0] B2A_conv_1_i; + logic ent_shift_2_i; + logic unsigned [63:0] B2A_conv_2_i; + logic unsigned [63:0] delta1_0_i; + logic unsigned [63:0] delta1_1_i; + logic ent_shift_3_i; + logic unsigned [63:0] B2A_conv_3_i; + logic unsigned [63:0] masked_sum_0_i; + logic unsigned [63:0] masked_sum_1_i; + logic unsigned [63:0] masked_sum_2_i; + logic ent_shift_4_i; + logic unsigned [63:0] A2B_conv_0_i; + + ent_shift_0_i = ent_shift(ent, 192'd1); + + B2A_conv_0_i = B2A_conv(w0.masked, w0.random, ent_shift_0_i, masked_carry, x_prime, mask, j); + + delta0_0_i = delta0(w1.masked); + + delta0_1_i = delta0(w1.random); + + ent_shift_1_i = ent_shift(ent, 192'd2); + + B2A_conv_1_i = B2A_conv(delta0_0_i, delta0_1_i, ent_shift_1_i, masked_carry, x_prime, mask, j); + + ent_shift_2_i = ent_shift(ent, 192'd4); + + B2A_conv_2_i = B2A_conv(w9.masked, w9.random, ent_shift_2_i, masked_carry, x_prime, mask, j); + + delta1_0_i = delta1(w14.masked); + + delta1_1_i = delta1(w14.random); + + ent_shift_3_i = ent_shift(ent, 192'd8); + + B2A_conv_3_i = B2A_conv(delta1_0_i, delta1_1_i, ent_shift_3_i, masked_carry, x_prime, mask, j); + + masked_sum_0_i = masked_sum(B2A_conv_2_i, B2A_conv_3_i); + + masked_sum_1_i = masked_sum(B2A_conv_1_i, masked_sum_0_i); + + masked_sum_2_i = masked_sum(B2A_conv_0_i, masked_sum_1_i); + + ent_shift_4_i = ent_shift(ent, 192'd16); + + A2B_conv_0_i = A2B_conv(masked_sum_2_i, m_rand, ent_shift_4_i, masked_carry, x_prime, mask, j); + + return A2B_conv_0_i; +endfunction + +function logic unsigned [63:0] compute_w_random(logic unsigned [63:0] w14, logic unsigned [63:0] w9, logic unsigned [63:0] w1, logic unsigned [63:0] w0); + logic unsigned [63:0] delta0_0_i; + logic unsigned [63:0] delta1_0_i; + logic unsigned [63:0] masked_sum_0_i; + logic unsigned [63:0] masked_sum_1_i; + logic unsigned [63:0] masked_sum_2_i; + + delta0_0_i = delta0(w1); + + delta1_0_i = delta1(w14); + + masked_sum_0_i = masked_sum(w9, delta1_0_i); + + masked_sum_1_i = masked_sum(delta0_0_i, masked_sum_0_i); + + masked_sum_2_i = masked_sum(w0, masked_sum_1_i); + + return masked_sum_2_i; 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)); +function logic unsigned [63:0] delta0(logic unsigned [63:0] x); + logic unsigned [63:0] rotr1_0_i; + logic unsigned [63:0] rotr8_0_i; + logic unsigned [63:0] shr7_0_i; + rotr1_0_i = rotr1(x); + + rotr8_0_i = rotr8(x); + + shr7_0_i = shr7(x); + + return ((rotr1_0_i ^ rotr8_0_i) ^ shr7_0_i); endfunction -function bit unsigned [63:0] delta0(bit unsigned [63:0] x); - return ((rotr1(x) ^ rotr8(x)) ^ shr7(x)); +function logic unsigned [63:0] delta1(logic unsigned [63:0] x); + logic unsigned [63:0] rotr19_0_i; + logic unsigned [63:0] rotr61_0_i; + logic unsigned [63:0] shr6_0_i; + rotr19_0_i = rotr19(x); + + rotr61_0_i = rotr61(x); + + shr6_0_i = shr6(x); + + return ((rotr19_0_i ^ rotr61_0_i) ^ shr6_0_i); endfunction -function bit unsigned [63:0] delta1(bit unsigned [63:0] x); - return ((rotr19(x) ^ rotr61(x)) ^ shr6(x)); +function logic ent_shift(logic unsigned [191:0] ent, logic unsigned [191:0] i); + return ((ent & i) == i); 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)); +function logic unsigned [63:0] masked_Ch_m(logic unsigned [63:0] e_masked, logic unsigned [63:0] e_random, logic unsigned [63:0] f_masked, logic unsigned [63:0] f_random, logic unsigned [63:0] g_masked, logic unsigned [63:0] g_random); + logic unsigned [63:0] masked_and_0_i; + logic unsigned [63:0] masked_and_1_i; + masked_and_0_i = masked_and(e_masked, e_random, f_masked, f_random); + + masked_and_1_i = masked_and(g_masked, g_random, ~e_masked, e_random); + + return (masked_and_0_i ^ masked_and_1_i); 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)); +function logic unsigned [63:0] masked_Maj(logic unsigned [63:0] a_masked, logic unsigned [63:0] a_random, logic unsigned [63:0] b_masked, logic unsigned [63:0] b_random, logic unsigned [63:0] c_masked, logic unsigned [63:0] c_random); + logic unsigned [63:0] masked_and_0_i; + logic unsigned [63:0] masked_and_1_i; + logic unsigned [63:0] masked_and_2_i; + masked_and_0_i = masked_and(a_masked, a_random, b_masked, b_random); + + masked_and_1_i = masked_and(a_masked, a_random, c_masked, c_random); + + masked_and_2_i = masked_and(b_masked, b_random, c_masked, c_random); + + return ((masked_and_0_i ^ masked_and_1_i) ^ masked_and_2_i); 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); +function logic unsigned [63:0] masked_and(logic unsigned [63:0] x_masked, logic unsigned [63:0] x_random, logic unsigned [63:0] y_masked, logic 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); +function logic unsigned [63:0] masked_sum(logic unsigned [63:0] x, logic unsigned [63:0] y); + return 64'((x + y)); +endfunction + +function logic unsigned [63:0] rotr1(logic unsigned [63:0] n); return 64'(((n >> 64'd1) | (n << 64'd63))); endfunction -function bit unsigned [63:0] rotr14(bit unsigned [63:0] n); +function logic unsigned [63:0] rotr14(logic unsigned [63:0] n); return 64'(((n >> 64'd14) | (n << 64'd50))); endfunction -function bit unsigned [63:0] rotr18(bit unsigned [63:0] n); +function logic unsigned [63:0] rotr18(logic unsigned [63:0] n); return 64'(((n >> 64'd18) | (n << 64'd46))); endfunction -function bit unsigned [63:0] rotr19(bit unsigned [63:0] n); +function logic unsigned [63:0] rotr19(logic unsigned [63:0] n); return 64'(((n >> 64'd19) | (n << 64'd45))); endfunction -function bit unsigned [63:0] rotr28(bit unsigned [63:0] n); +function logic unsigned [63:0] rotr28(logic unsigned [63:0] n); return 64'(((n >> 64'd28) | (n << 64'd36))); endfunction -function bit unsigned [63:0] rotr34(bit unsigned [63:0] n); +function logic unsigned [63:0] rotr34(logic unsigned [63:0] n); return 64'(((n >> 64'd34) | (n << 64'd30))); endfunction -function bit unsigned [63:0] rotr39(bit unsigned [63:0] n); +function logic unsigned [63:0] rotr39(logic unsigned [63:0] n); return 64'(((n >> 64'd39) | (n << 64'd25))); endfunction -function bit unsigned [63:0] rotr41(bit unsigned [63:0] n); +function logic unsigned [63:0] rotr41(logic unsigned [63:0] n); return 64'(((n >> 64'd41) | (n << 64'd23))); endfunction -function bit unsigned [63:0] rotr61(bit unsigned [63:0] n); +function logic unsigned [63:0] rotr61(logic unsigned [63:0] n); return 64'(((n >> 64'd61) | (n << 64'd3))); endfunction -function bit unsigned [63:0] rotr8(bit unsigned [63:0] n); +function logic unsigned [63:0] rotr8(logic unsigned [63:0] n); return 64'(((n >> 64'd8) | (n << 64'd56))); endfunction -function bit unsigned [63:0] shr6(bit unsigned [63:0] n); +function logic unsigned [63:0] shr6(logic unsigned [63:0] n); return (n >> 64'd6); endfunction -function bit unsigned [63:0] shr7(bit unsigned [63:0] n); +function logic unsigned [63:0] shr7(logic 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)); +function logic unsigned [63:0] sigma0(logic unsigned [63:0] x); + logic unsigned [63:0] rotr28_0_i; + logic unsigned [63:0] rotr34_0_i; + logic unsigned [63:0] rotr39_0_i; + rotr28_0_i = rotr28(x); + + rotr34_0_i = rotr34(x); + + rotr39_0_i = rotr39(x); + + return ((rotr28_0_i ^ rotr34_0_i) ^ rotr39_0_i); endfunction -function bit unsigned [63:0] sigma1(bit unsigned [63:0] x); - return ((rotr14(x) ^ rotr18(x)) ^ rotr41(x)); +function logic unsigned [63:0] sigma1(logic unsigned [63:0] x); + logic unsigned [63:0] rotr14_0_i; + logic unsigned [63:0] rotr18_0_i; + logic unsigned [63:0] rotr41_0_i; + rotr14_0_i = rotr14(x); + + rotr18_0_i = rotr18(x); + + rotr41_0_i = rotr41(x); + + return ((rotr14_0_i ^ rotr18_0_i) ^ rotr41_0_i); endfunction -function bit unsigned [63:0] slicer(bit unsigned [1023:0] block, bit signed [31:0] index); - return(block[(64*index)+:64]); +function logic unsigned [63:0] slicer(logic unsigned [1023:0] block, logic signed [31:0] index); + if ((index == 'sd0)) + return 64'((block >> 1024'd0)); + else if ((index == 'sd1)) + return 64'((block >> 1024'd64)); + else if ((index == 'sd2)) + return 64'((block >> 1024'd128)); + else if ((index == 'sd3)) + return 64'((block >> 1024'd192)); + else if ((index == 'sd4)) + return 64'((block >> 1024'd256)); + else if ((index == 'sd5)) + return 64'((block >> 1024'd320)); + else if ((index == 'sd6)) + return 64'((block >> 1024'd384)); + else if ((index == 'sd7)) + return 64'((block >> 1024'd448)); + else if ((index == 'sd8)) + return 64'((block >> 1024'd512)); + else if ((index == 'sd9)) + return 64'((block >> 1024'd576)); + else if ((index == 'sd10)) + return 64'((block >> 1024'd640)); + else if ((index == 'sd11)) + return 64'((block >> 1024'd704)); + else if ((index == 'sd12)) + return 64'((block >> 1024'd768)); + else if ((index == 'sd13)) + return 64'((block >> 1024'd832)); + else if ((index == 'sd14)) + return 64'((block >> 1024'd896)); + else if ((index == 'sd15)) + return 64'((block >> 1024'd960)); + else + return 64'((block >> 1024'd960)); 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 index 0a23239e2..f56bd25cc 100644 --- a/src/sha512_masked/formal/readme.md +++ b/src/sha512_masked/formal/readme.md @@ -1,11 +1,12 @@ # 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** +- model: Contains the high level abstracted model +- properties: Contains the assertion IP(AIP) named as **fv_sha512_masked.sv**,**fv_sha512_masked_pkg.sv**, **fv_coverpoints.sv** and the constraints in place for the respective AIP **fv_constraints.sv** ## DUT Overview @@ -21,7 +22,7 @@ The DUT sha512_core has the primary inputs and primary outputs as shown below. | 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 | +| 8 | entropy[191:0] | input | random bit vectors | | 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 | @@ -39,26 +40,26 @@ The Assertion IP signals are bound with the respective signals in the dut, where - 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_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_1_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_2_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_3_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. +- CTRL_RND_to_SHA_Rounds_4_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_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. +- SHA_Rounds_to_SHA_Rounds_1_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. +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.