Skip to main content
SpringerLink
Log in

Abstraction by Symbolic Indexing Transformations

  • Conference paper
  • First Online:
Book cover Formal Methods in Computer-Aided Design (FMCAD 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2517))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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

    Article  Google Scholar 

  2. Bryant, R.E.: A methodology for hardware verification based on logic simulation. Journal of the ACM 38 (1991) 299–328

    Article  MATH  MathSciNet  Google Scholar 

  3. 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

    Google Scholar 

  4. 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

    Google Scholar 

  5. Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers C-35 (1986) 677–691

    Article  Google Scholar 

  6. 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

    Chapter  Google Scholar 

  7. 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

    Article  Google Scholar 

  8. 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

    Google Scholar 

  9. Jones, R.B.: Applications of Symbolic Simulation to the Formal Verification of Microprocessors. PhD thesis, Department of Electrical Engineering, Stanford University (1999)

    Google Scholar 

  10. 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/.

  11. 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

    Chapter  Google Scholar 

  12. 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

    Google Scholar 

  13. 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

    Google Scholar 

  14. 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

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing Science, University of Glasgow, Glasgow, Scotland, G12 8QQ

    Thomas F. Melham

  2. Strategic CAD Labs, Intel Corporation, JF4-211, 2511 NE 25th Avenue, Hillsboro, OR, 97124, USA

    Robert B. Jones

Authors
  1. Thomas F. Melham
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Robert B. Jones
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Electrical and Computer Engineering, University of Waterloo, 200 University Avenue West, Waterloo, ON, N2L 3G1, Canada

    Mark D. Aagaard

  2. Strategic CAD Labs, Intel Corporation, 5200 NE ElamYoung Parkway, Hillsboro, OR, 97124-6497, USA

    John W. O’Leary

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation