Formal Verification of Pipelined Synthesized Designs by Exploiting Intermediary RTLs

Y. Kim, S. Tosun, H. Koc, S. Kopuri, and N. Mansouri

References

  1. [1] 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
  2. [2] 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.
  3. [3] 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. 219
  4. [4] 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).
  5. [5] M.K. Srivas & M. Bickford, Formal verification of a pipelined microprocessor, IEEE Software, 7(5), 1990, 52–64. doi:10.1109/52.57892
  6. [6] J. Burch & D. Dill, Automatic verification of pipelined microprocessor control, Conf. on Computer-Aided Verification, Stanford, CA, 1994, 68–80.
  7. [7] 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.
  8. [8] J. Sawada, Formal verification of pipelined machines with out-of-order execution, Technical Rep., University of Texas at Austin, Computer Science Department, Austin, TX.
  9. [9] 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.
  10. [10] T. Seceleanu & J. Plosila, Formal pipeline design, in T. Margaria & T. Melham (Eds.), Correct hardware design and verification methods (2001), 167–172.
  11. [11] J. Lewitt & K. Olukotun, A scalable formal verification methodology for pipelined microprocessors, 33rd Design Automation Conf. (ACM: Las Vegas, NE, 1996), 558-563.

Important Links:

Go Back