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

[ACT] Physical Memory Protection 64 #603

Open
wants to merge 15 commits into
base: dev
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
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: 23 additions & 30 deletions coverage/header_file.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -903,33 +903,26 @@ common:
RISCV_PGSIZE: (1 << RISCV_PGSHIFT)

PMP_MACROS:
PMPCFG_BIT_SET: 1
PMPCFG_BIT_NOT_SET: 0
PMPCFG_ONLY_R_SET: 0x01
PMPCFG_ONLY_X_SET: 0x04
PMPCFG_ONLY_RW_SET: 0x03
PMPCFG_ONLY_RX_SET: 0x05
PMPCFG_ONLY_RWX_SET: 0x07
PMPCFG_OFF_MODE: 0x00
PMPCFG_TOR_MODE: 0x08
PMPCFG_NA4_MODE: 0x10
PMPCFG_NAPOT_MODE: 0x18
PMPCFG_R_BIT: 0x01
PMPCFG_W_BIT: 0x02
PMPCFG_X_BIT: 0x04
PMPCFG_RWX_BIT: 0x07
PMPCFG_A_BIT: 0x18
PMPCFG_RW_BIT: 0x60
PMPCFG_L_BIT: 0x80
PMPCFG_ALL_BIT: 0xFF

PMP_helper_Coverpoints:
NAPOT_REGION_ADDRESS_MATCH: ((rs1_val + imm_val) ^ (pmpaddr1<<2)) & ~(((pmpaddr1 ^ (pmpaddr1+1))<<2) | 3) ==0 and ((rs1_val+imm_val+access_len-1 ) ^ (pmpaddr1<<2)) & ~(((pmpaddr1 ^ (pmpaddr1+1))<<2) | 3) ==0
NAPOT_PRIORITY_REGION_MATCH: ((rs1_val + imm_val) ^ (pmpaddr3<<2)) & ~(((pmpaddr3 ^ (pmpaddr3+1))<<2) | 3) ==0 and ((rs1_val+imm_val+access_len-1 ) ^ (pmpaddr3<<2)) & ~(((pmpaddr3 ^ (pmpaddr3+1))<<2) | 3) ==0
NAPOT_PRIORITY_2_REGION_MATCH: ((rs1_val + imm_val) ^ (pmpaddr1<<2)) & ~(((pmpaddr1 ^ (pmpaddr1+1))<<2) | 3) ==0 and ((rs1_val+imm_val+access_len-1 ) ^ (pmpaddr1<<2)) & ~(((pmpaddr1 ^ (pmpaddr1+1))<<2) | 3) ==0
TOR_REGION_ADDRESS_MATCH: (rs1_val + imm_val >= (pmpaddr1 << 2)) and (rs1_val + imm_val < (pmpaddr2 << 2))
TOR_PRIORITY_REGION_MATCH: (rs1_val + imm_val >= (pmpaddr2 << 2)) and (rs1_val + imm_val < (pmpaddr3 << 2))
TOR_PRIORITY_2_REGION_MATCH: (rs1_val + imm_val >= (pmpaddr0 << 2)) and (rs1_val + imm_val < (pmpaddr1 << 2))
NA4_REGION_ADDRESS_MATCH: (rs1_val + imm_val == (pmpaddr1 << 2))
NA4_PRIORITY_REGION_MATCH: (rs1_val + imm_val == (pmpaddr3 << 2))
NA4_PRIORITY_2_REGION_MATCH: (rs1_val + imm_val == (pmpaddr1 << 2))
PMP0_CFG_SHIFT: 0
PMP1_CFG_SHIFT: 8
PMP2_CFG_SHIFT: 16
PMP3_CFG_SHIFT: 24
PMP4_CFG_SHIFT: 32
PMP5_CFG_SHIFT: 40
PMP6_CFG_SHIFT: 48
PMP7_CFG_SHIFT: 56
PMP_CFG_LOCK: 0x80
PMP_CFG_RWX: 0x07
PMP_CFG_RX: 0x05
PMP_CFG_RW: 0x03
PMP_CFG_R: 0x01
PMP_CFG_X: 0x04
PMP_CFG_LRWX: 0x87
PMP_CFG_LRX: 0x85
PMP_CFG_LRW: 0x83
PMP_CFG_LR: 0x81
PMP_CFG_LX: 0x84
PMP_CFG_TOR: 0x08
PMP_CFG_NA4: 0x10
PMP_CFG_NAPOT: 0x18
PMPCFG_ALL_BIT: 0xFF
File renamed without changes.
211 changes: 211 additions & 0 deletions coverage/pmp/rv64_pmp.cgf
Original file line number Diff line number Diff line change
@@ -0,0 +1,211 @@
PMP_NAPOT_M:
config:
- check ISA:=regex(.*64.*); check ISA:=regex(.*I.*Zicsr.*); def rvtest_mtrap_routine=True;
mnemonics:
"{csrrw, ld, sd, lw, sw, lb, sb, lh, sh, jal, jalr}" : 0
csr_comb:
#All 5 cases checked here.
#checks for required permissions.
((pmpcfg2 >> {40, 32, 24, 16, 8}) & 0xFF == {${PMP_CFG_LRWX}, ${PMP_CFG_LRX}, ${PMP_CFG_LRW}, ${PMP_CFG_LR}, ${PMP_CFG_LX}}{[$1]} | ${PMP_CFG_NAPOT}): 0
val_comb:
#check the lb..ld, sb..sd accessed the address which was inside the TEST_FOR_EXECUTION PMP region atleast once and at that time the pmpaddr with NAPOT region selected.
? (mnemonic == {"ld", "lw", "lh", "lb", "sd", "sw", "sh", "sb"}) and
pmp_rgn_chk(rs1_val | imm_val, access_len, "NAPOT", (pmpaddr{13,12,11,10,9})) and
((pmpcfg2 >> {40, 32, 24, 16, 8}{[$2]}) & 0xFF == {${PMP_CFG_LRWX}, ${PMP_CFG_LRX}, ${PMP_CFG_LRW}, ${PMP_CFG_LR}, ${PMP_CFG_LX}}{[$2]} | ${PMP_CFG_NAPOT})
: 0
#checks for the faults.
#check for store access faults
? (mnemonic == {"sd", "sw", "sh", "sb"}) and
((pmpcfg2 >> {32, 16, 8}) & 0xFF == {${PMP_CFG_LRX}, ${PMP_CFG_LR}, ${PMP_CFG_LX}}{[$2]} | ${PMP_CFG_NAPOT}) and
mcause == ${CAUSE_STORE_ACCESS}
: 0

