Skip to content

Commit

Permalink
Parameterize reg sizes in SVA, add verilator flag around randomization
Browse files Browse the repository at this point in the history
  • Loading branch information
upadhyayulakiran committed Jan 7, 2025
1 parent b371824 commit 86a2f79
Show file tree
Hide file tree
Showing 3 changed files with 45 additions and 24 deletions.
43 changes: 27 additions & 16 deletions src/integration/asserts/caliptra_top_sva.sv
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,17 @@ module caliptra_top_sva
localparam SHA256_DIG_NUM_DWORDS = 8; //`SHA256_PATH.DIG_NUM_DWORDS;
localparam SHA256_BLOCK_NUM_DWORDS = 16; //`SHA256_PATH.BLOCK_NUM_DWORDS;
localparam DOE_256_NUM_ROUNDS = 14; //`DOE_INST_PATH.i_doe_core_cbc.keymem.DOE_256_NUM_ROUNDS

localparam SEED_NUM_DWORDS = 8;
localparam MSG_NUM_DWORDS = 16;
localparam PRIVKEY_NUM_DWORDS = 1224;
localparam PRIVKEY_REG_NUM_DWORDS = 32;
localparam PRIVKEY_REG_RHO_NUM_DWORDS = 8;
localparam SIGNATURE_H_NUM_DWORDS = 21;
localparam VERIFY_RES_NUM_DWORDS = 16;
localparam PRIVKEY_MEM_NUM_DWORDS = PRIVKEY_NUM_DWORDS - PRIVKEY_REG_NUM_DWORDS;
localparam SIGNATURE_C_NUM_DWORDS = 16;
localparam SIGNATURE_Z_NUM_DWORDS = 1120;
localparam SIGNATURE_NUM_DWORDS = SIGNATURE_H_NUM_DWORDS + SIGNATURE_Z_NUM_DWORDS + SIGNATURE_C_NUM_DWORDS;
//TODO: add disable condition based on doe cmd reg
DOE_lock_uds_set: assert property (
@(posedge `SVA_RDC_CLK)
Expand Down Expand Up @@ -275,10 +285,11 @@ module caliptra_top_sva
endgenerate
`endif

`ifndef VERILATOR
//MLDSA data checks
generate
begin: MLDSA_keygen_data_check
for (genvar dword = 0; dword < 32; dword++) begin
for (genvar dword = 0; dword < PRIVKEY_REG_NUM_DWORDS; dword++) begin
MLDSA_privkey_0_31_data_check: assert property (
@(posedge `SVA_RDC_CLK)
disable iff (`CPTRA_TOP_PATH.scan_mode || !`CPTRA_TOP_PATH.security_state.debug_locked)
Expand All @@ -287,22 +298,22 @@ module caliptra_top_sva
else $display("SVA ERROR: [MLDSA keygen] SK output %h does not match expected SK %h at index %h",`MLDSA_PATH.privatekey_reg.raw[dword], {`SERVICES_PATH.mldsa_test_vector.privkey[dword][7:0], `SERVICES_PATH.mldsa_test_vector.privkey[dword][15:8], `SERVICES_PATH.mldsa_test_vector.privkey[dword][23:16], `SERVICES_PATH.mldsa_test_vector.privkey[dword][31:24]}, dword);
end

for (genvar dword = 0; dword < 596; dword++) begin
for (genvar dword = 0; dword < PRIVKEY_MEM_NUM_DWORDS/2; dword++) begin
MLDSA_privkey_even_data_check: assert property (
@(posedge `SVA_RDC_CLK)
disable iff (`CPTRA_TOP_PATH.scan_mode || !`CPTRA_TOP_PATH.security_state.debug_locked)
(((`SERVICES_PATH.mldsa_keygen || `SERVICES_PATH.mldsa_keygen_signing) && `MLDSA_PATH.mldsa_status_done_p) |=> (`MLDSA_PATH.mldsa_sk_ram_bank0.ram[dword] == {`SERVICES_PATH.mldsa_test_vector.privkey[32+(2*dword)][7:0], `SERVICES_PATH.mldsa_test_vector.privkey[32+(2*dword)][15:8], `SERVICES_PATH.mldsa_test_vector.privkey[32+(2*dword)][23:16], `SERVICES_PATH.mldsa_test_vector.privkey[32+(2*dword)][31:24]}))
(((`SERVICES_PATH.mldsa_keygen || `SERVICES_PATH.mldsa_keygen_signing) && `MLDSA_PATH.mldsa_status_done_p) |=> (`MLDSA_PATH.mldsa_sk_ram_bank0.ram[dword] == {`SERVICES_PATH.mldsa_test_vector.privkey[PRIVKEY_REG_NUM_DWORDS+(2*dword)][7:0], `SERVICES_PATH.mldsa_test_vector.privkey[PRIVKEY_REG_NUM_DWORDS+(2*dword)][15:8], `SERVICES_PATH.mldsa_test_vector.privkey[PRIVKEY_REG_NUM_DWORDS+(2*dword)][23:16], `SERVICES_PATH.mldsa_test_vector.privkey[PRIVKEY_REG_NUM_DWORDS+(2*dword)][31:24]}))
)
else $display("SVA ERROR: [MLDSA keygen] SK output %h does not match expected SK %h at index %h",`MLDSA_PATH.mldsa_sk_ram_bank0.ram[dword], {`SERVICES_PATH.mldsa_test_vector.privkey[32+(2*dword)][7:0], `SERVICES_PATH.mldsa_test_vector.privkey[32+(2*dword)][15:8], `SERVICES_PATH.mldsa_test_vector.privkey[32+(2*dword)][23:16], `SERVICES_PATH.mldsa_test_vector.privkey[32+(2*dword)][31:24]}, 32+(2*dword));
else $display("SVA ERROR: [MLDSA keygen] SK output %h does not match expected SK %h at index %h",`MLDSA_PATH.mldsa_sk_ram_bank0.ram[dword], {`SERVICES_PATH.mldsa_test_vector.privkey[PRIVKEY_REG_NUM_DWORDS+(2*dword)][7:0], `SERVICES_PATH.mldsa_test_vector.privkey[PRIVKEY_REG_NUM_DWORDS+(2*dword)][15:8], `SERVICES_PATH.mldsa_test_vector.privkey[PRIVKEY_REG_NUM_DWORDS+(2*dword)][23:16], `SERVICES_PATH.mldsa_test_vector.privkey[PRIVKEY_REG_NUM_DWORDS+(2*dword)][31:24]}, PRIVKEY_REG_NUM_DWORDS+(2*dword));
end

