Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

PMP Assert - Fix CEXes #1636

Merged
merged 3 commits into from
Feb 15, 2023
Merged

PMP Assert - Fix CEXes #1636

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
5028d3e
pmp_assert: correct formatting issue in pmp model
silabs-robin Feb 9, 2023
280fcec
pmp_assert: model dm pmp/pma override
silabs-robin Feb 9, 2023
fc7807b
pmp_assert: heed dm override in pmp properties
silabs-robin Feb 9, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
53 changes: 39 additions & 14 deletions cv32e40s/tb/uvmt/uvmt_cv32e40s_pmp_assert.sv
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,27 +1,48 @@
// Copyright 2022 Silicon Labs, Inc.
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Copyright header was missing.

//
// SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1
//
// Licensed under the Solderpad Hardware License v 2.1 (the "License"); you may
// not use this file except in compliance with the License, or, at your option,
// the Apache License version 2.0.
//
// You may obtain a copy of the License at
// https://solderpad.org/licenses/SHL-2.1/
//
// Unless required by applicable law or agreed to in writing, any work
// distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
// WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
//
// See the License for the specific language governing permissions and
// limitations under the License.


`default_nettype none


module uvmt_cv32e40s_pmp_assert
import uvm_pkg::*;
import cv32e40s_pkg::*;
import uvmt_cv32e40s_pkg::*;
#(
parameter int PMP_GRANULARITY = 0,
parameter int PMP_NUM_REGIONS = 0,
parameter int IS_INSTR_SIDE = 0,
parameter mseccfg_t MSECCFG_RESET_VAL = MSECCFG_DEFAULT
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Tying this to "default" was just wrong.

parameter int PMP_GRANULARITY,
parameter int PMP_NUM_REGIONS,
parameter int IS_INSTR_SIDE,
parameter mseccfg_t PMP_MSECCFG_RV
)
(
// Clock and Reset
input wire clk,
input wire rst_n,

// Interface to CSRs
// CSRs
input wire pmp_csr_t csr_pmp_i,

// Privilege mode
// Mode Info
input wire privlvl_t priv_lvl_i,
input wire bus_trans_dbg,

// Access checking
// Access Checking
input wire [33:0] pmp_req_addr_i,
input wire pmp_req_e pmp_req_type_i,
input wire pmp_req_err_o,
Expand Down Expand Up @@ -51,8 +72,11 @@ module uvmt_cv32e40s_pmp_assert
match_status_t match_status;
uvmt_cv32e40s_pmp_model #(
.PMP_GRANULARITY (PMP_GRANULARITY),
.PMP_NUM_REGIONS (PMP_NUM_REGIONS)
.PMP_NUM_REGIONS (PMP_NUM_REGIONS),
.DM_REGION_START (uvmt_cv32e40s_pkg::CORE_PARAM_DM_REGION_START),
.DM_REGION_END (uvmt_cv32e40s_pkg::CORE_PARAM_DM_REGION_END)
) model_i (
.debug_mode (bus_trans_dbg),
.match_status_o (match_status),
.*
);
Expand Down Expand Up @@ -387,7 +411,7 @@ module uvmt_cv32e40s_pmp_assert
// U-mode fails if no match (vplan:UmodeNomatch)
a_nomatch_umode_fails: assert property (
priv_lvl_i == PRIV_LVL_U && match_status.is_matched == 1'b0 |->
pmp_req_err_o
pmp_req_err_o ^ match_status.is_dm_override
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

DM can now override PMP/PMA: https://docs.openhwgroup.org/projects/cv32e40s-user-manual/en/latest/debug.html

) else `uvm_error(info_tag, "non-matched umode access must fail");

// M-mode fails if: no match, and "mseccfg.MMWP" (vplan:WhiteList:Denied)
Expand All @@ -396,28 +420,29 @@ module uvmt_cv32e40s_pmp_assert
!match_status.is_matched &&
csr_pmp_i.mseccfg.mmwp
|->
pmp_req_err_o
pmp_req_err_o ^ match_status.is_dm_override
) else `uvm_error(info_tag, "non-matched mmode access must fail when MMWP");

// U-mode or L=1 succeed only if RWX (vplan:RwxUmode)
a_uorl_onlyif_rwx: assert property (
//TODO:silabs-robin Why, 'L=1' in comment, but 'is_matched' in code?
( priv_lvl_i == PRIV_LVL_U || match_status.is_matched == 1'b1 ) && !pmp_req_err_o |->
match_status.is_rwx_ok
( priv_lvl_i == PRIV_LVL_U || match_status.is_matched == 1'b1 ) && !pmp_req_err_o
|->
match_status.is_rwx_ok || match_status.is_dm_override
) else `uvm_error(info_tag, "RWX must agree for allowing umode and L");

