[rtl] Remove X assignments, add SVAs for selector signals

This commit replaces all X assignments in the RTL with defined
values. In addition, SystemVerilog Assertions are added to catch
invalid signal values in simulation. A new file containing the
corresponding assertion macros is added as well.

Signed-off-by: Pirmin Vogel <vogelpi@lowrisc.org>

dv/uvm/ibex_dv.f

@@ -10,6 +10,7 @@ ${PRJ_DIR}/ibex/shared/rtl/prim_clock_gating.sv
 
 // ibex CORE RTL files
 +incdir+${PRJ_DIR}/ibex/rtl
+${PRJ_DIR}/ibex/shared/rtl/prim_assert.sv
 ${PRJ_DIR}/ibex/rtl/ibex_pkg.sv
 ${PRJ_DIR}/ibex/rtl/ibex_tracer_pkg.sv
 ${PRJ_DIR}/ibex/rtl/ibex_tracer.sv

ibex_core.core

@@ -6,6 +6,8 @@ name: "lowrisc:ibex:ibex_core:0.1"
 description: "CPU core with 2 stage pipeline implementing the RV32IMC_Zicsr ISA"
 filesets:
   files_rtl:
+    depend:
+      - lowrisc:prim:assert
     files:
       - rtl/ibex_pkg.sv
       - rtl/ibex_alu.sv

ibex_tracer.core

@@ -6,6 +6,8 @@ name: "lowrisc:ibex:ibex_tracer:0.1"
 description: "Tracer for use with Ibex using the RVFI interface"
 filesets:
   files_rtl:
+    depend:
+      - lowrisc:prim:assert
     files:
       - rtl/ibex_tracer_pkg.sv
       - rtl/ibex_tracer.sv

lint/verilator_waiver.vlt

@@ -49,10 +49,14 @@ lint_off -msg UNUSED -file "*/rtl/ibex_register_file_ff.sv" -lines 21
 // Signal is not used: clk_i
 // leaving clk and reset connected in-case we want to add assertions
 lint_off -msg UNUSED -file "*/rtl/ibex_pmp.sv" -lines 15
+lint_off -msg UNUSED -file "*/rtl/ibex_compressed_decoder.sv" -lines 14
+lint_off -msg UNUSED -file "*/rtl/ibex_decoder.sv" -lines 21
 
 // Signal is not used: rst_ni
 // leaving clk and reset connected in-case we want to add assertions
 lint_off -msg UNUSED -file "*/rtl/ibex_pmp.sv" -lines 16
+lint_off -msg UNUSED -file "*/rtl/ibex_compressed_decoder.sv" -lines 15
+lint_off -msg UNUSED -file "*/rtl/ibex_decoder.sv" -lines 22
 
 // Signal unoptimizable: Feedback to clock or circular logic:
 // ibex_core.cs_registers_i.mie_q

rtl/ibex_compressed_decoder.sv

@@ -7,9 +7,12 @@
  * Compressed instruction decoder
  *
  * Decodes RISC-V compressed instructions into their RV32 equivalent.
