This repository has been archived by the owner on Dec 13, 2022. It is now read-only.

[firmware/Uart] uart_putchar precondition needs to be more generic #897

Open

dayeol opened this issue Aug 16, 2021 · 0 comments

Contributor

dayeol commented Aug 16, 2021 •

edited

Loading

In UartProperties.v, uart_putchar has a precondition execution t IDLE which means that the state needs to be IDLE.
However, this isn't necessarily required as you can write to WDATA as long as the FIFO is not full (i.e., uart_tx_full returns 0). #888
https://github.com/project-oak/silveroak/pull/888/files/e4726f92f4731ac63f4e06d952f32f54863d99f1#diff-d9411a34f7afad9c8a02c00eddb68b70ce66fe2bb82e348da435351876b3fcb0

The text was updated successfully, but these errors were encountered:

dayeol mentioned this issue

Uart semantics and proofs (cont'd) #888

Merged

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.