rtio-nmigen/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](https://nixos.org) environment by running `nix-shell` and do

```bash
$ python -m rtio.test.sed.output_network
```

## Progress

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

## License

Copyright (C) 2020 M-Labs Limited.

[LGPLv3](./LICENSE) or any later version
Add initial README 2020-09-23 17:10:41 +08:00			`# rtio-nmigen`

Add README and LICENSE 2020-09-23 17:14:27 +08:00			`Formally verified implementation of the ARTIQ RTIO core in nMigen`

Add failing trace and trace analysis 2020-10-20 13:05:38 +08:00			`## 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

Add instructions for running verification 2020-10-23 10:39:16 +08:00			`## Running the verification tasks`

Add mention of Nix in "Running the verification tasks" 2020-10-23 10:43:43 +08:00			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](https://nixos.org) environment by running `nix-shell` and do
Add instructions for running verification 2020-10-23 10:39:16 +08:00
			```bash
			`$ python -m rtio.test.sed.output_network`
			```

Add README and LICENSE 2020-09-23 17:14:27 +08:00			`## Progress`

Reset translation progress 2020-09-30 10:55:08 +08:00			- Devise a suitable migration strategy for `artiq.gateware.rtio` from Migen to nMigen
Add rtio.sed.output_driver 2020-10-09 11:16:01 +08:00			`- [x] Implement the core in nMigen`
Fix keyword argument issue for read_port in rtio.cri 2020-10-15 13:11:06 +08:00			- - [x] `rtio.cri` (`Interface` and `CRIDecoder` only)
Add rtio.rtlink 2020-10-07 16:32:20 +08:00			- - [x] `rtio.rtlink`
Add rtio.sed.layouts 2020-10-08 11:06:35 +08:00			- - [x] `rtio.sed.layouts`
Add rtio.sed.output_network 2020-10-08 17:05:04 +08:00			- - [x] `rtio.sed.output_network`
Add rtio.sed.output_driver 2020-10-09 11:16:01 +08:00			- - [x] `rtio.sed.output_driver`
Add README and LICENSE 2020-09-23 17:14:27 +08:00			`- [ ] Add suitable assertions for verification (BMC / unbounded proof?)`
Update README 2020-10-14 16:50:01 +08:00			- - [ ] `rtio.cri` (`Interface` and `CRIDecoder` only)
Update README 2020-10-23 11:15:47 +08:00			- - [x] `rtio.sed.output_network` - Sorting network (high priority)
Fix broken markdown in README 2020-10-14 16:50:57 +08:00			- - [ ] `rtio.sed.output_driver`
Restructure rtio.sed.output_driver to follow nMigen convention 2020-10-27 13:33:41 +08:00			`- [x] Restructure to code to follow nMigen convention and re-validate existing assertions (if any)`
Restructure rtio.cri to follow nMigen convention 2020-10-27 12:14:47 +08:00			- - [x] `rtio.cri` (`Interface` and `CRIDecoder` only)
Rewrite sorting network to follow nMigen convention 2020-10-23 14:57:29 +08:00			- - [x] `rtio.sed.output_network`
Restructure rtio.sed.output_driver to follow nMigen convention 2020-10-27 13:33:41 +08:00			- - [x] `rtio.sed.output_driver`
Update README with next objective 2020-10-29 13:32:54 +08:00			`- [ ] Simulate RTIO command for switching TTL`
Add README and LICENSE 2020-09-23 17:14:27 +08:00
			`## License`

			`Copyright (C) 2020 M-Labs Limited.`

Update README.md 2020-09-23 17:16:58 +08:00			`[LGPLv3](./LICENSE) or any later version`