serial: A proposal to add verification using formal tools

[nmigen-issue-migration]

Issue by HarryHo90sHK
Friday Jan 03, 2020 at 06:47 GMT
Originally opened as m-labs/nmigen-stdio#4

---

On this pull request, I propose modifications on @whitequark's UART / asynchronous serial transmitter/receiver that would introduce a way to formally verify the I/O. The major changes include:

1. Deprecated nMigen syntax (e.g. FFSynchronizer, nmigen.tools) have been eradicated.
2. AsyncSerialRX now has the following signals: ack for enabling transfer of received data to another module, busy for indicating ongoing data reception, and r_rdy for indicating whether or not the received data is ready to transfer.
3. AsyncSerialTX now has the following signals: ack for enabling transmission of data from another module, busy for indicating ongoing data transmission, and w_done for indicating whether or not the data has been transmitted.
4. The data bits are now ordered in ascending significance of bit, i.e. LSB is transmitted first, MSB is transmitted last.
5. Two test cases (AsyncSerialLoopbackTestCase and AsyncSerialBitstreamTestCase) that use a formal verification approach has been added to nmigen_stdio.test.test_serial. In short, they use Bounded Model Checking to check if the desired states (e.g. "DONE" for correct data transmission, or "ERROR" for data with errors) can be reached within certain numbers of cycles, usually equal to the duration that starts before the RX/TX is enabled and ends after the RX/TX asserts r_rdy/w_done.

I will provide further useful descriptions and explanations later on. I look forward to seeing further comments, thanks.

Edit: the version check in setup.py will be modified according to the final decision.

---

HarryHo90sHK included the following code: https://github.com/m-labs/nmigen-stdio/pull/4/commits

[whitequark]

The PR is outdated and the author is no longer working on it.