diff --git a/src/doe/formal/properties/fv_constraints.sv b/src/doe/formal/properties/fv_constraints.sv new file mode 100644 index 000000000..b83fa4f52 --- /dev/null +++ b/src/doe/formal/properties/fv_constraints.sv @@ -0,0 +1,206 @@ +// ------------------------------------------------- +// Contact: contact@lubis-eda.com +// Author: Tobias Ludwig, Michael Schwarz +// ------------------------------------------------- +// SPDX-License-Identifier: Apache-2.0 +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// + +module fv_constraints_m( + + //////////////////////////// + // Input / Output signals // + //////////////////////////// + // Clock and reset. + input clk, + input reset_n, + + input encdec, + input init_cmd, + input next_cmd, + input ready, + input IV_updated, + input keylen, + input [255:0] key, + input [127:0] block_msg, + input [127:0] IV +); + +logic init_reg, iv_updated_reg, next_cmd_reg; +logic keyexp_start,keyexp_done; +logic iv_start, iv_done; + +//////////////////////// +// Default Clock // +//////////////////////// + +default clocking default_clk @(posedge clk); endclocking + + +//////////////////////// +// Helper Logic // +//////////////////////// + +//keyexpansion helper logic +always @ (posedge clk or negedge reset_n) + begin : key_expansion + if (!reset_n) begin + keyexp_start <= 1'b0; + keyexp_done <= 1'b0; + end + else if (init_cmd) begin + keyexp_start <= 1'b1; + keyexp_done <= 1'b0; + end + else if (keyexp_start && doe_core_cbc.key_ready) begin + keyexp_start <= 1'b0; + keyexp_done <= 1'b1; + end + else if (keyexp_done && init_cmd) begin + keyexp_start <= 1'b1; + keyexp_done <= 1'b0; + end + end + +//IV helper logic +always @ (posedge clk or negedge reset_n) + begin : iv_control + if (!reset_n) begin + iv_start <= 1'b0; + iv_done <= 1'b0; + end + else if (keyexp_done && IV_updated) begin + iv_start <= 1'b1; + iv_done <= 1'b0; + end + else if (iv_start && next_cmd) begin + iv_start <= 1'b0; + iv_done <= 1'b1; + end + else if (iv_done && init_cmd) begin + iv_start <= 1'b0; + iv_done <= 1'b0; + end + end + + +//////////////////////////////////// +// CBC Constraint Properties // +/////////////////////////////////// + +//init_cmd, next_cmd and IV_updated can be only received if the doe_core_cbc is ready +cmd_on_ready_a: assume property (disable iff(!reset_n) cmd_on_ready_p); +property cmd_on_ready_p; + !ready +|-> + !init_cmd && !next_cmd && !IV_updated +;endproperty + +//next_cmd can only be received once there is an IV_updated before +next_cmd_order_a: assume property (disable iff(!reset_n) next_cmd_order_p); +property next_cmd_order_p; + !iv_start +|=> + !next_cmd || iv_done +;endproperty + +//next_cmd can only be received once the keyexpansion is done +next_cmd_keyexp_order_a: assume property (disable iff(!reset_n) next_cmd_keyexp_order_p); +property next_cmd_keyexp_order_p; + !keyexp_done +|-> + !next_cmd +;endproperty + +//IV_updated can only be received once there is an IV_updated before +IV_updated_order_a: assume property (disable iff(!reset_n) IV_updated_order_p); +property IV_updated_order_p; + iv_done +|-> + !IV_updated +;endproperty + +//IV_updated is a pulse +iv_updated_pulse_a: assume property (disable iff(!reset_n) iv_updated_pulse_p); +property iv_updated_pulse_p; + IV_updated |=> !IV_updated +;endproperty + +//init_cmd and next_cmd doesn't come together +init_next_a: assume property (disable iff(!reset_n) init_next_p); +property init_next_p; + !(init_cmd && next_cmd) +;endproperty + +//init_cmd and IV_updated doesn't come together +init_iv_a: assume property (disable iff(!reset_n) init_iv_p); +property init_iv_p; + !(init_cmd && IV_updated) +;endproperty + +//IV_updated and next_cmd doesn't come together +next_iv_a: assume property (disable iff(!reset_n) next_iv_p); +property next_iv_p; + !(next_cmd && IV_updated) +;endproperty + +//keylen is stable until there is a new init_cmd +stable_keylen_a: assume property (disable iff(!reset_n) keylen_stable); +property keylen_stable; + $stable(keylen) || init_cmd +;endproperty + +//key is stable until there is a new init_cmd +key_stable_during_expansion_a: assume property (disable iff(!reset_n) key_stable_during_expansion); +property key_stable_during_expansion; + $stable(key) || init_cmd +;endproperty + +//encdec is stable until there is a new next_cmd +encdec_during_operation_a: assume property (disable iff(!reset_n) encdec_during_operation_p); +property encdec_during_operation_p; + $stable(encdec) || next_cmd +;endproperty + +//block message is stable until doe_core_cbc is ready +blkmsg_during_operation_a: assume property (disable iff(!reset_n) blkmsg_during_operation_p); +property blkmsg_during_operation_p; + $stable(block_msg) || ready +;endproperty + +//IV has stable until encrypted block_msg sent to enc_block +iv_during_operation_a: assume property (disable iff(!reset_n) iv_during_operation_p); +property iv_during_operation_p; + ready || !iv_done + |-> + $stable(IV) +;endproperty + +endmodule + +//Connect this constraints module with the DUV +bind doe_core_cbc fv_constraints_m fv_constraints( + .clk(clk), + .reset_n(reset_n && !zeroize), + .encdec(encdec), + .init_cmd(init_cmd), + .next_cmd(next_cmd), + .ready(ready), + .IV_updated(IV_updated), + .key(key), + .block_msg(block_msg), + .keylen(keylen), + .IV(IV) +); + diff --git a/src/doe/formal/properties/fv_cover_points.sv b/src/doe/formal/properties/fv_cover_points.sv new file mode 100644 index 000000000..192b5d0e2 --- /dev/null +++ b/src/doe/formal/properties/fv_cover_points.sv @@ -0,0 +1,91 @@ +// ------------------------------------------------- +// Contact: contact@lubis-eda.com +// Author: Tobias Ludwig, Michael Schwarz +// ------------------------------------------------- +// SPDX-License-Identifier: Apache-2.0 +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// + +module fv_coverpoints_m( + input logic clk, + input logic reset_n, + input logic zeroize +); + +default clocking default_clk @(posedge clk); endclocking + +//Cover zeroize +cover_zeroize: cover property(disable iff(!reset_n) doe_core_cbc.zeroize ); + +//Assert zeroize input and check the status of all registers. All registers/internal memories should be cleared. +cover_zeroize_after_next: cover property(disable iff(!reset_n ) doe_core_cbc.zeroize && doe_core_cbc.ready && doe_core_cbc.next_cmd ); + +//Cover that checks multiple next_cmd can be received for CBC encryption/decryption. +cover_multiple_next: cover property(disable iff(!reset_n || zeroize) + doe_core_cbc.next_cmd && doe_core_cbc.ready ##1 !doe_core_cbc.init_cmd && doe_core_cbc.next_cmd && doe_core_cbc.ready[->1] +); + +//Cover that checks IV_updated asserted once the keyexapnsion is done +cover_transition_keyexp_to_iv: cover property (disable iff(!reset_n || zeroize) + doe_core_cbc.init_cmd + ##1 + doe_core_cbc.ready[->1] + ##0 + doe_core_cbc.IV_updated[->1] +); + +//Cover transition from keyexpansion to encryption/decryption +cover_transition_keyexp_to_encdec: cover property (disable iff(!reset_n || zeroize) + doe_core_cbc.init_cmd + ##1 + doe_core_cbc.ready[->1] + ##0 + doe_core_cbc.next_cmd[->1] +); + +//Cover transition from keyexpansion to keyexpansion +cover_transition_keyexp_to_keyexp: cover property (disable iff(!reset_n || zeroize) + doe_core_cbc.init_cmd + ##1 + doe_core_cbc.ready[->1] + ##0 + doe_core_cbc.init_cmd[->1] +); + +//Cover transition from encryption/decryption to encryption/decryption +cover_transition_encdec_to_encdec: cover property (disable iff(!reset_n || zeroize) + doe_core_cbc.next_cmd + ##1 + doe_core_cbc.ready[->1] + ##0 + doe_core_cbc.next_cmd[->1] +); + +//Cover transition from encryption/decryption to keyexpansion +cover_transition_encdec_to_keyexp: cover property (disable iff(!reset_n || zeroize) + doe_core_cbc.next_cmd + ##1 + doe_core_cbc.ready[->1] + ##0 + doe_core_cbc.init_cmd[->1] +); + +endmodule + +//Connect this coverpoints module with the DUV +bind doe_core_cbc fv_coverpoints_m fv_coverpoints( + .clk(clk), + .reset_n(reset_n), + .zeroize(zeroize) +); \ No newline at end of file diff --git a/src/doe/formal/properties/fv_doe_core_cbc.sv b/src/doe/formal/properties/fv_doe_core_cbc.sv new file mode 100644 index 000000000..bfbc562a1 --- /dev/null +++ b/src/doe/formal/properties/fv_doe_core_cbc.sv @@ -0,0 +1,161 @@ +// ------------------------------------------------- +// 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 doe_core_cbc_pkg::*; + +module fv_doe_cbc_checker_m( + + //////////////////////////// + // Input / Output signals // + //////////////////////////// + // Clock and reset. + input clk, + input reset_n, + input zeroize, + + input encdec, + input init_cmd, + input next_cmd, + input enc_ready, + input dec_ready, + input key_ready, + input [127:0] enc_new_block, + input [127:0] dec_new_block, + input [127:0] IV_decry, + input ready, + input [127:0] result, + input result_valid, + input [31 : 0] muxed_sboxw, + input [31 : 0] new_sboxw +); + +//////////////////////// +// Default Clock // +//////////////////////// +default clocking default_clk @(posedge clk); endclocking + +//Internal Signals +logic [31:0] fv_sbox; + +//Helper Logic +assign fv_sbox = get_sbox(muxed_sboxw); + +//////////////////////////////////// +// Core CBC Properties // +/////////////////////////////////// + +//Checks if doe_sbox block produces correct values +sbox_check_a: assert property (disable iff(!reset_n) sbox_check_p); +property sbox_check_p; + !ready +|-> + new_sboxw == fv_sbox +;endproperty + +//Checks if block asserts result_valid upon finishing encryption +result_valid_enc_a: assert property (disable iff(!reset_n) result_valid_enc_p); +property result_valid_enc_p; + encdec && + next_cmd + ##1 enc_ready[->1] +|=> + result_valid +;endproperty + +//Checks if block asserts result_valid upon finishing decryption +result_valid_dec_a: assert property (disable iff(!reset_n) result_valid_dec_p); +property result_valid_dec_p; + !encdec && + next_cmd + ##1 dec_ready[->1] +|=> + result_valid +;endproperty + +//Checks if block asserts ready upon finishing key expansion +ready_kemem_a: assert property (disable iff(!reset_n) ready_kemem_p); +property ready_kemem_p; + init_cmd + ##1 key_ready[->1] + |=> + ready +;endproperty + +//Checks if block asserts ready upon finishing encryption +ready_enc_a: assert property (disable iff(!reset_n) ready_enc_p); +property ready_enc_p; + encdec && + next_cmd + ##1 enc_ready[->1] +|=> + ready +;endproperty + +//Checks if block asserts ready upon finishing decryption +ready_dec_a: assert property (disable iff(!reset_n) ready_dec_p); +property ready_dec_p; + !encdec && + next_cmd + ##1 dec_ready[->1] +|=> + ready +;endproperty + +//Checks if block produces result upon finishing encryption +result_enc_a: assert property (disable iff(!reset_n) result_enc_p); +property result_enc_p; + encdec && + next_cmd + ##1 enc_ready[->1] +|-> + result == enc_new_block +;endproperty + +//Checks if block produces result upon finishing decryption +result_dec_a: assert property (disable iff(!reset_n) result_dec_p); +property result_dec_p; + !encdec && + next_cmd + ##1 dec_ready[->1] +|-> + result == dec_new_block +;endproperty + +endmodule + +//Connect this checker module with the DUV +bind doe_core_cbc fv_doe_cbc_checker_m fv_doe_cbc_inst( + .clk(clk), + .reset_n(reset_n && !zeroize), + .encdec(encdec), + .init_cmd(init_cmd), + .next_cmd(next_cmd), + .enc_ready(enc_ready), + .dec_ready(dec_ready), + .key_ready(key_ready), + .IV_decry(IV_decry), + .enc_new_block(enc_new_block), + .dec_new_block(dec_new_block ^ IV_decry), + .ready(ready), + .result(result), + .result_valid(result_valid), + .muxed_sboxw(muxed_sboxw), + .new_sboxw(new_sboxw) +); + diff --git a/src/doe/formal/properties/fv_doe_core_cbc_pkg.sv b/src/doe/formal/properties/fv_doe_core_cbc_pkg.sv new file mode 100644 index 000000000..4ffdddaed --- /dev/null +++ b/src/doe/formal/properties/fv_doe_core_cbc_pkg.sv @@ -0,0 +1,533 @@ +// ------------------------------------------------- +// 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 doe_core_cbc_pkg; + +// AES S-box +parameter [7:0] fv_sbox[0:255] = '{ + 8'h63, 8'h7C, 8'h77, 8'h7B, 8'hF2, 8'h6B, 8'h6F, 8'hC5, 8'h30, 8'h01, 8'h67, 8'h2B, 8'hFE, 8'hD7, 8'hAB, 8'h76, + 8'hCA, 8'h82, 8'hC9, 8'h7D, 8'hFA, 8'h59, 8'h47, 8'hF0, 8'hAD, 8'hD4, 8'hA2, 8'hAF, 8'h9C, 8'hA4, 8'h72, 8'hC0, + 8'hB7, 8'hFD, 8'h93, 8'h26, 8'h36, 8'h3F, 8'hF7, 8'hCC, 8'h34, 8'hA5, 8'hE5, 8'hF1, 8'h71, 8'hD8, 8'h31, 8'h15, + 8'h04, 8'hC7, 8'h23, 8'hC3, 8'h18, 8'h96, 8'h05, 8'h9A, 8'h07, 8'h12, 8'h80, 8'hE2, 8'hEB, 8'h27, 8'hB2, 8'h75, + 8'h09, 8'h83, 8'h2C, 8'h1A, 8'h1B, 8'h6E, 8'h5A, 8'hA0, 8'h52, 8'h3B, 8'hD6, 8'hB3, 8'h29, 8'hE3, 8'h2F, 8'h84, + 8'h53, 8'hD1, 8'h00, 8'hED, 8'h20, 8'hFC, 8'hB1, 8'h5B, 8'h6A, 8'hCB, 8'hBE, 8'h39, 8'h4A, 8'h4C, 8'h58, 8'hCF, + 8'hD0, 8'hEF, 8'hAA, 8'hFB, 8'h43, 8'h4D, 8'h33, 8'h85, 8'h45, 8'hF9, 8'h02, 8'h7F, 8'h50, 8'h3C, 8'h9F, 8'hA8, + 8'h51, 8'hA3, 8'h40, 8'h8F, 8'h92, 8'h9D, 8'h38, 8'hF5, 8'hBC, 8'hB6, 8'hDA, 8'h21, 8'h10, 8'hFF, 8'hF3, 8'hD2, + 8'hCD, 8'h0C, 8'h13, 8'hEC, 8'h5F, 8'h97, 8'h44, 8'h17, 8'hC4, 8'hA7, 8'h7E, 8'h3D, 8'h64, 8'h5D, 8'h19, 8'h73, + 8'h60, 8'h81, 8'h4F, 8'hDC, 8'h22, 8'h2A, 8'h90, 8'h88, 8'h46, 8'hEE, 8'hB8, 8'h14, 8'hDE, 8'h5E, 8'h0B, 8'hDB, + 8'hE0, 8'h32, 8'h3A, 8'h0A, 8'h49, 8'h06, 8'h24, 8'h5C, 8'hC2, 8'hD3, 8'hAC, 8'h62, 8'h91, 8'h95, 8'hE4, 8'h79, + 8'hE7, 8'hC8, 8'h37, 8'h6D, 8'h8D, 8'hD5, 8'h4E, 8'hA9, 8'h6C, 8'h56, 8'hF4, 8'hEA, 8'h65, 8'h7A, 8'hAE, 8'h08, + 8'hBA, 8'h78, 8'h25, 8'h2E, 8'h1C, 8'hA6, 8'hB4, 8'hC6, 8'hE8, 8'hDD, 8'h74, 8'h1F, 8'h4B, 8'hBD, 8'h8B, 8'h8A, + 8'h70, 8'h3E, 8'hB5, 8'h66, 8'h48, 8'h03, 8'hF6, 8'h0E, 8'h61, 8'h35, 8'h57, 8'hB9, 8'h86, 8'hC1, 8'h1D, 8'h9E, + 8'hE1, 8'hF8, 8'h98, 8'h11, 8'h69, 8'hD9, 8'h8E, 8'h94, 8'h9B, 8'h1E, 8'h87, 8'hE9, 8'hCE, 8'h55, 8'h28, 8'hDF, + 8'h8C, 8'hA1, 8'h89, 8'h0D, 8'hBF, 8'hE6, 8'h42, 8'h68, 8'h41, 8'h99, 8'h2D, 8'h0F, 8'hB0, 8'h54, 8'hBB, 8'h16 +}; + +// AES Inverse S-box +parameter [7:0] fv_inv_sbox[0:255] = '{ + 8'h52, 8'h09, 8'h6A, 8'hD5, 8'h30, 8'h36, 8'hA5, 8'h38, 8'hBF, 8'h40, 8'hA3, 8'h9E, 8'h81, 8'hF3, 8'hD7, 8'hFB, + 8'h7C, 8'hE3, 8'h39, 8'h82, 8'h9B, 8'h2F, 8'hFF, 8'h87, 8'h34, 8'h8E, 8'h43, 8'h44, 8'hC4, 8'hDE, 8'hE9, 8'hCB, + 8'h54, 8'h7B, 8'h94, 8'h32, 8'hA6, 8'hC2, 8'h23, 8'h3D, 8'hEE, 8'h4C, 8'h95, 8'h0B, 8'h42, 8'hFA, 8'hC3, 8'h4E, + 8'h08, 8'h2E, 8'hA1, 8'h66, 8'h28, 8'hD9, 8'h24, 8'hB2, 8'h76, 8'h5B, 8'hA2, 8'h49, 8'h6D, 8'h8B, 8'hD1, 8'h25, + 8'h72, 8'hF8, 8'hF6, 8'h64, 8'h86, 8'h68, 8'h98, 8'h16, 8'hD4, 8'hA4, 8'h5C, 8'hCC, 8'h5D, 8'h65, 8'hB6, 8'h92, + 8'h6C, 8'h70, 8'h48, 8'h50, 8'hFD, 8'hED, 8'hB9, 8'hDA, 8'h5E, 8'h15, 8'h46, 8'h57, 8'hA7, 8'h8D, 8'h9D, 8'h84, + 8'h90, 8'hD8, 8'hAB, 8'h00, 8'h8C, 8'hBC, 8'hD3, 8'h0A, 8'hF7, 8'hE4, 8'h58, 8'h05, 8'hB8, 8'hB3, 8'h45, 8'h06, + 8'hD0, 8'h2C, 8'h1E, 8'h8F, 8'hCA, 8'h3F, 8'h0F, 8'h02, 8'hC1, 8'hAF, 8'hBD, 8'h03, 8'h01, 8'h13, 8'h8A, 8'h6B, + 8'h3A, 8'h91, 8'h11, 8'h41, 8'h4F, 8'h67, 8'hDC, 8'hEA, 8'h97, 8'hF2, 8'hCF, 8'hCE, 8'hF0, 8'hB4, 8'hE6, 8'h73, + 8'h96, 8'hAC, 8'h74, 8'h22, 8'hE7, 8'hAD, 8'h35, 8'h85, 8'hE2, 8'hF9, 8'h37, 8'hE8, 8'h1C, 8'h75, 8'hDF, 8'h6E, + 8'h47, 8'hF1, 8'h1A, 8'h71, 8'h1D, 8'h29, 8'hC5, 8'h89, 8'h6F, 8'hB7, 8'h62, 8'h0E, 8'hAA, 8'h18, 8'hBE, 8'h1B, + 8'hFC, 8'h56, 8'h3E, 8'h4B, 8'hC6, 8'hD2, 8'h79, 8'h20, 8'h9A, 8'hDB, 8'hC0, 8'hFE, 8'h78, 8'hCD, 8'h5A, 8'hF4, + 8'h1F, 8'hDD, 8'hA8, 8'h33, 8'h88, 8'h07, 8'hC7, 8'h31, 8'hB1, 8'h12, 8'h10, 8'h59, 8'h27, 8'h80, 8'hEC, 8'h5F, + 8'h60, 8'h51, 8'h7F, 8'hA9, 8'h19, 8'hB5, 8'h4A, 8'h0D, 8'h2D, 8'hE5, 8'h7A, 8'h9F, 8'h93, 8'hC9, 8'h9C, 8'hEF, + 8'hA0, 8'hE0, 8'h3B, 8'h4D, 8'hAE, 8'h2A, 8'hF5, 8'hB0, 8'hC8, 8'hEB, 8'hBB, 8'h3C, 8'h83, 8'h53, 8'h99, 8'h61, + 8'h17, 8'h2B, 8'h04, 8'h7E, 8'hBA, 8'h77, 8'hD6, 8'h26, 8'hE1, 8'h69, 8'h14, 8'h63, 8'h55, 8'h21, 8'h0C, 8'h7D +}; + +// Rcon values for key schedule +parameter [31:0] fv_rcon[0:15] = '{ +32'h00000000, 32'h01000000, 32'h02000000, 32'h04000000, +32'h08000000, 32'h10000000, 32'h20000000, 32'h40000000, +32'h80000000, 32'h1B000000, 32'h36000000, 32'h6C000000, +32'hD8000000, 32'hAB000000, 32'h4D000000, 32'h9A000000 +}; + +// GF_2 for MixColumns +parameter [7:0] fv_gf2[0:255] = '{ + 8'h00, 8'h02, 8'h04, 8'h06, 8'h08, 8'h0A, 8'h0C, 8'h0E, 8'h10, 8'h12, 8'h14, 8'h16, 8'h18, 8'h1A, 8'h1C, 8'h1E, + 8'h20, 8'h22, 8'h24, 8'h26, 8'h28, 8'h2A, 8'h2C, 8'h2E, 8'h30, 8'h32, 8'h34, 8'h36, 8'h38, 8'h3A, 8'h3C, 8'h3E, + 8'h40, 8'h42, 8'h44, 8'h46, 8'h48, 8'h4a, 8'h4c, 8'h4e, 8'h50, 8'h52, 8'h54, 8'h56, 8'h58, 8'h5a, 8'h5c, 8'h5e, + 8'h60, 8'h62, 8'h64, 8'h66, 8'h68, 8'h6a, 8'h6c, 8'h6e, 8'h70, 8'h72, 8'h74, 8'h76, 8'h78, 8'h7a, 8'h7c, 8'h7e, + 8'h80, 8'h82, 8'h84, 8'h86, 8'h88, 8'h8a, 8'h8c, 8'h8e, 8'h90, 8'h92, 8'h94, 8'h96, 8'h98, 8'h9a, 8'h9c, 8'h9e, + 8'ha0, 8'ha2, 8'ha4, 8'ha6, 8'ha8, 8'haa, 8'hac, 8'hae, 8'hb0, 8'hb2, 8'hb4, 8'hb6, 8'hb8, 8'hba, 8'hbc, 8'hbe, + 8'hc0, 8'hc2, 8'hc4, 8'hc6, 8'hc8, 8'hca, 8'hcc, 8'hce, 8'hd0, 8'hd2, 8'hd4, 8'hd6, 8'hd8, 8'hda, 8'hdc, 8'hde, + 8'he0, 8'he2, 8'he4, 8'he6, 8'he8, 8'hea, 8'hec, 8'hee, 8'hf0, 8'hf2, 8'hf4, 8'hf6, 8'hf8, 8'hfa, 8'hfc, 8'hfe, + 8'h1b, 8'h19, 8'h1f, 8'h1d, 8'h13, 8'h11, 8'h17, 8'h15, 8'h0b, 8'h09, 8'h0f, 8'h0d, 8'h03, 8'h01, 8'h07, 8'h05, + 8'h3b, 8'h39, 8'h3f, 8'h3d, 8'h33, 8'h31, 8'h37, 8'h35, 8'h2b, 8'h29, 8'h2f, 8'h2d, 8'h23, 8'h21, 8'h27, 8'h25, + 8'h5b, 8'h59, 8'h5f, 8'h5d, 8'h53, 8'h51, 8'h57, 8'h55, 8'h4b, 8'h49, 8'h4f, 8'h4d, 8'h43, 8'h41, 8'h47, 8'h45, + 8'h7b, 8'h79, 8'h7f, 8'h7d, 8'h73, 8'h71, 8'h77, 8'h75, 8'h6b, 8'h69, 8'h6f, 8'h6d, 8'h63, 8'h61, 8'h67, 8'h65, + 8'h9b, 8'h99, 8'h9f, 8'h9d, 8'h93, 8'h91, 8'h97, 8'h95, 8'h8b, 8'h89, 8'h8f, 8'h8d, 8'h83, 8'h81, 8'h87, 8'h85, + 8'hbb, 8'hb9, 8'hbf, 8'hbd, 8'hb3, 8'hb1, 8'hb7, 8'hb5, 8'hab, 8'ha9, 8'haf, 8'had, 8'ha3, 8'ha1, 8'ha7, 8'ha5, + 8'hdb, 8'hd9, 8'hdf, 8'hdd, 8'hd3, 8'hd1, 8'hd7, 8'hd5, 8'hcb, 8'hc9, 8'hcf, 8'hcd, 8'hc3, 8'hc1, 8'hc7, 8'hc5, + 8'hfb, 8'hf9, 8'hff, 8'hfd, 8'hf3, 8'hf1, 8'hf7, 8'hf5, 8'heb, 8'he9, 8'hef, 8'hed, 8'he3, 8'he1, 8'he7, 8'he5 +}; + +// GF_3 for MixColumns +parameter [7:0] fv_gf3[0:255] = '{ + 8'h00, 8'h03, 8'h06, 8'h05, 8'h0C, 8'h0f, 8'h0A, 8'h09, 8'h18, 8'h1b, 8'h1E, 8'h1d, 8'h14, 8'h17, 8'h12, 8'h11, + 8'h30, 8'h33, 8'h36, 8'h35, 8'h3C, 8'h3f, 8'h3A, 8'h39, 8'h28, 8'h2b, 8'h2E, 8'h2d, 8'h24, 8'h27, 8'h22, 8'h21, + 8'h60, 8'h63, 8'h66, 8'h65, 8'h6c, 8'h6f, 8'h6a, 8'h69, 8'h78, 8'h7b, 8'h7e, 8'h7d, 8'h74, 8'h77, 8'h72, 8'h71, + 8'h50, 8'h53, 8'h56, 8'h55, 8'h5c, 8'h5f, 8'h5a, 8'h59, 8'h48, 8'h4b, 8'h4e, 8'h4d, 8'h44, 8'h47, 8'h42, 8'h41, + 8'hc0, 8'hc3, 8'hc6, 8'hc5, 8'hcc, 8'hcf, 8'hca, 8'hc9, 8'hd8, 8'hdb, 8'hde, 8'hdd, 8'hd4, 8'hd7, 8'hd2, 8'hd1, + 8'hf0, 8'hf3, 8'hf6, 8'hf5, 8'hfc, 8'hff, 8'hfa, 8'hf9, 8'he8, 8'heb, 8'hee, 8'hed, 8'he4, 8'he7, 8'he2, 8'he1, + 8'ha0, 8'ha3, 8'ha6, 8'ha5, 8'hac, 8'haf, 8'haa, 8'ha9, 8'hb8, 8'hbb, 8'hbe, 8'hbd, 8'hb4, 8'hb7, 8'hb2, 8'hb1, + 8'h90, 8'h93, 8'h96, 8'h95, 8'h9c, 8'h9f, 8'h9a, 8'h99, 8'h88, 8'h8b, 8'h8e, 8'h8d, 8'h84, 8'h87, 8'h82, 8'h81, + 8'h9b, 8'h98, 8'h9d, 8'h9e, 8'h97, 8'h94, 8'h91, 8'h92, 8'h83, 8'h80, 8'h85, 8'h86, 8'h8f, 8'h8c, 8'h89, 8'h8a, + 8'hab, 8'ha8, 8'had, 8'hae, 8'ha7, 8'ha4, 8'ha1, 8'ha2, 8'hb3, 8'hb0, 8'hb5, 8'hb6, 8'hbf, 8'hbc, 8'hb9, 8'hba, + 8'hfb, 8'hf8, 8'hfd, 8'hfe, 8'hf7, 8'hf4, 8'hf1, 8'hf2, 8'he3, 8'he0, 8'he5, 8'he6, 8'hef, 8'hec, 8'he9, 8'hea, + 8'hcb, 8'hc8, 8'hcd, 8'hce, 8'hc7, 8'hc4, 8'hc1, 8'hc2, 8'hd3, 8'hd0, 8'hd5, 8'hd6, 8'hdf, 8'hdc, 8'hd9, 8'hda, + 8'h5b, 8'h58, 8'h5d, 8'h5e, 8'h57, 8'h54, 8'h51, 8'h52, 8'h43, 8'h40, 8'h45, 8'h46, 8'h4f, 8'h4c, 8'h49, 8'h4a, + 8'h6b, 8'h68, 8'h6d, 8'h6e, 8'h67, 8'h64, 8'h61, 8'h62, 8'h73, 8'h70, 8'h75, 8'h76, 8'h7f, 8'h7c, 8'h79, 8'h7a, + 8'h3b, 8'h38, 8'h3d, 8'h3E, 8'h37, 8'h34, 8'h31, 8'h32, 8'h23, 8'h20, 8'h25, 8'h26, 8'h2f, 8'h2C, 8'h29, 8'h2A, + 8'h0b, 8'h08, 8'h0d, 8'h0E, 8'h07, 8'h04, 8'h01, 8'h02, 8'h13, 8'h10, 8'h15, 8'h16, 8'h1f, 8'h1C, 8'h19, 8'h1A +}; + +// GF_9 for MixColumns +parameter [7:0] fv_gf9[0:255] = '{ + 8'h00, 8'h09, 8'h12, 8'h1b, 8'h24, 8'h2d, 8'h36, 8'h3f, 8'h48, 8'h41, 8'h5a, 8'h53, 8'h6c, 8'h65, 8'h7e, 8'h77, + 8'h90, 8'h99, 8'h82, 8'h8b, 8'hb4, 8'hbd, 8'ha6, 8'haf, 8'hd8, 8'hd1, 8'hca, 8'hc3, 8'hfc, 8'hf5, 8'hee, 8'he7, + 8'h3b, 8'h32, 8'h29, 8'h20, 8'h1f, 8'h16, 8'h0d, 8'h04, 8'h73, 8'h7a, 8'h61, 8'h68, 8'h57, 8'h5e, 8'h45, 8'h4c, + 8'hab, 8'ha2, 8'hb9, 8'hb0, 8'h8f, 8'h86, 8'h9d, 8'h94, 8'he3, 8'hea, 8'hf1, 8'hf8, 8'hc7, 8'hce, 8'hd5, 8'hdc, + 8'h76, 8'h7f, 8'h64, 8'h6d, 8'h52, 8'h5b, 8'h40, 8'h49, 8'h3E, 8'h37, 8'h2C, 8'h25, 8'h1A, 8'h13, 8'h08, 8'h01, + 8'he6, 8'hef, 8'hf4, 8'hfd, 8'hc2, 8'hcb, 8'hd0, 8'hd9, 8'hae, 8'ha7, 8'hbc, 8'hb5, 8'h8a, 8'h83, 8'h98, 8'h91, + 8'h4d, 8'h44, 8'h5f, 8'h56, 8'h69, 8'h60, 8'h7b, 8'h72, 8'h05, 8'h0C, 8'h17, 8'h1E, 8'h21, 8'h28, 8'h33, 8'h3A, + 8'hdd, 8'hd4, 8'hcf, 8'hc6, 8'hf9, 8'hf0, 8'heb, 8'he2, 8'h95, 8'h9c, 8'h87, 8'h8e, 8'hb1, 8'hb8, 8'ha3, 8'haa, + 8'hec, 8'he5, 8'hfe, 8'hf7, 8'hc8, 8'hc1, 8'hda, 8'hd3, 8'ha4, 8'had, 8'hb6, 8'hbf, 8'h80, 8'h89, 8'h92, 8'h9b, + 8'h7c, 8'h75, 8'h6e, 8'h67, 8'h58, 8'h51, 8'h4a, 8'h43, 8'h34, 8'h3d, 8'h26, 8'h2f, 8'h10, 8'h19, 8'h02, 8'h0b, + 8'hd7, 8'hde, 8'hc5, 8'hcc, 8'hf3, 8'hfa, 8'he1, 8'he8, 8'h9f, 8'h96, 8'h8d, 8'h84, 8'hbb, 8'hb2, 8'ha9, 8'ha0, + 8'h47, 8'h4e, 8'h55, 8'h5c, 8'h63, 8'h6a, 8'h71, 8'h78, 8'h0f, 8'h06, 8'h1d, 8'h14, 8'h2b, 8'h22, 8'h39, 8'h30, + 8'h9a, 8'h93, 8'h88, 8'h81, 8'hbe, 8'hb7, 8'hac, 8'ha5, 8'hd2, 8'hdb, 8'hc0, 8'hc9, 8'hf6, 8'hff, 8'he4, 8'hed, + 8'h0A, 8'h03, 8'h18, 8'h11, 8'h2E, 8'h27, 8'h3C, 8'h35, 8'h42, 8'h4b, 8'h50, 8'h59, 8'h66, 8'h6f, 8'h74, 8'h7d, + 8'ha1, 8'ha8, 8'hb3, 8'hba, 8'h85, 8'h8c, 8'h97, 8'h9e, 8'he9, 8'he0, 8'hfb, 8'hf2, 8'hcd, 8'hc4, 8'hdf, 8'hd6, + 8'h31, 8'h38, 8'h23, 8'h2A, 8'h15, 8'h1C, 8'h07, 8'h0E, 8'h79, 8'h70, 8'h6b, 8'h62, 8'h5d, 8'h54, 8'h4f, 8'h46 +}; + +// GF_B for MixColumns +parameter [7:0] fv_gfB[0:255] = '{ + 8'h00, 8'h0b, 8'h16, 8'h1d, 8'h2C, 8'h27, 8'h3A, 8'h31, 8'h58, 8'h53, 8'h4e, 8'h45, 8'h74, 8'h7f, 8'h62, 8'h69, + 8'hb0, 8'hbb, 8'ha6, 8'had, 8'h9c, 8'h97, 8'h8a, 8'h81, 8'he8, 8'he3, 8'hfe, 8'hf5, 8'hc4, 8'hcf, 8'hd2, 8'hd9, + 8'h7b, 8'h70, 8'h6d, 8'h66, 8'h57, 8'h5c, 8'h41, 8'h4a, 8'h23, 8'h28, 8'h35, 8'h3E, 8'h0f, 8'h04, 8'h19, 8'h12, + 8'hcb, 8'hc0, 8'hdd, 8'hd6, 8'he7, 8'hec, 8'hf1, 8'hfa, 8'h93, 8'h98, 8'h85, 8'h8e, 8'hbf, 8'hb4, 8'ha9, 8'ha2, + 8'hf6, 8'hfd, 8'he0, 8'heb, 8'hda, 8'hd1, 8'hcc, 8'hc7, 8'hae, 8'ha5, 8'hb8, 8'hb3, 8'h82, 8'h89, 8'h94, 8'h9f, + 8'h46, 8'h4d, 8'h50, 8'h5b, 8'h6a, 8'h61, 8'h7c, 8'h77, 8'h1E, 8'h15, 8'h08, 8'h03, 8'h32, 8'h39, 8'h24, 8'h2f, + 8'h8d, 8'h86, 8'h9b, 8'h90, 8'ha1, 8'haa, 8'hb7, 8'hbc, 8'hd5, 8'hde, 8'hc3, 8'hc8, 8'hf9, 8'hf2, 8'hef, 8'he4, + 8'h3d, 8'h36, 8'h2b, 8'h20, 8'h11, 8'h1A, 8'h07, 8'h0C, 8'h65, 8'h6e, 8'h73, 8'h78, 8'h49, 8'h42, 8'h5f, 8'h54, + 8'hf7, 8'hfc, 8'he1, 8'hea, 8'hdb, 8'hd0, 8'hcd, 8'hc6, 8'haf, 8'ha4, 8'hb9, 8'hb2, 8'h83, 8'h88, 8'h95, 8'h9e, + 8'h47, 8'h4c, 8'h51, 8'h5a, 8'h6b, 8'h60, 8'h7d, 8'h76, 8'h1f, 8'h14, 8'h09, 8'h02, 8'h33, 8'h38, 8'h25, 8'h2E, + 8'h8c, 8'h87, 8'h9a, 8'h91, 8'ha0, 8'hab, 8'hb6, 8'hbd, 8'hd4, 8'hdf, 8'hc2, 8'hc9, 8'hf8, 8'hf3, 8'hee, 8'he5, + 8'h3C, 8'h37, 8'h2A, 8'h21, 8'h10, 8'h1b, 8'h06, 8'h0d, 8'h64, 8'h6f, 8'h72, 8'h79, 8'h48, 8'h43, 8'h5e, 8'h55, + 8'h01, 8'h0A, 8'h17, 8'h1C, 8'h2d, 8'h26, 8'h3b, 8'h30, 8'h59, 8'h52, 8'h4f, 8'h44, 8'h75, 8'h7e, 8'h63, 8'h68, + 8'hb1, 8'hba, 8'ha7, 8'hac, 8'h9d, 8'h96, 8'h8b, 8'h80, 8'he9, 8'he2, 8'hff, 8'hf4, 8'hc5, 8'hce, 8'hd3, 8'hd8, + 8'h7a, 8'h71, 8'h6c, 8'h67, 8'h56, 8'h5d, 8'h40, 8'h4b, 8'h22, 8'h29, 8'h34, 8'h3f, 8'h0E, 8'h05, 8'h18, 8'h13, + 8'hca, 8'hc1, 8'hdc, 8'hd7, 8'he6, 8'hed, 8'hf0, 8'hfb, 8'h92, 8'h99, 8'h84, 8'h8f, 8'hbe, 8'hb5, 8'ha8, 8'ha3 +}; + +// GF_D for MixColumns +parameter [7:0] fv_gfD[0:255] = '{ + 8'h00, 8'h0d, 8'h1A, 8'h17, 8'h34, 8'h39, 8'h2E, 8'h23, 8'h68, 8'h65, 8'h72, 8'h7f, 8'h5c, 8'h51, 8'h46, 8'h4b, + 8'hd0, 8'hdd, 8'hca, 8'hc7, 8'he4, 8'he9, 8'hfe, 8'hf3, 8'hb8, 8'hb5, 8'ha2, 8'haf, 8'h8c, 8'h81, 8'h96, 8'h9b, + 8'hbb, 8'hb6, 8'ha1, 8'hac, 8'h8f, 8'h82, 8'h95, 8'h98, 8'hd3, 8'hde, 8'hc9, 8'hc4, 8'he7, 8'hea, 8'hfd, 8'hf0, + 8'h6b, 8'h66, 8'h71, 8'h7c, 8'h5f, 8'h52, 8'h45, 8'h48, 8'h03, 8'h0E, 8'h19, 8'h14, 8'h37, 8'h3A, 8'h2d, 8'h20, + 8'h6d, 8'h60, 8'h77, 8'h7a, 8'h59, 8'h54, 8'h43, 8'h4e, 8'h05, 8'h08, 8'h1f, 8'h12, 8'h31, 8'h3C, 8'h2b, 8'h26, + 8'hbd, 8'hb0, 8'ha7, 8'haa, 8'h89, 8'h84, 8'h93, 8'h9e, 8'hd5, 8'hd8, 8'hcf, 8'hc2, 8'he1, 8'hec, 8'hfb, 8'hf6, + 8'hd6, 8'hdb, 8'hcc, 8'hc1, 8'he2, 8'hef, 8'hf8, 8'hf5, 8'hbe, 8'hb3, 8'ha4, 8'ha9, 8'h8a, 8'h87, 8'h90, 8'h9d, + 8'h06, 8'h0b, 8'h1C, 8'h11, 8'h32, 8'h3f, 8'h28, 8'h25, 8'h6e, 8'h63, 8'h74, 8'h79, 8'h5a, 8'h57, 8'h40, 8'h4d, + 8'hda, 8'hd7, 8'hc0, 8'hcd, 8'hee, 8'he3, 8'hf4, 8'hf9, 8'hb2, 8'hbf, 8'ha8, 8'ha5, 8'h86, 8'h8b, 8'h9c, 8'h91, + 8'h0A, 8'h07, 8'h10, 8'h1d, 8'h3E, 8'h33, 8'h24, 8'h29, 8'h62, 8'h6f, 8'h78, 8'h75, 8'h56, 8'h5b, 8'h4c, 8'h41, + 8'h61, 8'h6c, 8'h7b, 8'h76, 8'h55, 8'h58, 8'h4f, 8'h42, 8'h09, 8'h04, 8'h13, 8'h1E, 8'h3d, 8'h30, 8'h27, 8'h2A, + 8'hb1, 8'hbc, 8'hab, 8'ha6, 8'h85, 8'h88, 8'h9f, 8'h92, 8'hd9, 8'hd4, 8'hc3, 8'hce, 8'hed, 8'he0, 8'hf7, 8'hfa, + 8'hb7, 8'hba, 8'had, 8'ha0, 8'h83, 8'h8e, 8'h99, 8'h94, 8'hdf, 8'hd2, 8'hc5, 8'hc8, 8'heb, 8'he6, 8'hf1, 8'hfc, + 8'h67, 8'h6a, 8'h7d, 8'h70, 8'h53, 8'h5e, 8'h49, 8'h44, 8'h0f, 8'h02, 8'h15, 8'h18, 8'h3b, 8'h36, 8'h21, 8'h2C, + 8'h0C, 8'h01, 8'h16, 8'h1b, 8'h38, 8'h35, 8'h22, 8'h2f, 8'h64, 8'h69, 8'h7e, 8'h73, 8'h50, 8'h5d, 8'h4a, 8'h47, + 8'hdc, 8'hd1, 8'hc6, 8'hcb, 8'he8, 8'he5, 8'hf2, 8'hff, 8'hb4, 8'hb9, 8'hae, 8'ha3, 8'h80, 8'h8d, 8'h9a, 8'h97 +}; + +// GF_E for MixColumns +parameter [7:0] fv_gfE[0:255] = '{ + 8'h00, 8'h0E, 8'h1C, 8'h12, 8'h38, 8'h36, 8'h24, 8'h2A, 8'h70, 8'h7e, 8'h6c, 8'h62, 8'h48, 8'h46, 8'h54, 8'h5a, + 8'he0, 8'hee, 8'hfc, 8'hf2, 8'hd8, 8'hd6, 8'hc4, 8'hca, 8'h90, 8'h9e, 8'h8c, 8'h82, 8'ha8, 8'ha6, 8'hb4, 8'hba, + 8'hdb, 8'hd5, 8'hc7, 8'hc9, 8'he3, 8'hed, 8'hff, 8'hf1, 8'hab, 8'ha5, 8'hb7, 8'hb9, 8'h93, 8'h9d, 8'h8f, 8'h81, + 8'h3b, 8'h35, 8'h27, 8'h29, 8'h03, 8'h0d, 8'h1f, 8'h11, 8'h4b, 8'h45, 8'h57, 8'h59, 8'h73, 8'h7d, 8'h6f, 8'h61, + 8'had, 8'ha3, 8'hb1, 8'hbf, 8'h95, 8'h9b, 8'h89, 8'h87, 8'hdd, 8'hd3, 8'hc1, 8'hcf, 8'he5, 8'heb, 8'hf9, 8'hf7, + 8'h4d, 8'h43, 8'h51, 8'h5f, 8'h75, 8'h7b, 8'h69, 8'h67, 8'h3d, 8'h33, 8'h21, 8'h2f, 8'h05, 8'h0b, 8'h19, 8'h17, + 8'h76, 8'h78, 8'h6a, 8'h64, 8'h4e, 8'h40, 8'h52, 8'h5c, 8'h06, 8'h08, 8'h1A, 8'h14, 8'h3E, 8'h30, 8'h22, 8'h2C, + 8'h96, 8'h98, 8'h8a, 8'h84, 8'hae, 8'ha0, 8'hb2, 8'hbc, 8'he6, 8'he8, 8'hfa, 8'hf4, 8'hde, 8'hd0, 8'hc2, 8'hcc, + 8'h41, 8'h4f, 8'h5d, 8'h53, 8'h79, 8'h77, 8'h65, 8'h6b, 8'h31, 8'h3f, 8'h2d, 8'h23, 8'h09, 8'h07, 8'h15, 8'h1b, + 8'ha1, 8'haf, 8'hbd, 8'hb3, 8'h99, 8'h97, 8'h85, 8'h8b, 8'hd1, 8'hdf, 8'hcd, 8'hc3, 8'he9, 8'he7, 8'hf5, 8'hfb, + 8'h9a, 8'h94, 8'h86, 8'h88, 8'ha2, 8'hac, 8'hbe, 8'hb0, 8'hea, 8'he4, 8'hf6, 8'hf8, 8'hd2, 8'hdc, 8'hce, 8'hc0, + 8'h7a, 8'h74, 8'h66, 8'h68, 8'h42, 8'h4c, 8'h5e, 8'h50, 8'h0A, 8'h04, 8'h16, 8'h18, 8'h32, 8'h3C, 8'h2E, 8'h20, + 8'hec, 8'he2, 8'hf0, 8'hfe, 8'hd4, 8'hda, 8'hc8, 8'hc6, 8'h9c, 8'h92, 8'h80, 8'h8e, 8'ha4, 8'haa, 8'hb8, 8'hb6, + 8'h0C, 8'h02, 8'h10, 8'h1E, 8'h34, 8'h3A, 8'h28, 8'h26, 8'h7c, 8'h72, 8'h60, 8'h6e, 8'h44, 8'h4a, 8'h58, 8'h56, + 8'h37, 8'h39, 8'h2b, 8'h25, 8'h0f, 8'h01, 8'h13, 8'h1d, 8'h47, 8'h49, 8'h5b, 8'h55, 8'h7f, 8'h71, 8'h63, 8'h6d, + 8'hd7, 8'hd9, 8'hcb, 8'hc5, 8'hef, 8'he1, 8'hf3, 8'hfd, 8'ha7, 8'ha9, 8'hbb, 8'hb5, 8'h9f, 8'h91, 8'h83, 8'h8d +}; + +//Get SBOX value of a word +function logic[31:0] get_sbox(input logic [31:0] index_word); + logic [7:0] int_byte[0:3]; + logic [31:0] sbox_value; + + for (int i = 0; i < 4; i++) + int_byte[3-i] = fv_sbox[index_word[i*8 +: 8]]; + + sbox_value = {int_byte[0],int_byte[1],int_byte[2],int_byte[3]}; + + return sbox_value; +endfunction + +//Get Inverse SBOX value of a word +function logic[31:0] get_invsbox(input logic [31:0] index_word); + logic [7:0] int_byte[0:3]; + logic [31:0] invsbox_value; + + for (int i = 0; i < 4; i++) + int_byte[3-i] = fv_inv_sbox[index_word[i*8 +: 8]]; + + invsbox_value = {int_byte[0],int_byte[1],int_byte[2],int_byte[3]}; + + return invsbox_value; +endfunction + +//Rotation of a word +function logic[31:0] get_rotate_word(input logic [31:0] index_word); + logic [31:0] rotate_word; + rotate_word = {index_word[23:0], index_word[31:24]}; + return rotate_word; +endfunction + +//Get Rcon value +function logic[31:0] get_rcon(input logic [3:0] index); + return fv_rcon[index]; +endfunction + +//Compute Keyexpansion for 128bit configuration +function logic [127 : 0] compute_key_expansion_128(input logic [127 : 0] fv_key_int, input logic [3 : 0] fv_round_int); + logic [31:0] temp; + logic [31:0] w[0:43]; + logic [127:0] fv_round_key[0:10]; + + // The first four words are the original key + for (int i = 0; i < 4; i++) + w[3-i] = fv_key_int[i*32 +: 32]; + + // Compute all words of roundkeys - total of 44 words for 11 keys + for (int i = 4; i < 44; i++) begin + temp = w[i-1]; + if (i % 4 == 0) begin + temp = get_rotate_word(temp); + temp = get_sbox(temp); + temp = temp ^ get_rcon(i/4); + end + w[i] = w[i-4] ^ temp; + end + + //Assign the round keys + for (int i = 0; i < 11; i++) + fv_round_key[i] = {w[i*4], w[i*4+1], w[i*4+2], w[i*4+3]}; + + return fv_round_key[fv_round_int]; +endfunction + +//Compute Keyexpansion for 256bit configuration +function logic [127 : 0] compute_key_expansion_256(input logic [255 : 0] fv_key_int, input logic [3 : 0] fv_round_int); + logic [31:0] temp; + logic [31:0] w[0:59]; + logic [127:0] fv_round_key[0:14]; + + // The first eight words are the original key + for (int i = 0; i < 8; i++) + w[7-i] = fv_key_int[i*32 +: 32]; + + // Compute all words of roundkeys - total of 60 words for 15 keys + for (int i = 8; i < 60; i++) begin + temp = w[i-1]; + if (i % 8 == 0) begin + temp = get_rotate_word(temp); + temp = get_sbox(temp); + temp = temp ^ get_rcon(i/8); + w[i] = w[i-8] ^ temp; + end + else if ((i - (i/8)*8) == 4) begin + temp = get_sbox(temp); + w[i] = w[i-8] ^ temp; + end + else begin + w[i] = w[i-8] ^ w[i-1]; + end + end + + //Assign the round keys + for (int i = 0; i < 15; i++) + fv_round_key[i] = {w[i*4], w[i*4+1], w[i*4+2], w[i*4+3]}; + + return fv_round_key[fv_round_int]; +endfunction + + +//Compute MixColumns of the word +function logic[31:0] compute_mixcolums(input logic [31:0] index_word); + logic [7:0] int_byte[0:3]; + logic [7:0] mixcolumn_byte[0:3]; + logic [31:0] mixcolumn_value; + + for (int i = 0; i < 4; i++) + int_byte[3-i] = index_word[i*8 +: 8]; + + mixcolumn_byte[0] = fv_gf2[int_byte[0]] ^ fv_gf3[int_byte[1]] ^ int_byte[2] ^ int_byte[3]; + mixcolumn_byte[1] = int_byte[0] ^ fv_gf2[int_byte[1]] ^ fv_gf3[int_byte[2]] ^ int_byte[3]; + mixcolumn_byte[2] = int_byte[0] ^ int_byte[1] ^ fv_gf2[int_byte[2]] ^ fv_gf3[int_byte[3]]; + mixcolumn_byte[3] = fv_gf3[int_byte[0]] ^ int_byte[1] ^ int_byte[2] ^ fv_gf2[int_byte[3]]; + + mixcolumn_value = {mixcolumn_byte[0],mixcolumn_byte[1],mixcolumn_byte[2],mixcolumn_byte[3]}; + + return mixcolumn_value; +endfunction + +//Compute Inverse MixColumns of the word +function logic[31:0] compute_invmixcolums(input logic [31:0] index_word); + logic [7:0] int_byte[0:3]; + logic [7:0] invmixcolumn_byte[0:3]; + logic [31:0] invmixcolumn_value; + + for (int i = 0; i < 4; i++) + int_byte[3-i] = index_word[i*8 +: 8]; + + invmixcolumn_byte[0] = fv_gfE[int_byte[0]] ^ fv_gfB[int_byte[1]] ^ fv_gfD[int_byte[2]] ^ fv_gf9[int_byte[3]]; + invmixcolumn_byte[1] = fv_gf9[int_byte[0]] ^ fv_gfE[int_byte[1]] ^ fv_gfB[int_byte[2]] ^ fv_gfD[int_byte[3]]; + invmixcolumn_byte[2] = fv_gfD[int_byte[0]] ^ fv_gf9[int_byte[1]] ^ fv_gfE[int_byte[2]] ^ fv_gfB[int_byte[3]]; + invmixcolumn_byte[3] = fv_gfB[int_byte[0]] ^ fv_gfD[int_byte[1]] ^ fv_gf9[int_byte[2]] ^ fv_gfE[int_byte[3]]; + + invmixcolumn_value = {invmixcolumn_byte[0],invmixcolumn_byte[1],invmixcolumn_byte[2],invmixcolumn_byte[3]}; + + return invmixcolumn_value; +endfunction + +//Compute MixColumns of the msg +function logic[127:0] compute_mixcolums_msg(input logic [127:0] index_msg); + logic [31:0] int_word[0:3], mix_word[0:3]; + logic [127:0] mixcolumn_msg; + + for (int i = 0; i < 4; i++) + int_word[3-i] = index_msg[i*32 +: 32]; + + //Column 0 + mix_word[0] = compute_mixcolums(int_word[0]); + + //Column 1 + mix_word[1] = compute_mixcolums(int_word[1]); + + //Column 2 + mix_word[2] = compute_mixcolums(int_word[2]); + + //Column 3 + mix_word[3] = compute_mixcolums(int_word[3]); + + mixcolumn_msg = {mix_word[0],mix_word[1],mix_word[2],mix_word[3]}; + + return mixcolumn_msg; +endfunction + +//Compute Inverse MixColumns of the msg +function logic[127:0] compute_invmixcolums_msg(input logic [127:0] index_msg); + logic [31:0] int_word[0:3], invmix_word[0:3]; + logic [127:0] invmixcolumn_msg; + + for (int i = 0; i < 4; i++) + int_word[3-i] = index_msg[i*32 +: 32]; + + //Column 0 + invmix_word[0] = compute_invmixcolums(int_word[0]); + + //Column 1 + invmix_word[1] = compute_invmixcolums(int_word[1]); + + //Column 2 + invmix_word[2] = compute_invmixcolums(int_word[2]); + + //Column 3 + invmix_word[3] = compute_invmixcolums(int_word[3]); + + invmixcolumn_msg = {invmix_word[0],invmix_word[1],invmix_word[2],invmix_word[3]}; + + return invmixcolumn_msg; +endfunction + +//Compute AddRoundKey of index_msg with the key +function logic[127:0] compute_add_round_key(input logic [127:0] index_msg, input logic [127:0] index_key); + return (index_msg ^ index_key); +endfunction + +//Compute Shift row1 +function logic [31 : 0] compute_shiftrow1(input logic [31 : 0] index_word); + logic [7:0] int_byte[0:3]; + logic [31:0] shift_word; + + for (int i = 0; i < 4; i++) + int_byte[3-i] = index_word[i*8 +: 8]; + + shift_word = {int_byte[1],int_byte[2],int_byte[3],int_byte[0]}; + + return shift_word; +endfunction + +//Compute Inverse Shift row1 +function logic [31 : 0] compute_invshiftrow1(input logic [31 : 0] index_word); + logic [7:0] int_byte[0:3]; + logic [31:0] invshift_word; + + for (int i = 0; i < 4; i++) + int_byte[3-i] = index_word[i*8 +: 8]; + + invshift_word = {int_byte[3],int_byte[0],int_byte[1],int_byte[2]}; + + return invshift_word; +endfunction + +//Compute Shift row2 +function logic [31 : 0] compute_shiftrow2(input logic [31 : 0] index_word); + logic [7:0] int_byte[0:3]; + logic [31:0] shift_word; + + for (int i = 0; i < 4; i++) + int_byte[3-i] = index_word[i*8 +: 8]; + + shift_word = {int_byte[2],int_byte[3],int_byte[0],int_byte[1]}; + + return shift_word; +endfunction + +//Compute Inverse Shift row2 +function logic [31 : 0] compute_invshiftrow2(input logic [31 : 0] index_word); + logic [7:0] int_byte[0:3]; + logic [31:0] invshift_word; + + for (int i = 0; i < 4; i++) + int_byte[3-i] = index_word[i*8 +: 8]; + + invshift_word = {int_byte[2],int_byte[3],int_byte[0],int_byte[1]}; + + return invshift_word; +endfunction + +//Compute Shift row3 +function logic [31 : 0] compute_shiftrow3(input logic [31 : 0] index_word); + logic [7:0] int_byte[0:3]; + logic [31:0] shift_word; + + for (int i = 0; i < 4; i++) + int_byte[3-i] = index_word[i*8 +: 8]; + + shift_word = {int_byte[3],int_byte[0],int_byte[1],int_byte[2]}; + + return shift_word; +endfunction + +//Compute Inverse Shift row3 +function logic [31 : 0] compute_invshiftrow3(input logic [31 : 0] index_word); + logic [7:0] int_byte[0:3]; + logic [31:0] invshift_word; + + for (int i = 0; i < 4; i++) + int_byte[3-i] = index_word[i*8 +: 8]; + + invshift_word = {int_byte[1],int_byte[2],int_byte[3],int_byte[0]}; + + return invshift_word; +endfunction + +//Compute Shift rows +function logic [127 : 0] compute_shiftrow(input logic [127 : 0] index_msg); + logic [31:0] int_word[0:3]; + logic [31:0] shift_word[0:3]; + logic [127:0] shift_msg; + + for (int i = 0; i < 4; i++) + int_word[3-i] = index_msg[i*32 +: 32]; + + //Row 0 + shift_word[0] = {int_word[0][31:24],int_word[1][31:24],int_word[2][31:24],int_word[3][31:24]}; + + //Row 1 + shift_word[1] = {int_word[0][23:16],int_word[1][23:16],int_word[2][23:16],int_word[3][23:16]}; + shift_word[1] = compute_shiftrow1(shift_word[1]); + + //Row 2 + shift_word[2] = {int_word[0][15:8],int_word[1][15:8],int_word[2][15:8],int_word[3][15:8]}; + shift_word[2] = compute_shiftrow2(shift_word[2]); + + //Row 3 + shift_word[3] = {int_word[0][7:0],int_word[1][7:0],int_word[2][7:0],int_word[3][7:0]}; + shift_word[3] = compute_shiftrow3(shift_word[3]); + + //sent as a updated msg + int_word[0] = {shift_word[0][31:24],shift_word[1][31:24],shift_word[2][31:24],shift_word[3][31:24]}; + int_word[1] = {shift_word[0][23:16],shift_word[1][23:16],shift_word[2][23:16],shift_word[3][23:16]}; + int_word[2] = {shift_word[0][15:8],shift_word[1][15:8],shift_word[2][15:8],shift_word[3][15:8]}; + int_word[3] = {shift_word[0][7:0],shift_word[1][7:0],shift_word[2][7:0],shift_word[3][7:0]}; + + shift_msg = {int_word[0],int_word[1],int_word[2],int_word[3]}; + + return shift_msg; +endfunction + +//Compute Inverse Shift rows +function logic [127 : 0] compute_invshiftrow(input logic [127 : 0] index_msg); + logic [31:0] int_word[0:3]; + logic [31:0] invshift_word[0:3]; + logic [127:0] invshift_msg; + + for (int i = 0; i < 4; i++) + int_word[3-i] = index_msg[i*32 +: 32]; + + //Row 0 + invshift_word[0] = {int_word[0][31:24],int_word[1][31:24],int_word[2][31:24],int_word[3][31:24]}; + + //Row 1 + invshift_word[1] = {int_word[0][23:16],int_word[1][23:16],int_word[2][23:16],int_word[3][23:16]}; + invshift_word[1] = compute_invshiftrow1(invshift_word[1]); + + //Row 2 + invshift_word[2] = {int_word[0][15:8],int_word[1][15:8],int_word[2][15:8],int_word[3][15:8]}; + invshift_word[2] = compute_invshiftrow2(invshift_word[2]); + + //Row 3 + invshift_word[3] = {int_word[0][7:0],int_word[1][7:0],int_word[2][7:0],int_word[3][7:0]}; + invshift_word[3] = compute_invshiftrow3(invshift_word[3]); + + //sent as a updated msg + int_word[0] = {invshift_word[0][31:24],invshift_word[1][31:24],invshift_word[2][31:24],invshift_word[3][31:24]}; + int_word[1] = {invshift_word[0][23:16],invshift_word[1][23:16],invshift_word[2][23:16],invshift_word[3][23:16]}; + int_word[2] = {invshift_word[0][15:8],invshift_word[1][15:8],invshift_word[2][15:8],invshift_word[3][15:8]}; + int_word[3] = {invshift_word[0][7:0],invshift_word[1][7:0],invshift_word[2][7:0],invshift_word[3][7:0]}; + + invshift_msg = {int_word[0],int_word[1],int_word[2],int_word[3]}; + + return invshift_msg; +endfunction + +endpackage diff --git a/src/doe/formal/properties/fv_doe_decryption/fv_constraints.sv b/src/doe/formal/properties/fv_doe_decryption/fv_constraints.sv new file mode 100644 index 000000000..6a8c3fedb --- /dev/null +++ b/src/doe/formal/properties/fv_doe_decryption/fv_constraints.sv @@ -0,0 +1,118 @@ +// ------------------------------------------------- +// 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 doe_core_cbc_pkg::*; + +module fv_dec_constraints_m( + + //////////////////////////// + // Input / Output signals // + //////////////////////////// + input clk, + input reset_n, + + input next_cmd, + + input keylen, + input [3 : 0] round, + input [127 : 0] round_key, + + input [127 : 0] block_msg, + input [127 : 0] new_block, + input ready + +); + +//////////////////////// +// Default Clock // +//////////////////////// +default clocking default_clk @(posedge clk); endclocking + +//Internal Signals +logic [127:0] fv_round_key; +logic [127:0] fv_round_key_array[14:0]; + +//////////////////////// +// Symbolic logic // +//////////////////////// + +sym_roundkey_a: assume property (disable iff(!reset_n) sym_roundkey_p); +property sym_roundkey_p; + ##1 $stable(fv_round_key_array) +;endproperty + + +//Get expanded round keys for input key +function logic[127:0] get_roundkey(input logic [3:0] index_round); + logic [127:0] int_key; + + int_key = fv_round_key_array[index_round]; + + return int_key; +endfunction + +//Helper Logic +assign fv_round_key = get_roundkey(round); + +//////////////////////////////////////// +// Decryption Constraint Properties // +//////////////////////////////////////// + +//Constraint to drive correct value to round_key input +roundkey_constraint_a: assume property (disable iff(!reset_n) roundkey_constraint_p); +property roundkey_constraint_p; + round_key == fv_round_key +;endproperty + +//Constraint to keep keylen input stable +stable_keylen_a: assume property (disable iff(!reset_n) stable_keylen_p); +property stable_keylen_p; + $stable(keylen) || ready +;endproperty + +//Constraint to keep incoming block message stable +stable_blk_msg_a: assume property (disable iff(!reset_n) stable_blk_msg_p); +property stable_blk_msg_p; + $stable(block_msg) || ready +;endproperty + +//next_cmd can be only received if the doe_decipher_block is ready +cmd_on_ready_a: assume property (disable iff(!reset_n) cmd_on_ready_p); +property cmd_on_ready_p; + !ready +|-> + !next_cmd; +endproperty + +`ifdef CBC_BIND + //Constraint to drive correct value to fv_round_key_array signal in fv_decrypt checker + roundkey_array_cbc_a: assume property (disable iff(!reset_n) roundkey_array_cbc_p); + property roundkey_array_cbc_p; + doe_core_cbc.dec_block.fv_decrypt.fv_round_key_array == fv_round_key_array + ;endproperty +`endif + +endmodule + +//Connect this constraints module with the DUV +bind doe_decipher_block fv_dec_constraints_m fv_dec_constraints(.*, + .clk(clk), + .reset_n(reset_n && !zeroize) + ); + diff --git a/src/doe/formal/properties/fv_doe_decryption/fv_cover_points.sv b/src/doe/formal/properties/fv_doe_decryption/fv_cover_points.sv new file mode 100644 index 000000000..94e37ac97 --- /dev/null +++ b/src/doe/formal/properties/fv_doe_decryption/fv_cover_points.sv @@ -0,0 +1,46 @@ +// ------------------------------------------------- +// 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_dec_coverpoints_m( + input logic clk, + input logic reset_n, + input logic zeroize +); + +default clocking default_clk @(posedge clk); endclocking + +//Cover zeroize +cover_zeroize: cover property(disable iff(!reset_n) doe_decipher_block.zeroize ); + +//Assert zeroize input and check the status of all registers. All registers/internal memories should be cleared. +cover_zeroize_after_next: cover property(disable iff(!reset_n) doe_decipher_block.zeroize && doe_decipher_block.ready && doe_decipher_block.next_cmd ); + +//Cover that checks multiple next_cmd can be received for decipher block. +cover_multiple_next: cover property(disable iff(!reset_n || zeroize) + doe_decipher_block.next_cmd && doe_decipher_block.ready ##1 doe_decipher_block.next_cmd && doe_decipher_block.ready[->1] +); + +endmodule + +//Connect this coverpoints module with the DUV +bind doe_decipher_block fv_dec_coverpoints_m fv_dec_coverpoints( + .clk(clk), + .reset_n(reset_n), + .zeroize(zeroize) +); \ No newline at end of file diff --git a/src/doe/formal/properties/fv_doe_decryption/fv_doe_decrypt.sv b/src/doe/formal/properties/fv_doe_decryption/fv_doe_decrypt.sv new file mode 100644 index 000000000..5f1f75c80 --- /dev/null +++ b/src/doe/formal/properties/fv_doe_decryption/fv_doe_decrypt.sv @@ -0,0 +1,397 @@ +// ------------------------------------------------- +// 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 doe_core_cbc_pkg::*; + +module fv_decrypt_checker_m ( + + //////////////////////////// + // Input / Output signals // + //////////////////////////// + input clk, + input reset_n, + + input next_cmd, + + input keylen, + input [3 : 0] round, + input [127 : 0] round_key, + + input [127 : 0] block_msg, + input [127 : 0] new_block, + input ready, + + ////////////////////// + // States // + ////////////////////// + + input IDLE, + input Round_Compute, + + ////////////////////// + // Internal Signals // + ////////////////////// + input [127 : 0] block_new, + input [127 : 0] old_block, + + + //Signal for expanded keys + input [127 : 0] fv_round_key_array[14:0] + +); + +//localparams - Respective delays +localparam DLY_128 = 52; //no. of cycles the decryption takes for 128B configuration +localparam DLY_256 = 72; //no. of cycles the decryption takes for 256B configuration +localparam DLY_RND = 5; //no. of cycles the round computation takes +localparam DLY_SBOX = 4; //no. of cycles the SBOX computation takes + +//Compute first round intermediate step value for both 128/256 bit configuration +function logic [127 : 0] compute_firstdecrypt(input logic [127 : 0] index_msg, input logic mode); + logic [127:0] int_msg; + logic [31:0] int_word[0:3]; + + int_msg = index_msg; + + //Initial Step + if(mode) int_msg = compute_add_round_key(int_msg, fv_round_key_array[14]); + else int_msg = compute_add_round_key(int_msg, fv_round_key_array[10]); + + int_msg = compute_invshiftrow(int_msg); + + return int_msg; +endfunction + +//Compute Intermediate steps in each round +function logic [127 : 0] compute_round_decrypt(input logic [127 : 0] index_msg, input logic [3:0] int_rnd); + logic [127:0] int_msg; + logic [31:0] int_word[0:3]; + + int_msg = index_msg; + + //Round encryption + for (int i = 0; i < 4; i++) + int_word[3-i] = int_msg[i*32 +: 32]; + + for (int i = 0; i < 4; i++) + int_word[i] = get_invsbox(int_word[i]); + + int_msg = {int_word[0],int_word[1],int_word[2],int_word[3]}; + + int_msg = compute_add_round_key(int_msg, fv_round_key_array[int_rnd-1]); + + int_msg = compute_invmixcolums_msg(int_msg); + + int_msg = compute_invshiftrow(int_msg); + + return int_msg; +endfunction + +//Compute Intermediate step value in last round for both 128/256 bit configuration +function logic [127 : 0] compute_lastround_decrypt(input logic [127 : 0] index_msg); + logic [127:0] int_msg; + logic [31:0] int_word[0:3]; + + int_msg = index_msg; + + //Round encryption + for (int i = 0; i < 4; i++) + int_word[3-i] = int_msg[i*32 +: 32]; + + for (int i = 0; i < 4; i++) + int_word[i] = get_invsbox(int_word[i]); + + int_msg = {int_word[0],int_word[1],int_word[2],int_word[3]}; + + int_msg = compute_add_round_key(int_msg, fv_round_key_array[0]); + + return int_msg; +endfunction + +//Compute AES_Decryption for 128 bit configuration +function logic [127 : 0] compute_aes_decryption_128(input logic [127 : 0] index_msg); + logic [127:0] int_msg; + logic [31:0] int_word[0:3]; + + int_msg = index_msg; + + //Initial Step + int_msg = compute_add_round_key(int_msg, fv_round_key_array[10]); + + int_msg = compute_invshiftrow(int_msg); + + //Round encryption + for (int rnd = 9; rnd > 0; rnd--) begin + + //Round decryption + for (int i = 0; i < 4; i++) + int_word[3-i] = int_msg[i*32 +: 32]; + + for (int i = 0; i < 4; i++) + int_word[i] = get_invsbox(int_word[i]); + + int_msg = {int_word[0],int_word[1],int_word[2],int_word[3]}; + + int_msg = compute_add_round_key(int_msg, fv_round_key_array[rnd]); + + int_msg = compute_invmixcolums_msg(int_msg); + + int_msg = compute_invshiftrow(int_msg); + end + + //Final Round + for (int i = 0; i < 4; i++) + int_word[3-i] = int_msg[i*32 +: 32]; + + for (int i = 0; i < 4; i++) + int_word[i] = get_invsbox(int_word[i]); + + int_msg = {int_word[0],int_word[1],int_word[2],int_word[3]}; + + int_msg = compute_add_round_key(int_msg, fv_round_key_array[0]); + + return int_msg; +endfunction + +//Compute AES_Decryption for 256 bit configuration +function logic [127 : 0] compute_aes_decryption_256(input logic [127 : 0] index_msg); + logic [127:0] int_msg; + logic [31:0] int_word[0:3]; + + int_msg = index_msg; + + //Initial Step + int_msg = compute_add_round_key(int_msg, fv_round_key_array[14]); + + int_msg = compute_invshiftrow(int_msg); + + //Round encryption + for (int rnd = 13; rnd > 0; rnd--) begin + + //Round encryption + for (int i = 0; i < 4; i++) + int_word[3-i] = int_msg[i*32 +: 32]; + + for (int i = 0; i < 4; i++) + int_word[i] = get_invsbox(int_word[i]); + + int_msg = {int_word[0],int_word[1],int_word[2],int_word[3]}; + + int_msg = compute_add_round_key(int_msg, fv_round_key_array[rnd]); + + int_msg = compute_invmixcolums_msg(int_msg); + + int_msg = compute_invshiftrow(int_msg); + end + + //Final Round + for (int i = 0; i < 4; i++) + int_word[3-i] = int_msg[i*32 +: 32]; + + for (int i = 0; i < 4; i++) + int_word[i] = get_invsbox(int_word[i]); + + int_msg = {int_word[0],int_word[1],int_word[2],int_word[3]}; + + int_msg = compute_add_round_key(int_msg, fv_round_key_array[0]); + + return int_msg; +endfunction + +//////////////////////// +// Default Clock // +//////////////////////// +default clocking default_clk @(posedge clk); endclocking + +//////////////////////////////////// +// Decryption Checker Properties // +/////////////////////////////////// + +// Checks if the design is in IDLE state and ready is low +reset_a: assert property (reset_p); +property reset_p; + $past(!reset_n) +|-> + IDLE && + ready == 1 +;endproperty + +// Checks if block produces correct 128 bit decrypted value +decryption_check_128_a: assert property (disable iff(!reset_n) decryption_check_128_p); +property decryption_check_128_p; + logic [127:0] result, tracked_blk_msg; + + ##0 next_cmd + ##0 !keylen + ##0 (1'b1, tracked_blk_msg = block_msg) + ##DLY_128 (1'b1, result = compute_aes_decryption_128(tracked_blk_msg)) +|-> + ##0 new_block == result + ##0 ready +;endproperty + +// Checks if block produces correct sequence of round outputs for 128 bit configuration +round_check_128_a: assert property (disable iff(!reset_n) round_check_128_p); +property round_check_128_p; + ##0 next_cmd + ##0 !keylen +|-> + ##1 round == 10 && !ready[*DLY_RND] + ##1 round == 9 && !ready[*DLY_RND] + ##1 round == 8 && !ready[*DLY_RND] + ##1 round == 7 && !ready[*DLY_RND] + ##1 round == 6 && !ready[*DLY_RND] + ##1 round == 5 && !ready[*DLY_RND] + ##1 round == 4 && !ready[*DLY_RND] + ##1 round == 3 && !ready[*DLY_RND] + ##1 round == 2 && !ready[*DLY_RND] + ##1 round == 1 && !ready[*DLY_RND] + ##1 round == 0 && !ready + ##1 ready +;endproperty + +// Checks if block produces correct 256 bit decrypted value +decryption_check_256_a: assert property (disable iff(!reset_n) decryption_check_256_p); +property decryption_check_256_p; + logic [127:0] result, tracked_blk_msg; + + ##0 next_cmd + ##0 keylen + ##0 (1'b1, tracked_blk_msg = block_msg) + ##DLY_256 (1'b1, result = compute_aes_decryption_256(tracked_blk_msg)) +|-> + ##0 new_block == result + ##0 ready +;endproperty + +// Checks if block produces correct sequence of round outputs for 256 bit configuration +round_check_256_a: assert property (disable iff(!reset_n) round_check_256_p); +property round_check_256_p; + ##0 next_cmd + ##0 keylen +|-> + ##1 round == 14 && !ready[*DLY_RND] + ##1 round == 13 && !ready[*DLY_RND] + ##1 round == 12 && !ready[*DLY_RND] + ##1 round == 11 && !ready[*DLY_RND] + ##1 round == 10 && !ready[*DLY_RND] + ##1 round == 9 && !ready[*DLY_RND] + ##1 round == 8 && !ready[*DLY_RND] + ##1 round == 7 && !ready[*DLY_RND] + ##1 round == 6 && !ready[*DLY_RND] + ##1 round == 5 && !ready[*DLY_RND] + ##1 round == 4 && !ready[*DLY_RND] + ##1 round == 3 && !ready[*DLY_RND] + ##1 round == 2 && !ready[*DLY_RND] + ##1 round == 1 && !ready[*DLY_RND] + ##1 round == 0 && !ready + ##1 ready +;endproperty + +// Checks if block produces correct encrypted value for the first round +firstround_decrypt_a: assert property (disable iff(!reset_n) firstround_decrypt_p); +property firstround_decrypt_p; + logic [127:0] result, tracked_blk_msg, tracked_mode; + + ##0 next_cmd + ##0 (1'b1, tracked_blk_msg = block_msg) + ##0 (1'b1, tracked_mode = keylen) + ##0 (1'b1, result = compute_firstdecrypt(tracked_blk_msg,tracked_mode)) +|-> + ##1 block_new == result +;endproperty + +// Checks if block produces correct round encrypted value for each round in 128 bit configuration +for (genvar rnd = 9; rnd > 0; rnd--) begin: rndcompute_128 + round_compute_128_a: assert property (disable iff(!reset_n) round_compute_128_p(rnd+1)); +end +property round_compute_128_p(rndcnt); + logic [127:0] rnd_rslt, tracked_block; + ##0 Round_Compute && !keylen + ##0 round == rndcnt + ##1 (1'b1, tracked_block = old_block) + ##0 (1'b1, rnd_rslt = compute_round_decrypt(tracked_block,rndcnt)) +|-> + ##DLY_SBOX block_new == rnd_rslt +;endproperty + +// Checks if block produces correct round encrypted value for each round in 256 bit configuration +for (genvar rnd = 13; rnd > 0; rnd--) begin: rndcompute_256 + round_compute_256_a: assert property (disable iff(!reset_n) round_compute_256_p(rnd+1)); +end +property round_compute_256_p(rndcnt); + logic [127:0] rnd_rslt, tracked_block; + ##0 Round_Compute && keylen + ##0 round == rndcnt + ##1 (1'b1, tracked_block = old_block) + ##0 (1'b1, rnd_rslt = compute_round_decrypt(tracked_block,rndcnt)) +|-> + ##DLY_SBOX block_new == rnd_rslt +;endproperty + +// Checks if block produces correct encrypted value for the first round +lastround_decrypt_a: assert property (disable iff(!reset_n) lastround_decrypt_p); +property lastround_decrypt_p; + logic [127:0] rnd_rslt, tracked_block; + ##0 Round_Compute + ##0 round == 4'h1 + ##1 (1'b1, tracked_block = old_block) + ##0 (1'b1, rnd_rslt = compute_lastround_decrypt(tracked_block)) +|-> + ##DLY_SBOX block_new == rnd_rslt +;endproperty + +endmodule + +//Inputs driven from doe_core_cbc +`ifdef CBC_BIND + + bind doe_decipher_block fv_decrypt_checker_m + fv_decrypt( + .clk(doe_core_cbc.dec_block.clk), + .reset_n(doe_core_cbc.dec_block.reset_n && !doe_core_cbc.dec_block.zeroize), + .next_cmd(doe_core_cbc.dec_block.next_cmd), + .keylen(doe_core_cbc.dec_block.keylen), + .round(doe_core_cbc.dec_block.round), + .round_key(doe_core_cbc.dec_block.round_key), + .block_msg(doe_core_cbc.dec_block.block_msg), + .new_block(doe_core_cbc.dec_block.new_block), + .ready(doe_core_cbc.dec_block.ready), + .IDLE(doe_core_cbc.dec_block.dec_ctrl_reg == 0), + .Round_Compute((doe_core_cbc.dec_block.dec_ctrl_reg == 2'h1) || (doe_core_cbc.dec_block.dec_ctrl_reg == 2'h3)), + .old_block(doe_core_cbc.dec_block.round_logic.old_block), + .block_new(doe_core_cbc.dec_block.block_new), + .fv_round_key_array(doe_core_cbc.keymem.key_mem) + ); + +//Inputs driven with constraints on doe_decipher_block +`else + + bind doe_decipher_block fv_decrypt_checker_m + fv_decrypt(.*, + .clk(clk), + .reset_n(reset_n && !zeroize), + .IDLE(dec_ctrl_reg == 0), + .Round_Compute((dec_ctrl_reg == 2'h1) || (dec_ctrl_reg == 2'h3)), + .old_block(round_logic.old_block), + .block_new(block_new), + .fv_round_key_array(fv_dec_constraints.fv_round_key_array) + ); + +`endif \ No newline at end of file diff --git a/src/doe/formal/properties/fv_doe_encryption/fv_constraints.sv b/src/doe/formal/properties/fv_doe_encryption/fv_constraints.sv new file mode 100644 index 000000000..35b7614cd --- /dev/null +++ b/src/doe/formal/properties/fv_doe_encryption/fv_constraints.sv @@ -0,0 +1,128 @@ +// ------------------------------------------------- +// 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 doe_core_cbc_pkg::*; + +module fv_enc_constraints_m( + + //////////////////////////// + // Input / Output signals // + //////////////////////////// + input clk, + input reset_n, + + input next_cmd, + + input keylen, + input [3 : 0] round, + input [127 : 0] round_key, + + input [31 : 0] sboxw, + input [31 : 0] new_sboxw, + + input [127 : 0] block_msg, + input [127 : 0] new_block, + input ready + +); + +//////////////////////// +// Default Clock // +//////////////////////// +default clocking default_clk @(posedge clk); endclocking + +//Internal Signals +logic [31:0] fv_sbox; +logic [127:0] fv_round_key; +logic [127:0] fv_round_key_array[14:0]; + +//////////////////////// +// Symbolic Logic // +/////////////////////// + +sym_roundkey_a: assume property (disable iff(!reset_n) sym_roundkey_p); +property sym_roundkey_p; + ##1 $stable(fv_round_key_array) +;endproperty + +//Get expanded round keys for input key +function logic[127:0] get_roundkey(input logic [3:0] index_round); + logic [127:0] int_key; + + int_key = fv_round_key_array[index_round]; + + return int_key; +endfunction + +//Helper Logic +assign fv_sbox = get_sbox(sboxw); +assign fv_round_key = get_roundkey(round); + +//////////////////////////////////////// +// Encryption Constraint Properties // +////////////////////////////////////// + +//Constraint to drive correct value to new_sboxw input +sbox_constraint_a: assume property (disable iff(!reset_n) sbox_constraint_p); +property sbox_constraint_p; + new_sboxw == fv_sbox +;endproperty + +//Constraint to drive correct value to round_key input +roundkey_constraint_a: assume property (disable iff(!reset_n) roundkey_constraint_p); +property roundkey_constraint_p; + round_key == fv_round_key +;endproperty + +//Constraint to keep keylen input stable +stable_keylen_a: assume property (disable iff(!reset_n) stable_keylen_p); +property stable_keylen_p; + $stable(keylen) || ready +;endproperty + +//Constraint to keep incoming roundkey stable +stable_blk_msg_a: assume property (disable iff(!reset_n) stable_blk_msg_p); +property stable_blk_msg_p; + $stable(block_msg) || ready +;endproperty + +//next_cmd can be only received if the doe_encipher_block is ready +cmd_on_ready_a: assume property (disable iff(!reset_n) cmd_on_ready_p); +property cmd_on_ready_p; + !ready +|-> + !next_cmd; +endproperty + +`ifdef CBC_BIND + //Constraint to drive correct value to fv_round_key_array signal in fv_encrypt checker + roundkey_array_cbc_a: assume property (disable iff(!reset_n) roundkey_array_cbc_p); + property roundkey_array_cbc_p; + doe_core_cbc.enc_block.fv_encrypt.fv_round_key_array == fv_round_key_array + ;endproperty +`endif + +endmodule + +//Connect this constraints module with the DUV +bind doe_encipher_block fv_enc_constraints_m fv_enc_constraints(.*, + .clk(clk), + .reset_n(reset_n && !zeroize) + ); + diff --git a/src/doe/formal/properties/fv_doe_encryption/fv_cover_points.sv b/src/doe/formal/properties/fv_doe_encryption/fv_cover_points.sv new file mode 100644 index 000000000..a766f6f94 --- /dev/null +++ b/src/doe/formal/properties/fv_doe_encryption/fv_cover_points.sv @@ -0,0 +1,46 @@ +// ------------------------------------------------- +// 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_enc_coverpoints_m( + input logic clk, + input logic reset_n, + input logic zeroize +); + +default clocking default_clk @(posedge clk); endclocking + +//Cover zeroize +cover_zeroize: cover property(disable iff(!reset_n) doe_encipher_block.zeroize ); + +//Assert zeroize input and check the status of all registers. All registers/internal memories should be cleared. +cover_zeroize_after_next: cover property(disable iff(!reset_n) doe_encipher_block.zeroize && doe_encipher_block.ready && doe_encipher_block.next_cmd ); + +//Cover that checks multiple next_cmd can be received for encipher block. +cover_multiple_next: cover property(disable iff(!reset_n || zeroize) + doe_encipher_block.next_cmd && doe_encipher_block.ready ##1 doe_encipher_block.next_cmd && doe_encipher_block.ready[->1] +); + +endmodule + +//Connect this coverpoints module with the DUV +bind doe_encipher_block fv_enc_coverpoints_m fv_enc_coverpoints( + .clk(clk), + .reset_n(reset_n), + .zeroize(zeroize) +); \ No newline at end of file diff --git a/src/doe/formal/properties/fv_doe_encryption/fv_doe_encrypt.sv b/src/doe/formal/properties/fv_doe_encryption/fv_doe_encrypt.sv new file mode 100644 index 000000000..ba1603415 --- /dev/null +++ b/src/doe/formal/properties/fv_doe_encryption/fv_doe_encrypt.sv @@ -0,0 +1,348 @@ +// ------------------------------------------------- +// 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 doe_core_cbc_pkg::*; + +module fv_encrypt_checker_m ( + + //////////////////////////// + // Input / Output signals // + //////////////////////////// + input clk, + input reset_n, + + input next_cmd, + + input keylen, + input [3 : 0] round, + input [127 : 0] round_key, + + input [31 : 0] sboxw, + input [31 : 0] new_sboxw, + + input [127 : 0] block_msg, + input [127 : 0] new_block, + input ready, + + ////////////////////// + // States // + ////////////////////// + + input IDLE, + input Round_Compute, + + ////////////////////// + // Internal Signals // + ////////////////////// + input [127 : 0] block_new, + input [127 : 0] old_block, + + //Signal for expanded keys + input [127 : 0] fv_round_key_array[14:0] + +); + +//localparams - Respective delays +localparam DLY_128 = 52; //no. of cycles the decryption takes for 128B configuration +localparam DLY_256 = 72; //no. of cycles the decryption takes for 256B configuration +localparam DLY_RND = 5; //no. of cycles the round computation takes +localparam DLY_SBOX = 4; //no. of cycles the SBOX computation takes + +//Compute Intermediate steps in each round +function logic [127 : 0] compute_round_encrypt(input logic [127 : 0] index_msg, input logic [3:0] int_rnd); + logic [127:0] int_msg; + logic [31:0] int_word[0:3]; + + int_msg = index_msg; + + //Round encryption + for (int i = 0; i < 4; i++) + int_word[3-i] = int_msg[i*32 +: 32]; + + for (int i = 0; i < 4; i++) + int_word[i] = get_sbox(int_word[i]); + + int_msg = {int_word[0],int_word[1],int_word[2],int_word[3]}; + + int_msg = compute_shiftrow(int_msg); + + int_msg = compute_mixcolums_msg(int_msg); + + int_msg = compute_add_round_key(int_msg, fv_round_key_array[int_rnd]); + + return int_msg; +endfunction + +//Compute intermediate steps in last round +function logic [127 : 0] compute_lastround(input logic [127 : 0] index_msg, input logic [3:0] int_rnd); + logic [127:0] int_msg; + logic [31:0] int_word[0:3]; + + int_msg = index_msg; + + //Round encryption + for (int i = 0; i < 4; i++) + int_word[3-i] = int_msg[i*32 +: 32]; + + for (int i = 0; i < 4; i++) + int_word[i] = get_sbox(int_word[i]); + + int_msg = {int_word[0],int_word[1],int_word[2],int_word[3]}; + + int_msg = compute_shiftrow(int_msg); + + int_msg = compute_add_round_key(int_msg, fv_round_key_array[int_rnd]); + + return int_msg; +endfunction + +//Compute AES_Encryption 128 +function logic [127 : 0] compute_aes_encryption_128(input logic [127 : 0] index_msg); + logic [127:0] int_msg; + logic [31:0] int_word[0:3]; + + int_msg = index_msg; + + //Initial Step + int_msg = compute_add_round_key(int_msg, fv_round_key_array[0]); + + //Round encryption + for (int rnd = 1; rnd < 10; rnd++) begin + //Round encryption + int_msg = compute_round_encrypt(int_msg, rnd); + end + + //Final Round + int_msg = compute_lastround(int_msg, 4'ha); + + return int_msg; +endfunction + +//Compute AES_Encryption 256 +function logic [127 : 0] compute_aes_encryption_256(input logic [127 : 0] index_msg); + logic [127:0] int_msg; + logic [31:0] int_word[0:3]; + + int_msg = index_msg; + + //Initial Step + int_msg = compute_add_round_key(int_msg, fv_round_key_array[0]); + + //Round encryption + for (int rnd = 1; rnd < 14; rnd++) begin + //Round encryption + int_msg = compute_round_encrypt(int_msg, rnd); + end + + //Final Round + int_msg = compute_lastround(int_msg, 4'he); + + return int_msg; +endfunction + +//////////////////////// +// Default Clock // +//////////////////////// +default clocking default_clk @(posedge clk); endclocking + +////////////////////////////////////// +// Encryption Checker Properties // +//////////////////////////////////// + +// Checks if the design is in IDLE state and ready is low +reset_a: assert property (reset_p); +property reset_p; + $past(!reset_n) +|-> + IDLE && + ready == 1 +;endproperty + +// Checks if block produces correct 128 bit encrypted value +encryption_check_128_a: assert property (disable iff(!reset_n) encryption_check_128_p); +property encryption_check_128_p; + logic [127:0] result, tracked_blk_msg; + + ##0 next_cmd + ##0 !keylen + ##0 (1'b1, tracked_blk_msg = block_msg) + ##DLY_128 (1'b1, result = compute_aes_encryption_128(tracked_blk_msg)) +|-> + ##0 new_block == result + ##0 ready +;endproperty + +// Checks if block produces correct sequence of round outputs for 128 bit configuration +round_check_128_a: assert property (disable iff(!reset_n) round_check_128_p); +property round_check_128_p; + ##0 next_cmd + ##0 !keylen +|-> + ##1 round == 0 && !ready + ##1 round == 1 && !ready[*DLY_RND] + ##1 round == 2 && !ready[*DLY_RND] + ##1 round == 3 && !ready[*DLY_RND] + ##1 round == 4 && !ready[*DLY_RND] + ##1 round == 5 && !ready[*DLY_RND] + ##1 round == 6 && !ready[*DLY_RND] + ##1 round == 7 && !ready[*DLY_RND] + ##1 round == 8 && !ready[*DLY_RND] + ##1 round == 9 && !ready[*DLY_RND] + ##1 round == 10 && !ready[*DLY_RND] + ##1 ready +;endproperty + +// Checks if block produces correct 256 bit encrypted value +encryption_check_256_a: assert property (disable iff(!reset_n) encryption_check_256_p); +property encryption_check_256_p; + logic [127:0] result, tracked_blk_msg; + + ##0 next_cmd + ##0 keylen + ##0 (1'b1, tracked_blk_msg = block_msg) + ##DLY_256 (1'b1, result = compute_aes_encryption_256(tracked_blk_msg)) +|-> + ##0 new_block == result + ##0 ready +;endproperty + +// Checks if block produces correct sequence of round outputs for 256 bit configuration +round_check_256_a: assert property (disable iff(!reset_n) round_check_256_p); +property round_check_256_p; + ##0 next_cmd + ##0 keylen +|-> + ##1 round == 0 + ##1 round == 1 && !ready[*DLY_RND] + ##1 round == 2 && !ready[*DLY_RND] + ##1 round == 3 && !ready[*DLY_RND] + ##1 round == 4 && !ready[*DLY_RND] + ##1 round == 5 && !ready[*DLY_RND] + ##1 round == 6 && !ready[*DLY_RND] + ##1 round == 7 && !ready[*DLY_RND] + ##1 round == 8 && !ready[*DLY_RND] + ##1 round == 9 && !ready[*DLY_RND] + ##1 round == 10 && !ready[*DLY_RND] + ##1 round == 11 && !ready[*DLY_RND] + ##1 round == 12 && !ready[*DLY_RND] + ##1 round == 13 && !ready[*DLY_RND] + ##1 round == 14 && !ready[*DLY_RND] + ##1 ready +;endproperty + +// Checks if block produces correct round encrypted value for each round in 128 bit configuration +for (genvar rnd = 1; rnd < 10; rnd++) begin: rndcompute_128 + round_compute_128_a: assert property (disable iff(!reset_n) round_compute_128_p(rnd)); +end +property round_compute_128_p(rndcnt); + logic [127:0] result; + ##0 Round_Compute && !keylen + ##1 round == rndcnt + ##0 (1'b1, result = compute_round_encrypt(old_block,rndcnt)) +|-> + ##DLY_SBOX block_new == result +;endproperty + +// Checks if block produces correct round encrypted value for each round in 256 bit configuration +for (genvar rnd = 1; rnd < 14; rnd++) begin: rndcompute_256 + round_compute_256_a: assert property (disable iff(!reset_n) round_compute_256_p(rnd)); +end +property round_compute_256_p(rndcnt); + logic [127:0] result; + ##0 Round_Compute && keylen + ##1 round == rndcnt + ##0 (1'b1, result = compute_round_encrypt(old_block,rndcnt)) +|-> + ##DLY_SBOX block_new == result +;endproperty + +// Checks if block produces correct round encrypted value for last round in 128 bit configuration +lastround_computation_128_a: assert property (disable iff(!reset_n) lastround_computation_128_p); +property lastround_computation_128_p; + logic [127:0] result; + ##0 Round_Compute && !keylen + ##1 round == 4'ha + ##0 (1'b1, result = compute_lastround(old_block,4'ha)) +|-> + ##DLY_SBOX block_new == result +;endproperty + +// Checks if block produces correct round encrypted value for last round in 256 bit configuration +lastround_computation_256_a: assert property (disable iff(!reset_n) lastround_computation_256_p); +property lastround_computation_256_p; + logic [127:0] result; + ##0 Round_Compute && keylen + ##1 round == 4'he + ##0 (1'b1, result = compute_lastround(old_block,4'he)) +|-> + ##DLY_SBOX block_new == result +;endproperty + +// Checks if block produces correct encrypted value for the first round +firstround_compute_a: assert property (disable iff(!reset_n) firstround_compute_p); +property firstround_compute_p; + logic [127:0] result, tracked_blk_msg; + + ##0 next_cmd + ##0 (1'b1, tracked_blk_msg = block_msg) + ##0 (1'b1, result = compute_add_round_key(tracked_blk_msg, fv_round_key_array[0])) +|-> + ##1 block_new == result +;endproperty + +endmodule + +//Inputs driven from doe_core_cbc +`ifdef CBC_BIND + + bind doe_encipher_block fv_encrypt_checker_m + fv_encrypt( + .clk(doe_core_cbc.enc_block.clk), + .reset_n(doe_core_cbc.enc_block.reset_n && !doe_core_cbc.enc_block.zeroize), + .next_cmd(doe_core_cbc.enc_block.next_cmd), + .keylen(doe_core_cbc.enc_block.keylen), + .round(doe_core_cbc.enc_block.round), + .round_key(doe_core_cbc.enc_block.round_key), + .sboxw(doe_core_cbc.enc_block.sboxw), + .new_sboxw(doe_core_cbc.enc_block.new_sboxw), + .block_msg(doe_core_cbc.enc_block.block_msg), + .new_block(doe_core_cbc.enc_block.new_block), + .ready(doe_core_cbc.enc_block.ready), + .IDLE(doe_core_cbc.enc_block.enc_ctrl_reg == 0), + .Round_Compute((doe_core_cbc.enc_block.enc_ctrl_reg == 2'h1) || (doe_core_cbc.enc_block.enc_ctrl_reg == 2'h3)), + .old_block(doe_core_cbc.enc_block.round_logic.old_block), + .block_new(doe_core_cbc.enc_block.block_new), + .fv_round_key_array(doe_core_cbc.keymem.key_mem) + ); + +//Inputs driven with constraints on doe_encipher_block +`else + + bind doe_encipher_block fv_encrypt_checker_m + fv_encrypt(.*, + .clk(clk), + .reset_n(reset_n && !zeroize), + .IDLE(enc_ctrl_reg == 0), + .Round_Compute((enc_ctrl_reg == 2'h1) || (enc_ctrl_reg == 2'h3)), + .old_block(round_logic.old_block), + .block_new(block_new), + .fv_round_key_array(fv_enc_constraints.fv_round_key_array) + ); + +`endif diff --git a/src/doe/formal/properties/fv_doe_iv/fv_doe_iv_process.sv b/src/doe/formal/properties/fv_doe_iv/fv_doe_iv_process.sv new file mode 100644 index 000000000..19d13ac72 --- /dev/null +++ b/src/doe/formal/properties/fv_doe_iv/fv_doe_iv_process.sv @@ -0,0 +1,230 @@ +// ------------------------------------------------- +// 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 doe_iv_process_pkg::*; + +module fv_doe_iv_process_m( + input bit rst, + input bit rst_test, + input bit clk, + + // Inputs + input st_InPacket cmd_in, + input st_InPacket decrypt_in, + input st_InPacket result_in, + + // Outputs + input bit unsigned [127:0] ivdecry_out, + input bit unsigned [127:0] ivencry_out, + input bit doe_ready, + + // Ready signals + input bit cmd_in_ready, + input bit decrypt_in_ready, + input bit result_in_ready, + + // Registers + input bit unsigned [127:0] dec_prev_msg, + + // States + input bit idle, + input bit enc, + input bit dec_first, + input bit dec_next +); + + +default clocking default_clk @(posedge clk); endclocking + +// Checks if the design is in IDLE state and ready is high +reset_a: assert property (reset_p); +property reset_p; + $past(rst) |-> + idle && + doe_ready == 1 +;endproperty + +// Checks if the block updates IV_encry with the encoded message once encryption is done +enc_to_idle_a: assert property (disable iff(rst_test) enc_to_idle_p); +property enc_to_idle_p; + enc && + result_in_ready +|-> + ##1 + idle && + ivencry_out == $past(result_in.encoded_msg, 1); +endproperty + +// Checks if the block switches from idle state to enc state upon receiving next_cmd +idle_to_enc_a: assert property (disable iff(rst) idle_to_enc_p); +property idle_to_enc_p; + idle && + cmd_in_ready && + cmd_in.next_cmd && + cmd_in.encdec +|-> + ##1 + enc; +endproperty + +// Checks if the block waits in enc state until encryption is done +enc_wait_a: assert property (disable iff(rst) enc_wait_p); +property enc_wait_p; + enc && + !result_in_ready +|-> + ##1 + enc; +endproperty + +// Checks if the block waits iv_encry updated with IV +IV_encry_check_a: assert property (disable iff(rst) IV_encry_check_p); +property IV_encry_check_p; + doe_core_cbc.encdec && + cmd_in.IV_Updated_d +|-> + ##1 + ivencry_out == $past(cmd_in.IV, 1); +endproperty + +// Checks if the block switches from idle state to first decrypt state upon receiving next_cmd +// and updates IV_decry with the IV, IV_decry_next with incoming block message +idle_to_dec_first_a: assert property (disable iff(rst) idle_to_dec_first_p); +property idle_to_dec_first_p; + doe_core_cbc.IV_dec_state == 0 && + doe_core_cbc.next_cmd && doe_core_cbc.dec_ready && + !doe_core_cbc.encdec +|-> + ##1 + dec_first && + ivdecry_out == $past(doe_core_cbc.IV) && + dec_prev_msg == $past(doe_core_cbc.block_msg); +endproperty + +// Checks if the block switches from first decrypt state to next decrypt state upon receiving next_cmd +// and updates IV_decry with the previous IV_decry_next, IV_decry_next with incoming block message +dec_first_to_dec_next_a: assert property (disable iff(rst) dec_first_to_dec_next_p); +property dec_first_to_dec_next_p; + dec_first && + decrypt_in_ready +|-> + ##1 + dec_next && + ivdecry_out == $past(doe_core_cbc.IV_decry_next) && + dec_prev_msg == $past(doe_core_cbc.block_msg) +;endproperty + +// Checks if the block switches from next decrypt state to first decrypt state in next cycle +// and holds values of IV_decry, IV_decry_next from previous state +dec_next_to_dec_first_a: assert property (disable iff(rst) dec_next_to_dec_first_p); +property dec_next_to_dec_first_p; + dec_next +|-> + ##1 + dec_first && + ivdecry_out == $past(ivdecry_out) && + dec_prev_msg == $past(dec_prev_msg) +;endproperty + +// Checks if the block switches from first decrypt state to idle state upon receiving IV_updated +// and updates IV_decry, IV_decry_next with incoming IV +dec_first_to_idle_a: assert property (disable iff(rst) dec_first_to_idle_p); +property dec_first_to_idle_p; + dec_first && + decrypt_in.dec_ready && + !decrypt_in.next_cmd && + decrypt_in.IV_Updated_d +|-> + ##1 + idle && + ivdecry_out == $past(doe_core_cbc.IV, 1) && + dec_prev_msg == $past(doe_core_cbc.IV, 1) +;endproperty + +// Checks if the block waits in idle state until encryption/decryption is triggered +idle_wait_a: assert property (disable iff(rst) idle_wait_p); +property idle_wait_p; + idle && + !cmd_in_ready +|-> + ##1 + idle; +endproperty + +// Checks if the block waits in first decrypt state until new decryption starts or IV_updated is received +dec_first_wait_a: assert property (disable iff(rst) dec_first_wait_p); +property dec_first_wait_p; + dec_first && + !decrypt_in_ready && + !decrypt_in.IV_Updated_d +|-> + ##1 + dec_first +;endproperty + + +endmodule + + +module fv_doe_iv_process_ref_wrapper_m; + + +default clocking default_clk @(posedge (doe_core_cbc.clk)); endclocking + + +st_InPacket cmd_in = '{ encoded_msg: (doe_core_cbc.enc_new_block), block_msg: (doe_core_cbc.block_msg), IV: (doe_core_cbc.IV), encdec: (doe_core_cbc.encdec), enc_ready: (doe_core_cbc.enc_ready), dec_ready: (doe_core_cbc.dec_ready), IV_Updated_d: (doe_core_cbc.IV_updated_delayed), next_cmd: (doe_core_cbc.next_cmd), keylen: (doe_core_cbc.keylen) }; +st_InPacket decrypt_in = '{ encoded_msg: (doe_core_cbc.enc_new_block), block_msg: (doe_core_cbc.block_msg), IV: (doe_core_cbc.IV), encdec: (doe_core_cbc.encdec), enc_ready: (doe_core_cbc.enc_ready), dec_ready: (doe_core_cbc.dec_ready), IV_Updated_d: (doe_core_cbc.IV_updated_delayed), next_cmd: (doe_core_cbc.next_cmd), keylen: (doe_core_cbc.keylen) }; +st_InPacket result_in = '{ encoded_msg: (doe_core_cbc.enc_new_block), block_msg: (doe_core_cbc.block_msg), IV: (doe_core_cbc.IV), encdec: (doe_core_cbc.encdec), enc_ready: (doe_core_cbc.enc_ready), dec_ready: (doe_core_cbc.dec_ready), IV_Updated_d: (doe_core_cbc.IV_updated_delayed), next_cmd: (doe_core_cbc.next_cmd), keylen: (doe_core_cbc.keylen) }; + + +fv_doe_iv_process_m fv_doe_iv_process( + .rst(!(doe_core_cbc.reset_n && !doe_core_cbc.zeroize)), + .rst_test(!(doe_core_cbc.reset_n && !doe_core_cbc.zeroize) || $past(!(doe_core_cbc.reset_n && !doe_core_cbc.zeroize))), + .clk(doe_core_cbc.clk), + + // Inputs + .cmd_in(cmd_in), + .decrypt_in(decrypt_in), + .result_in(result_in), + + // Outputs + .ivdecry_out(doe_core_cbc.IV_decry), + .ivencry_out(doe_core_cbc.IV_encry), + .doe_ready(doe_core_cbc.ready), + + // Ready signals + .cmd_in_ready((doe_core_cbc.enc_ready && doe_core_cbc.enc_next) || (doe_core_cbc.dec_ready && doe_core_cbc.dec_next)), + .decrypt_in_ready(doe_core_cbc.dec_next && doe_core_cbc.dec_ready), + .result_in_ready((!$past(doe_core_cbc.enc_ready) && doe_core_cbc.enc_ready) ), + + // Registers + .dec_prev_msg(doe_core_cbc.IV_decry_next), + + // States + .idle(doe_core_cbc.IV_enc_state == 0 || doe_core_cbc.IV_dec_state == 0), + .enc(doe_core_cbc.IV_enc_state == 1), + .dec_first(doe_core_cbc.IV_dec_state == 2), + .dec_next(doe_core_cbc.IV_dec_state == 1) +); + + +endmodule + + +bind doe_core_cbc fv_doe_iv_process_ref_wrapper_m fv_doe_iv_process_ref_wrapper(); diff --git a/src/doe/formal/properties/fv_doe_iv/fv_doe_iv_process_pkg.sv b/src/doe/formal/properties/fv_doe_iv/fv_doe_iv_process_pkg.sv new file mode 100644 index 000000000..eecf72f01 --- /dev/null +++ b/src/doe/formal/properties/fv_doe_iv/fv_doe_iv_process_pkg.sv @@ -0,0 +1,37 @@ +// ------------------------------------------------- +// 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 doe_iv_process_pkg; + + + typedef struct { + bit unsigned [127:0] encoded_msg; + bit unsigned [127:0] block_msg; + bit unsigned [127:0] IV; + bit encdec; + bit enc_ready; + bit dec_ready; + bit IV_Updated_d; + bit next_cmd; + bit keylen; + } st_InPacket; + + +endpackage diff --git a/src/doe/formal/properties/fv_doe_keymem/fv_constraints.sv b/src/doe/formal/properties/fv_doe_keymem/fv_constraints.sv new file mode 100644 index 000000000..8ab13e7bd --- /dev/null +++ b/src/doe/formal/properties/fv_doe_keymem/fv_constraints.sv @@ -0,0 +1,89 @@ +// ------------------------------------------------- +// 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 doe_core_cbc_pkg::*; + +module fv_key_constraints_m( + + //////////////////////////// + // Input / Output signals // + //////////////////////////// + input clk, + input reset_n, + + input [255 : 0] key, + input keylen, + input init_cmd, + + input [3 : 0] round, + input [127 : 0] round_key, + input ready, + + + input [31 : 0] sboxw, + input [31 : 0] new_sboxw + +); + +//////////////////////// +// Default Clock // +//////////////////////// +default clocking default_clk @(posedge clk); endclocking + +//Internal Signals +logic [31:0] fv_sbox; + +//Helper Logic +assign fv_sbox = get_sbox(sboxw); + +//////////////////////////////////// +// KeyMem Constraint Properties // +/////////////////////////////////// + +//Constraint to drive correct value to new_sboxw input +sbox_constraint_a: assume property (disable iff(!reset_n) sbox_constraint_p); +property sbox_constraint_p; + new_sboxw == fv_sbox +;endproperty + +//Constraint to keep keylen input stable +stable_keylen_a: assume property (disable iff(!reset_n) stable_keylen_p); +property stable_keylen_p; + $stable(keylen) || ready +;endproperty + +//Constraint to keep key input stable +stable_key_a: assume property (disable iff(!reset_n) stable_key_p); +property stable_key_p; + $stable(key) || ready +;endproperty + +//Constraint to get init_cmd only when the design is in IDLE state +init_only_in_idle_a: assume property (disable iff(!reset_n) init_only_in_idle_p); +property init_only_in_idle_p; + init_cmd +|-> + doe_key_mem.key_mem_ctrl_reg == 0 +;endproperty + +endmodule + +//Connect this constraints module with the DUV +bind doe_key_mem fv_key_constraints_m fv_keymem_constraints(.* + ); \ No newline at end of file diff --git a/src/doe/formal/properties/fv_doe_keymem/fv_cover_points.sv b/src/doe/formal/properties/fv_doe_keymem/fv_cover_points.sv new file mode 100644 index 000000000..5f94b0574 --- /dev/null +++ b/src/doe/formal/properties/fv_doe_keymem/fv_cover_points.sv @@ -0,0 +1,46 @@ +// ------------------------------------------------- +// 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_keymem_coverpoints_m( + input logic clk, + input logic reset_n, + input logic zeroize +); + +default clocking default_clk @(posedge clk); endclocking + +//Cover zeroize +cover_zeroize: cover property(disable iff(!reset_n) doe_key_mem.zeroize ); + +//Assert zeroize input and check the status of all registers. All registers/internal memories should be cleared. +cover_zeroize_after_next: cover property(disable iff(!reset_n) doe_key_mem.zeroize && doe_key_mem.ready && doe_key_mem.init_cmd); + +//Cover that checks multiple init_cmd can be received +cover_multiple_init: cover property(disable iff(!reset_n || zeroize) + doe_key_mem.init_cmd && doe_key_mem.ready ##1 doe_key_mem.init_cmd && doe_key_mem.ready[->1] +); + +endmodule + +//Connect this coverpoints module with the DUV +bind doe_key_mem fv_keymem_coverpoints_m fv_keymem_coverpoints( + .clk(clk), + .reset_n(reset_n), + .zeroize(zeroize) +); \ No newline at end of file diff --git a/src/doe/formal/properties/fv_doe_keymem/fv_keymem.sv b/src/doe/formal/properties/fv_doe_keymem/fv_keymem.sv new file mode 100644 index 000000000..e45cc6d29 --- /dev/null +++ b/src/doe/formal/properties/fv_doe_keymem/fv_keymem.sv @@ -0,0 +1,273 @@ +// ------------------------------------------------- +// 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 doe_core_cbc_pkg::*; + +module fv_keymem_checker_m ( + + //////////////////////////// + // Input / Output signals // + //////////////////////////// + input clk, + input reset_n, + + input [255 : 0] key, + input keylen, + input init_cmd, + + input [3 : 0] round, + input [127 : 0] round_key, + input ready, + + + input [31 : 0] sboxw, + input [31 : 0] new_sboxw, + + input [127 : 0] roundkey_mem [14 : 0], + + ////////////////////// + // States // + ////////////////////// + + input IDLE, + input Keyexpansion_128, + input Keyexpansion_256 + +); + +//localparams - Respective delays +localparam DLY_128 = 14; //no. of cycles the key expansion takes for 128B configuration +localparam DLY_256 = 18; //no. of cycles the key expansion takes for 256B configuration + +//////////////////////// +// Default Clock // +//////////////////////// +default clocking default_clk @(posedge clk); endclocking + +//////////////////////////////////// +// KeyMem Checker Properties // +/////////////////////////////////// + +logic [6:0] curr_bit; +logic [3:0] idx; + +//////////////////////// +// Symbolic Logic // +//////////////////////// +sym_bit: assume property (##1 $stable(curr_bit)); +sym_idx: assume property (##1 $stable(idx)); + +////////////////////////////////// +// KeyMem Checker Properties // +///////////////////////////////// + +// Checks if the design is in IDLE state and ready is low +reset_a: assert property (reset_p); +property reset_p; + $past(!reset_n) |-> + IDLE && + ready == 0 +;endproperty + +// Checks if ready stays same during IDLE to IDLE state transition +IDLE_to_IDLE_a: assert property (disable iff(!reset_n) IDLE_to_IDLE_p); +property IDLE_to_IDLE_p; + IDLE && + !init_cmd +|-> + ##1 + IDLE && + ready == $past(ready, 1) +;endproperty + +// Checks if ready is low during IDLE to Keyexpansion128 state transition +IDLE_to_keyExpansion128_a: assert property (disable iff(!reset_n) IDLE_to_keyExpansion128_p); +property IDLE_to_keyExpansion128_p; + IDLE && + init_cmd && + !keylen +|-> + ##1 + Keyexpansion_128 && + (ready == 0) +;endproperty + +// Checks if ready is low during IDLE to Keyexpansion256 state transition +IDLE_to_keyExpansion256_a: assert property (disable iff(!reset_n) IDLE_to_keyExpansion256_p); +property IDLE_to_keyExpansion256_p; + IDLE && + init_cmd && + keylen +|-> + ##1 + Keyexpansion_256 && + ready == 0 +;endproperty + +//Properties to load when CBC is considered as top module +`ifdef CBC_BIND + + roundkey_check_128_cbc_a: assert property (disable iff(!reset_n) roundkey_check_128_cbc_p); + property roundkey_check_128_cbc_p; + logic [255:0] tracked_key; + logic [127:0] result; + + ##0 init_cmd + ##0 !keylen + ##0 (1'b1, tracked_key = key) + ##0 (idx < 11) + + ##DLY_128 (1'b1, result = compute_key_expansion_128(tracked_key[255:128], idx)) + |-> + ##0 roundkey_mem[idx][curr_bit] == result[curr_bit] + ##0 ready + ;endproperty + + roundkey_check_256_cbc_a: assert property (disable iff(!reset_n) roundkey_check_256_cbc_p); + property roundkey_check_256_cbc_p; + logic [255:0] tracked_key; + logic [127:0] result; + + ##0 init_cmd + ##0 keylen + ##0 (1'b1, tracked_key = key) + ##0 (idx < 15) + + ##DLY_256 (1'b1, result = compute_key_expansion_256(tracked_key, idx)) + |-> + ##0 roundkey_mem[idx][curr_bit] == result[curr_bit] + ##0 ready + ;endproperty + + // Checks computed roundkeys for 128bit configuration and the ready signal + for (genvar rnd = 0; rnd < 11; rnd++) begin: rndkey128 + roundkey_check_a: assert property (disable iff(!reset_n) roundkey_check_128_p(rnd)); + end + property roundkey_check_128_p(rndcnt); + logic [255:0] tracked_key; + logic [127:0] result; + + ##0 init_cmd + ##0 !keylen + ##0 (1'b1, tracked_key = key) + + ##DLY_128 round == rndcnt + ##0 (1'b1, result = compute_key_expansion_128(tracked_key[255:128], round)) + |-> + ##0 round_key[curr_bit] == result[curr_bit] + ##0 ready + ;endproperty + + // Checks computed roundkeys for 256bit configuration and the ready signal + for (genvar rnd = 0; rnd < 15; rnd++) begin: rndkey256 + roundkey_check_a: assert property (disable iff(!reset_n) roundkey_check_256_p(rnd)); + end + property roundkey_check_256_p(rndcnt); + logic [255:0] tracked_key; + logic [127:0] result; + + ##0 init_cmd + ##0 keylen + ##0 (1'b1, tracked_key = key) + + ##DLY_256 round == rndcnt + ##0 (1'b1, result = compute_key_expansion_256(tracked_key[255:0], round)) + |-> + ##0 round_key[curr_bit] == result[curr_bit] + ##0 ready + ;endproperty + +//Properties to load when doe_key_mem is considered as top module +`else + + // Checks computed roundkeys for 128bit configuration and the ready signal + for (genvar rnd = 0; rnd < 11; rnd++) begin: rndkey128 + roundkey_check_a: assert property (disable iff(!reset_n) roundkey_check_128_p(rnd)); + end + property roundkey_check_128_p(rndcnt); + logic [255:0] tracked_key; + logic [127:0] result; + + ##0 init_cmd + ##0 !keylen + ##0 (1'b1, tracked_key = key) + + ##DLY_128 round == rndcnt + ##0 (1'b1, result = compute_key_expansion_128(tracked_key[255:128], round)) + |-> + ##0 round_key[curr_bit] == result[curr_bit] + ##0 ready + ;endproperty + + // Checks computed roundkeys for 256bit configuration and the ready signal + for (genvar rnd = 0; rnd < 15; rnd++) begin: rndkey256 + roundkey_check_a: assert property (disable iff(!reset_n) roundkey_check_256_p(rnd)); + end + property roundkey_check_256_p(rndcnt); + logic [255:0] tracked_key; + logic [127:0] result; + + ##0 init_cmd + ##0 keylen + ##0 (1'b1, tracked_key = key) + + ##DLY_256 round == rndcnt + ##0 (1'b1, result = compute_key_expansion_256(tracked_key[255:0], round)) + |-> + ##0 round_key[curr_bit] == result[curr_bit] + ##0 ready + ;endproperty + +`endif + +endmodule + +//Inputs driven from doe_core_cbc +`ifdef CBC_BIND + + bind doe_key_mem fv_keymem_checker_m fv_key_mem ( + .clk(doe_core_cbc.keymem.clk), + .reset_n(doe_core_cbc.keymem.reset_n && !doe_core_cbc.keymem.zeroize), + .key(doe_core_cbc.keymem.key), + .keylen(doe_core_cbc.keymem.keylen), + .init_cmd(doe_core_cbc.keymem.init_cmd), + .round(doe_core_cbc.keymem.round), + .round_key(doe_core_cbc.keymem.round_key), + .ready(doe_core_cbc.keymem.ready), + .sboxw(doe_core_cbc.keymem.sboxw), + .new_sboxw(doe_core_cbc.keymem.new_sboxw), + .roundkey_mem(doe_core_cbc.keymem.key_mem [14 : 0]), + .IDLE(doe_key_mem.key_mem_ctrl_reg == 0), + .Keyexpansion_128((doe_key_mem.key_mem_ctrl_reg == 1) && !keylen), + .Keyexpansion_256((doe_key_mem.key_mem_ctrl_reg == 1) && keylen) + ); + +//Inputs driven with constraints on doe_key_mem +`else + + bind doe_key_mem fv_keymem_checker_m fv_key_mem (.*, + .clk(clk), + .reset_n(reset_n && !zeroize), + .roundkey_mem(doe_key_mem.key_mem [14 : 0]), + .IDLE(doe_key_mem.key_mem_ctrl_reg == 0), + .Keyexpansion_128((doe_key_mem.key_mem_ctrl_reg == 1) && !keylen), + .Keyexpansion_256((doe_key_mem.key_mem_ctrl_reg == 1) && keylen) + ); + +`endif \ No newline at end of file diff --git a/src/doe/readme.md b/src/doe/readme.md new file mode 100644 index 000000000..11fb2217b --- /dev/null +++ b/src/doe/readme.md @@ -0,0 +1,195 @@ +# DOE +Date: 29-08-2023 +Author: LUBIS EDA + +## Folder Structure +The following subdirectories are part of the main directory **formal** + +- properties: Contains the assertion IP(AIP) for each submodule of DUT along with the valid system constraints in **fv_constraints.sv** + - keymem: **fv_doe_keymem** folder contains the assertion IP(AIP) for the submodule doe_key_mem along with the constraints for the respective AIP. + - encipher: **fv_doe_encryption** folder contains the assertion IP(AIP) for the submodule doe_encipher_block along with the constraints for the respective AIP. + - decipher: **fv_doe_decryption** folder contains the assertion IP(AIP) for the submodule doe_decipher_block along with the constraints for the respective AIP. + - iv: **fv_doe_iv** folder contains the assertion IP(AIP) for the IV_Controller implementation in the DUT. + - The folder also contains assertion IP(AIP) **fv_doe_core_cbc.sv** that covers few primary IO's properties and **fv_constraints.sv** contains the valid system constraints that drive primary Inputs as intended. + +## DUT Overview + +The DUT doe_core_cbc has the primary inputs and primary outputs as shown below. + +| S.No | Port | Direction | Description | +| ---- | ----------------- | --------- | --------------------------------------------------------------------------------- | +| 1 | clk | input | The positive edge of the clk is used for all the signals | +| 2 | reset_n | input | The reset signal is active low and resets the core | +| 3 | zeroize | input | The core is reseted when this signal is triggered. | +| 4 | encdec | input | The core is driven to perform encryption or decryption. | +| 5 | init_cmd | input | The core is initialised for the key expansion | +| 6 | next_cmd | input | The core is initialised for the encryption or decryption | +| 7 | ready | output | Indicates that core is ready to accept new block in CBC | +| 8 | key[255:0] | input | The input key used for keyexpansion and later for encryption/decryption | +| 9 | keylen | input | The core is initialised for the 128/256 bit configuration | +| 10 | IV[127:0] | input | The 128 bit Initialization_Vector value for CBC | +| 11 | IV_updated | input | The core is initialised when to consider the IV for CBC | +| 12 | block_msg[127:0] | input | The 128 bit input block message for encryption/decryption | +| 13 | result[127:0] | output | The 128 bit encrypted/decrypted message | +| 14 | result_valid | output | Indicates that the /encryption/decryption is done | + +When init_cmd is received, the core module uses the incoming 256 bit key and starts keyexpansion to generate either 10/14 roundkeys based on the incoming keylen. +Once the keyexpansion is done, the core is ready to receive IV_updated. If the core receives IV_updated, it uses incoming IV value else the previous value will be used. +When next_cmd is received, the core starts performing the encryption/decryption. It asserts the ready signal once the encryption/decryption is done. +## Assertion IP Overview + +The Assertion IP signals are bound with the respective signals in the dut. + +**properties** folder contains **global_package.sv** where all the required functions are implemented either for AES encryption or decryption + +### fv_keymem + + **fv_doe_keymem** folder contains the assertion IP(AIP) for the submodule doe_key_mem along with the constraints for the respective AIP. When this submodule is verified individually considers constraints that are in **fv_doe_keymem/fv_constraints.sv** else all inputs are driven from DUT. + +- reset_a: Checks that the ready is low and the state is idle. + +- IDLE_to_IDLE_a: Checks if there isn't any init_cmd in idle state and then the state stays in idle and holds the past value of ready. + +- IDLE_to_keyExpansion128_a: Checks if there is init_cmd in idle state and there isn't keylen input and then the state changes to keyexpansion for 128 bit config and verify that the ready is still low during keyexpansion. + +- IDLE_to_keyExpansion256_a: Checks if there is init_cmd in idle state and there is keylen input and then the state changes to keyexpansion for 256 bit config and verify that the ready is still low during keyexpansion. + +- roundkey_check_128_cbc_a: Checks that once the keyexpansion is done, doe_key_mem module sends out correct round_key of 128bit configuration based on the round input. + +- roundkey_check_256_cbc_a: Checks that once the keyexpansion is done, doe_key_mem module sends out correct round_key of 256bit configuration based on the round input. + +### fv_encrypt + + **fv_doe_encryption** folder contains the assertion IP(AIP) for the submodule doe_encipher_block along with the constraints for the respective AIP. When this submodule is verified individually considers constraints that are in **fv_doe_encryption/fv_constraints.sv** else all inputs are driven from DUT. + +- reset_a: Checks that the ready is high and the state is idle. + +- encryption_check_128_a: Checks that once the encryption is done, doe_encipher_block module sends out the encrypted 128bit message to new_block along with the ready signal + +- round_check_128_a: Checks that round output sends out the correct round number during the encryption of 128 bit block message + +- encryption_check_256_a: Checks that once the encryption is done, doe_encipher_block module sends out the encrypted 256bit message to new_block along with the ready signal + +- round_check_256_a: Checks that round output sends out the correct round number during the encryption of 256 bit block message + +### fv_decrypt + + **fv_doe_decryption** folder contains the assertion IP(AIP) for the submodule doe_decipher_block along with the constraints for the respective AIP. When this submodule is verified individually considers constraints that are in **fv_doe_decryption/fv_constraints.sv** else all inputs are driven from DUT. + +- reset_a: Checks that the ready is high and the state is idle. + +- decryption_check_128_a: Checks that once the decryption is done, doe_encipher_block module sends out the encrypted 128bit message to new_block along with the ready signal + +- round_check_128_a: Checks that round output sends out the correct round number during the decryption of 128 bit block message + +- decryption_check_256_a: Checks that once the decryption is done, doe_encipher_block module sends out the encrypted 256bit message to new_block along with the ready signal + +- round_check_256_a: Checks that round output sends out the correct round number during the decryption of 256 bit block message + + +### fv_doe_iv_process + + **fv_doe_iv** folder contains the assertion IP(AIP) for the IV_Controller implementation for CBC in DUT. This checker uses the same set of constraints that on the doe_core_cbc module which are in **properties/fv_constraints.sv**. + + **doe_iv_process_pkg.sv** consists of defined struct of input data taht will be used in the **fv_doe_iv_process** checker + +- reset_a: Checks that the ready is high and the state is idle. + +- enc_to_idle_a: Checks if encryption is done and state changes to idle while IV_controller loads IV_encry with the encrypted message + +- idle_to_enc_a: Checks if there is next_cmd in idle state and there is encdec input and then the state changes to enc. + +- idle_to_dec_first_a: Checks if the block switches from idle state to first decrypt state upon receiving next_cmd and updates IV_decry with the IV, IV_decry_next with incoming block message + +- dec_first_to_dec_next_a: Checks if the block switches from first decrypt state to next decrypt state upon receiving next_cmd and updates IV_decry with the previous IV_decry_next, IV_decry_next with incoming block message + +- dec_next_to_dec_first_a: Checks if the block switches from next decrypt state to first decrypt state in next cycle and holds values of IV_decry, IV_decry_next from previous state + +- dec_first_to_idle_a: Checks if the block switches from first decrypt state to idle state upon receiving IV_updated and updates IV_decry, IV_decry_next with incoming IV + +- enc_wait_a: Checks if encryption is done else wait in the same state until encryption is finished + +- dec_first_wait_a: Checks if the block waits in first decrypt state until new decryption starts or IV_updated is received + +- idle_wait_a: Checks if there is encryption or decryption request in idle and waits in the same state until either of them are received + + +### fv_doe_cbc_inst + + **properties** folder contains the assertion IP(AIP) for few of the primary outputs in DUT that are not covered in the previous checkers. This checker uses the same set of constraints that on the doe_core_cbc module which are in **properties/fv_constraints.sv**. + +- result_valid_enc_a: Checks if result_valid is asserted once after the encryption is done. + +- result_valid_dec_a: Checks if result_valid is asserted once after the decryption is done. + +- ready_kemem_a: Checks if ready is asserted once after the keyexpansion is done. + +- ready_enc_a: Checks if ready is asserted once after the encryption is done. + +- result_enc_a: Checks if result is stored with the encrypted message once the encryption is done. + +- result_dec_a: Checks if result is stored with the decrypted message once the decryption is done. + +- sbox_check_a: Checks if doe_sbox block produces correct values + +### fv_coverpoints + +- cover_zeroize: Checks that the ready is high and the state is idle. + +- cover_zeroize_after_next: Assert zeroize input and check the status of all registers. All registers/internal memories should be cleared. + +- cover_multiple_next: Cover that checks multiple next_cmd can be received for CBC encryption/decryption. + +- cover_transition_keyexp_to_iv: Cover that checks IV_updated asserted once the keyexapnsion is done + +- cover_transition_keyexp_to_encdec: Cover that checks if design can have a trandition from keyexpansion to encryption/decryption + +- cover_transition_keyexp_to_keyexp: Cover that checks if design can have a trandition from keyexpansion to keyexpansion + +- cover_transition_encdec_to_encdec: Cover that checks if design can have a trandition from encryption/decryption to encryption/decryption + +- cover_transition_encdec_to_keyexp: Cover that checks if design can have a trandition from encryption/decryption to keyexpansion + + +# Reproduce results + +**MACROS :** +CBC_BIND + +- Differentiates the set of assertions and assumptions added when loaded with top as respective submodule or doe_core_cbc. + +- When defined, the assertions and assumptions are considered based on doe_core_cbc module. + +- When not defined, the assertions and assumptions are independednt of doe_core_cbc module. + +- Differentiates the binding of the checker files when loaded with top as respective submodule or doe_core_cbc. + +- When not defined, the inputs are open and necessary inputs are driven from the respective constraints + +- When defined, the inputs are driven from doe_core_cbc based on constraints on doe_core_cbc module. + + +## Proving the submodules + +- Load submodule as top in the formal tool. + +- Load the checker files along with the constraints and respective packages in the formal tool. + +- Run the properties with ASSERT_BIND macro defined to verify that submodule behaves as intended. + +## Proving the top + +- Load all design files in the formal tool and set doe_core_cbc as top module. + +- Load all the checker files with CBC_BIND macro defined along with the constraints and respective packages in the formal tool. + +- Copy all the submodule assertions, covers and assumptions into seperate task and cut the signals from the top that affect the submodule verification. + +- On the main task, disable all submodule assumptions and just keep the assumptions on the doe_core_cbc module. + +- Run the properties on the main task to verify that the top module behaves as intended. + +- Switch the tasks to one of the submodules which consists of the assumptions and assertions of that particular submodule. + +- Run the properties on each submodule task to verify that the submodule behaves as intended. +