for (genvar dword = 0; dword < 596; dword++) begin
for (genvar dword = 0; dword < PRIVKEY_MEM_NUM_DWORDS/2; dword++) begin
MLDSA_privkey_odd_data_check: assert property (
@(posedge `SVA_RDC_CLK)
disable iff (`CPTRA_TOP_PATH.scan_mode || !`CPTRA_TOP_PATH.security_state.debug_locked)
(((`SERVICES_PATH.mldsa_keygen || `SERVICES_PATH.mldsa_keygen_signing) && `MLDSA_PATH.mldsa_status_done_p) |=> (`MLDSA_PATH.mldsa_sk_ram_bank1.ram[dword] == {`SERVICES_PATH.mldsa_test_vector.privkey[33+(2*dword)][7:0], `SERVICES_PATH.mldsa_test_vector.privkey[33+(2*dword)][15:8], `SERVICES_PATH.mldsa_test_vector.privkey[33+(2*dword)][23:16], `SERVICES_PATH.mldsa_test_vector.privkey[33+(2*dword)][31:24]}))
(((`SERVICES_PATH.mldsa_keygen || `SERVICES_PATH.mldsa_keygen_signing) && `MLDSA_PATH.mldsa_status_done_p) |=> (`MLDSA_PATH.mldsa_sk_ram_bank1.ram[dword] == {`SERVICES_PATH.mldsa_test_vector.privkey[PRIVKEY_REG_NUM_DWORDS+1+(2*dword)][7:0], `SERVICES_PATH.mldsa_test_vector.privkey[PRIVKEY_REG_NUM_DWORDS+1+(2*dword)][15:8], `SERVICES_PATH.mldsa_test_vector.privkey[PRIVKEY_REG_NUM_DWORDS+1+(2*dword)][23:16], `SERVICES_PATH.mldsa_test_vector.privkey[PRIVKEY_REG_NUM_DWORDS+1+(2*dword)][31:24]}))
)
else $display("SVA ERROR: [MLDSA keygen] SK output %h does not match expected SK %h at index %h",`MLDSA_PATH.mldsa_sk_ram_bank0.ram[dword], {`SERVICES_PATH.mldsa_test_vector.privkey[33+(2*dword)][7:0], `SERVICES_PATH.mldsa_test_vector.privkey[33+(2*dword)][15:8], `SERVICES_PATH.mldsa_test_vector.privkey[33+(2*dword)][23:16], `SERVICES_PATH.mldsa_test_vector.privkey[33+(2*dword)][31:24]}, 33+(2*dword));
else $display("SVA ERROR: [MLDSA keygen] SK output %h does not match expected SK %h at index %h",`MLDSA_PATH.mldsa_sk_ram_bank0.ram[dword], {`SERVICES_PATH.mldsa_test_vector.privkey[PRIVKEY_REG_NUM_DWORDS+1+(2*dword)][7:0], `SERVICES_PATH.mldsa_test_vector.privkey[PRIVKEY_REG_NUM_DWORDS+1+(2*dword)][15:8], `SERVICES_PATH.mldsa_test_vector.privkey[PRIVKEY_REG_NUM_DWORDS+1+(2*dword)][23:16], `SERVICES_PATH.mldsa_test_vector.privkey[PRIVKEY_REG_NUM_DWORDS+1+(2*dword)][31:24]}, PRIVKEY_REG_NUM_DWORDS+1+(2*dword));
end

for (genvar dword = 0; dword < 8; dword++) begin
Expand Down Expand Up @@ -331,16 +342,16 @@ module caliptra_top_sva
endgenerate
generate
begin: MLDSA_signature_data_check
for (genvar dword = 0; dword < 21; dword++) begin
for (genvar dword = 0; dword < SIGNATURE_H_NUM_DWORDS; dword++) begin
MLDSA_signature_16_36_data_check: assert property (
@(posedge `SVA_RDC_CLK)
disable iff (`CPTRA_TOP_PATH.scan_mode || !`CPTRA_TOP_PATH.security_state.debug_locked)
(((`SERVICES_PATH.mldsa_signing || `SERVICES_PATH.mldsa_keygen_signing) && `MLDSA_PATH.mldsa_status_done_p) |=> (`MLDSA_PATH.signature_reg.raw[16+dword] == {`SERVICES_PATH.mldsa_test_vector.signature[1156-(20-dword)][7:0], `SERVICES_PATH.mldsa_test_vector.signature[1156-(20-dword)][15:8], `SERVICES_PATH.mldsa_test_vector.signature[1156-(20-dword)][23:16], `SERVICES_PATH.mldsa_test_vector.signature[1156-(20-dword)][31:24]}))
(((`SERVICES_PATH.mldsa_signing || `SERVICES_PATH.mldsa_keygen_signing) && `MLDSA_PATH.mldsa_status_done_p) |=> (`MLDSA_PATH.signature_reg.raw[SIGNATURE_C_NUM_DWORDS+dword] == {`SERVICES_PATH.mldsa_test_vector.signature[(SIGNATURE_NUM_DWORDS-1)-((SIGNATURE_H_NUM_DWORDS-1)-dword)][7:0], `SERVICES_PATH.mldsa_test_vector.signature[(SIGNATURE_NUM_DWORDS-1)-((SIGNATURE_H_NUM_DWORDS-1)-dword)][15:8], `SERVICES_PATH.mldsa_test_vector.signature[(SIGNATURE_NUM_DWORDS-1)-((SIGNATURE_H_NUM_DWORDS-1)-dword)][23:16], `SERVICES_PATH.mldsa_test_vector.signature[(SIGNATURE_NUM_DWORDS-1)-((SIGNATURE_H_NUM_DWORDS-1)-dword)][31:24]}))
)
else $display("SVA ERROR: [MLDSA signing] Signature output %h does not match expected signature %h at index %h",`MLDSA_PATH.signature_reg.raw[16+dword], {`SERVICES_PATH.mldsa_test_vector.signature[1156-(20-dword)][7:0], `SERVICES_PATH.mldsa_test_vector.signature[1156-(20-dword)][15:8], `SERVICES_PATH.mldsa_test_vector.signature[1156-(20-dword)][23:16], `SERVICES_PATH.mldsa_test_vector.signature[1156-(20-dword)][31:24]}, 16+dword);
else $display("SVA ERROR: [MLDSA signing] Signature output %h does not match expected signature %h at index %h",`MLDSA_PATH.signature_reg.raw[SIGNATURE_C_NUM_DWORDS+dword], {`SERVICES_PATH.mldsa_test_vector.signature[(SIGNATURE_NUM_DWORDS-1)-((SIGNATURE_H_NUM_DWORDS-1)-dword)][7:0], `SERVICES_PATH.mldsa_test_vector.signature[(SIGNATURE_NUM_DWORDS-1)-((SIGNATURE_H_NUM_DWORDS-1)-dword)][15:8], `SERVICES_PATH.mldsa_test_vector.signature[(SIGNATURE_NUM_DWORDS-1)-((SIGNATURE_H_NUM_DWORDS-1)-dword)][23:16], `SERVICES_PATH.mldsa_test_vector.signature[(SIGNATURE_NUM_DWORDS-1)-((SIGNATURE_H_NUM_DWORDS-1)-dword)][31:24]}, SIGNATURE_C_NUM_DWORDS+dword);
end

