From 425bc49784437131fa909be571c8414d315f482b Mon Sep 17 00:00:00 2001
From: Donald Sebastian Leung <dl@m-labs.hk>
Date: Fri, 18 Sep 2020 15:59:59 +0800
Subject: [PATCH] Parallelize all verification tasks for Minerva

---
 README.md                    |  2 --
 rvfi/cores/minerva/verify.py | 59 ++++++++++++++++++++++++------------
 2 files changed, 40 insertions(+), 21 deletions(-)

diff --git a/README.md b/README.md
index 8a8ebd9..f3f5af5 100644
--- a/README.md
+++ b/README.md
@@ -27,8 +27,6 @@ This should run the tests (cache, multiplier, divider) provided by Minerva itsel
 $ python -m rvfi.cores.minerva.verify
 ```
 
-This should complete within 2 hours.
-
 ## Scope
 
 The RV32I, RV32M, RV64I and RV64M ISAs are currently implemented but only RV32IM are being tested by integrating with the Minerva core.
diff --git a/rvfi/cores/minerva/verify.py b/rvfi/cores/minerva/verify.py
index 5248325..acc7916 100644
--- a/rvfi/cores/minerva/verify.py
+++ b/rvfi/cores/minerva/verify.py
@@ -230,8 +230,9 @@ class PcFwdSpec(Elaboratable):
 
 class PcFwdTestCase(FHDLTestCase):
     def verify(self):
-        self.assertFormal(PcFwdSpec(), mode="cover", depth=20)
-        self.assertFormal(PcFwdSpec(), mode="bmc", depth=20)
+        self.assertFormal(PcFwdSpec(), mode="cover", depth=20, spec_name="verify_pc_fwd")
+        self.assertFormal(PcFwdSpec(), mode="bmc", depth=20, spec_name="verify_pc_fwd")
+        print("verify_pc_fwd PASS")
 
 class PcBwdSpec(Elaboratable):
     def elaborate(self, platform):
@@ -279,8 +280,9 @@ class PcBwdSpec(Elaboratable):
 
 class PcBwdTestCase(FHDLTestCase):
     def verify(self):
-        self.assertFormal(PcBwdSpec(), mode="cover", depth=20)
-        self.assertFormal(PcBwdSpec(), mode="bmc", depth=20)
+        self.assertFormal(PcBwdSpec(), mode="cover", depth=20, spec_name="verify_pc_bwd")
+        self.assertFormal(PcBwdSpec(), mode="bmc", depth=20, spec_name="verify_pc_bwd")
+        print("verify_pc_bwd PASS")
 
 class RegSpec(Elaboratable):
     def elaborate(self, platform):
@@ -330,8 +332,9 @@ class RegSpec(Elaboratable):
 
 class RegTestCase(FHDLTestCase):
     def verify(self):
-        self.assertFormal(RegSpec(), mode="cover", depth=10)
-        self.assertFormal(RegSpec(), mode="bmc", depth=10)
+        self.assertFormal(RegSpec(), mode="cover", depth=10, spec_name="verify_reg")
+        self.assertFormal(RegSpec(), mode="bmc", depth=10, spec_name="verify_reg")
+        print("verify_reg PASS")
 
 class CausalSpec(Elaboratable):
     def elaborate(self, platform):
@@ -378,8 +381,9 @@ class CausalSpec(Elaboratable):
 
 class CausalTestCase(FHDLTestCase):
     def verify(self):
-        self.assertFormal(CausalSpec(), mode="cover", depth=20)
-        self.assertFormal(CausalSpec(), mode="bmc", depth=20)
+        self.assertFormal(CausalSpec(), mode="cover", depth=20, spec_name="verify_causal")
+        self.assertFormal(CausalSpec(), mode="bmc", depth=20, spec_name="verify_causal")
+        print("verify_causal PASS")
 
 class LivenessSpec(Elaboratable):
     def elaborate(self, platform):
@@ -444,8 +448,9 @@ class LivenessSpec(Elaboratable):
 
 class LivenessTestCase(FHDLTestCase):
     def verify(self):
-        self.assertFormal(LivenessSpec(), mode="cover", depth=40)
-        self.assertFormal(LivenessSpec(), mode="bmc", depth=40)
+        self.assertFormal(LivenessSpec(), mode="cover", depth=40, spec_name="verify_liveness")
+        self.assertFormal(LivenessSpec(), mode="bmc", depth=40, spec_name="verify_liveness")
+        print("verify_liveness PASS")
 
 class UniqueSpec(Elaboratable):
     def elaborate(self, platform):
@@ -493,8 +498,9 @@ class UniqueSpec(Elaboratable):
 
 class UniqueTestCase(FHDLTestCase):
     def verify(self):
-        self.assertFormal(UniqueSpec(), mode="cover", depth=25)
-        self.assertFormal(UniqueSpec(), mode="bmc", depth=25)
+        self.assertFormal(UniqueSpec(), mode="cover", depth=25, spec_name="verify_uniqueness")
+        self.assertFormal(UniqueSpec(), mode="bmc", depth=25, spec_name="verify_uniqueness")
+        print("verify_uniqueness PASS")
 
 print('*' * 80)
 print('*' + ' ' * 78 + '*')
@@ -503,25 +509,40 @@ print('*' + ' ' * 78 + '*')
 print('*' * 80)
 
 print("Verifying RV32M instructions ...")
-InsnTestCase().verify()
+p_insn = Process(target=InsnTestCase().verify)
+p_insn.start()
 
 print("Verifying PC forward checks ...")
-PcFwdTestCase().verify()
+p_pc_fwd = Process(target=PcFwdTestCase().verify)
+p_pc_fwd.start()
 
 print("Verifying PC backward checks ...")
-PcBwdTestCase().verify()
+p_pc_bwd = Process(target=PcBwdTestCase().verify)
+p_pc_bwd.start()
 
 print("Verifying register checks ...")
-RegTestCase().verify()
+p_reg = Process(target=RegTestCase().verify)
+p_reg.start()
 
 print("Verifying causal checks ...")
-CausalTestCase().verify()
+p_causal = Process(target=CausalTestCase().verify)
+p_causal.start()
 
 print("Verifying liveness checks ...")
-LivenessTestCase().verify()
+p_liveness = Process(target=LivenessTestCase().verify)
+p_liveness.start()
 
 print("Verifying uniqueness checks ...")
-UniqueTestCase().verify()
+p_uniqueness = Process(target=UniqueTestCase().verify)
+p_uniqueness.start()
+
+p_insn.join()
+p_pc_fwd.join()
+p_pc_bwd.join()
+p_reg.join()
+p_causal.join()
+p_liveness.join()
+p_uniqueness.join()
 
 print('*' * 80)
 print('*' + ' ' * 78 + '*')