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, PVSSystem Guide (SRI International, September 1999). Availableat http://pvs.csl.sri.com/documentation.shtml
  2. [2] N. Mansouri & R. Vemuri, Automated correctness conditiongeneration 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 commercialmicroprocessor, Technical Rep. SRICSL-95-12, SRI ComputerScience Laboratory, Menlo Park, CA, July 1995.219
  4. [4] P.J. Windley & M.L. Coe, A correctness model for pipelinedmicroprocessors, theorem provers in circuit design: Theory,practice, and experience, Lecture Notes in Computer Science901 (Springer Verlag: Bad Herrenalb, Germany, 1994).
  5. [5] M.K. Srivas & M. Bickford, Formal verification of a pipelinedmicroprocessor, IEEE Software, 7(5), 1990, 52–64. doi:10.1109/52.57892
  6. [6] J. Burch & D. Dill, Automatic verification of pipelined mi-croprocessor control, Conf. on Computer-Aided Verification,Stanford, CA, 1994, 68–80.
  7. [7] J. Sawada & W.A.H. Jr., Trace table based approach forpipelined microprocessor verification, 9th Int. Conf. on Com-puter Aided Verification, Haifa, Israel, 1997, 364–375.
  8. [8] J. Sawada, Formal verification of pipelined machines without-of-order execution, Technical Rep., University of Texas atAustin, Computer Science Department, Austin, TX.
  9. [9] S. Tahar & R. Kumar, Formal verification of pipeline conflictsin RISC processors, European Design Automation Conf. (IEEEComputer 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