Mixing Symbolic and Ternary Simulation Techniques for the Verification of Processor-Based Systems
Resumo
We present a new technique to support processor validation and verification in absence of information when modeling reactive systems. Current processor validation techniques will not tolerate absence of information for some of its registers. In order to overcome this problem we combine symbolic simulation with temary logic simulation techniques. We exemplify our technique by simulating an Application Specific lnstruction Processor(ASIP) core with its embedded logic.
Referências
C. H. Seger and R. E. Bryant. Formal Verification by Symbolic Evaluation of Partially. Ordered Trajectories. Technical Report 93-08, Department of Computer Science, University of British Columbia, July 1993.
R. E. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, pages 293-318, September 1992.
R. Lipsett, C. Schaefer and C. Ussery. VHDL: Hardware Description and Design. Kluwer Academic Publishers, 1989.
D. E. Thomas and P. R. Moorby. The Verilog hardware description language. Kluwer Academic Publishers, 1991.
B. A. Davey and H. A. Priestley. Introduction to Lattices and Order Cambridge University 1994.
D. L. Dill, A. J. Drexler, A. J. Hu and C, H Yang. Protocol Verification as a Hardware Design Aid. ICCD,1992.
Fujita et al. Bug Identification of a Real Chip Design by Symbolic Model Checking. EDAC, 1994.
JR. Burch, E. M. Clarke, D. E. Long, K. L. McMillan and D. L. Dill. Symbolic Model Checking for Sequential Circuit wion, IEEE Transaction on Computer-Aided Design of Integrated Circuits and Systems, Vol. 13. No. 4, April 1994.
D. L. Beatty. A Methodology for Formal Mardware Verification with Application to Micropocessors. PhD thesis, Camegie-Mellon University, 1993.
D. A. Patterson and J. L. Hennessy. Computer Architecture: A Quantitative Approach. Morgan Kaufmann Publishers, Inc.,1996.
D. L. Beatty, K. Brace, R. E. Randal, Kycongsoon Cho, and Lawrence Huang. User's guide to COSMOS: a compiled simulator for MOS circuits. Computer Science Department, Carnegie-Mellon University, October, 1987.
V. R. Pratt, Pentium Report #bug!, Department of Computer Science, Stanford University, 1994.
Mine, G., Formal Specification and verification of digital systems, McGraw-Hill, 1994
A. Gupta, Formal Hardware Verification Methods: A Survey, Formal Methods in System Design, Vol 1., No 2/3, 1992, pp.151-238
G. J. Milne, Circal and the represemation of communication, concurrency and time. ACM Trans. on Programming Languages and Systems, 7(2), 1985.
C.A.R. Hoare, Communicating Sequential Processes, Prentice Hall International Series in Computer Science, 1985.
R. E. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, pages 293-318, September 1992.
R. Lipsett, C. Schaefer and C. Ussery. VHDL: Hardware Description and Design. Kluwer Academic Publishers, 1989.
D. E. Thomas and P. R. Moorby. The Verilog hardware description language. Kluwer Academic Publishers, 1991.
B. A. Davey and H. A. Priestley. Introduction to Lattices and Order Cambridge University 1994.
D. L. Dill, A. J. Drexler, A. J. Hu and C, H Yang. Protocol Verification as a Hardware Design Aid. ICCD,1992.
Fujita et al. Bug Identification of a Real Chip Design by Symbolic Model Checking. EDAC, 1994.
JR. Burch, E. M. Clarke, D. E. Long, K. L. McMillan and D. L. Dill. Symbolic Model Checking for Sequential Circuit wion, IEEE Transaction on Computer-Aided Design of Integrated Circuits and Systems, Vol. 13. No. 4, April 1994.
D. L. Beatty. A Methodology for Formal Mardware Verification with Application to Micropocessors. PhD thesis, Camegie-Mellon University, 1993.
D. A. Patterson and J. L. Hennessy. Computer Architecture: A Quantitative Approach. Morgan Kaufmann Publishers, Inc.,1996.
D. L. Beatty, K. Brace, R. E. Randal, Kycongsoon Cho, and Lawrence Huang. User's guide to COSMOS: a compiled simulator for MOS circuits. Computer Science Department, Carnegie-Mellon University, October, 1987.
V. R. Pratt, Pentium Report #bug!, Department of Computer Science, Stanford University, 1994.
Mine, G., Formal Specification and verification of digital systems, McGraw-Hill, 1994
A. Gupta, Formal Hardware Verification Methods: A Survey, Formal Methods in System Design, Vol 1., No 2/3, 1992, pp.151-238
G. J. Milne, Circal and the represemation of communication, concurrency and time. ACM Trans. on Programming Languages and Systems, 7(2), 1985.
C.A.R. Hoare, Communicating Sequential Processes, Prentice Hall International Series in Computer Science, 1985.
Publicado
07/10/1997
Como Citar
MIANA, Flávio; COELHO JR, Claudionor N.; NATTRODT, Patricia; FERNANDES, Antônio O.; MELO, Júlio Cezar de.
Mixing Symbolic and Ternary Simulation Techniques for the Verification of Processor-Based Systems. In: INTERNATIONAL SYMPOSIUM ON COMPUTER ARCHITECTURE AND HIGH PERFORMANCE COMPUTING (SBAC-PAD), 9. , 1997, Campos do Jordão/SP.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
1997
.
p. 241-252.
DOI: https://doi.org/10.5753/sbac-pad.1997.22628.
