Interesting: https://github.com/acl2/acl2/tree/master/books/rtl

"This directory contains an ACL2 library of register-transfer logic, developed at #AMD from 1995 to 2011, at #Intel from 2012 to 2016, and at #Arm from 2016 to the present, in support of the mechanical verification of floating-point arithmetic units designed during those periods by the respective companies."

For those who don't know, #ACL2 is a theorem prover in #CommonLisp.

#Lisp #FormalVerifcation #RTL #HardwareEngineering #Semiconductors