github.com/coq/opam-coq-archive
Some proofs of hardware (adder, multiplier, memory block instruction)
opam install coq-circuits.8.10.0