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.

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

PMP Assert - Fix CEXes #1636

Merged

Conversation

silabs-robin
Copy link
Contributor

This PR fixes some CEXes in the PMP asserts, mostly related to the new DM_REGION_START/END.

Passes in formal.
Passes ci_check (except debug_test) BUT ONLY AFTER #1631 IS MERGED.

Signed-off-by: Robin Pedersen <Robin.Pedersen@silabs.com>
Signed-off-by: Robin Pedersen <Robin.Pedersen@silabs.com>
Signed-off-by: Robin Pedersen <Robin.Pedersen@silabs.com>
@@ -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.

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.

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


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.

.rvfi_valid (uvmt_cv32e40s_tb.dut_wrap.cv32e40s_wrapper_i.rvfi_i.rvfi_valid),
.rvfi_pc_rdata (uvmt_cv32e40s_tb.dut_wrap.cv32e40s_wrapper_i.rvfi_i.rvfi_pc_rdata),
u_pmp_assert_lsu(.rst_n (clknrst_if.reset_n),
.bus_trans_dbg (uvmt_cv32e40s_tb.dut_wrap.cv32e40s_wrapper_i.core_i.load_store_unit_i.mpu_i.bus_trans_o.dbg),
Copy link
Contributor Author

Choose a reason for hiding this comment

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

Note: This code trusts that the dbg value given to the MPU is correct in the core. Though, it should be verified by pmprvfi_assert when rvfi reports the "known" actual D-mode state and the PMP decisions are checked again.

@silabs-hfegran silabs-hfegran merged commit 63544ce into openhwgroup:cv32e40s/dev Feb 15, 2023
silabs-robin pushed a commit to silabs-robin/core-v-verif that referenced this pull request Mar 31, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants