Researchers and designers working on software tools for automatic generation of functional vectors for sequential circuits are this paper’s main audience. Unlike similar research for combinational circuits, which has traditionally been aimed at the testing of fabricated circuits for stuck-at faults, this work is more general. Its target is functional testing, which borders on hardware design validation and on the testing of programs by path traversal (“white box” testing). The results are applicable for automatic design verification, manufacturing testing, and power estimation of sequential circuits. Regarding the production testing, the authors are not too ambitious; they claim that the stuck-at fault coverage of their functional vectors is only 70 percent. However, the method’s main advantage is the speed of the testing procedure.
The process of deriving functional vectors described in the paper is based on a new formal model, the Extended Finite State Machine (EFSM). This model brings into the classical FSM an additional element, representing the data path in the modeled system. In order to avoid explosion in the size of the model, the EFSM allows the designer to define conditions on the data path in the form of predicates. The combination of the finite set of ranges of data values and of the EFSM states gives rise to the notions of a block, which is analogous to a state but has a data path component, and of a block transition. The paper defines the concept of a stable block transition, which is similar to the idea of a deterministic transition in classical FSMs. An algorithm for the stabilization of an EFSM is a crucial part of generating the set of functional vectors that traverse the EFSM arcs. The initial description of the system is done in a high-level language, such as C or VHDL. This description is transformed into an intermediate form (borrowed from AT&T’s Behavior Synthesis System). Next, an EFSM model is extracted from the intermediate form. Then, the initial EFSM model is stabilized and orthogonalized. Finally, functional vectors are generated from the stabilized and orthogonalized EFSM.
The paper presents experimental results on the application of the tools, executing the above procedure, to a set of benchmarks. The paper appears to be technically sound and useful. Using a single example throughout the paper is a good idea, reducing the chance of losing the reader.
I found the presentation style and the quality of proofreading a bit disappointing. There is no unified style for algorithms and procedures: some appear in the text and some in figures. In the main example, the figures appear significantly after the text explaining them. The proofreading of the formal notation is very poor. There are missing or incorrect subscripts on pages 60 and 68. In the notation for intervals of integers on page 67, some of the bounds should be denoted with parentheses, not square brackets. There is no explanation of symbols on page 68--what are these C’s and P’s? On page 72, in the structure <(s0, count=)>, a zero is missing, and it should apparently read <(s0, count=0)>. With all of these missing bits and pieces, it is difficult to check the proof in the appendix.
It would be helpful if the editors of this fairly new journal would take a firmer line on the quality of presentation of its papers.
