mirror of
https://github.com/openhwgroup/cve2.git
synced 2025-04-22 04:57:25 -04:00
[rtl] Modify ASSERT_KNOWN uses to work with xprop
When xprop is enabled various case and if/else constructs will propagate X leading to failures in ASSERT_KNOWN. This introduces enable terms to various ASSERT_KNOWN uses that would otherwise fail without them. prim_assert.sv changes copied across from OpenTitan respository.
This commit is contained in:
Greg Chadwick
parent
4f39160843
commit
cb8afccb7c
4 changed files with 72 additions and 54 deletions
|
|
@ -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];
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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,
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue