Formally verified ARTIQ RTIO core in nMigen

Go to file

Donald Sebastian Leung 160ac76ee7 Fix typo in rtio.sed.output_driver		2020-10-27 13:39:19 +08:00
rtio	Fix typo in rtio.sed.output_driver	2020-10-27 13:39:19 +08:00
LICENSE	Add README and LICENSE	2020-09-23 17:14:27 +08:00
NOTES.md	Add breakdown of cmp_wrap() for reference	2020-10-22 11:27:08 +08:00
README.md	Restructure rtio.sed.output_driver to follow nMigen convention	2020-10-27 13:33:41 +08:00
shell.nix	Remove dependence on custom version of nMigen	2020-10-23 15:02:11 +08:00

README.md

rtio-nmigen

Formally verified implementation of the ARTIQ RTIO core in nMigen

File Synopsis

LICENSE: License terms (LGPLv3+) for this project
README.md: this document
shell.nix: Nix file for setting up the environment for this project
rtio: RTIO core in nMigen

Running the verification tasks

Currently, only the sorting network contains assertions to be verified. To run the verification tasks for the sorting network, change directory to the root of this project, set up the Nix environment by running nix-shell and do

$ python -m rtio.test.sed.output_network

Progress

Devise a suitable migration strategy for artiq.gateware.rtio from Migen to nMigen
Implement the core in nMigen
- rtio.cri (Interface and CRIDecoder only)
- rtio.rtlink
- rtio.sed.layouts
- rtio.sed.output_network
- rtio.sed.output_driver
Add suitable assertions for verification (BMC / unbounded proof?)
- rtio.cri (Interface and CRIDecoder only)
- rtio.sed.output_network - Sorting network (high priority)
- rtio.sed.output_driver
Restructure to code to follow nMigen convention and re-validate existing assertions (if any)
- rtio.cri (Interface and CRIDecoder only)
- rtio.sed.output_network
- rtio.sed.output_driver

License

LGPLv3 or any later version