From 978a620cc62ad0615878255733a4a44b653523b3 Mon Sep 17 00:00:00 2001
From: Donald Sebastian Leung
Date: Mon, 21 Sep 2020 13:45:36 +0800
Subject: [PATCH] Limit no. of parallel processes to prevent thrashing
---
README.md | 15 ++--
rvfi/cores/minerva/verify.py | 162 ++++++++++++++++-------------------
2 files changed, 81 insertions(+), 96 deletions(-)
diff --git a/README.md b/README.md
index 42b2c99..684f11d 100644
--- a/README.md
+++ b/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)
diff --git a/rvfi/cores/minerva/verify.py b/rvfi/cores/minerva/verify.py
index acc7916..29119ae 100644
--- a/rvfi/cores/minerva/verify.py
+++ b/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()
-p_pc_fwd.join()
-p_pc_bwd.join()
-p_reg.join()
-p_causal.join()
-p_liveness.join()
-p_uniqueness.join()
+MinervaTestCase().verify()
print('*' * 80)
print('*' + ' ' * 78 + '*')