资 源 简 介
What is formal property verificaTIon? A natural language such as English allowsus to interpret the term formal property verificaTIon in two ways, namely:• VerificaTIon of formal properTIes, or• Formal methods for property verificationThis inherent ambiguity in natural languages has been the source of manylogical bugs in chip designs. Design specifications are sometimes interpretedin different ways by different designers with the result that the design’s architecturalintent is not implemented correctly. In an era where bugs are morecostly than transistors, the industry is beginning to realize the value of usingformal specifications.In practice there are indeed two ways in which property verification isdone today. These are static Assertion-based Verification (ABV) and dynamicAssertion-based Verification (ABV). In both forms, formal properties specifythe correctness requirements of the design, and the goal is to check whether agiven implementation satisfies the properties. Static ABV techniques formallyverify whether all possible behaviors of the design satisfy the given properties.Dynamic ABV is a simulation-based approach, where the properties arechecked over a simulation run – the verification is thereby confined to onlythose behaviors that are encountered during the simulation. In this book, weshall refer to static ABV as formal property verification (FPV), and continueto use dynamic ABV to refer to the simulation based property verificationapproach.The main tasks for a practitioner of property verification are as follows:1. Development of the formal property specification. The main challenge hereis to express key features of the design intent in terms of formal properties.2. Verifying the consistency and completeness of the specification. This is anecessary step, because the first task is a non-trivial one and subject toerrors and oversights.3. Verifying the implementation against the formal property specification. Inorder to perform this task effectively, a verification engineer must be awareof the limitations of the verification tool and must know the best way touse the tool under various types of constraints.All the above tasks are replete with open issues – the focus of this book is toconsider some of these issues and attempt to forecast the roadmap for FPVand dynamic ABV within the existing design verification flows of chip designcompanies. This chapter will summarize some of the major challenges. Let ususe the following case as a running example for our discussion.Example 1.1. Let us consider the specification of a 2-way priority arbiter havingthe following interface:mem-arbiter( input r1, r2, clk, output g1, g2 )r1 and r2 are the request lines, g1 and g2 are the corresponding grant lines,and clk is the clock on which the arbiter samples its inputs and performs thearbitration.We assume that the arbitration decision for the inputs at one cycleis reflected by the status of the grant lines in the next cycle. Let us supposethat the specification of the arbiter contains the following requirements:1. Request line r1 has higher priority than request line r2. Whenever r1 goeshigh, the grant line g1 must be asserted for the next two cycles.2. When none of the request lines are high, the arbiter parks the grant ong2 in the next cycle.3. The grant lines, g1 and g2, are mutually exclusive.It is difficult to locate a book on formal verification that does not have anarbiter example - we hereby follow the tradition!
