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 **correctness**is 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.

- basic-def.lisp
- ISA-def.lisp
- MA2-def.lisp
- MA2-lemmas.lisp
- MAETT-def.lisp
- invariants-def.lisp
- MAETT-lemmas.lisp
- MAETT-lemmas1.lisp
- MAETT-lemmas2.lisp
- modifier.lisp
- reg-ref.lisp
- in-order.lisp
- MI-inv.lisp
- ISA-comp.lisp
- memory-inv.lisp
- misc-inv.lisp
- uniq-inv.lisp
- wk-inv.lisp
- invariant-proof.lisp
- correctness.lisp