// After a match, LRWX determines access (vplan:LrwxDetermines)
a_lrwx_aftermatch: assert property (
//TODO:silabs-robin Why, "LRWX" in comment, but "rwx" in code?
match_status.is_matched == 1'b1 && !pmp_req_err_o |->
match_status.is_rwx_ok
match_status.is_rwx_ok || match_status.is_dm_override
) else `uvm_error(info_tag, "LRWX must agree for allowing matched access");

// SMEPMP 1: The reset value of mseccfg is implementation-specific, otherwise if backwards
// compatibility is a requirement it should reset to zero on hard reset.
// (vplan:MsecCfg:ResetValue)
a_mseccfg_reset_val: assert property (
$rose(rst_n) |-> csr_pmp_i.mseccfg === MSECCFG_RESET_VAL
$rose(rst_n) |-> csr_pmp_i.mseccfg === PMP_MSECCFG_RV
) else `uvm_error(info_tag, "mseccfg must be reset correctly");
end endgenerate

Expand Down
101 changes: 56 additions & 45 deletions cv32e40s/tb/uvmt/uvmt_cv32e40s_pmp_model.sv
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,26 +5,31 @@ module uvmt_cv32e40s_pmp_model
import uvm_pkg::*;
import uvmt_cv32e40s_pkg::*;
#(
parameter int PMP_GRANULARITY = 0,
parameter int PMP_NUM_REGIONS = 0
parameter int PMP_GRANULARITY,
parameter int PMP_NUM_REGIONS,
parameter logic [31:0] DM_REGION_START,
parameter logic [31:0] DM_REGION_END
)
(
// Clock and Reset
input wire clk,
input wire rst_n,

// Interface to CSRs
// CSRs
input wire pmp_csr_t csr_pmp_i,

// Privilege mode
// Privilege Mode
input wire privlvl_t priv_lvl_i,

// Access checking
// Access Checking
input wire [33:0] pmp_req_addr_i,
input wire pmp_req_e pmp_req_type_i,
input wire pmp_req_err_o,

//
// Debug Mode
input wire debug_mode,

// Match Status
output match_status_t match_status_o
);

