mirror of
https://github.com/lowRISC/ibex.git
synced 2025-04-22 21:07:34 -04:00
[dv] PMP related functional coverage points
Adding MSECCFG CSR related functionality also some write checks etc. Signed-off-by: Canberk Topal <ctopal@lowrisc.org>
This commit is contained in:
parent
ea4e9383db
commit
c253bd76a9
3 changed files with 425 additions and 83 deletions
|
@ -248,9 +248,9 @@ PMP
|
|||
|
||||
* Access fail & pass.
|
||||
|
||||
* All combinations of unaligned access split across a boundary, both halves pass, neither pass, just the first passes, just the second passes.
|
||||
* ``misaligned_lsu_access_cross`` - All combinations of unaligned access split across a boundary, both halves pass, neither pass, just the first passes, just the second passes.
|
||||
|
||||
* Two possible boundary splits; across a 32-bit boundary within a region or a boundary between PMP regions.
|
||||
* ``pmp_instr_edge_cross`` - Two possible boundary splits; across a 32-bit boundary within a region or a boundary between PMP regions.
|
||||
|
||||
* ``cp_pmp_iside_region_override``, ``cp_pmp_iside2_region_override``, ``cp_pmp_dside_region_override`` - Higher priority entry allows access that lower priority entry prevents.
|
||||
* Compressed instruction access (16-bit) passes PMP but 32-bit access at same address crosses PMP region boundary.
|
||||
|
@ -259,17 +259,17 @@ PMP
|
|||
|
||||
* RLB - rule locking bypass.
|
||||
|
||||
* Modify locked region with RLB set.
|
||||
* Try to enable RLB when RLB is disabled and locked regions present.
|
||||
* ``cp_edit_locked_pmpcfg``,``cp_edit_locked_pmpaddr`` - Modify locked region with RLB set.
|
||||
* ``rlb_csr_cross`` - Try to enable RLB when RLB is disabled and locked regions present.
|
||||
|
||||
* MMWP - machine mode whitelist policy.
|
||||
|
||||
* M-mode access fail due to not matching any PMP regions.
|
||||
* Try to disable when enabled.
|
||||
* ``pmp_dside/iside/iside2_nomatch_cross`` - M-mode access fail due to not matching any PMP regions.
|
||||
* ``mmwp_csr_cross`` - Try to disable when enabled.
|
||||
|
||||
* MML - machine mode lockdown policy.
|
||||
|
||||
* Try to disable when enabled.
|
||||
* ``rlb_csr_cross`` - Try to disable when enabled.
|
||||
|
||||
* Access close to PMP region modification that allows/disallows that access.
|
||||
|
||||
|
|
|
@ -21,7 +21,7 @@ interface core_ibex_pmp_fcov_if import ibex_pkg::*; #(
|
|||
|
||||
input logic data_req_out,
|
||||
|
||||
input logic lsu_req_done
|
||||
input fcov_csr_write
|
||||
);
|
||||
localparam int unsigned PMPNumChan = 3;
|
||||
|
||||
|
@ -31,40 +31,39 @@ interface core_ibex_pmp_fcov_if import ibex_pkg::*; #(
|
|||
// Enum to give more readable coverage results for privilege bits. 4 bits are from the pmpcfg CSF
|
||||
// (L, X, W, R) and the 5th is the MML bit. Setting the MML bit changes the meaning of the other
|
||||
// 4 bits
|
||||
// TODO: Better MML names?
|
||||
typedef enum logic [4:0] {
|
||||
PMP_PRIV_NONE = 5'b00000,
|
||||
PMP_PRIV_R = 5'b00001,
|
||||
PMP_PRIV_W = 5'b00010,
|
||||
PMP_PRIV_WR = 5'b00011,
|
||||
PMP_PRIV_X = 5'b00100,
|
||||
PMP_PRIV_XR = 5'b00101,
|
||||
PMP_PRIV_XW = 5'b00110,
|
||||
PMP_PRIV_XWR = 5'b00111,
|
||||
PMP_PRIV_L = 5'b01000,
|
||||
PMP_PRIV_LR = 5'b01001,
|
||||
PMP_PRIV_LW = 5'b01010,
|
||||
PMP_PRIV_LWR = 5'b01011,
|
||||
PMP_PRIV_LX = 5'b01100,
|
||||
PMP_PRIV_LXR = 5'b01101,
|
||||
PMP_PRIV_LXW = 5'b01110,
|
||||
PMP_PRIV_LXWR = 5'b01111,
|
||||
PMP_PRIV_MML_NONE = 5'b10000,
|
||||
PMP_PRIV_MML_R = 5'b10001,
|
||||
PMP_PRIV_MML_W = 5'b10010,
|
||||
PMP_PRIV_MML_WR = 5'b10011,
|
||||
PMP_PRIV_MML_X = 5'b10100,
|
||||
PMP_PRIV_MML_XR = 5'b10101,
|
||||
PMP_PRIV_MML_XW = 5'b10110,
|
||||
PMP_PRIV_MML_XWR = 5'b10111,
|
||||
PMP_PRIV_MML_L = 5'b11000,
|
||||
PMP_PRIV_MML_LR = 5'b11001,
|
||||
PMP_PRIV_MML_LW = 5'b11010,
|
||||
PMP_PRIV_MML_LWR = 5'b11011,
|
||||
PMP_PRIV_MML_LX = 5'b11100,
|
||||
PMP_PRIV_MML_LXR = 5'b11101,
|
||||
PMP_PRIV_MML_LXW = 5'b11110,
|
||||
PMP_PRIV_MML_LXWR = 5'b11111
|
||||
NONE = 5'b00000,
|
||||
R = 5'b00001,
|
||||
W = 5'b00010,
|
||||
WR = 5'b00011,
|
||||
X = 5'b00100,
|
||||
XR = 5'b00101,
|
||||
XW = 5'b00110,
|
||||
XWR = 5'b00111,
|
||||
L = 5'b01000,
|
||||
LR = 5'b01001,
|
||||
LW = 5'b01010,
|
||||
LWR = 5'b01011,
|
||||
LX = 5'b01100,
|
||||
LXR = 5'b01101,
|
||||
LXW = 5'b01110,
|
||||
LXWR = 5'b01111,
|
||||
MML_NONE = 5'b10000,
|
||||
MML_RU = 5'b10001,
|
||||
MML_WRM_RU = 5'b10010,
|
||||
MML_WRU = 5'b10011,
|
||||
MML_XU = 5'b10100,
|
||||
MML_XRU = 5'b10101,
|
||||
MML_WRM_WRU = 5'b10110,
|
||||
MML_XWRU = 5'b10111,
|
||||
MML_L = 5'b11000,
|
||||
MML_RM = 5'b11001,
|
||||
MML_XM_XU = 5'b11010,
|
||||
MML_WRM = 5'b11011,
|
||||
MML_XM = 5'b11100,
|
||||
MML_XRM = 5'b11101,
|
||||
MML_XRM_XU = 5'b11110,
|
||||
MML_RM_RU = 5'b11111
|
||||
} pmp_priv_bits_e;
|
||||
|
||||
// Break out PMP signals into individually named signals for direct use in `cross` as it cannot
|
||||
|
@ -80,6 +79,14 @@ interface core_ibex_pmp_fcov_if import ibex_pkg::*; #(
|
|||
logic [PMPNumRegions-1:0] current_priv_perm_check;
|
||||
bit en_pmp_fcov;
|
||||
|
||||
logic csr_wdata_mseccfg_rlb;
|
||||
logic csr_wdata_mseccfg_mmwp;
|
||||
logic csr_wdata_mseccfg_mml;
|
||||
|
||||
assign csr_wdata_mseccfg_rlb = cs_registers_i.csr_wdata_int[CSR_MSECCFG_RLB_BIT];
|
||||
assign csr_wdata_mseccfg_mmwp = cs_registers_i.csr_wdata_int[CSR_MSECCFG_MMWP_BIT];
|
||||
assign csr_wdata_mseccfg_mml = cs_registers_i.csr_wdata_int[CSR_MSECCFG_MML_BIT];
|
||||
|
||||
initial begin
|
||||
if (PMPEnable) begin
|
||||
void'($value$plusargs("enable_ibex_fcov=%d", en_pmp_fcov));
|
||||
|
@ -89,6 +96,44 @@ interface core_ibex_pmp_fcov_if import ibex_pkg::*; #(
|
|||
end
|
||||
|
||||
if (PMPEnable) begin : g_pmp_cgs
|
||||
logic [PMPNumRegions-1:0] pmp_iside_match;
|
||||
logic [PMPNumRegions-1:0] pmp_iside2_match;
|
||||
logic [PMPNumRegions-1:0] pmp_dside_match;
|
||||
logic [PMPNumRegions-1:0] pmp_dside_match_last;
|
||||
|
||||
logic pmp_iside_nomatch;
|
||||
logic pmp_iside2_nomatch;
|
||||
logic pmp_dside_nomatch;
|
||||
|
||||
logic pmp_iside_boundary_cross;
|
||||
logic pmp_dside_boundary_cross;
|
||||
|
||||
logic misaligned_pmp_err_last;
|
||||
|
||||
assign pmp_iside_match = g_pmp.pmp_i.region_match_all[PMP_I];
|
||||
assign pmp_iside2_match = g_pmp.pmp_i.region_match_all[PMP_I2];
|
||||
assign pmp_dside_match = g_pmp.pmp_i.region_match_all[PMP_D];
|
||||
|
||||
assign pmp_iside_nomatch = ~|pmp_iside_match;
|
||||
assign pmp_iside2_nomatch = ~|pmp_iside2_match;
|
||||
assign pmp_dside_nomatch = ~|pmp_dside_match;
|
||||
|
||||
assign misaligned_pmp_err_last = load_store_unit_i.fcov_ls_first_req ?
|
||||
load_store_unit_i.data_pmp_err_i :
|
||||
misaligned_pmp_err_last;
|
||||
|
||||
// Store the Data Channel PMP match info from the first request to calculate boundary cross
|
||||
always @(posedge clk_i or negedge rst_ni) begin
|
||||
if (!rst_ni) begin
|
||||
pmp_dside_match_last <= '0;
|
||||
end else if (load_store_unit_i.fcov_ls_first_req) begin
|
||||
pmp_dside_match_last <= pmp_dside_match;
|
||||
end
|
||||
end
|
||||
|
||||
assign pmp_iside_boundary_cross = |(pmp_iside_match ^ pmp_iside2_match);
|
||||
assign pmp_dside_boundary_cross = |(pmp_dside_match ^ pmp_dside_match_last);
|
||||
|
||||
for (genvar i_region = 0; i_region < PMPNumRegions; i_region += 1) begin : g_pmp_region_fcov
|
||||
pmp_priv_bits_e pmp_region_priv_bits;
|
||||
|
||||
|
@ -117,7 +162,6 @@ interface core_ibex_pmp_fcov_if import ibex_pkg::*; #(
|
|||
cp_region_mode : coverpoint csr_pmp_cfg[i_region].mode;
|
||||
|
||||
cp_region_priv_bits : coverpoint pmp_region_priv_bits {
|
||||
wildcard ignore_bins ignore = {5'b1????};
|
||||
wildcard illegal_bins illegal = {5'b0??10};
|
||||
}
|
||||
|
||||
|
@ -145,6 +189,8 @@ interface core_ibex_pmp_fcov_if import ibex_pkg::*; #(
|
|||
illegal_bins illegal = {PMP_ACC_EXEC};
|
||||
}
|
||||
|
||||
// Wildcards in crosses are not supported by VCS. As a workaround we are using `with`
|
||||
// keyword and basic logic expressions to constraint the condition as appropriate.
|
||||
pmp_iside_mode_cross : cross cp_region_mode, pmp_iside_req_err
|
||||
iff (g_pmp_fcov_signals.g_pmp_region_fcov[i_region].fcov_pmp_region_ichan_access);
|
||||
|
||||
|
@ -154,26 +200,54 @@ interface core_ibex_pmp_fcov_if import ibex_pkg::*; #(
|
|||
pmp_dside_mode_cross : cross cp_region_mode, pmp_dside_req_err
|
||||
iff (g_pmp_fcov_signals.g_pmp_region_fcov[i_region].fcov_pmp_region_dchan_access);
|
||||
|
||||
// TODO: Coverage for accesses that don't match any regions
|
||||
|
||||
pmp_iside_priv_bits_cross :
|
||||
cross cp_region_priv_bits, cp_req_type_iside, cp_priv_lvl_iside, pmp_iside_req_err
|
||||
iff (g_pmp_fcov_signals.g_pmp_region_fcov[i_region].fcov_pmp_region_ichan_access &&
|
||||
g_pmp_fcov_signals.fcov_pmp_region_ichan_priority[i_region] &&
|
||||
csr_pmp_cfg[i_region].mode != PMP_MODE_OFF) {
|
||||
|
||||
// Will never see a succesful exec access when execute is disallowed
|
||||
illegal_bins illegal_allow_exec = (binsof(cp_region_priv_bits) intersect {5'b00000,
|
||||
5'b00001, 5'b00010, 5'b00011, 5'b01000, 5'b01001, 5'b01010, 5'b01011} &&
|
||||
binsof(cp_req_type_iside) intersect {PMP_ACC_EXEC} &&
|
||||
binsof(pmp_iside_req_err) intersect {0}) with (cp_priv_lvl_iside == PRIV_LVL_U ||
|
||||
(cp_region_priv_bits & 5'b01000));
|
||||
|
||||
// Will never see an exec access denied when executed is allowed
|
||||
illegal_bins illegal_deny_exec = binsof(cp_region_priv_bits) intersect {5'b00100, 5'b00101,
|
||||
5'b00110, 5'b00111, 5'b01100, 5'b01101, 5'b01110, 5'b01111} &&
|
||||
binsof(cp_req_type_iside) intersect {PMP_ACC_EXEC} &&
|
||||
binsof(pmp_iside_req_err) intersect {1};
|
||||
// Will never see a succesful exec access when execute is disallowed
|
||||
illegal_bins illegal_allow_exec =
|
||||
// Ensuring MML is low and we are not in a X allowed configuration
|
||||
(binsof(cp_region_priv_bits) intersect {NONE, R, W, WR, L, LR, LW, LWR} &&
|
||||
binsof(cp_req_type_iside) intersect {PMP_ACC_EXEC} &&
|
||||
binsof(pmp_iside_req_err) intersect {0}) with (cp_priv_lvl_iside == PRIV_LVL_U ||
|
||||
(|(cp_region_priv_bits & 5'b01000)));
|
||||
illegal_bins illegal_machine_allow_exec =
|
||||
// Ensuring MML is high and we are not in a X allowed configuration in Machine Mode
|
||||
(binsof(cp_region_priv_bits) intersect {MML_NONE, MML_RU, MML_WRM_RU, MML_WRU, MML_XU,
|
||||
MML_XRU, MML_WRM_WRU, MML_XWRU, MML_L, MML_RM,
|
||||
MML_WRM, MML_RM_RU} &&
|
||||
binsof(cp_priv_lvl_iside) intersect {PRIV_LVL_M} &&
|
||||
binsof(cp_req_type_iside) intersect {PMP_ACC_EXEC} &&
|
||||
binsof(pmp_iside_req_err) intersect {0});
|
||||
illegal_bins illegal_user_allow_exec =
|
||||
// Ensuring MML is high and we are not in a X allowed configuration in User Mode
|
||||
(binsof(cp_region_priv_bits) intersect {MML_NONE, MML_RU, MML_WRM_RU, MML_WRU,
|
||||
MML_WRM_WRU, MML_L, MML_RM, MML_WRM,
|
||||
MML_XM, MML_XRM, MML_RM_RU} &&
|
||||
binsof(cp_priv_lvl_iside) intersect {PRIV_LVL_U} &&
|
||||
binsof(cp_req_type_iside) intersect {PMP_ACC_EXEC} &&
|
||||
binsof(pmp_iside_req_err) intersect {0});
|
||||
// Will never see an exec access denied when executed is allowed
|
||||
illegal_bins illegal_deny_exec =
|
||||
// Ensuring MML is low and we are in a X allowed configuration
|
||||
(binsof(cp_req_type_iside) intersect {PMP_ACC_EXEC} &&
|
||||
binsof(cp_region_priv_bits) intersect {X, XW, XR, XWR, LX, LXW, LXR, LXWR} &&
|
||||
binsof(pmp_iside_req_err) intersect {1});
|
||||
illegal_bins illegal_machine_deny_exec =
|
||||
// Ensuring MML is high and we are in a X allowed configuration in Machine Mode
|
||||
(binsof(cp_region_priv_bits) intersect {MML_XM_XU, MML_XRM_XU, MML_XRM, MML_XM} &&
|
||||
binsof(cp_priv_lvl_iside) intersect {PRIV_LVL_M} &&
|
||||
binsof(cp_req_type_iside) intersect {PMP_ACC_EXEC} &&
|
||||
binsof(pmp_iside_req_err) intersect {1});
|
||||
illegal_bins illegal_user_deny_exec =
|
||||
// Ensuring MML is high and we are in a X allowed configuration in User Mode
|
||||
(binsof(cp_region_priv_bits) intersect {MML_XM_XU, MML_XRM_XU, MML_XRU, MML_XU,
|
||||
MML_XWRU} &&
|
||||
binsof(cp_priv_lvl_iside) intersect {PRIV_LVL_U} &&
|
||||
binsof(cp_req_type_iside) intersect {PMP_ACC_EXEC} &&
|
||||
binsof(pmp_iside_req_err) intersect {1});
|
||||
}
|
||||
|
||||
pmp_iside2_priv_bits_cross :
|
||||
|
@ -183,17 +257,48 @@ interface core_ibex_pmp_fcov_if import ibex_pkg::*; #(
|
|||
csr_pmp_cfg[i_region].mode != PMP_MODE_OFF) {
|
||||
|
||||
// Will never see a succesful exec access when execute is disallowed
|
||||
illegal_bins illegal_allow_exec = (binsof(cp_region_priv_bits) intersect {5'b00000,
|
||||
5'b00001, 5'b00010, 5'b00011, 5'b01000, 5'b01001, 5'b01010, 5'b01011} &&
|
||||
binsof(cp_req_type_iside2) intersect {PMP_ACC_EXEC} &&
|
||||
binsof(pmp_iside2_req_err) intersect {0}) with (cp_priv_lvl_iside2 == PRIV_LVL_U ||
|
||||
(cp_region_priv_bits & 5'b01000));
|
||||
illegal_bins illegal_allow_exec =
|
||||
// Ensuring MML is low and we are not in a X allowed configuration
|
||||
(binsof(cp_region_priv_bits) intersect {NONE, R, W, WR, L, LR, LW, LWR} &&
|
||||
binsof(cp_req_type_iside2) intersect {PMP_ACC_EXEC} &&
|
||||
binsof(pmp_iside2_req_err) intersect {0}) with (cp_priv_lvl_iside2 == PRIV_LVL_U ||
|
||||
(cp_region_priv_bits & 5'b01000));
|
||||
illegal_bins illegal_machine_allow_exec =
|
||||
// Ensuring MML is high and we are not in a X allowed configuration in Machine Mode
|
||||
(binsof(cp_region_priv_bits) intersect {MML_NONE, MML_RU, MML_WRM_RU, MML_WRU, MML_XU,
|
||||
MML_XRU, MML_WRM_WRU, MML_XWRU, MML_L, MML_RM,
|
||||
MML_WRM, MML_RM_RU} &&
|
||||
binsof(cp_priv_lvl_iside2) intersect {PRIV_LVL_M} &&
|
||||
binsof(cp_req_type_iside2) intersect {PMP_ACC_EXEC} &&
|
||||
binsof(pmp_iside2_req_err) intersect {0});
|
||||
illegal_bins illegal_user_allow_exec =
|
||||
// Ensuring MML is high and we are not in a X allowed configuration in User Mode
|
||||
(binsof(cp_region_priv_bits) intersect {MML_NONE, MML_RU, MML_WRM_RU, MML_WRU,
|
||||
MML_WRM_WRU, MML_L, MML_RM, MML_WRM,
|
||||
MML_XM, MML_XRM, MML_RM_RU} &&
|
||||
binsof(cp_priv_lvl_iside2) intersect {PRIV_LVL_U} &&
|
||||
binsof(cp_req_type_iside2) intersect {PMP_ACC_EXEC} &&
|
||||
binsof(pmp_iside2_req_err) intersect {0});
|
||||
|
||||
// Will never see an exec access denied when execute is allowed
|
||||
illegal_bins illegal_deny_exec = binsof(cp_region_priv_bits) intersect {5'b00100, 5'b00101,
|
||||
5'b00110, 5'b00111, 5'b01100, 5'b01101, 5'b01110, 5'b01111} &&
|
||||
binsof(cp_req_type_iside2) intersect {PMP_ACC_EXEC} &&
|
||||
binsof(pmp_iside2_req_err) intersect {1};
|
||||
illegal_bins illegal_deny_exec =
|
||||
// Ensuring MML is low and we are in a X allowed configuration
|
||||
(binsof(cp_region_priv_bits) intersect {X, XW, XR, XWR, LX, LXW, LXR, LXWR} &&
|
||||
binsof(cp_req_type_iside2) intersect {PMP_ACC_EXEC} &&
|
||||
binsof(pmp_iside2_req_err) intersect {1});
|
||||
illegal_bins illegal_machine_deny_exec =
|
||||
// Ensuring MML is high and we are in a X allowed configuration in Machine Mode
|
||||
(binsof(cp_region_priv_bits) intersect {MML_XM_XU, MML_XRM_XU, MML_XRM, MML_XM} &&
|
||||
binsof(cp_priv_lvl_iside2) intersect {PRIV_LVL_M} &&
|
||||
binsof(cp_req_type_iside2) intersect {PMP_ACC_EXEC} &&
|
||||
binsof(pmp_iside2_req_err) intersect {1});
|
||||
illegal_bins illegal_user_deny_exec =
|
||||
// Ensuring MML is high and we are in a X allowed configuration in User Mode
|
||||
(binsof(cp_region_priv_bits) intersect {MML_XM_XU, MML_XRM_XU, MML_XRU, MML_XU,
|
||||
MML_XWRU} &&
|
||||
binsof(cp_priv_lvl_iside2) intersect {PRIV_LVL_U} &&
|
||||
binsof(cp_req_type_iside2) intersect {PMP_ACC_EXEC} &&
|
||||
binsof(pmp_iside2_req_err) intersect {1});
|
||||
}
|
||||
|
||||
pmp_dside_priv_bits_cross :
|
||||
|
@ -203,31 +308,103 @@ interface core_ibex_pmp_fcov_if import ibex_pkg::*; #(
|
|||
csr_pmp_cfg[i_region].mode != PMP_MODE_OFF) {
|
||||
|
||||
// Will never see a succesful read access when read is disallowed
|
||||
illegal_bins illegal_allow_read = (binsof(cp_region_priv_bits) intersect {5'b00000,
|
||||
5'b00010, 5'b00100, 5'b00110, 5'b01000, 5'b01010, 5'b01100, 5'b01110} &&
|
||||
binsof(cp_req_type_dside) intersect {PMP_ACC_READ} &&
|
||||
binsof(pmp_dside_req_err) intersect {0}) with (cp_priv_lvl_dside == PRIV_LVL_U ||
|
||||
(cp_region_priv_bits & 5'b01000));
|
||||
illegal_bins illegal_allow_read =
|
||||
// Ensuring MML is low and we are not in a R allowed configuration
|
||||
(binsof(cp_region_priv_bits) intersect {NONE, W, X, XW, L, LW, LX, LXW} &&
|
||||
binsof(cp_req_type_dside) intersect {PMP_ACC_READ} &&
|
||||
binsof(pmp_dside_req_err) intersect {0})
|
||||
with (cp_priv_lvl_dside == PRIV_LVL_U || (cp_region_priv_bits & 5'b01000));
|
||||
illegal_bins illegal_machine_allow_read =
|
||||
// Ensuring MML is high and we are not in a R allowed configuration in Machine Mode
|
||||
(binsof(cp_region_priv_bits) intersect {MML_NONE, MML_RU, MML_WRU, MML_XU, MML_XRU,
|
||||
MML_XWRU, MML_L, MML_XM_XU, MML_XM} &&
|
||||
binsof(cp_priv_lvl_dside) intersect {PRIV_LVL_M} &&
|
||||
binsof(cp_req_type_dside) intersect {PMP_ACC_READ} &&
|
||||
binsof(pmp_dside_req_err) intersect {0});
|
||||
illegal_bins illegal_user_allow_read =
|
||||
// Ensuring MML is high and we are not in a R allowed configuration in User Mode
|
||||
(binsof(cp_region_priv_bits) intersect {MML_NONE, MML_XU, MML_L, MML_RM, MML_XM_XU,
|
||||
MML_WRM, MML_XM, MML_XRM, MML_XRM_XU} &&
|
||||
binsof(cp_priv_lvl_dside) intersect {PRIV_LVL_U} &&
|
||||
binsof(cp_req_type_dside) intersect {PMP_ACC_READ} &&
|
||||
binsof(pmp_dside_req_err) intersect {0});
|
||||
|
||||
// Will never see a read access denied when read is allowed
|
||||
illegal_bins illegal_deny_read = binsof(cp_region_priv_bits) intersect {5'b00001, 5'b00011,
|
||||
5'b00101, 5'b00111, 5'b01001, 5'b01011, 5'b01101, 5'b01111} &&
|
||||
binsof(cp_req_type_dside) intersect {PMP_ACC_READ} &&
|
||||
binsof(pmp_dside_req_err) intersect {1};
|
||||
illegal_bins illegal_deny_read =
|
||||
// Ensuring MML is low and we are in a R allowed configuration
|
||||
(binsof(cp_region_priv_bits) intersect {R, WR, XR, XWR, LR, LWR, LXR, LXWR} &&
|
||||
binsof(cp_req_type_dside) intersect {PMP_ACC_READ} &&
|
||||
binsof(pmp_dside_req_err) intersect {1});
|
||||
illegal_bins illegal_machine_deny_read =
|
||||
// Ensuring MML is high and we are in a R allowed configuration in Machine Mode
|
||||
(binsof(cp_region_priv_bits) intersect {MML_WRM_RU, MML_WRM_WRU, MML_RM_RU, MML_RM,
|
||||
MML_WRM, MML_XRM, MML_XRM_XU} &&
|
||||
binsof(cp_priv_lvl_dside) intersect {PRIV_LVL_M} &&
|
||||
binsof(cp_req_type_dside) intersect {PMP_ACC_READ} &&
|
||||
binsof(pmp_dside_req_err) intersect {1});
|
||||
illegal_bins illegal_user_deny_read =
|
||||
// Ensuring MML is high and we are not in a R allowed configuration in User Mode
|
||||
(binsof(cp_region_priv_bits) intersect {MML_WRM_RU, MML_WRM_WRU, MML_RM_RU, MML_RU,
|
||||
MML_WRU, MML_XRU, MML_XWRU} &&
|
||||
binsof(cp_priv_lvl_dside) intersect {PRIV_LVL_U} &&
|
||||
binsof(cp_req_type_dside) intersect {PMP_ACC_READ} &&
|
||||
binsof(pmp_dside_req_err) intersect {1});
|
||||
|
||||
// Will never see a succesful write access when write is disallowed
|
||||
illegal_bins illegal_allow_write = (binsof(cp_region_priv_bits) intersect {5'b00000,
|
||||
5'b00001, 5'b00100, 5'b00101, 5'b01000, 5'b01001, 5'b01100, 5'b01101} &&
|
||||
binsof(cp_req_type_dside) intersect {PMP_ACC_WRITE} &&
|
||||
binsof(pmp_dside_req_err) intersect {0}) with (cp_priv_lvl_dside == PRIV_LVL_U ||
|
||||
(cp_region_priv_bits & 5'b01000));
|
||||
illegal_bins illegal_allow_write =
|
||||
// Ensuring MML is low and we are not in a W allowed configuration
|
||||
(binsof(cp_region_priv_bits) intersect {NONE, R, X, XR, L, LR, LX, LXR} &&
|
||||
binsof(cp_req_type_dside) intersect {PMP_ACC_WRITE} &&
|
||||
binsof(pmp_dside_req_err) intersect {0})
|
||||
with (cp_priv_lvl_dside == PRIV_LVL_U || (cp_region_priv_bits & 5'b01000));
|
||||
illegal_bins illegal_machine_allow_write =
|
||||
// Ensuring MML is high and we are not in a W allowed configuration in Machine Mode
|
||||
(binsof(cp_region_priv_bits) intersect {MML_NONE, MML_RU, MML_WRU, MML_XU, MML_XRU,
|
||||
MML_XWRU, MML_L, MML_RM, MML_XM_XU, MML_XM,
|
||||
MML_XRM, MML_XRM_XU, MML_RM_RU} &&
|
||||
binsof(cp_priv_lvl_dside) intersect {PRIV_LVL_M} &&
|
||||
binsof(cp_req_type_dside) intersect {PMP_ACC_WRITE} &&
|
||||
binsof(pmp_dside_req_err) intersect {1});
|
||||
illegal_bins illegal_user_allow_write =
|
||||
// Ensuring MML is high and we are not in a W allowed configuration in User Mode
|
||||
(binsof(cp_region_priv_bits) intersect {MML_NONE, MML_RU, MML_WRM_RU, MML_XU, MML_XRU,
|
||||
MML_L, MML_RM, MML_XM_XU, MML_WRM, MML_XM,
|
||||
MML_XRM, MML_XRM_XU, MML_RM_RU} &&
|
||||
binsof(cp_priv_lvl_dside) intersect {PRIV_LVL_U} &&
|
||||
binsof(cp_req_type_dside) intersect {PMP_ACC_WRITE} &&
|
||||
binsof(pmp_dside_req_err) intersect {1});
|
||||
|
||||
// Will never see a write access denied when write is allowed
|
||||
illegal_bins illegal_deny_write = binsof(cp_region_priv_bits) intersect {5'b00010, 5'b00011,
|
||||
5'b00110, 5'b00111, 5'b01010, 5'b01011, 5'b01110, 5'b01111} &&
|
||||
binsof(cp_req_type_dside) intersect {PMP_ACC_WRITE} &&
|
||||
binsof(pmp_dside_req_err) intersect {1};
|
||||
illegal_bins illegal_deny_write =
|
||||
// Ensuring MML is low and we are in a W allowed configuration
|
||||
(binsof(cp_region_priv_bits) intersect {W, WR, XW, XWR, LW, LWR, LXW, LXWR} &&
|
||||
binsof(cp_req_type_dside) intersect {PMP_ACC_WRITE} &&
|
||||
binsof(pmp_dside_req_err) intersect {1});
|
||||
illegal_bins illegal_machine_deny_write =
|
||||
// Ensuring MML is high and we are in a W allowed configuration in Machine Mode
|
||||
(binsof(cp_region_priv_bits) intersect {MML_WRM_WRU, MML_WRM_RU, MML_WRM} &&
|
||||
binsof(cp_priv_lvl_dside) intersect {PRIV_LVL_M} &&
|
||||
binsof(cp_req_type_dside) intersect {PMP_ACC_WRITE} &&
|
||||
binsof(pmp_dside_req_err) intersect {1});
|
||||
// Ensuring MML is high and we are in a W allowed configuration in User Mode
|
||||
illegal_bins illegal_user_deny_write =
|
||||
(binsof(cp_region_priv_bits) intersect {MML_WRM_WRU, MML_WRU, MML_XWRU} &&
|
||||
binsof(cp_priv_lvl_dside) intersect {PRIV_LVL_U} &&
|
||||
binsof(cp_req_type_dside) intersect {PMP_ACC_WRITE} &&
|
||||
binsof(pmp_dside_req_err) intersect {1});
|
||||
}
|
||||
|
||||
`DV_FCOV_EXPR_SEEN(edit_locked_pmpcfg,
|
||||
fcov_csr_write &&
|
||||
csr_pmp_cfg[i_region].lock &&
|
||||
cs_registers_i.g_pmp_registers.g_pmp_csrs[i_region].u_pmp_cfg_csr.wr_en_i &&
|
||||
csr_pmp_mseccfg.rlb)
|
||||
|
||||
`DV_FCOV_EXPR_SEEN(edit_locked_pmpaddr,
|
||||
fcov_csr_write &&
|
||||
csr_pmp_cfg[i_region].lock &&
|
||||
cs_registers_i.g_pmp_registers.g_pmp_csrs[i_region].u_pmp_addr_csr.wr_en_i &&
|
||||
csr_pmp_mseccfg.rlb)
|
||||
endgroup
|
||||
|
||||
`DV_FCOV_INSTANTIATE_CG(pmp_region_cg, en_pmp_fcov)
|
||||
|
@ -247,6 +424,158 @@ interface core_ibex_pmp_fcov_if import ibex_pkg::*; #(
|
|||
option.per_instance = 1;
|
||||
option.name = "pmp_top_cg";
|
||||
|
||||
cp_rlb : coverpoint csr_pmp_mseccfg.rlb{
|
||||
bins on = {1'b1};
|
||||
bins off = {1'b0};
|
||||
}
|
||||
|
||||
cp_mmwp : coverpoint csr_pmp_mseccfg.mmwp{
|
||||
bins on = {1'b1};
|
||||
bins off = {1'b0};
|
||||
}
|
||||
|
||||
cp_mml : coverpoint csr_pmp_mseccfg.mml{
|
||||
bins on = {1'b1};
|
||||
bins off = {1'b0};
|
||||
}
|
||||
|
||||
cp_wdata_rlb: coverpoint csr_wdata_mseccfg_rlb{
|
||||
bins on = {1'b1};
|
||||
bins off = {1'b0};
|
||||
}
|
||||
|
||||
cp_wdata_mmwp: coverpoint csr_wdata_mseccfg_mmwp{
|
||||
bins on = {1'b1};
|
||||
bins off = {1'b0};
|
||||
}
|
||||
|
||||
cp_wdata_mml: coverpoint csr_wdata_mseccfg_mml{
|
||||
bins on = {1'b1};
|
||||
bins off = {1'b0};
|
||||
}
|
||||
|
||||
//////// Redundant coverpoints for nomatch crosses ///////////
|
||||
cp_priv_lvl_iside : coverpoint g_pmp.pmp_priv_lvl[PMP_I] {
|
||||
illegal_bins illegal = {PRIV_LVL_H, PRIV_LVL_S};
|
||||
}
|
||||
|
||||
cp_req_type_iside : coverpoint g_pmp.pmp_req_type[PMP_I] {
|
||||
illegal_bins illegal = {PMP_ACC_WRITE, PMP_ACC_READ};
|
||||
}
|
||||
|
||||
cp_priv_lvl_iside2 : coverpoint g_pmp.pmp_priv_lvl[PMP_I2] {
|
||||
illegal_bins illegal = {PRIV_LVL_H, PRIV_LVL_S};
|
||||
}
|
||||
|
||||
cp_req_type_iside2 : coverpoint g_pmp.pmp_req_type[PMP_I2] {
|
||||
illegal_bins illegal = {PMP_ACC_WRITE, PMP_ACC_READ};
|
||||
}
|
||||
|
||||
cp_priv_lvl_dside : coverpoint g_pmp.pmp_priv_lvl[PMP_D] {
|
||||
illegal_bins illegal = {PRIV_LVL_H, PRIV_LVL_S};
|
||||
}
|
||||
|
||||
cp_req_type_dside : coverpoint g_pmp.pmp_req_type[PMP_D] {
|
||||
illegal_bins illegal = {PMP_ACC_EXEC};
|
||||
}
|
||||
//////////////////////////////////////////////////////////////
|
||||
|
||||
rlb_csr_cross : cross cp_rlb, cp_wdata_rlb
|
||||
iff (fcov_csr_write && cs_registers_i.csr_addr_i == CSR_MSECCFG) {
|
||||
// Trying to enable RLB when RLB is disabled and locked regions present will result
|
||||
// with an ignored write
|
||||
bins sticky = binsof(cp_rlb) intersect {1} && binsof(cp_wdata_rlb) intersect {0}
|
||||
iff (cs_registers_i.g_pmp_registers.any_pmp_entry_locked);
|
||||
}
|
||||
|
||||
mmwp_csr_cross : cross cp_mmwp, cp_wdata_mmwp
|
||||
iff (fcov_csr_write && cs_registers_i.csr_addr_i == CSR_MSECCFG) {
|
||||
bins sticky = binsof(cp_wdata_mmwp) intersect {0} && binsof(cp_mmwp) intersect {1};
|
||||
}
|
||||
|
||||
mml_sticky_cross : cross cp_mml, cp_wdata_mml
|
||||
iff (fcov_csr_write && cs_registers_i.csr_addr_i == CSR_MSECCFG) {
|
||||
bins sticky = binsof(cp_wdata_mml) intersect {0} && binsof(cp_mml) intersect {1};
|
||||
}
|
||||
|
||||
pmp_iside_nomatch_cross :
|
||||
cross cp_req_type_iside, cp_priv_lvl_iside, pmp_iside_req_err, cp_mmwp, cp_mml
|
||||
iff (pmp_iside_nomatch) {
|
||||
// Will never see a succesful exec access when execute is disallowed
|
||||
illegal_bins illegal_user_allow_exec =
|
||||
// In User mode - no match case, we should always deny
|
||||
(binsof(cp_priv_lvl_iside) intersect {PRIV_LVL_U} &&
|
||||
binsof(cp_req_type_iside) intersect {PMP_ACC_EXEC} &&
|
||||
binsof(pmp_iside_req_err) intersect {0});
|
||||
illegal_bins illegal_machine_allow_exec =
|
||||
// In Machine mode - no match case, we should deny always except MML=0 & MMWP=0
|
||||
(binsof(cp_priv_lvl_iside) intersect {PRIV_LVL_M} &&
|
||||
binsof(cp_req_type_iside) intersect {PMP_ACC_EXEC} &&
|
||||
(binsof(cp_mmwp) intersect {1} ||
|
||||
binsof(cp_mml) intersect {1}) &&
|
||||
binsof(pmp_iside_req_err) intersect {0});
|
||||
// Will never see an exec access denied when executed is ignored
|
||||
illegal_bins illegal_deny_exec =
|
||||
// Ignore Exec in MML=0, MMWP=0 and in Machine mode
|
||||
(binsof(cp_priv_lvl_iside) intersect {PRIV_LVL_M} &&
|
||||
binsof(cp_req_type_iside) intersect {PMP_ACC_EXEC} &&
|
||||
binsof(cp_mmwp) intersect {0} &&
|
||||
binsof(cp_mml) intersect {0} &&
|
||||
binsof(pmp_iside_req_err) intersect {1});
|
||||
}
|
||||
|
||||
pmp_iside2_nomatch_cross :
|
||||
cross cp_req_type_iside2, cp_priv_lvl_iside2, pmp_iside2_req_err, cp_mmwp, cp_mml
|
||||
iff (pmp_iside2_nomatch) {
|
||||
// Will never see a succesful exec access when execute is disallowed
|
||||
illegal_bins illegal_user_allow_exec =
|
||||
// In User mode - no match case, we should always deny
|
||||
(binsof(cp_priv_lvl_iside2) intersect {PRIV_LVL_U} &&
|
||||
binsof(cp_req_type_iside2) intersect {PMP_ACC_EXEC} &&
|
||||
binsof(pmp_iside2_req_err) intersect {0});
|
||||
illegal_bins illegal_machine_allow_exec =
|
||||
// In Machine mode - no match case, we should deny always except MML=0 & MMWP=0
|
||||
(binsof(cp_priv_lvl_iside2) intersect {PRIV_LVL_M} &&
|
||||
binsof(cp_req_type_iside2) intersect {PMP_ACC_EXEC} &&
|
||||
(binsof(cp_mmwp) intersect {1} ||
|
||||
binsof(cp_mml) intersect {1}) &&
|
||||
binsof(pmp_iside2_req_err) intersect {0});
|
||||
// Will never see an exec access denied when executed is ignored
|
||||
illegal_bins illegal_deny_exec =
|
||||
// Ignore Exec in MML=0, MMWP=0 and in Machine mode
|
||||
(binsof(cp_priv_lvl_iside2) intersect {PRIV_LVL_M} &&
|
||||
binsof(cp_req_type_iside2) intersect {PMP_ACC_EXEC} &&
|
||||
binsof(cp_mmwp) intersect {0} &&
|
||||
binsof(cp_mml) intersect {0} &&
|
||||
binsof(pmp_iside2_req_err) intersect {1});
|
||||
}
|
||||
|
||||
pmp_dside_nomatch_cross :
|
||||
cross cp_req_type_dside, cp_priv_lvl_dside, pmp_dside_req_err, cp_mmwp, cp_mml
|
||||
iff (pmp_dside_nomatch) {
|
||||
|
||||
// Will never see a succesful write/read access when it should be denied
|
||||
illegal_bins illegal_machine_allow_wr =
|
||||
// Deny WR when MMWP = 1 in Machine mode
|
||||
(binsof(cp_priv_lvl_dside) intersect {PRIV_LVL_M} &&
|
||||
binsof(cp_req_type_dside) intersect {PMP_ACC_READ, PMP_ACC_WRITE} &&
|
||||
binsof(cp_mmwp) intersect {1} &&
|
||||
binsof(pmp_dside_req_err) intersect {0});
|
||||
illegal_bins illegal_user_allow_wr =
|
||||
// Deny WR everytime in User mode
|
||||
(binsof(cp_priv_lvl_dside) intersect {PRIV_LVL_U} &&
|
||||
binsof(cp_req_type_dside) intersect {PMP_ACC_READ, PMP_ACC_WRITE} &&
|
||||
binsof(pmp_dside_req_err) intersect {0});
|
||||
|
||||
// Will never see a write/read access denied when write/read is ignored
|
||||
illegal_bins illegal_deny_wr =
|
||||
// Ignore WR when MMWP = 0 in Machine mode
|
||||
(binsof(cp_priv_lvl_dside) intersect {PRIV_LVL_M} &&
|
||||
binsof(cp_req_type_dside) intersect {PMP_ACC_READ, PMP_ACC_WRITE} &&
|
||||
binsof(cp_mmwp) intersect {0} &&
|
||||
binsof(pmp_dside_req_err) intersect {1});
|
||||
}
|
||||
|
||||
cp_pmp_iside_region_override :
|
||||
coverpoint g_pmp.pmp_i.g_access_check[PMP_I].fcov_pmp_region_override
|
||||
iff (if_stage_i.if_id_pipe_reg_we);
|
||||
|
@ -273,6 +602,15 @@ interface core_ibex_pmp_fcov_if import ibex_pkg::*; #(
|
|||
binsof(cs_registers_i.mstatus_q.mpp) intersect {PRIV_LVL_H, PRIV_LVL_S} ||
|
||||
binsof(cs_registers_i.priv_mode_id_o) intersect {PRIV_LVL_H, PRIV_LVL_S};
|
||||
}
|
||||
|
||||
pmp_instr_edge_cross: cross if_stage_i.instr_is_compressed_id_o,
|
||||
pmp_iside_req_err, pmp_iside2_req_err
|
||||
iff (pmp_iside_boundary_cross);
|
||||
|
||||
misaligned_lsu_access_cross: cross misaligned_pmp_err_last,
|
||||
load_store_unit_i.fcov_ls_mis_pmp_err_2
|
||||
iff (pmp_dside_boundary_cross);
|
||||
|
||||
endgroup
|
||||
|
||||
`DV_FCOV_INSTANTIATE_CG(pmp_top_cg, en_pmp_fcov)
|
||||
|
|
|
@ -561,6 +561,10 @@ module ibex_load_store_unit #(
|
|||
`DV_FCOV_SIGNAL(logic, ls_first_req, lsu_req_i & (ls_fsm_cs == IDLE))
|
||||
`DV_FCOV_SIGNAL(logic, ls_second_req,
|
||||
(ls_fsm_cs inside {WAIT_GNT, WAIT_RVALID_MIS}) & data_req_o & addr_incr_req_o)
|
||||
`DV_FCOV_SIGNAL(logic, ls_mis_pmp_err_1,
|
||||
(ls_fsm_cs inside {WAIT_RVALID_MIS, WAIT_GNT_MIS}) && pmp_err_q)
|
||||
`DV_FCOV_SIGNAL(logic, ls_mis_pmp_err_2,
|
||||
(ls_fsm_cs inside {WAIT_RVALID_MIS, WAIT_RVALID_MIS_GNTS_DONE}) && data_pmp_err_i)
|
||||
|
||||
////////////////
|
||||
// Assertions //
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue