# 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