The esim hardware verification tutorial.
The ESIM tutorial walks through the verification of some very simple hardware designs using Centaur's ESIM books. These hardware designs are all contrived and are far simpler than real hardware. But this makes them easy to understand and verify.
The ESIM tutorial is meant to be followed along with interactively. To begin, please go to this file:
centaur/esim/tutorial/intro.lisp
in your ACL2 books directory (sometimes called