for (genvar dword = 0; dword < 16; dword++) begin
for (genvar dword = 0; dword < SIGNATURE_C_NUM_DWORDS; dword++) begin
MLDSA_signature_0_15_data_check: assert property (
@(posedge `SVA_RDC_CLK)
disable iff (`CPTRA_TOP_PATH.scan_mode || !`CPTRA_TOP_PATH.security_state.debug_locked)
Expand All @@ -366,17 +377,17 @@ module caliptra_top_sva
endgenerate
generate
begin: MLDSA_verify_data_check
for (genvar dword = 0; dword < 16; dword++) begin
for (genvar dword = 0; dword < VERIFY_RES_NUM_DWORDS; dword++) begin
MLDSA_verify_res_data_check: assert property (
@(posedge `SVA_RDC_CLK)
disable iff (`CPTRA_TOP_PATH.scan_mode || !`CPTRA_TOP_PATH.security_state.debug_locked)
((`SERVICES_PATH.mldsa_verify && `MLDSA_PATH.mldsa_status_done_p) |=> (`MLDSA_REG_PATH.hwif_out.MLDSA_VERIFY_RES[dword] == {`SERVICES_PATH.mldsa_test_vector.verify_res[15-dword][7:0], `SERVICES_PATH.mldsa_test_vector.verify_res[15-dword][15:8], `SERVICES_PATH.mldsa_test_vector.verify_res[15-dword][23:16], `SERVICES_PATH.mldsa_test_vector.verify_res[15-dword][31:24]}))
((`SERVICES_PATH.mldsa_verify && `MLDSA_PATH.mldsa_status_done_p) |=> (`MLDSA_REG_PATH.hwif_out.MLDSA_VERIFY_RES[dword] == {`SERVICES_PATH.mldsa_test_vector.verify_res[(VERIFY_RES_NUM_DWORDS-1)-dword][7:0], `SERVICES_PATH.mldsa_test_vector.verify_res[(VERIFY_RES_NUM_DWORDS-1)-dword][15:8], `SERVICES_PATH.mldsa_test_vector.verify_res[(VERIFY_RES_NUM_DWORDS-1)-dword][23:16], `SERVICES_PATH.mldsa_test_vector.verify_res[(VERIFY_RES_NUM_DWORDS-1)-dword][31:24]}))
)
else $display("SVA ERROR: [MLDSA verify] Verify output %h does not match expected verify res %h at index %h",`MLDSA_REG_PATH.hwif_out.MLDSA_VERIFY_RES[dword], {`SERVICES_PATH.mldsa_test_vector.verify_res[15-dword][7:0], `SERVICES_PATH.mldsa_test_vector.verify_res[15-dword][15:8], `SERVICES_PATH.mldsa_test_vector.verify_res[15-dword][23:16], `SERVICES_PATH.mldsa_test_vector.verify_res[15-dword][31:24]}, dword);
else $display("SVA ERROR: [MLDSA verify] Verify output %h does not match expected verify res %h at index %h",`MLDSA_REG_PATH.hwif_out.MLDSA_VERIFY_RES[dword], {`SERVICES_PATH.mldsa_test_vector.verify_res[(VERIFY_RES_NUM_DWORDS-1)-dword][7:0], `SERVICES_PATH.mldsa_test_vector.verify_res[(VERIFY_RES_NUM_DWORDS-1)-dword][15:8], `SERVICES_PATH.mldsa_test_vector.verify_res[(VERIFY_RES_NUM_DWORDS-1)-dword][23:16], `SERVICES_PATH.mldsa_test_vector.verify_res[(VERIFY_RES_NUM_DWORDS-1)-dword][31:24]}, dword);
end
end
endgenerate

