ESTONIAN ACADEMY
PUBLISHERS
eesti teaduste
akadeemia kirjastus
cover
Estonian Journal of Engineering

Application of high-level decision diagrams for simulation-based verification tasks; pp. 56–77

Full article in PDF format | doi: 10.3176/eng.2010.1.07

Authors
Maksim Jenihhin, Jaan Raik, Anton Chepurov, Raimund Ubar

Abstract
This paper describes the advantages of the application of a system representation model, called High-Level Decision Diagrams (HLDDs), for hardware functional verification. Two tasks of simulation-based verification, considered in this paper, are assertion checking and code coverage analysis. Assertion checking employs temporal extension of an existing HLDD model aimed at supporting temporal properties, expressed in Property Specification Language (PSL). The described approach to code coverage analysis provides for more accurate results than traditional VHDL code coverage methods. Experimental results show the feasibility and efficiency of the HLDDs-based approaches.
References

  1. Ubar, R., Raik, J. and Morawiec, A. Back-tracing and event-driven techniques in high-level simulation with decision diagrams. In Proc. IEEE International Symposium on Circuits and Systems. Geneva, 2000, 208–211.

  2. Bryant, R. E. Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers, 1986, C-35, 677–691.
doi:10.1109/TC.1986.1676819

  3. Clarke, E., Fujita, M., McGeer, P., McMillan, K. L., Yang, J. and Zhao, X. Multi terminal BDDs: an efficient data structure for matrix representation. In Proc. International Work­shop on Logic Synthesis, Louvain, Belgium, 1993, 1–15.

  4. Drechsler, R., Becker, B. and Ruppertz, S.  K *BMDs: a new data structure for verification. In Proc. European Design & Test Conference, Paris, 1996, 2–8.

  5. Chayakul, V., Gajski, D. D. and Ramachandran, L. High-level transformations for minimizing syntactic variances. In Proc. ACM IEEE Design Automation Conference. Texas, TX, 1993, 413–441.

  6. Piziali, A. Functional Verification Coverage Measurement and Analysis. Springer Science, New York, 2008.

  7. Bullseye testing technology. Code coverage analysis. Minimum acceptable code coverage. URL: http://www.bullseye.com (September 28, 2009).

  8. Raik, J., Reinsalu, U., Ubar, R., Jenihhin, M. and Ellervee, P. Code coverage analysis using high-level decision diagrams. In Proc. IEEE International Symposium on Design and Diagnostics of Electronic Circuits and Systems. Bratislava, Slovakia, 2008, 201–206.

  9. Jenihhin, M., Raik, J., Chepurov, A. and Ubar, R. PSL assertion checking with temporally extended high-level decision diagrams. In Proc. IEEE Latin-American Test Workshop. Puebla, Mexico, 2008, 49–54.

10. Minakova, K., Reinsalu, U., Chepurov, A., Raik, J., Jenihhin, M., Ubar, R. and Ellervee, P. High-level decision diagram manipulations for code coverage analysis. In Proc. IEEE International Biennal Baltic Electronics Conference. Tallinn, Estonia, 2008, 207–210.

11. International technology roadmap for semiconductors. URL: http://www.itrs.net (September 28, 2009).

12. Yuan, J., Pixley, C. and Aziz, A. Constraint-Based Verification. Springer Science, New York, 2006.

13. Accellera. Property Specification Language Reference Manual, v1.1. Accellera Organization, Napa, USA, 2004.

14. IEEE-Commission. IEEE standard for Property Specification Language (PSL). IEEE Std 1850-2005, 2005.

15. Gheorghita, S. and Grigore, R. Constructing checkers from PSL properties. In Proc. 15th Inter­national Conference on Control Systems and Computer Science (CSCS). Bucharest, Roumania, 2005, 757–762.

16. Bustan, D., Fisman, D. and Havlicek, J. Automata construction for PSL. Technical Report MCS05-04, The Weizmann Institute of Science, 2005.

17. Boulé, M. and Zilic, Z. Efficient automata-based assertion-checker synthesis of PSL properties. In Proc. IEEE International High Level Design Validation and Test Workshop. Monterey, CA, 2006, 1–6.

18. Morin-Allory, K. and Borrione, D. Proven correct monitors from PSL specifications. In Proc. Design, Automation and Test in Europe Conference. Munich, Germany, 2006, 1–6.

19. IBM AlphaWorks. FoCs property checkers generator ver. 2.04. URL: http://www.alphaworks.
ibm.com/tech/FoCs
, (September 28, 2009).

20. Jenihhin, M., Raik, J., Chepurov, A. and Ubar, R. Assertion checking with PSL and high-level decision diagrams. In Proc. IEEE Workshop on RTL and High Level Testing. Beijing, China, 2007, 1–6.

21. Eisner, C. and Fisman, D. A Practical Introduction to PSL. Springer Science, New York, 2006.

22. Jenihhin, M., Raik, J., Chepurov, A. and Ubar, R. Temporally extended high-level decision diagrams for PSL assertions simulation. In Proc. IEEE European Test Symposium. Verbania, Italy, 2008, 61–68.

23. Corno, F., Reorda, M. S. and Squillero, G. RT-level ITC’99 benchmarks and first ATPG results. IEEE Journal Design & Test of Computers, 2000, 17, 44–53.
doi:10.1109/54.867894

Back to Issue