rtio-nmigen/README.md

754 B

rtio-nmigen

Formally verified implementation of the ARTIQ 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

License

Copyright (C) 2020 M-Labs Limited.

LGPLv3 or any later version