27 lines
837 B
Markdown
27 lines
837 B
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
|
|
|
|
To run the verification tasks for the sorting network (unbounded proofs with variable numbers of lanes), 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
|
|
```
|
|
|
|
This should complete in under an hour. The time to complete each verification task (2 lanes, 4 lanes, 8 lanes) is printed to standard output.
|
|
|
|
## License
|
|
|
|
Copyright (C) 2020 M-Labs Limited.
|
|
|
|
[LGPLv3](./LICENSE) or any later version
|