# rtio-nmigen

Formally verified implementation of the ARTIQ RTIO core in nMigen

## Progress

- [ ] Implement the core in nMigen
- - [ ] `rtio.core`
- - [ ] `rtio.cri`
- - [x] `rtio.rtlink`
- - [x] `rtio.channel`
- - [ ] `rtio.sed.core`
- - [x] `rtio.sed.layouts`
- - [ ] `rtio.sed.lane_distributor`
- - [ ] `rtio.sed.fifos`
- - [ ] `rtio.sed.gates`
- - [ ] `rtio.sed.output_driver`
- - [ ] `rtio.sed.output_network`
- - [ ] `rtio.input_collector`
- [ ] Add suitable assertions for verification (BMC / unbounded proof?)

## License

Copyright (C) 2020 M-Labs Limited.

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