Limit no. of parallel processes to prevent thrashing

README.md

@@ -27,17 +27,18 @@ This should run the tests (cache, multiplier, divider) provided by Minerva itsel
 $ python -m rvfi.cores.minerva.verify
 ```
 
+Note that a pool of `# of cores on your machine` processes is created by default which enables the verification tasks to execute in parallel. The number of processes in the pool can be configured by passing in a command-line argument, e.g.
+
+```bash
+$ python -m rvfi.cores.minerva.verify 8
+```
+
+creates a pool of 8 processes.
+
 ## Scope
 
 The RV32I, RV32M, RV64I and RV64M ISAs are currently implemented but only RV32IM are being tested by integrating with the Minerva core.
 
-## Possible improvements
-
-In no particular order:
-
-- Allow configurable limit for no. of running processes in order to prevent thrashing
-- Combine individual instruction checks into single ISA check (currently, doing so takes forever even when depth is set to only `20`)
-
 ## License
 
 See [LICENSE](./LICENSE)

rvfi/cores/minerva/verify.py

@@ -53,7 +53,14 @@ from ...insns.insn_divu import *
 from ...insns.insn_rem import *
 from ...insns.insn_remu import *
 from collections import namedtuple
-from multiprocessing import Process
+from multiprocessing import Pool
+import sys
+import os
+
+if len(sys.argv) == 1:
+    processes = os.cpu_count()
+else:
+    processes = int(sys.argv[1])
 
 RISCVFormalParameters = namedtuple('RISCVFormalParameters',
     ['ilen', 'xlen', 'csr_misa', 'compressed', 'aligned_mem', 'altops'])
@@ -123,67 +130,6 @@ class InsnSpec(Elaboratable):
 
         return m
 
-class InsnTestCase(FHDLTestCase):
-    def verify(self):
-        def verify_insn(insn_spec, spec_name):
-            self.assertFormal(InsnSpec(insn_spec), mode="cover", depth=20, spec_name=spec_name)
-            self.assertFormal(InsnSpec(insn_spec), mode="bmc", depth=20, spec_name=spec_name)
-            print("%s PASS" % spec_name)
-        insns = [
-            (InsnLui, "verify_lui"),
-            (InsnAuipc, "verify_auipc"),
-            (InsnJal, "verify_jal"),
-            (InsnJalr, "verify_jalr"),
-            (InsnBeq, "verify_beq"),
-            (InsnBne, "verify_bne"),
-            (InsnBlt, "verify_blt"),
-            (InsnBge, "verify_bge"),
-            (InsnBltu, "verify_bltu"),
-            (InsnBgeu, "verify_bgeu"),
-            (InsnLb, "verify_lb"),
-            (InsnLh, "verify_lh"),
-            (InsnLw, "verify_lw"),
-            (InsnLbu, "verify_lbu"),
-            (InsnLhu, "verify_lhu"),
-            (InsnSb, "verify_sb"),
-            (InsnSh, "verify_sh"),
-            (InsnSw, "verify_sw"),
-            (InsnAddi, "verify_addi"),
-            (InsnSlti, "verify_slti"),
-            (InsnSltiu, "verify_sltiu"),
-            (InsnXori, "verify_xori"),
-            (InsnOri, "verify_ori"),
-            (InsnAndi, "verify_andi"),
-            (InsnSlli, "verify_slli"),
-            (InsnSrli, "verify_srli"),
-            (InsnSrai, "verify_srai"),
-            (InsnAdd, "verify_add"),
-            (InsnSub, "verify_sub"),
-            (InsnSll, "verify_sll"),
-            (InsnSlt, "verify_slt"),
-            (InsnSltu, "verify_sltu"),
-            (InsnXor, "verify_xor"),
-            (InsnSrl, "verify_srl"),
-            (InsnSra, "verify_sra"),
-            (InsnOr, "verify_or"),
-            (InsnAnd, "verify_and"),
-            (InsnMul, "verify_mul"),
-            (InsnMulh, "verify_mulh"),
-            (InsnMulhsu, "verify_mulhsu"),
-            (InsnMulhu, "verify_mulhu"),
-            (InsnDiv, "verify_div"),
-            (InsnDivu, "verify_divu"),
-            (InsnRem, "verify_rem"),
-            (InsnRemu, "verify_remu")
-        ]
-        ps = []
-        for insn_spec, spec_name in insns:
-            p = Process(target=verify_insn, args=(insn_spec,spec_name))
-            ps.append(p)
-            p.start()
-        for p in ps:
-            p.join()
-
 class PcFwdSpec(Elaboratable):
     def elaborate(self, platform):
         m = Module()
@@ -502,6 +448,70 @@ class UniqueTestCase(FHDLTestCase):
         self.assertFormal(UniqueSpec(), mode="bmc", depth=25, spec_name="verify_uniqueness")
         print("verify_uniqueness PASS")
 
