basic-def.lispISA-def.lispMA2-def.lispMAETT-def.lispinvariants-def.lispMA2-lemmas.lispMAETT-lemmas.lispMAETT-lemmas1.lispMAETT-lemmas2.lispmemory-inv.lispmodifier.lispwk-inv.lispin-order.lispMI-inv.lispreg-ref.lispISA-comp.lispmisc-inv.lispuniq-inv.lispinvariant-proof.lispcorrectness.lispGraphical Viewer of the FM9801 Verification Scripts

FM9801 Verification Script Map  (Click the file you want to look at!!)

This picture shows the dependency of the files. For instance, in order to prove the lemmas in book reg-ref, we have to use the lemmas proved in book modifier. Note that this dependency is transitive.  For instance, the proof of the lemmas in book reg-ref can use the lemmas proved in memory-inv and MAETT-lemmas.

Book MA2-def defines the microarchitectural design of the FM9801.  Book ISA-def defines the ISA mode.  Register files and the memory are defined in basic-def.   Book MAETT-def provides the definition of our intermediate abstraction, and book invariants-def defines our machine invariant.

Book correctnessis where main theorem is proved.  Look for exintr-correctness-criteria and correctness-criteria for the final theorems.  Invariant Proof layer of the proof structure contains the proof of the inductive invariants.  The invariants are proved individually in various files, and summarized in book invariant-proof.  Book MAETT-lemmas is divided into two sections MAETT-lemmas1 and MAETT-lemmas2. MAETT-lemmas itself is a wrapping file.  Simply, there are too many shared lemmas, and I preferred to separate them in two files so that we can load ACL2 books into the prover more efficiently.

I suggest readers to read the comments of the proof scripts.  Important lemmas has comments so that the reader can get an intuitive idea what has been proven by each lemma.  (Note: the comments are not complete at this moment. This is still an unpolished version.  We will continue to revise it.  So be patient, and send e-mail for more info.  I will write more comments.)

To see individual books, please click the rectangles in the figure, or the file names below.

The figure above does not show all the books used in the FM9801 verification.  There are files that prove the basic lemmas: and the books that verify multiplies, which is not a part of the original FM9801 design.