ABV - Assertions Based Verification
Assertions are closely related to the previously discusses constrained random verification. The set of produced test vectors can be very large while applying new verification techniques like constrained random verification. Simulation of a design with full testbench takes often several days. Even if we cover entire design with detailed tests one more problem arises. How to effectively debug our design and avoid multiple simulation runs, which take days. The propagation time for an error from its source to design outputs can be very long. Usually, incorrect operations of the tested design appear on its outputs several hours later during simulation. Verification engineers may spend several days running subsequent simulations and looking for source of the error. It is possible to run one simulation with dumping full debugging information and states of all signals but it slows down significantly simulation and does not help much.
Assertions address this issue and help verification engineers to work more effectively. Assertion is a dedicated code, which controls operations of tested units and reports immediately detected errors. Assertions have been used since many years in hardware description languages. VHDL language provides assert construct for modeling combinatorial assertions. Verilog-HDL assertions are modeled using if(...) $display constructs. However, assertions based verification was formalized during past several years and can be now systematically used by verification engineers.
Using assertions in a design provides the following benefits:
-
Detecting errors close to the source
-
Design functionality is documented in a form of executable specification
-
Correct operations can be also detected and logged for coverage analysis
It is worth mentioning that assertions are used not only to detect errors. We can also detect correct design operations to check if tested units are fully covered with detailed testes.
Assertions are getting popular and many EDA vendors started working on formal verification tools. Such tools analyze statically the design code and detects conditions that causes assertions failures. The same assertions will fail during simulation if we have fully covered design and enough time to wait until the failure conditions are reached. Formal verification is much faster. It reports quickly all possible assertions that fail during verification. However, it is quite difficult approach and requires from the user to define inputs behavior to correctly analyze the code. Assertions can be also checked dynamically during simulation and it still seems to be more popular approach than formal verification.
Assertions should express design intent for a module or its interface. Several languages dedicated to assertions are available on the market. The languages have different syntax but their structure is quite similar. The languages allow to define Boolean equations and sequences of such equations in time. An example of such language is PSL (Property Specification Language). Below is an example of VHDL code with PSL assertions.
process(CLK, RESET)
begin
if(rising_edge(CLK)) then
if(RESET='1') then
shift_reg <= (others=>'0');
else
if(CLK_EN='1') then
shift_reg <= shift_reg(SIZE-2 downto 0) & SHIFT_IN;
end if;
end if;
end if;
end process;
SHIFT_OUT <= shift_reg(SIZE-1);
--psl ChReset: assert always (RESET -> next(or_reduce(shift_reg)='0')) @rising_edge(CLK);
--psl ChShift: assert always ({CLK_EN[*SIZE]} |-> {SHIFT_OUT=prev(SHIFT_IN, SIZE)}) abort RESET @rising_edge(CLK);
--psl CrShift: cover({not RESET and CLK_EN; shift_reg(0)=prev(SHIFT_IN)}) @rising_edge(CLK);
HDL designer is focused on single cycles while writing RTL code. Assertions languages work differently, they keep designers focus on a sequence of cycles, which should appear in the tested design. It is not very likely to write the same errors in RTL and assertion language. We should take a closer look into PSL language structure to understand assertions languages. PSL is divided into four layers:
-
Boolean layer. It is used to build expressions that identify occurrence of some important events in the tested design
-
Temporal layer. We can define here an order of our events in time. It means that we can define here sequences that describe properties of our design
-
Verification layer. This layer specifies how all the sequences should be treated during verification. The sequences may describe valid design operations and any difference detected during verification is reported as an error. Other sequences may be checked to verify if they are covered by tests
-
Modeling layer. This layer is used for modeling design inputs. It is used in formal verification.
PSL language has multiple flavors of its syntax. The is the most important advantage of the language. We can use VHDL functions and operators while writing PSL assertions for VHDL code. Similarly in Verilog-HDL or SystemC languages. PSL uses functions and operators available in hardware description languages and does not define the same operators in its syntax.
Assertions works very well for detecting the following errors:
-
Incorrect stimulus
-
Inter-connection errors
-
Signaling protocol errors
-
X,U value propagation
-
Block functional errors
Assertions solve the debugging problem mentioned earlier in the document. They simplify verification engineers work and ensure higher verification quality. They are really beneficial when our modules are integrated some time later with larger system. The time spent on writing assertions is recovered back during simulation and debugging of the design or further integration with larger systems.
|
Home