+def verify_insn(testcase, insn_spec, spec_name):
+    testcase.assertFormal(InsnSpec(insn_spec), mode="cover", depth=20, spec_name=spec_name)
+    testcase.assertFormal(InsnSpec(insn_spec), mode="bmc", depth=20, spec_name=spec_name)
+    print("%s PASS" % spec_name)
+
+class MinervaTestCase(FHDLTestCase):
+    def verify(self):
+        with Pool(processes=processes) as pool:
+            insns = [
+                (InsnLui, "verify_lui"),
+                (InsnAuipc, "verify_auipc"),
+                (InsnJal, "verify_jal"),
+                (InsnJalr, "verify_jalr"),
+                (InsnBeq, "verify_beq"),
+                (InsnBne, "verify_bne"),
+                (InsnBlt, "verify_blt"),
+                (InsnBge, "verify_bge"),
+                (InsnBltu, "verify_bltu"),
+                (InsnBgeu, "verify_bgeu"),
+                (InsnLb, "verify_lb"),
+                (InsnLh, "verify_lh"),
+                (InsnLw, "verify_lw"),
+                (InsnLbu, "verify_lbu"),
+                (InsnLhu, "verify_lhu"),
+                (InsnSb, "verify_sb"),
+                (InsnSh, "verify_sh"),
+                (InsnSw, "verify_sw"),
+                (InsnAddi, "verify_addi"),
+                (InsnSlti, "verify_slti"),
+                (InsnSltiu, "verify_sltiu"),
+                (InsnXori, "verify_xori"),
+                (InsnOri, "verify_ori"),
+                (InsnAndi, "verify_andi"),
+                (InsnSlli, "verify_slli"),
+                (InsnSrli, "verify_srli"),
+                (InsnSrai, "verify_srai"),
+                (InsnAdd, "verify_add"),
+                (InsnSub, "verify_sub"),
+                (InsnSll, "verify_sll"),
+                (InsnSlt, "verify_slt"),
+                (InsnSltu, "verify_sltu"),
+                (InsnXor, "verify_xor"),
+                (InsnSrl, "verify_srl"),
+                (InsnSra, "verify_sra"),
+                (InsnOr, "verify_or"),
+                (InsnAnd, "verify_and"),
+                (InsnMul, "verify_mul"),
+                (InsnMulh, "verify_mulh"),
+                (InsnMulhsu, "verify_mulhsu"),
+                (InsnMulhu, "verify_mulhu"),
+                (InsnDiv, "verify_div"),
+                (InsnDivu, "verify_divu"),
+                (InsnRem, "verify_rem"),
+                (InsnRemu, "verify_remu")
+            ]
+            tasks = [pool.apply_async(verify_insn, (self, insn_spec, spec_name)) for insn_spec, spec_name in insns]
+            tasks.append(pool.apply_async(PcFwdTestCase().verify))
+            tasks.append(pool.apply_async(PcBwdTestCase().verify))
+            tasks.append(pool.apply_async(RegTestCase().verify))
+            tasks.append(pool.apply_async(CausalTestCase().verify))
+            tasks.append(pool.apply_async(LivenessTestCase().verify))
+            tasks.append(pool.apply_async(UniqueTestCase().verify))
+            [p.get() for p in tasks]
+
 print('*' * 80)
 print('*' + ' ' * 78 + '*')
 print('*                        Verifying the Minerva core ...                        *')
@@ -509,40 +519,14 @@ print('*' + ' ' * 78 + '*')
 print('*' * 80)
 
 print("Verifying RV32M instructions ...")
-p_insn = Process(target=InsnTestCase().verify)
-p_insn.start()
-
 print("Verifying PC forward checks ...")
-p_pc_fwd = Process(target=PcFwdTestCase().verify)
-p_pc_fwd.start()
-
 print("Verifying PC backward checks ...")
-p_pc_bwd = Process(target=PcBwdTestCase().verify)
-p_pc_bwd.start()
-
 print("Verifying register checks ...")
-p_reg = Process(target=RegTestCase().verify)
-p_reg.start()
-
 print("Verifying causal checks ...")
-p_causal = Process(target=CausalTestCase().verify)
-p_causal.start()
-
 print("Verifying liveness checks ...")
-p_liveness = Process(target=LivenessTestCase().verify)
-p_liveness.start()
-
 print("Verifying uniqueness checks ...")
-p_uniqueness = Process(target=UniqueTestCase().verify)
-p_uniqueness.start()
 
-p_insn.join()
+MinervaTestCase().verify()
-p_pc_fwd.join()
-p_pc_bwd.join()
-p_reg.join()
-p_causal.join()
-p_liveness.join()
-p_uniqueness.join()
 
 print('*' * 80)
 print('*' + ' ' * 78 + '*')