STE Verification Method For Concurrent Behaviors In Digital Circuit

Design verification plays an important part in the design process of digital circuits. Functional correctness verification is essential for design verification which is used to check on the conformance between specification and implementation. In the past twenty years, people have studied extensively and proposed several effective verification methods for sequential behaviors of digital circuits, such as simulation method and formal method. However, digital circuits are typical concurrent systems, due to the complexity researchers have not proposed any direct and effective methods for the verification of concurrent behaviors. How to perform the verification of concurrent behaviors is a critical factor to insure the functional correctness of digital circuits.This paper discusses some issues of verification for concurrent behaviors. First, introduce the basic theories and techniques of STE verification method and evaluate its advantages and weaknesses. Then extend STE verification specification using graphical theory, propose the concept of assertion graph and implement assertion based verification algorithm. Further, introduce process algebra language for describing the concurrent systems, build up associated concurrent model and give the transformation from language to model and verification process for concurrent systems behaviors. At last, discusses the important role of action refinement in specification language's hierarchical descriptions.