Expand All @@ -39,10 +44,12 @@ module uvmt_cv32e40s_pmp_model
always_comb begin
match_status_o = {<<{'0}};

// Lock Detection
for (int region = 0; region < PMP_NUM_REGIONS; region++) begin
match_status_o.is_any_locked = csr_pmp_i.cfg[region].lock ? 1'b1 : match_status_o.is_any_locked;
end

// Match Detection
for (int i = 0; i < PMP_NUM_REGIONS; i++) begin
automatic logic [$clog2(PMP_MAX_REGIONS)-1:0] region = i;

Expand All @@ -53,6 +60,10 @@ module uvmt_cv32e40s_pmp_model
end
end

// Debug Module Override
match_status_o.is_dm_override =
debug_mode && ((DM_REGION_START <= pmp_req_addr_i) && (pmp_req_addr_i <= DM_REGION_END));

// Allowed access whitelist table
if (match_status_o.is_matched) begin
match_status_o.is_locked = csr_pmp_i.cfg[match_status_o.val_index].lock;
Expand Down Expand Up @@ -321,50 +332,52 @@ module uvmt_cv32e40s_pmp_model
end // PMP_ACC_EXEC
endcase // case(pmp_req_type_i)

end else begin // mmwp low
case ( priv_lvl_i )
PRIV_LVL_M:
case ( {pmp_req_type_i, match_status_o.is_locked} )
{ PMP_ACC_READ, 1'b1 }: match_status_o.val_access_allowed_reason.r_mmode_lr = csr_pmp_i.cfg[match_status_o.val_index].read;
{ PMP_ACC_READ, 1'b0 }: match_status_o.val_access_allowed_reason.r_mmode_r = 1'b1;
{ PMP_ACC_WRITE, 1'b1 }: match_status_o.val_access_allowed_reason.w_mmode_lw = csr_pmp_i.cfg[match_status_o.val_index].write;
{ PMP_ACC_WRITE, 1'b0 }: match_status_o.val_access_allowed_reason.w_mmode_w = 1'b1;
{ PMP_ACC_EXEC, 1'b1 }: match_status_o.val_access_allowed_reason.x_mmode_lx = csr_pmp_i.cfg[match_status_o.val_index].exec;
{ PMP_ACC_EXEC, 1'b0 }: match_status_o.val_access_allowed_reason.x_mmode_x = 1'b1;
endcase
PRIV_LVL_U:
case ( pmp_req_type_i )
PMP_ACC_READ: match_status_o.val_access_allowed_reason.r_umode_r = csr_pmp_i.cfg[match_status_o.val_index].read;
PMP_ACC_WRITE: match_status_o.val_access_allowed_reason.w_umode_w = csr_pmp_i.cfg[match_status_o.val_index].write;
PMP_ACC_EXEC: match_status_o.val_access_allowed_reason.x_umode_x = csr_pmp_i.cfg[match_status_o.val_index].exec;
endcase
endcase // case (priv_lvl_i)

end
match_status_o.is_rwx_ok = |match_status_o.val_access_allowed_reason;
end else begin // mmwp low
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This code was indented one level too much, so it was difficult to scroll up/down and see which if-stmt clause the execution was in.

case ( priv_lvl_i )
PRIV_LVL_M:
case ( {pmp_req_type_i, match_status_o.is_locked} )
{ PMP_ACC_READ, 1'b1 }: match_status_o.val_access_allowed_reason.r_mmode_lr = csr_pmp_i.cfg[match_status_o.val_index].read;
{ PMP_ACC_READ, 1'b0 }: match_status_o.val_access_allowed_reason.r_mmode_r = 1'b1;
{ PMP_ACC_WRITE, 1'b1 }: match_status_o.val_access_allowed_reason.w_mmode_lw = csr_pmp_i.cfg[match_status_o.val_index].write;
{ PMP_ACC_WRITE, 1'b0 }: match_status_o.val_access_allowed_reason.w_mmode_w = 1'b1;
{ PMP_ACC_EXEC, 1'b1 }: match_status_o.val_access_allowed_reason.x_mmode_lx = csr_pmp_i.cfg[match_status_o.val_index].exec;
{ PMP_ACC_EXEC, 1'b0 }: match_status_o.val_access_allowed_reason.x_mmode_x = 1'b1;
endcase
PRIV_LVL_U:
case ( pmp_req_type_i )
PMP_ACC_READ: match_status_o.val_access_allowed_reason.r_umode_r = csr_pmp_i.cfg[match_status_o.val_index].read;
PMP_ACC_WRITE: match_status_o.val_access_allowed_reason.w_umode_w = csr_pmp_i.cfg[match_status_o.val_index].write;
PMP_ACC_EXEC: match_status_o.val_access_allowed_reason.x_umode_x = csr_pmp_i.cfg[match_status_o.val_index].exec;
endcase
endcase // case (priv_lvl_i)

end else begin
// ------------------------------------------------------------
// NO MATCH REGION
// ------------------------------------------------------------
// No matching region found, allow only M-access, and only if MMWP bit is not set
case ( {pmp_req_type_i, priv_lvl_i} )
{ PMP_ACC_READ, PRIV_LVL_M }:
match_status_o.val_access_allowed_reason.r_mmode_nomatch_nommwp_r = !csr_pmp_i.mseccfg.mmwp;
{ PMP_ACC_WRITE, PRIV_LVL_M }:
match_status_o.val_access_allowed_reason.w_mmode_nomatch_nommwp_w = !csr_pmp_i.mseccfg.mmwp;
{ PMP_ACC_EXEC, PRIV_LVL_M }:
match_status_o.val_access_allowed_reason.x_mmode_nomatch_nommwp_x = !csr_pmp_i.mseccfg.mmwp && !csr_pmp_i.mseccfg.mml;
endcase
match_status_o.is_access_allowed_no_match = |match_status_o.val_access_allowed_reason;
end
// Access is allowed if any one of the above conditions matches
match_status_o.is_access_allowed = |match_status_o.val_access_allowed_reason;

match_status_o.is_rwx_ok = |match_status_o.val_access_allowed_reason;
end else begin
// ------------------------------------------------------------
// NO MATCH REGION
// ------------------------------------------------------------
// No matching region found, allow only M-access, and only if MMWP bit is not set
case ( {pmp_req_type_i, priv_lvl_i} )
{ PMP_ACC_READ, PRIV_LVL_M }:
match_status_o.val_access_allowed_reason.r_mmode_nomatch_nommwp_r = !csr_pmp_i.mseccfg.mmwp;
{ PMP_ACC_WRITE, PRIV_LVL_M }:
match_status_o.val_access_allowed_reason.w_mmode_nomatch_nommwp_w = !csr_pmp_i.mseccfg.mmwp;
{ PMP_ACC_EXEC, PRIV_LVL_M }:
match_status_o.val_access_allowed_reason.x_mmode_nomatch_nommwp_x = !csr_pmp_i.mseccfg.mmwp && !csr_pmp_i.mseccfg.mml;
endcase
match_status_o.is_access_allowed_no_match = |match_status_o.val_access_allowed_reason;
end

// Access is allowed if any one of the above conditions matches (or DM override)
match_status_o.is_access_allowed =
|match_status_o.val_access_allowed_reason || match_status_o.is_dm_override;
end


// Helper functions

function automatic int is_match_na4(input logic[$clog2(PMP_MAX_REGIONS)-1:0] region);
is_match_na4 = (csr_pmp_i.cfg[region].mode == PMP_MODE_NA4) &&
(csr_pmp_i.addr[region][33:2] == pmp_req_addr_i[33:2]);
Expand All @@ -380,7 +393,6 @@ module uvmt_cv32e40s_pmp_model
is_match_tor = (csr_pmp_i.cfg[region].mode == PMP_MODE_TOR) &&
(lo <= req) &&
(req < hi);

endfunction : is_match_tor

function automatic int is_match_napot(input logic[$clog2(PMP_MAX_REGIONS)-1:0] region);
Expand All @@ -390,7 +402,6 @@ module uvmt_cv32e40s_pmp_model

is_match_napot = (csr_pmp_i.cfg[region].mode == PMP_MODE_NAPOT) &&
(csr_addr_masked == req_addr_masked);

endfunction : is_match_napot

function automatic logic[31:0] gen_mask(input logic[$clog2(PMP_MAX_REGIONS)-1:0] i);
Expand Down
57 changes: 40 additions & 17 deletions cv32e40s/tb/uvmt/uvmt_cv32e40s_pmprvfi_assert.sv
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,10 @@ module uvmt_cv32e40s_pmprvfi_assert
input wire [31:0] rvfi_csr_mseccfgh_wdata,
input wire [31:0] rvfi_csr_mseccfgh_wmask,
//(mstatus)
input wire [31:0] rvfi_csr_mstatus_rdata
input wire [31:0] rvfi_csr_mstatus_rdata,

// Debug
input wire rvfi_dbg_mode
);


Expand Down Expand Up @@ -187,66 +190,86 @@ module uvmt_cv32e40s_pmprvfi_assert

uvmt_cv32e40s_pmp_model #(
.PMP_GRANULARITY (PMP_GRANULARITY),
.PMP_NUM_REGIONS (PMP_NUM_REGIONS)
.PMP_NUM_REGIONS (PMP_NUM_REGIONS),
.DM_REGION_START (uvmt_cv32e40s_pkg::CORE_PARAM_DM_REGION_START),
.DM_REGION_END (uvmt_cv32e40s_pkg::CORE_PARAM_DM_REGION_END)
) model_instr_i (
.clk (clk_i),
.rst_n (rst_ni),

.csr_pmp_i (pmp_csr_rvfi_rdata),
.priv_lvl_i (privlvl_t'(rvfi_mode)),
.debug_mode (rvfi_dbg_mode),
.pmp_req_addr_i ({2'b 00, rvfi_pc_rdata}),
.pmp_req_type_i (PMP_ACC_EXEC),
.pmp_req_err_o ('Z),
.pmp_req_type_i (PMP_ACC_EXEC),
.priv_lvl_i (privlvl_t'(rvfi_mode)),

.match_status_o (match_status_instr),

.match_status_o (match_status_instr)
.*
);

uvmt_cv32e40s_pmp_model #(
.PMP_GRANULARITY (PMP_GRANULARITY),
.PMP_NUM_REGIONS (PMP_NUM_REGIONS)
.PMP_NUM_REGIONS (PMP_NUM_REGIONS),
.DM_REGION_START (uvmt_cv32e40s_pkg::CORE_PARAM_DM_REGION_START),
.DM_REGION_END (uvmt_cv32e40s_pkg::CORE_PARAM_DM_REGION_END)
) model_data_i (
.clk (clk_i),
.rst_n (rst_ni),

.csr_pmp_i (pmp_csr_rvfi_rdata),
.priv_lvl_i (privlvl_t'(rvfi_effective_mode)),
.debug_mode (rvfi_dbg_mode),
.pmp_req_addr_i ({2'b 00, rvfi_mem_addr}), // TODO:silabs-robin Multi-op instructions
.pmp_req_type_i (rvfi_mem_wmask ? PMP_ACC_WRITE : PMP_ACC_READ), // TODO:silabs-robin Not completely accurate...
.pmp_req_err_o ('Z),
.pmp_req_type_i (rvfi_mem_wmask ? PMP_ACC_WRITE : PMP_ACC_READ), // TODO:silabs-robin Not completely accurate...
.priv_lvl_i (privlvl_t'(rvfi_effective_mode)),

.match_status_o (match_status_data),

.match_status_o (match_status_data)
.*
);

uvmt_cv32e40s_pmp_model #(
.PMP_GRANULARITY (PMP_GRANULARITY),
.PMP_NUM_REGIONS (PMP_NUM_REGIONS)
.PMP_NUM_REGIONS (PMP_NUM_REGIONS),
.DM_REGION_START (uvmt_cv32e40s_pkg::CORE_PARAM_DM_REGION_START),
.DM_REGION_END (uvmt_cv32e40s_pkg::CORE_PARAM_DM_REGION_END)
) model_upperinstr_i (
.clk (clk_i),
.rst_n (rst_ni),

.csr_pmp_i (pmp_csr_rvfi_rdata),
.priv_lvl_i (privlvl_t'(rvfi_mode)),
.debug_mode (rvfi_dbg_mode),
.pmp_req_addr_i ({2'b 00, rvfi_pc_upperrdata}),
.pmp_req_type_i (PMP_ACC_EXEC),
.pmp_req_err_o ('Z),
.pmp_req_type_i (PMP_ACC_EXEC),
.priv_lvl_i (privlvl_t'(rvfi_mode)),

.match_status_o (match_status_upperinstr),

.match_status_o (match_status_upperinstr)
.*
);

uvmt_cv32e40s_pmp_model #(
.PMP_GRANULARITY (PMP_GRANULARITY),
.PMP_NUM_REGIONS (PMP_NUM_REGIONS)
.PMP_NUM_REGIONS (PMP_NUM_REGIONS),
.DM_REGION_START (uvmt_cv32e40s_pkg::CORE_PARAM_DM_REGION_START),
.DM_REGION_END (uvmt_cv32e40s_pkg::CORE_PARAM_DM_REGION_END)
) model_upperdata_i (
.clk (clk_i),
.rst_n (rst_ni),

.csr_pmp_i (pmp_csr_rvfi_rdata),
.priv_lvl_i (privlvl_t'(rvfi_effective_mode)),
.debug_mode (rvfi_dbg_mode),
.pmp_req_addr_i ({2'b 00, rvfi_mem_upperaddr}), // TODO:silabs-robin Multi-op instructions
.pmp_req_type_i (rvfi_mem_wmask ? PMP_ACC_WRITE : PMP_ACC_READ), // TODO:silabs-robin Not completely accurate...
.pmp_req_err_o ('Z),
.pmp_req_type_i (rvfi_mem_wmask ? PMP_ACC_WRITE : PMP_ACC_READ), // TODO:silabs-robin Not completely accurate...
.priv_lvl_i (privlvl_t'(rvfi_effective_mode)),

.match_status_o (match_status_upperdata),

.match_status_o (match_status_upperdata)
.*
);

var [31:0] clk_cnt;
Expand Down
Loading