Form Of Authentication Methods For Sequential Logic Circuits Research

As the scale of digital circuits become very bigger and the function of circuit become very complicated recently, it is difficult to ensure the correctness of design in VLSI system. So the efficient verification of the design and implement of circuit must be introduced for building the higher responsible VLSI system. Simulative verification and formal verification are two main methods in VLSI design. Simulative verification is the leading method in industry, however, it cannot fully suit for the development of VLSI industry. People are paying more attention to formal verification.Model checking is a promising formal verification method for VLSI system. In this approach specification are expressed in a temporal logic and system are modeled as finite state transition systems. An efficient procedure is used to check if a given finite state transition system is a model for the specification. Model checking is completely automatic and fast. Above all, it can produce counterexamples to aid in debugging. Consequently, it is suitable for verifying VLSI system.Building the transition relation of sequential logic circuit is one of the key technologies for applying model checking method to verify the sequential logic circuit. We discuss elaborately the expression of the sequential logic circuits through BDD. With this understanding, we proposed and implemented an aglorithm for expressing the stable transistion relation of a kind of special fundamental-mode asynchronous circuit.Symbolic model checking method uses a more efficient "symbolic" representation for the system. Since the sizes of these representations is typically the limiting factor in applying model checking, an efficient representation can potentially allow much larger systems to be verified. We mended a typical symbolic model verifier and implemented basically a symbolic model checking system.