- * This module is fully combinatorial.
+ * This module is fully combinatorial, clock and reset are used for
+ * assertions only.
  */
 module ibex_compressed_decoder (
+    input  logic        clk_i,
+    input  logic        rst_ni,
     input  logic [31:0] instr_i,
     output logic [31:0] instr_o,
     output logic        is_compressed_o,
@@ -23,7 +26,8 @@ module ibex_compressed_decoder (
 
   always_comb begin
     illegal_instr_o = 1'b0;
-    instr_o         = 'X;
+    // Default instruction is NOP (ADDI x0, x0, 0)
+    instr_o         = {12'd0, 5'd0, 3'd0, 5'd0, OPCODE_OP_IMM};
 
     unique case (instr_i[1:0])
       // C0
@@ -152,13 +156,13 @@ module ibex_compressed_decoder (
                   end
 
                   default: begin
-                    illegal_instr_o = 1'bX;
+                    illegal_instr_o = 1'b1;
                   end
                 endcase
               end
 
               default: begin
-                illegal_instr_o = 1'bX;
+                illegal_instr_o = 1'b1;
               end
             endcase
           end
@@ -172,7 +176,7 @@ module ibex_compressed_decoder (
           end
 
           default: begin
-            illegal_instr_o = 1'bX;
+            illegal_instr_o = 1'b1;
           end
         endcase
       end
@@ -240,7 +244,7 @@ module ibex_compressed_decoder (
           end
 
           default: begin
-            illegal_instr_o = 1'bX;
+            illegal_instr_o = 1'b1;
           end
         endcase
       end
@@ -254,4 +258,18 @@ module ibex_compressed_decoder (
 
   assign is_compressed_o = (instr_i[1:0] != 2'b11);
 
+  ////////////////
+  // Assertions //
+  ////////////////
+
+  // Selectors must be known/valid.
+  `ASSERT(IbexC1Known1, (instr_i[1:0] == 2'b01) |-> !$isunknown(instr_i[15:13]), clk_i, !rst_ni)
+  `ASSERT(IbexC1Known2,
+      ((instr_i[1:0] == 2'b01) && (instr_i[15:13] == 3'b100)) |->
+      !$isunknown(instr_i[11:10]), clk_i, !rst_ni)
+  `ASSERT(IbexC1Known3,
+      ((instr_i[1:0] == 2'b01) && (instr_i[15:13] == 3'b100) && (instr_i[11:10] == 2'b11)) |->
+      !$isunknown({instr_i[12], instr_i[6:5]}), clk_i, !rst_ni)
+  `ASSERT(IbexC2Known1, (instr_i[1:0] == 2'b10) |-> !$isunknown(instr_i[15:13]), clk_i, !rst_ni)
+
 endmodule

rtl/ibex_controller.sv

@@ -585,7 +585,7 @@ module ibex_controller (
 
       default: begin
         instr_req_o = 1'b0;
-        ctrl_fsm_ns = ctrl_fsm_e'(1'bX);
+        ctrl_fsm_ns = RESET;
       end
     endcase
   end
@@ -636,4 +636,14 @@ module ibex_controller (
     end
   end
 
+  ////////////////
+  // Assertions //
+  ////////////////
+
+  // Selectors must be known/valid.
+  `ASSERT(IbexCtrlStateValid, ctrl_fsm_cs inside {
+      RESET, BOOT_SET, WAIT_SLEEP, SLEEP, FIRST_FETCH, DECODE, FLUSH,
+      IRQ_TAKEN, DBG_TAKEN_IF, DBG_TAKEN_ID
+      }, clk_i, !rst_ni)
+
 endmodule

rtl/ibex_cs_registers.sv

@@ -613,8 +613,8 @@ module ibex_cs_registers #(
         csr_wreq      = 1'b0;
       end
       default: begin
-        csr_wdata_int = 'X;
+        csr_wdata_int = csr_wdata_i;
-        csr_wreq      = 1'bX;
+        csr_wreq      = 1'b0;
       end
     endcase
   end
@@ -777,7 +777,7 @@ module ibex_cs_registers #(
           2'b10   : pmp_cfg_wdata[i].mode = (PMPGranularity == 0) ? PMP_MODE_NA4:
                                                                     PMP_MODE_OFF;
           2'b11   : pmp_cfg_wdata[i].mode = PMP_MODE_NAPOT;
-          default : pmp_cfg_wdata[i].mode = pmp_cfg_mode_e'('X);
+          default : pmp_cfg_wdata[i].mode = PMP_MODE_OFF;
         endcase
       end
       assign pmp_cfg_wdata[i].exec  = csr_wdata_int[(i%4)*PMP_CFG_W+2];
@@ -1013,4 +1013,17 @@ module ibex_cs_registers #(
     assign trigger_match_o      = 'b0;
   end
 
+  ////////////////
+  // Assertions //
+  ////////////////
+
+  // Selectors must be known/valid.
+  `ASSERT(IbexCsrOpValid, csr_op_i inside {
+      CSR_OP_READ,
+      CSR_OP_WRITE,
+      CSR_OP_SET,
+      CSR_OP_CLEAR
+      }, clk_i, !rst_ni)
+  `ASSERT_KNOWN(IbexCsrWdataIntKnown, csr_wdata_int, clk_i, !rst_ni)
+
 endmodule

rtl/ibex_decoder.sv

@@ -10,11 +10,17 @@
 
 /**
  * Instruction decoder
+ *
+ * This module is fully combinatorial, clock and reset are used for
+ * assertions only.
  */
 module ibex_decoder #(
     parameter bit RV32E = 0,
     parameter bit RV32M = 1
 ) (
+    input  logic                 clk_i,
+    input  logic                 rst_ni,
+
     // to/from controller
     output logic                 illegal_insn_o,        // illegal instr encountered
     output logic                 ebrk_insn_o,           // trap instr encountered
@@ -395,7 +401,7 @@ module ibex_decoder #(
           end
 
           default: begin
-            alu_operator_o = alu_op_e'({$bits(alu_op_e){1'bX}});
+            alu_operator_o = ALU_SLTU;
           end
         endcase
       end
@@ -615,4 +621,12 @@ module ibex_decoder #(
   // do not propgate regfile write enable if non-available registers are accessed in RV32E
   assign regfile_we_o = regfile_we & ~illegal_reg_rv32e;
 
+  ////////////////
+  // Assertions //
+  ////////////////
+
+  // Selectors must be known/valid.
+  `ASSERT(IbexRegImmAluOpKnown, (opcode == OPCODE_OP_IMM) |->
+      !$isunknown(instr[14:12]), clk_i, !rst_ni)
+
 endmodule // controller

rtl/ibex_id_stage.sv

@@ -233,7 +233,7 @@ module ibex_id_stage #(
       OP_A_FWD:    alu_operand_a = lsu_addr_last_i;
       OP_A_CURRPC: alu_operand_a = pc_id_i;
       OP_A_IMM:    alu_operand_a = imm_a;
-      default:     alu_operand_a = 'X;
+      default:     alu_operand_a = pc_id_i;
     endcase
   end
 
@@ -251,7 +251,7 @@ module ibex_id_stage #(
       IMM_B_J:         imm_b = imm_j_type;
       IMM_B_INCR_PC:   imm_b = instr_is_compressed_i ? 32'h2 : 32'h4;
       IMM_B_INCR_ADDR: imm_b = 32'h4;
-      default:         imm_b = 'X;
+      default:         imm_b = 32'h4;
     endcase
   end
 
@@ -273,8 +273,8 @@ module ibex_id_stage #(
       RF_WD_EX:  regfile_wdata = regfile_wdata_ex_i;
       RF_WD_LSU: regfile_wdata = regfile_wdata_lsu_i;
       RF_WD_CSR: regfile_wdata = csr_rdata_i;
-      default:   regfile_wdata = 'X;
+      default:   regfile_wdata = regfile_wdata_ex_i;
-    endcase;
+    endcase
   end
 
   ///////////////////
@@ -317,6 +317,9 @@ module ibex_id_stage #(
       .RV32E ( RV32E ),
       .RV32M ( RV32M )
   ) decoder_i (
+      .clk_i                           ( clk_i                ),
+      .rst_ni                          ( rst_ni               ),
+
       // controller
       .illegal_insn_o                  ( illegal_insn_dec     ),
       .ebrk_insn_o                     ( ebrk_insn            ),
@@ -600,7 +603,7 @@ module ibex_id_stage #(
       end
 
       default: begin
-        id_wb_fsm_ns = id_fsm_e'(1'bX);
+        id_wb_fsm_ns = IDLE;
       end
     endcase
   end
@@ -611,6 +614,24 @@ module ibex_id_stage #(
   // Assertions //
   ////////////////
 
+  // Selectors must be known/valid.
+  `ASSERT_KNOWN(IbexAluOpMuxSelKnown, alu_op_a_mux_sel, clk_i, !rst_ni)
+  `ASSERT(IbexImmBMuxSelValid, imm_b_mux_sel inside {
+      IMM_B_I,
+      IMM_B_S,
+      IMM_B_B,
+      IMM_B_U,
+      IMM_B_J,
+      IMM_B_INCR_PC,
+      IMM_B_INCR_ADDR
+      }, clk_i, !rst_ni)
+  `ASSERT(IbexRegfileWdataSelValid, regfile_wdata_sel inside {
+      RF_WD_LSU,
+      RF_WD_EX,
+      RF_WD_CSR
+      }, clk_i, !rst_ni)
+  `ASSERT_KNOWN(IbexWbStateKnown, id_wb_fsm_cs, clk_i, !rst_ni)
+
 `ifndef VERILATOR
   // branch decision must be valid when jumping
   assert property (@(posedge clk_i) disable iff (!rst_ni)

rtl/ibex_if_stage.sv

@@ -109,7 +109,7 @@ module ibex_if_stage #(
       EXC_PC_IRQ:     exc_pc = { csr_mtvec_i[31:8], 1'b0, irq_id[4:0], 2'b00 };
       EXC_PC_DBD:     exc_pc = DmHaltAddr;
       EXC_PC_DBG_EXC: exc_pc = DmExceptionAddr;
-      default:        exc_pc = 'X;
+      default:        exc_pc = { csr_mtvec_i[31:8], 8'h00                    };
     endcase
   end
 
@@ -121,7 +121,7 @@ module ibex_if_stage #(
       PC_EXC:  fetch_addr_n = exc_pc;                       // set PC to exception handler
       PC_ERET: fetch_addr_n = csr_mepc_i;                   // restore PC when returning from EXC
       PC_DRET: fetch_addr_n = csr_depc_i;
-      default: fetch_addr_n = 'X;
+      default: fetch_addr_n = { boot_addr_i[31:8], 8'h80 };
     endcase
   end
 
@@ -217,6 +217,8 @@ module ibex_if_stage #(
   logic        instr_is_compressed_int;
 
   ibex_compressed_decoder compressed_decoder_i (
+      .clk_i           ( clk_i                   ),
+      .rst_ni          ( rst_ni                  ),
       .instr_i         ( fetch_rdata             ),
       .instr_o         ( instr_decompressed      ),
       .is_compressed_o ( instr_is_compressed_int ),
@@ -255,6 +257,17 @@ module ibex_if_stage #(
   ////////////////
   // Assertions //
   ////////////////
+
+  // Selectors must be known/valid.
+  `ASSERT_KNOWN(IbexExcPcMuxKnown, exc_pc_mux_i, clk_i, !rst_ni)
+  `ASSERT(IbexPcMuxValid, pc_mux_i inside {
+      PC_BOOT,
+      PC_JUMP,
+      PC_EXC,
+      PC_ERET,
+      PC_DRET
+      }, clk_i, !rst_ni)
+
 `ifndef VERILATOR
   // boot address must be aligned to 256 bytes
   assert property (@(posedge clk_i) disable iff (!rst_ni)

rtl/ibex_load_store_unit.sv

@@ -105,7 +105,7 @@ module ibex_load_store_unit (
             2'b01:   data_be = 4'b1110;
             2'b10:   data_be = 4'b1100;
             2'b11:   data_be = 4'b1000;
-            default: data_be = 'X;
+            default: data_be = 4'b1111;
           endcase // case (data_offset)
         end else begin // second part of misaligned transaction
           unique case (data_offset)
@@ -113,7 +113,7 @@ module ibex_load_store_unit (
             2'b01:   data_be = 4'b0001;
             2'b10:   data_be = 4'b0011;
             2'b11:   data_be = 4'b0111;
-            default: data_be = 'X;
+            default: data_be = 4'b1111;
           endcase // case (data_offset)
         end
       end
@@ -125,7 +125,7 @@ module ibex_load_store_unit (
             2'b01:   data_be = 4'b0110;
             2'b10:   data_be = 4'b1100;
             2'b11:   data_be = 4'b1000;
-            default: data_be = 'X;
+            default: data_be = 4'b1111;
           endcase // case (data_offset)
         end else begin // second part of misaligned transaction
           data_be = 4'b0001;
@@ -139,11 +139,11 @@ module ibex_load_store_unit (
           2'b01:   data_be = 4'b0010;
           2'b10:   data_be = 4'b0100;
           2'b11:   data_be = 4'b1000;
-          default: data_be = 'X;
+          default: data_be = 4'b1111;
         endcase // case (data_offset)
       end
 
-      default:     data_be = 'X;
+      default:     data_be = 4'b1111;
     endcase // case (data_type_ex_i)
   end
 
@@ -159,7 +159,7 @@ module ibex_load_store_unit (
       2'b01:   data_wdata = {data_wdata_ex_i[23:0], data_wdata_ex_i[31:24]};
       2'b10:   data_wdata = {data_wdata_ex_i[15:0], data_wdata_ex_i[31:16]};
       2'b11:   data_wdata = {data_wdata_ex_i[ 7:0], data_wdata_ex_i[31: 8]};
-      default: data_wdata = 'X;
+      default: data_wdata =  data_wdata_ex_i[31:0];
     endcase // case (data_offset)
   end
 
@@ -208,7 +208,7 @@ module ibex_load_store_unit (
       2'b01:   rdata_w_ext = {data_rdata_i[ 7:0], rdata_q[31:8]};
       2'b10:   rdata_w_ext = {data_rdata_i[15:0], rdata_q[31:16]};
       2'b11:   rdata_w_ext = {data_rdata_i[23:0], rdata_q[31:24]};
-      default: rdata_w_ext = 'X;
+      default: rdata_w_ext =  data_rdata_i[31:0];
     endcase
   end
 
@@ -251,7 +251,7 @@ module ibex_load_store_unit (
         end
       end
 
-      default: rdata_h_ext = 'X;
+      default: rdata_h_ext = {16'h0000, data_rdata_i[15:0]};
     endcase // case (rdata_offset_q)
   end
 
@@ -290,7 +290,7 @@ module ibex_load_store_unit (
         end
       end
 
-      default: rdata_b_ext = 'X;
+      default: rdata_b_ext = {24'h00_0000, data_rdata_i[7:0]};
     endcase // case (rdata_offset_q)
   end
 
@@ -300,8 +300,8 @@ module ibex_load_store_unit (
       2'b00:       data_rdata_ext = rdata_w_ext;
       2'b01:       data_rdata_ext = rdata_h_ext;
       2'b10,2'b11: data_rdata_ext = rdata_b_ext;
-      default:     data_rdata_ext = 'X;
+      default:     data_rdata_ext = rdata_w_ext;
-    endcase //~case(rdata_type_q)
+    endcase // case (data_type_q)
   end
 
   /////////////
@@ -433,7 +433,7 @@ module ibex_load_store_unit (
       end
 
       default: begin
-        ls_fsm_ns = ls_fsm_e'(1'bX);
+        ls_fsm_ns = IDLE;
       end
     endcase
   end
@@ -482,6 +482,16 @@ module ibex_load_store_unit (
   // Assertions //
   ////////////////
 
+  // Selectors must be known/valid.
+  `ASSERT_KNOWN(IbexDataTypeKnown, data_type_ex_i, clk_i, !rst_ni)
+  `ASSERT_KNOWN(IbexDataOffsetKnown, data_offset, clk_i, !rst_ni)
+  `ASSERT_KNOWN(IbexRDataOffsetQKnown, rdata_offset_q, clk_i, !rst_ni)
+  `ASSERT_KNOWN(IbexDataTypeQKnown, data_type_q, clk_i, !rst_ni)
+  `ASSERT(IbexLsuStateValid, ls_fsm_cs inside {
+      IDLE, WAIT_GNT_MIS, WAIT_RVALID_MIS, WAIT_GNT, WAIT_RVALID,
+      WAIT_RVALID_DONE
+      }, clk_i, !rst_ni)
+
 `ifndef VERILATOR
   // there must not be an rvalid unless the FSM is handlling it
   assert property (@(posedge clk_i) disable iff (!rst_ni)

rtl/ibex_multdiv_fast.sv

@@ -238,7 +238,7 @@ module ibex_multdiv_fast (
       end
 
       default: begin
-        md_state_n = md_fsm_e'(1'bX);
+        md_state_n = MD_IDLE;
       end
     endcase // md_state_q
   end
@@ -318,9 +318,15 @@ module ibex_multdiv_fast (
         mult_valid   = 1'b1;
       end
       default: begin
-        mult_state_n = mult_fsm_e'(1'bX);
+        mult_state_n = ALBL;
       end
     endcase // mult_state_q
   end
 
+  // States must be knwon/valid.
+  `ASSERT(IbexMultDivStateValid, md_state_q inside {
+      MD_IDLE, MD_ABS_A, MD_ABS_B, MD_COMP, MD_LAST, MD_CHANGE_SIGN, MD_FINISH
+      }, clk_i, !rst_ni)
+  `ASSERT_KNOWN(IbexMultStateKnown, mult_state_q, clk_i, !rst_ni)
+
 endmodule // ibex_mult

rtl/ibex_multdiv_slow.sv

@@ -272,7 +272,7 @@ module ibex_multdiv_slow (
         end
 
         default: begin
-          md_state_d = md_fsm_e'(1'bX);
+          md_state_d = MD_IDLE;
         end
         endcase // md_state_q
       end
@@ -283,4 +283,9 @@ module ibex_multdiv_slow (
                    (operator_i == MD_OP_MULL |
                     operator_i == MD_OP_MULH));
 
+  // State must be valid.
+  `ASSERT(IbexMultDivStateValid, md_state_q inside {
+      MD_IDLE, MD_ABS_A, MD_ABS_B, MD_COMP, MD_LAST, MD_CHANGE_SIGN, MD_FINISH
+      }, clk_i, !rst_ni)
+
 endmodule // ibex_mult

shared/prim_assert.core

@@ -0,0 +1,17 @@
+CAPI=2:
+# Copyright lowRISC contributors.
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+
+name: "lowrisc:prim:assert:0.1"
+description: "Assertion primitives"
+filesets:
+  files_rtl:
+    files:
+      - rtl/prim_assert.sv
+    file_type: systemVerilogSource
+
+targets:
+  default:
+    filesets:
+      - files_rtl

shared/rtl/prim_assert.sv

@@ -0,0 +1,197 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+// Macros and helper code for using assertions.
+//  - Provides default clk and rst options to simplify code
+//  - Provides boiler plate template for common assertions
+
+// TODO:
+//  - check if ASSERT_FINAL needs an `ifndef SYNTHESIS
+//  - should we add ASSERT_INIT_DISABLE?
+//  - can we remove pragma translate_off and ifndef VERILATOR?
+//  - should we add "pragma coverage off" and "VCS coverage off"?
+
+`ifdef UVM_PKG_SV
+  // report assertion error with UVM if compiled
+  package assert_rpt_pkg;
+    import uvm_pkg::*;
+    `include "uvm_macros.svh"
+    function void assert_rpt(string msg);
+      `uvm_error("ASSERT FAILED", msg)
+    endfunction
+  endpackage
+`endif
+
+
+///////////////////
+// Helper macros //
+///////////////////
+
+
+// Converts an arbitrary block of code into a Verilog string
+`define PRIM_STRINGIFY(__x) `"__x`"
+
+  // ASSERT_RPT is available to change the reporting mechanism when an assert fails
+`define ASSERT_RPT(__name, __msg)                                         \
+`ifdef UVM_PKG_SV                                                         \
+  assert_rpt_pkg::assert_rpt($sformatf("[%m] %s: %s (%s:%0d)",            \
+                             __name, __msg, `__FILE__, `__LINE__));       \
+`else                                                                     \
+  $error("[ASSERT FAILED] [%m] %s: %s", __name, __msg);                   \
+`endif
+
+///////////////////////////////////////
+// Simple assertion and cover macros //
+///////////////////////////////////////
+
+// Immediate assertion
+// Note that immediate assertions are sensitive to simulation glitches.
+`define ASSERT_I(__name, __prop)                                       \
+`ifndef VERILATOR                                                      \
+  //pragma translate_off                                               \
+  __name: assert (__prop)                                              \
+    else `ASSERT_RPT(`PRIM_STRINGIFY(__name), `PRIM_STRINGIFY(__prop)) \
+  //pragma translate_on                                                \
+`endif
+
+// Assertion in initial block. Can be used for things like parameter checking.
+`define ASSERT_INIT(__name, __prop)                                      \
+`ifndef VERILATOR                                                        \
+  //pragma translate_off                                                 \
+  initial                                                                \
+    __name: assert (__prop)                                              \
+      else `ASSERT_RPT(`PRIM_STRINGIFY(__name), `PRIM_STRINGIFY(__prop)) \
+  //pragma translate_on                                                  \
+`endif
+
+// Assertion in final block. Can be used for things like queues being empty
+// at end of sim, all credits returned at end of sim, state machines in idle
+// at end of sim.
+`define ASSERT_FINAL(__name, __prop)                                         \
+`ifndef VERILATOR                                                            \
+  //pragma translate_off                                                     \
+  final                                                                      \
+    __name: assert (__prop || $test$plusargs("disable_assert_final_checks")) \
+      else `ASSERT_RPT(`PRIM_STRINGIFY(__name), `PRIM_STRINGIFY(__prop))     \
+  //pragma translate_on                                                      \
+`endif
+
+// Assert a concurrent property directly.
+// It can be called as a module (or interface) body item.
+`define ASSERT(__name, __prop, __clk, __rst)                                     \
+`ifndef VERILATOR                                                                \
+  //pragma translate_off                                                         \
+  __name: assert property (@(posedge __clk) disable iff (__rst !== '0) (__prop)) \
+    else `ASSERT_RPT(`PRIM_STRINGIFY(__name), `PRIM_STRINGIFY(__prop))           \
+  //pragma translate_on                                                          \
+`endif
+// Note: Above we use (__rst !== '0) in the disable iff statements instead of
+// (__rst == '1).  This properly disables the assertion in cases when reset is X at
+// the beginning of a simulation. For that case, (reset == '1) does not disable the
+// assertion.
+
+// Assert a concurrent property NEVER happens
+`define ASSERT_NEVER(__name, __prop, __clk, __rst)                                   \
+`ifndef VERILATOR                                                                    \
+  //pragma translate_off                                                             \
+  __name: assert property (@(posedge __clk) disable iff (__rst !== '0) not (__prop)) \
+    else `ASSERT_RPT(`PRIM_STRINGIFY(__name), `PRIM_STRINGIFY(__prop))               \
+  //pragma translate_on                                                              \
+`endif
+
+// Assert that signal has a known value (each bit is either '0' or '1') after reset.
+// It can be called as a module (or interface) body item.
+`define ASSERT_KNOWN(__name, __sig, __clk, __rst)   \
+`ifndef VERILATOR                                   \
+  //pragma translate_off                            \
+  `ASSERT(__name, !$isunknown(__sig), __clk, __rst) \
+  //pragma translate_on                             \
+`endif
+
+//  Cover a concurrent property
+`define COVER(__name, __prop, __clk, __rst)                                      \
+`ifndef VERILATOR                                                                \
+  //pragma translate_off                                                         \
+  __name: cover property (@(posedge __clk) disable iff (__rst !== '0) (__prop)); \
+  //pragma translate_on                                                          \
+`endif
+
+//////////////////////////////
+// Complex assertion macros //
+//////////////////////////////
+
+// Assert that signal is an active-high pulse with pulse length of 1 clock cycle
+`define ASSERT_PULSE(__name, __sig, __clk, __rst)          \
+`ifndef VERILATOR                                          \
+  //pragma translate_off                                   \
+  `ASSERT(__name, $rose(__sig) |=> !(__sig), __clk, __rst) \
+  //pragma translate_on                                    \
+`endif
+
+// Assert that valid is known after reset and data is known when valid == 1
+`define ASSERT_VALID_DATA(__name, __valid, __dat, __clk, __rst)                  \
+`ifndef VERILATOR                                                                \
+  //pragma translate_off                                                         \
+  `ASSERT_KNOWN(__name``KnownValid, __valid, __clk, __rst)                       \
+  `ASSERT_NEVER(__name``KnownData, (__valid) && $isunknown(__dat), __clk, __rst) \
+  //pragma translate_on                                                          \
+`endif
+
+// Same as ASSERT_VALID_DATA, but also assert that ready is known after reset
+`define ASSERT_VALID_READY_DATA(__name, __valid, __ready, __dat, __clk, __rst)   \
+`ifndef VERILATOR                                                                \
+  //pragma translate_off                                                         \
+  `ASSERT_KNOWN(__name``KnownValid, __valid, __clk, __rst)                       \
+  `ASSERT_KNOWN(__name``KnownReady, __ready, __clk, __rst)                       \
+  `ASSERT_NEVER(__name``KnownData, (__valid) && $isunknown(__dat), __clk, __rst) \
+  //pragma translate_on                                                          \
+`endif
+
+///////////////////////
+// Assumption macros //
+///////////////////////
+
+// Assume a concurrent property
+`define ASSUME(__name, __prop, __clk, __rst)                                      \
+`ifndef VERILATOR                                                                 \
+  __name: assume property (@(posedge __clk) disable iff (__rst !== '0) (__prop))  \
+     else begin `ASSERT_RPT(`PRIM_STRINGIFY(__name), `PRIM_STRINGIFY(__prop)) end \
+`endif
+
+// Assume an immediate property
+`define ASSUME_I(__name, __prop)                                       \
+`ifndef VERILATOR                                                      \
+  //pragma translate_off                                               \
+  __name: assume (__prop)                                              \
+    else `ASSERT_RPT(`PRIM_STRINGIFY(__name), `PRIM_STRINGIFY(__prop)) \
+  //pragma translate_on                                                \
+`endif
+
+//////////////////////////////////
+// For formal verification only //
+//////////////////////////////////
+
+// Note that the existing set of ASSERT macros specified above shall be used for FPV,
+// thereby ensuring that the assertions are evaluated during DV simulations as well.
+
+// ASSUME_FPV
+// Assume a concurrent property during formal verification only.
+`define ASSUME_FPV(__name, __prop, __clk, __rst) \
+`ifdef FPV_ON                                    \
+   `ASSUME(__name, __prop, __clk, __rst)         \
+`endif
+
+// ASSUME_I_FPV
+// Assume a concurrent property during formal verification only.
+`define ASSUME_I_FPV(__name, __prop)             \
+`ifdef FPV_ON                                    \
+   `ASSUME_I(__name, __prop)                     \
+`endif
+
+// COVER_FPV
+// Cover a concurrent property during formal verification
+`define COVER_FPV(__name, __prop, __clk, __rst)  \
+`ifdef FPV_ON                                    \
+   `COVER(__name, __prop, __clk, __rst)          \
+`endif