M-Labs/rtio-nmigen
7
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
Formally verified ARTIQ RTIO core in nMigen
44 Commits 1 Branch 0 Tags 98 KiB
Python 98.3%
Nix 1.7%
25a8a741bb
Go to file
Donald Sebastian Leung 25a8a741bb Refine assertions for case with replacements in sorting network
2020-10-22 13:32:12 +08:00
rtio Refine assertions for case with replacements in sorting network 2020-10-22 13:32:12 +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 breakdown of cmp_wrap() for reference 2020-10-22 11:27:08 +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

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