This repository was archived by the owner on Dec 13, 2022. It is now read-only.
This repository was archived by the owner on Dec 13, 2022. It is now read-only.
[firmware/Uart] Need an invariant on maximum number of busy cycles #898
Description
#888 introduces ncycles_processing and fifo_depth parameters.
We should be able to prove the invariant that the number of busy cycles in the state BUSY cycles doesn't go over (fifo_depth + 1) * ncycles_processing.
@samuelgruetter proposed:
forall t s, execution t s -> forall tx, s = BUSY tx -> tx < (fifo_depth + 1) * ncycles_processing