From 1d5ee12431b4f0de057ad2c58dda8754d24d6c79 Mon Sep 17 00:00:00 2001
From: Donald Sebastian Leung <dl@m-labs.hk>
Date: Wed, 11 Nov 2020 13:59:40 +0800
Subject: [PATCH] Measure completion time for each unbounded proof

---
 README.md                       | 21 ++-------------------
 rtio/test/sed/output_network.py |  7 +++++++
 2 files changed, 9 insertions(+), 19 deletions(-)

diff --git a/README.md b/README.md
index 1050166..6c26eea 100644
--- a/README.md
+++ b/README.md
@@ -11,30 +11,13 @@ Formally verified implementation of the ARTIQ 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
+To run the verification tasks for the sorting network (unbounded proofs with variable numbers of lanes), 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
-- - [ ] `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
+This should complete in under an hour. The time to complete each verification task (2 lanes, 4 lanes, 8 lanes) is printed to standard output.
 
 ## License
 
diff --git a/rtio/test/sed/output_network.py b/rtio/test/sed/output_network.py
index 9e61aa2..514830a 100644
--- a/rtio/test/sed/output_network.py
+++ b/rtio/test/sed/output_network.py
@@ -2,6 +2,7 @@ from nmigen import *
 from nmigen.asserts import *
 from nmigen.test.utils import *
 from ...sed.output_network import *
+from datetime import datetime
 
 """
 Verification tasks for OutputNetwork
@@ -107,14 +108,20 @@ class OutputNetworkSpec(Elaboratable):
 
 class OutputNetworkTestCase(FHDLTestCase):
     def verify(self):
+        startTime = datetime.now()
         self.assertFormal(
             OutputNetworkSpec(2, 2, [("data", 32), ("channel", 3)]),
             mode="prove", depth=latency(2))
+        print("Verification of sorting network with 2 lanes completed in %f ms" % ((datetime.now() - startTime).total_seconds() * 1000))
+        startTime = datetime.now()
         self.assertFormal(
             OutputNetworkSpec(4, 2, [("data", 32), ("channel", 3)]),
             mode="prove", depth=latency(4))
+        print("Verification of sorting network with 4 lanes completed in %f ms" % ((datetime.now() - startTime).total_seconds() * 1000))
+        startTime = datetime.now()
         self.assertFormal(
             OutputNetworkSpec(8, 2, [("data", 32), ("channel", 3)]),
             mode="prove", depth=latency(8))
+        print("Verification of sorting network with 8 lanes completed in %f ms" % ((datetime.now() - startTime).total_seconds() * 1000))
 
 OutputNetworkTestCase().verify()