rtio-nmigen/README.md

35 lines
1.1 KiB
Markdown
Raw Normal View History

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
2020-10-20 13:05:38 +08:00
## 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
- `traces`: History of traces for debugging
2020-09-23 17:14:27 +08:00
## Progress
2020-09-30 10:55:08 +08:00
- Devise a suitable migration strategy for `artiq.gateware.rtio` from Migen to nMigen
2020-10-09 11:16:01 +08:00
- [x] Implement the core in nMigen
- - [x] `rtio.cri` (`Interface` and `CRIDecoder` only)
2020-10-07 16:32:20 +08:00
- - [x] `rtio.rtlink`
2020-10-08 11:06:35 +08:00
- - [x] `rtio.sed.layouts`
2020-10-08 17:05:04 +08:00
- - [x] `rtio.sed.output_network`
2020-10-09 11:16:01 +08:00
- - [x] `rtio.sed.output_driver`
2020-09-23 17:14:27 +08:00
- [ ] Add suitable assertions for verification (BMC / unbounded proof?)
2020-10-14 16:50:01 +08:00
- - [ ] `rtio.cri` (`Interface` and `CRIDecoder` only)
- - [ ] `rtio.rtlink`
- - [ ] `rtio.sed.layouts`
- - [ ] `rtio.sed.output_network` - Sorting network (high priority)
2020-10-14 16:50:57 +08:00
- - [ ] `rtio.sed.output_driver`
- [ ] Restructure to code to follow nMigen convention and re-validate existing assertions
2020-09-23 17:14:27 +08:00
## License
Copyright (C) 2020 M-Labs Limited.
2020-09-23 17:16:58 +08:00
[LGPLv3](./LICENSE) or any later version