3 ms·
Have there been any attempts to use generative testing (e.g. quickcheck) or dependent types to verify processors? I am not sure how quite how this would be inte
by bgorman 7y ago
Have there been any attempts to use generative testing (e.g. quickcheck) or dependent types to verify processors? I am not sure how quite how this would be integrated into the synthesis of the processor, but it seems to be in line with the general "declarative" approach to building RTL through VHDL I remember from undergrad.
- 9q9 7y agoThere is a lot of random testing in processor design. To what extent you'd call it property-based testing can be argued. Intersting factoid: Koen Claessen, one of QuickCheck's inventors, also co-designed Lava, a circuit designer DSL in the Haskell eco-system. If by dependent types you mean theorem provers, then that is used, but rarely -- hand-verification doesn't scale to modern processors, usually you model check against some temporal logic formulas that the processor meets its specification. If OTOH you mean using HDLs (= hardware description languages) that use dependent types, then mostly not. Arm's ASL (= Architecture Specification Language) has a tiny bit of dependency build in to reason about length of bit vectors.