PEak: A Single Source of Truth for Hardware Design and Verification

on YouTube ↗12m

" summary

PEak is an open-source Python DSL that claims a single source of truth by generating an executable Python model, a SMT formal model, and Magma RTL generation from one specification. The system translates algebraic instruction types and register logic into symbolic SMT queries (checks for existence of counterexamples) to prove properties like reg1 == in1, and it emits RTL used in fabricated chips (Amber, Onyx) and in automated compiler-synthesis and design-space-exploration flows that successfully ran.

AI-written summary · about

" chapters (9)

1. 0:00PEak introduction
2. 1:44Ideal hardware specs
3. 4:15Hardware types and representations
4. 5:45Functional verification with Python
5. 8:51Formal verification with SMT
6. 9:54Real-world chips
7. 10:16Compiler synthesis with models
8. 11:20Design space exploration
9. 12:01Summary