-
Notifications
You must be signed in to change notification settings - Fork 235
Open
Description
When you perform an access to an MMIO device we do this:
if within_mmio_writable(paddr, width)
then mmio_write(paddr, width, data)
else {
let wk = write_kind_of_flags(aq, rl, con);
phys_mem_write(wk, paddr, width, data, meta)
}
...
function within_mmio_writable forall 'n, 0 < 'n <= max_mem_access . (addr : physaddr, width : int('n)) -> bool =
if get_config_rvfi()
then false
else within_clint(addr, width) | (within_htif_writable(addr, width) & 'n <= 8)
...
function mmio_write forall 'n, 0 < 'n <= max_mem_access . (paddr : physaddr, width : int('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) =
if within_clint(paddr, width)
then clint_store(paddr, width, data)
else if within_htif_writable(paddr, width)
then htif_store(paddr, width, data)
else Err(E_SAMO_Access_Fault())
This is slightly odd for misaligned accesses that intersect the device but aren't full contained within it. In this case we should get an access fault. So the code should be like this:
if intersects_mmio_writable(paddr, width)
then mmio_write(paddr, width, data)
else {
let wk = write_kind_of_flags(aq, rl, con);
phys_mem_write(wk, paddr, width, data, meta)
}
...
function intersects_mmio_writable forall 'n, 0 < 'n <= max_mem_access . (addr : physaddr, width : int('n)) -> bool =
if get_config_rvfi()
then false
else intersects_clint(addr, width) | (intersects_htif_writable(addr, width) & 'n <= 8)
...
function mmio_write forall 'n, 0 < 'n <= max_mem_access . (paddr : physaddr, width : int('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) =
if within_clint(paddr, width)
then clint_store(paddr, width, data)
else if within_htif_writable(paddr, width)
then htif_store(paddr, width, data)
else Err(E_SAMO_Access_Fault())
So that it is handled by the MMIO code if it intersects an MMIO device, but then it causes an access fault if it isn't fully contained in the MMIO device.
We should also add standard functions in range_util.sail for intersects and within if they aren't there already, because the optimal logic for these operations tends to be a bit confusing.
pmundkur
Metadata
Metadata
Assignees
Labels
No labels