The SHA driver code performs 8-bit MMIO, so I adapted the bedrock2-to-RISC-V part of the end-to-end proofs to support n-byte MMIO, where n=1,2 or 4.
However, the RISC-V-to-Cava connection still assumes that all MMIO is 32-bit. To make sure we're ready to connect to the Cava SHA/HMAC device, it would be good to do the following:
InternalMMIOMachine.device.run1 should take an additional argument indicating whether we're exchanging 8, 16 or 32 bits. I can imagine different signatures to express this and have not yet thought about which one would be best, but probably it would be good to stay close to the TileLink spec and to what Cava does.- To test whether everything plays together end-to-end, it would be interesting to adapt the
IncrementWait example to use an 8-bit register for the status rather than a 32-bit register, ie to replace io! status = READ32 ( STATUS_ADDR ) by io! status = READ8 ( STATUS_ADDR ) in firmware/IncrementWait/IncrementWait.v, adapt IncrementWaitSemantics.read/write_step to take an additional size argument that indicates how many bytes are exchanged (1,2, or 4, like in HmacSemantics), and see whether the end-to-end proof about IncrementWait still goes through.
The SHA driver code performs 8-bit MMIO, so I adapted the bedrock2-to-RISC-V part of the end-to-end proofs to support n-byte MMIO, where n=1,2 or 4.
However, the RISC-V-to-Cava connection still assumes that all MMIO is 32-bit. To make sure we're ready to connect to the Cava SHA/HMAC device, it would be good to do the following:
InternalMMIOMachine.device.run1should take an additional argument indicating whether we're exchanging 8, 16 or 32 bits. I can imagine different signatures to express this and have not yet thought about which one would be best, but probably it would be good to stay close to the TileLink spec and to what Cava does.IncrementWaitexample to use an 8-bit register for the status rather than a 32-bit register, ie to replaceio! status = READ32 ( STATUS_ADDR )byio! status = READ8 ( STATUS_ADDR )infirmware/IncrementWait/IncrementWait.v, adaptIncrementWaitSemantics.read/write_stepto take an additional size argument that indicates how many bytes are exchanged (1,2, or 4, like inHmacSemantics), and see whether the end-to-end proof aboutIncrementWaitstill goes through.