ACL2
ACL2 is a {theorem prover} based on Common Lisp commonly used for the verification of hardware.
[The wiki] is an excellent source of information on the language.
[This work] discusses the verification of AIG graph representations of boolean functions.
[This page] has good programming exercises for ACL2.
Often used in {Emacs} with [Proof General].
[Introduction to ACL2 programming.]
[Computer Aided Reasoning], the textbook out of UT, is likely worth spending time reading as well.
[Pete's site for Computer-Aided Reasoning]: lots of good resources for ACL2/S and working with the technology. Add his setup - or some modification of it - to your emacs configuration as a module!