diff --git a/sample_cgfs/dataset.cgf b/sample_cgfs/dataset.cgf index bf0f52e4..8a28d257 100644 --- a/sample_cgfs/dataset.cgf +++ b/sample_cgfs/dataset.cgf @@ -286,6 +286,7 @@ datasets: 'rs1_val > 0 and rs2_val < 0': 0 'rs1_val < 0 and rs2_val < 0': 0 'rs1_val < 0 and rs2_val > 0': 0 + 'rs1_val == -0x8000000000000000 and rs2_val == -0x01': 0 'rs1_val == rs2_val': 0 'rs1_val != rs2_val': 0 diff --git a/sample_cgfs/rv32i_priv.cgf b/sample_cgfs/rv32i_priv.cgf index 320dbda2..0b83cdfa 100644 --- a/sample_cgfs/rv32i_priv.cgf +++ b/sample_cgfs/rv32i_priv.cgf @@ -156,3 +156,799 @@ misalign-beq: ' rs1_val==rs2_val and ea_align == 2': 0 +####################################################################################################################################################################################################### +# These coverpoints belongs to the test plan for RISC-V Privilege Arch Compliance developed by 10xEngineers +####################################################################################################################################################################################################### + +######## misa ##################################################################################################################################################################################################### + +misa: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*F.*D.*Zicsr.*); check is_implemented(misa) = True; check is_legal_warl(misa, 0x28, 0x28) = True; + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + ((write_val(misa) & 0x20) == 0) && ((old_val(misa) & 0x28) == 0x28) && ((misa & 0x28) == 0) # checking if the misa register has the correct ISA extensions enabled by checking if bits 5 and 3 are set, and if bits 5 and 3 were previously set before the write to the misa register. + + +misa_mxl_check_32: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); check is_implemented(misa) = True; + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + misa >> (xlen-2) == 0x01 : 0 # checks whether the mxl field of misa register is 1. + + +misa_mxl_check_64: + config: + - check ISA:=regex(.*64.*); check ISA:=regex(.*I.*Zicsr.*); check is_implemented(misa) = True; + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + misa >> (xlen-2) == 0x02 : 0 # checks whether the mxl field of misa register is 2. + + +misa_mxl_check_128: + config: + - check ISA:=regex(.*128.*); check ISA:=regex(.*I.*Zicsr.*); check is_implemented(misa) = True; + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + misa >> (xlen-2) == 0x03 : 0 # checks whether the mxl field of misa register is 3. + + +misa_Umode: + config: + - check ISA:=regex(.*I.*Zicsr.*U.*); check is_implemented(misa) = True; + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + (misa >> 20) & 0x01 == 0x01 : 0 # checking if U bit gets set if there is support for user mode RV32 + + +misa_Smode: + config: + - check ISA:=regex(.*I.*Zicsr.*S.*); check is_implemented(misa) = True; + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + (misa >> 18) & 0x01 == 0x01 : 0 # checking if S bit gets set if there is support for supervisor mode RV32 + +######## mcause ##################################################################################################################################################################################################### + +mcause: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); check is_implemented_software(mcause) = True; + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + is_trap == True and (mcause >> 31) & 1 == 1 : 0 # checks if the exception or interrupt was an interrupt + is_trap == True and (mcause >> 31) & 1 == 0 : 0 # checks if the exception or interrupt was an exception + is_trap == True and (mcause >> 31) & 1 == 0 && (mcause & 0xff) == 8'h01 : 0 # Instruction access fault exception + is_trap == True and (mcause >> 31) & 1 == 0 && (mcause & 0xff) == 8'h02 : 0 # Illegal instruction exception + is_trap == True and (mcause >> 31) & 1 == 0 && (mcause & 0xff) == 8'h03 : 0 # Breakpoint exception + is_trap == True and (mcause >> 31) & 1 == 0 && (mcause & 0xff) == 8'h04 : 0 # Load address misaligned exception + is_trap == True and (mcause >> 31) & 1 == 0 && (mcause & 0xff) == 8'h05 : 0 # Load access fault exception + is_trap == True and (mcause >> 31) & 1 == 0 && (mcause & 0xff) == 8'h06 : 0 # Store/AMO address misaligned exception + is_trap == True and (mcause >> 31) & 1 == 0 && (mcause & 0xff) == 8'h07 : 0 # Store/AMO access fault exception + is_trap == True and (mcause >> 31) & 1 == 0 && (mcause & 0xff) == 8'h0b : 0 # Environment call from M-mode exception + is_trap == True and (mcause >> 31) & 1 == 1 && (mcause & 0xff) == 8'h03 : 0 # Machine software interrupt + is_trap == True and (mcause >> 31) & 1 == 1 && (mcause & 0xff) == 8'h07 : 0 # Machine timer interrupt + is_trap == True and (mcause >> 31) & 1 == 1 && (mcause & 0xff) == 8'h0b : 0 # Machine external interrupt + + +mcause_PageFault: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*S.*U.*); check satp.mode != "bare"; # checks if the satp.mode field, which determines the paging scheme, is implemented in software + mnemonics: + csrrs: 0 + csr_comb: + (mcause & 0xff) == 0x0c && mcause[31] == 0 && is_trap == True : 0 # checks for page fault caused by a data access + (mcause & 0xff) == 0x0d && mcause[31] == 0 && is_trap == True : 0 # checks for page table fault caused by a data access + (mcause & 0xff) == 0x0f && mcause[31] == 0 && is_trap == True : 0 # checks for page access fault caused by a data access + + +mcause_InstAddr_MissAligned: # This coverpoint checks for the instruction address misaligned exception and verifies that it does not occur when the C extension is present and enabled. + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*C.*Zicsr.*); check mstatus.MPRV == 0; # Check that C extension is present and enabled, and that MPRV is 0 + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + is_trap == True & (mcause >> 31) & 1 == 0 & (mcause & 0x7f) == 0b0000011: 0 # Verify that the instruction address misaligned exception does not occur when the C extension is present and enabled. Note that we are checking the 7 least significant bits of the mcause register to capture all possible exception codes for instruction address misaligned exceptions. + + +mcause_Smode: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*S.*); check is_implemented_software(mcause) = True; + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + (mcause >> 31) & 1 == 1 && (mcause & 0xff) == 8'h01 : 0 # Supervisor software interrupt + (mcause >> 31) & 1 == 1 && (mcause & 0xff) == 8'h05 : 0 # Supervisor timer interrupt + (mcause >> 31) & 1 == 1 && (mcause & 0xff) == 8'h09 : 0 # Supervisor external interrupt + (mcause >> 31) & 1 == 0 && (mcause & 0xff) == 8'h09 : 0 # Environment call from S-mode exception + + +mcause_Umode: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*U.*); check is_implemented_software(mcause) = True; + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + (mcause >> 31) & 1 == 0 && (mcause & 0xff) == 8'h08 : 0 # Environment call from U-mode exception + +######## mstatus ##################################################################################################################################################################################################### + +mstatus: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + (mstatus >> 3) & 0x01 == 0x01 : 0 # checking if the MIE gets enabled + (mstatus >> 7) & 0x01 == 0x01 : 0 # MPIE holds the value of the interrupt-enable bit active prior to the trap, checking whether it does that or not + (mstatus >> 21) & 0x1 == 0x00 : 0 # TW is set to 0 when there are no privilege levels below M. + + +mstatus_Smode: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*S.*); + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + (mstatus >> 1) & 0x01 == 0x01 : 0 # Check that the SIE bit is set to 1 when the processor is in supervisor mode + (mstatus >> 5) & 0x01 == 0x01 : 0 # Check that the SPIE bit is set to 1 when interrupts are enabled in supervisor mode and that it is set to 0 when interrupts are disabled in supervisor mode + (mstatus >> 8) & 0x01 == 0x01 : 0 # checks SPP bit + (mstatus >> 22) & 0x1 == 0x01 : 0 # When TSR=1, attempts to execute SRET while executing in S-mode will raise an illegal instruction exception. + (mstatus >> 20) & 0x1 == 0x01 : 0 # TVM=1, illegal instruction exception in S-mode + (mstatus >> 20) & 0x1 == 0x00 : 0 # TVM=0, permitted in S-mode + (mstatus >> 21) & 0x1 == 0x01 : 0 # When TW=1 and WFI is executed in a lower-privileged mode, it causes an illegal instruction exception if not completed within a bounded time limit, which may be 0 + (mstatus >> 19) & 0x1 == 0x01 : 0 # When MXR is set to 1, memory pages that are either marked as readable (R=1) or executable (X=1) can be loaded successfully. + (mstatus >> 19) & 0x1 == 0x00 : 0 # When MXR is set to 0, only loading data from pages that are marked as readable (with R=1) will be successful. + (mstatus >> 18) & 0x1 == 0x00 : 0 # SUM=0, S-mode memory accesses to pages accessible by U-mode will fault + (mstatus >> 18) & 0x1 == 0x01 : 0 # SUM=1, these accesses to pages accessible by U-mode are permitted + + +mstatus_MPRV: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*S.*); check satp.mode != "bare"; check is_implemented_software(mstatus) = True; check is_writable(mstatus.MPRV) = True; + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + (mstatus >> 17) & 0x1 == 1 & (mstatus.MPP != 3) : 0 + + +mstatus_MtoM: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + is_trap == True & (mstatus >> 11) & 0x3 == 0x3 : 0 # M-mode to M-mode transition + + +mstatus_StoM: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*S.*); + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + csrrw: 0 + is_trap == True & ((mstatus >> 11) & 0x1) == 0x0 & ((mstatus >> 10) & 0x3) == 0x3 : 0 # S-mode to M-mode transition + + +mstatus_UtoM: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*U.*); + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + is_trap == True & ((mstatus >> 11) & 0x1) == 0x1 & ((mstatus >> 10) & 0x3) == 0x3 & ((mstatus >> 2) & 0x3) == 0x0 : 0 # U-mode to M-mode transition + + +mstatus_MtoS: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*S.*); + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + is_trap == True & (mstatus >> 10) & 0x3 == 0x1 : 0 # M-mode to S-mode transition + + +mstatus_StoS: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*S.*); + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + is_trap == True & (mstatus >> 10) & 0x3 == 0x1 & (mstatus >> 11) & 0x1 == 0x0 & (mstatus >> 8) & 0x1 == 0x0 : 0 # S-mode to S-mode transition + + +mstatus_UtoS: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*U.*S.*); check is_trap = True; + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + is_trap == True & (mstatus >> 10) & 0x3 == 0x1 & (mstatus >> 11) & 0x1 == 0x1 : 0 # U-mode to S-mode transition + + +mstatus_MtoU: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*U.*); check is_trap = True; + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + is_trap == True & (mstatus >> 10) & 0x3 == 0x0 : 0 # M-mode to U-mode transition + + +mstatush: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); + mnemonics: + csrrw: 0 + csrrs: 0 +csr_comb: + (mstatush >> 5) & 0x1 == 0x01 : 0 # checks if machine-mode byte enable (MBE) is set to enabled. If this bit is set to 1, the coverpoint will evaluate to 0, indicating that MBE is enabled + + +mstatus_little-endian: + config: + - check ISA:=regex(.*64.*); check ISA:=regex(.*I.*Zicsr.*); + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + (mstatush >> 5) & (mstatus >> 4) & (mstatus >> 6) == 0 : 0 # checks if all three of these bits are set to 0, indicating that MBE, SBE, and UBE are all disabled. When these bits are all disabled, the processor is in little-endian mode, and accesses made to memory will be little-endian. + + +mstatus_big_endian: + config: + - check ISA:=regex(.*64.*); check ISA:=regex(.*I.*Zicsr.*S.*); check big_endian_support=True; + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + (mstatus >> 37) & 0x1 == 0x01 : 0 # checks the sixth least significant bit of the upper 32 bits of the mstatus register to ensure that machine-mode byte enable (MBE) is set to enabled. If this bit is set to 1, the coverpoint will evaluate to 0, indicating that MBE is enabled + + +mstatus_big_endian_Smode: + config: + - check ISA:=regex(.*64.*); check ISA:=regex(.*I.*Zicsr.*S.*); check big_endian_support=True; + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + (mstatush >> 4) & 0x1 == 0x01 : 0 # ensures that certain instructions or operations are only executed when the processor is in supervisor mode and in big-endian mode + + +mstatus_big_endian__Umode: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*U.*); check big_endian_support=True; + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + (mstatus >> 6) & 0x1 == 0x01 : 0 # check UBE = 1, it controls whether explicit load and store memory accesses made from U-mode is big-endian + + +mstatus_checking_SD: + config: + - check ISA:=regex(.*I.*Zicsr.*F.*V.*); + csr_comb: + mstatus >> (xlen-1) == 1 && ((mstatus >> fs_shift) & fs_mask == fs_val) || ((mstatus >> vs_shift) & vs_mask == vs_val) : 0 # The SD bit is read-only and is set when either the FS, VS bits encode a Dirty state + mstatus >> (xlen-1) == 0 && ((mstatus >> fs_shift) & fs_mask == fs_val) || ((mstatus >> vs_shift) & vs_mask == vs_val) : 0 # The SD bit is read-only and is set when either the FS, VS bits encode a Dirty state + +######## mcycle ##################################################################################################################################################################################################### + +mcycle: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + mcycle == 0x0 : 0 # where the value in mcycle register is 0 + mcycle > 1000 : 0 # More than 1000 cycles were executed + mcycle > 10000 : 0 # More than 10000 cycles were executed + mcycle > 100000 : 0 # More than 100000 cycles were executed + +######## mcounteren ##################################################################################################################################################################################################### + +mcounteren: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + (mcounteren >> 0) & 0x1: 0 # Check that the CY bit is set, allowing access to the cycle register + (mcounteren >> 1) & 0x1: 0 # Check that the TM bit is set, allowing access to the time register + (mcounteren >> 2) & 0x1: 0 # Check that the IR bit is set, allowing access to the instret register + (mcounteren >> 3) & 0xFFFFFFF8 == 0: 0 # Check that all other bits are cleared, indicating that no other counters are accessible + +######## mcountinhibit ##################################################################################################################################################################################################### + +mcountinhibit: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + (mcountinhibit >> 0) & 0x1: 0 # Check that the CY bit is set, allowing the cycle counter to increment + (mcountinhibit >> 2) & 0x1: 0 # Check that the IR bit is set, allowing the instret counter to increment + (mcountinhibit >> 3) & 0xFFFFFFF8 == 0: 0 # Check that all other bits are cleared, indicating that no other counters are inhibited + +######## mvendorid ##################################################################################################################################################################################################### + +mvendorid: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.Zicsr.); check is_implemented(mvendorid) = True; # Check if the CSR is present and implemented + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + write_val(mvendorid) = mvendorid: 0 # Check that the value returned is not zero, indicating that the field is implemented or that this is a commercial implementation. + +######## marchid ##################################################################################################################################################################################################### + +marchid: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.Zicsr.); check is_implemented(marchid) = True; # Check if the CSR is present and implemented + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + write_val(marchid) = marchid: 0: 0 # Ensure that marchid is not equal to zero as a value of 0 indicates that the field is not implemented. + +######## mimpid ##################################################################################################################################################################################################### + +mimpid: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.Zicsr.); check is_implemented(mimpid) = True; # Check if the CSR is present and implemented + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + write_val(mimpid) = mimpid: 0 # Check that the value returned is not zero, indicating that the field is implemented + +######## mhartid ##################################################################################################################################################################################################### + +mhartid: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.Zicsr.); check is_implemented(mhartid) = True + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + write_val(mhartid) = mhartid: 0 # Check that at least one hart has a known hart ID of zero + +######## mscratch ##################################################################################################################################################################################################### + +mscratch_valid_address: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); check mscratch >= 0; + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + 0 : 0 # no check needed since this coverpoint only checks if mscratch is a valid address + +######## mepc ##################################################################################################################################################################################################### + +mepc_alignment: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); check is_aligned(mepc, 4) = True; + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + 0 : 0 # no check needed since this coverpoint only checks mepc alignment + + +mepc_write_masked: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + (mepc & 0xFFFFFFFE) == mepc : 0 # check that mepc[1] is masked when IALIGN=32 + +######## mconfigptr ##################################################################################################################################################################################################### + +mconfigptr_base_alignment: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); check is_aligned(mconfigptr, 4) = True; + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + 0 : 0 # no check needed since this coverpoint only checks mconfigptr base alignment + + +mconfigptr_not_zero: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + mconfigptr != 0 : 0 # check that mconfigptr is not zero # check that mconfigptr is not zero + +######## menvcfg & menvcfgh ##################################################################################################################################################################################################### + +menvcfg_FIOM: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*S.*U.*); + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + (menvcfg & (1 << 0)) == 0 or (menvcfg & (1 << 0)) == (1 << 0) : 0 # Check if the FIOM bit is either 0 or 1 using a bitwise AND operation with (1 << 0). If the result is 0 or (1 << 0), the coverpoint is satisfied. + + +menvcfg_PBMTE: + config: + - check ISA:=regex(.*64.*); check ISA:=regex(.*I.*Zicsr.*S.*U.*); + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + (menvcfg & (1 << 61)) == 0 or (menvcfg & (1 << 61)) == (1 << 61) : 0 # Check if the PBMTE bit is either 0 or 1 using a bitwise AND operation with (1 << 61). If the result is 0 or (1 << 61), the coverpoint is satisfied. + + +menvcfgh_PBMTE: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*S.*U.*); + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + (menvcfgh & (1 << 29)) == 0 || (menvcfgh & (1 << 29)) == (1 << 29) : 0 # Check if the PBMTE bit is either 0 or 1 using a bitwise AND operation with (1 << 29). If the result is 0 or (1 << 29), the coverpoint is satisfied. + + +menvcfg_WPRI_3_1: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*S.*U.*); + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + (menvcfg & (0x0E << 1)) == 0 : 0 # This checks that bits 3 to 1 in menvcfg are all zero, as these bits are labeled as WPRI in the specification. + +######## mtime & mtimecmp ##################################################################################################################################################################################################### + +mtime: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); + mnemonics: + csrrs: 0 + csrrw: 0 + csr_comb: + mtime < mtimecmp : 0 # Verify that mtime is always less than mtimecmp + + +mtimecmp: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); + mnemonics: + csrrs: 0 + csrrw: 0 + csr_comb: + (mtimecmp >> 32) == 0 : 0 # Verify that writes to mtimecmp only modify the lower 32 bits + (mtimecmp - mtime) > 0 : 0 # Verify that mtimecmp is always greater than mtime after a write + + +mtimecmp_timer_interrupt: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + (mtime >= mtimecmp) & (mstatus.MIE == 1) & (mie.MTIE == 1): 0 # Check that the machine timer interrupt is only taken when mtime contains a value greater than or equal to mtimecmp, and that interrupts are enabled and the MTIE bit is set in the mie register. + + +mtimecmp_write: + config: + - check ISA:=regex(.*32.*|.*64.*); check ISA:=regex(.*I.*Zicsr.*); + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + (mtime >= mtimecmp) & (mstatus.MIE == 1) & (mie.MTIE == 1): 0 # Check that writes to mtime and mtimecmp are guaranteed to be reflected in MTIP eventually, but not necessarily immediately. + + +mtime: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); + - check ISA:=regex(.*64.*); check ISA:=regex(.*I.*Zicsr.*); + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + (mtime >= 0) & (mtime < 2**64): 0 # Check that mtime is a memory-mapped read-write register with the correct bit width. + +######## pmpcfg ##################################################################################################################################################################################################### + + +pmp_napot_mode: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); check hw_data_misaligned_support:=True; def rvtest_mtrap_routine=True; check is_implemented(pmpcfg0) = True; + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); check hw_data_misaligned_support:=True; def rvtest_mtrap_routine=True; check is_implemented(pmpcfg1) = True; + + + check is_implemented(pmpcfg2) = True; check is_implemented(pmpcfg3) = True; + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + (pmpcfg0 >> 16) & 0x18 = 0x18 : 0 # Check if the NAPOT (Naturally Aligned Power-of-Two) mode is set for the PMP entry + (pmpcfg1 >> 16) & 0x18 = 0x18 : 0 # Check if the NAPOT (Naturally Aligned Power-of-Two) mode is set for the PMP entry + (pmpcfg2 >> 16) & 0x18 = 0x18 : 0 # Check if the NAPOT (Naturally Aligned Power-of-Two) mode is set for the PMP entry + (pmpcfg3 >> 16) & 0x18 = 0x18 : 0 # Check if the NAPOT (Naturally Aligned Power-of-Two) mode is set for the PMP entry + + +pmp_na4_mode: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); check hw_data_misaligned_support:=True; def rvtest_mtrap_routine=True; check is_implemented(pmpcfg0) = True; check is_implemented(pmpcfg1) = True; check is_implemented(pmpcfg2) = True; check is_implemented(pmpcfg3) = True; + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + (pmpcfg0 >> 16) & 0x18 == 0x10 : 0 # Check if the NA4 (Naturally Aligned 4-byte region) mode is set for the PMP entry + (pmpcfg1 >> 16) & 0x18 == 0x10 : 0 # Check if the NA4 (Naturally Aligned 4-byte region) mode is set for the PMP entry + (pmpcfg2 >> 16) & 0x18 == 0x10 : 0 # Check if the NA4 (Naturally Aligned 4-byte region) mode is set for the PMP entry + (pmpcfg3 >> 16) & 0x18 == 0x10 : 0 # Check if the NA4 (Naturally Aligned 4-byte region) mode is set for the PMP entry + + +pmp_tor_mode: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); check hw_data_misaligned_support:=True; def rvtest_mtrap_routine=True; check is_implemented(pmpcfg0) = True; check is_implemented(pmpcfg1) = True; check is_implemented(pmpcfg2) = True; check is_implemented(pmpcfg3) = True; + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + '(pmpcfg0 >> 16) & 0x18 == 0x08': 0 # Check if the NA4 (Naturally Aligned 4-byte region) mode is set for the PMP entry + '(pmpcfg1 >> 16) & 0x18 == 0x08': 0 # Check if the NA4 (Naturally Aligned 4-byte region) mode is set for the PMP entry + '(pmpcfg2 >> 16) & 0x18 == 0x08': 0 # Check if the NA4 (Naturally Aligned 4-byte region) mode is set for the PMP entry + '(pmpcfg3 >> 16) & 0x18 == 0x08': 0 # Check if the NA4 (Naturally Aligned 4-byte region) mode is set for the PMP entry + + +# TOR with lw instruction +pmp_tor_mode_address_match_lw: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); def rvtest_mtrap_routine=True; + mnemonics: + lw: 0 + val_comb: + '(pmpcfg1 & 0x18 == 0x08) and (rs1_val + imm_val >= (pmpaddr0 << 2)) and (rs1_val + imm_val < (pmpaddr1 << 2))': 0 + +# TOR with lh instruction +pmp_tor_mode_address_match_lh: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); def rvtest_mtrap_routine=True; + mnemonics: + lh: 0 + val_comb: + '(pmpcfg1 & 0x18 == 0x08) and (rs1_val + imm_val >= (pmpaddr0 << 2)) and (rs1_val + (imm_val << pmpaddr1))': 0 + +# TOR with sw instruction +pmp_tor_mode_address_match_sw: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); def rvtest_mtrap_routine=True; + mnemonics: + sw: 0 + val_comb: + '(pmpcfg1 & 0x18 == 0x08) and (rs1_val + imm_val >= (pmpaddr0 << 2)) and (rs1_val + imm_val < (pmpaddr1 << 2))': 0 + +# TOR with sh instruction +pmp_tor_mode_address_match_sh: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); def rvtest_mtrap_routine=True; + mnemonics: + sh: 0 + val_comb: + '(pmpcfg1 & 0x18 == 0x08) and (rs1_val + imm_val >= (pmpaddr0 << 2)) and (rs1_val + imm_val < (pmpaddr1 << 2))': 0 + +# TOR with sb instruction +pmp_tor_mode_address_match_sb: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); def rvtest_mtrap_routine=True; + mnemonics: + sb: 0 + val_comb: + '(pmpcfg1 & 0x18 == 0x08) and (rs1_val + imm_val >= (pmpaddr0 << 2)) and (rs1_val + imm_val < (pmpaddr1 << 2))': 0 + + +# NA4 with lw instruction +pmp_tor_mode_address_match_lw: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); def rvtest_mtrap_routine=True; + mnemonics: + lw: 0 + val_comb: + '(pmpcfg1 & 0x18 == 0x10) and (rs1_val + imm_val >= (pmpaddr << 2)) and (rs1_val +imm_val < (pmpaddr << 2))': 0 + +# NA4 with lh instruction +pmp_tor_mode_address_match_lh: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); def rvtest_mtrap_routine=True; + mnemonics: + lh: 0 + val_comb: + '(pmpcfg1 & 0x18 == 0x10) and (rs1_val + imm_val >= (pmpaddr << 2)) and (rs1_val +imm_val < (pmpaddr << 2))': 0 + +# NA4 with sw instruction +pmp_tor_mode_address_match_sw: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); def rvtest_mtrap_routine=True; + mnemonics: + sw: 0 + val_comb: + '(pmpcfg1 & 0x18 == 0x10) and (rs1_val + imm_val >= (pmpaddr << 2)) and (rs1_val +imm_val < (pmpaddr << 2))': 0 + +# NA4 with sh instruction +pmp_tor_mode_address_match_sh: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); def rvtest_mtrap_routine=True; + mnemonics: + sh: 0 + val_comb: + '(pmpcfg1 & 0x18 == 0x10) and (rs1_val + imm_val >= (pmpaddr << 2)) and (rs1_val +imm_val < (pmpaddr << 2))': 0 + +# NA4 with sb instruction +pmp_tor_mode_address_match_sb: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); def rvtest_mtrap_routine=True; + mnemonics: + sb: 0 + val_comb: + '(pmpcfg1 & 0x18 == 0x10) and (rs1_val + imm_val >= (pmpaddr << 2)) and (rs1_val +imm_val < (pmpaddr << 2))': 0 + +# NAPOT with lw instruction +pmp_napot_mode_address_match_lw: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); def rvtest_mtrap_routine=True; + mnemonics: + lw: 0 + val_comb: + '(pmpcfg1 & 0x18 == 0x18) and (rs1_val + imm_val >= (pmpaddr1 << 2)) and (rs1_val + imm_val < ((((((pmpaddr1 << 2) | 3) + 1) | (((pmpaddr1 << 2) | 3))) + 1)))': 0 + +# NAPOT with lh instruction +pmp_napot_mode_address_match_lh: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); def rvtest_mtrap_routine=True; + mnemonics: + lh: 0 + val_comb: + '(pmpcfg1 & 0x18 == 0x18) and (rs1_val + imm_val >= (pmpaddr1 << 2)) and (rs1_val + imm_val < ((((((pmpaddr1 << 2) | 3) + 1) | (((pmpaddr1 << 2) | 3))) + 1)))': 0 + +# NAPOT with sw instruction +pmp_napot_mode_address_match_sw: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); def rvtest_mtrap_routine=True; + mnemonics: + sw: 0 + val_comb: + '(pmpcfg1 & 0x18 == 0x18) and (rs1_val + imm_val >= (pmpaddr1 << 2)) and (rs1_val + imm_val < ((((((pmpaddr1 << 2) | 3) + 1) | (((pmpaddr1 << 2) | 3))) + 1)))': 0 + +# NAPOT with sh instruction +pmp_napot_mode_address_match_sh: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); def rvtest_mtrap_routine=True; + mnemonics: + sh: 0 + val_comb: + '(pmpcfg1 & 0x18 == 0x18) and (rs1_val + imm_val >= (pmpaddr1 << 2)) and (rs1_val + imm_val < ((((((pmpaddr1 << 2) | 3) + 1) | (((pmpaddr1 << 2) | 3))) + 1)))': 0 + +# NAPOT with sb instruction +pmp_napot_mode_address_match_sb: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); def rvtest_mtrap_routine=True; + mnemonics: + sb: 0 + val_comb: + '(pmpcfg1 & 0x18 == 0x18) and (rs1_val + imm_val >= (pmpaddr1 << 2)) and (rs1_val + imm_val < ((((((pmpaddr1 << 2) | 3) + 1) | (((pmpaddr1 << 2) | 3))) + 1)))': 0 + +pmp_locked_NAPOT_OR_NA4: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); check hw_data_misaligned_support:=True; def rvtest_mtrap_routine=True; check is_implemented(pmpcfg0) = True + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + ((pmpcfg0 & 0x80) == 0x80) & ((pmpcfg0 & 0x18) == 0x10 || (pmpcfg0 & 0x18) == 0x18) & (old_val(pmpcfg0 & 0xFF) ) & (old_val(pmpaddr0)) : 0 # Check if lock bit is set for pmp0cfg0 and pmp0 is configured in either the NAPOT or NA4 mode, then the values of pmpcfg0[7:0] and pmpaddr0 should not change. + + +pmp_locked_TOR_region0: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); check hw_data_misaligned_support:=True; def rvtest_mtrap_routine=True; check is_implemented(pmpcfg0) = True + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + ((pmpcfg0 & 0x80) == 0x80) & ((pmpcfg0 & 0x18) == 0x08) & (old_val(pmpcfg0 & 0xFF) ) & (old_val(pmpaddr0)) : 0 # Check if lock bit is set for pmp0cfg0 and pmp0 is configured in TOR mode, then the values of pmpcfg0[7:0] and pmpaddr0 should not change. + + +pmp_locked_TOR: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); check hw_data_misaligned_support:=True; def rvtest_mtrap_routine=True; check is_implemented(pmpcfg0) = True + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + (((pmpcfg0 >> 8) & 0x80) == 0x80) & (((pmpcfg0 >> 8) & 0x18) == 0x08) & (old_val((pmpcfg0 >> 8) & 0xFF)) & (old_val(pmpaddr1)) & (old_val(pmpaddr0)) : 0 # Check if lock bit is set for pmp1cfg0 and pmp1 is configured in TOR mode, then the values of pmpcfg0[15:8], pmpaddr0 and pmpaddr1 should not change. + + + + +pmp_lock_region_disabled: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); check hw_data_misaligned_support:=True; def rvtest_mtrap_routine=True; check is_implemented(pmpcfg0) = True + mnemonics: + csrrw: 0 + csrrs: 0 + csr_comb: + (((pmpcfg0 & 0x80) == 0x80) & ((pmpcfg0 >> 3) & 0x3) == 0x0) & (old_val(pmpcfg0 & 0xFF) ) & (old_val(pmpaddr0)) : 0 + # Check if lock bit is set for pmpcfg0, pmpcfg0.A is set to OFF, and the values of pmpcfg0 and pmpaddr0 should not change. + +# Lock bit set, no R/W/X access in machine mode and lw in that region +locking_L_M_mode: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); def rvtest_mtrap_routine=True; + mnemonics: + lw: 0 + val_comb: + '(pmpcfg0 & 0x8000 == 0x8000) and (pmpcfg0 & 0x800 == 0x800) and (pmpcfg0 & 0x700 == 0x00) and (rs1_val + imm_val < (pmpaddr1 << 2)) and (rs1_val +imm_val >= (pmpaddr0 << 2))': 0 + +# Lock bit unset, no R/W/X access in machine mode and lw in that region +locking_M_mode: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); def rvtest_mtrap_routine=True; + mnemonics: + lw: 0 + val_comb: + '(pmpcfg0 & 0x8000 == 0x00) and (pmpcfg0 & 0x800 == 0x800) and (pmpcfg0 & 0x700 == 0x00) and (rs1_val + imm_val < (pmpaddr1 << 2)) and (rs1_val +imm_val >= (pmpaddr0 << 2))': 0 + +# Lock bit set, given R/W/X access in machine mode and lw in that region +locking_LRWX_M_mode: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); def rvtest_mtrap_routine=True; + mnemonics: + lw: 0 + val_comb: + '(pmpcfg0 & 0x8000 == 0x8000) and (pmpcfg0 & 0x800 == 0x800) and (pmpcfg0 & 0x700 == 0x700) and (rs1_val + imm_val < (pmpaddr1 << 2)) and (rs1_val +imm_val >= (pmpaddr0 << 2))': 0 + +# Lock bit unset, given R/W/X access in machine mode and lw in that region +locking_RWX_M_mode: + config: + - check ISA:=regex(.*32.*); check ISA:=regex(.*I.*Zicsr.*); def rvtest_mtrap_routine=True; + mnemonics: + lw: 0 + val_comb: + '(pmpcfg0 & 0x8000 == 0x00) and (pmpcfg0 & 0x800 == 0x800) and (pmpcfg0 & 0x700 == 0x700) and (rs1_val + imm_val < (pmpaddr1 << 2)) and (rs1_val +imm_val >= (pmpaddr0 << 2))': 0 +