In
electronic design automation
Electronic design automation (EDA), also referred to as electronic computer-aided design (ECAD), is a category of software tools for designing Electronics, electronic systems such as integrated circuits and printed circuit boards. The tools wo ...
, functional verification is the task of verifying that the
logic design
In computer engineering, logic synthesis is a process by which an abstract specification of desired circuit behavior, typically at register transfer level (RTL), is turned into a design implementation in terms of logic gates, typically by a comp ...
conforms to specification.
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 a part of more encompassing ''design verification'', which, besides functional verification, considers non-functional aspects like timing, layout and power.
Functional verification is very difficult because of the sheer volume of possible test-cases that exist in even a simple design. Frequently there are more than 10^80 possible tests to comprehensively verify a design – a number that is impossible to achieve in a lifetime. This effort is equivalent to
program verification
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal metho ...
, and is
NP-hard
In computational complexity theory, NP-hardness ( non-deterministic polynomial-time hardness) is the defining property of a class of problems that are informally "at least as hard as the hardest problems in NP". A simple example of an NP-hard pr ...
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
Logic simulation is the use of simulation software to predict the behavior of digital circuits and hardware description languages. Simulation can be performed at varying degrees of physical abstraction, such as at the transistor level, gate le ...
simulates the logic before it is built.
*Simulation acceleration applies special purpose hardware to the logic simulation problem.
*
Emulation
Emulation may refer to:
*Emulation (computing), imitation of behavior of a computer or other electronic system with the help of another type of system
:*Video game console emulator, software which emulates video game consoles
*Gaussian process em ...
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
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal metho ...
attempts to prove mathematically that certain requirements (also expressed formally) are met, or that certain undesired behaviors (such as deadlock) cannot occur.
*
Intelligent verification
{{Use American English, date = April 2019
Intelligent Verification, including intelligent testbench automation, is a form of functional verification of electronic hardware designs used to verify that a design conforms to specification before devic ...
uses automation to adapt the testbench to changes in the
register transfer level
In digital circuit design, register-transfer level (RTL) is a design abstraction which models a synchronous digital circuit in terms of the flow of digital signals (data) between hardware registers, and the logical operations performed on those ...
code.
*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
Generator may refer to:
* Signal generator, electronic devices that generate repeating or non-repeating electronic signals
* Electric generator, a device that converts mechanical energy to electrical energy.
* Generator (circuit theory), an eleme ...
generates input vectors that are used to search for anomalies that exist between the intent (specifications) and the implementation (HDL Code). This type of generator utilizes an NP-complete type of SAT Solver that can be computationally expensive. Other types of generators include manually created vectors, Graph-Based generators (GBMs) proprietary generators. Modern generators create directed-random and random stimuli that are statistically driven to verify random parts of the design. 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
Constraint satisfaction problems (CSPs) are mathematical questions defined as a set of objects whose state must satisfy a number of constraints or limitations. CSPs represent the entities in a problem as a homogeneous collection of finite constra ...
(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
A simulation is the imitation of the operation of a real-world process or system over time. Simulations require the use of models; the model represents the key characteristics or behaviors of the selected system or process, whereas the s ...
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
Monitor or monitor may refer to:
Places
* Monitor, Alberta
* Monitor, Indiana, town in the United States
* Monitor, Kentucky
* Monitor, Oregon, unincorporated community in the United States
* Monitor, Washington
* Monitor, Logan County, West ...
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
Coverage may refer to:
Filmmaking
* Coverage (lens), the size of the image a lens can produce
* Camera coverage, the amount of footage shot and different camera setups used in filming a scene
* Script coverage, a short summary of a script, wri ...
metrics are defined to assess that the design has been adequately exercised. These include functional coverage (has every functionality of the design been exercised?), statement coverage (has each line of HDL been exercised?), and branch coverage (has each direction of every branch been exercised?).
Tools
*
Aldec
Aldec, Inc. is a privately owned electronic design automation company based in Henderson, Nevada that provides software and Electronic hardware, hardware used in creation and verification of digital designs targeting FPGA and Application-specific ...
*
Arrow Devices
* Avery Design Systems: SimCluster (for parallel logic simulation) and Insight (for formal verification)
*
Breker Verification Systems, Inc.: Trek (a model-based test generation tool for complex SoCs)
*
Cadence Design Systems
Cadence Design Systems, Inc. (stylized as cādence), headquartered in San Jose, California, is an American multinational corporation, multinational computational software company, founded in 1988 by the merger of SDA Systems and ECAD, Inc. The co ...
*
EVE/ZeBu
EVE/ZeBu is a provider of hardware-assisted verification tools for functional verification of Application-specific integrated circuits (ASICs) and system on chip (SOC) designs and for validation of embedded software (software driver, Operating ...
*
Mentor Graphics
Siemens EDA is a US-based electronic design automation (EDA) multinational corporation for electrical engineering and electronics, headquartered in Wilsonville, Oregon. Founded in 1981 as Mentor Graphics, the company was acquired by Siemens in ...
*
Nusym Technology
Nusym Technology, Inc. was a company that produced intelligent verification software products, also known as ''intelligent testbench'' products, which are a form of functional verification that targets and maximizes test coverage of a logic design ...
* Obsidian Software
*
OneSpin Solutions
*
Synopsys
Synopsys is an American electronic design automation (EDA) company that focuses on silicon design and verification, silicon intellectual property and software security and quality. Products include tools for logic synthesis and physical design ...
*
Valtrix Systems: Sting (a versatile design verification tool for complex SoC/CPU implementations)
See also
*
Analog verification
Analog verification is a methodology for performing functional verification on analog, mixed-signal and RF integrated circuits and systems on chip.Henry Chang and Ken KundertVerification of Complex Analog and RF IC Designs ''Proceedings of th ...
*
Cleanroom software engineering
The cleanroom software engineering process is a software development process intended to produce software with a certifiable level of reliability. The cleanroom process was originally developed by Harlan Mills and several of his colleagues i ...
*
High-level verification
High-level verification (HLV), or electronic system-level (ESL) verification, is the task to verify ESL designs at high abstraction level, i.e., it is the task to verify a model that represents hardware above register-transfer level (RTL) abstract ...
References
{{Reflist
Electronic circuit verification
Logic in computer science