42 lines
1.3 KiB
Markdown
42 lines
1.3 KiB
Markdown
# 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
|
|
|
|
## Running the verification tasks
|
|
|
|
Currently, only the sorting network contains assertions to be verified. To run the verification tasks for the sorting network, change directory to the root of this project and do
|
|
|
|
```bash
|
|
$ python -m rtio.test.sed.output_network
|
|
```
|
|
|
|
## 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
|