github-mirrors/cve2
1
0
Fork 0
mirror of https://github.com/openhwgroup/cve2.git synced 2025-04-22 04:57:25 -04:00
Code Issues Projects Releases Packages Wiki Activity Actions

[rtl] Introduce default clk/reset to prim_assert

Browse source 
This mirrors the change made in OpenTitan
(https://github.com/lowRISC/opentitan/pull/1485)
This commit is contained in:
Greg Chadwick 2020-02-07 16:44:46 +00:00
parent c914ec5e6a
commit 5d16a5b104
10 changed files with 77 additions and 82 deletions
Download patch file Download diff file Expand all files Collapse all files

12
rtl/ibex_compressed_decoder.sv
View file

@ -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

3
rtl/ibex_controller.sv
View file

@ -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

4
rtl/ibex_cs_registers.sv
View file

@ -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

2
rtl/ibex_decoder.sv
View file

@ -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

4
rtl/ibex_fetch_fifo.sv
View file

@ -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

20
rtl/ibex_id_stage.sv
View file

@ -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

13
rtl/ibex_if_stage.sv
View file

@ -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

20
rtl/ibex_load_store_unit.sv
View file

@ -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

5
rtl/ibex_multdiv_fast.sv
View file

@ -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

76
shared/rtl/prim_assert.sv
View file

@ -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