rtio-nmigen/README.md

44 lines
1.5 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, set up the [Nix](https://nixos.org) environment by running `nix-shell` 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)
- - [x] `rtio.sed.output_network` - Sorting network (high priority)
- - [ ] `rtio.sed.output_driver`
- [x] Restructure to code to follow nMigen convention and re-validate existing assertions (if any)
- - [x] `rtio.cri` (`Interface` and `CRIDecoder` only)
- - [x] `rtio.sed.output_network`
- - [x] `rtio.sed.output_driver`
- [ ] Simulate RTIO command for switching TTL
## License
Copyright (C) 2020 M-Labs Limited.
[LGPLv3](./LICENSE) or any later version