M-Labs
/
rtio-nmigen
7
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
Formally verified ARTIQ RTIO core in nMigen
47 Commits 1 Branch 0 Tags 98 KiB
Python 98.3%
Nix 1.7%
Go to file
Donald Sebastian Leung 69a3e5606f Add mention of Nix in "Running the verification tasks" 2020-10-23 10:43:43 +08:00
rtio Refine assertions for case with replacements in sorting network 2020-10-23 10:31:56 +08:00
LICENSE Add README and LICENSE 2020-09-23 17:14:27 +08:00
NOTES.md Add breakdown of cmp_wrap() for reference 2020-10-22 11:27:08 +08:00
README.md Add mention of Nix in "Running the verification tasks" 2020-10-23 10:43:43 +08:00
shell.nix Update shell.nix 2020-10-08 13:52:35 +08:00

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

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 environment by running nix-shell and do

$ python -m rtio.test.sed.output_network

Progress

  • Devise a suitable migration strategy for artiq.gateware.rtio from Migen to nMigen
  • Implement the core in nMigen
    • rtio.cri (Interface and CRIDecoder only)
    • rtio.rtlink
    • rtio.sed.layouts
    • rtio.sed.output_network
    • rtio.sed.output_driver
  • Add suitable assertions for verification (BMC / unbounded proof?)
    • rtio.cri (Interface and CRIDecoder only)
    • rtio.rtlink
    • rtio.sed.layouts
    • rtio.sed.output_network - Sorting network (high priority)
    • rtio.sed.output_driver
  • Restructure to code to follow nMigen convention and re-validate existing assertions

License

Copyright (C) 2020 M-Labs Limited.

LGPLv3 or any later version