#check for Load access faults
? (mnemonic == {"ld", "lw", "lh", "lb"}) and
((pmpcfg2 >> 8) & 0xFF == ${PMP_CFG_LX} | ${PMP_CFG_NAPOT}) and
mcause == ${CAUSE_LOAD_ACCESS}
: 0

#check for Fetch access faults
? ((pmpcfg2 >> {24, 16}) & 0xFF == {${PMP_CFG_LRW}, ${PMP_CFG_LR}}{[$1]} | ${PMP_CFG_NAPOT}) and
mcause == ${CAUSE_FETCH_ACCESS}
: 0

PMP_NA4_M:
config:
- check ISA:=regex(.*64.*); check ISA:=regex(.*I.*Zicsr.*); def rvtest_mtrap_routine=True;
mnemonics:
"{ld, sd, lw, sw, lb, sb, lh, sh, jal, jalr}" : 0
csr_comb:
#All 5 cases checked here.
#checks for required permissions.
((pmpcfg2 >> {40, 32, 24, 16, 8}) & 0xFF == {${PMP_CFG_LRWX}, ${PMP_CFG_LRX}, ${PMP_CFG_LRW}, ${PMP_CFG_LR}, ${PMP_CFG_LX}}{[$1]} | ${PMP_CFG_NA4}): 0
val_comb:
#check the lb..ld, sb..sd accessed the address which was inside the TEST_FOR_EXECUTION PMP region atleast once and at that time the pmpaddr with NA4 region selected.
? (mnemonic == {"ld", "lw", "lh", "lb", "sd", "sw", "sh", "sb"}) and
pmp_rgn_chk(rs1_val | imm_val, access_len, "NA4", (pmpaddr{13,12,11,10,9})) and
((pmpcfg2 >> {40, 32, 24, 16, 8}{[$2]}) & 0xFF == {${PMP_CFG_LRWX}, ${PMP_CFG_LRX}, ${PMP_CFG_LRW}, ${PMP_CFG_LR}, ${PMP_CFG_LX}}{[$2]} | ${PMP_CFG_NA4})
: 0
#checks for the faults.
#check for store access faults
? (mnemonic == {"sd", "sw", "sh", "sb"}) and
((pmpcfg2 >> {32, 16, 8}) & 0xFF == {${PMP_CFG_LRX}, ${PMP_CFG_LR}, ${PMP_CFG_LX}}{[$2]} | ${PMP_CFG_NA4}) and
mcause == ${CAUSE_STORE_ACCESS}
: 0

