Making Concurrent Hardware Verification Sequential
summary
Introduces Fjfj, a Bluespec-like language that removes exponential proof cases by separating action methods vs value methods and forbidding multiple action calls to the same module in one rule, yielding sequential module characterizations. Implements the framework in Coq and proves a refinement theorem that composes modules one method at a time. Validates on a pipelined processor, parameterized crossbar, and network switch and reports a static analysis over ~300k lines of Bluespec code with only a few violations.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 0:44Hardware verification modularity
- 2:08Hardware verification challenges
- 3:52BlueCheck methodology
- 5:37Concurrency in BlueCheck
- 7:05Restricting concurrency
- 8:54Refinement and simulation theory
- 9:56Assessing BlueCheck restrictions
- 10:36Verifying processor pipeline
- 12:21Simple processor specs fail
- 13:25Generalizing processor specs
- 15:10Formalizing generalized spec
- 16:11Key insights and future work
- 17:13Q&A
related talks
56mProof Assistants At the Hardware-Software Interface
24mFreeSpec: Specifying, Verifying, and Executing Impure Computations in Coq
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
24mStrong Formal Verification For RISC V: From Instruction Set Manual To RTL
31mFormal Specification
29mTowards Formally Verified Just-In-Time Compilation
24mConcurrent Quantum Separation Logic for Fine-Grained Parallelism
15mMy Journey in Secure Compilation