diff --git a/rtl/ibex_compressed_decoder.sv b/rtl/ibex_compressed_decoder.sv index 442b5791..12a487fe 100644 --- a/rtl/ibex_compressed_decoder.sv +++ b/rtl/ibex_compressed_decoder.sv @@ -284,17 +284,17 @@ module ibex_compressed_decoder ( // Selectors must be known/valid. `ASSERT(IbexInstrLSBsKnown, valid_i |-> - !$isunknown(instr_i[1:0]), clk_i, !rst_ni) + !$isunknown(instr_i[1:0])) `ASSERT(IbexC0Known1, (valid_i && (instr_i[1:0] == 2'b00)) |-> - !$isunknown(instr_i[15:13]), clk_i, !rst_ni) + !$isunknown(instr_i[15:13])) `ASSERT(IbexC1Known1, (valid_i && (instr_i[1:0] == 2'b01)) |-> - !$isunknown(instr_i[15:13]), clk_i, !rst_ni) + !$isunknown(instr_i[15:13])) `ASSERT(IbexC1Known2, (valid_i && (instr_i[1:0] == 2'b01) && (instr_i[15:13] == 3'b100)) |-> - !$isunknown(instr_i[11:10]), clk_i, !rst_ni) + !$isunknown(instr_i[11:10])) `ASSERT(IbexC1Known3, (valid_i && (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) + !$isunknown({instr_i[12], instr_i[6:5]})) `ASSERT(IbexC2Known1, (valid_i && (instr_i[1:0] == 2'b10)) |-> - !$isunknown(instr_i[15:13]), clk_i, !rst_ni) + !$isunknown(instr_i[15:13])) endmodule diff --git a/rtl/ibex_controller.sv b/rtl/ibex_controller.sv index aee4f55b..893d835d 100644 --- a/rtl/ibex_controller.sv +++ b/rtl/ibex_controller.sv @@ -660,7 +660,6 @@ module ibex_controller ( // 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) + IRQ_TAKEN, DBG_TAKEN_IF, DBG_TAKEN_ID}) endmodule diff --git a/rtl/ibex_cs_registers.sv b/rtl/ibex_cs_registers.sv index 67ab0013..8ce5e664 100644 --- a/rtl/ibex_cs_registers.sv +++ b/rtl/ibex_cs_registers.sv @@ -1025,7 +1025,7 @@ module ibex_cs_registers #( CSR_OP_WRITE, CSR_OP_SET, CSR_OP_CLEAR - }, clk_i, !rst_ni) - `ASSERT_KNOWN(IbexCsrWdataIntKnown, csr_wdata_int, clk_i, !rst_ni) + }) + `ASSERT_KNOWN(IbexCsrWdataIntKnown, csr_wdata_int) endmodule diff --git a/rtl/ibex_decoder.sv b/rtl/ibex_decoder.sv index ae3cf86e..40a5b7b5 100644 --- a/rtl/ibex_decoder.sv +++ b/rtl/ibex_decoder.sv @@ -809,5 +809,5 @@ module ibex_decoder #( // Selectors must be known/valid. `ASSERT(IbexRegImmAluOpKnown, (opcode == OPCODE_OP_IMM) |-> - !$isunknown(instr[14:12]), clk_i, !rst_ni) + !$isunknown(instr[14:12])) endmodule // controller diff --git a/rtl/ibex_fetch_fifo.sv b/rtl/ibex_fetch_fifo.sv index 1839d599..2f15c7e2 100644 --- a/rtl/ibex_fetch_fifo.sv +++ b/rtl/ibex_fetch_fifo.sv @@ -225,10 +225,10 @@ module ibex_fetch_fifo #( // Must not push and pop simultaneously when FIFO full. `ASSERT(IbexFetchFifoPushPopFull, - (in_valid_i && pop_fifo) |-> (!valid_q[DEPTH-1] || clear_i), clk_i, !rst_ni) + (in_valid_i && pop_fifo) |-> (!valid_q[DEPTH-1] || clear_i)) // Must not push to FIFO when full. `ASSERT(IbexFetchFifoPushFull, - (in_valid_i) |-> (!valid_q[DEPTH-1] || clear_i), clk_i, !rst_ni) + (in_valid_i) |-> (!valid_q[DEPTH-1] || clear_i)) endmodule diff --git a/rtl/ibex_id_stage.sv b/rtl/ibex_id_stage.sv index 56c8c5aa..99d1b149 100644 --- a/rtl/ibex_id_stage.sv +++ b/rtl/ibex_id_stage.sv @@ -659,37 +659,33 @@ module ibex_id_stage #( IMM_B_U, IMM_B_J, IMM_B_INCR_PC, - IMM_B_INCR_ADDR - }, clk_i, !rst_ni) + IMM_B_INCR_ADDR}) `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) + RF_WD_CSR}) + `ASSERT_KNOWN(IbexWbStateKnown, id_wb_fsm_cs) // Branch decision must be valid when jumping. - `ASSERT(IbexBranchDecisionValid, branch_in_dec |-> !$isunknown(branch_decision_i), clk_i, !rst_ni) + `ASSERT(IbexBranchDecisionValid, branch_in_dec |-> !$isunknown(branch_decision_i)) // Instruction delivered to ID stage can not contain X. `ASSERT(IbexIdInstrKnown, - (instr_valid_i && !(illegal_c_insn_i || instr_fetch_err_i)) |-> !$isunknown(instr_rdata_i), - clk_i, !rst_ni) + (instr_valid_i && !(illegal_c_insn_i || instr_fetch_err_i)) |-> !$isunknown(instr_rdata_i)) // Instruction delivered to ID stage can not contain X. `ASSERT(IbexIdInstrALUKnown, - (instr_valid_i && !(illegal_c_insn_i || instr_fetch_err_i)) |-> !$isunknown(instr_rdata_alu_i), - clk_i, !rst_ni) + (instr_valid_i && !(illegal_c_insn_i || instr_fetch_err_i)) |-> !$isunknown(instr_rdata_alu_i)) // Multicycle enable signals must be unique. `ASSERT(IbexMulticycleEnableUnique, - $onehot0({data_req_dec, multdiv_en_dec, branch_in_dec, jump_in_dec}), clk_i, !rst_ni) + $onehot0({data_req_dec, multdiv_en_dec, branch_in_dec, jump_in_dec})) // Duplicated instruction flops must match `ASSERT(IbexDuplicateInstrMatch, instr_valid_i |-> instr_rdata_i == instr_rdata_alu_i, clk_i, !rst_ni); `ifdef CHECK_MISALIGNED - `ASSERT(IbexMisalignedMemoryAccess, !lsu_addr_incr_req_i, clk_i, !rst_ni) + `ASSERT(IbexMisalignedMemoryAccess, !lsu_addr_incr_req_i) `endif endmodule diff --git a/rtl/ibex_if_stage.sv b/rtl/ibex_if_stage.sv index 1f9b9251..bda2f82f 100644 --- a/rtl/ibex_if_stage.sv +++ b/rtl/ibex_if_stage.sv @@ -268,25 +268,24 @@ module ibex_if_stage #( //////////////// // Selectors must be known/valid. - `ASSERT_KNOWN(IbexExcPcMuxKnown, exc_pc_mux_i, clk_i, !rst_ni) + `ASSERT_KNOWN(IbexExcPcMuxKnown, exc_pc_mux_i) `ASSERT(IbexPcMuxValid, pc_mux_i inside { PC_BOOT, PC_JUMP, PC_EXC, PC_ERET, - PC_DRET - }, clk_i, !rst_ni) + PC_DRET}) // Boot address must be aligned to 256 bytes. - `ASSERT(IbexBootAddrUnaligned, boot_addr_i[7:0] == 8'h00, clk_i, !rst_ni) + `ASSERT(IbexBootAddrUnaligned, boot_addr_i[7:0] == 8'h00) // Errors must only be sent together with rvalid. - `ASSERT(IbexInstrErrWithoutRvalid, instr_err_i |-> instr_rvalid_i, clk_i, !rst_ni) + `ASSERT(IbexInstrErrWithoutRvalid, instr_err_i |-> instr_rvalid_i) // Address must not contain X when request is sent. - `ASSERT(IbexInstrAddrUnknown, instr_req_o |-> !$isunknown(instr_addr_o), clk_i, !rst_ni) + `ASSERT(IbexInstrAddrUnknown, instr_req_o |-> !$isunknown(instr_addr_o)) // Address must be word aligned when request is sent. - `ASSERT(IbexInstrAddrUnaligned, instr_req_o |-> (instr_addr_o[1:0] == 2'b00), clk_i, !rst_ni) + `ASSERT(IbexInstrAddrUnaligned, instr_req_o |-> (instr_addr_o[1:0] == 2'b00)) endmodule diff --git a/rtl/ibex_load_store_unit.sv b/rtl/ibex_load_store_unit.sv index e9fd74bc..5363888d 100644 --- a/rtl/ibex_load_store_unit.sv +++ b/rtl/ibex_load_store_unit.sv @@ -486,29 +486,27 @@ module ibex_load_store_unit ( //////////////// // 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_KNOWN(IbexDataTypeKnown, data_type_ex_i) + `ASSERT_KNOWN(IbexDataOffsetKnown, data_offset) + `ASSERT_KNOWN(IbexRDataOffsetQKnown, rdata_offset_q) + `ASSERT_KNOWN(IbexDataTypeQKnown, data_type_q) `ASSERT(IbexLsuStateValid, ls_fsm_cs inside { IDLE, WAIT_GNT_MIS, WAIT_RVALID_MIS, WAIT_GNT, WAIT_RVALID, - WAIT_RVALID_DONE - }, clk_i, !rst_ni) + WAIT_RVALID_DONE}) // There must not be an rvalid unless the FSM is handlling it. `ASSERT(IbexRvalidNotHandled, data_rvalid_i |-> ( (ls_fsm_cs == WAIT_RVALID) || (ls_fsm_cs == WAIT_RVALID_MIS) || - (ls_fsm_cs == WAIT_RVALID_DONE) - ), clk_i, !rst_ni) + (ls_fsm_cs == WAIT_RVALID_DONE))) // Errors must only be sent together with rvalid. - `ASSERT(IbexDataErrWithoutRvalid, data_err_i |-> data_rvalid_i, clk_i, !rst_ni) + `ASSERT(IbexDataErrWithoutRvalid, data_err_i |-> data_rvalid_i) // Address must not contain X when request is sent. - `ASSERT(IbexDataAddrUnknown, data_req_o |-> !$isunknown(data_addr_o), clk_i, !rst_ni) + `ASSERT(IbexDataAddrUnknown, data_req_o |-> !$isunknown(data_addr_o)) // Address must be word aligned when request is sent. - `ASSERT(IbexDataAddrUnaligned, data_req_o |-> (data_addr_o[1:0] == 2'b00), clk_i, !rst_ni) + `ASSERT(IbexDataAddrUnaligned, data_req_o |-> (data_addr_o[1:0] == 2'b00)) endmodule diff --git a/rtl/ibex_multdiv_fast.sv b/rtl/ibex_multdiv_fast.sv index 5fbbf09f..e4adbf5a 100644 --- a/rtl/ibex_multdiv_fast.sv +++ b/rtl/ibex_multdiv_fast.sv @@ -328,8 +328,7 @@ module ibex_multdiv_fast ( // 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) + MD_IDLE, MD_ABS_A, MD_ABS_B, MD_COMP, MD_LAST, MD_CHANGE_SIGN, MD_FINISH}) + `ASSERT_KNOWN(IbexMultStateKnown, mult_state_q) endmodule // ibex_mult diff --git a/shared/rtl/prim_assert.sv b/shared/rtl/prim_assert.sv index 588a4321..f569292c 100644 --- a/shared/rtl/prim_assert.sv +++ b/shared/rtl/prim_assert.sv @@ -47,6 +47,10 @@ // Simple assertion and cover macros // /////////////////////////////////////// +// Default clk and reset signals used by assertion macros below. +`define ASSERT_DEFAULT_CLK clk_i +`define ASSERT_DEFAULT_RST !rst_ni + // Immediate assertion // Note that immediate assertions are sensitive to simulation glitches. `define ASSERT_I(__name, __prop) \ @@ -75,10 +79,10 @@ // Assert a concurrent property directly. // It can be called as a module (or interface) body item. -`define ASSERT(__name, __prop, __clk, __rst) \ -`ifdef INC_ASSERT \ - __name: assert property (@(posedge __clk) disable iff (__rst !== '0) (__prop)) \ - else `ASSERT_RPT(`PRIM_STRINGIFY(__name), `PRIM_STRINGIFY(__prop)) \ +`define ASSERT(__name, __prop, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \ +`ifdef INC_ASSERT \ + __name: assert property (@(posedge __clk) disable iff (__rst !== '0) (__prop)) \ + else `ASSERT_RPT(`PRIM_STRINGIFY(__name), `PRIM_STRINGIFY(__prop)) \ `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 @@ -86,23 +90,23 @@ // assertion. // Assert a concurrent property NEVER happens -`define ASSERT_NEVER(__name, __prop, __clk, __rst) \ -`ifdef INC_ASSERT \ - __name: assert property (@(posedge __clk) disable iff (__rst !== '0) not (__prop)) \ - else `ASSERT_RPT(`PRIM_STRINGIFY(__name), `PRIM_STRINGIFY(__prop)) \ +`define ASSERT_NEVER(__name, __prop, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \ +`ifdef INC_ASSERT \ + __name: assert property (@(posedge __clk) disable iff (__rst !== '0) not (__prop)) \ + else `ASSERT_RPT(`PRIM_STRINGIFY(__name), `PRIM_STRINGIFY(__prop)) \ `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) \ -`ifdef INC_ASSERT \ - `ASSERT(__name, !$isunknown(__sig), __clk, __rst) \ +`define ASSERT_KNOWN(__name, __sig, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \ +`ifdef INC_ASSERT \ + `ASSERT(__name, !$isunknown(__sig), __clk, __rst) \ `endif // Cover a concurrent property -`define COVER(__name, __prop, __clk, __rst) \ -`ifdef INC_ASSERT \ - __name: cover property (@(posedge __clk) disable iff (__rst !== '0) (__prop)); \ +`define COVER(__name, __prop, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \ +`ifdef INC_ASSERT \ + __name: cover property (@(posedge __clk) disable iff (__rst !== '0) (__prop)); \ `endif ////////////////////////////// @@ -110,24 +114,24 @@ ////////////////////////////// // Assert that signal is an active-high pulse with pulse length of 1 clock cycle -`define ASSERT_PULSE(__name, __sig, __clk, __rst) \ -`ifdef INC_ASSERT \ - `ASSERT(__name, $rose(__sig) |=> !(__sig), __clk, __rst) \ +`define ASSERT_PULSE(__name, __sig, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \ +`ifdef INC_ASSERT \ + `ASSERT(__name, $rose(__sig) |=> !(__sig), __clk, __rst) \ `endif // Assert that valid is known after reset and data is known when valid == 1 -`define ASSERT_VALID_DATA(__name, __valid, __dat, __clk, __rst) \ -`ifdef INC_ASSERT \ - `ASSERT_KNOWN(__name``KnownValid, __valid, __clk, __rst) \ - `ASSERT_NEVER(__name``KnownData, (__valid) && $isunknown(__dat), __clk, __rst) \ +`define ASSERT_VALID_DATA(__name, __valid, __dat, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \ +`ifdef INC_ASSERT \ + `ASSERT_KNOWN(__name``KnownValid, __valid, __clk, __rst) \ + `ASSERT_NEVER(__name``KnownData, (__valid) && $isunknown(__dat), __clk, __rst) \ `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) \ -`ifdef INC_ASSERT \ - `ASSERT_KNOWN(__name``KnownValid, __valid, __clk, __rst) \ - `ASSERT_KNOWN(__name``KnownReady, __ready, __clk, __rst) \ - `ASSERT_NEVER(__name``KnownData, (__valid) && $isunknown(__dat), __clk, __rst) \ +`define ASSERT_VALID_READY_DATA(__name, __valid, __ready, __dat, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \ +`ifdef INC_ASSERT \ + `ASSERT_KNOWN(__name``KnownValid, __valid, __clk, __rst) \ + `ASSERT_KNOWN(__name``KnownReady, __ready, __clk, __rst) \ + `ASSERT_NEVER(__name``KnownData, (__valid) && $isunknown(__dat), __clk, __rst) \ `endif /////////////////////// @@ -135,10 +139,10 @@ /////////////////////// // Assume a concurrent property -`define ASSUME(__name, __prop, __clk, __rst) \ -`ifdef INC_ASSERT \ - __name: assume property (@(posedge __clk) disable iff (__rst !== '0) (__prop)) \ - else begin `ASSERT_RPT(`PRIM_STRINGIFY(__name), `PRIM_STRINGIFY(__prop)) end \ +`define ASSUME(__name, __prop, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \ +`ifdef INC_ASSERT \ + __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 @@ -157,9 +161,9 @@ // 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) \ +`define ASSUME_FPV(__name, __prop, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \ +`ifdef FPV_ON \ + `ASSUME(__name, __prop, __clk, __rst) \ `endif // ASSUME_I_FPV @@ -171,9 +175,9 @@ // COVER_FPV // Cover a concurrent property during formal verification -`define COVER_FPV(__name, __prop, __clk, __rst) \ -`ifdef FPV_ON \ - `COVER(__name, __prop, __clk, __rst) \ +`define COVER_FPV(__name, __prop, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \ +`ifdef FPV_ON \ + `COVER(__name, __prop, __clk, __rst) \ `endif `endif // PRIM_ASSERT_SV