M-Labs
/
rtio-nmigen
10
0
Fork 0
Code Issues 0 Pull Requests 0 Releases 0 Wiki Activity
Formally verified ARTIQ RTIO core in nMigen
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
70 Commits
1 Branch
156 KiB
 
 
Branch: master
Branches Tags
${ item.name }
Create branch ${ searchTerm }
from 'master'
${ noResults }
 ZIP  TAR.GZ
Donald Sebastian Leung e82a82538b Add simulation for CRI write command(?) 5 months ago
rtio Add simulation for CRI write command(?) 5 months ago
LICENSE Add README and LICENSE 7 months ago
README.md Measure completion time for each unbounded proof 5 months ago
shell.nix Remove dependence on custom version of nMigen 6 months ago

README.md

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 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.

License

Copyright (C) 2020 M-Labs Limited.

LGPLv3 or any later version