# 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

## Progress

- Devise a suitable migration strategy for `artiq.gateware.rtio` from Migen to nMigen
- [x] Implement the core in nMigen
- - [x] `rtio.cri` (`Interface` and `CRIDecoder` only)
- - [x] `rtio.rtlink`
- - [x] `rtio.sed.layouts`
- - [x] `rtio.sed.output_network`
- - [x] `rtio.sed.output_driver`
- [ ] Add suitable assertions for verification (BMC / unbounded proof?)
- - [ ] `rtio.cri` (`Interface` and `CRIDecoder` 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

## License

Copyright (C) 2020 M-Labs Limited.

[LGPLv3](./LICENSE) or any later version