Abstract
Symbolic indexing is a data abstraction technique that exploits the partially-ordered state space of symbolic trajectory evaluation (STE). Use of this technique has been somewhat limited in practice because of its complexity. We present logical machinery and efficient algorithms that provide a much simpler interface to symbolic indexing for the STE user. Our logical machinery also allows correctness assertions proved by symbolic indexing to be composed into larger properties, something previously not possible.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Seger, C.J.H., Bryant, R.E.: Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design 6 (1995) 147–189
Bryant, R.E.: A methodology for hardware verification based on logic simulation. Journal of the ACM 38 (1991) 299–328
Pandey, M., Raimi, R., Bryant, R.E., Abadir, M.S.: Formal verification of content addressable memories using symbolic trajectory evaluation. In: ACM/IEEE Design Automation Conference, ACM Press (1997) 167–172
Bryant, R.E., Beatty, D.L., Seger, C.J.H.: Formal hardware verification by symbolic ternary trajectory evaluation. In: ACM/IEEE Design Automation Conference, ACM Press (1991) 397–402
Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers C-35 (1986) 677–691
Chou, C.T.: The mathematical foundation of symbolic trajectory evaluation. In Halbwachs, N., Peled, D., eds.: Computer Aided Verification (CAV). Volume 1633 of Lecture Notes in Computer Science., Springer-Verlag (1999) 196–207
Jain, P., Gopalakrishnan, G.: Efficient symbolic simulation-based verification using the parametric form of Boolean expressions. IEEE Transactions on Computer-Aided Design of Integrated Circuits 13 (1994) 1005–1015
Aagaard, M.D., Jones, R.B., Seger, C.J.H.: Formal verification using parametric representations of Boolean constraints. In: ACM/IEEE Design Automation Conference, ACM Press (1999) 402–407
Jones, R.B.: Applications of Symbolic Simulation to the Formal Verification of Microprocessors. PhD thesis, Department of Electrical Engineering, Stanford University (1999)
O’Leary, J.W., Zhao, X., Gerth, R., Seger, C.J.H.: Formally verifying IEEE compliance of floating-point hardware. Intel Technical Journal (First quarter, 1999) Available at http://www.developer.intel.com/technology/itj/.
Kaivola, R., Aagaard, M.D.: Divider circuit verification with model checking and theorem proving. In Aagaard, M., Harrison, J., eds.: Theorem Proving in Higher Order Logics. Volume 1869 of Lecture Notes in Computer Science., Springer-Verlag (2000) 338–355
Aagaard, M.D., Jones, R.B., Seger, C.J.H.: Combining theorem proving and trajectory evaluation in an industrial environment. In: ACM/IEEE Design Automation Conference, ACM Press (1998) 538–541
Bjesse, P., Leonard, T., Mokkedem, A.: Finding bugs in an Alpha microprocessor using satisfiability solvers. In Berry, G., Comon, H., Finkel, A., eds.: Computer Aided Verification (CAV). Volume 2102 of Lecture Notes in Computer Science., Springer-Verlag (2001) 454–464
Yang, J., Seger, C.J.H.: Introduction to generalized symbolic trajectory evaluation. In: Proceedings of 2001 IEEE International Conference on Computer Design. (2001) 360–365
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Melham, T.F., Jones, R.B. (2002). Abstraction by Symbolic Indexing Transformations. In: Aagaard, M.D., O’Leary, J.W. (eds) Formal Methods in Computer-Aided Design. FMCAD 2002. Lecture Notes in Computer Science, vol 2517. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36126-X_1
Download citation
DOI: https://doi.org/10.1007/3-540-36126-X_1
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00116-4
Online ISBN: 978-3-540-36126-8
eBook Packages: Springer Book Archive