Donald Sebastian Leung b391f0e413 | ||
---|---|---|
rtio | ||
LICENSE | ||
NOTES.md | ||
README.md | ||
shell.nix |
README.md
rtio-nmigen
Formally verified implementation of the ARTIQ RTIO core in nMigen
File Synopsis
LICENSE
: License terms (LGPLv3+) for this projectREADME.md
: this documentshell.nix
: Nix file for setting up the environment for this projectrtio
: 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
andCRIDecoder
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
andCRIDecoder
only)
-
rtio.rtlink
-
rtio.sed.layouts
-
rtio.sed.output_network
- Sorting network (high priority)
-
rtio.sed.output_driver
- Restructure to code to follow nMigen convention and re-validate existing assertions
-
rtio.cri
(Interface
andCRIDecoder
only)
-
rtio.rtlink
-
rtio.sed.layouts
-
rtio.sed.output_network
-
rtio.sed.output_driver
License
Copyright (C) 2020 M-Labs Limited.
LGPLv3 or any later version