"Using the ACL2 Theorem Prover to Reason about VHDL Components."

Vanderlei Moraes Rodrigues, Dominique Borrione, Philippe Georgelin (2000)
a service of Schloss Dagstuhl - Leibniz Center for Informatics