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:
- Deprecated nMigen syntax (e.g. FFSynchronizer, nmigen.tools) have been eradicated.
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.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.- The data bits are now ordered in ascending significance of bit, i.e. LSB is transmitted first, MSB is transmitted last.
- 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
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:
AsyncSerialRXnow has the following signals:ackfor enabling transfer of received data to another module,busyfor indicating ongoing data reception, andr_rdyfor indicating whether or not the received data is ready to transfer.AsyncSerialTXnow has the following signals:ackfor enabling transmission of data from another module,busyfor indicating ongoing data transmission, andw_donefor indicating whether or not the data has been transmitted.AsyncSerialLoopbackTestCaseandAsyncSerialBitstreamTestCase) that use a formal verification approach has been added tonmigen_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 assertsr_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.pywill be modified according to the final decision.HarryHo90sHK included the following code: https://github.com/m-labs/nmigen-stdio/pull/4/commits