References
- S. Owre, N. Shankar, J. Rushby, & D. Stringer-Calvert, PVS System Guide (SRI International, September 1999). Available at http://pvs.csl.sri.com/documentation.shtml
- N. Mansouri & R. Vemuri, Automated correctness condition generation for formal verification of synthesized RTL designs, Journal of Formal Methods in System Design (FMSD), 16(1), Special issue on Formal Methods in Computer-Aided Design, January 2000.
- M.K. Srivas & S.P. Miller, Formal verification of a commercial microprocessor, Technical Rep. SRICSL-95-12, SRI Computer Science Laboratory, Menlo Park, CA, July 1995.
- P.J. Windley & M.L. Coe, A correctness model for pipelined microprocessors, theorem provers in circuit design: Theory, practice, and experience, Lecture Notes in Computer Science 901 (Springer Verlag: Bad Herrenalb, Germany, 1994).
- M.K. Srivas & M. Bickford, Formal verification of a pipelined microprocessor, IEEE Software, 7(5), 1990, 52–64.
- J. Burch & D. Dill, Automatic verification of pipelined microprocessor control, Conf. on Computer-Aided Verification, Stanford, CA, 1994, 68–80.
- J. Sawada & W.A.H. Jr., Trace table based approach for pipelined microprocessor verification, 9th Int. Conf. on Computer Aided Verification, Haifa, Israel, 1997, 364–375.
- J. Sawada, Formal verification of pipelined machines with out-of-order execution, Technical Rep., University of Texas at Austin, Computer Science Department, Austin, TX .
- S. Tahar & R. Kumar, Formal verification of pipeline conflicts in RISC processors, European Design Automation Conf. (IEEE Computer Society Press: Grenoble, France, 1994), 285–289.
- T. Seceleanu & J. Plosila, Formal pipeline design, in T. Margaria & T. Melham (Eds.), Correct hardware design and verification methods (2001), 167–172.
- J. Lewitt & K. Olukotun, A scalable formal verification methodology for pipelined microprocessors, 33rd Design Automation Conf. (ACM: Las Vegas, NE, 1996), 558–563.