
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Sudarshan K. Srinivasan, "Automatic Refinement Checking of Pipelines with OutofOrder Execution," IEEE Transactions on Computers, vol. 59, no. 8, pp. 11381144, August, 2010.  
BibTex  x  
@article{ 10.1109/TC.2010.18, author = {Sudarshan K. Srinivasan}, title = {Automatic Refinement Checking of Pipelines with OutofOrder Execution}, journal ={IEEE Transactions on Computers}, volume = {59}, number = {8}, issn = {00189340}, year = {2010}, pages = {11381144}, doi = {http://doi.ieeecomputersociety.org/10.1109/TC.2010.18}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Computers TI  Automatic Refinement Checking of Pipelines with OutofOrder Execution IS  8 SN  00189340 SP1138 EP1144 EPD  11381144 A1  Sudarshan K. Srinivasan, PY  2010 KW  Pipelined machine verification KW  refinement KW  outoforder execution. VL  59 JA  IEEE Transactions on Computers ER   
[1] AMD Opteron "x86, 64Bit Processors for Servers and Workstations," http://www.amd.com/usen/Processors/ProductInformation 030_118_ 8825,00.html , 2008.
[2] T. Arons, "Verification of an Advanced MipsType OutofOrder Execution Algorithm," Proc. Int'l Conf. ComputerAided Verification (CAV '04), pp. 414426, 2004.
[3] T. Arons and A. Pnueli, "A Comparison of Two Verification Methods for Speculative Instruction Execution," Proc. Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS '00), pp. 487502, Mar. 2000.
[4] R.E. Bryant, S.K. Lahiri, and S. Seshia, "Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions," Proc. Int'l Conf. ComputerAided Verification (CAV '02), pp. 7892, 2002.
[5] J.R. Burch and D.L. Dill, "Automatic Verification of Pipelined Microprocessor Control," Proc. Int'l Conf. ComputerAided Verification (CAV '94), pp. 6880, 1994.
[6] A.C.J. Fox, "Formal Specification and Verification of ARM6," Lecture Notes in Computer Science, vol. 2758, pp. 2540, Springer Berlin/Heidelberg 2003.
[7] R. Hosabettu, M. Srivas, and G. Gopalakrishnan, "Proof of Correctness of a Processor with Reorder Buffer Using the Completion Functions Approach," Proc. Int'l Conf. ComputerAided Verification (CAV '99), pp. 4759, 1999.
[8] W.A. Hunt and J. Sawada, "Verifying the FM9801 Microarchitecture," IEEE Micro, vol. 19, no. 3, pp. 4755, May 1999.
[9] Intel, "Core 2 Duo Processor Overview," http://www.intel.com/products/ processor/ core2duoindex.htm, 2008.
[10] R.B. Jones, J.U. Skakkebæk, and D.L. Dill, "Formal Verification of OutofOrder Execution with Incremental Flushing," Formal Methods in System Design, Special Issue on Microprocessor Verification, vol. 20, no. 2, pp. 139158, Mar. 2002.
[11] R. Kane, P. Manolios, and S.K. Srinivasan, "Monolithic Verification of Deep Pipelines with Collapsed Flushing," Proc. Conf. Design, Automation and Test in Europe (DATE '06), pp. 12341239, 2006.
[12] M. Kaufmann, P. Manolios, and J.S. Moore, ComputerAided Reasoning: An Approach. Kluwer Academic Publishers, July 2000.
[13] D. Kroning, "Formal Verification of Pipelined Microprocessors," PhD thesis, Universität des Saarlandes, 2001.
[14] S. Lahiri, S. Seshia, and R. Bryant, "Modeling and Verification of OutofOrder Microprocessors Using UCLID," Proc. Int'l Conf. Formal Methods in ComputerAided Design (FMCAD '02), pp. 142159, 2002.
[15] P. Manolios, "Correctness of Pipelined Machines," Proc. Int'l Conf. Formal Methods in ComputerAided Design (FMCAD '00), pp. 161178, 2000.
[16] P. Manolios, "Mechanical Verification of Reactive Systems," PhD thesis, Univ. of Texas at Austin, http://www.cc.gatech.edu/~manolios publications.html , Aug. 2001.
[17] P. Manolios, "A Compositional Theory of Refinement for Branching Time," Proc. 12th IFIP WG 10.5 Advanced Research Working Conf. Correct Hardware Design and Verification Methods (CHARME '03), pp. 304318, 2003.
[18] P. Manolios and S.K. Srinivasan, "Automatic Verification of Safety and Liveness for XScaleLike Processor Models Using WEB Refinements," Proc. Conf. Design, Automation and Test in Europe (DATE '04), pp. 168175, 2004.
[19] P. Manolios and S.K. Srinivasan, "A Complete Compositional Reasoning Framework for the Efficient Verification of Pipelined Machines," Proc. IEEE Int'l Conf. ComputerAided Design (ICCAD '05), pp. 863870, 2005.
[20] P. Manolios and S.K. Srinivasan, "A Computationally Efficient Method Based on Commitment Refinement Maps for Verifying Pipelined Machines," Proc. IEEE Int'l Conf. Formal Methods and Models for CoDesign (MEMOCODE '05), pp. 188197, July 2005.
[21] H.I. Shehata and M. Aagaard, "A General Decomposition Strategy for Verifying Register Renaming," Proc. Design Automation Conf. (DAC '04), pp. 234237, 2004.
[22] S.K. Srinivasan, "Efficient Verification of BitLevel Pipelined Machines Using Refinement," PhD thesis, Georgia Inst. of Technology, http://etd.gatech.edu/theses/availableetd08242007111625 /, Dec. 2007.
[23] M.N. Velev, "Using Rewriting Rules and Positive Equality to Formally Verify Wide Issue OutofOrder Microprocessors with a Reorder Buffer," Proc. Conf. Design, Automation and Test in Europe (DATE '02), pp. 2835, 2002.
[24] M.N. Velev, "Using Automatic Case Splits and Efficient CNF Translation to Guide a SatSolver When Formally Verifying OutofOrder Processors," Proc. Int'l Symp. Artificial Intelligence and Math. (AI&M), 2004.
[25] M.N. Velev, "Using Positive Equality to Prove Liveness for Pipelined Microprocessors," Proc. Asia and South Pacific Design Automation Conf. (ASPDAC), pp. 316321, 2004.
[26] M.N. Velev, "Automatic Formal Verification of Liveness for Pipelined Processors with Multicycle Functional Units," Proc. Conf. Correct Hardware Design and Verification Methods (CHARME), pp. 97113, 2005.
[27] Yices, "Home Page," http://fm.csl.sri.comyices, 2007.