|Donald Sebastian Leung e82a82538b||5 months ago|
|rtio||5 months ago|
|LICENSE||7 months ago|
|README.md||5 months ago|
|shell.nix||6 months ago|
Formally verified implementation of the ARTIQ RTIO core in nMigen
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
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 environment by running
nix-shell and do
$ 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.
Copyright (C) 2020 M-Labs Limited.
LGPLv3 or any later version