Simulator vs. Specification
Verification
• We are building a verified simulator for SDL
specifications – one-time effort
• Design engineers can use the simulator  to
verify SDL specifications – multiple
verification efforts on multiple designs
• ACL2 used in both cases