2020-09-23 17:10:41 +08:00
|
|
|
# rtio-nmigen
|
|
|
|
|
|
2020-09-23 17:14:27 +08:00
|
|
|
Formally verified implementation of the ARTIQ RTIO core in nMigen
|
|
|
|
|
|
|
|
|
|
## Progress
|
|
|
|
|
|
|
|
|
|
- [ ] Implement the core in nMigen
|
2020-09-25 15:10:07 +08:00
|
|
|
- - [ ] `rtio.core`
|
|
|
|
|
- - [ ] `rtio.cri`
|
|
|
|
|
- - [x] `rtio.rtlink`
|
|
|
|
|
- - [x] `rtio.channel`
|
|
|
|
|
- - [ ] `rtio.sed.core`
|
|
|
|
|
- - [x] `rtio.sed.layouts`
|
2020-09-28 16:01:43 +08:00
|
|
|
- - [x] `rtio.sed.lane_distributor`
|
2020-09-25 15:10:07 +08:00
|
|
|
- - [ ] `rtio.sed.fifos`
|
|
|
|
|
- - [ ] `rtio.sed.gates`
|
|
|
|
|
- - [ ] `rtio.sed.output_driver`
|
2020-09-29 16:35:59 +08:00
|
|
|
- - [x] `rtio.sed.output_network`
|
2020-09-25 15:10:07 +08:00
|
|
|
- - [ ] `rtio.input_collector`
|
2020-09-23 17:14:27 +08:00
|
|
|
- [ ] Add suitable assertions for verification (BMC / unbounded proof?)
|
|
|
|
|
|
|
|
|
|
## License
|
|
|
|
|
|
|
|
|
|
Copyright (C) 2020 M-Labs Limited.
|
|
|
|
|
|
2020-09-23 17:16:58 +08:00
|
|
|
[LGPLv3](./LICENSE) or any later version
|
