Formally verified ARTIQ RTIO core in nMigen

Go to file

Donald Sebastian Leung fd1b469322 Remove redundant (object) in rtio.rtlink		2020-10-08 09:34:29 +08:00
rtio	Remove redundant (object) in rtio.rtlink	2020-10-08 09:34:29 +08:00
LICENSE	Add README and LICENSE	2020-09-23 17:14:27 +08:00
README.md	Add rtio.rtlink	2020-10-07 16:32:20 +08:00
shell.nix	Add shell.nix	2020-09-24 15:11:24 +08:00

README.md

rtio-nmigen

Formally verified implementation of the ARTIQ RTIO core in nMigen

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?)

License

Copyright (C) 2020 M-Labs Limited.

LGPLv3 or any later version