From Wikipedia, the free encyclopedia

Functional verification, in electronic design automation, is the task of verifying that the logic design conforms to specification. In everyday terms, functional verification attempts to answer the question "Does this proposed design do what is intended?" This is a complex task, and takes the majority of time and effort in most large electronic system design projects.

Functional verification is very difficult - it is equivalent to program verification, and is NP-hard or even worse - and no solution has been found that works well in all cases. However, it can be attacked by many methods. None of them are perfect, but each can be helpful in certain circumstances:

• Logic simulation simulates the logic before it is built.
• Simulation acceleration applies special purpose hardware to the logic simulation problem.
• Emulation builds a version of system using programmable logic. This is expensive, and still much slower than the real hardware, but orders of magnitude faster than simulation. It can be used, for example, to boot the operating system on a processor.
• Formal verification attempts to prove mathematically that certain requirements (also expressed formally) are met, or that certain undesired behaviors (such as deadlock) cannot occur.
• HDL-specific versions of lint, and other heuristics, are used to find common problems.

Simulation based verification (also called 'dynamic verification') is widely used to "simulate" the design, since this method scales up very easily. Stimulus is provided to exercise each line in the HDL code. A test-bench is built to functionally verify the design by providing meaningful scenarios to check that given certain input, the design performs to specification.

A simulation environment is typically composed of several types of components:

• The generator (or irritator) generates input vectors. Modern generators generate random, biased, and valid stimuli. The randomness is important to achieve a high distribution over the huge space of the available input stimuli. To this end, users of these generators intentionally under-specify the requirements for the generated tests. It is the role of the generator to randomly fill this gap. This mechanism allows the generator to create inputs that reveal bugs not being searched for directly by the user. Generators also bias the stimuli toward design corner cases to further stress the logic. Biasing and randomness serve different goals and there are tradeoffs between them, hence different generators have a different mix of these characteristics. Since the input for the design must be valid (legal) and many targets (such as biasing) should be maintained, many generators use the Constraint Satisfaction Problem (CSP) technique to solve the complex testing requirements. The legality of the design inputs and the biasing arsenal are modeled. The model-based generators use this model to produce the correct stimuli for the target design.
• The drivers translate the stimuli produced by the generator into the actual inputs for the design under verification. Generators create inputs at a high level of abstraction, namely, as transactions or assembly language. The drivers convert this input into actual design inputs as defined in the specification of the design's interface.
• The simulator produces the outputs of the design, based on the design’s current state (the state of the flip-flops) and the injected inputs. The simulator has a description of the design net-list. This description is created by synthesizing the HDL to a low gate level net-list.
• The monitor converts the state of the design and its outputs to a transaction abstraction level so it can be stored in a 'score-boards' database to be checked later on.
• The checker validates that the contents of the 'score-boards' are legal. There are cases where the generator creates expected results, in addition to the inputs. In these cases, the checker must validate that the actual results match the expected ones.
• The arbitration manager manages all the above components together.

Different coverage metrics are defined to assess that the design has been adequately exercised. These include function coverage (has every function been exercised?), statement coverage (has each line of HDL been exercised?), and branch coverage (has each direction of every branch been exercised?). None of these are sufficient to prove a design works, but all are helpful in pointing out areas of the HDL that have not been tested.

• Certess Technology