#check for Load access faults
? (mnemonic == {"ld", "lw", "lh", "lb"}) and
((pmpcfg2 >> 8) & 0xFF == ${PMP_CFG_LX} | ${PMP_CFG_NA4}) and
mcause == ${CAUSE_LOAD_ACCESS}
: 0

#check for Fetch access faults
? ((pmpcfg2 >> {24, 16}) & 0xFF == {${PMP_CFG_LRW}, ${PMP_CFG_LR}}{[$1]} | ${PMP_CFG_NA4}) and
mcause == ${CAUSE_FETCH_ACCESS}
: 0

PMP_TOR_M:
config:
- check ISA:=regex(.*64.*); check ISA:=regex(.*I.*Zicsr.*); def rvtest_mtrap_routine=True;
mnemonics:
"{ld, sd, lw, sw, lb, sb, lh, sh, jal, jalr}" : 0
csr_comb:
#All 5 cases checked here.
#checks for required permissions.
((pmpcfg2 >> {40, 24, 8}) & 0xFF == {${PMP_CFG_LRWX}, ${PMP_CFG_LRX}, ${PMP_CFG_LRW}}{[$1]} | ${PMP_CFG_TOR}): 0
((pmpcfg0 >> {56, 40}) & 0xFF == {${PMP_CFG_LR}, ${PMP_CFG_LX}}{[$1]} | ${PMP_CFG_TOR}): 0
val_comb:
? (mnemonic == {"ld", "lw", "lh", "lb", "sd", "sw", "sh", "sb"}) and
pmp_rgn_chk(rs1_val | imm_val, access_len, "TOR", (pmpaddr{13,11,9}), (pmpaddr{12, 10, 8}{[$2]})) and
((pmpcfg2 >> {40, 24, 8}{[$2]}) & 0xFF == {${PMP_CFG_LRWX}, ${PMP_CFG_LRX}, ${PMP_CFG_LRW}}{[$2]} | ${PMP_CFG_TOR})
: 0

? (mnemonic == {"ld", "lw", "lh", "lb", "sd", "sw", "sh", "sb"}) and
pmp_rgn_chk(rs1_val | imm_val, access_len, "TOR", (pmpaddr{7, 5}), (pmpaddr{6, 4}{[$2]})) and
((pmpcfg0 >> {56, 40}{[$2]}) & 0xFF == {${PMP_CFG_LR}, ${PMP_CFG_LX}}{[$2]} | ${PMP_CFG_TOR})
: 0
#checks for the faults.
#check for store access faults
? (mnemonic == {"sd", "sw", "sh", "sb"}) and
((pmpcfg2 >> {40, 24, 8}) & 0xFF == {${PMP_CFG_LRWX}, ${PMP_CFG_LRX}, ${PMP_CFG_LRW}}{[$2]} | ${PMP_CFG_TOR}) and
mcause == ${CAUSE_STORE_ACCESS}
: 0

? (mnemonic == {"sd", "sw", "sh", "sb"}) and
((pmpcfg0 >> {56, 40}) & 0xFF == {${PMP_CFG_LR}, ${PMP_CFG_LX}}{[$2]} | ${PMP_CFG_TOR}) and
mcause == ${CAUSE_STORE_ACCESS}
: 0

