Skip to main content
SpringerLink
Log in

Verification of Large Scale Nano Systems with Unreliable Nano Devices

  • Chapter
Nano, Quantum and Molecular Computing

  • 483 Accesses

Abstract

Any nano-system that designers build must guarantee functional correctness. The sheer scale factor and the added layers of uncertainty in nano-systems demand revolutionary breakthroughs in system design tools and algorithms. Formal verification of nano systems, then, must be able to deal with large state spaces, together with the presence of unknowns and uncertainties. The methods described in this chapter present a suite of algorithms that can offer potential in reducing the problem complexity in verification of nano-systems.

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 129.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 169.99
Price excludes VAT (USA)
  • Durable hardcover 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. J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. In Proc. Logic in Computer Science, pages 428–439, 1990.

    Google Scholar 

  2. K. L. McMillan. Symbolic Model Checking: An Approach to State Explosion Problem. Kluwer Academic publishers, 1993.

    Google Scholar 

  3. G. Cabodi, S. Nocco, and S. Quer. Improving sat-based bounded model checking by means of BDD-based approximated traversals. In Proc. Design Automation and Test in Europe Conf., pages 898–903. IEEE/ACM, 2003.

    Google Scholar 

  4. A. Gupta, M. Ganai, C. Wang, Z. Yang, and P. Ashar. Learning from 03 in sat-based bounded model checking. In Proc. Design Automation Conf., pages 824–829. IEEE/ACM, 2003.

    Google Scholar 

  5. Y. Novikov. Local search for boolean relations on the basis of unit propagation. In Proc. Design Automation and Test in Europe Conf., pages 810–815. IEEE/ACM, 2003.

    Google Scholar 

  6. F. Lu, L.-C. Wang, K. Cheng, and R. C.-Y Huang. A circuit sat solver with signal correlation guided learning. In Proc. Design Automation and Test in Europe Conf., pages 892–897. IEEE/ACM, 2003.

    Google Scholar 

  7. F. Bacchus and J. Winter. Effective preprocessing with hyper-resolution and equality reduction. In Proc. International Conf. Theory and App. Satisfiability Testing. IEEE, 2003.

    Google Scholar 

  8. R. Arora and M. S. Hsiao. Enhancing sat-based bounded model checking using sequential logic implications. In Proc. VLSI Design Conf., pages 784–787. IEEE, 2004.

    Google Scholar 

  9. J. Zhao, J. A. Newquist, and J. Patel. A graph traversal based framework for sequential logic implication with an application to c-cycle redundancy identification. In Proc. VLSI Design Conf., pages 163–169. IEEE, 2001.

    Google Scholar 

  10. M. S. Hsiao. Maximizing impossibilities for untestable fault identification. In Proc. Design Automation and Test in Europe Conf., pages 949–953. IEEE, 2002.

    Google Scholar 

  11. M. Syal and M. S. Hsiao. A novel, low-cost algorithm for sequentially untestable fault identification. In Proc. Design Automation and Test in Europe Conf., pages 316–321. IEEE, 2003.

    Google Scholar 

  12. E. Goldberg and Y. Novikov. Berkmin: a fast and robust sat-solver. In Proc. Design Aut. and Test in Europe Conference, pages 142–149. IEEE, 2002.

    Google Scholar 

  13. S. Sheng and M. S. Hsiao. Efficient preimage computation using a novel success-driven ATPG. In Proc. Design Automation and Test in Europe Conf., pages 822–827. IEEE, 2003.

    Google Scholar 

  14. S. Sheng, K. Takayama, and M. S. Hsiao. Effective safety property checking based on simulation-based ATPG. In Proc. Design Automation Conf., pages 813–818. IEEE, 2002.

    Google Scholar 

  15. M. S. Hsiao and J. Jain. Practical use of sequential ATPG for model checking: going the extra mile does pay off. In Proc. Int’l Workshop High Level Design Validation and Test., pages 39–44. IEEE, 2001.

    Google Scholar 

  16. A. Jain. On arbitrary defects: modeling and applications. In M.S. Thesis, Department of Electrical and Computer Engineering, Rutgers University, June 1999.

    Google Scholar 

  17. A. Jain, V. Boppana, R. Mukherjee, J. Jain, M. S. Hsiao, and M. Fujita. Testing, verification, and diagnosis in the presence of unknowns. In Proc. VLSI Test Symp., pages 263–269. IEEE, 2000.

    Google Scholar 

  18. C. Scholl and B. Becker. Checking equivalence for partial implementations. In Proc. Design Automation Conf., pages 238–243, 2001.

    Google Scholar 

  19. R. Arora and M. S. Hsiao. Enhancing sat-based equivalence checking with static logic implications. In Proc. IEEE High-Level Design Validation and Test Workshop, pages 63–68. IEEE, 2003.

    Google Scholar 

  20. Q. Wu and M. S. Hsiao. Efficient ATPG for design validation based on partitioned state exploration histories. In to appear Proc. IEEE VLSI Test Symp.. IEEE, 2004.

    Google Scholar 

  21. B. Li, M. S. Hsiao, and S. Sheng, A novel SAT all-solutions solver for efficient preimage computation In Proceedings of the IEEE/ACM Design Automation and Test in Europe (DATE) Conference, pages 272–277. February, 2004.

    Google Scholar 

  22. K. Chandrasekar and M. S. Hsiao, ATPG-based preImage computation: efficient search space pruning With ZBDD In Proceedings of the IEEE High-Level Design Validation and Test Workshop, November 2003, pp. 117–122.

    Google Scholar 

  23. V. Boppana, S. P. Rajan, K. Takayama, and M. Fujita, Model checking based on sequential ATPG In Proc. Computer Aided Verification, 1999, pp. 418–429.

    Google Scholar 

  24. A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu, Symbolic model checking without BDDs In Tools and Algorithms for Analysis and Construction of Systems, 1999, pp. 193–207.

    Google Scholar 

  25. N. Narayan, J. Jain, M. Fujita, A. Sangiovanni-Vincentelli, Partitioned ROBDDs: A compact, canonical and efficiently manipulable representation for Boolean functions In Proc. Intl Conf. Computer Aided Design, 1996, pp. 547–554.

    Google Scholar 

  26. D. Wang, P.-H. Ho, J. Long, J. Kukula, Y. Zhu, T. Ma, and R. Damiano, Formal Property Verification by Abstraction Refinement with Formal, Simulation and Hybrid Engines In Proc. of Design Automation Conference, 2001.

    Google Scholar 

  27. A. Biere, A. Cimatti, E.M. Clarke, M. Fujita, and Y. Zhu, “Symbolic Model Checking Using SAT Procedures Instead of BDDs,” Proc. DAC, 1999, pp.317–20.

    Google Scholar 

  28. P. A. Abdulla, P. Bjesse, and N. Een., Symbolic Reachability Analysis Based on SAT-solvers In Proc. of TACAS, 2000.

    Google Scholar 

  29. A. Gupta, Z. Yang, P. Ashar and A. Gupta, SAT-based Image Computation with Application in Reachability Analysis In Proc. FMCAD, 2000.

    Google Scholar 

  30. A. Gupta, Z. Yang, P. Ashar, L. Zhang, and S. Malik, Partition-Based Decision Heuristics for Image Computation using SAT and BDDs In Proc. ICCAD, 2001, pp. 286–292.

    Google Scholar 

  31. K. L. McMillan, Applying SAT methods in Unbounded Symbolic Model Checking In Proc. of CAV, 2002.

    Google Scholar 

  32. H. Kang and I. Park, SAT-based Unbounded Symbolic Model Checking In Proc. of DAC, 2003.

    Google Scholar 

  33. D. Roth, On the Hardness of Approximate Reasoning In Journal of Artificial Intelligence, 1996.

    Google Scholar 

  34. J. P. Marques and K. A. Sakallah, Dynamic Search-Space Pruning Techniques in Path Sensitization Proc. DAC, 1994.

    Google Scholar 

  35. J. P. Marques-Silva and K. A. Sakallah, GRASP: A Search Algorithm for Propositional Satisfiability In IEEE Trans. Computers, vol. 48, no. 5, pp. 506–521, May, 1999.

    Article  MathSciNet  Google Scholar 

  36. L. Zhang, C. F. Madigan, M. H. Moskewicz and S. Malik, Efficient Conflict Driven Learning in a Boolean Satisfiability Solver Proc. ICCAD, 2001, pp. 279–285.

    Google Scholar 

  37. L. Zhang and S. Malik, Towards Symmetric Treatment of Conflicts And Satisfaction in Quantified Boolean Satisfiability Solver In Proc. 8th Intl. Conf. on Principles and Practice of Constraint Programming(CP2002), 2002.

    Google Scholar 

  38. M. H. Schulz, E. Trischler and T. M. Sarfert, SOCRATES: A Highly Efficient Automatic Test Pattern Generation System In IEEE Trans. CAD, vol.7, no. 1, pp. 126–137, 1988.

    Google Scholar 

  39. M. Abramovici, M. A. Breuer and A. D. Friedman, Digital Systems Testing and Testable Design, IEEE Press, 1990.

    Google Scholar 

  40. P. Chung, I. N. Hajj and J. H. Patel, Efficient Variable Ordering Heuristics for Shared ROBDD Proc. ISCAS, 1993, pp. 1690–1693.

    Google Scholar 

  41. H. Iwashita and T. Nakata, Forward Model Checking Techniques Oriented to Buggy Designs In Proc. ICCAD, pp.400–404, Nov. 1997.

    Google Scholar 

  42. J. P. M. Silva, “On Computing Minimum Size Prime Implicants,” Proc. International Workshop on Logic Synthesis, 1997.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Electrical and Computer Engineering Virginia Tech, USA

    Michael S. Hsiao & Rajat Arora

  2. Mentor Graphics Corporation, Wilsonville, OR

    Shuo Sheng

  3. Haas School of Business, University of California at Berkeley, USA

    Ankur Jain

  4. Zenasis Technologies, USA

    Vamsi Boppana

Authors
  1. Michael S. Hsiao
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Shuo Sheng
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Rajat Arora
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Ankur Jain
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Vamsi Boppana
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Virginia Polytechnic and State University, Blacksburg, USA

    Sandeep K. Shukla

  2. Brown University, Providence, USA

    R. Iris Bahar

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Kluwer Academic Publishers

About this chapter

Cite this chapter

Hsiao, M.S., Sheng, S., Arora, R., Jain, A., Boppana, V. (2004). Verification of Large Scale Nano Systems with Unreliable Nano Devices. In: Shukla, S.K., Bahar, R.I. (eds) Nano, Quantum and Molecular Computing. Springer, Boston, MA. https://doi.org/10.1007/1-4020-8068-9_11

Download citation

  • DOI: https://doi.org/10.1007/1-4020-8068-9_11

  • Publisher Name: Springer, Boston, MA

  • Print ISBN: 978-1-4020-8067-8

  • Online ISBN: 978-1-4020-8068-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation