Formally verified ARTIQ RTIO core in nMigen
rtio | ||
LICENSE | ||
README.md | ||
shell.nix |
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
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
License
Copyright (C) 2020 M-Labs Limited.
LGPLv3 or any later version