#check for store access faults
? (mnemonic == {"ld", "lw", "lh", "lb"}) and
((pmpcfg0 >> 40) & 0xFF == ${PMP_CFG_LX} | ${PMP_CFG_TOR}) and
mcause == ${CAUSE_LOAD_ACCESS}
: 0

#check for Fetch access faults
? ((pmpcfg2 >> 8) & 0xFF == ${PMP_CFG_LRW} | ${PMP_CFG_TOR}) and
mcause == ${CAUSE_FETCH_ACCESS}
: 0

? ((pmpcfg0 >> 56) & 0xFF == ${PMP_CFG_LR} | ${PMP_CFG_TOR}) and
mcause == ${CAUSE_FETCH_ACCESS}
: 0

PMP_TOR_S_U:
config:
- check ISA:=regex(.*64.*); check ISA:=regex(.*I.*Zicsr.*); def rvtest_mtrap_routine=True;
mnemonics:
"{ld, sd, lw, sw, lb, sb, lh, sh, jal, jalr}" : 0
csr_comb:
#All 5 cases checked here.
#checks for required permissions.
(mode == {'S', 'U'}) and ((pmpcfg0 >> ${PMP1_CFG_SHIFT}) & 0xFF == {${PMP_CFG_RWX}, ${PMP_CFG_RX}, ${PMP_CFG_RW}, ${PMP_CFG_R}, ${PMP_CFG_X}} | ${PMP_CFG_TOR}): 0
val_comb:
? (mode == {'S', 'U'}) and (mnemonic == {"ld", "lw", "lh", "lb", "sd", "sw", "sh", "sb"}) and
pmp_rgn_chk(rs1_val | imm_val, access_len, "TOR", (pmpaddr1), (pmpaddr0)) and
((pmpcfg0 >> ${PMP1_CFG_SHIFT}) & 0xFF == {${PMP_CFG_RWX}, ${PMP_CFG_RX}, ${PMP_CFG_RW}, ${PMP_CFG_R}, ${PMP_CFG_X}} | ${PMP_CFG_TOR})
: 0

# #checks for the faults.
# #check for store access faults
? (mode == {'S', 'U'}) and (mnemonic == {"sd", "sw", "sh", "sb"}) and
((pmpcfg0 >> ${PMP1_CFG_SHIFT}) & 0xFF == {${PMP_CFG_RX}, ${PMP_CFG_R}, ${PMP_CFG_X}} | ${PMP_CFG_TOR}) and
mcause == ${CAUSE_STORE_ACCESS}
: 0

#check for load access faults
? (mode == {'S', 'U'}) and (mnemonic == {"ld", "lw", "lh", "lb"}) and
((pmpcfg0 >> ${PMP1_CFG_SHIFT}) & 0xFF == ${PMP_CFG_X} | ${PMP_CFG_TOR}) and
mcause == ${CAUSE_LOAD_ACCESS}
: 0

#check for fetch access faults
? ((pmpcfg0 >> ${PMP1_CFG_SHIFT}) & 0xFF == {${PMP_CFG_RW},${PMP_CFG_R}} | ${PMP_CFG_TOR}) and
mcause == ${CAUSE_FETCH_ACCESS}
: 0

PMP_NAPOT_S_U:
config:
- check ISA:=regex(.*64.*); check ISA:=regex(.*I.*Zicsr.*); def rvtest_mtrap_routine=True;
mnemonics:
"{csrrw, ld, sd, lw, sw, lb, sb, lh, sh, jal, jalr}" : 0
csr_comb:
#All 5 cases checked here.
#checks for required permissions.
((pmpcfg0 >> ${PMP0_CFG_SHIFT}) & 0xFF == {${PMP_CFG_RWX}, ${PMP_CFG_RX}, ${PMP_CFG_RW}, ${PMP_CFG_R}, ${PMP_CFG_X}} | ${PMP_CFG_NAPOT}): 0
val_comb:
#check the lb..ld, sb..sd accessed the address which was inside the TEST_FOR_EXECUTION PMP region atleast once and at that time the pmpaddr with NAPOT region selected.
? (mode == {'S', 'U'}) and (mnemonic == {"ld", "lw", "lh", "lb", "sd", "sw", "sh", "sb"}) and
pmp_rgn_chk(rs1_val | imm_val, access_len, "NAPOT", (pmpaddr0)) and
((pmpcfg0 >> ${PMP0_CFG_SHIFT}) & 0xFF == {${PMP_CFG_RWX}, ${PMP_CFG_RX}, ${PMP_CFG_RW}, ${PMP_CFG_R}, ${PMP_CFG_X}} | ${PMP_CFG_NAPOT})
: 0
#checks for the faults.
#check for store access faults
? (mode == {'S', 'U'}) and (mnemonic == {"sd", "sw", "sh", "sb"}) and
((pmpcfg0 >> ${PMP0_CFG_SHIFT}) & 0xFF == {${PMP_CFG_RX}, ${PMP_CFG_R}, ${PMP_CFG_X}} | ${PMP_CFG_NAPOT}) and
mcause == ${CAUSE_STORE_ACCESS}
: 0

