There 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

There 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.