Formally verified ARTIQ RTIO core in nMigen
Go to file
Donald Sebastian Leung bf08fe1d50 Add partial implementation of lane distributor 2020-09-28 11:36:26 +08:00
rtio Add partial implementation of lane distributor 2020-09-28 11:36:26 +08:00
LICENSE Add README and LICENSE 2020-09-23 17:14:27 +08:00
README.md Remove redundant 'artiq.gateware' from module names 2020-09-25 15:10:07 +08:00
shell.nix Add shell.nix 2020-09-24 15:11:24 +08:00

README.md

rtio-nmigen

Formally verified implementation of the ARTIQ RTIO core in nMigen

Progress

  • Implement the core in nMigen
    • rtio.core
    • rtio.cri
    • rtio.rtlink
    • rtio.channel
    • rtio.sed.core
    • rtio.sed.layouts
    • rtio.sed.lane_distributor
    • rtio.sed.fifos
    • rtio.sed.gates
    • rtio.sed.output_driver
    • rtio.sed.output_network
    • rtio.input_collector
  • Add suitable assertions for verification (BMC / unbounded proof?)

License

Copyright (C) 2020 M-Labs Limited.

LGPLv3 or any later version