diff --git a/rtl/ibex_core.sv b/rtl/ibex_core.sv index 6e1d7fdf..5d3fe04a 100644 --- a/rtl/ibex_core.sv +++ b/rtl/ibex_core.sv @@ -854,6 +854,15 @@ module ibex_core #( .div_wait_i ( perf_div_wait ) ); + // These assertions are in top-level as instr_valid_id required as the enable term + `ASSERT(IbexCsrOpValid, instr_valid_id |-> csr_op inside { + CSR_OP_READ, + CSR_OP_WRITE, + CSR_OP_SET, + CSR_OP_CLEAR + }) + `ASSERT_KNOWN_IF(IbexCsrWdataIntKnown, cs_registers_i.csr_wdata_int, csr_access & instr_valid_id) + if (PMPEnable) begin : g_pmp logic [33:0] pmp_req_addr [PMP_NUM_CHAN]; pmp_req_e pmp_req_type [PMP_NUM_CHAN]; diff --git a/rtl/ibex_cs_registers.sv b/rtl/ibex_cs_registers.sv index 1aa428cb..29024883 100644 --- a/rtl/ibex_cs_registers.sv +++ b/rtl/ibex_cs_registers.sv @@ -1077,13 +1077,6 @@ module ibex_cs_registers #( // Assertions // //////////////// - // Selectors must be known/valid. - `ASSERT(IbexCsrOpValid, csr_op_i inside { - CSR_OP_READ, - CSR_OP_WRITE, - CSR_OP_SET, - CSR_OP_CLEAR - }) - `ASSERT_KNOWN(IbexCsrWdataIntKnown, csr_wdata_int) + `ASSERT(IbexCsrOpEnRequiresAccess, csr_op_en_i |-> csr_access_i) endmodule diff --git a/rtl/ibex_id_stage.sv b/rtl/ibex_id_stage.sv index 2a511a8e..62756cbb 100644 --- a/rtl/ibex_id_stage.sv +++ b/rtl/ibex_id_stage.sv @@ -893,21 +893,21 @@ module ibex_id_stage #( //////////////// // Selectors must be known/valid. - `ASSERT_KNOWN(IbexAluOpMuxSelKnown, alu_op_a_mux_sel, clk_i, !rst_ni) - `ASSERT(IbexAluAOpMuxSelValid, alu_op_a_mux_sel inside { + `ASSERT_KNOWN_IF(IbexAluOpMuxSelKnown, alu_op_a_mux_sel, instr_valid_i) + `ASSERT(IbexAluAOpMuxSelValid, instr_valid_i |-> alu_op_a_mux_sel inside { OP_A_REG_A, OP_A_FWD, OP_A_CURRPC, OP_A_IMM}) if (BranchTargetALU) begin : g_btalu_assertions - `ASSERT(IbexImmBMuxSelValid, imm_b_mux_sel inside { + `ASSERT(IbexImmBMuxSelValid, instr_valid_i |-> imm_b_mux_sel inside { IMM_B_I, IMM_B_S, IMM_B_U, IMM_B_INCR_PC, IMM_B_INCR_ADDR}) end else begin : g_nobtalu_assertions - `ASSERT(IbexImmBMuxSelValid, imm_b_mux_sel inside { + `ASSERT(IbexImmBMuxSelValid, instr_valid_i |-> imm_b_mux_sel inside { IMM_B_I, IMM_B_S, IMM_B_B, @@ -916,31 +916,31 @@ module ibex_id_stage #( IMM_B_INCR_PC, IMM_B_INCR_ADDR}) end - `ASSERT_KNOWN(IbexBTAluAOpMuxSelKnown, bt_a_mux_sel, clk_i, !rst_ni) - `ASSERT(IbexBTAluAOpMuxSelValid, bt_a_mux_sel inside { + `ASSERT_KNOWN_IF(IbexBTAluAOpMuxSelKnown, bt_a_mux_sel, instr_valid_i) + `ASSERT(IbexBTAluAOpMuxSelValid, instr_valid_i |-> bt_a_mux_sel inside { OP_A_REG_A, OP_A_CURRPC}) - `ASSERT_KNOWN(IbexBTAluBOpMuxSelKnown, bt_b_mux_sel, clk_i, !rst_ni) - `ASSERT(IbexBTAluBOpMuxSelValid, bt_b_mux_sel inside { + `ASSERT_KNOWN_IF(IbexBTAluBOpMuxSelKnown, bt_b_mux_sel, instr_valid_i) + `ASSERT(IbexBTAluBOpMuxSelValid, instr_valid_i |-> bt_b_mux_sel inside { IMM_B_I, IMM_B_B, IMM_B_J, IMM_B_INCR_PC}) - `ASSERT(IbexRegfileWdataSelValid, rf_wdata_sel inside { + `ASSERT(IbexRegfileWdataSelValid, instr_valid_i |-> rf_wdata_sel inside { RF_WD_EX, RF_WD_CSR}) `ASSERT_KNOWN(IbexWbStateKnown, id_fsm_q) // Branch decision must be valid when jumping. - `ASSERT(IbexBranchDecisionValid, branch_in_dec |-> !$isunknown(branch_decision_i)) + `ASSERT_KNOWN_IF(IbexBranchDecisionValid, branch_decision_i, instr_valid_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)) + `ASSERT_KNOWN_IF(IbexIdInstrKnown, instr_rdata_i, + instr_valid_i && !(illegal_c_insn_i || instr_fetch_err_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)) + `ASSERT_KNOWN_IF(IbexIdInstrALUKnown, instr_rdata_alu_i, + instr_valid_i && !(illegal_c_insn_i || instr_fetch_err_i)) // Multicycle enable signals must be unique. `ASSERT(IbexMulticycleEnableUnique, diff --git a/shared/rtl/prim_assert.sv b/shared/rtl/prim_assert.sv index 1e536bf8..7e67adaa 100644 --- a/shared/rtl/prim_assert.sv +++ b/shared/rtl/prim_assert.sv @@ -53,18 +53,23 @@ // Immediate assertion // Note that immediate assertions are sensitive to simulation glitches. -`define ASSERT_I(__name, __prop) \ -`ifdef INC_ASSERT \ - __name: assert (__prop) \ - else `ASSERT_RPT(`PRIM_STRINGIFY(__name)) \ +`define ASSERT_I(__name, __prop) \ +`ifdef INC_ASSERT \ + __name: assert (__prop) \ + else begin \ + `ASSERT_RPT(`PRIM_STRINGIFY(__name)) \ + end \ `endif // Assertion in initial block. Can be used for things like parameter checking. -`define ASSERT_INIT(__name, __prop) \ -`ifdef INC_ASSERT \ - initial \ - __name: assert (__prop) \ - else `ASSERT_RPT(`PRIM_STRINGIFY(__name)) \ +`define ASSERT_INIT(__name, __prop) \ +`ifdef INC_ASSERT \ + initial begin \ + __name: assert (__prop) \ + else begin \ + `ASSERT_RPT(`PRIM_STRINGIFY(__name)) \ + end \ + end \ `endif // Assertion in final block. Can be used for things like queues being empty @@ -72,9 +77,12 @@ // at end of sim. `define ASSERT_FINAL(__name, __prop) \ `ifdef INC_ASSERT \ - final \ + final begin \ __name: assert (__prop || $test$plusargs("disable_assert_final_checks")) \ - else `ASSERT_RPT(`PRIM_STRINGIFY(__name)) \ + else begin \ + `ASSERT_RPT(`PRIM_STRINGIFY(__name)) \ + end \ + end \ `endif // Assert a concurrent property directly. @@ -82,7 +90,9 @@ `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)) \ + else begin \ + `ASSERT_RPT(`PRIM_STRINGIFY(__name)) \ + end \ `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 @@ -93,7 +103,9 @@ `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)) \ + else begin \ + `ASSERT_RPT(`PRIM_STRINGIFY(__name)) \ + end \ `endif // Assert that signal has a known value (each bit is either '0' or '1') after reset. @@ -119,19 +131,19 @@ `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 = `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) \ +// Assert that a property is true only when an enable signal is set. It can be called as a module +// (or interface) body item. +`define ASSERT_IF(__name, __prop, __enable, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \ +`ifdef INC_ASSERT \ + `ASSERT(__name, (__enable) |-> (__prop), __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 = `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) \ +// Assert that signal has a known value (each bit is either '0' or '1') after reset if enable is +// set. It can be called as a module (or interface) body item. +`define ASSERT_KNOWN_IF(__name, __sig, __enable, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \ +`ifdef INC_ASSERT \ + `ASSERT_KNOWN(__name``KnownEnable, __enable, __clk, __rst) \ + `ASSERT_IF(__name, !$isunknown(__sig), __enable, __clk, __rst) \ `endif /////////////////////// @@ -142,14 +154,18 @@ `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 `ASSERT_RPT(`PRIM_STRINGIFY(__name)) \ + else begin \ + `ASSERT_RPT(`PRIM_STRINGIFY(__name)) \ + end \ `endif // Assume an immediate property -`define ASSUME_I(__name, __prop) \ -`ifdef INC_ASSERT \ - __name: assume (__prop) \ - else `ASSERT_RPT(`PRIM_STRINGIFY(__name)) \ +`define ASSUME_I(__name, __prop) \ +`ifdef INC_ASSERT \ + __name: assume (__prop) \ + else begin \ + `ASSERT_RPT(`PRIM_STRINGIFY(__name)) \ + end \ `endif ////////////////////////////////// @@ -168,9 +184,9 @@ // ASSUME_I_FPV // Assume a concurrent property during formal verification only. -`define ASSUME_I_FPV(__name, __prop) \ -`ifdef FPV_ON \ - `ASSUME_I(__name, __prop) \ +`define ASSUME_I_FPV(__name, __prop) \ +`ifdef FPV_ON \ + `ASSUME_I(__name, __prop) \ `endif // COVER_FPV