SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
  SRI Logo

Microprocessor Verification in PVS
 by David Cryluk.

In the past we have verified a variety of different hardware circuits using different verification systems. In this paper we report on one such verification. The verification is that of a simple pipelined microprocessor first verified in [8]. We use this example as a vehicle for exploring a general methodology of verifying state machine systems in the PVS verification system. It is our hope that such a methodology can be extended to verify the correctness of actual commercial microprocessors.


About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2018 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy