A Coq framework to support implementing, specifying, verifying, and compiling Bluespec-style hardware components with high developer productivity.