../src/lowrisc_ip_hmac_0.1/rtl/hmac.sv Cov: 99.7%

   1: // Copyright lowRISC contributors.
   2: // Licensed under the Apache License, Version 2.0, see LICENSE for details.
   3: // SPDX-License-Identifier: Apache-2.0
   4: //
   5: // HMAC-SHA256
   6: 
   7: `include "prim_assert.sv"
   8: 
   9: module hmac
  10:   import prim_alert_pkg::*;
  11:   import hmac_pkg::*;
  12:   import hmac_reg_pkg::*;
  13: (
  14:   input clk_i,
  15:   input rst_ni,
  16: 
  17:   input  tlul_pkg::tl_h2d_t tl_i,
  18:   output tlul_pkg::tl_d2h_t tl_o,
  19: 
  20:   output logic intr_hmac_done_o,
  21:   output logic intr_fifo_empty_o,
  22:   output logic intr_hmac_err_o,
  23: 
  24:   // alerts
  25:   input  alert_rx_t [NumAlerts-1:0] alert_rx_i,
  26:   output alert_tx_t [NumAlerts-1:0] alert_tx_o
  27: );
  28: 
  29: 
  30:   /////////////////////////
  31:   // Signal declarations //
  32:   /////////////////////////
  33:   hmac_reg2hw_t reg2hw;
  34:   hmac_hw2reg_t hw2reg;
  35: 
  36:   tlul_pkg::tl_h2d_t  tl_win_h2d[1];
  37:   tlul_pkg::tl_d2h_t  tl_win_d2h[1];
  38: 
  39:   logic [255:0] secret_key;
  40: 
  41:   logic        wipe_secret;
  42:   logic [31:0] wipe_v;
  43: 
  44:   logic        fifo_rvalid;
  45:   logic        fifo_rready;
  46:   sha_fifo_t   fifo_rdata;
  47: 
  48:   logic        fifo_wvalid, fifo_wready;
  49:   sha_fifo_t   fifo_wdata;
  50:   logic        fifo_full;
  51:   logic        fifo_empty;
  52:   logic [4:0]  fifo_depth;
  53: 
  54:   logic        msg_fifo_req;
  55:   logic        msg_fifo_gnt;
  56:   logic        msg_fifo_we;
  57:   logic [8:0]  msg_fifo_addr;   // NOT_READ
  58:   logic [31:0] msg_fifo_wdata;
  59:   logic [31:0] msg_fifo_wmask;
  60:   logic [31:0] msg_fifo_rdata;
  61:   logic        msg_fifo_rvalid;
  62:   logic [1:0]  msg_fifo_rerror;
  63:   logic [31:0] msg_fifo_wdata_endian;
  64:   logic [31:0] msg_fifo_wmask_endian;
  65: 
  66:   logic        packer_ready;
  67:   logic        packer_flush_done;
  68: 
  69:   logic        reg_fifo_wvalid;
  70:   sha_word_t   reg_fifo_wdata;
  71:   sha_word_t   reg_fifo_wmask;
  72:   logic        hmac_fifo_wsel;
  73:   logic        hmac_fifo_wvalid;
  74:   logic [2:0]  hmac_fifo_wdata_sel;
  75: 
  76:   logic        shaf_rvalid;
  77:   sha_fifo_t   shaf_rdata;
  78:   logic        shaf_rready;
  79: 
  80:   logic        sha_en;
  81:   logic        hmac_en;
  82:   logic        endian_swap;
  83:   logic        digest_swap;
  84: 
  85:   logic        reg_hash_start;
  86:   logic        sha_hash_start;
  87:   logic        hash_start;      // Valid hash_start_signal
  88:   logic        reg_hash_process;
  89:   logic        sha_hash_process;
  90: 
  91:   logic        reg_hash_done;
  92:   logic        sha_hash_done;
  93: 
  94:   logic [63:0] message_length;
  95:   logic [63:0] sha_message_length;
  96: 
  97:   err_code_e   err_code;
  98:   logic        err_valid;
  99: 
 100:   sha_word_t [7:0] digest;
 101: 
 102:   hmac_reg2hw_cfg_reg_t cfg_reg;
 103:   logic                 cfg_block;  // Prevent changing config
 104:   logic                 msg_allowed; // MSG_FIFO from software is allowed
 105: 
 106:   ///////////////////////
 107:   // Connect registers //
 108:   ///////////////////////
 109:   assign hw2reg.status.fifo_full.d  = fifo_full;
 110:   assign hw2reg.status.fifo_empty.d = fifo_empty;
 111:   assign hw2reg.status.fifo_depth.d = fifo_depth;
 112: 
 113:   // secret key
 114:   assign wipe_secret = reg2hw.wipe_secret.qe;
 115:   assign wipe_v      = reg2hw.wipe_secret.q;
 116: 
 117:   always_ff @(posedge clk_i or negedge rst_ni) begin
 118:     if (!rst_ni) begin
 119:       secret_key <= '0;
 120:     end else if (wipe_secret) begin
 121:       secret_key <= secret_key ^ {8{wipe_v}};
 122:     end else if (!cfg_block) begin
 123:       // Allow updating secret key only when the engine is in Idle.
 124:       for (int i = 0; i < 8; i++) begin
 125:         if (reg2hw.key[7-i].qe) begin
 126:           secret_key[32*i+:32] <= reg2hw.key[7-i].q;
 127:         end
 128:       end
 129:     end
 130:   end
 131: 
 132:   for (genvar i = 0; i < 8; i++) begin : gen_key_digest
 133:     assign hw2reg.key[7-i].d      = '0;
 134:     // digest
 135:     assign hw2reg.digest[i].d = conv_endian(digest[i], digest_swap);
 136:   end
 137: 
 138:   logic [3:0] unused_cfg_qe;
 139: 
 140:   assign unused_cfg_qe = {cfg_reg.sha_en.qe,      cfg_reg.hmac_en.qe,
 141:                           cfg_reg.endian_swap.qe, cfg_reg.digest_swap.qe};
 142: 
 143:   assign sha_en      = cfg_reg.sha_en.q;
 144:   assign hmac_en     = cfg_reg.hmac_en.q;
 145:   assign endian_swap = cfg_reg.endian_swap.q;
 146:   assign digest_swap = cfg_reg.digest_swap.q;
 147:   assign hw2reg.cfg.hmac_en.d     = cfg_reg.hmac_en.q;
 148:   assign hw2reg.cfg.sha_en.d      = cfg_reg.sha_en.q;
 149:   assign hw2reg.cfg.endian_swap.d = cfg_reg.endian_swap.q;
 150:   assign hw2reg.cfg.digest_swap.d = cfg_reg.digest_swap.q;
 151: 
 152:   assign reg_hash_start   = reg2hw.cmd.hash_start.qe   & reg2hw.cmd.hash_start.q;
 153:   assign reg_hash_process = reg2hw.cmd.hash_process.qe & reg2hw.cmd.hash_process.q;
 154: 
 155:   // Error code register
 156:   assign hw2reg.err_code.de = err_valid;
 157:   assign hw2reg.err_code.d  = err_code;
 158: 
 159:   /////////////////////
 160:   // Control signals //
 161:   /////////////////////
 162:   assign hash_start = reg_hash_start & sha_en & ~cfg_block;
 163: 
 164:   always_ff @(posedge clk_i or negedge rst_ni) begin
 165:     if (!rst_ni) begin
 166:       cfg_block <= '0;
 167:     end else if (hash_start) begin
 168:       cfg_block <= 1'b 1;
 169:     end else if (reg_hash_done) begin
 170:       cfg_block <= 1'b 0;
 171:     end
 172:   end
 173:   // Hold the configuration during the process
 174:   always_ff @(posedge clk_i or negedge rst_ni) begin
 175:     if (!rst_ni) begin
 176:       cfg_reg <= '{endian_swap: '{q: 1'b1, qe: 1'b0}, default:'0};
 177:     end else if (!cfg_block && reg2hw.cfg.hmac_en.qe) begin
 178:       cfg_reg <= reg2hw.cfg ;
 179:     end
 180:   end
 181: 
 182:   // Open up the MSG_FIFO from the TL-UL port when it is ready
 183:   always_ff @(posedge clk_i or negedge rst_ni) begin
 184:     if (!rst_ni) begin
 185:       msg_allowed <= '0;
 186:     end else if (hash_start) begin
 187:       msg_allowed <= 1'b 1;
 188:     end else if (packer_flush_done) begin
 189:       msg_allowed <= 1'b 0;
 190:     end
 191:   end
 192:   ////////////////
 193:   // Interrupts //
 194:   ////////////////
 195:   logic fifo_empty_q, fifo_empty_event;
 196:   always_ff @(posedge clk_i or negedge rst_ni) begin
 197:     if (!rst_ni) begin
 198:       fifo_empty_q <= '1; // By default, it is empty
 199:     end else if (!hmac_fifo_wsel) begin
 200:       fifo_empty_q <= fifo_empty;
 201:     end
 202:   end
 203:   assign fifo_empty_event = fifo_empty & ~fifo_empty_q;
 204: 
 205:   logic [2:0] event_intr;
 206:   assign event_intr = {err_valid, fifo_empty_event, reg_hash_done};
 207: 
 208:   // instantiate interrupt hardware primitive
 209:   prim_intr_hw #(.Width(1)) intr_hw_hmac_done (
 210:     .event_intr_i           (event_intr[0]),
 211:     .reg2hw_intr_enable_q_i (reg2hw.intr_enable.hmac_done.q),
 212:     .reg2hw_intr_test_q_i   (reg2hw.intr_test.hmac_done.q),
 213:     .reg2hw_intr_test_qe_i  (reg2hw.intr_test.hmac_done.qe),
 214:     .reg2hw_intr_state_q_i  (reg2hw.intr_state.hmac_done.q),
 215:     .hw2reg_intr_state_de_o (hw2reg.intr_state.hmac_done.de),
 216:     .hw2reg_intr_state_d_o  (hw2reg.intr_state.hmac_done.d),
 217:     .intr_o                 (intr_hmac_done_o)
 218:   );
 219:   prim_intr_hw #(.Width(1)) intr_hw_fifo_empty (
 220:     .event_intr_i           (event_intr[1]),
 221:     .reg2hw_intr_enable_q_i (reg2hw.intr_enable.fifo_empty.q),
 222:     .reg2hw_intr_test_q_i   (reg2hw.intr_test.fifo_empty.q),
 223:     .reg2hw_intr_test_qe_i  (reg2hw.intr_test.fifo_empty.qe),
 224:     .reg2hw_intr_state_q_i  (reg2hw.intr_state.fifo_empty.q),
 225:     .hw2reg_intr_state_de_o (hw2reg.intr_state.fifo_empty.de),
 226:     .hw2reg_intr_state_d_o  (hw2reg.intr_state.fifo_empty.d),
 227:     .intr_o                 (intr_fifo_empty_o)
 228:   );
 229:   prim_intr_hw #(.Width(1)) intr_hw_hmac_err (
 230:     .event_intr_i           (event_intr[2]),
 231:     .reg2hw_intr_enable_q_i (reg2hw.intr_enable.hmac_err.q),
 232:     .reg2hw_intr_test_q_i   (reg2hw.intr_test.hmac_err.q),
 233:     .reg2hw_intr_test_qe_i  (reg2hw.intr_test.hmac_err.qe),
 234:     .reg2hw_intr_state_q_i  (reg2hw.intr_state.hmac_err.q),
 235:     .hw2reg_intr_state_de_o (hw2reg.intr_state.hmac_err.de),
 236:     .hw2reg_intr_state_d_o  (hw2reg.intr_state.hmac_err.d),
 237:     .intr_o                 (intr_hmac_err_o)
 238:   );
 239: 
 240:   ///////////////
 241:   // Instances //
 242:   ///////////////
 243: 
 244:   assign msg_fifo_rvalid = msg_fifo_req & ~msg_fifo_we;
 245:   assign msg_fifo_rdata  = '1;  // Return all F
 246:   assign msg_fifo_rerror = '1;  // Return error for read access
 247:   assign msg_fifo_gnt    = msg_fifo_req & ~hmac_fifo_wsel & packer_ready;
 248: 
 249:   // FIFO control
 250:   sha_fifo_t reg_fifo_wentry;
 251:   assign reg_fifo_wentry.data = conv_endian(reg_fifo_wdata, 1'b1); // always convert
 252:   assign reg_fifo_wentry.mask = {reg_fifo_wmask[0],  reg_fifo_wmask[8],
 253:                                  reg_fifo_wmask[16], reg_fifo_wmask[24]};
 254:   assign fifo_full   = ~fifo_wready;
 255:   assign fifo_empty  = ~fifo_rvalid;
 256:   assign fifo_wvalid = (hmac_fifo_wsel && fifo_wready) ? hmac_fifo_wvalid : reg_fifo_wvalid;
 257:   assign fifo_wdata  = (hmac_fifo_wsel) ? '{data: digest[hmac_fifo_wdata_sel], mask: '1}
 258:                                        : reg_fifo_wentry;
 259: 
 260:   prim_fifo_sync #(
 261:     .Width ($bits(sha_fifo_t)),
 262:     .Pass  (1'b0),
 263:     .Depth (MsgFifoDepth)
 264:   ) u_msg_fifo (
 265:     .clk_i,
 266:     .rst_ni,
 267:     .clr_i  (1'b0),
 268: 
 269:     .wvalid (fifo_wvalid & sha_en),
 270:     .wready (fifo_wready),
 271:     .wdata  (fifo_wdata),
 272: 
 273:     .depth  (fifo_depth),
 274: 
 275:     .rvalid (fifo_rvalid),
 276:     .rready (fifo_rready),
 277:     .rdata  (fifo_rdata)
 278:   );
 279: 
 280:   // TL ADAPTER SRAM
 281:   tlul_adapter_sram #(
 282:     .SramAw (9),
 283:     .SramDw (32),
 284:     .Outstanding (1),
 285:     .ByteAccess  (1),
 286:     .ErrOnRead   (1)
 287:   ) u_tlul_adapter (
 288:     .clk_i,
 289:     .rst_ni,
 290:     .tl_i   (tl_win_h2d[0]),
 291:     .tl_o   (tl_win_d2h[0]),
 292: 
 293:     .req_o    (msg_fifo_req   ),
 294:     .gnt_i    (msg_fifo_gnt   ),
 295:     .we_o     (msg_fifo_we    ),
 296:     .addr_o   (msg_fifo_addr  ), // Doesn't care the address other than sub-word
 297:     .wdata_o  (msg_fifo_wdata ),
 298:     .wmask_o  (msg_fifo_wmask ),
 299:     .rdata_i  (msg_fifo_rdata ),
 300:     .rvalid_i (msg_fifo_rvalid),
 301:     .rerror_i (msg_fifo_rerror)
 302:   );
 303: 
 304:   // TL-UL to MSG_FIFO byte write handling
 305:   logic msg_write;
 306: 
 307:   assign msg_write = msg_fifo_req & msg_fifo_we & ~hmac_fifo_wsel & msg_allowed;
 308: 
 309:   logic [$clog2(32+1)-1:0] wmask_ones;
 310: 
 311:   always_comb begin
 312:     wmask_ones = '0;
 313:     for (int i = 0 ; i < 32 ; i++) begin
 314:       wmask_ones = wmask_ones + msg_fifo_wmask[i];
 315:     end
 316:   end
 317: 
 318:   // Calculate written message
 319:   always_ff @(posedge clk_i or negedge rst_ni) begin
 320:     if (!rst_ni) begin
 321:       message_length <= '0;
 322:     end else if (hash_start) begin
 323:       message_length <= '0;
 324:     end else if (msg_write && sha_en && packer_ready) begin
 325:       message_length <= message_length + 64'(wmask_ones);
 326:     end
 327:   end
 328: 
 329:   assign hw2reg.msg_length_upper.de = 1'b1;
 330:   assign hw2reg.msg_length_upper.d = message_length[63:32];
 331:   assign hw2reg.msg_length_lower.de = 1'b1;
 332:   assign hw2reg.msg_length_lower.d = message_length[31:0];
 333: 
 334: 
 335:   // Convert endian here
 336:   //    prim_packer always packs to the right, but SHA engine assumes incoming
 337:   //    to be big-endian, [31:24] comes first. So, the data is reverted after
 338:   //    prim_packer before the message fifo. here to reverse if not big-endian
 339:   //    before pushing to the packer.
 340:   assign msg_fifo_wdata_endian = conv_endian(msg_fifo_wdata, ~endian_swap);
 341:   assign msg_fifo_wmask_endian = conv_endian(msg_fifo_wmask, ~endian_swap);
 342: 
 343:   prim_packer #(
 344:     .InW      (32),
 345:     .OutW     (32)
 346:   ) u_packer (
 347:     .clk_i,
 348:     .rst_ni,
 349: 
 350:     .valid_i      (msg_write & sha_en),
 351:     .data_i       (msg_fifo_wdata_endian),
 352:     .mask_i       (msg_fifo_wmask_endian),
 353:     .ready_o      (packer_ready),
 354: 
 355:     .valid_o      (reg_fifo_wvalid),
 356:     .data_o       (reg_fifo_wdata),
 357:     .mask_o       (reg_fifo_wmask),
 358:     .ready_i      (fifo_wready & ~hmac_fifo_wsel),
 359: 
 360:     .flush_i      (reg_hash_process),
 361:     .flush_done_o (packer_flush_done) // ignore at this moment
 362:   );
 363: 
 364: 
 365:   hmac_core u_hmac (
 366:     .clk_i,
 367:     .rst_ni,
 368: 
 369:     .secret_key,
 370: 
 371:     .wipe_secret,
 372:     .wipe_v,
 373: 
 374:     .hmac_en,
 375: 
 376:     .reg_hash_start   (hash_start),
 377:     .reg_hash_process (packer_flush_done), // Trigger after all msg written
 378:     .hash_done      (reg_hash_done),
 379:     .sha_hash_start,
 380:     .sha_hash_process,
 381:     .sha_hash_done,
 382: 
 383:     .sha_rvalid     (shaf_rvalid),
 384:     .sha_rdata      (shaf_rdata),
 385:     .sha_rready     (shaf_rready),
 386: 
 387:     .fifo_rvalid,
 388:     .fifo_rdata,
 389:     .fifo_rready,
 390: 
 391:     .fifo_wsel      (hmac_fifo_wsel),
 392:     .fifo_wvalid    (hmac_fifo_wvalid),
 393:     .fifo_wdata_sel (hmac_fifo_wdata_sel),
 394:     .fifo_wready,
 395: 
 396:     .message_length,
 397:     .sha_message_length
 398:   );
 399: 
 400:   sha2 u_sha2 (
 401:     .clk_i,
 402:     .rst_ni,
 403: 
 404:     .wipe_secret,
 405:     .wipe_v,
 406: 
 407:     .fifo_rvalid      (shaf_rvalid),
 408:     .fifo_rdata       (shaf_rdata),
 409:     .fifo_rready      (shaf_rready),
 410: 
 411:     .sha_en,
 412:     .hash_start       (sha_hash_start),
 413:     .hash_process     (sha_hash_process),
 414:     .hash_done        (sha_hash_done),
 415: 
 416:     .message_length   (sha_message_length),
 417: 
 418:     .digest
 419:   );
 420: 
 421:   hmac_reg_top u_reg (
 422:     .clk_i,
 423:     .rst_ni,
 424: 
 425:     .tl_i,
 426:     .tl_o,
 427: 
 428:     .tl_win_o   (tl_win_h2d),
 429:     .tl_win_i   (tl_win_d2h),
 430: 
 431:     .reg2hw,
 432:     .hw2reg,
 433: 
 434:     .devmode_i  (1'b1)
 435:   );
 436: 
 437:   /////////////////////////
 438:   // HMAC Error Handling //
 439:   /////////////////////////
 440:   logic msg_push_sha_disabled, hash_start_sha_disabled, update_seckey_inprocess;
 441:   logic hash_start_active;  // `reg_hash_start` set when hash already in active
 442:   logic msg_push_not_allowed; // Message is received when `hash_start` isn't set
 443:   assign msg_push_sha_disabled = msg_write & ~sha_en;
 444:   assign hash_start_sha_disabled = reg_hash_start & ~sha_en;
 445:   assign hash_start_active = reg_hash_start & cfg_block;
 446:   assign msg_push_not_allowed = msg_fifo_req & ~msg_allowed;
 447: 
 448:   always_comb begin
 449:     update_seckey_inprocess = 1'b0;
 450:     if (cfg_block) begin
 451:       for (int i = 0 ; i < 8 ; i++) begin
 452:         if (reg2hw.key[i].qe) begin
 453:           update_seckey_inprocess = update_seckey_inprocess | 1'b1;
 454:         end
 455:       end
 456:     end else begin
 457:       update_seckey_inprocess = 1'b0;
 458:     end
 459:   end
 460: 
 461:   // Update ERR_CODE register and interrupt only when no pending interrupt.
 462:   // This ensures only the first event of the series of events can be seen to sw.
 463:   // It is recommended that the software reads ERR_CODE register when interrupt
 464:   // is pending to avoid any race conditions.
 465:   assign err_valid = ~reg2hw.intr_state.hmac_err.q &
 466:                    ( msg_push_sha_disabled | hash_start_sha_disabled
 467:                    | update_seckey_inprocess | hash_start_active
 468:                    | msg_push_not_allowed );
 469: 
 470:   always_comb begin
 471:     err_code = NoError;
 472:     unique case (1'b1)
 473:       msg_push_sha_disabled: begin
 474:         err_code = SwPushMsgWhenShaDisabled;
 475:       end
 476:       hash_start_sha_disabled: begin
 477:         err_code = SwHashStartWhenShaDisabled;
 478:       end
 479: 
 480:       update_seckey_inprocess: begin
 481:         err_code = SwUpdateSecretKeyInProcess;
 482:       end
 483: 
 484:       hash_start_active: begin
 485:         err_code = SwHashStartWhenActive;
 486:       end
 487: 
 488:       msg_push_not_allowed: begin
 489:         err_code = SwPushMsgWhenDisallowed;
 490:       end
 491: 
 492:       default: begin
 493:         err_code = NoError;
 494:       end
 495:     endcase
 496:   end
 497: 
 498:   /////////////////////
 499:   // Hardware Alerts //
 500:   /////////////////////
 501: 
 502:   // TODO: add CSR with REGWEN to test alert via SW
 503:   logic [NumAlerts-1:0] alerts;
 504:   assign alerts = {msg_push_sha_disabled};
 505: 
 506:   for (genvar j = 0; j < hmac_pkg::NumAlerts; j++) begin : gen_alert_tx
 507:     prim_alert_sender #(
 508:       .AsyncOn(hmac_pkg::AlertAsyncOn[j])
 509:     ) i_prim_alert_sender (
 510:       .clk_i      ( clk_i         ),
 511:       .rst_ni     ( rst_ni        ),
 512:       .alert_i    ( alerts[j]     ),
 513:       .alert_rx_i ( alert_rx_i[j] ),
 514:       .alert_tx_o ( alert_tx_o[j] )
 515:     );
 516:   end : gen_alert_tx
 517: 
 518:   //////////////////////////////////////////////
 519:   // Assertions, Assumptions, and Coverpoints //
 520:   //////////////////////////////////////////////
 521: 
 522: `ifndef VERILATOR
 523: `ifndef SYNTHESIS
 524:   // HMAC assumes TL-UL mask is byte-aligned.
 525:   property wmask_bytealign_p(wmask_byte, clk, rst_n);
 526:     @(posedge clk) disable iff (rst_n == 0)
 527:       msg_fifo_req & msg_fifo_we |-> wmask_byte inside {'0, '1};
 528:   endproperty
 529: 
 530:   for (genvar i = 0 ; i < 4; i++) begin: gen_assert_wmask_bytealign
 531:     assert property (wmask_bytealign_p(msg_fifo_wmask[8*i+:8], clk_i, rst_ni));
 532:   end
 533: 
 534:   // To pass FPV, this shouldn't add pragma translate_off even these two signals
 535:   // are used in Assertion only
 536:   logic in_process;
 537:   always_ff @(posedge clk_i or negedge rst_ni) begin
 538:     if (!rst_ni)               in_process <= 1'b0;
 539:     else if (reg_hash_process) in_process <= 1'b1;
 540:     else if (reg_hash_done)    in_process <= 1'b0;
 541:   end
 542: 
 543:   logic initiated;
 544:   always_ff @(posedge clk_i or negedge rst_ni) begin
 545:     if (!rst_ni)               initiated <= 1'b0;
 546:     else if (hash_start)       initiated <= 1'b1;
 547:     else if (reg_hash_process) initiated <= 1'b0;
 548:   end
 549: 
 550:   // the host doesn't write data after hash_process until hash_start.
 551:   // Same as "message_length shouldn't be changed between hash_process and done
 552:   `ASSERT(ValidWriteAssert, msg_fifo_req |-> !in_process)
 553: 
 554:   // `hash_process` shall be toggle and paired with `hash_start`.
 555:   // Below condition is covered by the design (2020-02-19)
 556:   //`ASSERT(ValidHashStartAssert, hash_start |-> !initiated)
 557:   `ASSERT(ValidHashProcessAssert, reg_hash_process |-> initiated)
 558: 
 559:   // between `hash_done` and `hash_start`, message FIFO should be empty
 560:   `ASSERT(MsgFifoEmptyWhenNoOpAssert,
 561:           !in_process && !initiated |-> $stable(message_length))
 562: 
 563:   // hmac_en should be modified only when the logic is Idle
 564:   `ASSERT(ValidHmacEnConditionAssert,
 565:           hmac_en != $past(hmac_en) |-> !in_process && !initiated)
 566: 
 567:   // All outputs should be known value after reset
 568:   `ASSERT_KNOWN(IntrHmacDoneOKnown, intr_hmac_done_o)
 569:   `ASSERT_KNOWN(IntrFifoEmptyOKnown, intr_fifo_empty_o)
 570:   `ASSERT_KNOWN(TlODValidKnown, tl_o.d_valid)
 571:   `ASSERT_KNOWN(TlOAReadyKnown, tl_o.a_ready)
 572: 
 573:   // Alert outputs
 574:   `ASSERT_KNOWN(AlertTxOKnown, alert_tx_o)
 575: 
 576: `endif // SYNTHESIS
 577: `endif // VERILATOR
 578: 
 579: endmodule
 580: