Nerv: Probabilistic Dynamic Partial Order Reduction for Hardware
summary
Proposes probabilistic dynamic partial order reduction that records state transitions from warm-up runs, builds a probability table over transaction pairs, and samples transactions to fill reordered clock-cycle slots; implemented as a pure Verilog stimulus generator that plugs into existing simulators, periodically cools probabilities to escape local minima, and targets synchronous RTL with many interfaces. Claims scale improvements over formal DPOR, reports integration work with cocotb being slow and plans to drive tests with CSMC and compare to prior POR and fuzzers.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 0:16What is Partial Order Reduction
- 0:47Scheduling Partial Order Reduction
- 1:22Multiple Read Writes
- 1:44Linearization
- 3:23Hardware
- 5:32Synchronous
- 5:58Generalization
- 8:15Architecture
- 9:19Conclusion
related talks
16mA Pragmatic Approach to Stateful Partial Order Reduction
20mTruly Stateless, Optimal Dynamic Partial Order Reduction
23mRandomized Testing of Distributed Systems with Probabilistic Guarantees
19mState Space Estimation for DPOR-Based Model Checkers
34mSymbolic Execution for Randomized Programs
22mCompositional Programming and Testing of Dynamic Distributed Systems
40mTesting Distributed Systems w/ Deterministic Simulation
12mRISC-V: Hardcore/Softcore Co-Simulation Environment with Cycle-Accurate Rollback