Issues

[Formal finding VEX-RTL-019] medelegh is not implemented on an XLEN=32 hart with S-mode, so the upper half of the 64-bit medeleg is unreachable and a read traps

#498

· StandardAsh opened

on Sep 18, 2026

[Formal finding VEX-RTL-016] scause implements only 4 bits of Exception Code, but the architecture requires bits 4-0 so the register can hold 0-31

#497

· StandardAsh opened

on Sep 18, 2026

[Formal finding VEX-RTL-015] menvcfg and menvcfgh are not implemented on a hart with U-mode and S-mode, so reads of them raise illegal-instruction exceptions

#496

· StandardAsh opened

on Sep 18, 2026

[Formal finding VEX-RTL-014] sepc has no low-bit masking: sepc[0] is writable and reads back as one

#495

· StandardAsh opened

on Sep 18, 2026

[Formal finding VEX-RTL-011] mstatus.MPRV is not writable on a hart that implements U-mode

#494

· StandardAsh opened

on Sep 18, 2026

[Formal finding VEX-RTL-010] misa.Extensions reports B and G and omits I on a core that implements RV32I, and the E bit is not the complement of I

#493

· StandardAsh opened

on Sep 18, 2026

[Formal finding VEX-RTL-007] mtval is not written on an interrupt trap, so it retains the faulting address left by the previous exception instead of being set to zero

#492

· StandardAsh opened

on Sep 18, 2026

[Formal finding VEX-RTL-006] mcause has no reset value, so after reset it reads an undefined value instead of one indicating the cause of the reset

#491

· StandardAsh opened

on Sep 18, 2026

[Formal finding VEX-RTL-004] On an environment-call exception mtval is written with the ECALL instruction encoding instead of zero

#490

· StandardAsh opened

on Sep 18, 2026

[Formal finding VEX-RTL-003] mepc has no low-bit masking: mepc[0] is writable and reads back as one, and MRET then redirects the fetch to an unaligned address

#489

· StandardAsh opened

on Sep 18, 2026

[Formal finding VEX-RTL-002] MRET sets mstatus.MPP to 00 (U-mode) on a hart that implements only M-mode, leaving an unsupported privilege encoding architecturally readable

#488

· StandardAsh opened

on Sep 18, 2026

MMU plugin allows supervisor execution of code in user pages when status.SUM is 1

#487

· MichaelBell opened

on Sep 17, 2026

Navigation Menu

All issues

[Formal finding VEX-RTL-019] medelegh is not implemented on an XLEN=32 hart with S-mode, so the upper half of the 64-bit medeleg is unreachable and a read traps

[Formal finding VEX-RTL-016] scause implements only 4 bits of Exception Code, but the architecture requires bits 4-0 so the register can hold 0-31

[Formal finding VEX-RTL-015] menvcfg and menvcfgh are not implemented on a hart with U-mode and S-mode, so reads of them raise illegal-instruction exceptions

[Formal finding VEX-RTL-014] sepc has no low-bit masking: sepc[0] is writable and reads back as one

[Formal finding VEX-RTL-011] mstatus.MPRV is not writable on a hart that implements U-mode

[Formal finding VEX-RTL-010] misa.Extensions reports B and G and omits I on a core that implements RV32I, and the E bit is not the complement of I

[Formal finding VEX-RTL-007] mtval is not written on an interrupt trap, so it retains the faulting address left by the previous exception instead of being set to zero

[Formal finding VEX-RTL-006] mcause has no reset value, so after reset it reads an undefined value instead of one indicating the cause of the reset

[Formal finding VEX-RTL-004] On an environment-call exception mtval is written with the ECALL instruction encoding instead of zero

[Formal finding VEX-RTL-003] mepc has no low-bit masking: mepc[0] is writable and reads back as one, and MRET then redirects the fetch to an unaligned address

[Formal finding VEX-RTL-002] MRET sets mstatus.MPP to 00 (U-mode) on a hart that implements only M-mode, leaving an unsupported privilege encoding architecturally readable

MMU plugin allows supervisor execution of code in user pages when status.SUM is 1

Search results