Automatic generation of functional vectors using the extended finite state machine model

ABSTRACT

We present a method of automatic generation of functional vectors for sequential circuits. These vectors can be used for design verification, manufacturing testing, or power estimation. A high-level description of the circuit in VHDL or C is assumed available. Our method automatically transforms the high-level description of a circuit in VHDL or C into an extended finite state machine (EFSM) model that is used to generate functional vectors. The EFSM model is a generalization of the traditional state machine model. It is a compact representation of models with local data variables and preserves many nice properties of a traditional state machine model. The theoretical background of the EFSM model is addressed in this article. Our method guarantees that the generated vectors cover every statement in the high-level description at least once. Experimental results show that a set of comprehensive functional vectors for sequential circuits with more than a hundred flip-flops can be generated automatically in a few minutes of CPU time using our prototype system.

REFERENCES

• 1: Karl S. Brace , Richard L. Rudell , Randal E. Bryant, Efficient implementation of a BDD package, Proceedings of the 27th ACM/IEEE conference on Design automation, p.40-45, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.123222]
• 2: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 3: J. R. Burch , E. M. Clarke , K. L. McMillan , David L. Dill, Sequential circuit verification using symbolic model checking, Proceedings of the 27th ACM/IEEE conference on Design automation, p.46-51, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.123223]
• 4: Kwang-Ting Cheng , Vishwani D. Agrawal, Unified Methods for VLSI Simulation and Test Generation, Kluwer Academic Publishers, Norwell, MA, 1989
• 5: CHENG, W.T. 1988. The BACK algorithm for sequential test generation. In Proceedings of the International Conference on Computer Design (ICCD-88) (Rye Brook, NY, Oct.), 66-69.
• 6: Hyunwoo Cho , Gary D. Hachtel , Fabio Somenzi, Fast Sequential ATPG Based on Implicit State Enumeration, Proceedings of the IEEE International Test Conference on Test: Faster, Better, Sooner, p.67-74, October 26-30, 1991
• 7: CHO, H., et al. 1990. ATPG aspects of FSM verification. In Proceedings of the International Conference on CAD (Santa Clara, CA, Nov.), 134-137.
• 8: COUDERT, O., AND MADRE, J.-C. 1990. A unified framework for the formal verification of sequential circuits. In Proceedings of the International Conference on CAD (Nov.), 126-129.
• 9: COUDERT, O., BERTHET, C., AND MADRE, J.C. 1989. Verification of sequential machines using boolean functional vectors. In Proceedings of the IFIP International Workshop on Applied Formal Methods for Current VLSI Design (Leuven, Belgium, Nov.), 111-128.
• 10: Srinivas Devadas , Kurt Keutzer , A. S. Krishnakumar, Design Verfication and Reachability Analysis Using Algebraic Manipulation, Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, p.250-258, October 14-16, 1991
• 11: GHOSH, A., DEVADAS, S., AND NEWTON, A. R. 1991. Test generation and verification for highly sequential circuits. IEEE Trans. Comput. Aided Des. 10, 5 (May), 652-667.
• 12: IEEE. 1987. IEEE Standard VHDL Language Reference Manual, IEEE Standard, 1076- 1987.
• 13: Jov, J-Y., ROTHWEILER, S., ERNST, R., SUTARWALA, S., AND PRABHU, A. 1989. BESTMAP: Behavioral Synthesis from C. In International Workshop on Logic Synthesis (Research Triangle Park, NC, May).
• 14: KELSEY, T. P. AND SALUJA, K. K. 1989. Fast test generation for sequential circuits. In Proceedings of the International Conference on Computer-Aided Design (Santa Clara, CA, Nov.), 354-357.
• 15: David Lee , Mihalis Yannakakis, Online minimization of transition systems (extended abstract), Proceedings of the twenty-fourth annual ACM symposium on Theory of computing, p.264-274, May 04-06, 1992, Victoria, British Columbia, Canada [doi>10.1145/129712.129738]
• 16: MA, H-K. T., DEVADAS, S., NEWTON, A. R., AND SANGIOVANNI-VINCENTELLI, A. 1988. Test generation for sequential circuits. IEEE Trans. Comput. Aided Des. (Oct.), 1081-1093.
• 17: Edward F. Moore, Sequential Machines: Selected Papers, Addison-Wesley Longman Ltd., Essex, UK, 1964
• 18: Thomas Niermann , Janak H. Patel, HITEC: a test generation package for sequential circuits, Proceedings of the conference on European design automation, February 25-28, 1991, Amsterdam, The Netherlands
• 19: POMERANZ, I. AND REDDY, S.M. 1991. Test generation for synchronous sequential circuits using multiple observation times. In Fault-Tolerant Computing Symposium (Montreal, June).
• 20: TOUATI, H. J., SARVOJ, H., LIN, B., BRAYTON, R. K., AND SANGIOVANNI-VINCENTILLI, A. 1990. Implicit state enumeration of finite state machines using BDDs. In Proceedings of the International Conference on CAD (Nov.), 130-133.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS
      B.7.2 Design Aids
          Subjects: Verification

Additional Classification:
  B. Hardware
  B.5 REGISTER-TRANSFER-LEVEL IMPLEMENTATION
  B.6 LOGIC DESIGN
      B.6.1 Design Styles
          Subjects: Sequential circuits
      B.6.3 Design Aids
          Subjects: Hardware description languages
  B.7 INTEGRATED CIRCUITS
      B.7.3 Reliability and Testing**
          Subjects: Testability**

  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Automata (e.g., finite, push-down, resource-bounded)

  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS
      G.2.2 Graph Theory
          Subjects: Graph algorithms

General Terms:
Algorithms, Experimentation, Languages, Theory, Verification

Keywords:
automatic test generation, design verification, extended finite state machines, functional testing