( ESNUG 558 Item 2 ) -------------------------------------------- [02/19/16]
From: [ Jim Hogan of Vista Ventures LLC ]
Subject: Where Formal ABV whomps HDL simulation for chip verification
Hi, John,
The truth is Formal and Verilog/VHDL simulation go quite well together.
While simulation is time-based, and formal is state-space based. Any
verification plan that uses both simulation & formal will hit its coverage
goals much faster because together they perform a broader range of tests in
much less human time.
Anyway, my true goal here is to show your readers how Formal Assertion-Based
Verification (F-ABV) has expanded into chip verification -- and where it
beats old school standalone Verilog/VHDL RTL simulation.
The general rule is:
- FORMAL operates on all states concurrently over short bursts of time.
For example, if you have 27 scenarios which must be examined at the
same time (e.g. 27 branch conditions), formal works well and will
examine each of these branches to a typical depth of 30 clock cycles.
And it can go up to 150 clock cycles in, depending on the code.
- SIMULATION can be thought of as operating on limited set of states
over large timescales. For example, if you have one sequence going
state-by-state over a 1000 clock cycles, simulation is far better.
Fundamental differences between Verilog/VHDL simulation and F-ABV:
- Simulation
Verilog/VHDL simulation requires time-based stimulus to transition your
chip around a specific sequence of states. You write test vectors to
get the simulator to cycle through a series of design states to reach
a particular operational scenario of interest. With early simulation,
you reach a reasonable level (~80%) of coverage quickly, because a few
tests will run a design through most of its basic operating scenarios.
However, to get a high coverage level (close to 100%), a much larger
number of tests is needed to get the design into the corner cases that
early simulation doesn't touch. Writing testbenches to do this is a
lot of work, and it's also humanly impossible to test all possible
scenarios that a chip can get into.
- Formal Assertion-Based Verification (F-ABV)
Formal ABV operates in the state-space. It has a record of all states
a design can get into, so it does not require stimulus to drive the
design into a specific state. You use assertions to ask questions
about different operational state scenarios, and receive an exhaustive
reply as to every state related to the scenario in question.
As you increase the number of cycles, the number of state transitions
for your design grows exponentially. This is why engineers like to use
formal on the more obscure scenarios, so they can be tested.
To improve formal tool performance, engineers use constraints to focus
it away from states which do not occur in real life. "Why waste formal
tool CPU runtime testing states that the chip will never get into?"
F-ABV usually beats out Verilog/VHDL simulation when you use:
- Finite State Machine (FSM) logic and other control structures
- Communication or handshaking protocols where specific actions
and reactions are expected over time
- Data transport mechanisms, such as pipelines and bus bridges
- Check logic that's wrapped around certain design structures,
e.g. FIFO full/empty logic
- Bug hunting. Testing for corner-case scenarios in a large
block -- especially where it is hard to drive the design into
the state where this corner-case may be observed
- Testing stuck-at faults across various operating conditions
Formal ABV and simulation are already commonly used in the same design flow.
The traditional approach is often to do simulation first, then look at ways
to close the coverage gap using F-ABV. However, it's more efficient to look
at the full design up front in F-ABV first to quickly identify the scenarios
where F-ABV is more useful.
SIX WAYS FORMAL ABV IS BETTER THAN SIMULATION
Let's dive into more detail on where design teams generally find F-ABV is
more efficient than simulation.
1. General Assurance or Functional Testing
F-ABV is particularly useful for verifying state-intensive blocks such as
FSMs and control logic. Here assertions are created to get full overall
coverage on a design block -- and is particularly effective when there's
a complex state machine involved which must be exhaustively tested.
2. Corner Case Testing or Bug Hunting
F-ABV is often used to test certain scenarios that are hard to recreate
during Verilog/VHDL simulation, due to the complex stimulus required to
get the block into the problem state.
This is especially true when many parts of the design must be manipulated
to reach the target problem state. Formal is then used to augment HDL
simulation because you can specify a particular problem corner case using
constraints and assertions.
This is so thorough that it's used to test nuclear power plant controls.
3. Assume-Guarantee
If you have Verilog/VHDL code that's too big for Formal ABV to digest,
you can partition that source code into smaller, more manageable blocks.
For example:
- You break your design into 3 blocks that are chained together in
sequence, such that the 1st block drives the 2nd block which drives
the 3rd block.
- You then verify the 1st block with F-ABV using an initial set of
assertions and constraints specific only to that 1st block.
This verification task then creates a new set of assertions
called "1st block output" assertions.
- You then convert those new "1st block output" assertions into
constraints which are fed as "2nd block input constraints". The
assertions for the 2nd block are now much simpler for F-ABV to
create because they have been constrained from the 1st block.
- Next, the 2nd block's output assertions are turned into constraints
which are fed as inputs constraints to the 3rd block.
- And so on.
This is easy to do because the SVA assertion format and SVA constraint
formats are very similar.
This "Assume-Guarantee" approach makes it easier to develop assertions
for large design elements.
Assume-Guarantee comes from the idea that you are testing assumptions
about blocks, then propagating them downstream through the design.
4. Integration or Structure Testing
This is using Formal ABV to test if your IP blocks are all wired up to
each other correctly, plus it goes beyond that to check for functional
inconsistencies during operation, based on the chip's architecture.
An example is: before RTL synthesis, you have a 4-bit register array.
A 4-bit array can only be addressed from 0 to 15. F-ABV checks to see
if bad addresses 16, 17, 18... come in.
These are the cheap seats for formal, because it's a replacement for
simple linting. However, the additional checks for operational errors
due to connectivity mistakes are something that linting doesn't do.
It's heavily used to do protocol compliance checking with established
interface standards like ARM AXI, PCIe, AHD, and APB.
5. Directed or Component Testing
Most of the time, it's verification engineers who are the ones who use
F-ABV. Directed testing is used by design engineers. In this
case, the designers use formal ABV to pre-verify small IP components for
specific functionality, prior to integrating them into a larger block.
With this directed test method, the designers then either provide the
assertions to the verification team with the IP, or use the assertions to
demonstrate a sign-off criteria.
A recent twist is F-ABV runs examples of chip operation with minimal
input, and then use these same examples to generate simulation tests.
You create your assertions, run the formal tool, verify it's correct,
then you feed those assertions into your RTL simulation.
And yet another new tweak to this twist is that your formal tool also
now generates a Verilog/VHDL simulation testbench.
Designers love this.
6. Abstract Algorithm Analysis (C/C++ Property Checking)
This is where F-ABV is used on SystemC/C++ algorithm code targeted for
High Level Synthesis (HLS). The assertions here only have limited
sequential detail which corresponds to the high level specification
of algorithm behavior.
This use of F-ABV is not limited to SystemC/C++. It can be applied to
any code written at a high level abstraction.
Engineers are working on using these same assertions post-synthesis on
fully-timed RTL code to test that the algorithm's behavior has been
preserved. The problem here is that they must write assertions that are
relevant to both the untimed pre-synthesized code and the cycle-based
HLS output -- not an easy task to do.
FIVE WAYS TO CREATE ASSERTIONS WITHOUT MANUALLY WRITING THEM
System Verilog Assertions (SVA) and PSL both have a rich syntax which lets
you create full temporal assertions ranging from simple operation checks to
extended transcriptions of specification elements. One major roadblock
to using assertions was that it took a lot of engineering man-hours to write
them. Engineers hated this extra work.
This section is on the available options engineers have to save time in
creating SVA or PSL assertions automatically instead of by hand.
1. Generating from RTL design code
There are assertion (or property) synthesis tools such as Synopsys
NextOp and Cadence JasperGold which attempt to synthesize assertions
directly from your chip's RTL source code and simulation tests. There
are also formal apps which do the same thing.
Other vendors sell tools that automatically generate assertions to test
for specific common design issues (e.g. "array out of bounds" access).
They extend automated testing beyond plain old HDL linting by checking
the operation of your chip -- in addition to code syntax and semantics.
These tools include OneSpin Inspect, Real Intent Ascent, and Mentor
AutoCheck.
2. Abstract/Graphical Representations
A number of schemes exist which allow assertions to be written in an
abstract or graphical fashion. These include IBM Diver and Cadence
Jasper Visualize for graphical entry.
For abstract entry, OneSpin Operational Assertions is a SV class library
to provide transactional assertions. You write abstract SV functions
which are then automatically converted into lower level assertions.
The Accellera Portable Stimulus Group is currently focused on simulation
stimulus, but is also rumored to be discussing higher level assertions.
3. Alternative Specification Models
In #2 above (Abstract/Graphical Representations), the engineers create
assertions directly -- ans they are thinking in terms of the assertions
themselves.
With an "Alternative Specification Model" the engineers are instead
thinking in terms of their design spec. They write a separate model in
a special proprietary language that is then converted into testbenches
and assertions.
Examples of this approach are Logic Refinery RuleSmith, and arguably
Cadence Verisity Specman 'e' (although there's no 'e'-to-SVA translator).
4. Automated Tools & Formal Apps
In another section of this report (ESNUG 558 #4), we discuss how 16 types
of formal apps generate assertions based on a specific design and/or for
a specific complex verification task.
Some companies allow these assertions to be visible and editable, whereas
others do not. Not all companies offering these formal apps are formal
verification vendors (e.g. security verification company Tortuga Logic).
5. Assertion Verification IP (VIP)
Most formal verification vendors, along with a number of consultants and
IP providers, sell assertions packaged into Verification IP (VIP) to
test specific design scenarios, busses, and protocols. "Why should I
have to write PCIe assertions when we can just buy them?"
Cadence, Mentor, OneSpin, Synopsys all offer a wide range of VIP models.
---- ---- ---- ---- ---- ---- ----
What follows next in ESNUG 558 #3 is a detailed technical discussion of the
metrics and gotchas of F-ABV tools.
- Jim Hogan
Vista Ventures LLC, OneSpin BoD Los Gatos, CA
---- ---- ---- ---- ---- ---- ----
Related Articles
Jim Hogan on how "this is not your father's formal verification"
Where Formal ABV whomps HDL simulation for chip verification
9 major and 23 minor Formal ABV tool metrics - plus their gotchas
16 Formal Apps that make Formal easy for us non-Formal engineers
Hogan on Cadence, Mentor, OneSpin, Real Intent, Synopsys formal
Join
Index
Next->Item
|
|
