We Propose an integrated design and test assistance method for pipelined processors. Our approach generates behavioral-level test environments for pipeline control mechanisms from a machine-readable specification. It includes automatic generation of test programs and behavioral descriptions. Verification can be done by applying logic simulation to both the designers' descriptions and the behavioral descriptions, and then comparing the results. We have implemented an experimental system that enumerates all hazard patterns--instruction patterns that cause pipeline hazards--from the specifications, and generates the test programs and the behavioral descriptions for the pipeline controllers. The test programs cover all of the hazard patterns. The behavioral descriptions can manipulate any instruction stream. Experimental results for several RISC processors show that actual hazard patterns are too numerous to be easily enumerated by hand. Using workstations, our system can generate the test programs that cover all of the patterns, taking a few minutes. Results suggest that the system can be used to evaluate pipeline design.

Two schemes are described for digital fault simulation; one is on MOS circuit modeling for detecting transistor stuck faults in bidirectional transfer gates, and the other is on fault collapsing for reducing the number of faults in gate level circuits which include transformed logic gates. By using the proposed technique, all stuck-at faults on signal lines and all transistor faults in MOS transmission gates can be modeled by the conventional stuck-at faults. Several experimental results are also shown to reveal that the proposed schemes can be effectively applied to fault simulation of VLSI circuits including bidirectional MOS transmission gates.

For subgraph enumeration problems, very efficient algorithms have been proposed whose time complexities are far smaller than the number of subgraphs. Although the number of subgraphs can exponentially increase with the input graph size, these algorithms exploit compressed representations to output and maintain enumerated subgraphs compactly so as to reduce the time and space complexities. However, they are designed for enumerating only some specific types of subgraphs, e.g., paths or trees. In this paper, we propose an algorithm framework, called the frontier-based search, which generalizes these specific algorithms without losing their efficiency. Our frontier-based search will be used to resolve various practical problems that include constrained subgraph enumeration.

We present a symbolic language emptiness check algorithm based on forward state traversal. A verification property is given by a set of error traces written in ω-regular expression and is manipulated explicitly as a non-deterministic state transition graph. State space of the design model is implicitly traversed along the explicit graph. This method has a large amount of flexibility for controlling state traversal on the property space. It should become a good framework of incremental or approximate verification of ω-regular properties.