Executable Formal Models (EFM) Project The Executable Formal Models Project Goal : Single source for simulation and reasoning Modeled the JEM1 in the logic of ACL2 Used model to generate a cycle based simulator Achieved C-like execution speeds Performed simple reasoning over model Explored the border between ACL2 and Common Lisp Conclusion : Optimal performance requires dual mode A Formal Model (ACL2) -or- A Simulator (GCL) Used conditional forms (#+) to direct model creation