M-Labs
/
rtio-nmigen
9
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.
44 Commits
1 Branch
105KB
Branch: master
Branches Tags
${ item.name }
Create branch ${ searchTerm }
from 'master'
${ noResults }
Donald Sebastian Leung 25a8a741bb Refine assertions for case with replacements in sorting network 18 hours ago
rtio Refine assertions for case with replacements in sorting network 18 hours ago
LICENSE Add README and LICENSE 4 weeks ago
NOTES.md Add breakdown of cmp_wrap() for reference 20 hours ago
README.md Add breakdown of cmp_wrap() for reference 20 hours ago
shell.nix Update shell.nix 2 weeks 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

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