Skip to main content
SpringerLink
Log in

Word level bitwidth reduction for unbounded hardware model checking

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

In this paper we present a word-level model checking method that attempts to speed up safety property checking of industrial netlists. Our aim is to construct an algorithm that allows us to check both bounded and unbounded properties using standard bit-level model checking methods as back-end decision procedures, while incurring minimum runtime penalties for designs that are unsuited to our analysis. We do this by combining modifications of several previously known techniques into a static abstraction algorithm which is guaranteed to produce bit-level netlists that are as small or smaller than the original bitblasted designs. We evaluate our algorithm on several challenging hardware components.

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

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Baumgartner J, Gloekler T, Shanmugam D, Seigler R, Huben GV, Mony H, Roessler P, Ramanandray B (2006) Enabling large-scale pervasive logic verification through multi-algorithmic formal reasoning. In: Proc of the formal methods in CAD conf, 2006

  2. Bjesse P (2008) A practical approach to word level model checking of industrial netlists. In: Proc of the computer aided verification conf, 2008

  3. Bryant R, German S, Velev M (1999) Exploiting positive equality in a logic of equality with uninterpreted functions. In: Proc of the computer aided verification conf, 1999

  4. Bryant R, Lahiri S, Seshia S (2002) Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Proc of the computer aided verification conf, 2002

  5. Galler B, Fischer M (1964) An improved equivalence algorithm. Commun ACM (May)

  6. Hojati R, Brayton R (1995) Automatic datapath abstraction in hardware systems. In: Proc of the computer aided verification conf, 1995

  7. Ip CN, Dill DL (1996) Better verification through symmetry. Form Methods Syst Des (August)

  8. Johannesen P (2002) Speeding up hardware verification by automated data path scaling. PhD thesis, Christian-Albrechts-Universität zu Kiel

  9. Manolios P, Srinivasan S, Vroon D (2007) BAT: The bit-level analysis tool. In: Proc of the computer aided verification conf, 2007

  10. Peh L-S, Dally W (2001) A delay model and speculative architecture for pipelined routers. In: Proc intl symposium on high-performance computer architecture, 2001

  11. Pnueli A, Rodeh Y, Strichmann O, Siegel M (2002) The small model property: how small can it be? Inf Comput 178:279–293

    MATH  Google Scholar 

  12. Pugh W (1999) Skip lists: a probabilistic alternative to balanced trees. Commun ACM (June)

  13. Ranise S, Tinelli C (2006) Satisfiability modulo theories. Trends and controversies. IEEE Intell Syst Mag (December)

Download references

Author information

Authors and Affiliations

  1. Synopsys Inc., 2025 NW Cornelius Pass Rd., Hillsboro, OR, 97124, USA

    Per Bjesse

Authors
  1. Per Bjesse
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Per Bjesse.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Bjesse, P. Word level bitwidth reduction for unbounded hardware model checking. Form Methods Syst Des 35, 56–72 (2009). https://doi.org/10.1007/s10703-009-0080-2

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-009-0080-2

Keywords

Search

Navigation