From 321e7ae930a02d7167bc0ac942a60e1a72e4dcfb Mon Sep 17 00:00:00 2001 From: ludwig247 Date: Fri, 8 Sep 2023 08:51:14 +0200 Subject: [PATCH 1/5] Update on Readme --- src/sha512/formal/model/SHA512.luref | 490 ------------------ src/sha512/formal/model/refinement.luctrl | 9 - src/sha512/formal/model/sha512.h | 57 +- .../model/{PriniTestBench => tb}/sc_main.cpp | 0 .../model/{PriniTestBench => tb}/tb.cpp | 0 .../formal/model/{PriniTestBench => tb}/tb.h | 0 .../testvectors/224.txt | 0 .../testvectors/256.txt | 0 .../testvectors/384.txt | 0 .../testvectors/384_long_msg.txt | 0 .../testvectors/512.txt | 0 .../testvectors/512_long_msg.txt | 0 .../formal/properties/fv_constraints.sv | 7 + .../formal/properties/fv_coverpoints.sv | 44 ++ src/sha512/formal/properties/fv_sha512.sv | 125 +++-- src/sha512/formal/properties/fv_sha512_pkg.sv | 37 +- src/sha512/formal/readme.md | 34 +- 17 files changed, 151 insertions(+), 652 deletions(-) delete mode 100644 src/sha512/formal/model/SHA512.luref delete mode 100644 src/sha512/formal/model/refinement.luctrl rename src/sha512/formal/model/{PriniTestBench => tb}/sc_main.cpp (100%) rename src/sha512/formal/model/{PriniTestBench => tb}/tb.cpp (100%) rename src/sha512/formal/model/{PriniTestBench => tb}/tb.h (100%) rename src/sha512/formal/model/{PriniTestBench => tb}/testvectors/224.txt (100%) rename src/sha512/formal/model/{PriniTestBench => tb}/testvectors/256.txt (100%) rename src/sha512/formal/model/{PriniTestBench => tb}/testvectors/384.txt (100%) rename src/sha512/formal/model/{PriniTestBench => tb}/testvectors/384_long_msg.txt (100%) rename src/sha512/formal/model/{PriniTestBench => tb}/testvectors/512.txt (100%) rename src/sha512/formal/model/{PriniTestBench => tb}/testvectors/512_long_msg.txt (100%) create mode 100644 src/sha512/formal/properties/fv_coverpoints.sv diff --git a/src/sha512/formal/model/SHA512.luref b/src/sha512/formal/model/SHA512.luref deleted file mode 100644 index 262cdb555..000000000 --- a/src/sha512/formal/model/SHA512.luref +++ /dev/null @@ -1,490 +0,0 @@ -{ - "version": 17, - "module": { - "name": "SHA512", - "reset_signal": { - "signal": "(sha512_core.reset_n) && !(sha512_core.zeroize)", - "is_active_low": true - }, - "clock_signal": { - "signal": "clk", - "is_falling_edge": false - }, - "next_shift_amount": 0, - "rtl_module_name": "sha512_core", - "instance_name": "inst", - "default_assertion_duration": 1, - "default_disable_iff": "", - "reset": { - "documentation_comment": "" - }, - "additional_includes": "fv_constraints.sv", - "additional_imports": "", - "sync_macros": [ - { - "name": "SHA_Input_sync", - "datatype": "bool", - "refinement": "((sha512_core.init_cmd) || (sha512_core.next_cmd))", - "create_commitments": true, - "timing": 0, - "unused": false - } - ], - "notify_macros": [ - { - "name": "out_notify", - "datatype": "bool", - "refinement": "(sha512_core.digest_valid) && ((sha512_core.sha512_ctrl_reg==2'h0) && $past(sha512_core.sha512_ctrl_reg==2'h2) )", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "SHA_Input_notify", - "datatype": "bool", - "refinement": "sha512_core.ready", - "create_commitments": true, - "timing": 0, - "unused": false - } - ], - "input_datapath_macros": [ - { - "name": "SHA_Input_sig_in", - "datatype": "sc_big_unsigned_1024", - "refinement": "sha512_core.block_msg", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "SHA_Input_sig_init", - "datatype": "bool", - "refinement": "sha512_core.init_cmd", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "SHA_Input_sig_next", - "datatype": "bool", - "refinement": "sha512_core.next_cmd", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "SHA_Input_sig_SHA_Mode", - "datatype": "signed_32", - "refinement": "if(sha512_core.mode==0)\n\treturn 224;\nelse if(sha512_core.mode==1)\n\treturn 256;\nelse if(sha512_core.mode==2)\n\treturn 384;\nelse\n\treturn 512;", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "SHA_Input_sig_zeroize", - "datatype": "bool", - "refinement": "sha512_core.zeroize", - "create_commitments": true, - "timing": 0, - "unused": false - } - ], - "output_datapath_macros": [ - { - "name": "out_sig", - "datatype": "sc_big_unsigned_512", - "refinement": "sha512_core.digest", - "create_commitments": true, - "timing": 0, - "unused": false - } - ], - "state_macros": [ - { - "name": "DONE", - "datatype": "bool", - "refinement": "sha512_core.sha512_ctrl_reg==2'h2", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "IDLE", - "datatype": "bool", - "refinement": "sha512_core.sha512_ctrl_reg==2'h0", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "SHA_Rounds", - "datatype": "bool", - "refinement": "sha512_core.sha512_ctrl_reg==2'h1", - "create_commitments": true, - "timing": 0, - "unused": false - } - ], - "register_macros": [ - { - "name": "a", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.a_reg", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "b", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.b_reg", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "c", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.c_reg", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "d", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.d_reg", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "e", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.e_reg", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "f", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.f_reg", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "g", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.g_reg", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "h", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.h_reg", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "H_0", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.H0_reg", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "H_1", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.H1_reg", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "H_2", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.H2_reg", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "H_3", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.H3_reg", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "H_4", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.H4_reg", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "H_5", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.H5_reg", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "H_6", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.H6_reg", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "H_7", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.H7_reg", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "i", - "datatype": "signed_32", - "refinement": "sha512_core.round_ctr_reg", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "W_0", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.w_mem_inst.w_mem[00]", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "W_1", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.w_mem_inst.w_mem[01]", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "W_10", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.w_mem_inst.w_mem[10]", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "W_11", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.w_mem_inst.w_mem[11]", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "W_12", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.w_mem_inst.w_mem[12]", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "W_13", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.w_mem_inst.w_mem[13]", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "W_14", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.w_mem_inst.w_mem[14]", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "W_15", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.w_mem_inst.w_mem[15]", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "W_2", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.w_mem_inst.w_mem[02]", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "W_3", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.w_mem_inst.w_mem[03]", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "W_4", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.w_mem_inst.w_mem[04]", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "W_5", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.w_mem_inst.w_mem[05]", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "W_6", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.w_mem_inst.w_mem[06]", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "W_7", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.w_mem_inst.w_mem[07]", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "W_8", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.w_mem_inst.w_mem[08]", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "W_9", - "datatype": "sc_big_unsigned_64", - "refinement": "sha512_core.w_mem_inst.w_mem[09]", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "MSG_digest", - "datatype": "sc_big_unsigned_512", - "refinement": "", - "create_commitments": true, - "timing": 0, - "unused": true - } - ], - "assertions": [ - { - "name": "DONE_to_IDLE", - "disable_iff": "", - "duration": -1, - "documentation_comment": "", - "unused": false - }, - { - "name": "IDLE_to_SHA_Rounds", - "disable_iff": "", - "duration": -1, - "documentation_comment": "", - "unused": false - }, - { - "name": "IDLE_to_SHA_Rounds_1", - "disable_iff": "", - "duration": -1, - "documentation_comment": "", - "unused": false - }, - { - "name": "IDLE_to_SHA_Rounds_2", - "disable_iff": "", - "duration": -1, - "documentation_comment": "", - "unused": false - }, - { - "name": "IDLE_to_SHA_Rounds_3", - "disable_iff": "", - "duration": -1, - "documentation_comment": "", - "unused": false - }, - { - "name": "IDLE_to_SHA_Rounds_4", - "disable_iff": "", - "duration": -1, - "documentation_comment": "", - "unused": false - }, - { - "name": "SHA_Rounds_to_DONE", - "disable_iff": "", - "duration": -1, - "documentation_comment": "", - "unused": false - }, - { - "name": "SHA_Rounds_to_SHA_Rounds", - "disable_iff": "", - "duration": -1, - "documentation_comment": "", - "unused": false - }, - { - "name": "SHA_Rounds_to_SHA_Rounds_1", - "disable_iff": "", - "duration": -1, - "documentation_comment": "", - "unused": false - }, - { - "name": "IDLE_to_IDLE", - "disable_iff": "", - "duration": -1, - "documentation_comment": "", - "unused": true - }, - { - "name": "IDLE_to_SHA_Rounds_5", - "disable_iff": "", - "duration": -1, - "documentation_comment": "", - "unused": true - } - ], - "waits": [ - { - "name": "IDLE_wait", - "documentation_comment": "", - "unused": false - } - ] - } -} \ No newline at end of file diff --git a/src/sha512/formal/model/refinement.luctrl b/src/sha512/formal/model/refinement.luctrl deleted file mode 100644 index 7b7979b22..000000000 --- a/src/sha512/formal/model/refinement.luctrl +++ /dev/null @@ -1,9 +0,0 @@ -{ - "version": 13, - "modules": [ - { - "name": "SHA512", - "path": "SHA512.luref" - } - ] -} \ No newline at end of file diff --git a/src/sha512/formal/model/sha512.h b/src/sha512/formal/model/sha512.h index 357080d88..4bbad71a6 100644 --- a/src/sha512/formal/model/sha512.h +++ b/src/sha512/formal/model/sha512.h @@ -1,6 +1,26 @@ +// ------------------------------------------------- +// Contact: contact@lubis-eda.com +// Author: Tobias Ludwig, Michael Schwarz +// ------------------------------------------------- +// SPDX-License-Identifier: Apache-2.0 +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// + #ifndef SHA #define SHA + #include #include "systemc.h" #include "string.h" @@ -215,6 +235,7 @@ struct SHA_Args{ sc_biguint<64>(0x431d67c49c100d4c), sc_biguint<64>(0x4cc5d4becb3e42b6), sc_biguint<64>(0x597f299cfc657e2a),\ sc_biguint<64>(0x5fcb6fab3ad6faec), sc_biguint<64>(0x6c44198c4a475817)};; + SC_MODULE(SHA512) { blocking_in SHA_Input; @@ -304,30 +325,22 @@ while(true){ W = {sc_biguint<64>(0)}; } - //next(block_in); - //W_schedule(block_in); block_copy = block_in; for (j=0; j<16; ++j) { W[15-j] = slicer(block_copy, j); }; - - //copy_digest(); + a = H[0]; b = H[1];c = H[2]; d = H[3]; e = H[4]; f = H[5];g = H[6]; h = H[7]; for (i=0; i> (MSG_digest >> sc_biguint<512>(64)); MSG_digest += static_cast> (H[j] << sc_biguint<64>(448)); } - //MSG_digest = compute_dig(static_cast>(0),H[7],H[6],H[5],H[4],H[3],H[2],H[1],H[0]); - //MSG_digest = concati(MSG_digest, H, j); - /* BYME: to comply with rtl - switch (SHA_Mode_in){ - case 224: - MSG_digest = static_cast> (MSG_digest >> sc_biguint<512>(288)); - break; - case 256: - MSG_digest = static_cast> (MSG_digest >> sc_biguint<512>(256)); - break; - case 384: - MSG_digest = static_cast> (MSG_digest >> sc_biguint<512>(128)); - break; - default: - MSG_digest = static_cast> (MSG_digest); - break; - }*/ out->master_write(static_cast> (MSG_digest)); - - //}; - - //out->write(static_cast> (MSG_digest >> static_cast>(512-SHA_Mode_in))); } + }; #endif diff --git a/src/sha512/formal/model/PriniTestBench/sc_main.cpp b/src/sha512/formal/model/tb/sc_main.cpp similarity index 100% rename from src/sha512/formal/model/PriniTestBench/sc_main.cpp rename to src/sha512/formal/model/tb/sc_main.cpp diff --git a/src/sha512/formal/model/PriniTestBench/tb.cpp b/src/sha512/formal/model/tb/tb.cpp similarity index 100% rename from src/sha512/formal/model/PriniTestBench/tb.cpp rename to src/sha512/formal/model/tb/tb.cpp diff --git a/src/sha512/formal/model/PriniTestBench/tb.h b/src/sha512/formal/model/tb/tb.h similarity index 100% rename from src/sha512/formal/model/PriniTestBench/tb.h rename to src/sha512/formal/model/tb/tb.h diff --git a/src/sha512/formal/model/PriniTestBench/testvectors/224.txt b/src/sha512/formal/model/tb/testvectors/224.txt similarity index 100% rename from src/sha512/formal/model/PriniTestBench/testvectors/224.txt rename to src/sha512/formal/model/tb/testvectors/224.txt diff --git a/src/sha512/formal/model/PriniTestBench/testvectors/256.txt b/src/sha512/formal/model/tb/testvectors/256.txt similarity index 100% rename from src/sha512/formal/model/PriniTestBench/testvectors/256.txt rename to src/sha512/formal/model/tb/testvectors/256.txt diff --git a/src/sha512/formal/model/PriniTestBench/testvectors/384.txt b/src/sha512/formal/model/tb/testvectors/384.txt similarity index 100% rename from src/sha512/formal/model/PriniTestBench/testvectors/384.txt rename to src/sha512/formal/model/tb/testvectors/384.txt diff --git a/src/sha512/formal/model/PriniTestBench/testvectors/384_long_msg.txt b/src/sha512/formal/model/tb/testvectors/384_long_msg.txt similarity index 100% rename from src/sha512/formal/model/PriniTestBench/testvectors/384_long_msg.txt rename to src/sha512/formal/model/tb/testvectors/384_long_msg.txt diff --git a/src/sha512/formal/model/PriniTestBench/testvectors/512.txt b/src/sha512/formal/model/tb/testvectors/512.txt similarity index 100% rename from src/sha512/formal/model/PriniTestBench/testvectors/512.txt rename to src/sha512/formal/model/tb/testvectors/512.txt diff --git a/src/sha512/formal/model/PriniTestBench/testvectors/512_long_msg.txt b/src/sha512/formal/model/tb/testvectors/512_long_msg.txt similarity index 100% rename from src/sha512/formal/model/PriniTestBench/testvectors/512_long_msg.txt rename to src/sha512/formal/model/tb/testvectors/512_long_msg.txt diff --git a/src/sha512/formal/properties/fv_constraints.sv b/src/sha512/formal/properties/fv_constraints.sv index 2ffc12032..f250ba431 100644 --- a/src/sha512/formal/properties/fv_constraints.sv +++ b/src/sha512/formal/properties/fv_constraints.sv @@ -16,6 +16,7 @@ // See the License for the specific language governing permissions and // limitations under the License. // + module fv_constraints_m(init_cmd, next_cmd, reset_n, clk); input bit init_cmd, next_cmd, reset_n, clk; reg init_reg; @@ -31,6 +32,12 @@ default clocking default_clk @(posedge clk); endclocking !init_reg |-> !next_cmd; endproperty + + property next_only_if_digest_valid; + next_cmd |-> sha512_core.digest_valid ; + endproperty + next_only_if_digtest_valid_a: assume property (next_only_if_digest_valid); + always @ (posedge clk or negedge reset_n) begin : init_reg_order if (!reset_n) diff --git a/src/sha512/formal/properties/fv_coverpoints.sv b/src/sha512/formal/properties/fv_coverpoints.sv new file mode 100644 index 000000000..a05b9c144 --- /dev/null +++ b/src/sha512/formal/properties/fv_coverpoints.sv @@ -0,0 +1,44 @@ +// ------------------------------------------------- +// 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 +); + + default clocking default_clk @(posedge clk); endclocking + + //Cover zeroize: + //Assert zeroize input and check the status of all registers. All registers/internal memories should be cleared. + cover_zeroize: cover property(disable iff(!reset_n) sha512_core.zeroize ); + cover_zeroize_after_next: cover property(disable iff(!reset_n) sha512_core.zeroize && sha512_core.next_cmd ); + + //Cover modes: + //Cover all 4 different modes for SHA512 + cover_mode_224: cover property(disable iff(!reset_n) sha512_core.mode == 0 && sha512_core.init_cmd ); + cover_mode_256: cover property(disable iff(!reset_n) sha512_core.mode == 1 && sha512_core.init_cmd ); + cover_mode_384: cover property(disable iff(!reset_n) sha512_core.mode == 2 && sha512_core.init_cmd ); + cover_mode_512: cover property(disable iff(!reset_n) sha512_core.mode == 3 && sha512_core.init_cmd ); + + +endmodule +bind sha512_core fv_coverpoints_m fv_coverpoints( + .clk(clk), + .reset_n(reset_n) +); \ No newline at end of file diff --git a/src/sha512/formal/properties/fv_sha512.sv b/src/sha512/formal/properties/fv_sha512.sv index f36f06ff0..6d3030f49 100644 --- a/src/sha512/formal/properties/fv_sha512.sv +++ b/src/sha512/formal/properties/fv_sha512.sv @@ -24,7 +24,7 @@ module fv_sha_512_m( input bit rst, input bit clk, input bit unsigned [1023:0] block_in, - input bit unsigned [31:0] block_sha_mode, + input bit signed [31:0] block_sha_mode, input bit block_init, input bit block_next, input bit block_zeroize, @@ -172,8 +172,8 @@ property DONE_to_IDLE_p; endproperty -IDLE_to_SHA_Rounds_a: assert property (disable iff(!rst) IDLE_to_SHA_Rounds_p); -property IDLE_to_SHA_Rounds_p; +IDLE_to_SHA_Rounds_224_a: assert property (disable iff(!rst) IDLE_to_SHA_Rounds_224_p); +property IDLE_to_SHA_Rounds_224_p; IDLE && block_in_valid && block_init && @@ -219,8 +219,8 @@ property IDLE_to_SHA_Rounds_p; endproperty -IDLE_to_SHA_Rounds_1_a: assert property (disable iff(!rst) IDLE_to_SHA_Rounds_1_p); -property IDLE_to_SHA_Rounds_1_p; +IDLE_to_SHA_Rounds_256_a: assert property (disable iff(!rst) IDLE_to_SHA_Rounds_256_p); +property IDLE_to_SHA_Rounds_256_p; IDLE && block_in_valid && block_init && @@ -266,8 +266,8 @@ property IDLE_to_SHA_Rounds_1_p; endproperty -IDLE_to_SHA_Rounds_2_a: assert property (disable iff(!rst) IDLE_to_SHA_Rounds_2_p); -property IDLE_to_SHA_Rounds_2_p; +IDLE_to_SHA_Rounds_512_a: assert property (disable iff(!rst) IDLE_to_SHA_Rounds_512_p); +property IDLE_to_SHA_Rounds_512_p; IDLE && block_in_valid && block_init && @@ -313,14 +313,12 @@ property IDLE_to_SHA_Rounds_2_p; endproperty -IDLE_to_SHA_Rounds_3_a: assert property (disable iff(!rst) IDLE_to_SHA_Rounds_3_p); -property IDLE_to_SHA_Rounds_3_p; +IDLE_to_SHA_Rounds_384_a: assert property (disable iff(!rst) IDLE_to_SHA_Rounds_384_p); +property IDLE_to_SHA_Rounds_384_p; IDLE && block_in_valid && block_init && - (block_sha_mode != 'sd224) && - (block_sha_mode != 'sd256) && - (block_sha_mode != 'sd512) + block_sha_mode == 'sd384 |-> ##1 (block_in_ready == 0) and ##1 (digest_valid == 0) and @@ -362,8 +360,8 @@ property IDLE_to_SHA_Rounds_3_p; endproperty -IDLE_to_SHA_Rounds_4_a: assert property (disable iff(!rst) IDLE_to_SHA_Rounds_4_p); -property IDLE_to_SHA_Rounds_4_p; +IDLE_to_SHA_Rounds_next_a: assert property (disable iff(!rst) IDLE_to_SHA_Rounds_next_p); +property IDLE_to_SHA_Rounds_next_p; IDLE && block_in_valid && !block_init @@ -411,7 +409,6 @@ endproperty SHA_Rounds_to_DONE_a: assert property (disable iff(!rst) SHA_Rounds_to_DONE_p); property SHA_Rounds_to_DONE_p; SHA_Rounds && - (i >= 'sd16) && (('sd1 + i) >= 'sd80) |-> ##1 (block_in_ready == 0) and @@ -454,7 +451,7 @@ property SHA_Rounds_to_DONE_p; endproperty -SHA_Rounds_to_SHA_Rounds_a: assert property (disable iff(!rst) SHA_Rounds_to_SHA_Rounds_p); +SHA_Rounds_to_SHA_Rounds_before_16_a: assert property (disable iff(!rst) SHA_Rounds_to_SHA_Rounds_p); property SHA_Rounds_to_SHA_Rounds_p; SHA_Rounds && (i < 'sd16) @@ -499,7 +496,7 @@ property SHA_Rounds_to_SHA_Rounds_p; endproperty -SHA_Rounds_to_SHA_Rounds_1_a: assert property (disable iff(!rst) SHA_Rounds_to_SHA_Rounds_1_p); +SHA_Rounds_to_SHA_Rounds_after_16_a: assert property (disable iff(!rst) SHA_Rounds_to_SHA_Rounds_1_p); property SHA_Rounds_to_SHA_Rounds_1_p; SHA_Rounds && (i >= 'sd16) && @@ -593,52 +590,52 @@ endproperty endmodule bind sha512_core fv_sha_512_m fv_sha512( - .rst((sha512_core.reset_n) && !(sha512_core.zeroize)), - .clk(sha512_core.clk), - .block_in(sha512_core.block_msg), - .block_sha_mode(get_block_sha_mode(sha512_core.mode)), - .block_init(sha512_core.init_cmd), - .block_next(sha512_core.next_cmd), - .block_zeroize(sha512_core.zeroize), - .digest_out(sha512_core.digest), - .block_in_valid(((sha512_core.init_cmd) || (sha512_core.next_cmd))), - .block_in_ready(sha512_core.ready), - .digest_valid((sha512_core.digest_valid) ), - .H_0(sha512_core.H0_reg), - .H_1(sha512_core.H1_reg), - .H_2(sha512_core.H2_reg), - .H_3(sha512_core.H3_reg), - .H_4(sha512_core.H4_reg), - .H_5(sha512_core.H5_reg), - .H_6(sha512_core.H6_reg), - .H_7(sha512_core.H7_reg), - .W_0(sha512_core.w_mem_inst.w_mem[00]), - .W_1(sha512_core.w_mem_inst.w_mem[01]), - .W_2(sha512_core.w_mem_inst.w_mem[02]), - .W_3(sha512_core.w_mem_inst.w_mem[03]), - .W_4(sha512_core.w_mem_inst.w_mem[04]), - .W_5(sha512_core.w_mem_inst.w_mem[05]), - .W_6(sha512_core.w_mem_inst.w_mem[06]), - .W_7(sha512_core.w_mem_inst.w_mem[07]), - .W_8(sha512_core.w_mem_inst.w_mem[08]), - .W_9(sha512_core.w_mem_inst.w_mem[09]), - .W_10(sha512_core.w_mem_inst.w_mem[10]), - .W_11(sha512_core.w_mem_inst.w_mem[11]), - .W_12(sha512_core.w_mem_inst.w_mem[12]), - .W_13(sha512_core.w_mem_inst.w_mem[13]), - .W_14(sha512_core.w_mem_inst.w_mem[14]), - .W_15(sha512_core.w_mem_inst.w_mem[15]), - .a(sha512_core.a_reg), - .b(sha512_core.b_reg), - .c(sha512_core.c_reg), - .d(sha512_core.d_reg), - .e(sha512_core.e_reg), - .f(sha512_core.f_reg), - .g(sha512_core.g_reg), - .h(sha512_core.h_reg), - .i(sha512_core.round_ctr_reg), - .IDLE(sha512_core.sha512_ctrl_reg==2'h0), - .SHA_Rounds(sha512_core.sha512_ctrl_reg==2'h1), - .DONE(sha512_core.sha512_ctrl_reg==2'h2) + .rst((reset_n) && !(zeroize)), + .clk(clk), + .block_in(block_msg), + .block_sha_mode((mode==0)?224:(mode==1)?256:(mode==2)?384:512), + .block_init(init_cmd), + .block_next(next_cmd), + .block_zeroize(zeroize), + .digest_out(digest), + .block_in_valid(((init_cmd) || (next_cmd))), + .block_in_ready(ready), + .digest_valid((digest_valid) ), + .H_0(H0_reg), + .H_1(H1_reg), + .H_2(H2_reg), + .H_3(H3_reg), + .H_4(H4_reg), + .H_5(H5_reg), + .H_6(H6_reg), + .H_7(H7_reg), + .W_0(w_mem_inst.w_mem[00]), + .W_1(w_mem_inst.w_mem[01]), + .W_2(w_mem_inst.w_mem[02]), + .W_3(w_mem_inst.w_mem[03]), + .W_4(w_mem_inst.w_mem[04]), + .W_5(w_mem_inst.w_mem[05]), + .W_6(w_mem_inst.w_mem[06]), + .W_7(w_mem_inst.w_mem[07]), + .W_8(w_mem_inst.w_mem[08]), + .W_9(w_mem_inst.w_mem[09]), + .W_10(w_mem_inst.w_mem[10]), + .W_11(w_mem_inst.w_mem[11]), + .W_12(w_mem_inst.w_mem[12]), + .W_13(w_mem_inst.w_mem[13]), + .W_14(w_mem_inst.w_mem[14]), + .W_15(w_mem_inst.w_mem[15]), + .a(a_reg), + .b(b_reg), + .c(c_reg), + .d(d_reg), + .e(e_reg), + .f(f_reg), + .g(g_reg), + .h(h_reg), + .i(round_ctr_reg), + .IDLE(sha512_ctrl_reg==2'h0), + .SHA_Rounds(sha512_ctrl_reg==2'h1), + .DONE(sha512_ctrl_reg==2'h2) ); diff --git a/src/sha512/formal/properties/fv_sha512_pkg.sv b/src/sha512/formal/properties/fv_sha512_pkg.sv index 45ab5eb0c..da402d0a2 100644 --- a/src/sha512/formal/properties/fv_sha512_pkg.sv +++ b/src/sha512/formal/properties/fv_sha512_pkg.sv @@ -38,6 +38,7 @@ function bit unsigned [63:0] Maj(bit unsigned [63:0] x, bit unsigned [63:0] y, b return (((x & y) ^ (x & z)) ^ (y & z)); endfunction + function bit unsigned [63:0] T1(bit unsigned [63:0] e, bit unsigned [63:0] f, bit unsigned [63:0] g, bit unsigned [63:0] h, bit unsigned [63:0] k, bit unsigned [63:0] w); return 64'(((((h + sigma1(e)) + Ch(e, f, g)) + k) + w)); endfunction @@ -143,41 +144,7 @@ function bit unsigned [63:0] sigma1(bit unsigned [63:0] x); endfunction function bit unsigned [63:0] slicer(bit unsigned [1023:0] block, bit signed [31:0] index); - if ((index == 'sd0)) - return 64'((block >> 1024'd0)); - else if ((index == 'sd1)) - return 64'((block >> 1024'd64)); - else if ((index == 'sd2)) - return 64'((block >> 1024'd128)); - else if ((index == 'sd3)) - return 64'((block >> 1024'd192)); - else if ((index == 'sd4)) - return 64'((block >> 1024'd256)); - else if ((index == 'sd5)) - return 64'((block >> 1024'd320)); - else if ((index == 'sd6)) - return 64'((block >> 1024'd384)); - else if ((index == 'sd7)) - return 64'((block >> 1024'd448)); - else if ((index == 'sd8)) - return 64'((block >> 1024'd512)); - else if ((index == 'sd9)) - return 64'((block >> 1024'd576)); - else if ((index == 'sd10)) - return 64'((block >> 1024'd640)); - else if ((index == 'sd11)) - return 64'((block >> 1024'd704)); - else if ((index == 'sd12)) - return 64'((block >> 1024'd768)); - else if ((index == 'sd13)) - return 64'((block >> 1024'd832)); - else if ((index == 'sd14)) - return 64'((block >> 1024'd896)); - else if ((index == 'sd15)) - return 64'((block >> 1024'd960)); - else - return 64'((block >> 1024'd960)); + return(block[(64*index)+:64]); endfunction - endpackage diff --git a/src/sha512/formal/readme.md b/src/sha512/formal/readme.md index 8bfb89433..fce56dd87 100644 --- a/src/sha512/formal/readme.md +++ b/src/sha512/formal/readme.md @@ -29,44 +29,36 @@ The DUT sha512_core has the primary inputs and primary outputs as shown below. When the respective mode is selected and initalised the core iterates for 80 rounds to process the hash value, if the next is triggered then the previous values of the **H** registers are in place for processing the hash value. The digest is always generated of 512 bits, in which if the mode changes to 384 then from MSB 384 bits is a valid output and rest is garbage value. ## Assertion IP Overview -The Assertion IP signals are bound with the respective signals in the dut, where for the **rst** reset_n && !zeroize is used, which ensures the reset functionality. And another AIP signal block_in_valid is triggered whenever the init or next is high. +The Assertion IP signals are bound with the respective signals in the dut, where for the **rst** in binded with the DUT (reset_n && !zeroize), which ensures the reset functionality. And another AIP signal block_in_valid is triggered whenever the init or next is high. - reset_a: Checks that all the resgiters are resetted and the state is idle, with the ready to high. - DONE_to_IDLE_a: Checks the necessary registers,outputs holds the values when state transits from Done to idle, -- IDLE_to_SHA_Rounds_a: Checks if the state is in idle ,the mode choosen as 224,the init is triggered then the registers should be initialised with the respective constants of 224. +- IDLE_to_SHA_Rounds_224_a: Checks if the state is in idle ,the mode choosen as 224,the init is triggered then the registers should be initialised with the respective constants of 224. -- IDLE_to_SHA_Rounds_1_a: Checks if the state is in idle ,the mode choosen as 256,the init is triggered then the registers should be initialised with the respective constants of 256. +- IDLE_to_SHA_Rounds_256_a: Checks if the state is in idle ,the mode choosen as 256,the init is triggered then the registers should be initialised with the respective constants of 256. -- IDLE_to_SHA_Rounds_2_a: Checks if the state is in idle ,the mode choosen as 512,the init is triggered then the registers should be initialised with the respective constants of 512. +- IDLE_to_SHA_Rounds_512_a: Checks if the state is in idle ,the mode choosen as 512,the init is triggered then the registers should be initialised with the respective constants of 512. -- IDLE_to_SHA_Rounds_3_a: Checks if the state is in idle ,the mode choosen is neither 512,256 nor 224,the init is triggered then the registers should be initialised with the respective constants of default, which covers 384 mode also. +- IDLE_to_SHA_Rounds_384_a: Checks if the state is in idle ,the mode choosen is neither 512,256 nor 224,the init is triggered then the registers should be initialised with the respective constants of default, which covers 384 mode also. -- IDLE_to_SHA_Rounds_4_a: Checks if the state is in idle and there is no init signal and the next signal asserts then the register holds the past values. +- IDLE_to_SHA_Rounds_next_a: Checks if the state is in idle and there is no init signal and the next signal asserts then the register holds the past values. - SHA_Rounds_to_DONE_a: Checks if the rounds are done then the registers are updated correctly. -- SHA_Rounds_to_SHA_Rounds_a: Checks if the the rounds less than 16 then the necessary registers are updated correctly and the round increments. +- SHA_Rounds_to_SHA_Rounds_before_16a: Checks if the the rounds less than 16 then the necessary registers are updated correctly and the round increments. -- SHA_Rounds_to_SHA_Rounds_1_a: Checks if the rounds are greater than 16 and less than 80 then the respective registers are updated correctly and the round increments. +- SHA_Rounds_to_SHA_Rounds_after_16a_a: Checks if the rounds are greater than 16 and less than 80 then the respective registers are updated correctly and the round increments. - IDLE_wait_a: Checks if there isn't either init or next signal triggered in idle state then the state stays in idle and holds the past values and the core is ready. -- -## Loading the AIP -For onespin:
- 1. Open onespin, select file, run source.
- 2. Select the prove.tcl in onespin folder for running the properties.
+## Reproduce results -For VCformal:
- 1. Navigate to the vcf folder containing tcl scripts.
- 2. open terminal
- 3. run the cmd vcf -f prove.tcl (for running the properties).
+The AIP has been tested with two major FV tools. For both tools proves pass in less then 2 hour and coverage is at 100%. -For JasperGold: - 1. Open Jaspergold, click on file -> Tcl scripts -> Source.
- 2. Now Navigate to the script location and select the prove.tcl.
- 3. All the checkers and constraints would be loaded to the interface, right click on them and click on prove task.
+For reproducing the results: +Load the AIP, sha512_core and fv_constraints together in your formal tool. +Feel free to reach out to contact@lubis-eda.com to request the loadscripts. From bd6d759d7715086fcaf954866277823ecd007a86 Mon Sep 17 00:00:00 2001 From: ludwig247 Date: Fri, 8 Sep 2023 09:56:51 +0200 Subject: [PATCH 2/5] SHA 256 final --- src/sha256/formal/model/sha256_core.h | 316 ++++++ .../formal/model/sha256_core_generation.h | 256 +++++ .../formal/model/tb/sha256_core_tests.h | 983 ++++++++++++++++++ src/sha256/formal/model/tb/sha256_memory.h | 185 ++++ .../formal/properties/fv_constraints.sv | 54 + .../formal/properties/fv_coverpoints.sv | 48 + src/sha256/formal/properties/fv_sha256.sv | 600 +++++++++++ src/sha256/formal/properties/fv_sha256_pkg.sv | 75 ++ src/sha256/formal/readme.md | 61 ++ 9 files changed, 2578 insertions(+) create mode 100644 src/sha256/formal/model/sha256_core.h create mode 100644 src/sha256/formal/model/sha256_core_generation.h create mode 100644 src/sha256/formal/model/tb/sha256_core_tests.h create mode 100644 src/sha256/formal/model/tb/sha256_memory.h create mode 100644 src/sha256/formal/properties/fv_constraints.sv create mode 100644 src/sha256/formal/properties/fv_coverpoints.sv create mode 100644 src/sha256/formal/properties/fv_sha256.sv create mode 100644 src/sha256/formal/properties/fv_sha256_pkg.sv create mode 100644 src/sha256/formal/readme.md diff --git a/src/sha256/formal/model/sha256_core.h b/src/sha256/formal/model/sha256_core.h new file mode 100644 index 000000000..808628fa1 --- /dev/null +++ b/src/sha256/formal/model/sha256_core.h @@ -0,0 +1,316 @@ +// ------------------------------------------------- +// Contact: contact@lubis-eda.com +// Author: Tobias Ludwig, Michael Schwarz +// ------------------------------------------------- +// SPDX-License-Identifier: Apache-2.0 +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// + + +#ifndef SHA256_CORE_H +#define SHA256_CORE_H + +#include "systemc.h" +#include "Interfaces.h" +#include +#include +#include +#include +#include +#include +#include + +SC_MODULE(sha256_core) +{ +public: + uint32_t maj, xorA, ch, xorE, sum, newA, newE; + std::array m; + std::array state; + std::array K; + std::array m_state; + std::array n; + std::array hashing;//uint8 + uint32_t i, k; + uint32_t j; + int next_dummy, init_transform_dummy, ctrl_done_dummy, mode_dummy; + + blocking_in> w_core; + blocking_in mode; +#define loopstart 0u +#define loopbound 2u +#define incr 1u + +#ifdef SIMULATION + + blocking_out digest_block; +#else + blocking_out> digest_block;//uint8 +#endif + + blocking_in next_signal, init_signal, ctrl_done; + + SC_CTOR(sha256_core) + { + SC_THREAD(fsm); + } + + uint32_t rotr(uint32_t x, uint32_t n) const + { + return (x >> n) | (x << (32u - n)); + } + uint32_t choose(uint32_t e, uint32_t f, uint32_t g) const + { + return (e & f) ^ (~e & g); + } + uint32_t majority(uint32_t a, uint32_t b, uint32_t c) const + { + return (a & (b | c)) | (b & c); + } + uint32_t sig0(uint32_t x) const + { + return rotr(x, 7u) ^ rotr(x, 18u) ^ (x >> 3u); + } + uint32_t sig1(uint32_t x) const + { + return rotr(x, 17u) ^ rotr(x, 19u) ^ (x >> 10u); + } + + void fsm() + { + K[0] = 0x428a2f98u; + K[1] = 0x71374491u; + K[2] = 0xb5c0fbcfu; + K[3] = 0xe9b5dba5u; + K[4] = 0x3956c25bu; + K[5] = 0x59f111f1u; + K[6] = 0x923f82a4u; + K[7] = 0xab1c5ed5u; + K[8] = 0xd807aa98u; + K[9] = 0x12835b01u; + K[10] = 0x243185beu; + K[11] = 0x550c7dc3u; + K[12] = 0x72be5d74u; + K[13] = 0x80deb1feu; + K[14] = 0x9bdc06a7u; + K[15] = 0xc19bf174u; + K[16] = 0xe49b69c1u; + K[17] = 0xefbe4786u; + K[18] = 0x0fc19dc6u; + K[19] = 0x240ca1ccu; + K[20] = 0x2de92c6fu; + K[21] = 0x4a7484aau; + K[22] = 0x5cb0a9dcu; + K[23] = 0x76f988dau; + K[24] = 0x983e5152u; + K[25] = 0xa831c66du; + K[26] = 0xb00327c8u; + K[27] = 0xbf597fc7u; + K[28] = 0xc6e00bf3u; + K[29] = 0xd5a79147u; + K[30] = 0x06ca6351u; + K[31] = 0x14292967u; + K[32] = 0x27b70a85u; + K[33] = 0x2e1b2138u; + K[34] = 0x4d2c6dfcu; + K[35] = 0x53380d13u; + K[36] = 0x650a7354u; + K[37] = 0x766a0abbu; + K[38] = 0x81c2c92eu; + K[39] = 0x92722c85u; + K[40] = 0xa2bfe8a1u; + K[41] = 0xa81a664bu; + K[42] = 0xc24b8b70u; + K[43] = 0xc76c51a3u; + K[44] = 0xd192e819u; + K[45] = 0xd6990624u; + K[46] = 0xf40e3585u; + K[47] = 0x106aa070u; + K[48] = 0x19a4c116u; + K[49] = 0x1e376c08u; + K[50] = 0x2748774cu; + K[51] = 0x34b0bcb5u; + K[52] = 0x391c0cb3u; + K[53] = 0x4ed8aa4au; + K[54] = 0x5b9cca4fu; + K[55] = 0x682e6ff3u; + K[56] = 0x748f82eeu; + K[57] = 0x78a5636fu; + K[58] = 0x84c87814u; + K[59] = 0x8cc70208u; + K[60] = 0x90befffau; + K[61] = 0xa4506cebu; + K[62] = 0xbef9a3f7u; + K[63] = 0xc67178f2u; + m_state[0] = 0x0u; + m_state[1] = 0x0u; + m_state[2] = 0x0u; + m_state[3] = 0x0u; + m_state[4] = 0x0u; + m_state[5] = 0x0u; + m_state[6] = 0x0u; + m_state[7] = 0x0u; + state[0] = 0x0u; + state[1] = 0x0u; + state[2] = 0x0u; + state[3] = 0x0u; + state[4] = 0x0u; + state[5] = 0x0u; + state[6] = 0x0u; + state[7] = 0x0u; + while (true) + + { + mode->read(mode_dummy, "idle"); + ctrl_done->read(ctrl_done_dummy, "idle"); + next_signal->read(next_dummy, "idle"); + init_signal->read(init_transform_dummy, "idle"); + + if (mode_dummy == 0) + { + m_state[0] = 0x6a09e667u; + m_state[1] = 0xbb67ae85u; + m_state[2] = 0x3c6ef372u; + m_state[3] = 0xa54ff53au; + m_state[4] = 0x510e527fu; + m_state[5] = 0x9b05688cu; + m_state[6] = 0x1f83d9abu; + m_state[7] = 0x5be0cd19u; + } + else if (mode_dummy == 1) + { + + m_state[0] = 0xc1059ed8u; + m_state[1] = 0x367cd507u; + m_state[2] = 0x3070dd17u; + m_state[3] = 0xf70e5939u; + m_state[4] = 0xffc00b31u; + m_state[5] = 0x68581511u; + m_state[6] = 0x64f98fa7u; + m_state[7] = 0xbefa4fa4u; + } + + if (next_dummy == 1 || init_transform_dummy == 1 || ctrl_done_dummy == 1) + { + + if (next_dummy == 1 || init_transform_dummy == 1 || ctrl_done_dummy == 1) + + { + + w_core->read(n, "ctrl_rotation"); + for (j = 0u; j < 8u; ++j) // 16 + { + + m[j] = n[j]; + } + + for (k = 0u; k < 2u; ++k) // 64 + { + m[k] = sig1(m[k - 2u]) + m[k - 7u] + sig0(m[k - 15u]) + m[k - 16u]; + } + + for (i = 0u; i < 8u; ++i) + { + state[i] = m_state[i]; + } + + for (i = 0u; i < 2u; ++i) // 64 + { + maj = majority(state[0], state[1], state[2]); + xorA = rotr(state[0], 2u) ^ rotr(state[0], 13u) ^ rotr(state[0], 22u); + + ch = choose(state[4], state[5], state[6]); + + xorE = rotr(state[4], 6u) ^ rotr(state[4], 11u) ^ rotr(state[4], 25u); + + sum = m[i] + K[i] + state[7u] + ch + xorE; + newA = xorA + maj + sum; + newE = state[3] + sum; + + state[7] = state[6]; + state[6] = state[5]; + state[5] = state[4]; + state[4] = newE; + state[3] = state[2]; + state[2] = state[1]; + state[1] = state[0]; + state[0] = newA; + } + + /*for (i = 0u; i < 8u; ++i) // 8 + { //The error is here. + m_state[i]+=state[i]; + }*/ + } + } + if (next_dummy == 0 && init_transform_dummy == 0 && ctrl_done_dummy == 1) + { + + for (i = 0u; i < 1u; ++i) // 4 + { + for (k = 0u; k < 2u; ++k) // 8 + { + hashing[i + (k * 4u)] = (m_state[k] >> (24u - i * 8u))& 0x000000ffu; + } + } + } +#ifdef SIMULATION + std::stringstream s; // THIS PART IS FOR TESTING + s << std::setfill('0') << std::hex; // THIS PART IS FOR TESTING + if (mode_dummy == 0) + { + for (uint8_t i = 0; i < 32; i++) // THIS PART IS FOR TESTING + { + s << std::setw(2) << (unsigned int)hashing[i]; // THIS PART IS FOR TESTING + } + } + else + { + for (uint8_t i = 0; i < 28; i++) // THIS PART IS FOR TESTING + { + s << std::setw(2) << (unsigned int)hashing[i]; // THIS PART IS FOR TESTING + } + + } // THIS PART IS FOR TESTING + digest_block->write(s.str(), "ctrl_done"); // THIS PART IS FOR TESTING +#else + digest_block->write(hashing, "ctrl_done"); +#endif + + if (mode_dummy == 0) + { + m_state[0] = 0x6a09e667u; + m_state[1] = 0xbb67ae85u; + m_state[2] = 0x3c6ef372u; + m_state[3] = 0xa54ff53au; + m_state[4] = 0x510e527fu; + m_state[5] = 0x9b05688cu; + m_state[6] = 0x1f83d9abu; + m_state[7] = 0x5be0cd19u; + } + else if (mode_dummy == 1) + { + + m_state[0] = 0xc1059ed8u; + m_state[1] = 0x367cd507u; + m_state[2] = 0x3070dd17u; + m_state[3] = 0xf70e5939u; + m_state[4] = 0xffc00b31u; + m_state[5] = 0x68581511u; + m_state[6] = 0x64f98fa7u; + m_state[7] = 0xbefa4fa4u; + } + } + } +}; +#endif diff --git a/src/sha256/formal/model/sha256_core_generation.h b/src/sha256/formal/model/sha256_core_generation.h new file mode 100644 index 000000000..66ad266ae --- /dev/null +++ b/src/sha256/formal/model/sha256_core_generation.h @@ -0,0 +1,256 @@ +// ------------------------------------------------- +// Contact: contact@lubis-eda.com +// Author: Tobias Ludwig, Michael Schwarz +// ------------------------------------------------- +// SPDX-License-Identifier: Apache-2.0 +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// + +#ifndef SHA256_CORE_H +#define SHA256_CORE_H + +#include "systemc.h" +#include "Interfaces.h" +#include +const std::array K{0x428a2f98u, 0x71374491u, 0xb5c0fbcfu, 0xe9b5dba5u, + 0x3956c25bu, 0x59f111f1u, 0x923f82a4u, 0xab1c5ed5u, + 0xd807aa98u, 0x12835b01u, 0x243185beu, 0x550c7dc3u, + 0x72be5d74u, 0x80deb1feu, 0x9bdc06a7u, 0xc19bf174u, + 0xe49b69c1u, 0xefbe4786u, 0x0fc19dc6u, 0x240ca1ccu, + 0x2de92c6fu, 0x4a7484aau, 0x5cb0a9dcu, 0x76f988dau, + 0x983e5152u, 0xa831c66du, 0xb00327c8u, 0xbf597fc7u, + 0xc6e00bf3u, 0xd5a79147u, 0x06ca6351u, 0x14292967u, + 0x27b70a85u, 0x2e1b2138u, 0x4d2c6dfcu, 0x53380d13u, + 0x650a7354u, 0x766a0abbu, 0x81c2c92eu, 0x92722c85u, + 0xa2bfe8a1u, 0xa81a664bu, 0xc24b8b70u, 0xc76c51a3u, + 0xd192e819u, 0xd6990624u, 0xf40e3585u, 0x106aa070u, + 0x19a4c116u, 0x1e376c08u, 0x2748774cu, 0x34b0bcb5u, + 0x391c0cb3u, 0x4ed8aa4au, 0x5b9cca4fu, 0x682e6ff3u, + 0x748f82eeu, 0x78a5636fu, 0x84c87814u, 0x8cc70208u, + 0x90befffau, 0xa4506cebu, 0xbef9a3f7u, 0xc67178f2u}; + +uint32_t rotr(uint32_t x, uint32_t n) + { + return (x >> n) | (x << (32u - n)); + } + uint32_t choose(uint32_t e, uint32_t f, uint32_t g) + { + return (e & f) ^ (~e & g); + } + uint32_t majority(uint32_t a, uint32_t b, uint32_t c) + { + return (a & (b | c)) | (b & c); + } + uint32_t sig0(uint32_t x) + { + return rotr(x, 7u) ^ rotr(x, 18u) ^ (x >> 3u); + } + uint32_t sig1(uint32_t x) + { + return rotr(x, 17u) ^ rotr(x, 19u) ^ (x >> 10u); + } + uint32_t Summ(uint32_t x, uint32_t y, uint32_t z, uint32_t m, uint32_t e) + { + return x + y + z + m + e; + } + uint32_t newe(uint32_t x, uint32_t y) + { + return x + y; + } + uint32_t newa(uint32_t x, uint32_t y, uint32_t z) + { + return x + y + z; + } + uint32_t mult_xor(uint32_t x, uint32_t a, uint32_t b,uint32_t c) { + return (rotr(x,a)^rotr(x,b)^rotr(x,c)); + } + uint32_t compute_w(uint32_t m14, uint32_t m9,uint32_t m1, uint32_t m0){ + return (sig1(m14)+m9+sig0(m1)+m0); + } +SC_MODULE(sha256_core) +{ +public: + uint32_t k_constant; + uint32_t maj, xorA, ch, xorE, sum, newA, newE, w_temp, w_data; + std::array state; + + std::array m_state; + std::array block_dummy; + std::array m; + int i, l, k; + uint32_t j; + + bool next_dummy, init_transform_dummy, mode_dummy, zeroize_dummy; + blocking_in> w_core; + shared_in mode; + sc_biguint<512> out; + + master_out> digest_block; + + shared_in next_signal, init_signal, zeroize; + + SC_CTOR(sha256_core) + { + SC_THREAD(fsm); + } + + void fsm() + { + + state[0] = 0x0u; + state[1] = 0x0u; + state[2] = 0x0u; + state[3] = 0x0u; + state[4] = 0x0u; + state[5] = 0x0u; + state[6] = 0x0u; + state[7] = 0x0u; + m_state[0] = 0x0u; + m_state[1] = 0x0u; + m_state[2] = 0x0u; + m_state[3] = 0x0u; + m_state[4] = 0x0u; + m_state[5] = 0x0u; + m_state[6] = 0x0u; + m_state[7] = 0x0u; + w_data = 0x0u; + k_constant = 0x0u; + w_temp = 0x0u; + i = 0x0u; + + while (true) + + { + + w_core->read(block_dummy, "idle"); + init_signal->get(init_transform_dummy); + next_signal->get(next_dummy); + mode->get(mode_dummy); + zeroize->get(zeroize_dummy); + + if (init_transform_dummy == true) + { + + if(mode_dummy==false){ + // 224 + m_state[0] = 0xc1059ed8; + m_state[1] = 0x367cd507; + m_state[2] = 0x3070dd17; + m_state[3] = 0xf70e5939; + m_state[4] = 0xffc00b31; + m_state[5] = 0x68581511; + m_state[6] = 0x64f98fa7; + m_state[7] = 0xbefa4fa4; + k_constant = 0u; + } + else {// 256 + m_state[0] = 0x6a09e667u; + m_state[1] = 0xbb67ae85u; + m_state[2] = 0x3c6ef372u; + m_state[3] = 0xa54ff53au; + m_state[4] = 0x510e527fu; + m_state[5] = 0x9b05688cu; + m_state[6] = 0x1f83d9abu; + m_state[7] = 0x5be0cd19u; + k_constant = 0u; + } + + + } + for (k = 0u; k < 16u; ++k) + + { + m[k] = 0; + } + + for (j = 0u; j < 16u; ++j) + { + m[j] = block_dummy[15 - j]; + } + state[7] = m_state[7]; + state[6] = m_state[6]; + state[5] = m_state[5]; + state[4] = m_state[4]; + state[3] = m_state[3]; + state[2] = m_state[2]; + state[1] = m_state[1]; + state[0] = m_state[0]; + + + // states a b c + // m_states h h h + + j = 0u; + + for (i = 0u; i < 64u; ++i) + { + insert_state("ctrl_rotationss"); + //j = i; + if (i < 16) + { + + w_data = m[i]; + } + else + { + //w_temp = sig1(m[14]) + m[9] + sig0(m[1]) + m[0]; + w_temp = compute_w(m[14],m[9],m[1],m[0]); + for (l = 0u; l < 15u; ++l) + { + m[l] = m[(l + 1)]; + } + m[15] = w_temp; + w_data = w_temp; + } + + k_constant = K[i]; + + maj = majority(state[0], state[1], state[2]); + //xorA = rotr(state[0], 2u) ^ rotr(state[0], 13u) ^ rotr(state[0], 22u); + xorA = mult_xor(state[0],2u,13u,22u); + ch = choose(state[4], state[5], state[6]); + + //xorE = rotr(state[4], 6u) ^ rotr(state[4], 11u) ^ rotr(state[4], 25u); + xorE = mult_xor(state[4],6u,11u,25u); + sum = Summ(w_data, K[i], state[7u], ch, xorE); // m + newA = newa(xorA, maj, sum); + newE = newe(state[3], sum); + + state[7] = state[6]; + state[6] = state[5]; + state[5] = state[4]; + state[4] = newE; + state[3] = state[2]; + state[2] = state[1]; + state[1] = state[0]; + state[0] = newA; + } + + i = 0; + + insert_state("ctrl_done"); + m_state[7] = (state[7] + m_state[7]); // M_statea=H[0], States=A[b] + m_state[6] = (state[6] + m_state[6]); + m_state[5] = (state[5] + m_state[5]); + m_state[4] = (state[4] + m_state[4]); + m_state[3] = (state[3] + m_state[3]); + m_state[2] = (state[2] + m_state[2]); + m_state[1] = (state[1] + m_state[1]); + m_state[0] = (state[0] + m_state[0]); + + digest_block->master_write(m_state); + } + } +}; +#endif diff --git a/src/sha256/formal/model/tb/sha256_core_tests.h b/src/sha256/formal/model/tb/sha256_core_tests.h new file mode 100644 index 000000000..148166b40 --- /dev/null +++ b/src/sha256/formal/model/tb/sha256_core_tests.h @@ -0,0 +1,983 @@ +// ------------------------------------------------- +// Contact: contact@lubis-eda.com +// Author: Tobias Ludwig, Michael Schwarz +// ------------------------------------------------- +// SPDX-License-Identifier: Apache-2.0 +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// + +#ifndef SHA256_CORE_TESTS_H +#define SHA256_CORE_TESTS_H + +#include "systemc.h" +#include "Interfaces.h" +#include +#include +#include +#include +#include +#include +#include + +SC_MODULE(sha256_core_tests) +{ +public: + SC_CTOR(sha256_core_tests) + { + + SC_THREAD(tests); + } + blocking_out< int> out_mode; + blocking_out in_block; // Original type: 'wire [511:0]' + blocking_in out_block; // Original type: 'wire [255:0]' + +private: + void tests() + { + std::string in, out; + out_mode->write(0); + in = "Hello world"; + in_block->write(in); + out_block->read(out); + if (out == "64ec88ca00b268e5ba1a35678a1b5316d212f4f366b2477232534a8aeca37f3c") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Lubis EDA"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "d97541dcee8f0a27ff699624c553512f00e0d0096d1abd84e4272389d869678d") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Tu Kaiserslautern"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "28742eba07604f9d3d3b46870ab1d16225e129a86047c50d113222776de1768b") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Mostafa Elnahas"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "2f001374ae549a41a9235c4e4f4d07431219218dbe557d8f3295c6da09253cc0") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Tobias Ludwig"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "236244ccdbabb40dc5624dd44da2ea97b4aea5a950dc7ee3454d138b34bd7d9d") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Lubis EDA"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "d97541dcee8f0a27ff699624c553512f00e0d0096d1abd84e4272389d869678d") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "5145"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "766af62a6275002e9909af31d1f15e02609d9443de336c0ce13ba52cb3e56042") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + in = "Michael Shwarz"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "bd94211bd6edc570c1b6ab198b22b3562d658f1585a950a7f5d05171ba16c780") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Max"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "a1a5936d3b0f8a69fd62c91ed9990d3bd414c5e78c603e2837c65c9f46a93eb8") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Tim"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "aac09a648fc382b6f78897595486e691d00de9dfc742f3ba1930464b56eecda6") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Tom"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "81f3bf42a93cf18dece9321ac5c93313126eb5ca92164d74643e4cbf60ecde9c") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Luiz"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "0dd0029404cbe8bbad2cd84ec0f5089e4ca29d46719323b15595ffa765a88ffe") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Advaith"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "28c37e54d13bf521c4967aa26c30750b9703ba35bf27e2d2cff2933f48029abb") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Sandeep"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "b22db2a12b26ae466aa309491c247b7e517ca9502c6005310dc642eb96ab3c19") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Rohith"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "49e4d11bf1c03edc1c3804381a1fb6b9dbaa18b2264abe2ec05b91a9d633b587") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Christian"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "67e0082893e848c8706431c32dea6c3ca86c488ae24ee6b0661489cb8b3bb78a") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Kathrin"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "d89a423ad0035508ac3cc7a7525a379f28e06c3527ffa3d1562b97a074ea4472") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Fatemeh"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "6aa81ce731a2cfb14016b63d4803642a0fc616b0838892bbf77de7d12105bbdc") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Lilo"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "6ef693f0db886ad4bf27c4d0a77c7d9ad74300211c438689a70c5f0461c79694") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Stitch"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "acc870db91ebe17c3c5d593c244f9a1b1593c4d3d6509846618702f6fbf1047b") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + ; + in = "Goofy"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "ba89bbde79460200e4aeb0f6ea27e4a304adf58853f9ad124aa66726710463d8") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Pluto"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "8dad5f6a7dd2dcd8c35ec2fd7babb499bcad60d27d73fe73eca2ce025dfd3b47") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Donald duck"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "49d2118f9e78d5dcbafbdf0e6fd3979bc4d38ad26736ec2733e480e51e374778") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "aeriel"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "6179fc95ef559edb65dc55f565718c9e13167e774dc78c1f8687495ba98b8ead") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Mulan"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "cbaa9fe121b76892d534db5412b1082cf35c417ad7f2de572149a1eaf17789ac") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Woody"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "08bb39b964dcab376f5862d7e9c8f34b8f96cfaf380142246631d78178986125") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Buzz Alrdrin"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "45883804cf4f2f87688af4c94780dd4fa59a59d6f82c00ba490d4c732b6ec0e4") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Mickey Mouse"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "ac752a50e0f6d3cdecb914d6f4fe52250ac5a8ab7238e6b7b9cef0f4b6daf652") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Mini Mouse"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "b5b85dc31e212989ceef783a24098d92d98ce1d8c97e3842fc2694c514ac3cbe") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Simba"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "f9c552cca49d95db9e09a876bbd74eb833ee063e5ce058d121d53ad0271cedc4") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Mufasa"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "de83276e6b45237548b7d6c990b6fe6fd55de68a725e9ddeaf35666f7d93c475") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Scar"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "ed82f3944eeda21207da3b2214f58830ed56d728c0161297ccc03dea247102c2") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Timon"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "f2cc6496143be1714a909f7c955ccb82bf0aaefa6505a49cf3409dc1e789fdcc") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Nala"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "aa6a77d9ccef603ca1a6e07ea856d85d067f69d1fa94f01cf22cdfafd1777255") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Alaa Eldin"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "01570ab379e65f32949f55a29af26c885409e6db1b2dce9c1b6fa9f268e32df6") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Genie"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "bc8359eb1335ec654b14ddb264bdcaa1ffe6ebebe431ebb2c2ede4552026a8c2") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Winnie"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "168bb5b349fe144916def9f699ef4544353b89728aa377822a469274388b141b") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Piglet"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "d9b336af11e4299f3b75110fe04bbf8ccc99f8bd3e50f38db9614d7486bfefed") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Hercules"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "ef97a66f04394990d341c2a51eab11d6490d90f92318b50cc02988bd5fde0d88") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Zeus"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "0ff0ef099ecb754b08b36053f2a8327f0d5b470cc3656c9fd043b9d1a2d719f5") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Tigger"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "49df5f6cae1d5191dfbf17a3696ef9818ee5bc9b11e5179afe21f0a23f9e385e") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "philoctetes"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "1d321e3644f7384f47f6df2a7e8eebaf14f417d5b6d0cc20c8b1cd6d9f6b25a5") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "A"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "559aead08264d5795d3909718cdd05abd49572e84fe55590eef31a88a08fdffd") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "AB"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "38164fbd17603d73f696b8b4d72664d735bb6a7c88577687fd2ae33fd6964153") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "ABC"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "b5d4045c3f466fa91fe2cc6abe79232a1a57cdf104f7a26e716e0a1e2789df78") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "ABCDE"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "f0393febe8baaa55e32f7be2a7cc180bf34e52137d99e056c817a9c07b8f239a") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "ABCDEF"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "e9c0f8b575cbfcb42ab3b78ecc87efa3b011d9a5d10b09fa4e96f240bf6a82f5") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "ABCDEFG"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "e9a92a2ed0d53732ac13b031a27b071814231c8633c9f41844ccba884d482b16") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "ABCDEFGH"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "9ac2197d9258257b1ae8463e4214e4cd0a578bc1517f2415928b91be4283fc48") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "ABCDEFGHI"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "2cdf6e152315e807562e3265bea43b48fe82511242d002fc45a35d190067a3d0") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "ABCDEFGHIJ"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "261305762671a58cae5b74990bcfc236c2336fb04a0fbac626166d9491d2884c") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "ABCDEFGHIJK"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "62ee2337525d8cf6e6529cf8579d51191555cb32c033c903bedb8ca295e03f81") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "ABCDEFGHIJKL"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "922429ccdb7045d11143e2e3982a11afc11b537bf259d88d2425fa8806e86e78") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "ABCDEFGHIJKLM"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "170f5660fece35db218fece184b25e99771ddb3e8852850aba6f237624341ff4") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "N"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "8ce86a6ae65d3692e7305e2c58ac62eebd97d3d943e093f577da25c36988246b") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "NO"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "23794d91c53ae875c8e247d72561e35d9d06ee07c70c9e0dbcc977a6d161504a") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "NOP"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "692b4856a5ca2f45e38d56256b64b254865b31069ffe891f4e7876c9075f6b10") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "NOPQ"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "0006b627f94247c2991955b58be1821c649c649e4fdf445469bebc3762919d2d") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "NOPQR"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "29259343584eee776b38f7b89ddcee6b72a1aa71ee4aa9dc5d655a8ec8289ca7") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "NOPQRS"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "12be4169c73bf011b81f405d6b7f8bbf897d42a94fd4b88282efe3a2d100aa02") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "NOPQRST"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "20d5fd7f8e1f2f1b4656153a4800a04ea6d5c70dc7b24ea0b593ea13053232f8") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "NOPQRSTW"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "68201bf9788c3be4a6f411b95202ffcf3a40fa15bdd6074160a7ee1465cb25aa") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "NOPQRSTWX"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "233d4813648dd26e37304cb8c0c18ffeae60a656f6b95395a9068a6df0643149") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "XYZ"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "ade099751d2ea9f3393f0f32d20c6b980dd5d3b0989dea599b966ae0d3cd5a1e") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Super-Man"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "eef32a6ad13cd7ce249a66eedfebfdc019d3a07946029dc82bd60feff083aecf") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "BatMan"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "1175f8ee115c0a5da53eccfd2c852c4ee0c5fb513ce2d71f0c4a69c2faf370da") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "CatWoman"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "690aa6b8a7aa834ba0137fa8efbf4ce8287dbae06e2d0c1bab01142558d1a53d") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + + in = "Jadal"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "32ffebd23525c0424caa9aac71dcb26e66fd891ae28a8da6de5cf1761e00eacb") + cout << "test passed " << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + in = "Jadal"; + out_mode->write(1); + in_block->write(in); + out_block->read(out); + if (out == "5296ec14dd94b33683767b95b2d83078647f3aa082be16a8b975a9a5") + { + cout << "test passedsha224" << endl; + } + else + { + cout << out << endl; + cout << "test failed" << endl; + } + in = "Einstien"; + out_mode->write(0); + + in_block->write(in); + out_block->read(out); + if (out == "7a287e7aab0d8218a74531bdcc1ad83fd5fef954e67c66d346d1e51e6be0f66b") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } + in = "ad9dbaff7b64c8a7124d49712c962c1adc1295c311ec04b8b013bb3ad709d897ad9dbaff7b64c8a7124d49712c962c1adc1295c311ec04b8b013bb3ad709d897ad9dbaff7b64c8a7124d49712c962c1adc1295c311ec04b8b013bb3ad709d897ad9dbaff7b64c8a7124d49712c962c1adc1295c311ec04b8b013bb3ad709d897"; + out_mode->write(0); + in_block->write(in); + out_block->read(out); + if (out == "126f5f6829b04b22bbe37812955030fa4bb94aad0c853356857b3d2cdd138438") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + } +/* + + in = "ad9dbaff7b64c8a7124d49712c962c1adc1295c311ec04b8b013bb3ad709d897ad9dbaff7b64c8a7124d49712c962c1adc1295c311ec04b8b013bb3ad709d897ad9dbaff7b64c8a7124d49712c962c1adc1295c311ec04b8b013bb3ad709d897ad9dbaff7b64c8a7124d49712c962c1adc1295c311ec04b8b013bb3ad709d897"; + out_mode->write(0); + in_block->write(in); + out_block->read(out); + if (out == "abd613f1556aa411e2008c61b3045ab1e56a798494685993ffdc66d8") + cout << "test passed" << endl; + else + { + cout << out << endl; + cout << "test failed" << endl; + }*/ + } +}; + +#endif diff --git a/src/sha256/formal/model/tb/sha256_memory.h b/src/sha256/formal/model/tb/sha256_memory.h new file mode 100644 index 000000000..4a743b6c0 --- /dev/null +++ b/src/sha256/formal/model/tb/sha256_memory.h @@ -0,0 +1,185 @@ + +// ------------------------------------------------- +// Contact: contact@lubis-eda.com +// Author: Tobias Ludwig, Michael Schwarz +// ------------------------------------------------- +// SPDX-License-Identifier: Apache-2.0 +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// + +#ifndef SHA256_MEMORY_H +#define SHA256_MEMORY_H + +#include "systemc.h" +#include "Interfaces.h" +#include +#include +#include +#include +#include +#include +#include + +SC_MODULE(sha256_memory) +{ + +public: + blocking_in block; + blocking_out> w; + blocking_out< int> next; + blocking_out< int> ctrl_done; + blocking_out< int> init_transfrom; + + SC_CTOR(sha256_memory) + { + SC_THREAD(mem); + } + +private: + uint32_t m_blocklen = 0, m[16] = {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0}; + uint64_t m_bitlen = 0; + uint8_t m_data[64] = {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0}; + std::array mj = {0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0}; + std::string block_dummy; + + void update(const uint8_t *data, size_t length) + { + m_bitlen = 0; + m_blocklen = 0; + + for (size_t i = 0; i < length; i++) + { + m_data[m_blocklen++] = data[i]; + + if (m_blocklen == 64) + { + + for (uint8_t i = 0, j = 0; i < 16; i++, j += 4) + { + m[i] = (m_data[j] << 24) | (m_data[j + 1] << 16) | (m_data[j + 2] << 8) | (m_data[j + 3]); + } + for (int i = 0; i < 16; i++) + { + + mj[i] = m[i]; + } + + if (m_bitlen < 512) + { + + ctrl_done->write(0); + next->write(0); + init_transfrom->write(1); + w->write(mj); + } + + else + { + ctrl_done->write(0); + next->write(1); + init_transfrom->write(0); + w->write(mj); + } + + m_bitlen = m_bitlen + 512; + m_blocklen = 0; + } + } + } + + void update(const std::string &data) + { + update(reinterpret_cast(data.c_str()), data.size()); + } + + void mem() + + { + + while (true) + { + + block->read(block_dummy); + + update(block_dummy); + + uint64_t i = m_blocklen; + uint8_t end = m_blocklen < 56 ? 56 : 64; + m_data[i++] = 0x80; // Append a bit 1 + while (i < end) + + { + m_data[i++] = 0x00; // Pad with zeros + } + + if (m_blocklen >= 56) + { + for (uint8_t i = 0, j = 0; i < 16; i++, j += 4) + + { + m[i] = (m_data[j] << 24) | (m_data[j + 1] << 16) | (m_data[j + 2] << 8) | (m_data[j + 3]); + } + + for (int i = 0; i < 16; i++) + { + + mj[i] = m[i]; + } + + if (m_bitlen < 512) + { + ctrl_done->write(0); + next->write(0); + init_transfrom->write(1); + w->write(mj); + } + + else + { + ctrl_done->write(0); + next->write(1); + init_transfrom->write(0); + w->write(mj); + } + memset(m_data, 0, 56); + } + + // Append to the padding the total message's length in bits and transform. + m_bitlen += m_blocklen * 8; + m_data[63] = m_bitlen; + m_data[62] = m_bitlen >> 8; + m_data[61] = m_bitlen >> 16; + m_data[60] = m_bitlen >> 24; + m_data[59] = m_bitlen >> 32; + m_data[58] = m_bitlen >> 40; + m_data[57] = m_bitlen >> 48; + m_data[56] = m_bitlen >> 56; + for (uint8_t i = 0, j = 0; i < 16; i++, j += 4) + + { + m[i] = (m_data[j] << 24) | (m_data[j + 1] << 16) | (m_data[j + 2] << 8) | (m_data[j + 3]); + } + for (uint32_t i = 0; i < 16; i++) + { + + mj[i] = m[i]; + } + ctrl_done->write(1); + next->write(0); + init_transfrom->write(0); + w->write(mj); + } + } +}; +#endif \ No newline at end of file diff --git a/src/sha256/formal/properties/fv_constraints.sv b/src/sha256/formal/properties/fv_constraints.sv new file mode 100644 index 000000000..a945bc1cc --- /dev/null +++ b/src/sha256/formal/properties/fv_constraints.sv @@ -0,0 +1,54 @@ + +// ------------------------------------------------- +// 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( init, next, reset_n, clk, mode); + input bit init, next, reset_n, clk, mode; + reg init_reg; + + default clocking default_clk @(posedge clk); endclocking + remove_int_next_together_a: assume property (remove_int_next_together); + property remove_int_next_together; + !(init && next); + endproperty + + int_next_order_a: assume property (int_next_order); + property int_next_order; + !init_reg |-> !next; + endproperty + + + + always @ (posedge clk or negedge reset_n) + begin : init_reg_order + if (!reset_n) + init_reg <= 1'b0; + else if (init) + init_reg <= 1'b1; + end + +endmodule + +bind sha256_core fv_constraints inst2( + .init(init_cmd), + .next(next_cmd), + .reset_n(reset_n), + .clk(clk), + .mode(mode) +); \ No newline at end of file diff --git a/src/sha256/formal/properties/fv_coverpoints.sv b/src/sha256/formal/properties/fv_coverpoints.sv new file mode 100644 index 000000000..f1ddeb0b7 --- /dev/null +++ b/src/sha256/formal/properties/fv_coverpoints.sv @@ -0,0 +1,48 @@ +// ------------------------------------------------- +// Contact: contact@lubis-eda.com +// Author: Tobias Ludwig, Michael Schwarz +// ------------------------------------------------- +// SPDX-License-Identifier: Apache-2.0 +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// + +module fv_coverpoints_m( + input logic clk, + input logic reset_n +); + + default clocking default_clk @(posedge clk); endclocking + + //Cover zeroize: + //Assert zeroize input and check the status of all registers. All registers/internal memories should be cleared. + cover_zeroize: cover property(disable iff(!reset_n) sha256_core.zeroize ); + cover_zeroize_after_next: cover property(disable iff(!reset_n) sha256_core.zeroize && sha256_core.next_cmd ); + + //Cover modes: + //Cover all 4 different modes for SHA512 + cover_mode_224: cover property(disable iff(!reset_n) sha256_core.mode == 0 && sha256_core.init_cmd ); + cover_mode_256: cover property(disable iff(!reset_n) sha256_core.mode == 1 && sha256_core.init_cmd ); + + + //Cover: i>16 + cover_rnd_cnt_bigger_16: cover property(disable iff(!reset_n) sha256_core.t_ctr_reg == 17 ##1 sha256_core.t_ctr_reg == 17[->1] ); + + + + +endmodule +bind sha256_core fv_coverpoints_m fv_coverpoints( + .clk(clk), + .reset_n(reset_n) +); \ No newline at end of file diff --git a/src/sha256/formal/properties/fv_sha256.sv b/src/sha256/formal/properties/fv_sha256.sv new file mode 100644 index 000000000..356e51c80 --- /dev/null +++ b/src/sha256/formal/properties/fv_sha256.sv @@ -0,0 +1,600 @@ +// ------------------------------------------------- +// Contact: contact@lubis-eda.com +// Author: Tobias Ludwig, Michael Schwarz +// ------------------------------------------------- +// SPDX-License-Identifier: Apache-2.0 +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// + +import fv_sha256_pkg::*; + +module fv_sha_256_m( + input bit rst, + input bit clk, + input bit unsigned [31:0] digest_out_0, + input bit unsigned [31:0] digest_out_1, + input bit unsigned [31:0] digest_out_2, + input bit unsigned [31:0] digest_out_3, + input bit unsigned [31:0] digest_out_4, + input bit unsigned [31:0] digest_out_5, + input bit unsigned [31:0] digest_out_6, + input bit unsigned [31:0] digest_out_7, + input bit block_init, + input bit block_mode, + input bit block_next, + input bit unsigned [31:0] block_in_0, + input bit unsigned [31:0] block_in_1, + input bit unsigned [31:0] block_in_2, + input bit unsigned [31:0] block_in_3, + input bit unsigned [31:0] block_in_4, + input bit unsigned [31:0] block_in_5, + input bit unsigned [31:0] block_in_6, + input bit unsigned [31:0] block_in_7, + input bit unsigned [31:0] block_in_8, + input bit unsigned [31:0] block_in_9, + input bit unsigned [31:0] block_in_10, + input bit unsigned [31:0] block_in_11, + input bit unsigned [31:0] block_in_12, + input bit unsigned [31:0] block_in_13, + input bit unsigned [31:0] block_in_14, + input bit unsigned [31:0] block_in_15, + input bit block_zeroize, + input bit block_in_valid, + input bit digest_valid, + input bit block_in_ready, + input bit unsigned [5:0] i, + input bit unsigned [31:0] W_0, + input bit unsigned [31:0] W_1, + input bit unsigned [31:0] W_2, + input bit unsigned [31:0] W_3, + input bit unsigned [31:0] W_4, + input bit unsigned [31:0] W_5, + input bit unsigned [31:0] W_6, + input bit unsigned [31:0] W_7, + input bit unsigned [31:0] W_8, + input bit unsigned [31:0] W_9, + input bit unsigned [31:0] W_10, + input bit unsigned [31:0] W_11, + input bit unsigned [31:0] W_12, + input bit unsigned [31:0] W_13, + input bit unsigned [31:0] W_14, + input bit unsigned [31:0] W_15, + input bit unsigned [31:0] H_0, + input bit unsigned [31:0] H_1, + input bit unsigned [31:0] H_2, + input bit unsigned [31:0] H_3, + input bit unsigned [31:0] H_4, + input bit unsigned [31:0] H_5, + input bit unsigned [31:0] H_6, + input bit unsigned [31:0] H_7, + input bit unsigned [31:0] a, + input bit unsigned [31:0] b, + input bit unsigned [31:0] c, + input bit unsigned [31:0] d, + input bit unsigned [31:0] e, + input bit unsigned [31:0] f, + input bit unsigned [31:0] g, + input bit unsigned [31:0] h, + input bit idle, + input bit ctrl_rotationss, + input bit ctrl_done +); + + +default clocking default_clk @(posedge clk); endclocking +logic [15:0][31:0] w; +logic [3:0] j; + +assign j = i[3:0]; +assign w = {W_15,W_14,W_13,W_12,W_11,W_10,W_9,W_8,W_7,W_6,W_5,W_4,W_3,W_2,W_1,W_0}; + +sequence reset_sequence; + !rst ##1 rst; +endsequence + + +reset_a: assert property (reset_p); +property reset_p; + reset_sequence |-> + idle && + i == 'sd0 && + W_0 == 0 && + W_10 == 0 && + W_11 == 0 && + W_12 == 0 && + W_13 == 0 && + W_14 == 0 && + W_15 == 0 && + W_1 == 0 && + W_2 == 0 && + W_3 == 0 && + W_4 == 0 && + W_5 == 0 && + W_6 == 0 && + W_7 == 0 && + W_8 == 0 && + W_9 == 0 && + H_0 == 0 && + H_1 == 0 && + H_2 == 0 && + H_3 == 0 && + H_4 == 0 && + H_5 == 0 && + H_6 == 0 && + H_7 == 0 && + a == 0 && + b == 0 && + c == 0 && + d == 0 && + e == 0 && + f == 0 && + g == 0 && + h == 0 && + digest_valid == 0 && + block_in_ready == 1; +endproperty + + +DONE_to_IDLE_a: assert property (disable iff(!rst) DONE_to_IDLE_p); +property DONE_to_IDLE_p; + ctrl_done +|-> + ##1 + idle && + digest_out_0 == ($past(a, 1) + $past(H_0, 1)) && + digest_out_1 == ($past(b, 1) + $past(H_1, 1)) && + digest_out_2 == ($past(c, 1) + $past(H_2, 1)) && + digest_out_3 == ($past(d, 1) + $past(H_3, 1)) && + digest_out_4 == ($past(e, 1) + $past(H_4, 1)) && + digest_out_5 == ($past(f, 1) + $past(H_5, 1)) && + digest_out_6 == ($past(g, 1) + $past(H_6, 1)) && + digest_out_7 == ($past(h, 1) + $past(H_7, 1)) && + i == $past(i, 1) && + W_0 == $past(W_0, 1) && + W_10 == $past(W_10, 1) && + W_11 == $past(W_11, 1) && + W_12 == $past(W_12, 1) && + W_13 == $past(W_13, 1) && + W_14 == $past(W_14, 1) && + W_15 == $past(W_15, 1) && + W_1 == $past(W_1, 1) && + W_2 == $past(W_2, 1) && + W_3 == $past(W_3, 1) && + W_4 == $past(W_4, 1) && + W_5 == $past(W_5, 1) && + W_6 == $past(W_6, 1) && + W_7 == $past(W_7, 1) && + W_8 == $past(W_8, 1) && + W_9 == $past(W_9, 1) && + H_0 == ($past(a, 1) + $past(H_0, 1)) && + H_1 == ($past(b, 1) + $past(H_1, 1)) && + H_2 == ($past(c, 1) + $past(H_2, 1)) && + H_3 == ($past(d, 1) + $past(H_3, 1)) && + H_4 == ($past(e, 1) + $past(H_4, 1)) && + H_5 == ($past(f, 1) + $past(H_5, 1)) && + H_6 == ($past(g, 1) + $past(H_6, 1)) && + H_7 == ($past(h, 1) + $past(H_7, 1)) && + a == $past(a, 1) && + b == $past(b, 1) && + c == $past(c, 1) && + d == $past(d, 1) && + e == $past(e, 1) && + f == $past(f, 1) && + g == $past(g, 1) && + h == $past(h, 1) && + digest_valid == 1 && + block_in_ready == 1; +endproperty + + +SHA_Rounds_to_DONE_a: assert property (disable iff(!rst) SHA_Rounds_to_DONE_p); +property SHA_Rounds_to_DONE_p; + ctrl_rotationss && + (i >= 'sd16) && + (('sd1 + i) >= 'sd64) +|-> + ##1 (digest_valid == 0) and + ##1 (block_in_ready == 0) and + ##1 + ctrl_done && + i == 'sd0 && + W_0 == $past(W_1, 1) && + W_10 == $past(W_11, 1) && + W_11 == $past(W_12, 1) && + W_12 == $past(W_13, 1) && + W_13 == $past(W_14, 1) && + W_14 == $past(W_15, 1) && + W_15 == $past(compute_w(W_14,W_9,W_1,W_0)) && + W_1 == $past(W_2, 1) && + W_2 == $past(W_3, 1) && + W_3 == $past(W_4, 1) && + W_4 == $past(W_5, 1) && + W_5 == $past(W_6, 1) && + W_6 == $past(W_7, 1) && + W_7 == $past(W_8, 1) && + W_8 == $past(W_9, 1) && + W_9 == $past(W_10, 1) && + H_0 == $past(H_0, 1) && + H_1 == $past(H_1, 1) && + H_2 == $past(H_2, 1) && + H_3 == $past(H_3, 1) && + H_4 == $past(H_4, 1) && + H_5 == $past(H_5, 1) && + H_6 == $past(H_6, 1) && + H_7 == $past(H_7, 1) && + a == $past(newa(mult_xor(a, 2, 13, 22),majority(a,b,c),Summ(compute_w(W_14,W_9,W_1,W_0),K[i],h,choose(e,f,g),mult_xor(e, 6, 11, 25)))) && + b == $past(a, 1) && + c == $past(b, 1) && + d == $past(c, 1) && + e == $past(newe(d,Summ(compute_w(W_14,W_9,W_1,W_0),K[i],h,choose(e,f,g),mult_xor(e,6,11,25)))) && + f == $past(e, 1) && + g == $past(f, 1) && + h == $past(g, 1); +endproperty + + +SHA_Rounds_to_SHA_Rounds_before_16_a: assert property (disable iff(!rst) SHA_Rounds_to_SHA_Rounds_before_16_p); +property SHA_Rounds_to_SHA_Rounds_before_16_p; + ctrl_rotationss && + (i < 'sd16) +|-> + ##1 (digest_valid == 0) and + ##1 (block_in_ready == 0) and + ##1 + ctrl_rotationss && + i == ('sd1 + $past(i, 1)) && + W_0 == $past(W_0, 1) && + W_10 == $past(W_10, 1) && + W_11 == $past(W_11, 1) && + W_12 == $past(W_12, 1) && + W_13 == $past(W_13, 1) && + W_14 == $past(W_14, 1) && + W_15 == $past(W_15, 1) && + W_1 == $past(W_1, 1) && + W_2 == $past(W_2, 1) && + W_3 == $past(W_3, 1) && + W_4 == $past(W_4, 1) && + W_5 == $past(W_5, 1) && + W_6 == $past(W_6, 1) && + W_7 == $past(W_7, 1) && + W_8 == $past(W_8, 1) && + W_9 == $past(W_9, 1) && + H_0 == $past(H_0, 1) && + H_1 == $past(H_1, 1) && + H_2 == $past(H_2, 1) && + H_3 == $past(H_3, 1) && + H_4 == $past(H_4, 1) && + H_5 == $past(H_5, 1) && + H_6 == $past(H_6, 1) && + H_7 == $past(H_7, 1) && + a == $past(newa(mult_xor(a, 2, 13, 22),majority(a,b,c),Summ(w[j],K[i],h,choose(e,f,g),mult_xor(e, 6, 11, 25)))) && + b == $past(a, 1) && + c == $past(b, 1) && + d == $past(c, 1) && + e == $past(newe(d,Summ(w[j],K[i],h,choose(e,f,g),mult_xor(e,6,11,25)))) && + f == $past(e, 1) && + g == $past(f, 1) && + h == $past(g, 1); +endproperty + + +SHA_Rounds_to_SHA_Rounds_after_16_a: assert property (disable iff(!rst) SHA_Rounds_to_SHA_Rounds_after_16_p); +property SHA_Rounds_to_SHA_Rounds_after_16_p; + ctrl_rotationss && + (i >= 'sd16) && + (('sd1 + i) < 'sd64) +|-> + ##1 (digest_valid == 0) and + ##1 (block_in_ready == 0) and + ##1 + ctrl_rotationss && + i == ('sd1 + $past(i, 1)) && + W_0 == $past(W_1, 1) && + W_10 == $past(W_11, 1) && + W_11 == $past(W_12, 1) && + W_12 == $past(W_13, 1) && + W_13 == $past(W_14, 1) && + W_14 == $past(W_15, 1) && + W_15 == $past(compute_w(W_14,W_9,W_1,W_0)) && + W_1 == $past(W_2, 1) && + W_2 == $past(W_3, 1) && + W_3 == $past(W_4, 1) && + W_4 == $past(W_5, 1) && + W_5 == $past(W_6, 1) && + W_6 == $past(W_7, 1) && + W_7 == $past(W_8, 1) && + W_8 == $past(W_9, 1) && + W_9 == $past(W_10, 1) && + H_0 == $past(H_0, 1) && + H_1 == $past(H_1, 1) && + H_2 == $past(H_2, 1) && + H_3 == $past(H_3, 1) && + H_4 == $past(H_4, 1) && + H_5 == $past(H_5, 1) && + H_6 == $past(H_6, 1) && + H_7 == $past(H_7, 1) && + a == $past(newa(mult_xor(a, 2, 13, 22),majority(a,b,c),Summ(compute_w(W_14,W_9,W_1,W_0),K[i],h,choose(e,f,g),mult_xor(e, 6, 11, 25)))) && + b == $past(a, 1) && + c == $past(b, 1) && + d == $past(c, 1) && + e == $past(newe(d,Summ(compute_w(W_14,W_9,W_1,W_0),K[i],h,choose(e,f,g),mult_xor(e,6,11,25)))) && + f == $past(e, 1) && + g == $past(f, 1) && + h == $past(g, 1); +endproperty + + +IDLE_to_SHA_Rounds_224_a: assert property (disable iff(!rst) IDLE_to_SHA_Rounds_224_p); +property IDLE_to_SHA_Rounds_224_p; + idle && + block_in_valid && + block_init && + !block_mode +|-> + ##1 (digest_valid == 0) and + ##1 (block_in_ready == 0) and + ##1 + ctrl_rotationss && + i == 'sd0 && + W_0 == $past(block_in_15, 1) && + W_10 == $past(block_in_5, 1) && + W_11 == $past(block_in_4, 1) && + W_12 == $past(block_in_3, 1) && + W_13 == $past(block_in_2, 1) && + W_14 == $past(block_in_1, 1) && + W_15 == $past(block_in_0, 1) && + W_1 == $past(block_in_14, 1) && + W_2 == $past(block_in_13, 1) && + W_3 == $past(block_in_12, 1) && + W_4 == $past(block_in_11, 1) && + W_5 == $past(block_in_10, 1) && + W_6 == $past(block_in_9, 1) && + W_7 == $past(block_in_8, 1) && + W_8 == $past(block_in_7, 1) && + W_9 == $past(block_in_6, 1) && + H_0 == 32'd3238371032 && + H_1 == 32'd914150663 && + H_2 == 32'd812702999 && + H_3 == 32'd4144912697 && + H_4 == 32'd4290775857 && + H_5 == 32'd1750603025 && + H_6 == 32'd1694076839 && + H_7 == 32'd3204075428 && + a == 32'd3238371032 && + b == 32'd914150663 && + c == 32'd812702999 && + d == 32'd4144912697 && + e == 32'd4290775857 && + f == 32'd1750603025 && + g == 32'd1694076839 && + h == 32'd3204075428; +endproperty + + +IDLE_to_SHA_Rounds_256_a: assert property (disable iff(!rst) IDLE_to_SHA_Rounds_256_p); +property IDLE_to_SHA_Rounds_256_p; + idle && + block_in_valid && + block_init && + block_mode +|-> + ##1 (digest_valid == 0) and + ##1 (block_in_ready == 0) and + ##1 + ctrl_rotationss && + i == 'sd0 && + W_0 == $past(block_in_15, 1) && + W_10 == $past(block_in_5, 1) && + W_11 == $past(block_in_4, 1) && + W_12 == $past(block_in_3, 1) && + W_13 == $past(block_in_2, 1) && + W_14 == $past(block_in_1, 1) && + W_15 == $past(block_in_0, 1) && + W_1 == $past(block_in_14, 1) && + W_2 == $past(block_in_13, 1) && + W_3 == $past(block_in_12, 1) && + W_4 == $past(block_in_11, 1) && + W_5 == $past(block_in_10, 1) && + W_6 == $past(block_in_9, 1) && + W_7 == $past(block_in_8, 1) && + W_8 == $past(block_in_7, 1) && + W_9 == $past(block_in_6, 1) && + H_0 == 32'd1779033703 && + H_1 == 32'd3144134277 && + H_2 == 32'd1013904242 && + H_3 == 32'd2773480762 && + H_4 == 32'd1359893119 && + H_5 == 32'd2600822924 && + H_6 == 32'd528734635 && + H_7 == 32'd1541459225 && + a == 32'd1779033703 && + b == 32'd3144134277 && + c == 32'd1013904242 && + d == 32'd2773480762 && + e == 32'd1359893119 && + f == 32'd2600822924 && + g == 32'd528734635 && + h == 32'd1541459225; +endproperty + + +IDLE_to_SHA_Rounds_next_a: assert property (disable iff(!rst) IDLE_to_SHA_Rounds_next_p); +property IDLE_to_SHA_Rounds_next_p; + idle && + block_in_valid && + !block_init +|-> + ##1 (digest_valid == 0) and + ##1 (block_in_ready == 0) and + ##1 + ctrl_rotationss && + i == 'sd0 && + W_0 == $past(block_in_15, 1) && + W_10 == $past(block_in_5, 1) && + W_11 == $past(block_in_4, 1) && + W_12 == $past(block_in_3, 1) && + W_13 == $past(block_in_2, 1) && + W_14 == $past(block_in_1, 1) && + W_15 == $past(block_in_0, 1) && + W_1 == $past(block_in_14, 1) && + W_2 == $past(block_in_13, 1) && + W_3 == $past(block_in_12, 1) && + W_4 == $past(block_in_11, 1) && + W_5 == $past(block_in_10, 1) && + W_6 == $past(block_in_9, 1) && + W_7 == $past(block_in_8, 1) && + W_8 == $past(block_in_7, 1) && + W_9 == $past(block_in_6, 1) && + H_0 == $past(H_0, 1) && + H_1 == $past(H_1, 1) && + H_2 == $past(H_2, 1) && + H_3 == $past(H_3, 1) && + H_4 == $past(H_4, 1) && + H_5 == $past(H_5, 1) && + H_6 == $past(H_6, 1) && + H_7 == $past(H_7, 1) && + a == $past(H_0, 1) && + b == $past(H_1, 1) && + c == $past(H_2, 1) && + d == $past(H_3, 1) && + e == $past(H_4, 1) && + f == $past(H_5, 1) && + g == $past(H_6, 1) && + h == $past(H_7, 1); +endproperty + + +idle_wait_a: assert property (disable iff(!rst) idle_wait_p); +property idle_wait_p; + idle && + !block_in_valid +|-> + ##1 + idle && + i == $past(i, 1) && + W_0 == $past(W_0, 1) && + W_10 == $past(W_10, 1) && + W_11 == $past(W_11, 1) && + W_12 == $past(W_12, 1) && + W_13 == $past(W_13, 1) && + W_14 == $past(W_14, 1) && + W_15 == $past(W_15, 1) && + W_1 == $past(W_1, 1) && + W_2 == $past(W_2, 1) && + W_3 == $past(W_3, 1) && + W_4 == $past(W_4, 1) && + W_5 == $past(W_5, 1) && + W_6 == $past(W_6, 1) && + W_7 == $past(W_7, 1) && + W_8 == $past(W_8, 1) && + W_9 == $past(W_9, 1) && + H_0 == $past(H_0, 1) && + H_1 == $past(H_1, 1) && + H_2 == $past(H_2, 1) && + H_3 == $past(H_3, 1) && + H_4 == $past(H_4, 1) && + H_5 == $past(H_5, 1) && + H_6 == $past(H_6, 1) && + H_7 == $past(H_7, 1) && + a == $past(a, 1) && + b == $past(b, 1) && + c == $past(c, 1) && + d == $past(d, 1) && + e == $past(e, 1) && + f == $past(f, 1) && + g == $past(g, 1) && + h == $past(h, 1) && + digest_valid == $past(digest_valid) && + block_in_ready == 1; +endproperty + + +endmodule + + + +bind sha256_core fv_sha_256_m fv_sha256( + .rst(sha256_core.reset_n && !sha256_core.zeroize), + .clk(sha256_core.clk), + .digest_out_0(sha256_core.digest [255:224]), + .digest_out_1(sha256_core.digest [223:192]), + .digest_out_2(sha256_core.digest [191:160]), + .digest_out_3(sha256_core.digest [159:128]), + .digest_out_4(sha256_core.digest [127:96]), + .digest_out_5(sha256_core.digest [95:64]), + .digest_out_6(sha256_core.digest [63:32]), + .digest_out_7(sha256_core.digest [31:0]), + .block_init(sha256_core.init_cmd), + .block_mode(sha256_core.mode), + .block_next(sha256_core.next_cmd), + .block_in_0(sha256_core.block_msg[31:0]), + .block_in_1(sha256_core.block_msg[63:32]), + .block_in_2(sha256_core.block_msg[95:64]), + .block_in_3(sha256_core.block_msg[127:96]), + .block_in_4(sha256_core.block_msg[159:128]), + .block_in_5(sha256_core.block_msg[191:160]), + .block_in_6(sha256_core.block_msg[223:192]), + .block_in_7(sha256_core.block_msg[255:224]), + .block_in_8(sha256_core.block_msg[287:256]), + .block_in_9(sha256_core.block_msg[319:288]), + .block_in_10(sha256_core.block_msg[351:320]), + .block_in_11(sha256_core.block_msg[383:352]), + .block_in_12(sha256_core.block_msg[415:384]), + .block_in_13(sha256_core.block_msg[447:416]), + .block_in_14(sha256_core.block_msg[479:448]), + .block_in_15(sha256_core.block_msg[511:480]), + .block_zeroize(sha256_core.zeroize), + .block_in_valid((sha256_core.init_cmd) || (sha256_core.next_cmd)), + .digest_valid(sha256_core.digest_valid), + .block_in_ready(sha256_core.ready), + .i(sha256_core.t_ctr_reg), + .W_0(sha256_core.w_mem_inst.w_mem[00]), + .W_1(sha256_core.w_mem_inst.w_mem[01]), + .W_2(sha256_core.w_mem_inst.w_mem[02]), + .W_3(sha256_core.w_mem_inst.w_mem[03]), + .W_4(sha256_core.w_mem_inst.w_mem[04]), + .W_5(sha256_core.w_mem_inst.w_mem[05]), + .W_6(sha256_core.w_mem_inst.w_mem[06]), + .W_7(sha256_core.w_mem_inst.w_mem[07]), + .W_8(sha256_core.w_mem_inst.w_mem[08]), + .W_9(sha256_core.w_mem_inst.w_mem[09]), + .W_10(sha256_core.w_mem_inst.w_mem[10]), + .W_11(sha256_core.w_mem_inst.w_mem[11]), + .W_12(sha256_core.w_mem_inst.w_mem[12]), + .W_13(sha256_core.w_mem_inst.w_mem[13]), + .W_14(sha256_core.w_mem_inst.w_mem[14]), + .W_15(sha256_core.w_mem_inst.w_mem[15]), + .H_0(sha256_core.H0_reg), + .H_1(sha256_core.H1_reg), + .H_2(sha256_core.H2_reg), + .H_3(sha256_core.H3_reg), + .H_4(sha256_core.H4_reg), + .H_5(sha256_core.H5_reg), + .H_6(sha256_core.H6_reg), + .H_7(sha256_core.H7_reg), + .a(sha256_core.a_reg), + .b(sha256_core.b_reg), + .c(sha256_core.c_reg), + .d(sha256_core.d_reg), + .e(sha256_core.e_reg), + .f(sha256_core.f_reg), + .g(sha256_core.g_reg), + .h(sha256_core.h_reg), + .idle(sha256_core.sha256_ctrl_reg==2'h0), + .ctrl_rotationss(sha256_core.sha256_ctrl_reg==2'h1), + .ctrl_done(sha256_core.sha256_ctrl_reg==2'h2) +); + + + diff --git a/src/sha256/formal/properties/fv_sha256_pkg.sv b/src/sha256/formal/properties/fv_sha256_pkg.sv new file mode 100644 index 000000000..71d9803de --- /dev/null +++ b/src/sha256/formal/properties/fv_sha256_pkg.sv @@ -0,0 +1,75 @@ +// ------------------------------------------------- +// Contact: contact@lubis-eda.com +// Author: Tobias Ludwig, Michael Schwarz +// ------------------------------------------------- +// SPDX-License-Identifier: Apache-2.0 +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// +package fv_sha256_pkg; + +typedef bit unsigned [31:0] a_unsigned_32_64 [63:0]; + +// Constants + +parameter a_unsigned_32_64 K = '{ 0:'h428A2F98, 1:'h71374491, 2:'hB5C0FBCF, 3:'hE9B5DBA5, 4:'h3956C25B, 5:'h59F111F1, 6:'h923F82A4, 7:'hAB1C5ED5, 8:'hD807AA98, 9:'h12835B01, 10:'h243185BE, 11:'h550C7DC3, 12:'h72BE5D74, 13:'h80DEB1FE, 14:'h9BDC06A7, 15:'hC19BF174, 16:'hE49B69C1, 17:'hEFBE4786, 18:'hFC19DC6, 19:'h240CA1CC, 20:'h2DE92C6F, 21:'h4A7484AA, 22:'h5CB0A9DC, 23:'h76F988DA, 24:'h983E5152, 25:'hA831C66D, 26:'hB00327C8, 27:'hBF597FC7, 28:'hC6E00BF3, 29:'hD5A79147, 30:'h6CA6351, 31:'h14292967, 32:'h27B70A85, 33:'h2E1B2138, 34:'h4D2C6DFC, 35:'h53380D13, 36:'h650A7354, 37:'h766A0ABB, 38:'h81C2C92E, 39:'h92722C85, 40:'hA2BFE8A1, 41:'hA81A664B, 42:'hC24B8B70, 43:'hC76C51A3, 44:'hD192E819, 45:'hD6990624, 46:'hF40E3585, 47:'h106AA070, 48:'h19A4C116, 49:'h1E376C08, 50:'h2748774C, 51:'h34B0BCB5, 52:'h391C0CB3, 53:'h4ED8AA4A, 54:'h5B9CCA4F, 55:'h682E6FF3, 56:'h748F82EE, 57:'h78A5636F, 58:'h84C87814, 59:'h8CC70208, 60:'h90BEFFFA, 61:'hA4506CEB, 62:'hBEF9A3F7, 63:'hC67178F2 }; + + +// Functions + +function bit unsigned [31:0] Summ(bit unsigned [31:0] x, bit unsigned [31:0] y, bit unsigned [31:0] z, bit unsigned [31:0] m, bit unsigned [31:0] e); + return ((((x + y) + z) + m) + e); +endfunction + +function bit unsigned [31:0] choose(bit unsigned [31:0] e, bit unsigned [31:0] f, bit unsigned [31:0] g); + return ((e & f) ^ (~e & g)); +endfunction + +function bit unsigned [31:0] compute_w(bit unsigned [31:0] m14, bit unsigned [31:0] m9, bit unsigned [31:0] m1, bit unsigned [31:0] m0); + return (((sig1(m14) + m9) + sig0(m1)) + m0); +endfunction + +function bit unsigned [31:0] majority(bit unsigned [31:0] a, bit unsigned [31:0] b, bit unsigned [31:0] c); + return ((a & (b | c)) | (b & c)); +endfunction + +function bit unsigned [31:0] mult_xor(bit unsigned [31:0] x, bit unsigned [31:0] a, bit unsigned [31:0] b, bit unsigned [31:0] c); + return ((rotr(x, a) ^ rotr(x, b)) ^ rotr(x, c)); +endfunction + +function bit unsigned [31:0] newa(bit unsigned [31:0] x, bit unsigned [31:0] y, bit unsigned [31:0] z); + return ((x + y) + z); +endfunction + +function bit unsigned [31:0] newe(bit unsigned [31:0] x, bit unsigned [31:0] y); + return (x + y); +endfunction + +function bit unsigned [31:0] past_m(bit unsigned [5:0]i,bit unsigned [31:0] m_0,bit unsigned [31:0] m_1,bit unsigned [31:0] m_2,bit unsigned [31:0] m_3,bit unsigned [31:0] m_4,bit unsigned [31:0] m_5,bit unsigned [31:0] m_6,bit unsigned [31:0] m_7,bit unsigned [31:0] m_8,bit unsigned [31:0] m_9,bit unsigned [31:0] m_10,bit unsigned [31:0] m_11,bit unsigned [31:0] m_12,bit unsigned [31:0] m_13,bit unsigned [31:0] m_14,bit unsigned [31:0] m_15); + return ((i == 'sd0 ? m_0 : (i == 'sd1) ? m_1 : (i == 'sd2) ? m_2 : (i == 'sd3) ? m_3 : (i == 'sd4) ? m_4 : (i == 'sd5) ? m_5 : (i == 'sd6) ? m_6 : (i == 'sd7) ? m_7 : (i == 'sd8) ? m_8 : (i == 'sd9) ? m_9 : (i == 'sd10) ? m_10 : (i == 'sd11) ? m_11 : (i == 'sd12) ? m_12 : (i == 'sd13) ? m_13 : (i == 'sd14) ? m_14 : m_15)); +endfunction + +function bit unsigned [31:0] rotr(bit unsigned [31:0] x, bit unsigned [31:0] n); + return ((x >> n) | (x << (32 - n))); +endfunction + +function bit unsigned [31:0] sig0(bit unsigned [31:0] x); + return ((rotr(x, 7) ^ rotr(x, 18)) ^ (x >> 3)); +endfunction + +function bit unsigned [31:0] sig1(bit unsigned [31:0] x); + return ((rotr(x, 17) ^ rotr(x, 19)) ^ (x >> 10)); +endfunction + + +endpackage diff --git a/src/sha256/formal/readme.md b/src/sha256/formal/readme.md new file mode 100644 index 000000000..1300932fc --- /dev/null +++ b/src/sha256/formal/readme.md @@ -0,0 +1,61 @@ +# SHA256 +Date: 25.07.2023 + +Author: LUBIS EDA + +## Folder Structure +The following subdirectories are part of the main directory **formal** + +- model: Contains the high level abstracted model +- properties: Contains the assertion IP(AIP) named as **fv_sha256.sv** and the constraints in place for the respective AIP **fv_constraints.sv** + + +## DUT Overview + +The DUT sha256_core has the primary inputs and primary outputs as shown below. + +| S.No | Port | Direction | Description | +| ---- | ----------------- | --------- | --------------------------------------------------------------------------------- | +| 1 | clk | input | The positive edge of the clk is used for all the signals | +| 2 | reset_n | input | The reset signal is active low and resets the core | +| 3 | zeroize | input | The core is reseted when this signal is triggered. | +| 4 | init_cmd | input | The core is initialised with respective mode constants and processes the message. | +| 5 | next_cmd | input | The core processes the message block with the previously computed results | +| 6 | mode | input | Define which hash function: SHA256,SHA224. | +| 7 | block_msg[511:0] | input | The padded block message | +| 8 | ready | output | When triggered indicates that the core is ready | +| 9 | digest[255:0] | output | The hashed value of the given message block | +| 10 | digest_valid | output | When triggered indicates that the computed digest is ready | + +When the respective mode is selected and initalised the core iterates for 63 rounds to process the hash value, if the next is triggered then the previous values of the **H** registers are in place for processing the hash value. The digest is always generated of 256 bits, in which if the mode changes to 224 then from MSB 224 bits is a valid output and rest is garbage value. +## Assertion IP Overview + +The Assertion IP signals are bound with the respective signals in the dut, where for the **rst** in binded with the DUT (reset_n && !zeroize), which ensures the reset functionality. And another AIP signal block_in_valid is triggered whenever the init or next is high. + +- reset_a: Checks that all the resgiters are resetted and the state is idle, with the ready to high. + +- DONE_to_IDLE_a: Checks the necessary registers, outputs holds the values when state transits from done to idle. + +- SHA_Rounds_to_DONE_a: Checks if the rounds are done then the registers are updated correctly. + +- SHA_Rounds_to_SHA_Rounds_before_16_a: Checks if the the rounds less than 16 then the necessary registers are updated correctly and the round increments. + +- SHA_Rounds_to_SHA_Rounds_after_16_a: Checks if the rounds are greater than 16 and less than 80 then the respective registers are updated correctly and the round increments. + +- IDLE_to_SHA_Rounds_next_a: Checks if the state is in idle and there is no init signal and the next signal asserts then the register holds the past values. + +- IDLE_to_SHA_Rounds_256_a: Checks if the state is in idle and there is init signal and the mode selected is 256. + +- IDLE_to_SHA_Rounds_224_a: Checks if the state is in idle and there is init signal and the mode selected is 224. + +- IDLE_wait_a: Checks if there isn't either init or next signal triggered in idle state then the state stays in idle and holds the past values and the core is ready. +- +## Reproduce results + +The AIP has been tested with two major FV tools. For both tools proves pass in less then 2 hour and coverage is at 100%. + +For reproducing the results: +Load the AIP, sha512_core and fv_constraints together in your formal tool. + +Feel free to reach out to contact@lubis-eda.com to request the loadscripts. + From 514a42e1d27568d5e35716d3c945de792c7e9d80 Mon Sep 17 00:00:00 2001 From: ludwig247 Date: Tue, 12 Sep 2023 16:38:29 +0200 Subject: [PATCH 3/5] update on readme --- src/sha256/formal/readme.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sha256/formal/readme.md b/src/sha256/formal/readme.md index 1300932fc..fbec141be 100644 --- a/src/sha256/formal/readme.md +++ b/src/sha256/formal/readme.md @@ -55,7 +55,7 @@ The Assertion IP signals are bound with the respective signals in the dut, where The AIP has been tested with two major FV tools. For both tools proves pass in less then 2 hour and coverage is at 100%. For reproducing the results: -Load the AIP, sha512_core and fv_constraints together in your formal tool. +Load the AIP, sha256_core and fv_constraints together in your formal tool. Feel free to reach out to contact@lubis-eda.com to request the loadscripts. From 42de674b91814428f2b6c4f5f47bc9699ad38c92 Mon Sep 17 00:00:00 2001 From: ludwig247 Date: Tue, 12 Sep 2023 16:41:52 +0200 Subject: [PATCH 4/5] Added HMAC --- src/hmac/formal/model/HMAC.luref | 640 ++++++++++++++++++ src/hmac/formal/model/hmac_core.h | 183 +++++ src/hmac/formal/model/refinement.luctrl | 9 + .../model/simulation_model/hmac_sha_join.h | 161 +++++ .../formal/model/simulation_model/sha_algo.h | 409 +++++++++++ .../model/simulation_model/sha_algo_masked.h | 487 +++++++++++++ .../simulation/CMakeLists.txt | 51 ++ .../simulation_model/simulation/hmac_main.cpp | 25 + .../simulation_model/simulation/hmac_tests.h | 107 +++ .../simulation/hmac_vectors_singleblk.txt | 35 + src/hmac/formal/model/simulation_model/top.h | 86 +++ src/hmac/formal/properties/fv_constraints.sv | 79 +++ .../formal/properties/fv_constraints_wip.sv | 40 ++ src/hmac/formal/properties/fv_coverpoints.sv | 43 ++ src/hmac/formal/properties/fv_hmac_core.sv | 236 +++++++ src/hmac/formal/properties/fv_hmac_pkg.sv | 28 + .../formal/properties/fv_key_stable_top.sv | 28 + src/hmac/formal/readme.md | 70 ++ 18 files changed, 2717 insertions(+) create mode 100644 src/hmac/formal/model/HMAC.luref create mode 100644 src/hmac/formal/model/hmac_core.h create mode 100644 src/hmac/formal/model/refinement.luctrl create mode 100644 src/hmac/formal/model/simulation_model/hmac_sha_join.h create mode 100644 src/hmac/formal/model/simulation_model/sha_algo.h create mode 100644 src/hmac/formal/model/simulation_model/sha_algo_masked.h create mode 100644 src/hmac/formal/model/simulation_model/simulation/CMakeLists.txt create mode 100644 src/hmac/formal/model/simulation_model/simulation/hmac_main.cpp create mode 100644 src/hmac/formal/model/simulation_model/simulation/hmac_tests.h create mode 100644 src/hmac/formal/model/simulation_model/simulation/hmac_vectors_singleblk.txt create mode 100644 src/hmac/formal/model/simulation_model/top.h create mode 100644 src/hmac/formal/properties/fv_constraints.sv create mode 100644 src/hmac/formal/properties/fv_constraints_wip.sv create mode 100644 src/hmac/formal/properties/fv_coverpoints.sv create mode 100644 src/hmac/formal/properties/fv_hmac_core.sv create mode 100644 src/hmac/formal/properties/fv_hmac_pkg.sv create mode 100644 src/hmac/formal/properties/fv_key_stable_top.sv create mode 100644 src/hmac/formal/readme.md diff --git a/src/hmac/formal/model/HMAC.luref b/src/hmac/formal/model/HMAC.luref new file mode 100644 index 000000000..d0ccbea25 --- /dev/null +++ b/src/hmac/formal/model/HMAC.luref @@ -0,0 +1,640 @@ +{ + "version": 17, + "module": { + "name": "HMAC", + "reset_signal": { + "signal": "(!hmac_core.reset_n || hmac_core.zeroize)", + "is_active_low": false + }, + "clock_signal": { + "signal": "hmac_core.clk", + "is_falling_edge": false + }, + "next_shift_amount": 0, + "rtl_module_name": "hmac_core", + "instance_name": "fv_hmac_core", + "default_assertion_duration": 1, + "default_disable_iff": "", + "reset": { + "documentation_comment": "" + }, + "additional_includes": "", + "additional_imports": "", + "sync_macros": [ + { + "name": "H1_digest_sync", + "datatype": "bool", + "refinement": "(hmac_core.H1_ready && hmac_core.H2_ready) && !hmac_core.first_round", + "create_commitments": true, + "timing": 0, + "unused": false + }, + { + "name": "H1_setup_digest_sync", + "datatype": "bool", + "refinement": "hmac_core.H1_ready && !hmac_core.first_round", + "create_commitments": true, + "timing": 0, + "unused": false + }, + { + "name": "H2_digest_sync", + "datatype": "bool", + "refinement": "hmac_core.H2_ready && !hmac_core.first_round", + "create_commitments": true, + "timing": 0, + "unused": false + }, + { + "name": "hmac_msg_sync", + "datatype": "bool", + "refinement": "hmac_core.init_cmd || hmac_core.next_cmd", + "create_commitments": true, + "timing": 0, + "unused": false + } + ], + "notify_macros": [ + { + "name": "H1_digest_notify", + "datatype": "bool", + "refinement": "hmac_core.H1_digest_valid && hmac_core.H2_digest_valid", + "create_commitments": false, + "timing": 0, + "unused": false + }, + { + "name": "H1_setup_digest_notify", + "datatype": "bool", + "refinement": "hmac_core.H1_digest_valid", + "create_commitments": false, + "timing": 0, + "unused": false + }, + { + "name": "H2_digest_notify", + "datatype": "bool", + "refinement": "hmac_core.H2_digest_valid", + "create_commitments": false, + "timing": 0, + "unused": false + }, + { + "name": "hmac_msg_notify", + "datatype": "bool", + "refinement": "hmac_core.ready", + "create_commitments": true, + "timing": 0, + "unused": false + }, + { + "name": "sha_msg_1_notify", + "datatype": "bool", + "refinement": "1'b1", + "create_commitments": false, + "timing": 0, + "unused": true + }, + { + "name": "sha_msg_2_notify", + "datatype": "bool", + "refinement": "1'b1", + "create_commitments": false, + "timing": 0, + "unused": true + }, + { + "name": "tag_notify", + "datatype": "bool", + "refinement": "hmac_core.tag_valid", + "create_commitments": true, + "timing": 0, + "unused": false + }, + { + "name": "sha_msg_notify", + "datatype": "bool", + "refinement": "", + "create_commitments": true, + "timing": 0, + "unused": false + } + ], + "input_datapath_macros": [ + { + "name": "H1_digest_sig", + "datatype": "sc_big_unsigned_512", + "refinement": "{hmac_core.H1_digest,hmac_core.garbage_bit_vector1}", + "create_commitments": true, + "timing": 0, + "unused": false + }, + { + "name": "H1_setup_digest_sig", + "datatype": "sc_big_unsigned_512", + "refinement": "{hmac_core.H1_digest,hmac_core.garbage_bit_vector1}", + "create_commitments": true, + "timing": 0, + "unused": false + }, + { + "name": "H2_digest_sig", + "datatype": "sc_big_unsigned_512", + "refinement": "{hmac_core.H2_digest,hmac_core.garbage_bit_vector2}", + "create_commitments": true, + "timing": 0, + "unused": false + }, + { + "name": "hmac_msg_sig_block_msg", + "datatype": "sc_big_unsigned_1024", + "refinement": "hmac_core.block_msg", + "create_commitments": true, + "timing": 0, + "unused": false + }, + { + "name": "hmac_msg_sig_init", + "datatype": "bool", + "refinement": "!hmac_core.next_cmd", + "create_commitments": true, + "timing": 0, + "unused": false + }, + { + "name": "hmac_msg_sig_key", + "datatype": "sc_big_unsigned_384", + "refinement": "hmac_core.key", + "create_commitments": true, + "timing": 0, + "unused": false + }, + { + "name": "hmac_msg_sig_next", + "datatype": "bool", + "refinement": "hmac_core.next_cmd", + "create_commitments": true, + "timing": 0, + "unused": false + } + ], + "output_datapath_macros": [ + { + "name": "sha_msg_1_sig_sha1_block_msg", + "datatype": "sc_big_unsigned_1024", + "refinement": "hmac_core.H1_block", + "create_commitments": true, + "timing": 0, + "unused": true + }, + { + "name": "sha_msg_1_sig_sha1_init", + "datatype": "bool", + "refinement": "hmac_core.H1_init", + "create_commitments": true, + "timing": 0, + "unused": true + }, + { + "name": "sha_msg_1_sig_sha1_next", + "datatype": "bool", + "refinement": "hmac_core.H1_next", + "create_commitments": true, + "timing": 0, + "unused": true + }, + { + "name": "sha_msg_1_sig_sha2_block_msg", + "datatype": "sc_big_unsigned_1024", + "refinement": "hmac_core.H2_block", + "create_commitments": true, + "timing": 0, + "unused": true + }, + { + "name": "sha_msg_1_sig_sha2_init", + "datatype": "bool", + "refinement": "hmac_core.H2_init", + "create_commitments": true, + "timing": 0, + "unused": true + }, + { + "name": "sha_msg_1_sig_sha2_next", + "datatype": "bool", + "refinement": "hmac_core.H2_next", + "create_commitments": true, + "timing": 0, + "unused": true + }, + { + "name": "sha_msg_2_sig_sha1_block_msg", + "datatype": "sc_big_unsigned_1024", + "refinement": "hmac_core.H1_block", + "create_commitments": true, + "timing": 0, + "unused": true + }, + { + "name": "sha_msg_2_sig_sha1_init", + "datatype": "bool", + "refinement": "hmac_core.H1_init", + "create_commitments": true, + "timing": 0, + "unused": true + }, + { + "name": "sha_msg_2_sig_sha1_next", + "datatype": "bool", + "refinement": "hmac_core.H1_next", + "create_commitments": true, + "timing": 0, + "unused": true + }, + { + "name": "sha_msg_2_sig_sha2_block_msg", + "datatype": "sc_big_unsigned_1024", + "refinement": "hmac_core.H2_block", + "create_commitments": true, + "timing": 0, + "unused": true + }, + { + "name": "sha_msg_2_sig_sha2_init", + "datatype": "bool", + "refinement": "hmac_core.H2_init", + "create_commitments": true, + "timing": 0, + "unused": true + }, + { + "name": "sha_msg_2_sig_sha2_next", + "datatype": "bool", + "refinement": "hmac_core.H2_next", + "create_commitments": true, + "timing": 0, + "unused": true + }, + { + "name": "tag_sig", + "datatype": "sc_big_unsigned_384", + "refinement": "hmac_core.tag", + "create_commitments": true, + "timing": 0, + "unused": false + }, + { + "name": "sha_msg_sig_sha1_block_msg", + "datatype": "sc_big_unsigned_1024", + "refinement": "", + "create_commitments": true, + "timing": 0, + "unused": false + }, + { + "name": "sha_msg_sig_sha1_init", + "datatype": "bool", + "refinement": "", + "create_commitments": true, + "timing": 0, + "unused": false + }, + { + "name": "sha_msg_sig_sha1_next", + "datatype": "bool", + "refinement": "", + "create_commitments": true, + "timing": 0, + "unused": false + }, + { + "name": "sha_msg_sig_sha2_block_msg", + "datatype": "sc_big_unsigned_1024", + "refinement": "", + "create_commitments": true, + "timing": 0, + "unused": false + }, + { + "name": "sha_msg_sig_sha2_init", + "datatype": "bool", + "refinement": "", + "create_commitments": true, + "timing": 0, + "unused": false + }, + { + "name": "sha_msg_sig_sha2_next", + "datatype": "bool", + "refinement": "", + "create_commitments": true, + "timing": 0, + "unused": false + } + ], + "state_macros": [ + { + "name": "compute_tag", + "datatype": "bool", + "refinement": "hmac_core.hmac_ctrl_reg==3'h3", + "create_commitments": true, + "timing": 0, + "unused": true + }, + { + "name": "done", + "datatype": "bool", + "refinement": "hmac_core.hmac_ctrl_reg==3'h4", + "create_commitments": true, + "timing": 0, + "unused": true + }, + { + "name": "idle", + "datatype": "bool", + "refinement": "hmac_core.hmac_ctrl_reg==3'h0", + "create_commitments": true, + "timing": 0, + "unused": false + }, + { + "name": "sha1_setup", + "datatype": "bool", + "refinement": "hmac_core.hmac_ctrl_reg==3'h1", + "create_commitments": true, + "timing": 0, + "unused": true + }, + { + "name": "sha2_setup", + "datatype": "bool", + "refinement": "hmac_core.hmac_ctrl_reg==3'h2", + "create_commitments": true, + "timing": 0, + "unused": true + }, + { + "name": "ipad", + "datatype": "bool", + "refinement": "", + "create_commitments": true, + "timing": 0, + "unused": true + }, + { + "name": "opad", + "datatype": "bool", + "refinement": "", + "create_commitments": true, + "timing": 0, + "unused": true + }, + { + "name": "hmac_done", + "datatype": "bool", + "refinement": "", + "create_commitments": true, + "timing": 0, + "unused": true + }, + { + "name": "done_tag", + "datatype": "bool", + "refinement": "", + "create_commitments": true, + "timing": 0, + "unused": false + }, + { + "name": "ctrl_ipad", + "datatype": "bool", + "refinement": "", + "create_commitments": true, + "timing": 0, + "unused": false + }, + { + "name": "ctrl_opad", + "datatype": "bool", + "refinement": "", + "create_commitments": true, + "timing": 0, + "unused": false + }, + { + "name": "ctrl_hmac", + "datatype": "bool", + "refinement": "", + "create_commitments": true, + "timing": 0, + "unused": false + } + ], + "register_macros": [ + { + "name": "hmac_block_msg", + "datatype": "sc_big_unsigned_1024", + "refinement": "(hmac_core.block_msg)", + "create_commitments": false, + "timing": 0, + "unused": false + }, + { + "name": "hmac_key", + "datatype": "sc_big_unsigned_384", + "refinement": "(hmac_core.key)", + "create_commitments": false, + "timing": 0, + "unused": false + }, + { + "name": "sha_digest_out_opad", + "datatype": "sc_big_unsigned_512", + "refinement": "{hmac_core.H2_digest,hmac_core.garbage_bit_vector2}", + "create_commitments": false, + "timing": 0, + "unused": false + } + ], + "assertions": [ + { + "name": "compute_tag_to_done", + "disable_iff": "", + "duration": -1, + "documentation_comment": "", + "unused": true + }, + { + "name": "done_to_idle", + "disable_iff": "", + "duration": -1, + "documentation_comment": "", + "unused": true + }, + { + "name": "idle_to_sha1_setup", + "disable_iff": "", + "duration": -1, + "documentation_comment": "", + "unused": true + }, + { + "name": "idle_to_sha2_setup", + "disable_iff": "", + "duration": -1, + "documentation_comment": "", + "unused": true + }, + { + "name": "sha1_setup_to_sha2_setup", + "disable_iff": "", + "duration": -1, + "documentation_comment": "", + "unused": true + }, + { + "name": "sha2_setup_to_compute_tag", + "disable_iff": "", + "duration": -1, + "documentation_comment": "", + "unused": true + }, + { + "name": "hmac_done_to_done", + "disable_iff": "", + "duration": -1, + "documentation_comment": "", + "unused": true + }, + { + "name": "idle_to_ipad", + "disable_iff": "", + "duration": -1, + "documentation_comment": "", + "unused": true + }, + { + "name": "idle_to_opad", + "disable_iff": "", + "duration": -1, + "documentation_comment": "", + "unused": true + }, + { + "name": "ipad_to_opad", + "disable_iff": "", + "duration": -1, + "documentation_comment": "", + "unused": true + }, + { + "name": "opad_to_hmac_done", + "disable_iff": "", + "duration": -1, + "documentation_comment": "", + "unused": true + }, + { + "name": "done_tag_to_idle", + "disable_iff": "", + "duration": -1, + "documentation_comment": "", + "unused": false + }, + { + "name": "hmac_done_to_done_tag", + "disable_iff": "", + "duration": -1, + "documentation_comment": "", + "unused": true + }, + { + "name": "ctrl_hmac_to_done_tag", + "disable_iff": "", + "duration": -1, + "documentation_comment": "", + "unused": false + }, + { + "name": "ctrl_ipad_to_ctrl_opad", + "disable_iff": "", + "duration": -1, + "documentation_comment": "", + "unused": false + }, + { + "name": "ctrl_opad_to_ctrl_hmac", + "disable_iff": "", + "duration": -1, + "documentation_comment": "", + "unused": false + }, + { + "name": "idle_to_ctrl_ipad", + "disable_iff": "", + "duration": -1, + "documentation_comment": "", + "unused": false + }, + { + "name": "idle_to_ctrl_opad", + "disable_iff": "", + "duration": -1, + "documentation_comment": "", + "unused": false + } + ], + "waits": [ + { + "name": "compute_tag_wait", + "documentation_comment": "", + "unused": true + }, + { + "name": "idle_wait", + "documentation_comment": "", + "unused": false + }, + { + "name": "sha1_setup_wait", + "documentation_comment": "", + "unused": true + }, + { + "name": "sha2_setup_wait", + "documentation_comment": "", + "unused": true + }, + { + "name": "hmac_done_wait", + "documentation_comment": "", + "unused": true + }, + { + "name": "ipad_wait", + "documentation_comment": "", + "unused": true + }, + { + "name": "opad_wait", + "documentation_comment": "", + "unused": true + }, + { + "name": "ctrl_hmac_wait", + "documentation_comment": "", + "unused": false + }, + { + "name": "ctrl_ipad_wait", + "documentation_comment": "", + "unused": false + }, + { + "name": "ctrl_opad_wait", + "documentation_comment": "", + "unused": false + } + ] + } +} \ No newline at end of file diff --git a/src/hmac/formal/model/hmac_core.h b/src/hmac/formal/model/hmac_core.h new file mode 100644 index 000000000..935f34fd6 --- /dev/null +++ b/src/hmac/formal/model/hmac_core.h @@ -0,0 +1,183 @@ + +#ifndef HMAC_H_ +#define HMAC_H_ + +#include "systemc.h" +#include "Interfaces.h" +#include +#include +#include +#include + +using namespace std; + +#define MSG_WIDTH 1024 // b bits +#define PAD_WIDTH 640 +#define DIGEST_WIDTH 512 +#define KEY_WIDTH 384 // n bits +#define MASK_WIDTH 512 + +const sc_biguint IPAD = sc_biguint("0x3636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636"); +const sc_biguint OPAD = "0x5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c5c"; +const sc_biguint FINAL_PAD = "0x8000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000580"; +const sc_biguint garbage_vector = "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000000000000000000000000000000000000000000000"; + +enum state +{ + state_IPAD, + state_OPAD, + state_HMAC +}; + +struct sha_block +{ + sc_biguint block_msg; + bool init; + bool next; + sc_biguint<74> lfsr_rnd; +}; + +struct sha_splitter +{ + sha_block sha1; + sha_block sha2; +}; + +struct block +{ + sc_biguint key; + sc_biguint block_msg; + bool init, next; +}; + +sc_biguint key_ipadded(sc_biguint key) +{ + return (static_cast>((static_cast>(key << (PAD_WIDTH))) ^ IPAD)); +} + +sc_biguint key_opadded(sc_biguint key) +{ + return (static_cast>(static_cast>(key << (PAD_WIDTH))) ^ OPAD); +} + +sc_biguint hmac_padded(sc_biguint hmac_digest) +{ + return (static_cast>(static_cast>(hmac_digest << (PAD_WIDTH))) | FINAL_PAD); +} + +SC_MODULE(HMAC) +{ +public: + SC_CTOR(HMAC) + { + + SC_THREAD(fsm); + } + +#ifndef LUBIS + blocking_out sha_msg_1 , sha_msg_2; +#else + master_out sha_msg /*, sha_msg_2*/; +#endif + + blocking_in> H1_digest, H2_digest, H1_setup_digest; + blocking_in hmac_msg; + +#ifndef LUBIS + blocking_out> tag; + +#else + master_out> tag; +#endif + +private: + sc_biguint sha_msg_input_ipad; + sc_biguint sha_digest_out_ipad, sha_digest_out_ipad_2, sha_digest_out_opad; + sc_biguint S1, S2; + sc_biguint temp; + bool first_round; + block hmac; + sc_biguint hmac_blk_msg; + sha_splitter sha_inst; + sc_biguint key_i; + sc_biguint block_msg_i; + bool init_i, next_i; + + void fsm() + { + + while (true) + { + + sha_msg_input_ipad = hmac_padded(sc_biguint(0)); + + hmac_msg->read(hmac, "idle"); + cout<<"INIT"<write(sha_inst); +#else + + sha_msg->master_write(sha_inst); +#endif + cout<<"IPAD"<read(sha_digest_out_ipad, "ctrl_ipad"); + } + + sha_inst.sha2.block_msg = key_opadded(hmac.key); + sha_inst.sha2.next = false; + sha_inst.sha2.init = true; + sha_inst.sha1.block_msg = hmac.block_msg; + sha_inst.sha1.init = false; + sha_inst.sha1.next = true; +#ifndef LUBIS + sha_msg_1->write(sha_inst); +#else + sha_msg->master_write(sha_inst); +#endif + cout<<"OPAD"<read(sha_digest_out_ipad, "ctrl_opad"); + + temp = static_cast>(sha_digest_out_ipad >> 128); + + sha_msg_input_ipad = hmac_padded(temp); + + sha_inst.sha1.block_msg = key_ipadded(hmac.key); + sha_inst.sha1.init = false; + sha_inst.sha1.next = false; + sha_inst.sha2.block_msg = sha_msg_input_ipad; + sha_inst.sha2.init = false; + sha_inst.sha2.next = true; + + +#ifndef LUBIS + sha_msg_2->write(sha_inst); +#else + sha_msg->master_write(sha_inst); +#endif + cout<<"ctrl_hmac"<read(sha_digest_out_opad, "ctrl_hmac"); + insert_state("done_tag"); + + cout<<"done"<write((sha_digest_out_opad >> 128)); +#else + tag->master_write((sha_digest_out_opad >> 128)); +#endif + } + } +}; + +#endif diff --git a/src/hmac/formal/model/refinement.luctrl b/src/hmac/formal/model/refinement.luctrl new file mode 100644 index 000000000..5dddd9870 --- /dev/null +++ b/src/hmac/formal/model/refinement.luctrl @@ -0,0 +1,9 @@ +{ + "version": 13, + "modules": [ + { + "name": "HMAC", + "path": "HMAC.luref" + } + ] +} \ No newline at end of file diff --git a/src/hmac/formal/model/simulation_model/hmac_sha_join.h b/src/hmac/formal/model/simulation_model/hmac_sha_join.h new file mode 100644 index 000000000..275e33a04 --- /dev/null +++ b/src/hmac/formal/model/simulation_model/hmac_sha_join.h @@ -0,0 +1,161 @@ +#ifndef HMAC_SHA_ +#define HMAC_SHA_ + +#include "systemc.h" +#include "Interfaces.h" +#include +#include +#include +#include +#include +#include "../hmac_core.h" + +using namespace std; + +#define MSG_WIDTH 1024 // b bits +#define PAD_WIDTH 640 +#define DIGEST_WIDTH 512 +#define KEY_WIDTH 384 // n bits +#define MASK_WIDTH 512 + +SC_MODULE(hmac_sha) +{ +public: + SC_CTOR(hmac_sha) + { + SC_THREAD(fsm); + } + + blocking_in sha_msg_split_1 ,sha_msg_split_2; + blocking_out> hmac_setup_digest, hmac_1_digest, hmac_2_digest; + + blocking_out h_sha_msg_1, h_sha_msg_2; + blocking_in> sha_1_digest, sha_2_digest; + +private: + sha_splitter chunk1, chunk2, chunk3; + sha_block shablock1, shablock2; + sc_biguint<1024> MSG_raw_1, MSG_raw_2, block_msg_reg; + sc_biguint<2048> msg_comb; + sc_biguint<104000> MSG_padded, shift_pad; + sc_biguint sha_digest_out_ipad, sha_digest_out_ipad_2, sha_digest_out_opad; + sc_uint<32> MSG_Length; + sc_biguint<384> expected_result; + sc_biguint garabage_digest; + bool init_reg, next_reg; + + int num = 1; + int zero_pad_len, MSG_chnks, i, j; + + void fsm() + { + std::random_device seed; + std::default_random_engine generator(seed()); + std::uniform_int_distribution distribution(0,0xFFFFFFFFFFFFFFFF); + while (true) + { + + // cout << "sha_hmac_read_start" << endl; + sha_msg_split_1->read(chunk1, "ipad_state1"); + if (chunk1.sha1.init) + { + shablock1.block_msg = chunk1.sha1.block_msg; + shablock1.init = chunk1.sha1.init; + + shablock1.next = chunk1.sha1.next; + shablock2.block_msg = chunk1.sha1.block_msg; + shablock2.init = chunk1.sha2.init; + shablock2.next = chunk1.sha2.next; + + h_sha_msg_1->write(shablock1, "send_sha1_key"); + + sha_1_digest->read(garabage_digest, "sha1_digest_out"); + hmac_setup_digest->write(garabage_digest, "read_garbage_digest"); + sha_msg_split_1->read(chunk2, "ipad_state2"); + + MSG_Length = 1024; + MSG_chnks = 2; + // cout << "sha_hmac_read_block" << endl; + + MSG_raw_1 = chunk2.sha1.block_msg; + + init_reg = chunk2.sha2.init; + block_msg_reg = chunk2.sha2.block_msg; + next_reg = chunk2.sha2.next; + + shablock1.init = chunk2.sha1.init; + shablock1.next = chunk2.sha1.next; + } + else + { + MSG_Length = 1024; + MSG_chnks = 2; + // cout << "sha_hmac_read_block" << endl; + + MSG_raw_1 = chunk1.sha1.block_msg; + + init_reg = chunk1.sha2.init; + block_msg_reg = chunk1.sha2.block_msg; + next_reg = chunk1.sha2.next; + + shablock1.init = chunk1.sha1.init; + shablock1.next = chunk1.sha1.next; + } + + MSG_padded = static_cast>(static_cast>(MSG_raw_1 << (1024)) + (static_cast>(8) << static_cast>(1020)) + static_cast>(2048)); + //cout << "MSG_padded::" << MSG_padded << endl; + for (i = 0; i < MSG_chnks; ++i) + { + shablock1.lfsr_rnd= static_cast>(distribution(generator))*sc_biguint<74>(1024) + static_cast>(distribution(generator)); + shablock1.block_msg = static_cast>(MSG_padded >> (1024 * (MSG_chnks - 1))); + if (i > 0) + { + shablock1.next = chunk2.sha1.next; + } + + h_sha_msg_1->write(shablock1, "send_ipad_msg"); + MSG_padded = static_cast>(MSG_padded << 1024); + shablock1.init = chunk2.sha1.init; + + sha_1_digest->read(sha_digest_out_ipad_2, "sha1_digest_out"); + } + hmac_1_digest->write(sha_digest_out_ipad_2, "shaop_IPAD_DIGEST_HMAC"); + ////////////////////////////////////// + + MSG_Length = 1024; + MSG_chnks = 2; + // cout << "sha_hmac_read_digest" << endl; + + sha_msg_split_2->read(chunk3, "ipad_state2"); + shablock1.block_msg = chunk3.sha1.block_msg; + shablock1.init = chunk3.sha1.init; + shablock1.next = chunk3.sha1.next; + MSG_raw_2 = chunk3.sha2.block_msg; + + MSG_padded = ((static_cast>(block_msg_reg)) << 1024) | (MSG_raw_2); + // cout << "MSG_padded_sha2::" << MSG_padded << endl; + + shablock2.init = init_reg; + shablock2.next = next_reg; + + for (j = 0; j < MSG_chnks; j++) + { + shablock2.lfsr_rnd= static_cast>(distribution(generator))*sc_biguint<74>(1024) + static_cast>(distribution(generator)); + shablock2.block_msg = static_cast>(MSG_padded >> (1024 * (MSG_chnks - 1))); + if (j > 0) + { + shablock2.next = chunk3.sha1.next; + } + h_sha_msg_2->write(shablock2, "send_ipad_msg"); + MSG_padded = static_cast>(MSG_padded << 1024); + shablock2.init = chunk3.sha1.init; + sha_2_digest->read(sha_digest_out_opad, "sha1_digest_out"); + } + hmac_2_digest->write(sha_digest_out_opad, "shaop_IPAD_DIGEST_HMAC"); + + chunk1.sha1.init = chunk3.sha1.init; + } + } +}; + +#endif \ No newline at end of file diff --git a/src/hmac/formal/model/simulation_model/sha_algo.h b/src/hmac/formal/model/simulation_model/sha_algo.h new file mode 100644 index 000000000..138467449 --- /dev/null +++ b/src/hmac/formal/model/simulation_model/sha_algo.h @@ -0,0 +1,409 @@ +#ifndef SHA +#define SHA + +#include +#include "systemc.h" +#include "string.h" +#include "Interfaces.h" +#include "../hmac_core.h" + +using namespace std; +#define NUM_ROUNDS 80 + +//----------------------------------------------------------------------------- +//----------------------------------------------------------------------------- + + sc_biguint<64> slicer(sc_biguint<1024> block, int index) { + switch (index){ + case 0: + return static_cast> (block >> sc_biguint<1024>(64 * 0)); + break; + case 1: + return static_cast> (block >> sc_biguint<1024>(64 * 1)); + break; + case 2: + return static_cast> (block >> sc_biguint<1024>(64 * 2)); + break; + case 3: + return static_cast> (block >> sc_biguint<1024>(64 * 3)); + break; + case 4: + return static_cast> (block >> sc_biguint<1024>(64 * 4)); + break; + case 5: + return static_cast> (block >> sc_biguint<1024>(64 * 5)); + break; + case 6: + return static_cast> (block >> sc_biguint<1024>(64 * 6)); + break; + case 7: + return static_cast> (block >> sc_biguint<1024>(64 * 7)); + break; + case 8: + return static_cast> (block >> sc_biguint<1024>(64 * 8)); + break; + case 9: + return static_cast> (block >> sc_biguint<1024>(64 * 9)); + break; + case 10: + return static_cast> (block >> sc_biguint<1024>(64 * 10)); + break; + case 11: + return static_cast> (block >> sc_biguint<1024>(64 * 11)); + break; + case 12: + return static_cast> (block >> sc_biguint<1024>(64 * 12)); + break; + case 13: + return static_cast> (block >> sc_biguint<1024>(64 * 13)); + break; + case 14: + return static_cast> (block >> sc_biguint<1024>(64 * 14)); + break; + case 15: + return static_cast> (block >> sc_biguint<1024>(64 * 15)); + break; + default: + return static_cast> (block >> sc_biguint<1024>(64 * 15)); + break; + } +} + +sc_biguint<64> Ch(sc_biguint<64> a, sc_biguint<64> b, sc_biguint<64> c) { + return static_cast>((a & b) ^ (~a & c)); +} + +sc_biguint<64> Maj(sc_biguint<64> x, sc_biguint<64> y, sc_biguint<64> z) { + return static_cast>((x & y) ^ (x & z) ^ (y & z)); +} + +sc_biguint<64> shr6(sc_biguint<64> n) { + return static_cast>(n >> sc_biguint<64>(6)); +} + +sc_biguint<64> shr7(sc_biguint<64> n) { + return static_cast>(n >> sc_biguint<64>(7)); +} + +sc_biguint<64> rotr1(sc_biguint<64> n) { + return static_cast>((n >> (sc_biguint<64>(1))) | (n << (sc_biguint<64>(63)))); +} + +sc_biguint<64> rotr8(sc_biguint<64> n) { + return static_cast>((n >> (sc_biguint<64>(8))) | (n << (sc_biguint<64>(56)))); +} + +sc_biguint<64> rotr14(sc_biguint<64> n) { + return static_cast>((n >> (sc_biguint<64>(14))) | (n << (sc_biguint<64>(50)))); +} + +sc_biguint<64> rotr18(sc_biguint<64> n) { + return static_cast>((n >> (sc_biguint<64>(18))) | (n << (sc_biguint<64>(46)))); +} + +sc_biguint<64> rotr19(sc_biguint<64> n) { + return static_cast>((n >> (sc_biguint<64>(19))) | (n << (sc_biguint<64>(45)))); +} + +sc_biguint<64> rotr28(sc_biguint<64> n) { + return static_cast>((n >> (sc_biguint<64>(28))) | (n << (sc_biguint<64>(36)))); +} + +sc_biguint<64> rotr34(sc_biguint<64> n) { + return static_cast>((n >> (sc_biguint<64>(34))) | (n << (sc_biguint<64>(30)))); +} + +sc_biguint<64> rotr39(sc_biguint<64> n) { + return static_cast>((n >> (sc_biguint<64>(39))) | (n << (sc_biguint<64>(25)))); +} + +sc_biguint<64> rotr41(sc_biguint<64> n) { + return static_cast>((n >> (sc_biguint<64>(41))) | (n << (sc_biguint<64>(23)))); +} + +sc_biguint<64> rotr61(sc_biguint<64> n) { + return static_cast>((n >> (sc_biguint<64>(61))) | (n << (sc_biguint<64>(3)))); +} + +sc_biguint<64> sigma0(sc_biguint<64> x){ + return static_cast> (rotr28(x) ^ rotr34(x) ^ rotr39(x)); +} + +sc_biguint<64> sigma1(sc_biguint<64> x) { + return static_cast> (rotr14(x) ^ rotr18(x) ^ rotr41(x)); +} + +sc_biguint<64> delta0(sc_biguint<64> x) { + return static_cast> (rotr1(x) ^ rotr8(x) ^ shr7(x)); +} + +sc_biguint<64> delta1(sc_biguint<64> x) { + return static_cast> (rotr19(x) ^ rotr61(x) ^ shr6(x)); +} + +sc_biguint<64> T1(sc_biguint<64> e, sc_biguint<64> f, sc_biguint<64> g, sc_biguint<64> h, sc_biguint<64> k, sc_biguint<64> w) { + return static_cast>(h + sigma1(e) + Ch(e, f, g) + k + w); +} + +sc_biguint<64> T2(sc_biguint<64> a, sc_biguint<64> b, sc_biguint<64> c) { + return static_cast>(sigma0(a) + Maj(a, b, c)); +} +sc_biguint<64> compute_e(sc_biguint<64> d,sc_biguint<64> e, sc_biguint<64> f, sc_biguint<64> g, sc_biguint<64> h, sc_biguint<64> k, sc_biguint<64> w) { + return static_cast>(d+ h + sigma1(e) + Ch(e, f, g) + k + w); +} +sc_biguint<64> compute_a(sc_biguint<64> e, sc_biguint<64> f, sc_biguint<64> g, sc_biguint<64> h, sc_biguint<64> k, sc_biguint<64> w,sc_biguint<64> a, sc_biguint<64> b, sc_biguint<64> c) { + return static_cast>((static_cast>(h + sigma1(e) + Ch(e, f, g) + k + w))+(static_cast>(sigma0(a) + Maj(a, b, c)))); +} + +sc_biguint<64> compute_w(sc_biguint<64> w14, sc_biguint<64> w9, sc_biguint<64> w1, sc_biguint<64> w0) { + return static_cast>(delta1(w14) + w9 + delta0(w1) + w0); +} + +sc_biguint<512> compute_dig (sc_biguint<512> dig,sc_biguint<64> h7, sc_biguint<64> h6, sc_biguint<64> h5, sc_biguint<64> h4,sc_biguint<64> h3,sc_biguint<64> h2, sc_biguint<64> h1, sc_biguint<64> h0){ + dig += static_cast> (h6 << sc_biguint<64>(448)); + dig = static_cast> (dig >> sc_biguint<512>(64)); + dig += static_cast> (h6 << sc_biguint<64>(448)); + dig = static_cast> (dig >> sc_biguint<512>(64)); + dig += static_cast> (h5 << sc_biguint<64>(448)); + dig = static_cast> (dig >> sc_biguint<512>(64)); + dig += static_cast> (h4 << sc_biguint<64>(448)); + dig = static_cast> (dig >> sc_biguint<512>(64)); + dig += static_cast> (h3 << sc_biguint<64>(448)); + dig = static_cast> (dig >> sc_biguint<512>(64)); + dig += static_cast> (h2 << sc_biguint<64>(448)); + dig = static_cast> (dig >> sc_biguint<512>(64)); + dig += static_cast> (h1 << sc_biguint<64>(448)); + dig = static_cast> (dig >> sc_biguint<512>(64)); + dig += static_cast> (h0 << sc_biguint<64>(448)); + + return(dig); + +} +// struct SHA_Args{ +// sc_biguint<1024> in; +// bool init; +// bool next; +// }; + +/*struct sha_block{ + sc_biguint block_msg; + bool init; + bool next; +};*/ +//----------------------------------------------------------------------------- +//----------------------------------------------------------------------------- + const array , 80> K = + {sc_biguint<64>(0x428a2f98d728ae22), sc_biguint<64>(0x7137449123ef65cd), sc_biguint<64>(0xb5c0fbcfec4d3b2f),\ + sc_biguint<64>(0xe9b5dba58189dbbc), sc_biguint<64>(0x3956c25bf348b538), sc_biguint<64>(0x59f111f1b605d019),\ + sc_biguint<64>(0x923f82a4af194f9b), sc_biguint<64>(0xab1c5ed5da6d8118), sc_biguint<64>(0xd807aa98a3030242),\ + sc_biguint<64>(0x12835b0145706fbe), sc_biguint<64>(0x243185be4ee4b28c), sc_biguint<64>(0x550c7dc3d5ffb4e2),\ + sc_biguint<64>(0x72be5d74f27b896f), sc_biguint<64>(0x80deb1fe3b1696b1), sc_biguint<64>(0x9bdc06a725c71235),\ + sc_biguint<64>(0xc19bf174cf692694), sc_biguint<64>(0xe49b69c19ef14ad2), sc_biguint<64>(0xefbe4786384f25e3),\ + sc_biguint<64>(0x0fc19dc68b8cd5b5), sc_biguint<64>(0x240ca1cc77ac9c65), sc_biguint<64>(0x2de92c6f592b0275),\ + sc_biguint<64>(0x4a7484aa6ea6e483), sc_biguint<64>(0x5cb0a9dcbd41fbd4), sc_biguint<64>(0x76f988da831153b5),\ + sc_biguint<64>(0x983e5152ee66dfab), sc_biguint<64>(0xa831c66d2db43210), sc_biguint<64>(0xb00327c898fb213f),\ + sc_biguint<64>(0xbf597fc7beef0ee4), sc_biguint<64>(0xc6e00bf33da88fc2), sc_biguint<64>(0xd5a79147930aa725),\ + sc_biguint<64>(0x06ca6351e003826f), sc_biguint<64>(0x142929670a0e6e70), sc_biguint<64>(0x27b70a8546d22ffc),\ + sc_biguint<64>(0x2e1b21385c26c926), sc_biguint<64>(0x4d2c6dfc5ac42aed), sc_biguint<64>(0x53380d139d95b3df),\ + sc_biguint<64>(0x650a73548baf63de), sc_biguint<64>(0x766a0abb3c77b2a8), sc_biguint<64>(0x81c2c92e47edaee6),\ + sc_biguint<64>(0x92722c851482353b), sc_biguint<64>(0xa2bfe8a14cf10364), sc_biguint<64>(0xa81a664bbc423001),\ + sc_biguint<64>(0xc24b8b70d0f89791), sc_biguint<64>(0xc76c51a30654be30), sc_biguint<64>(0xd192e819d6ef5218),\ + sc_biguint<64>(0xd69906245565a910), sc_biguint<64>(0xf40e35855771202a), sc_biguint<64>(0x106aa07032bbd1b8),\ + sc_biguint<64>(0x19a4c116b8d2d0c8), sc_biguint<64>(0x1e376c085141ab53), sc_biguint<64>(0x2748774cdf8eeb99),\ + sc_biguint<64>(0x34b0bcb5e19b48a8), sc_biguint<64>(0x391c0cb3c5c95a63), sc_biguint<64>(0x4ed8aa4ae3418acb),\ + sc_biguint<64>(0x5b9cca4f7763e373), sc_biguint<64>(0x682e6ff3d6b2b8a3), sc_biguint<64>(0x748f82ee5defb2fc),\ + sc_biguint<64>(0x78a5636f43172f60), sc_biguint<64>(0x84c87814a1f0ab72), sc_biguint<64>(0x8cc702081a6439ec),\ + sc_biguint<64>(0x90befffa23631e28), sc_biguint<64>(0xa4506cebde82bde9), sc_biguint<64>(0xbef9a3f7b2c67915),\ + sc_biguint<64>(0xc67178f2e372532b), sc_biguint<64>(0xca273eceea26619c), sc_biguint<64>(0xd186b8c721c0c207),\ + sc_biguint<64>(0xeada7dd6cde0eb1e), sc_biguint<64>(0xf57d4f7fee6ed178), sc_biguint<64>(0x06f067aa72176fba),\ + sc_biguint<64>(0x0a637dc5a2c898a6), sc_biguint<64>(0x113f9804bef90dae), sc_biguint<64>(0x1b710b35131c471b),\ + sc_biguint<64>(0x28db77f523047d84), sc_biguint<64>(0x32caab7b40c72493), sc_biguint<64>(0x3c9ebe0a15c9bebc),\ + sc_biguint<64>(0x431d67c49c100d4c), sc_biguint<64>(0x4cc5d4becb3e42b6), sc_biguint<64>(0x597f299cfc657e2a),\ + sc_biguint<64>(0x5fcb6fab3ad6faec), sc_biguint<64>(0x6c44198c4a475817)};; + +SC_MODULE(SHA512) { + + blocking_in SHA_Input; + blocking_out > out; + + array , 16> W; + array , 8> H; + + sc_biguint<64> t1 = sc_biguint<64> (0), t2 = sc_biguint<64> (0), + a = sc_biguint<64> (0), b = sc_biguint<64> (0), + c = sc_biguint<64> (0), d = sc_biguint<64> (0), + e = sc_biguint<64> (0), f = sc_biguint<64> (0), + g = sc_biguint<64> (0), h = sc_biguint<64> (0), + w = sc_biguint<64> (0), k = sc_biguint<64> (0); + sc_biguint<64> tmp_w; + + sc_biguint<1024> block_in; + sc_biguint<1024> block_copy; + sc_biguint<512> MSG_digest; + + sha_block SHA_in; + int SHA_Mode_in; + bool init, next, success, zeroize; + + int i, j, m=0; + + void fsm(); + + SC_CTOR(SHA512){ + SC_THREAD(fsm); + } +}; + +void SHA512::fsm(){ + +while(true){ + + SHA_Input->read(SHA_in, "IDLE"); + + block_in = SHA_in.block_msg; + SHA_Mode_in = 384; + init = SHA_in.init; + next = SHA_in.next; + //zeroize = SHA_in.zeroize; + cout<<"sha_called"<(0x8c3d37c819544da2), sc_biguint<64>(0x73e1996689dcd4d6),\ + sc_biguint<64>(0x1dfab7ae32ff9c82), sc_biguint<64>(0x679dd514582f9fcf),\ + sc_biguint<64>(0x0f6d2b697bd44da8), sc_biguint<64>(0x77e36f7304c48942),\ + sc_biguint<64>(0x3f9d85a86a1d36c8), sc_biguint<64>(0x1112e6ad91d692a1)}; + break; + case 256: + H ={sc_biguint<64>(0x22312194fc2bf72c), sc_biguint<64>(0x9f555fa3c84c64c2),\ + sc_biguint<64>(0x2393b86b6f53b151), sc_biguint<64>(0x963877195940eabd),\ + sc_biguint<64>(0x96283ee2a88effe3), sc_biguint<64>(0xbe5e1e2553863992),\ + sc_biguint<64>(0x2b0199fc2c85b8aa), sc_biguint<64>(0x0eb72ddc81c52ca2)}; + break; + case 384: + H ={sc_biguint<64>(0xcbbb9d5dc1059ed8), sc_biguint<64>(0x629a292a367cd507),\ + sc_biguint<64>(0x9159015a3070dd17), sc_biguint<64>(0x152fecd8f70e5939),\ + sc_biguint<64>(0x67332667ffc00b31), sc_biguint<64>(0x8eb44a8768581511),\ + sc_biguint<64>(0xdb0c2e0d64f98fa7), sc_biguint<64>(0x47b5481dbefa4fa4)}; + break; + case 512: + H ={sc_biguint<64>(0x6a09e667f3bcc908), sc_biguint<64>(0xbb67ae8584caa73b),\ + sc_biguint<64>(0x3c6ef372fe94f82b), sc_biguint<64>(0xa54ff53a5f1d36f1),\ + sc_biguint<64>(0x510e527fade682d1), sc_biguint<64>(0x9b05688c2b3e6c1f),\ + sc_biguint<64>(0x1f83d9abfb41bd6b), sc_biguint<64>(0x5be0cd19137e2179)}; + + break; + default: + H ={sc_biguint<64>(0xcbbb9d5dc1059ed8), sc_biguint<64>(0x629a292a367cd507),\ + sc_biguint<64>(0x9159015a3070dd17), sc_biguint<64>(0x152fecd8f70e5939),\ + sc_biguint<64>(0x67332667ffc00b31), sc_biguint<64>(0x8eb44a8768581511),\ + sc_biguint<64>(0xdb0c2e0d64f98fa7), sc_biguint<64>(0x47b5481dbefa4fa4)}; + break; + } + + t1 = sc_biguint<64> (0); t2 = sc_biguint<64> (0); + a = sc_biguint<64> (0); b = sc_biguint<64> (0); + c = sc_biguint<64> (0); d = sc_biguint<64> (0); + e = sc_biguint<64> (0); f = sc_biguint<64> (0); + g = sc_biguint<64> (0); h = sc_biguint<64> (0); + w = sc_biguint<64> (0); k = sc_biguint<64> (0); + W = {sc_biguint<64>(0)}; + } + + std::cout << "*****************"<< std::endl; + std::cout << "H[0] registers: "<< std::hex<> (H[7] << (sc_biguint<64>(448))); + for (j=6; j > -1; --j) { + MSG_digest = static_cast> (MSG_digest >> sc_biguint<512>(64)); + MSG_digest += static_cast> (H[j] << sc_biguint<64>(448)); + } + //MSG_digest = compute_dig(static_cast>(0),H[7],H[6],H[5],H[4],H[3],H[2],H[1],H[0]); + //MSG_digest = concati(MSG_digest, H, j); + /* BYME: to comply with rtl + switch (SHA_Mode_in){ + case 224: + MSG_digest = static_cast> (MSG_digest >> sc_biguint<512>(288)); + break; + case 256: + MSG_digest = static_cast> (MSG_digest >> sc_biguint<512>(256)); + break; + case 384: + MSG_digest = static_cast> (MSG_digest >> sc_biguint<512>(128)); + break; + default: + MSG_digest = static_cast> (MSG_digest); + break; + }*/ + + out->write(static_cast> (MSG_digest)); + + + //}; + + //out->write(static_cast> (MSG_digest >> static_cast>(512-SHA_Mode_in))); + } +}; +#endif \ No newline at end of file diff --git a/src/hmac/formal/model/simulation_model/sha_algo_masked.h b/src/hmac/formal/model/simulation_model/sha_algo_masked.h new file mode 100644 index 000000000..01d2f1449 --- /dev/null +++ b/src/hmac/formal/model/simulation_model/sha_algo_masked.h @@ -0,0 +1,487 @@ +#ifndef SHA +#define SHA + +#include +#include +#include "systemc.h" +#include "string.h" +#include "Interfaces.h" +#include "../hmac_core.h" +using namespace std; + +#define NUM_ROUNDS 80 +#define SHA512_RNDs 9 +const sc_biguint<74> LFSR_INIT_SEED = sc_biguint<74>(0xA79D0EC11E389277); + +std::random_device seed; +std::default_random_engine generator(seed()); +std::uniform_int_distribution distribution(0,0xFFFFFFFFFFFFFFFF); + +//0x079D0EC11E389277); // a random value, copied from RTL: +//BYME: check latest versin of code, Luref, functions23A +//ASK: I don't want some stuff in luref +//BYME: changed fv_constraints to fix block_msg +//----------------------------------------------------------------------------- +//----------------------------------------------------------------------------- + +/* struct sha_block +{ + sc_biguint block_msg; + bool init; + bool next; + sc_biguint<74> lfsr_rnd; +}; */ +struct masked_reg_t { + sc_biguint<64> masked, random; +}; + +//----------------------------------------------------------------------------- +//----------------------------------------------------------------------------- + + sc_biguint<64> slicer(sc_biguint<1024> block, int index) { + switch (index){ + case 0: + return static_cast> (block >> sc_biguint<1024>(64 * 0)); + break; + case 1: + return static_cast> (block >> sc_biguint<1024>(64 * 1)); + break; + case 2: + return static_cast> (block >> sc_biguint<1024>(64 * 2)); + break; + case 3: + return static_cast> (block >> sc_biguint<1024>(64 * 3)); + break; + case 4: + return static_cast> (block >> sc_biguint<1024>(64 * 4)); + break; + case 5: + return static_cast> (block >> sc_biguint<1024>(64 * 5)); + break; + case 6: + return static_cast> (block >> sc_biguint<1024>(64 * 6)); + break; + case 7: + return static_cast> (block >> sc_biguint<1024>(64 * 7)); + break; + case 8: + return static_cast> (block >> sc_biguint<1024>(64 * 8)); + break; + case 9: + return static_cast> (block >> sc_biguint<1024>(64 * 9)); + break; + case 10: + return static_cast> (block >> sc_biguint<1024>(64 * 10)); + break; + case 11: + return static_cast> (block >> sc_biguint<1024>(64 * 11)); + break; + case 12: + return static_cast> (block >> sc_biguint<1024>(64 * 12)); + break; + case 13: + return static_cast> (block >> sc_biguint<1024>(64 * 13)); + break; + case 14: + return static_cast> (block >> sc_biguint<1024>(64 * 14)); + break; + case 15: + return static_cast> (block >> sc_biguint<1024>(64 * 15)); + break; + default: + return static_cast> (block >> sc_biguint<1024>(64 * 15)); + break; + } +} + +sc_biguint<512> concati(sc_biguint<512> MSG_digest, array , 8> H, int j) { + MSG_digest = static_cast> (H[7] << (sc_biguint<64>(448))); + for (j=6; j > -1; --j) { + MSG_digest = static_cast> (MSG_digest >> sc_biguint<512>(64)); + MSG_digest += static_cast> (H[j] << sc_biguint<64>(448)); + }; + return MSG_digest; +} + +sc_biguint<64> shr6(sc_biguint<64> n) { + return static_cast>(n >> sc_biguint<64>(6)); +} + +sc_biguint<64> shr7(sc_biguint<64> n) { + return static_cast>(n >> sc_biguint<64>(7)); +} + +sc_biguint<64> rotr1(sc_biguint<64> n) { + return static_cast>((n >> (sc_biguint<64>(1))) | (n << (sc_biguint<64>(63)))); +} + +sc_biguint<64> rotr8(sc_biguint<64> n) { + return static_cast>((n >> (sc_biguint<64>(8))) | (n << (sc_biguint<64>(56)))); +} + +sc_biguint<64> rotr14(sc_biguint<64> n) { + return static_cast>((n >> (sc_biguint<64>(14))) | (n << (sc_biguint<64>(50)))); +} + +sc_biguint<64> rotr18(sc_biguint<64> n) { + return static_cast>((n >> (sc_biguint<64>(18))) | (n << (sc_biguint<64>(46)))); +} + +sc_biguint<64> rotr19(sc_biguint<64> n) { + return static_cast>((n >> (sc_biguint<64>(19))) | (n << (sc_biguint<64>(45)))); +} + +sc_biguint<64> rotr28(sc_biguint<64> n) { + return static_cast>((n >> (sc_biguint<64>(28))) | (n << (sc_biguint<64>(36)))); +} + +sc_biguint<64> rotr34(sc_biguint<64> n) { + return static_cast>((n >> (sc_biguint<64>(34))) | (n << (sc_biguint<64>(30)))); +} + +sc_biguint<64> rotr39(sc_biguint<64> n) { + return static_cast>((n >> (sc_biguint<64>(39))) | (n << (sc_biguint<64>(25)))); +} + +sc_biguint<64> rotr41(sc_biguint<64> n) { + return static_cast>((n >> (sc_biguint<64>(41))) | (n << (sc_biguint<64>(23)))); +} + +sc_biguint<64> rotr61(sc_biguint<64> n) { + return static_cast>((n >> (sc_biguint<64>(61))) | (n << (sc_biguint<64>(3)))); +} + +sc_biguint<64> sigma0(sc_biguint<64> x){ + return static_cast> (rotr28(x) ^ rotr34(x) ^ rotr39(x)); +} + +sc_biguint<64> sigma1(sc_biguint<64> x) { + return static_cast> (rotr14(x) ^ rotr18(x) ^ rotr41(x)); +} + +sc_biguint<64> delta0(sc_biguint<64> x) { + return static_cast> (rotr1(x) ^ rotr8(x) ^ shr7(x)); +} + +sc_biguint<64> delta1(sc_biguint<64> x) { + return static_cast> (rotr19(x) ^ rotr61(x) ^ shr6(x)); +} + +sc_biguint<64> masked_and(sc_biguint<64> x_masked, sc_biguint<64> x_random, sc_biguint<64> y_masked, sc_biguint<64> y_random) { + return (~y_masked & ((~y_random & x_random) | (y_random & x_masked))) | (y_masked & ((y_random & x_random) | (~y_random & x_masked))); //x & y; +} + +sc_biguint<64> masked_Maj(sc_biguint<64> a_masked, sc_biguint<64> a_random, sc_biguint<64> b_masked, sc_biguint<64> b_random, sc_biguint<64> c_masked, sc_biguint<64> c_random) { + return masked_and(a_masked, a_random, b_masked, b_random) ^ masked_and(a_masked, a_random, c_masked, c_random) ^ masked_and(b_masked, b_random, c_masked, c_random); +} + +sc_biguint<64> masked_Ch_m(sc_biguint<64> e_masked, sc_biguint<64> e_random, sc_biguint<64> f_masked, sc_biguint<64> f_random, sc_biguint<64> g_masked, sc_biguint<64> g_random) { + return masked_and(e_masked, e_random, f_masked, f_random) ^ masked_and(g_masked, g_random, ~e_masked, e_random); +} + +sc_biguint<64> masked_Ch_r(sc_biguint<64> e_masked, sc_biguint<64> e_random, sc_biguint<64> f_masked, sc_biguint<64> f_random, sc_biguint<64> g_masked, sc_biguint<64> g_random) { + return e_random ^ g_random; +} + +sc_biguint<64> B2A_conv(sc_biguint<64> x_masked, sc_biguint<64> x_random, bool q, bool masked_carry, sc_biguint<128> x_prime, sc_biguint<64> mask, int j) { // convert x_masked = x ^ rnd to x_prime = x + rand + // masked_carry[j] = c[j] ^ qs + mask = sc_biguint<64>(0x01); + x_prime = sc_biguint<128>(0); + masked_carry = q; //used this initial value to avoid the separate case of 0 + + for (j = 0; j < 64; ++j) { //BYME: change next line + x_prime += ((x_masked & mask) == mask) != masked_carry != q ? sc_biguint<128>(16) * sc_biguint<128>(0x01000000000000000) : sc_biguint<128>(0); + masked_carry = (!((x_masked & mask) == mask) and (((x_random & mask) == mask) != q)) or (((x_masked & mask) == mask) and masked_carry); + + x_prime = x_prime >> sc_biguint<128>(1); + mask = mask << sc_biguint<64>(1); + } + + return static_cast>(x_prime);//x_prime +} + +sc_biguint<64> A2B_conv(sc_biguint<64> x_masked, sc_biguint<64> x_random, bool q, bool masked_carry, sc_biguint<128> x_m, sc_biguint<64> mask, int j) { // convert x_prime = x + rand to x_masked = x ^ rnd + // masked_carry[j] = c[j] ^ q + mask = sc_biguint<64>(0x01); + x_m = static_cast>((x_masked & mask) << (sc_biguint<128>(64))); + masked_carry = (not((x_masked & mask) == mask) and ((x_random & mask) == mask)) != q;//used this initial value to avoid separate case of 0 + + for (j = 1; j < 64; ++j) { + mask = mask << sc_biguint<64>(1); + + x_m = (x_m >> 1);//BYME: change next line + x_m += ((x_masked & mask) == mask) != masked_carry != q ? sc_biguint<128>(16) * sc_biguint<128>(0x01000000000000000) : sc_biguint<128>(0); + + masked_carry = ((((x_masked & mask) == mask) != ((x_random & mask) == mask)) and (((x_random & mask) == mask) != q)) or ((!((x_masked & mask) == mask) != ((x_random & mask) == mask)) and masked_carry); + + } + x_m = (x_m >> 1); + + + return static_cast>(x_m);//x_m +} + +sc_biguint<64> T1_m(sc_biguint<64> e_masked, sc_biguint<64> e_random, sc_biguint<64> f_masked, sc_biguint<64> f_random, sc_biguint<64> g_masked, sc_biguint<64> g_random, sc_biguint<64> h_masked, sc_biguint<64> h_random, sc_biguint<64> k, sc_biguint<64> w_masked, sc_biguint<64> w_random, bool masked_carry, sc_biguint<128> x_prime, sc_biguint<64> mask, bool q_masking_rnd_0, bool q_masking_rnd_1, bool q_masking_rnd_2, bool q_masking_rnd_3, bool q_masking_rnd_4, int j) { + + return static_cast>(B2A_conv(h_masked, h_random, q_masking_rnd_0, masked_carry, x_prime, mask, j) + + B2A_conv(sigma1(e_masked), sigma1(e_random), q_masking_rnd_1, masked_carry, x_prime, mask, j)+ + B2A_conv(masked_Ch_m(e_masked, e_random, f_masked, f_random, g_masked, g_random), e_random ^ g_random, q_masking_rnd_2, masked_carry, x_prime, mask, j) + + B2A_conv(k, sc_biguint<64>(0x0), q_masking_rnd_3, masked_carry, x_prime, mask, j) + + B2A_conv(w_masked, w_random, q_masking_rnd_4, masked_carry, x_prime, mask, j)); +} + +sc_biguint<64> T1_r(sc_biguint<64> e_random, sc_biguint<64> g_random, sc_biguint<64> h_random, sc_biguint<64> w_random) { + return static_cast>(h_random + sigma1(e_random) + (e_random ^ g_random) + w_random); +} + +sc_biguint<64> T2_m(sc_biguint<64> a_masked, sc_biguint<64> a_random, sc_biguint<64> b_masked, sc_biguint<64> b_random, sc_biguint<64> c_masked, sc_biguint<64> c_random, bool masked_carry, sc_biguint<128> x_prime, sc_biguint<64> mask, bool q_masking_rnd_5, bool q_masking_rnd_6, int j) { + return static_cast>(B2A_conv(sigma0(a_masked), sigma0(a_random), q_masking_rnd_5, masked_carry, x_prime, mask, j) + + B2A_conv(masked_Maj(a_masked, a_random, b_masked, b_random, c_masked, c_random), b_random, q_masking_rnd_6, masked_carry, x_prime, mask, j)); +} + +sc_biguint<64> T2_r(sc_biguint<64> a_random, sc_biguint<64> b_random) { + return static_cast>(sigma0(a_random) + b_random); +} + +sc_biguint<74> lfsr(sc_biguint<74> a) { + return static_cast>((a * 2) + (a[73] ^ a[72] ^ a[58] ^ a[57])); +} + +//----------------------------------------------------------------------------- +//----------------------------------------------------------------------------- +const array , 80> K = + {sc_biguint<64>(0x428a2f98d728ae22), sc_biguint<64>(0x7137449123ef65cd), sc_biguint<64>(0xb5c0fbcfec4d3b2f),\ + sc_biguint<64>(0xe9b5dba58189dbbc), sc_biguint<64>(0x3956c25bf348b538), sc_biguint<64>(0x59f111f1b605d019),\ + sc_biguint<64>(0x923f82a4af194f9b), sc_biguint<64>(0xab1c5ed5da6d8118), sc_biguint<64>(0xd807aa98a3030242),\ + sc_biguint<64>(0x12835b0145706fbe), sc_biguint<64>(0x243185be4ee4b28c), sc_biguint<64>(0x550c7dc3d5ffb4e2),\ + sc_biguint<64>(0x72be5d74f27b896f), sc_biguint<64>(0x80deb1fe3b1696b1), sc_biguint<64>(0x9bdc06a725c71235),\ + sc_biguint<64>(0xc19bf174cf692694), sc_biguint<64>(0xe49b69c19ef14ad2), sc_biguint<64>(0xefbe4786384f25e3),\ + sc_biguint<64>(0x0fc19dc68b8cd5b5), sc_biguint<64>(0x240ca1cc77ac9c65), sc_biguint<64>(0x2de92c6f592b0275),\ + sc_biguint<64>(0x4a7484aa6ea6e483), sc_biguint<64>(0x5cb0a9dcbd41fbd4), sc_biguint<64>(0x76f988da831153b5),\ + sc_biguint<64>(0x983e5152ee66dfab), sc_biguint<64>(0xa831c66d2db43210), sc_biguint<64>(0xb00327c898fb213f),\ + sc_biguint<64>(0xbf597fc7beef0ee4), sc_biguint<64>(0xc6e00bf33da88fc2), sc_biguint<64>(0xd5a79147930aa725),\ + sc_biguint<64>(0x06ca6351e003826f), sc_biguint<64>(0x142929670a0e6e70), sc_biguint<64>(0x27b70a8546d22ffc),\ + sc_biguint<64>(0x2e1b21385c26c926), sc_biguint<64>(0x4d2c6dfc5ac42aed), sc_biguint<64>(0x53380d139d95b3df),\ + sc_biguint<64>(0x650a73548baf63de), sc_biguint<64>(0x766a0abb3c77b2a8), sc_biguint<64>(0x81c2c92e47edaee6),\ + sc_biguint<64>(0x92722c851482353b), sc_biguint<64>(0xa2bfe8a14cf10364), sc_biguint<64>(0xa81a664bbc423001),\ + sc_biguint<64>(0xc24b8b70d0f89791), sc_biguint<64>(0xc76c51a30654be30), sc_biguint<64>(0xd192e819d6ef5218),\ + sc_biguint<64>(0xd69906245565a910), sc_biguint<64>(0xf40e35855771202a), sc_biguint<64>(0x106aa07032bbd1b8),\ + sc_biguint<64>(0x19a4c116b8d2d0c8), sc_biguint<64>(0x1e376c085141ab53), sc_biguint<64>(0x2748774cdf8eeb99),\ + sc_biguint<64>(0x34b0bcb5e19b48a8), sc_biguint<64>(0x391c0cb3c5c95a63), sc_biguint<64>(0x4ed8aa4ae3418acb),\ + sc_biguint<64>(0x5b9cca4f7763e373), sc_biguint<64>(0x682e6ff3d6b2b8a3), sc_biguint<64>(0x748f82ee5defb2fc),\ + sc_biguint<64>(0x78a5636f43172f60), sc_biguint<64>(0x84c87814a1f0ab72), sc_biguint<64>(0x8cc702081a6439ec),\ + sc_biguint<64>(0x90befffa23631e28), sc_biguint<64>(0xa4506cebde82bde9), sc_biguint<64>(0xbef9a3f7b2c67915),\ + sc_biguint<64>(0xc67178f2e372532b), sc_biguint<64>(0xca273eceea26619c), sc_biguint<64>(0xd186b8c721c0c207),\ + sc_biguint<64>(0xeada7dd6cde0eb1e), sc_biguint<64>(0xf57d4f7fee6ed178), sc_biguint<64>(0x06f067aa72176fba),\ + sc_biguint<64>(0x0a637dc5a2c898a6), sc_biguint<64>(0x113f9804bef90dae), sc_biguint<64>(0x1b710b35131c471b),\ + sc_biguint<64>(0x28db77f523047d84), sc_biguint<64>(0x32caab7b40c72493), sc_biguint<64>(0x3c9ebe0a15c9bebc),\ + sc_biguint<64>(0x431d67c49c100d4c), sc_biguint<64>(0x4cc5d4becb3e42b6), sc_biguint<64>(0x597f299cfc657e2a),\ + sc_biguint<64>(0x5fcb6fab3ad6faec), sc_biguint<64>(0x6c44198c4a475817)}; + +SC_MODULE(SHA512_masked) { + + blocking_in SHA_Input; + blocking_out > out; + + array , 16> W; + array , 8> H; + array , 8> rh_masking_rnd = {sc_biguint<64>(0)}; + + masked_reg_t t1 = {sc_biguint<64>(0)}, t2 = {sc_biguint<64>(0)}, + a = {sc_biguint<64>(0)}, b = {sc_biguint<64>(0)}, + c = {sc_biguint<64>(0)}, d = {sc_biguint<64>(0)}, + e = {sc_biguint<64>(0)}, f = {sc_biguint<64>(0)}, + g = {sc_biguint<64>(0)}, h = {sc_biguint<64>(0)}, + w_data = {sc_biguint<64>(0)}; + sc_biguint<64> w = sc_biguint<64> (0), k = sc_biguint<64> (0); + sc_biguint<64> tmp_w; + + sc_biguint<1024> block_in; + sc_biguint<1024> block_copy; + sc_biguint<512> MSG_digest; + + sc_biguint<74> lfsr_rnd; + //sc_biguint<74> lfsr_rnd = LFSR_INIT_SEED; + sc_biguint<74> lfsr_rnd_c; + + sha_block SHA_in; + int SHA_Mode_in; + bool init_cmd, next_cmd, success, zeroize; + + bool masked_carry; + sc_biguint<64> mask = sc_biguint<64>(0x01);; + sc_biguint<64> rw_masking_rnd; + array q_masking_rnd; + sc_biguint<128> x_prime; + sc_biguint<128> x_masked; + + int i, j, m=0, p; + + void fsm(); + + SC_CTOR(SHA512_masked){ + SC_THREAD(fsm); + } +}; + +void SHA512_masked::fsm(){ + + while(true){ + //lfsr_rnd = LFSR_INIT_SEED; //BYME: otherwise in reset property would be 0 + SHA_Input->read(SHA_in, "IDLE"); + + block_in = SHA_in.block_msg; + lfsr_rnd = SHA_in.lfsr_rnd; + SHA_Mode_in = 384; + init_cmd = SHA_in.init; + next_cmd = SHA_in.next; + //zeroize = SHA_in.zeroize; + + //for (p=0; p(0x8c3d37c819544da2), sc_biguint<64>(0x73e1996689dcd4d6),\ + sc_biguint<64>(0x1dfab7ae32ff9c82), sc_biguint<64>(0x679dd514582f9fcf),\ + sc_biguint<64>(0x0f6d2b697bd44da8), sc_biguint<64>(0x77e36f7304c48942),\ + sc_biguint<64>(0x3f9d85a86a1d36c8), sc_biguint<64>(0x1112e6ad91d692a1)}; + break; + case 1: + H ={sc_biguint<64>(0x22312194fc2bf72c), sc_biguint<64>(0x9f555fa3c84c64c2),\ + sc_biguint<64>(0x2393b86b6f53b151), sc_biguint<64>(0x963877195940eabd),\ + sc_biguint<64>(0x96283ee2a88effe3), sc_biguint<64>(0xbe5e1e2553863992),\ + sc_biguint<64>(0x2b0199fc2c85b8aa), sc_biguint<64>(0x0eb72ddc81c52ca2)}; + break; + /*case 2: + H ={sc_biguint<64>(0xcbbb9d5dc1059ed8), sc_biguint<64>(0x629a292a367cd507),\ + sc_biguint<64>(0x9159015a3070dd17), sc_biguint<64>(0x152fecd8f70e5939),\ + sc_biguint<64>(0x67332667ffc00b31), sc_biguint<64>(0x8eb44a8768581511),\ + sc_biguint<64>(0xdb0c2e0d64f98fa7), sc_biguint<64>(0x47b5481dbefa4fa4)}; + break;*/ + case 3: + H ={sc_biguint<64>(0x6a09e667f3bcc908), sc_biguint<64>(0xbb67ae8584caa73b),\ + sc_biguint<64>(0x3c6ef372fe94f82b), sc_biguint<64>(0xa54ff53a5f1d36f1),\ + sc_biguint<64>(0x510e527fade682d1), sc_biguint<64>(0x9b05688c2b3e6c1f),\ + sc_biguint<64>(0x1f83d9abfb41bd6b), sc_biguint<64>(0x5be0cd19137e2179)}; + break; + default: + H ={sc_biguint<64>(0xcbbb9d5dc1059ed8), sc_biguint<64>(0x629a292a367cd507),\ + sc_biguint<64>(0x9159015a3070dd17), sc_biguint<64>(0x152fecd8f70e5939),\ + sc_biguint<64>(0x67332667ffc00b31), sc_biguint<64>(0x8eb44a8768581511),\ + sc_biguint<64>(0xdb0c2e0d64f98fa7), sc_biguint<64>(0x47b5481dbefa4fa4)}; + break; + } + // BYME: Wasn't it this way before? + t1= {sc_biguint<64>(0)}; t2 = {sc_biguint<64>(0)}; + a = {sc_biguint<64>(0)}; b = {sc_biguint<64>(0)}; + c = {sc_biguint<64>(0)}; d = {sc_biguint<64>(0)}; + e = {sc_biguint<64>(0)}; f = {sc_biguint<64>(0)}; + g = {sc_biguint<64>(0)}; h = {sc_biguint<64>(0)}; + w = sc_biguint<64> (0); k = sc_biguint<64> (0); + W = {sc_biguint<64>(0)}; + //lfsr_rnd = LFSR_INIT_SEED;//BYME lfsr_seed; + } + + for (j=0; j<8; ++j) { //BYME: if (masking_init)rh_masking_rnd[rnd_ctr_reg[2 : 0]] <= lfsr_rnd[63 : 0]; + rh_masking_rnd[j] = lfsr_rnd; + }; + + //next(block_in); + //W_schedule(block_in); + block_copy = block_in; + + for (j=0; j<16; ++j) { + W[15-j] = slicer(block_copy, j); + }; + + //copy_digest(); + a = {H[0] ^ rh_masking_rnd[0], rh_masking_rnd[0]}; b = {H[1] ^ rh_masking_rnd[1], rh_masking_rnd[1]}; + c = {H[2] ^ rh_masking_rnd[2], rh_masking_rnd[2]}; d = {H[3] ^ rh_masking_rnd[3], rh_masking_rnd[3]}; + e = {H[4] ^ rh_masking_rnd[4], rh_masking_rnd[4]}; f = {H[5] ^ rh_masking_rnd[5], rh_masking_rnd[5]}; + g = {H[6] ^ rh_masking_rnd[6], rh_masking_rnd[6]}; h = {H[7] ^ rh_masking_rnd[7], rh_masking_rnd[7]}; + + for (i=0; i>(distribution(generator))*sc_biguint<74>(1024) + static_cast>(distribution(generator)); + //std::cout << std::dec << "LFSR_RND in round " << i << " is: " << std::hex << lfsr_rnd << std::endl; + insert_state("SHA_Rounds"); + //sha512_round(i); + k = K[i]; + //w = next_w(i); + + if (i < 16) + w = W[i]; + else { + tmp_w = delta1(W[14]) + W[9] + delta0(W[1]) + W[0]; + for (j=0; j<15; ++j) { + W[j] = W[(j+1)]; + }; + W[15] = tmp_w; + w = tmp_w; + }; + + rw_masking_rnd = static_cast>(lfsr_rnd); + lfsr_rnd_c = lfsr_rnd >> 64; + for (j=0; j<10; ++j) { + q_masking_rnd[j] = ((lfsr_rnd_c) & 0x1) == 1; + lfsr_rnd_c = lfsr_rnd_c >> 1; + }; + w_data = {w ^ rw_masking_rnd, rw_masking_rnd}; + t1 = {T1_m(e.masked, e.random, f.masked, f.random, g.masked, g.random, h.masked, h.random, k, w_data.masked, w_data.random, masked_carry, x_prime, mask, q_masking_rnd[0], q_masking_rnd[1], q_masking_rnd[2], q_masking_rnd[3], q_masking_rnd[4], j), T1_r(e.random, g.random, h.random, w_data.random)}; + t2 = {T2_m(a.masked, a.random, b.masked, b.random, c.masked, c.random, masked_carry, x_prime, mask, q_masking_rnd[5], q_masking_rnd[6], j), T2_r(a.random, b.random)}; + h = g; + g = f; + f = e; + e = {A2B_conv((B2A_conv(d.masked, d.random, q_masking_rnd[7], masked_carry, x_prime, mask, j) + t1.masked), (d.random + t1.random), q_masking_rnd[9], masked_carry, x_masked, mask, j), (d.random + t1.random)}; + d = c; + c = b; + b = a; + a = {A2B_conv((t1.masked + t2.masked), (t1.random + t2.random), q_masking_rnd[8], masked_carry, x_masked, mask, j), (t1.random + t2.random)}; + + }; + insert_state("DONE"); + //update_digest(); + H[0] = (H[0] + (a.masked ^ a.random)); + H[1] = (H[1] + (b.masked ^ b.random)); + H[2] = (H[2] + (c.masked ^ c.random)); + H[3] = (H[3] + (d.masked ^ d.random)); + H[4] = (H[4] + (e.masked ^ e.random)); + H[5] = (H[5] + (f.masked ^ f.random)); + H[6] = (H[6] + (g.masked ^ g.random)); + H[7] = (H[7] + (h.masked ^ h.random)); + + MSG_digest = static_cast> (H[7] << (sc_biguint<64>(448))); + for (j=6; j > -1; --j) { + MSG_digest = static_cast> (MSG_digest >> sc_biguint<512>(64)); + MSG_digest += static_cast> (H[j] << sc_biguint<64>(448)); + }; + //MSG_digest = concati(MSG_digest, H, j); + /* BYME: to comply with rtl + switch (SHA_Mode_in){ + case 0: + MSG_digest = static_cast> (MSG_digest >> sc_biguint<512>(288)); + break; + case 1: + MSG_digest = static_cast> (MSG_digest >> sc_biguint<512>(256)); + break; + case 2: + MSG_digest = static_cast> (MSG_digest >> sc_biguint<512>(128)); + break; + case 3: + MSG_digest = static_cast> (MSG_digest); + break; + default: + MSG_digest = static_cast> (MSG_digest >> sc_biguint<512>(128)); + break; + }*/ + + out->write(static_cast> (MSG_digest)); + + //}; + + //out->write(static_cast> (MSG_digest >> static_cast>(512-SHA_Mode_in))); + } +}; +#endif \ No newline at end of file diff --git a/src/hmac/formal/model/simulation_model/simulation/CMakeLists.txt b/src/hmac/formal/model/simulation_model/simulation/CMakeLists.txt new file mode 100644 index 000000000..19c71a4ee --- /dev/null +++ b/src/hmac/formal/model/simulation_model/simulation/CMakeLists.txt @@ -0,0 +1,51 @@ +########################## Configuration ########################## + +# Set the path to the directory where the 'Interfaces.h' header can be found +set(INTERFACES_DIR "/home/advaith-sreevalsan/.vscode-server/extensions/lubis.lubis-vsc-plugin-2023.3.2/LUBIS/include/interfaces") +# Set TRUE if this CMakeLists should download and install SystemC by itself, +# otherwise set to FALSE and give a directory path to another SystemC installation +set(INSTALL_SYSTEMC TRUE) +set(SYSTEMC_INCLUDE_DIR "/home/advaith-sreevalsan/.vscode-server/extensions/lubis.lubis-vsc-plugin-2023.3.2/LUBIS/include/systemc") +set(SYSTEMC_LIB_DIR "") + +################################################################### + +include(FetchContent) + +cmake_minimum_required(VERSION 3.10) +project(LUBIS_Simulation) +set(CMAKE_CXX_STANDARD 14) +set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_SOURCE_DIR}/bin) +set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_SOURCE_DIR}/bin) + +if(INSTALL_SYSTEMC) + FetchContent_Declare(SYSTEMC + GIT_REPOSITORY https://github.com/accellera-official/systemc + GIT_TAG 2.3.3 + GIT_SHALLOW TRUE + GIT_PROGRESS TRUE + ) + FetchContent_MakeAvailable(SYSTEMC) + include_directories( + ${CMAKE_CACHEFILE_DIR}/_deps/systemc-src/src + ) +else() + include_directories( + ${SYSTEMC_INCLUDE_DIR} + ) + link_directories( + ${SYSTEMC_LIB_DIR} + ) +endif() + +include_directories( + ${INTERFACES_DIR} +) + +add_executable(hmac_tests + hmac_main.cpp +) + +target_link_libraries(hmac_tests PRIVATE + systemc +) diff --git a/src/hmac/formal/model/simulation_model/simulation/hmac_main.cpp b/src/hmac/formal/model/simulation_model/simulation/hmac_main.cpp new file mode 100644 index 000000000..f702df25f --- /dev/null +++ b/src/hmac/formal/model/simulation_model/simulation/hmac_main.cpp @@ -0,0 +1,25 @@ +#include "systemc.h" +#include "Interfaces.h" +#include "../../hmac_core.h" +#include "hmac_tests.h" +#include "../top.h" +#include "../sha_algo_masked.h" + +int sc_main(int argc, char **argv) { + top top1("top1"); + hmac_tests tests("tests"); + + + Blocking hmac_msg("hmac_msg"); + Blocking> tag("tag"); + + top1.top_hmac(hmac_msg); + top1.top_tag(tag); + + tests.hmac_msg(hmac_msg); + tests.tag(tag); + + + sc_start(); + return 0; +} diff --git a/src/hmac/formal/model/simulation_model/simulation/hmac_tests.h b/src/hmac/formal/model/simulation_model/simulation/hmac_tests.h new file mode 100644 index 000000000..f3e73e917 --- /dev/null +++ b/src/hmac/formal/model/simulation_model/simulation/hmac_tests.h @@ -0,0 +1,107 @@ +#ifndef HMAC_CORE_TESTS_H +#define HMAC_CORE_TESTS_H + + +#include "systemc.h" +#include "Interfaces.h" +#include +#include +#include "../sha_algo_masked.h" +#include "../../hmac_core.h" +//#include "../top.h" + +using namespace std; + + +SC_MODULE(hmac_tests) { +public: + SC_CTOR(hmac_tests) { + // read_test_vectors(file_path); + SC_THREAD(testbench) + } + + blocking_out hmac_msg; + blocking_in> tag; + +private: + void testbench() { + + sc_biguint<384> test_result; + block test_input; + sc_biguint<384>KEY; + string COUNT; + sc_biguint<104000> MSG_raw; + sc_biguint<104000> MSG_padded; + sc_uint<32> MSG_Length; + sc_biguint<384> expected_result; + int num = 1; + int zero_pad_len, MSG_chnks,i; + /* std::string filename = "hmac_vectors_singleblk.txt"; + //std::ifstream myfile; + + std::ifstream myfile(filename); + + if (!myfile.is_open()) { + std::cout << "Failed to open the file: " << filename << std::endl; + // Handle the error condition + return; +} + while (myfile) + { + myfile >> COUNT; + myfile >> MSG_Length; + myfile >> std::hex >> KEY; + myfile >> std::hex >> MSG_padded; + myfile >> expected_result; + + + MSG_chnks = static_cast (MSG_Length / 1024); */ + while(true){ + test_input.init = 1; + test_input.next = 0; + test_input.key = 0; + MSG_padded = "0x01010101010101010101010101010101010101010101010101010101010101010101010101010101010101010101010100768412320f7b0aa5812fce428dc4706b3cae50e02a64caa16a782249bfe8efc4b7ef1ccb126255d196047dfedf17a0a96b9d3dad2e1b8c1c05b19875b6659f4de23c3b667bf297ba9aa47740787137d896d5724e4c70a825f872c9ea60d2edf5800000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000888"; + expected_result = 0; + MSG_Length = 2048; + MSG_chnks = static_cast (MSG_Length / 1024); + + for (i=0; i >(MSG_padded >> (1024*(MSG_chnks-1))); + cout<0){ + test_input.next = 1; + test_input.init = 0;} + hmac_msg->write(test_input); + MSG_padded = static_cast> (MSG_padded << 1024); + test_input.init = 0; + tag->read(test_result, "success"); + + }; + + if (test_result != (expected_result)){ + std::cout << "Test " << COUNT << " Failed!" << std::endl; + std::cout << std::hex << "Output: " << test_result << std::endl; + std::cout << std::hex << "Expected: " << expected_result << std::endl; + } + else { + std::cout << "Test " << COUNT << " Passed!" << std::endl; + } + + + + + //myfile.close(); + sc_stop(); +} + } +}; + + +#endif + + + + + + diff --git a/src/hmac/formal/model/simulation_model/simulation/hmac_vectors_singleblk.txt b/src/hmac/formal/model/simulation_model/simulation/hmac_vectors_singleblk.txt new file mode 100644 index 000000000..0912d3479 --- /dev/null +++ b/src/hmac/formal/model/simulation_model/simulation/hmac_vectors_singleblk.txt @@ -0,0 +1,35 @@ +COUNT0 +1024 +0x000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F +0x53616D706C65206D65737361676520666F72206B65796C656E3C626C6F636B6C656E80000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000510 +0xbe92ab28770b45bdbff7c1ff8e559ec8db51852fe8ba1ac86e7f87c9dc8f2e5eb71a10b0033160740c8ab06181b62d7a +COUNT1 +1024 +0x0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b +0x4869205468657265800000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000440 +0x47a071f44d2ea7df1ac5ff7cf937068ea34ed0453aed3a61c63d39ae475ed03ea426dce81fb89c3d239887fe2284c267 +COUNT2 +1024 +0x4a6566654a6566654a6566654a6566654a6566654a6566654a6566654a6566654a6566654a6566654a6566654a656665 +0x7768617420646f2079612077616e7420666f72206e6f7468696e673f800000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000004e0 +0xe51de7ae00cc719ec8a304d9ff962d53358a7e0b5b6874533af75a66e01a4ee504b9173fd582ba618fe1f6264a889d91 +COUNT3 +1024 +0xaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa +0xdddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddd800000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000590 +0x06d08f889071a284af1bf4ba6b35599e728e20b0fbfa2103c7ebcb2aed872a8adc3769847c9dad14c43fbc9bb12a9e87 +COUNT4 +1024 +0x0102030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e1f200a0b0c0d0e0f10111213141516171819 +0xcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcdcd800000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000590 +0x40e90e787a5cbffeba9252ee2fd76750701199b320cd4b7b9caaa196348ede37d26760e3ebb9ace726ec08a030c3cc2a +COUNT5 +1024 +0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff +0x0000000000000000000000000000000000000000000000000000000000000000000080000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000510 +0x282cf79e9dbe17f48911baa32b7840c4a045786992cde132a1d0dba00e0dd2631d94705be075ea5b90e90ea0c8da26e9 +COUNT6 +1024 +0x000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 +0x0000000000000000000000000000000000000000000000000000000000000000000080000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000510 +0x4088db02e38c741c3d108cd17814afcdf5b27e93fa7baa5ea1d64f61ab9f70604a120e9fe5c3f713ede59db7adbc1c3e \ No newline at end of file diff --git a/src/hmac/formal/model/simulation_model/top.h b/src/hmac/formal/model/simulation_model/top.h new file mode 100644 index 000000000..76675ada4 --- /dev/null +++ b/src/hmac/formal/model/simulation_model/top.h @@ -0,0 +1,86 @@ +#include "systemc.h" +#include "Interfaces.h" +#include "../hmac_core.h" +#include "sha_algo_masked.h" +#include "hmac_sha_join.h" + +SC_MODULE(top) +{ + + HMAC hmc; + SHA512_masked sha384_1; + SHA512_masked sha384_2; + hmac_sha hmacsha; + + blocking_in top_hmac; + blocking_out> top_tag; + + Blocking hmac_msg; + Blocking> tag; + + Blocking sha_msg_split_1, sha_msg_split_2; + Blocking> H1_setup_digest, hmac_1_digest, hmac_2_digest; + Blocking h_sha_msg_1, h_sha_msg_2; + Blocking> sha_1_digest, sha_2_digest; + + SC_CTOR(top) : hmc("hmc"), + sha384_1("sha384_1"), + sha384_2("sha384_2"), + hmacsha("hmacsha"), + + top_hmac("top_in"), + top_tag("top_out"), + + hmac_msg("hmac_msg"), + tag("tag"), + + sha_msg_split_1("sha_msg_split_1"), + sha_msg_split_2("sha_msg_split_2"), + //sha_msg_split_2("sha_msg_split_2"), + + H1_setup_digest("H1_setup_digest"), + hmac_1_digest("hmac_1_digest"), + hmac_2_digest("hmac_2_digest"), + + h_sha_msg_1("h_sha_msg_1"), + h_sha_msg_2("h_sha_msg_2"), + sha_1_digest("sha_1_digest"), + sha_2_digest("sha_2_digest") + { + + hmc.hmac_msg(top_hmac); + + hmc.sha_msg_1(sha_msg_split_1); + hmacsha.sha_msg_split_1(sha_msg_split_1); + + hmacsha.h_sha_msg_1(h_sha_msg_1); + sha384_1.SHA_Input(h_sha_msg_1); + + sha384_1.out(sha_1_digest); + + hmacsha.hmac_setup_digest(H1_setup_digest); + hmc.H1_setup_digest(H1_setup_digest); + + // hmc.sha_msg_2(sha_msg_split_2); + // hmacsha.sha_msg_split_2(sha_msg_split_2); + + hmacsha.sha_1_digest(sha_1_digest); + + hmacsha.hmac_1_digest(hmac_1_digest); + hmc.H1_digest(hmac_1_digest); + + hmc.sha_msg_2(sha_msg_split_2); + hmacsha.sha_msg_split_2(sha_msg_split_2); + + hmacsha.h_sha_msg_2(h_sha_msg_2); + sha384_2.SHA_Input(h_sha_msg_2); + + sha384_2.out(sha_2_digest); + hmacsha.sha_2_digest(sha_2_digest); + + hmacsha.hmac_2_digest(hmac_2_digest); + hmc.H2_digest(hmac_2_digest); + + hmc.tag(top_tag); + } +}; \ No newline at end of file diff --git a/src/hmac/formal/properties/fv_constraints.sv b/src/hmac/formal/properties/fv_constraints.sv new file mode 100644 index 000000000..41e800989 --- /dev/null +++ b/src/hmac/formal/properties/fv_constraints.sv @@ -0,0 +1,79 @@ +module fv_constraints_m +( + input logic clk, + input logic rst_n, + input logic zeroize, + input logic hmac_init, + input logic hmac_next, + input logic [383:0] hmac_key +); + + logic fv_hmac_init_reg; + + default clocking default_clk @(posedge clk); endclocking + + + always @ (posedge clk or negedge rst_n) + begin + if (!rst_n || zeroize) + fv_hmac_init_reg <= 1'h0; + else if (hmac_init) + fv_hmac_init_reg <= 1'h1; + end + + + ////////////////////////// + // Assumptions 1 + // hmac_init and hmac_next + // cannot be high at same + // time. + ///// + property hmac_init_and_next_not_high_same; + !(hmac_init && hmac_next); + endproperty + assume_hmac_init_and_next_not_high_same: assume property(disable iff(!rst_n)hmac_init_and_next_not_high_same); + + /////////////////////////// + // Assumptions 2 + // hmac_init should be high + // first then next. + ////// + property hmac_first_init_then_next; + !fv_hmac_init_reg + |-> + !hmac_next; + endproperty + assume_hmac_first_init_then_next : assume property(disable iff(!rst_n) hmac_first_init_then_next); + + /////////////////////////// + // Assumptions 3 + // hmac_key must be stable + // from the receiving of the + // key + ///// + property hmac_key_stable; + ##1 $stable(hmac_key) || hmac_init; + endproperty + assume_key_stable: assume property(disable iff(!rst_n)hmac_key_stable); + + /////////////////////////// + // Assumptions 4 + // hmac_init must be high + // unitl ready is high + assume_init_not_ready: assume property (disable iff (!rst_n) + !hmac_core.ready + |-> + !hmac_init); + + endmodule + + bind hmac_core fv_constraints_m fv_constraints ( + .clk (clk ), + .rst_n (reset_n ), + .zeroize (zeroize ), + .hmac_init (init_cmd ), + .hmac_next (next_cmd ), + .hmac_key (key ) + ); + + diff --git a/src/hmac/formal/properties/fv_constraints_wip.sv b/src/hmac/formal/properties/fv_constraints_wip.sv new file mode 100644 index 000000000..3413ef780 --- /dev/null +++ b/src/hmac/formal/properties/fv_constraints_wip.sv @@ -0,0 +1,40 @@ +module fv_constraints_wip_m +( + input logic clk, + input logic rst_n, + input logic hmac_init, + input logic hmac_next, + input wire [383 : 0] key, + input wire [1023 : 0] block_msg, + input logic sha1_init, + input logic sha1_next, + input logic sha2_init, + input logic sha2_next, + input logic [2 : 0] ctrl_reg, + input logic first_round +); + default clocking default_clk @(posedge clk); endclocking + +/* assume_wip_key_stable: assume property(disable iff(!rst_n) + hmac_init + |=> + ($stable(key) || hmac_init) + ); + */ + + endmodule + + bind hmac_core fv_constraints_wip_m constraints_wip( + .clk (clk ), + .rst_n (reset_n && !zeroize ), + .hmac_init (init_cmd ), + .hmac_next (next_cmd ), + .sha1_init (u_sha512_core_h1.init_cmd), + .sha1_next (u_sha512_core_h1.next_cmd), + .sha2_init (u_sha512_core_h2.init_cmd), + .sha2_next (u_sha512_core_h2.next_cmd), + .ctrl_reg (hmac_ctrl_new ), + .first_round(first_round ), + .key (key ), + .block_msg (block_msg ) + ); \ No newline at end of file diff --git a/src/hmac/formal/properties/fv_coverpoints.sv b/src/hmac/formal/properties/fv_coverpoints.sv new file mode 100644 index 000000000..bed308d18 --- /dev/null +++ b/src/hmac/formal/properties/fv_coverpoints.sv @@ -0,0 +1,43 @@ +module fv_coverpoints_m( + input logic clk, + input logic reset_n, + input logic zeroize +); + + default clocking default_clk @(posedge clk); endclocking + + //Cover zeroize: + //Assert zeroize input and check the status of all registers. All registers/internal memories should be cleared. + cover_zeroize: cover property(disable iff(!reset_n) hmac_core.zeroize ); + cover_zeroize_after_next: cover property(disable iff(!reset_n ) hmac_core.zeroize && hmac_core.ready && hmac_core.next_cmd ); + cover_multiple_next: cover property(disable iff(!reset_n || zeroize ) + hmac_core.next_cmd && hmac_core.ready ##1 hmac_core.next_cmd && hmac_core.ready[->1] ); + + // Assert init_cmd or next_cmd when HMAC_ready is still low. The engine ignores the new command and continues + // to complete the previous command. + cover_init_and_next_ready_low: cover property(disable iff(!reset_n || zeroize) + (hmac_core.init_cmd || + hmac_core.next_cmd) && + !hmac_core.ready + ); + + + // Assert to check if init_cmd then process the key if not process the block message. + cover_init_IPAD: cover property(disable iff(!reset_n || zeroize) + hmac_core.init_cmd + ##2 + hmac_core.CTRL_IPAD + ); + + cover_next_OPAD: cover property(disable iff(!reset_n || zeroize) + (hmac_core.next_cmd + ##2 + hmac_core.CTRL_OPAD + )); + + endmodule +bind hmac_core fv_coverpoints_m fv_coverpoints( + .clk(clk), + .reset_n(reset_n), + .zeroize(zeroize) +); \ No newline at end of file diff --git a/src/hmac/formal/properties/fv_hmac_core.sv b/src/hmac/formal/properties/fv_hmac_core.sv new file mode 100644 index 000000000..9745915c8 --- /dev/null +++ b/src/hmac/formal/properties/fv_hmac_core.sv @@ -0,0 +1,236 @@ + +import global_package::*; + +module fv_hmac_core_m( + input bit rst, + input bit clk, + input bit unsigned [511:0] H1_digest, + input bit unsigned [511:0] H1_setup_digest, + input bit unsigned [511:0] H2_digest, + input bit unsigned [383:0] hmac_msg_key, + input bit unsigned [1023:0] hmac_msg_block_msg, + input bit hmac_msg_init, + input bit hmac_msg_next, + input bit unsigned [1023:0] sha1_block_msg, + input bit sha1_init, + input bit sha1_next, + input bit unsigned [1023:0] sha2_block_msg, + input bit sha2_init, + input bit sha2_next, + input bit unsigned [383:0] tag, + input bit H1_digest_ready, + input bit H1_setup_digest_ready, + input bit H2_digest_ready, + input bit hmac_msg_valid, + input bit H1_digest_valid, + input bit H1_setup_digest_valid, + input bit H2_digest_valid, + input bit hmac_msg_ready, + input bit tag_valid, + input bit unsigned [383:0] hmac_key, + input bit unsigned [1023:0] hmac_block_msg, + input bit unsigned [511:0] sha_digest_out_opad, + input bit idle, + input bit ctrl_ipad, + input bit ctrl_opad, + input bit ctrl_hmac, + input bit done_tag +); + + +default clocking default_clk @(posedge clk); endclocking + +sequence reset_sequence; + rst ##1 !rst; +endsequence + +reset_a: assert property (reset_p); +property reset_p; + reset_sequence |-> + idle && + hmac_msg_ready == 1 && + tag_valid == 0; +endproperty + + +ctrl_hmac_to_done_tag_a: assert property (disable iff(rst) ctrl_hmac_to_done_tag_p); +property ctrl_hmac_to_done_tag_p; + ctrl_hmac && + H2_digest_ready +|-> + ##1 (hmac_msg_ready == 0) and + ##1 (tag_valid == 0) and + ##1 done_tag; +endproperty + + +done_tag_to_idle_a: assert property (disable iff(rst) done_tag_to_idle_p); +property done_tag_to_idle_p; + done_tag +|-> + ##1 + idle && + tag == 384'(((sha_digest_out_opad) >> 512'd128)) && + hmac_msg_ready == 1 && + tag_valid == 1; +endproperty + + +idle_to_ctrl_ipad_a: assert property (disable iff(rst) idle_to_ctrl_ipad_p); +property idle_to_ctrl_ipad_p; + idle && + hmac_msg_valid && + hmac_msg_init +|-> + ##1 (hmac_msg_ready == 0) and + ##1 (tag_valid == 0) and + ##1 + ctrl_ipad && + sha1_block_msg == key_ipadded($past(hmac_msg_key, 1)) && + sha1_init == 1 && + sha1_next == 0 && + sha2_block_msg == key_opadded($past(hmac_msg_key, 1)) && + sha2_init == 0 && + sha2_next == 0; +endproperty + + +idle_to_ctrl_opad_a: assert property (disable iff(rst) idle_to_ctrl_opad_p); +property idle_to_ctrl_opad_p; + idle && + hmac_msg_valid && + !hmac_msg_init +|-> + ##1 (hmac_msg_ready == 0) and + ##1 (tag_valid == 0) and + ##1 + ctrl_opad && + sha1_block_msg == (hmac_block_msg) && + sha1_init == 0 && + sha1_next == 1 && + sha2_block_msg == key_opadded($past(hmac_msg_key, 1)) && + sha2_init == 1 && + sha2_next == 0; +endproperty + + +ctrl_ipad_to_ctrl_opad_a: assert property (disable iff(rst) ctrl_ipad_to_ctrl_opad_p); +property ctrl_ipad_to_ctrl_opad_p; + ctrl_ipad && + H1_setup_digest_ready +|-> + ##1 (hmac_msg_ready == 0) and + ##1 (tag_valid == 0) and + ##1 + ctrl_opad && + sha1_block_msg == (hmac_block_msg) && + sha1_init == 0 && + sha1_next == 1 && + sha2_block_msg == key_opadded($past(hmac_key, 1)) && + sha2_init == 1 && + sha2_next == 0; +endproperty + + +ctrl_opad_to_ctrl_hmac_a: assert property (disable iff(rst) ctrl_opad_to_ctrl_hmac_p); +property ctrl_opad_to_ctrl_hmac_p; + ctrl_opad && + H1_digest_ready +|-> + ##1 (hmac_msg_ready == 0) and + ##1 (tag_valid == 0) and + ##1 + ctrl_hmac && + sha1_block_msg == key_ipadded($past(hmac_key, 1)) && + sha1_init == 0 && + sha1_next == 0 && + sha2_block_msg == hmac_padded(384'(((H1_digest) >> 512'd128))) && + sha2_init == 0 && + sha2_next == 1; +endproperty + + +ctrl_hmac_wait_a: assert property (disable iff(rst) ctrl_hmac_wait_p); +property ctrl_hmac_wait_p; + ctrl_hmac && + !H2_digest_ready +|-> + ##1 + ctrl_hmac && + hmac_msg_ready == 0 && + tag_valid == 0; +endproperty + + +idle_wait_a: assert property (disable iff(rst) idle_wait_p); +property idle_wait_p; + idle && + !hmac_msg_valid +|-> + ##1 + idle && + hmac_msg_ready == 1 && + tag_valid == $past(tag_valid); +endproperty + + +ctrl_ipad_wait_a: assert property (disable iff(rst) ctrl_ipad_wait_p); +property ctrl_ipad_wait_p; + ctrl_ipad && + !H1_setup_digest_ready +|-> + ##1 + ctrl_ipad && + hmac_msg_ready == 0 && + tag_valid == 0; +endproperty + + +ctrl_opad_wait_a: assert property (disable iff(rst) ctrl_opad_wait_p); +property ctrl_opad_wait_p; + ctrl_opad && + !H1_digest_ready +|-> + ##1 + ctrl_opad && + hmac_msg_ready == 0 && + tag_valid == 0; +endproperty + +endmodule + +bind hmac_core fv_hmac_core_m fv_hmac_core( + .rst((!hmac_core.reset_n || hmac_core.zeroize)), + .clk(hmac_core.clk), + .H1_digest({hmac_core.H1_digest,hmac_core.garbage_bit_vector1}), + .H1_setup_digest({hmac_core.H1_digest,hmac_core.garbage_bit_vector1}), + .H2_digest({hmac_core.H2_digest,hmac_core.garbage_bit_vector2}), + .hmac_msg_key(hmac_core.key), + .hmac_msg_block_msg(hmac_core.block_msg), + .hmac_msg_init(hmac_core.init_cmd), + .hmac_msg_next(hmac_core.next_cmd), + .sha1_block_msg(hmac_core.H1_block), + .sha1_init(hmac_core.H1_init), + .sha1_next(hmac_core.H1_next), + .sha2_block_msg(hmac_core.H2_block), + .sha2_init(hmac_core.H2_init), + .sha2_next(hmac_core.H2_next), + .tag(hmac_core.tag), + .H1_digest_ready((hmac_core.H1_ready && hmac_core.H2_ready) && !hmac_core.first_round), + .H1_setup_digest_ready(hmac_core.H1_ready && !hmac_core.first_round), + .H2_digest_ready(hmac_core.H2_ready && !hmac_core.first_round), + .hmac_msg_valid(hmac_core.init_cmd || hmac_core.next_cmd), + .H1_digest_valid(hmac_core.H1_digest_valid && hmac_core.H2_digest_valid), + .H1_setup_digest_valid(hmac_core.H1_digest_valid), + .H2_digest_valid(hmac_core.H2_digest_valid), + .hmac_msg_ready(hmac_core.ready), + .tag_valid(hmac_core.tag_valid), + .hmac_key((hmac_core.key)), + .hmac_block_msg((hmac_core.block_msg)), + .sha_digest_out_opad({hmac_core.H2_digest,hmac_core.garbage_bit_vector2}), + .idle(hmac_core.hmac_ctrl_reg==3'h0), + .ctrl_ipad(hmac_core.hmac_ctrl_reg==3'h1), + .ctrl_opad(hmac_core.hmac_ctrl_reg==3'h2), + .ctrl_hmac(hmac_core.hmac_ctrl_reg==3'h3), + .done_tag(hmac_core.hmac_ctrl_reg==3'h4) +); diff --git a/src/hmac/formal/properties/fv_hmac_pkg.sv b/src/hmac/formal/properties/fv_hmac_pkg.sv new file mode 100644 index 000000000..4f40fd576 --- /dev/null +++ b/src/hmac/formal/properties/fv_hmac_pkg.sv @@ -0,0 +1,28 @@ +package global_package; + + +// Constants + +localparam bit unsigned [639:0] FINAL_PAD = 640'h8000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000580; + +localparam bit unsigned [1023:0] IPAD = 1024'h3636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636; + +localparam bit unsigned [1023:0] OPAD = 1024'h5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C5C; + + +// Functions + +function bit unsigned [1023:0] hmac_padded(bit unsigned [383:0] hmac_digest); + return ((hmac_digest << 384'd640) | FINAL_PAD); +endfunction + +function bit unsigned [1023:0] key_ipadded(bit unsigned [383:0] key); + return ((key << 384'd640) ^ IPAD); +endfunction + +function bit unsigned [1023:0] key_opadded(bit unsigned [383:0] key); + return ((key << 384'd640) ^ OPAD); +endfunction + + +endpackage diff --git a/src/hmac/formal/properties/fv_key_stable_top.sv b/src/hmac/formal/properties/fv_key_stable_top.sv new file mode 100644 index 000000000..661e6ee27 --- /dev/null +++ b/src/hmac/formal/properties/fv_key_stable_top.sv @@ -0,0 +1,28 @@ +module fv_key_stable_top_m +( + input logic clk, + input logic rst_n +); + + default clocking default_clk @(posedge clk); endclocking + +//TODO: hmac top should keep the key stable for signle computation. Check with assertion +logic [383:0] hmac_key; +logic hmac_init; + +assign hmac_key = hmac_ctrl.hmac_inst.core.key; +assign hmac_init = hmac_ctrl.hmac_inst.core.init_cmd; + + +assert_wip_key_stable: assert property(disable iff(!rst_n) + hmac_init + |=> + ($stable(hmac_key) || hmac_init) + ); + + +endmodule + bind hmac_ctrl fv_key_stable_top_m fv_key_stable_top ( + .clk (clk ), + .rst_n (reset_n ) + ); \ No newline at end of file diff --git a/src/hmac/formal/readme.md b/src/hmac/formal/readme.md new file mode 100644 index 000000000..82a97de80 --- /dev/null +++ b/src/hmac/formal/readme.md @@ -0,0 +1,70 @@ +# HMAC + +Date: 28-07-2023 Author: LUBIS EDA + +## Folder Structure + +The following subdirectories are part of the main directory **formal** + +- model: Contains the high level abstracted model +- properties: Contains the assertion IP(AIP) named as fv_hmac.sv and the constraints in place for the respective AIP fv_constraints.sv and fv_constraints_wip.sv + +## DUT Overview + +The DUT hmac_core has the primary inputs and primary outputs as shown below. + +|S.No | Port |Direction| Description | +|---- |----------------- |-------- |-------------------------------------------------------------------------------------------| +|1 |clk | input | The positive edge of the clk is used for all the signals | +|2 |reset_n | input | The reset signal is active low and resets the core | +|3 |zeroize | input | The core is reseted when this signal is triggered. | +|4 |init_cmd | input | The core is initialised with respective mode constants and processes the message. | +|5 |next_cmd | input | The core processes the message block with the previously computed results | +|6 |key[383:0] | input | The input key | +|7 |block_msg[1023:0] | input | The padded block message | +|8 |lfsr_seed[147:0] | input | The input constant value that is feed to sha512_masked as an input for digest computation | +|8 |ready | output | When triggered indicates that the core is ready | +|9 |tag[383:0] | output | The tag value of the given message block | +|10 |tag_valid | output | When triggered indicates that the computed tag is ready | + +Hmac algorithm starts with padding the key with IPAD and OPAD constants. Once HMAC receives init_cmd, it initalizes both HMAC and first instantance of SHA, with IPAD padded key. With next_cmd, HMAC feeds block msg to first instantance of SHA, at the same time initalizes second instantance of SHA with OPAD padded key. With the digest recieved from first SHA, the digest is padded to have 1024 bit and later feed to second instantance of SHA, to get the final digest value, which the tag for HMAC. The digest of SHA is always of 512 bits, first 384 is considered valid while rest is garabage value. + +## Assertion IP Overview + +The Assertion IP signals are bound with the respective signals in the dut, where for the rst is binded with the DUT (reset_n && !zeroize), which ensures the reset functionality. Assertion IP is binded with hmac_core and checks for the functionality of only hmac_core. The digest of sha512_masked_core is considered to be cut open. This is perfomed on the formal tool. This way the tool has the freedom to choose any random value of digest coming out of sha512_maked_core so as to reduce the complex functionality of sha512 hashing. With this approach, IP makes sure hmac_core is functionality correct irrespective of correct computed value of digest and helps in proof convergence. Constraints are made on init_cmd and next_cmd signals of hmac_core The constraints can be looked up at fv_constraints.sv. + +- reset_a: Checks that all the resgiters are resetted and the state is idle, with the ready to high. + +- ctrl_hmac_to_done_tag_a: Checks the necessary registers, outputs holds the values when state transits from Done to idle, + +- done_tag_to_idle_a: Checks if tag register outputs correct value and tag_valid is high, when transition from done to idle states. + +- idle_to_ctrl_ipad_a: Checks if the state is in idle , if init is triggered then the sha_blocks should be assigned with respective padded key values and SHA1 is initailized. + +- idle_to_ctrl_opad_a: Checks if the state is in idle , if next is triggered then SHA2 is initailized with right padded key value, and SHA1 should be assigned with hmac block msg. + +- ctrl_ipad_to_ctrl_opad_a: Checks if the state is transitioned from inner_padding to outer_padding state , then SHA2 is initailized with right padded key value, and SHA1 should be assigned with hmac block msg. + +- ctrl_hmac_wait_a: Checks if digest from SHA2 is not ready, it remains in the same state until digest is ready. + +- idle_wait_a: Checks if the state remains same until, there is an init or next command. + +- ctrl_ipad_wait_a: Checks if the state remains same until, digest from SHA1 is ready. + +- ctrl_opad_wait_a: Checks if the state remains same until, digest from SHA2 is ready. + + +## Reproduce results + +The AIP has been tested with two major FV tools. For both tools proves pass in less then 2 hour and coverage is at 100%. + +For reproducing the results: +Load the AIP, hmac_core and fv_constraints together in your formal tool. +To ensure converging proves cut the following signals: + +cut u_sha512_core_h1.digest +cut u_sha512_core_h2.digest + +The sha512_masked core had been verified separately. By cutting the signal model complexity is drastically reduced. + +Feel free to reach out to contact@lubis-eda.com to request the loadscripts. \ No newline at end of file From 797dda75594ad2e4c8b1944449bcab61df8f854b Mon Sep 17 00:00:00 2001 From: tobias ludwig Date: Wed, 13 Sep 2023 15:07:31 +0200 Subject: [PATCH 5/5] Updated coprights --- src/hmac/formal/model/HMAC.luref | 640 ------------------ src/hmac/formal/model/hmac_core.h | 18 + src/hmac/formal/model/refinement.luctrl | 9 - .../model/simulation_model/hmac_sha_join.h | 19 + .../formal/model/simulation_model/sha_algo.h | 19 + .../model/simulation_model/sha_algo_masked.h | 19 + src/hmac/formal/model/simulation_model/top.h | 19 + src/hmac/formal/properties/fv_constraints.sv | 19 + .../formal/properties/fv_constraints_wip.sv | 19 + src/hmac/formal/properties/fv_coverpoints.sv | 18 + src/hmac/formal/properties/fv_hmac_core.sv | 19 +- src/hmac/formal/properties/fv_hmac_pkg.sv | 19 + .../formal/properties/fv_key_stable_top.sv | 19 + 13 files changed, 206 insertions(+), 650 deletions(-) delete mode 100644 src/hmac/formal/model/HMAC.luref delete mode 100644 src/hmac/formal/model/refinement.luctrl diff --git a/src/hmac/formal/model/HMAC.luref b/src/hmac/formal/model/HMAC.luref deleted file mode 100644 index d0ccbea25..000000000 --- a/src/hmac/formal/model/HMAC.luref +++ /dev/null @@ -1,640 +0,0 @@ -{ - "version": 17, - "module": { - "name": "HMAC", - "reset_signal": { - "signal": "(!hmac_core.reset_n || hmac_core.zeroize)", - "is_active_low": false - }, - "clock_signal": { - "signal": "hmac_core.clk", - "is_falling_edge": false - }, - "next_shift_amount": 0, - "rtl_module_name": "hmac_core", - "instance_name": "fv_hmac_core", - "default_assertion_duration": 1, - "default_disable_iff": "", - "reset": { - "documentation_comment": "" - }, - "additional_includes": "", - "additional_imports": "", - "sync_macros": [ - { - "name": "H1_digest_sync", - "datatype": "bool", - "refinement": "(hmac_core.H1_ready && hmac_core.H2_ready) && !hmac_core.first_round", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "H1_setup_digest_sync", - "datatype": "bool", - "refinement": "hmac_core.H1_ready && !hmac_core.first_round", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "H2_digest_sync", - "datatype": "bool", - "refinement": "hmac_core.H2_ready && !hmac_core.first_round", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "hmac_msg_sync", - "datatype": "bool", - "refinement": "hmac_core.init_cmd || hmac_core.next_cmd", - "create_commitments": true, - "timing": 0, - "unused": false - } - ], - "notify_macros": [ - { - "name": "H1_digest_notify", - "datatype": "bool", - "refinement": "hmac_core.H1_digest_valid && hmac_core.H2_digest_valid", - "create_commitments": false, - "timing": 0, - "unused": false - }, - { - "name": "H1_setup_digest_notify", - "datatype": "bool", - "refinement": "hmac_core.H1_digest_valid", - "create_commitments": false, - "timing": 0, - "unused": false - }, - { - "name": "H2_digest_notify", - "datatype": "bool", - "refinement": "hmac_core.H2_digest_valid", - "create_commitments": false, - "timing": 0, - "unused": false - }, - { - "name": "hmac_msg_notify", - "datatype": "bool", - "refinement": "hmac_core.ready", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "sha_msg_1_notify", - "datatype": "bool", - "refinement": "1'b1", - "create_commitments": false, - "timing": 0, - "unused": true - }, - { - "name": "sha_msg_2_notify", - "datatype": "bool", - "refinement": "1'b1", - "create_commitments": false, - "timing": 0, - "unused": true - }, - { - "name": "tag_notify", - "datatype": "bool", - "refinement": "hmac_core.tag_valid", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "sha_msg_notify", - "datatype": "bool", - "refinement": "", - "create_commitments": true, - "timing": 0, - "unused": false - } - ], - "input_datapath_macros": [ - { - "name": "H1_digest_sig", - "datatype": "sc_big_unsigned_512", - "refinement": "{hmac_core.H1_digest,hmac_core.garbage_bit_vector1}", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "H1_setup_digest_sig", - "datatype": "sc_big_unsigned_512", - "refinement": "{hmac_core.H1_digest,hmac_core.garbage_bit_vector1}", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "H2_digest_sig", - "datatype": "sc_big_unsigned_512", - "refinement": "{hmac_core.H2_digest,hmac_core.garbage_bit_vector2}", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "hmac_msg_sig_block_msg", - "datatype": "sc_big_unsigned_1024", - "refinement": "hmac_core.block_msg", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "hmac_msg_sig_init", - "datatype": "bool", - "refinement": "!hmac_core.next_cmd", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "hmac_msg_sig_key", - "datatype": "sc_big_unsigned_384", - "refinement": "hmac_core.key", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "hmac_msg_sig_next", - "datatype": "bool", - "refinement": "hmac_core.next_cmd", - "create_commitments": true, - "timing": 0, - "unused": false - } - ], - "output_datapath_macros": [ - { - "name": "sha_msg_1_sig_sha1_block_msg", - "datatype": "sc_big_unsigned_1024", - "refinement": "hmac_core.H1_block", - "create_commitments": true, - "timing": 0, - "unused": true - }, - { - "name": "sha_msg_1_sig_sha1_init", - "datatype": "bool", - "refinement": "hmac_core.H1_init", - "create_commitments": true, - "timing": 0, - "unused": true - }, - { - "name": "sha_msg_1_sig_sha1_next", - "datatype": "bool", - "refinement": "hmac_core.H1_next", - "create_commitments": true, - "timing": 0, - "unused": true - }, - { - "name": "sha_msg_1_sig_sha2_block_msg", - "datatype": "sc_big_unsigned_1024", - "refinement": "hmac_core.H2_block", - "create_commitments": true, - "timing": 0, - "unused": true - }, - { - "name": "sha_msg_1_sig_sha2_init", - "datatype": "bool", - "refinement": "hmac_core.H2_init", - "create_commitments": true, - "timing": 0, - "unused": true - }, - { - "name": "sha_msg_1_sig_sha2_next", - "datatype": "bool", - "refinement": "hmac_core.H2_next", - "create_commitments": true, - "timing": 0, - "unused": true - }, - { - "name": "sha_msg_2_sig_sha1_block_msg", - "datatype": "sc_big_unsigned_1024", - "refinement": "hmac_core.H1_block", - "create_commitments": true, - "timing": 0, - "unused": true - }, - { - "name": "sha_msg_2_sig_sha1_init", - "datatype": "bool", - "refinement": "hmac_core.H1_init", - "create_commitments": true, - "timing": 0, - "unused": true - }, - { - "name": "sha_msg_2_sig_sha1_next", - "datatype": "bool", - "refinement": "hmac_core.H1_next", - "create_commitments": true, - "timing": 0, - "unused": true - }, - { - "name": "sha_msg_2_sig_sha2_block_msg", - "datatype": "sc_big_unsigned_1024", - "refinement": "hmac_core.H2_block", - "create_commitments": true, - "timing": 0, - "unused": true - }, - { - "name": "sha_msg_2_sig_sha2_init", - "datatype": "bool", - "refinement": "hmac_core.H2_init", - "create_commitments": true, - "timing": 0, - "unused": true - }, - { - "name": "sha_msg_2_sig_sha2_next", - "datatype": "bool", - "refinement": "hmac_core.H2_next", - "create_commitments": true, - "timing": 0, - "unused": true - }, - { - "name": "tag_sig", - "datatype": "sc_big_unsigned_384", - "refinement": "hmac_core.tag", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "sha_msg_sig_sha1_block_msg", - "datatype": "sc_big_unsigned_1024", - "refinement": "", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "sha_msg_sig_sha1_init", - "datatype": "bool", - "refinement": "", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "sha_msg_sig_sha1_next", - "datatype": "bool", - "refinement": "", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "sha_msg_sig_sha2_block_msg", - "datatype": "sc_big_unsigned_1024", - "refinement": "", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "sha_msg_sig_sha2_init", - "datatype": "bool", - "refinement": "", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "sha_msg_sig_sha2_next", - "datatype": "bool", - "refinement": "", - "create_commitments": true, - "timing": 0, - "unused": false - } - ], - "state_macros": [ - { - "name": "compute_tag", - "datatype": "bool", - "refinement": "hmac_core.hmac_ctrl_reg==3'h3", - "create_commitments": true, - "timing": 0, - "unused": true - }, - { - "name": "done", - "datatype": "bool", - "refinement": "hmac_core.hmac_ctrl_reg==3'h4", - "create_commitments": true, - "timing": 0, - "unused": true - }, - { - "name": "idle", - "datatype": "bool", - "refinement": "hmac_core.hmac_ctrl_reg==3'h0", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "sha1_setup", - "datatype": "bool", - "refinement": "hmac_core.hmac_ctrl_reg==3'h1", - "create_commitments": true, - "timing": 0, - "unused": true - }, - { - "name": "sha2_setup", - "datatype": "bool", - "refinement": "hmac_core.hmac_ctrl_reg==3'h2", - "create_commitments": true, - "timing": 0, - "unused": true - }, - { - "name": "ipad", - "datatype": "bool", - "refinement": "", - "create_commitments": true, - "timing": 0, - "unused": true - }, - { - "name": "opad", - "datatype": "bool", - "refinement": "", - "create_commitments": true, - "timing": 0, - "unused": true - }, - { - "name": "hmac_done", - "datatype": "bool", - "refinement": "", - "create_commitments": true, - "timing": 0, - "unused": true - }, - { - "name": "done_tag", - "datatype": "bool", - "refinement": "", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "ctrl_ipad", - "datatype": "bool", - "refinement": "", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "ctrl_opad", - "datatype": "bool", - "refinement": "", - "create_commitments": true, - "timing": 0, - "unused": false - }, - { - "name": "ctrl_hmac", - "datatype": "bool", - "refinement": "", - "create_commitments": true, - "timing": 0, - "unused": false - } - ], - "register_macros": [ - { - "name": "hmac_block_msg", - "datatype": "sc_big_unsigned_1024", - "refinement": "(hmac_core.block_msg)", - "create_commitments": false, - "timing": 0, - "unused": false - }, - { - "name": "hmac_key", - "datatype": "sc_big_unsigned_384", - "refinement": "(hmac_core.key)", - "create_commitments": false, - "timing": 0, - "unused": false - }, - { - "name": "sha_digest_out_opad", - "datatype": "sc_big_unsigned_512", - "refinement": "{hmac_core.H2_digest,hmac_core.garbage_bit_vector2}", - "create_commitments": false, - "timing": 0, - "unused": false - } - ], - "assertions": [ - { - "name": "compute_tag_to_done", - "disable_iff": "", - "duration": -1, - "documentation_comment": "", - "unused": true - }, - { - "name": "done_to_idle", - "disable_iff": "", - "duration": -1, - "documentation_comment": "", - "unused": true - }, - { - "name": "idle_to_sha1_setup", - "disable_iff": "", - "duration": -1, - "documentation_comment": "", - "unused": true - }, - { - "name": "idle_to_sha2_setup", - "disable_iff": "", - "duration": -1, - "documentation_comment": "", - "unused": true - }, - { - "name": "sha1_setup_to_sha2_setup", - "disable_iff": "", - "duration": -1, - "documentation_comment": "", - "unused": true - }, - { - "name": "sha2_setup_to_compute_tag", - "disable_iff": "", - "duration": -1, - "documentation_comment": "", - "unused": true - }, - { - "name": "hmac_done_to_done", - "disable_iff": "", - "duration": -1, - "documentation_comment": "", - "unused": true - }, - { - "name": "idle_to_ipad", - "disable_iff": "", - "duration": -1, - "documentation_comment": "", - "unused": true - }, - { - "name": "idle_to_opad", - "disable_iff": "", - "duration": -1, - "documentation_comment": "", - "unused": true - }, - { - "name": "ipad_to_opad", - "disable_iff": "", - "duration": -1, - "documentation_comment": "", - "unused": true - }, - { - "name": "opad_to_hmac_done", - "disable_iff": "", - "duration": -1, - "documentation_comment": "", - "unused": true - }, - { - "name": "done_tag_to_idle", - "disable_iff": "", - "duration": -1, - "documentation_comment": "", - "unused": false - }, - { - "name": "hmac_done_to_done_tag", - "disable_iff": "", - "duration": -1, - "documentation_comment": "", - "unused": true - }, - { - "name": "ctrl_hmac_to_done_tag", - "disable_iff": "", - "duration": -1, - "documentation_comment": "", - "unused": false - }, - { - "name": "ctrl_ipad_to_ctrl_opad", - "disable_iff": "", - "duration": -1, - "documentation_comment": "", - "unused": false - }, - { - "name": "ctrl_opad_to_ctrl_hmac", - "disable_iff": "", - "duration": -1, - "documentation_comment": "", - "unused": false - }, - { - "name": "idle_to_ctrl_ipad", - "disable_iff": "", - "duration": -1, - "documentation_comment": "", - "unused": false - }, - { - "name": "idle_to_ctrl_opad", - "disable_iff": "", - "duration": -1, - "documentation_comment": "", - "unused": false - } - ], - "waits": [ - { - "name": "compute_tag_wait", - "documentation_comment": "", - "unused": true - }, - { - "name": "idle_wait", - "documentation_comment": "", - "unused": false - }, - { - "name": "sha1_setup_wait", - "documentation_comment": "", - "unused": true - }, - { - "name": "sha2_setup_wait", - "documentation_comment": "", - "unused": true - }, - { - "name": "hmac_done_wait", - "documentation_comment": "", - "unused": true - }, - { - "name": "ipad_wait", - "documentation_comment": "", - "unused": true - }, - { - "name": "opad_wait", - "documentation_comment": "", - "unused": true - }, - { - "name": "ctrl_hmac_wait", - "documentation_comment": "", - "unused": false - }, - { - "name": "ctrl_ipad_wait", - "documentation_comment": "", - "unused": false - }, - { - "name": "ctrl_opad_wait", - "documentation_comment": "", - "unused": false - } - ] - } -} \ No newline at end of file diff --git a/src/hmac/formal/model/hmac_core.h b/src/hmac/formal/model/hmac_core.h index 935f34fd6..b534e3046 100644 --- a/src/hmac/formal/model/hmac_core.h +++ b/src/hmac/formal/model/hmac_core.h @@ -1,3 +1,21 @@ +// ------------------------------------------------- +// Contact: contact@lubis-eda.com +// Author: Tobias Ludwig, Michael Schwarz +// ------------------------------------------------- +// SPDX-License-Identifier: Apache-2.0 +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// #ifndef HMAC_H_ #define HMAC_H_ diff --git a/src/hmac/formal/model/refinement.luctrl b/src/hmac/formal/model/refinement.luctrl deleted file mode 100644 index 5dddd9870..000000000 --- a/src/hmac/formal/model/refinement.luctrl +++ /dev/null @@ -1,9 +0,0 @@ -{ - "version": 13, - "modules": [ - { - "name": "HMAC", - "path": "HMAC.luref" - } - ] -} \ No newline at end of file diff --git a/src/hmac/formal/model/simulation_model/hmac_sha_join.h b/src/hmac/formal/model/simulation_model/hmac_sha_join.h index 275e33a04..775adac21 100644 --- a/src/hmac/formal/model/simulation_model/hmac_sha_join.h +++ b/src/hmac/formal/model/simulation_model/hmac_sha_join.h @@ -1,3 +1,22 @@ +// ------------------------------------------------- +// Contact: contact@lubis-eda.com +// Author: Tobias Ludwig, Michael Schwarz +// ------------------------------------------------- +// SPDX-License-Identifier: Apache-2.0 +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// + #ifndef HMAC_SHA_ #define HMAC_SHA_ diff --git a/src/hmac/formal/model/simulation_model/sha_algo.h b/src/hmac/formal/model/simulation_model/sha_algo.h index 138467449..498359e54 100644 --- a/src/hmac/formal/model/simulation_model/sha_algo.h +++ b/src/hmac/formal/model/simulation_model/sha_algo.h @@ -1,3 +1,22 @@ +// ------------------------------------------------- +// Contact: contact@lubis-eda.com +// Author: Tobias Ludwig, Michael Schwarz +// ------------------------------------------------- +// SPDX-License-Identifier: Apache-2.0 +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// + #ifndef SHA #define SHA diff --git a/src/hmac/formal/model/simulation_model/sha_algo_masked.h b/src/hmac/formal/model/simulation_model/sha_algo_masked.h index 01d2f1449..6187434a9 100644 --- a/src/hmac/formal/model/simulation_model/sha_algo_masked.h +++ b/src/hmac/formal/model/simulation_model/sha_algo_masked.h @@ -1,3 +1,22 @@ +// ------------------------------------------------- +// Contact: contact@lubis-eda.com +// Author: Tobias Ludwig, Michael Schwarz +// ------------------------------------------------- +// SPDX-License-Identifier: Apache-2.0 +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// + #ifndef SHA #define SHA diff --git a/src/hmac/formal/model/simulation_model/top.h b/src/hmac/formal/model/simulation_model/top.h index 76675ada4..3c7c7504f 100644 --- a/src/hmac/formal/model/simulation_model/top.h +++ b/src/hmac/formal/model/simulation_model/top.h @@ -1,3 +1,22 @@ +// ------------------------------------------------- +// 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. +// + #include "systemc.h" #include "Interfaces.h" #include "../hmac_core.h" diff --git a/src/hmac/formal/properties/fv_constraints.sv b/src/hmac/formal/properties/fv_constraints.sv index 41e800989..2b9377ea7 100644 --- a/src/hmac/formal/properties/fv_constraints.sv +++ b/src/hmac/formal/properties/fv_constraints.sv @@ -1,3 +1,22 @@ +// ------------------------------------------------- +// Contact: contact@lubis-eda.com +// Author: Tobias Ludwig, Michael Schwarz +// ------------------------------------------------- +// SPDX-License-Identifier: Apache-2.0 +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// + module fv_constraints_m ( input logic clk, diff --git a/src/hmac/formal/properties/fv_constraints_wip.sv b/src/hmac/formal/properties/fv_constraints_wip.sv index 3413ef780..346e7ac94 100644 --- a/src/hmac/formal/properties/fv_constraints_wip.sv +++ b/src/hmac/formal/properties/fv_constraints_wip.sv @@ -1,3 +1,22 @@ +// ------------------------------------------------- +// 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_wip_m ( input logic clk, diff --git a/src/hmac/formal/properties/fv_coverpoints.sv b/src/hmac/formal/properties/fv_coverpoints.sv index bed308d18..fbbc7b9f6 100644 --- a/src/hmac/formal/properties/fv_coverpoints.sv +++ b/src/hmac/formal/properties/fv_coverpoints.sv @@ -1,3 +1,21 @@ +// ------------------------------------------------- +// 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, diff --git a/src/hmac/formal/properties/fv_hmac_core.sv b/src/hmac/formal/properties/fv_hmac_core.sv index 9745915c8..cfb56bae9 100644 --- a/src/hmac/formal/properties/fv_hmac_core.sv +++ b/src/hmac/formal/properties/fv_hmac_core.sv @@ -1,4 +1,21 @@ - +// ------------------------------------------------- +// 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 global_package::*; module fv_hmac_core_m( diff --git a/src/hmac/formal/properties/fv_hmac_pkg.sv b/src/hmac/formal/properties/fv_hmac_pkg.sv index 4f40fd576..70f635ba6 100644 --- a/src/hmac/formal/properties/fv_hmac_pkg.sv +++ b/src/hmac/formal/properties/fv_hmac_pkg.sv @@ -1,3 +1,22 @@ +// ------------------------------------------------- +// 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 global_package; diff --git a/src/hmac/formal/properties/fv_key_stable_top.sv b/src/hmac/formal/properties/fv_key_stable_top.sv index 661e6ee27..f7f8c88bb 100644 --- a/src/hmac/formal/properties/fv_key_stable_top.sv +++ b/src/hmac/formal/properties/fv_key_stable_top.sv @@ -1,3 +1,22 @@ +// ------------------------------------------------- +// 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_key_stable_top_m ( input logic clk,