#check for Load access faults
? (mode == {'S', 'U'}) and (mnemonic == {"ld", "lw", "lh", "lb"}) and
((pmpcfg0 >> ${PMP0_CFG_SHIFT}) & 0xFF == ${PMP_CFG_X} | ${PMP_CFG_NAPOT}) and
mcause == ${CAUSE_LOAD_ACCESS}
: 0

#check for Fetch access faults
? ((pmpcfg0 >> ${PMP0_CFG_SHIFT}) & 0xFF == {${PMP_CFG_RW}, ${PMP_CFG_R}} | ${PMP_CFG_NAPOT}) and
mcause == ${CAUSE_FETCH_ACCESS}
: 0

PMP_NA4_S_U:
config:
- check ISA:=regex(.*64.*); check ISA:=regex(.*I.*Zicsr.*); def rvtest_mtrap_routine=True;
mnemonics:
"{ld, sd, lw, sw, lb, sb, lh, sh, jal, jalr}" : 0
csr_comb:
#All 5 cases checked here.
#checks for required permissions.
(mode == {'S', 'U'}) and ((pmpcfg0 >> ${PMP0_CFG_SHIFT}) & 0xFF == {${PMP_CFG_RWX}, ${PMP_CFG_RX}, ${PMP_CFG_RW}, ${PMP_CFG_R}, ${PMP_CFG_X}} | ${PMP_CFG_NA4}): 0
val_comb:
#check the lb..ld, sb..sd accessed the address which was inside the TEST_FOR_EXECUTION PMP region atleast once and at that time the pmpaddr with NAPOT region selected.
? (mode == {'S', 'U'}) and (mnemonic == {"ld", "lw", "lh", "lb", "sd", "sw", "sh", "sb"}) and
pmp_rgn_chk(rs1_val | imm_val, access_len, "NAPOT", (pmpaddr0)) and
((pmpcfg0 >> ${PMP0_CFG_SHIFT}) & 0xFF == {${PMP_CFG_RWX}, ${PMP_CFG_RX}, ${PMP_CFG_RW}, ${PMP_CFG_R}, ${PMP_CFG_X}} | ${PMP_CFG_NA4})
: 0
#checks for the faults.
#check for store access faults
? (mode == {'S', 'U'}) and (mnemonic == {"sd", "sw", "sh", "sb"}) and
((pmpcfg0 >> ${PMP0_CFG_SHIFT}) & 0xFF == {${PMP_CFG_RX}, ${PMP_CFG_R}, ${PMP_CFG_X}} | ${PMP_CFG_NA4}) and
mcause == ${CAUSE_STORE_ACCESS}
: 0

#check for Load access faults
? (mode == {'S', 'U'}) and (mnemonic == {"ld", "lw", "lh", "lb"}) and
((pmpcfg0 >> ${PMP0_CFG_SHIFT}) & 0xFF == ${PMP_CFG_X} | ${PMP_CFG_NA4}) and
mcause == ${CAUSE_LOAD_ACCESS}
: 0

#check for Fetch access faults
? ((pmpcfg0 >> ${PMP0_CFG_SHIFT}) & 0xFF == {${PMP_CFG_RW}, ${PMP_CFG_R}} | ${PMP_CFG_NA4}) and
mcause == ${CAUSE_FETCH_ACCESS}
: 0
Loading
Loading