For system-level verification of a large-scale design, logic simulation is widely used. When a simulation trace exposes a design error a designer may rectify the design inadequately because the trace shows only one particular erroneous path. This is one of the essential problems of simulation based verification. On the other hand, model checkers are becoming widely used in industry but cannot verify large designs. We propose a new verification methodology based on a "navigated" model checking in order to overcome the above problems. We first generalize the trace and generate a property. We then verify the rectified design against the property by navigating state traversal in model checking. With navigation, we can verify designs without ad-hoc simplification and also can check various possible paths relating the error, instead of concentrating on a particular path of the trace. We have successfully verified bus transactions of a system-on-a-chip having two million transistors with our methodology. For one case, we found that the rectification was inadequate, and we fixed it successfully.

This paper presents a new approach of data pipelining for mincut partitioning acceleration using a parallel computer. We choose the hardware CAD accelerator TP5000 to implement our approach. We obtain a speed improvement of 20 to 25 times as fast as a SPARCStation-10 by using 10 processors in the TP5000.

We present a CTL model checking algorithm based mainly on forward state traversal, which can check many realistic CTL properties without doing backward state traversal. This algorithm is effective in many situations where backward state traversal is more expensive than forward state traversal. We combine it with BDD-based state traversal techniques using partitioned transition relations. Experimental results show that our method can verify actual CTL properties of large industrial models which cannot be handled by conventional model checkers.

Logic synthesis for look-up tables (LUTs) has received much attention in the past few years, since Xilinx introduced its LUT-based field-programmable gate array (FPGA) architectures. An m-input LUT can implement any Boolean function of up to m inputs. So the goal of synthesis for such architectures has been to synthesize a circuit in which each function can be implemented by one m-LUT such that either the total number of functions or the number of levels of the circuit is minimized. In this work, we focus on a different though related problem: synthesize the given circuit on a single memory or LUT L, which has a capacity of M bits. In addition to satisfying the memory constraint M, we also wish to minimize the total number of functions to be implemented. The main motivation for the problem comes from the problem of minimizing the simulation time on a hardware accelerator for logic simulation. This accelerator uses memory as a logic primitive. In fact, the problem is also relevant in the context of compile-code or software simulation. Another situation where the problem arises is in synthesis for the FPGA architectures being proposed that have on-chip memory for storing programs and data. The unused memory locations can be used to store logic functions. We show that the existing LUT synthesis methods are inadequate to solve this problem. We propose techniques to solve the problem and present experimental evidence to demonstrate their effectiveness.

The degree of needs for high quality test pattern sets for delay faults becomes more serious as VLSI chips have more complex structures and higher performance. In spite of its importance, it is more difficult to find complete test pattern sets for delay faults than for stuck-at faults. It thus takes much time to generate high quality test pattern sets. To acquire high quality test pattern sets for delay faults as fast as possible, the authors take an approach that executes a test pattern generation process for delay faults on the very high speed logic simulation processor 'SP'. As a result, to apply ISCAS'89 benchmark circuits, the authors achieved a fault coverage rate of 85% in two minutes testing for a circuit which has about 1000 gates. They confirmed that this system is effective as a pre-processing method to exclude many faults at very highspeed.>

A method is presented to accelerate test generation, which synthesizes a test-generation circuit S(C, F) that combines the original combinational circuit C (modified by programmable faults F) and peripheral circuits that automatically generate a test of C. The test patterns are generated by searching the inputs to expose faults to the outputs using an ultrahigh-speed simulator (SP).>

This paper deals with placement and routing techniques for master slice LSIs. The basic idea of both techniques is to make wiring density on the chip more uniform. Algorithms and some experimental results are described.