Automatic simulation vectors generation is an efficient method to accelerate digital system’s design verification process. An algorithm that generates coverage metrics and simulation vectors for state-pair of interacting FSM is presented in this paper. Compared with FSM (finite state machines) product method and the method which treats the interacting FSM as a single FSM, this algorithm can generate accurate coverage metrics and the shortest simulation vectors. Experimental results show that this algorithm is efficient in memory usage and perfectly solves the states space exploration problem.
[1]Ho R, Yang C, Horowitz M, Dill D. Architecture validation for processors. In: Patterson DA, ed. Proceedings of the International Symposium on Computer Architecture. Santa Margerita Ligure: ACM Press, 1995. 404~413.
[2]Shen J, Abraham JA. An RTL abstraction technique for processor microarchitecture validation and test generation. Journal of Electronic Testing: Theory and Application, 1999,16(1,2):67~81.
[3]Moundanos D, Abraham JA, Hoskote YV. Abstraction techniques for validation coverage analysis and test generation. IEEE Transactions on Computers, 1998,47(1):2~13.
[4]Geist D, Farkas M, Landver A, Lichtenstein Y, Ur S, Wolfsthal Y. Coverage-Directed test generation using symbolic techniques. In: Srivas MK, Camilleri AJ, eds. Proceedings of the Conference on Formal Methods in Computer-Aided Design. Palo Alto, CA: Springer-Verlag, 1996. 143~158.
[5]Aziz A, Kukula J, Shiple T. Hybrid verification using saturated simulation. In: Irwin MJ, ed. Proceedings of the 35th Design Automation Conference. San Francisco, CA: ACM Press, 1998. 615~618.
[6]Ho P-H, Shiple T, Harer K, Kukula JH, Damiano R, Bertacco VM, Taylor J, Long J. Smart simulation using collaborative formal and simulation engines. In: Proceedings of the International Conference on Computer Aided Design. San Jose, CA: IEEE Press, 2000. 120~126.
[7]Biere A, Cimatti A, Clarke E, Fujita M, Zhu Y. Symbolic model checking using SAT procedures instead of BDDs. In: Irwin MJ, ed. Proceedings of the 36th Design Automation Conference. New Orleans, LA: ACM Press, 1999. 317~320.
[8]Bryant RE. Graph-Based algorithms for Boolean function manipulation. IEEE Transactions on Computers, 1986,35(8):677~691.
[9]Liu CNJ, Yen C-C, Jou J-Y. Automatic functional vector generation using the interacting FSM model. In: Proceedings of the International Symposium on Quality Electronic Design. San Jose, CA: ACM Press, 2001. 372~377.
[10]Narayan A, Jain J, Fujita M, Sangiovanni-Vincentelli AL. Partitioned-ROBDDs--a compact, canonical and efficiently manipulable representation for Boolean functions. In: Rutenbar RA, Otten RHJM, eds. Proceedings of the International Conference on Computer Aided Design. San Jose, CA: ACM and IEEE Computer Society, 1996. 547~554.
[11]McMillan KL. Symbolic Model Checking. Boston: Kluwer Academic Publishers, 1994.
[12]Narayan A, Isles AJ, Jain J, Brayton RK. Reachability analysis using partitioned-ROBDDs. In: Rutenbar RA, ed. Proceedings of the International Conference on Computer Aided Design. San Jose, CA: ACM and IEEE Computer Society, 1997. 388~393.
[13]Somenzi F. CUDD: CU Decision Diagram Package. 2001. ftp://vlsi.colorado.edu/.