`endif
//Generate disable signal for fuse_wr_check sva when hwclr is asserted. The disable needs to be for 3 clks in order to ignore the fuses being cleared
logic clear_obf_secrets_f;
logic clear_obf_secrets_ff;
Expand Down
22 changes: 16 additions & 6 deletions src/integration/tb/caliptra_top_tb_services.sv
Original file line number Diff line number Diff line change
Expand Up @@ -92,6 +92,14 @@ module caliptra_top_tb_services
//=========================================================================-
// Parameters
//=========================================================================-
localparam SEED_NUM_DWORDS = 8;
localparam MSG_NUM_DWORDS = 16;
localparam PRIVKEY_NUM_DWORDS = 1224;
localparam PRIVKEY_REG_NUM_DWORDS = 32;
localparam PRIVKEY_REG_RHO_NUM_DWORDS = 8;
localparam SIGNATURE_H_NUM_DWORDS = 21;
localparam VERIFY_RES_NUM_DWORDS = 16;

`ifndef VERILATOR
int MAX_CYCLES;
initial begin
Expand Down Expand Up @@ -641,6 +649,7 @@ module caliptra_top_tb_services
release caliptra_top_dut.mldsa.norm_check_inst.invalid;
end

`ifndef VERILATOR
logic mldsa_keygen, mldsa_signing, mldsa_verify, mldsa_keygen_signing;

always @(negedge clk or negedge cptra_rst_b) begin
Expand Down Expand Up @@ -680,7 +689,7 @@ module caliptra_top_tb_services
genvar mldsa_dword;
generate
//MLDSA keygen - inject seed
for (mldsa_dword = 0; mldsa_dword < 8; mldsa_dword++) begin
for (mldsa_dword = 0; mldsa_dword < SEED_NUM_DWORDS; mldsa_dword++) begin
always @(negedge clk) begin
if (mldsa_keygen | mldsa_keygen_signing) begin
force caliptra_top_dut.mldsa.mldsa_reg_inst.hwif_out.MLDSA_SEED[mldsa_dword].SEED.value = {mldsa_test_vector.seed[7-mldsa_dword][7:0], mldsa_test_vector.seed[7-mldsa_dword][15:8], mldsa_test_vector.seed[7-mldsa_dword][23:16], mldsa_test_vector.seed[7-mldsa_dword][31:24]};
Expand All @@ -692,7 +701,7 @@ module caliptra_top_tb_services
end

//MLDSA signing or MLDSA verify - inject msg
for (mldsa_dword = 0; mldsa_dword < 16; mldsa_dword++) begin
for (mldsa_dword = 0; mldsa_dword < MSG_NUM_DWORDS; mldsa_dword++) begin
always @(negedge clk) begin
if (mldsa_signing | mldsa_verify | mldsa_keygen_signing) begin
force caliptra_top_dut.mldsa.mldsa_reg_inst.hwif_out.MLDSA_MSG[mldsa_dword].MSG.value = {mldsa_test_vector.msg[15-mldsa_dword][7:0], mldsa_test_vector.msg[15-mldsa_dword][15:8], mldsa_test_vector.msg[15-mldsa_dword][23:16], mldsa_test_vector.msg[15-mldsa_dword][31:24]};
Expand All @@ -704,7 +713,7 @@ module caliptra_top_tb_services
end

//MLDSA signing - inject sk
for (mldsa_dword = 0; mldsa_dword < 4; mldsa_dword++) begin
for (mldsa_dword = 0; mldsa_dword < PRIVKEY_REG_RHO_NUM_DWORDS/2; mldsa_dword++) begin
always @(negedge clk) begin
if (mldsa_signing) begin
force caliptra_top_dut.mldsa.mldsa_ctrl_inst.privatekey_reg.enc.rho[mldsa_dword] = {mldsa_test_vector.privkey[((mldsa_dword*2)+1)][7:0], mldsa_test_vector.privkey[((mldsa_dword*2)+1)][15:8], mldsa_test_vector.privkey[((mldsa_dword*2)+1)][23:16], mldsa_test_vector.privkey[((mldsa_dword*2)+1)][31:24],
Expand All @@ -731,7 +740,7 @@ module caliptra_top_tb_services
end
end

for (mldsa_dword = 32; mldsa_dword < 1224; mldsa_dword++) begin
for (mldsa_dword = PRIVKEY_REG_NUM_DWORDS; mldsa_dword < PRIVKEY_NUM_DWORDS; mldsa_dword++) begin
always @(negedge clk) begin
if (mldsa_signing) begin
if ((mldsa_dword % 2) == 0) begin
Expand Down Expand Up @@ -773,7 +782,7 @@ module caliptra_top_tb_services
end

//MLDSA verify - inject signature
for (mldsa_dword = 0; mldsa_dword < 16; mldsa_dword++) begin
for (mldsa_dword = 0; mldsa_dword < VERIFY_RES_NUM_DWORDS; mldsa_dword++) begin
always @(negedge clk) begin
if (mldsa_verify) begin
force caliptra_top_dut.mldsa.mldsa_ctrl_inst.signature_reg.enc.c[mldsa_dword] = {mldsa_test_vector.signature[mldsa_dword][7:0], mldsa_test_vector.signature[mldsa_dword][15:8], mldsa_test_vector.signature[mldsa_dword][23:16], mldsa_test_vector.signature[mldsa_dword][31:24]};
Expand All @@ -783,7 +792,7 @@ module caliptra_top_tb_services
end
end
end
for (mldsa_dword = 0; mldsa_dword < 21; mldsa_dword++) begin
for (mldsa_dword = 0; mldsa_dword < SIGNATURE_H_NUM_DWORDS; mldsa_dword++) begin
always @(negedge clk) begin
if (mldsa_verify) begin
force caliptra_top_dut.mldsa.mldsa_ctrl_inst.signature_reg.enc.h[mldsa_dword] = {mldsa_test_vector.signature[1136+mldsa_dword][7:0], mldsa_test_vector.signature[1136+mldsa_dword][15:8], mldsa_test_vector.signature[1136+mldsa_dword][23:16], mldsa_test_vector.signature[1136+mldsa_dword][31:24]};
Expand All @@ -806,6 +815,7 @@ module caliptra_top_tb_services
end
end
endgenerate
`endif

//Randomized wntz
generate
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -505,15 +505,15 @@ void main() {
mldsa_zeroize();
cptra_intr_rcv.mldsa_notif = 0;

mldsa_keygen_signing_flow(seed, msg, sign_rnd, entropy, sign, 0x00);
mldsa_keygen_signing_flow(seed, msg, sign_rnd, entropy, sign);
mldsa_zeroize();
cptra_intr_rcv.mldsa_notif = 0;

mldsa_signing_flow(privkey, msg, sign_rnd, entropy, sign);
mldsa_zeroize();
cptra_intr_rcv.mldsa_notif = 0;

mldsa_verifying_flow(msg, pubkey, sign, verify_res, 0x00);
mldsa_verifying_flow(msg, pubkey, sign, verify_res);
mldsa_zeroize();
cptra_intr_rcv.mldsa_notif = 0;

Expand Down

0 comments on commit 86a2f79

Please sign in to comment.