( ESNUG 558 Item 4 ) -------------------------------------------- [02/19/16]
From: [ Jim Hogan of Vista Ventures LLC ]
Subject: 16 Formal Apps that make Formal easy for us non-Formal engineers
Hi, John,
While standard F-ABV tools can solve a lot of verification problems for a
verification engineer well versed in Formal -- there's a set of tools
called "Formal Apps" that does design-specific assertion writing for you;
and then it automatically runs these assertions in your Formal tool of
choice for you. It's prepackaged Formal for the non-Formal user.
This approach both saves engineering man-hours plus it ups the quality of
the assertions used to verify your chip. (Remember assertions have a
Garbage In, Garbage Out sensitivity. If you try to verify your design
with bad assertions, your verification fails.)
Here's the 16 major categories of Formal Apps sold on the market today:
1. Register Checking App
2. Connectivity Checking App
3. Structural Property (or Assertion Synthesis) App
4. Activation Checks and Code Unreachability App
5. Scoreboarding App
6. Safety Fault Analysis App
7. Security Verification App
8. Clock Domain Crossing (CDC) App
9. Power Domain Management App
10. X-Propagation Checking App
11. Abstract Assertion Authoring App
12. Sim-Trace Property Synthesis App
13. Protocol Compliance Apps
14. Sequential Verilog/VHDL RTL Equivalency Checking App
15. Arithmetic Precision Analysis App
16. And the 3rd Party App Marketplace
Real Intent was the first formal vendor to offer a formal app. The company
started off with property checking, then in 2007 they announced their Clock
Domain Crossing (CDC) "checker" app.
All the major verification players now have formal apps -- although the term
"app" itself was made popular by Jasper.
Below I've compiled the major formal apps commercially available today.
- Jim Hogan
Vista Ventures LLC, OneSpin BoD Los Gatos, CA
---- ---- ---- ---- ---- ---- ----
1. REGISTER CHECKING APP
Register checking involves verifying a register address map against your
Verilog/VHDL RTL code. In your RTL code, a register consists of flip-
flops buried within logic. It must be accessible from your bus interface.
It's easy to make a mistake when wiring these flip-flops to the correct
address decoder and "read"/"write" logic. This error won't be picked up
until a software driver discovers it's not accessing the correct registers;
which is quite late to be discovering HW problems in a chip project.
Without the app: Most chips can have 100s to 1000s of registers, so checking
source RTL for addressing consistency is very painful to do by hand and it
can take weeks. The process is error prone, and a common source of bugs.
With the app: Checking the register address map against your RTL source code
is automatic, has no human errors, and only takes 1-2 hours. The register
address map is typically in IP-XACT or Accellera RDL format. Depending on
the app, other functional details -- such as correct "read and write" access
over a specific bus protocol -- may also be checked. Often the same IP-XACT
file is used in the chip's software spec, ensuring consistency between the
hardware and software register addresses.
2. CONNECTIVITY CHECKING APP
Are the parts of your design accessing each other correctly? This can be a
real check to see if your chip wiring is correct -- or testing if a virtual
connection path between two chip parts exists through on-chip networks,
busses and other structures. "Is the interrupt output from peripheral 53
actually making it to the interrupt controller in CPU 3?"
Without the app: There are easily 1000's of real and virtual connections
on a chip. Some are just direct wires, others may be complicated paths
going through 10's of elements on your chip.
Manual connectivity checking is an error prone, and irritating process, that
can take days. No one wants to do this job. And it's not a value added
task for engineers. It's perfect for automation.
With the app: Feed the app your Verilog/VHDL source code plus your list of
key signal connections, and it automatically tests all the real and virtual
connections. The entire check is just 1-2 hours for a 1000 connections;
with no human errors.
3. STRUCTURAL PROPERTY (OR ASSERTION SYNTHESIS) APP
The structural property, or assertion synthesis, app creates properties (or
assertions) from your RTL code, to test for common HDL issues.
Without the app: Static linting tools like Spyglass use syntax and semantics
to check your source code. It will then flag thousands of potential errors;
of which only a few may occur during actual chip operation. This is the
classic false positive problem. The chip designer must check them all out,
which is an intensive process done by hand - and again, error prone.
With the app: Initially, the app appears to operate the same as a static
linting tool; however this app generates formal assertions to check whether
those errors will actually occur in the chip during operation.
Because this formal app only identifies actual operational problems, it
narrows the human engineering follow-up needed and dramatically reduces the
manual overhead needed -- by as much as 10X. It eliminates the time wasted
having to sort through every "potential" error.
For example, imagine an array of 47 elements, addressed with a variable that
can take a value from 0-Y, where Y is greater than 47. That is, a classic
"array-out-of-bounds" check.
- A linter will flag this as a possible error.
- This formal app inspects your RTL code *operation* to see if the
addressing variable ever goes greater than 47, and only flags
the actual code only if this occurs. It also generates counter-
example waveforms, making these errors easier to fix.
4. ACTIVATION CHECKS & CODE UNREACHABILITY APP
These formal apps check your RTL design source code for unreachable parts.
Without the app:
- Design error. One example of a design error could be if a code segment
is not connected correctly, such as a bad arc in a state machine. This
error could take a lot of time and effort to uncover through traditional
Verilog/VHDL simulation.
- Over-constrained code. These are constraints added to narrow the formal
verification process to only legal operations. Over-constraining is
when important functionality is ignored during verification. You had
constrained so much you fail to test functional parts of the design.
- Integration issues. Your IP was miswired during integration, resulting
in dead parts of your chip. This leaves swaths of inactive and
unreachable RTL code.
- Unremoved test code. In some cases unreachability is originally created
on purpose -- for example, temporary test code -- but was accidently
left in your design. It's an unreachable independent block within the
chip, costing area and potentially more serious problems if it happens
to get activated.
- Redundant code. Two identical blocks included for fail safe operation
in the chip. Can both blocks be activated independently? This is hard
to verify because you can get strange effects during RTL simulation if
you are not expecting it. This formal app will pick out the two blocks
and tell you if one, or the other, or both blocks are active.
With the app: You catch all these dead spots that RTL simulation failed to
see. This formal app delivers a coverage metric for simulation by telling
your coverage tool which exact parts of your design can't be simulated.
The way it works is that you run the formal tool, get a list of dead spots,
then re-simulate in Verilog/VHDL. This tells the simulator "don't bother
trying to increase coverage on these parts of the design because they are
unreachable".
The app has general activation checks, toggle checks (signal activation),
FSM transition tests, etc.
5. SCOREBOARDING APP
Verification engineers must often check for data transport issues through
various on-chip structures -- such as does all the data going to a specific
design block arrive as expected? For example, "did the read from memory 47
actually arrive at CPU 6?"
Without the app: There are 1000s of data transport permutations. Imagine a
bus bridge with multiple data input and output ports. Using Verilog/VHDL
simulation, you would need to check all the possible permutations to all the
data inputs, and then check for the correct outputs.
This requires a tremendous amount of design stimulus. It can take 1000s of
man-hours to create and weeks of simulation to run. It's also very easy
to miss a specific case due to the sheer volume of work required.
With the app: You come up with a set of rules based on the chip design spec
on how the data will be transported. For example, "a 32 bit data packet
that arrives at input port C will then be routed 30 cycles later to output
port F without duplication."
The formal app inspects your design source code to provide an exhaustive
report on your expected data transport behavior. It confirms that the
data transport in your RTL code is operating correctly without having to
test every data permutation. This includes looking for missing data at
an output, duplicated data, or data output at an incorrect time.
This aspect of formal is brilliant because it saves 1000s of man-hours on
a project. And you also don't miss any possible errors.
6. SAFETY FAULT ANALYSIS APP
When a safety critical chip is in the field, it must be "fail-safe", meaning
it can recover in real-time from an operating condition failure -- such as a
memory bit flip due to electromagnetic interference.
This app makes sure bad things won't happen if any part of your chip fails.
That is, the chip detects and fixes the problem instantly and keeps working
even with the failure. (Error correcting codes and redundant modules are
two HW examples of this.)
Without the app: The initially obvious way to do safety fault analysis is to
break some part of your Verilog/VHDL code (i.e. change your design) and to
then re-simulate. However, ISO 26262 rules require that you run your test
without changing your design. So instead you must inject faults one-by-one
all over your design, and then see if your chip successfully recovers.
Others use old-fashioned fault simulation tools. The trouble with fault
simulation is that you must re-simulate the entire design for every single
fault. For a million gate design, you have a fault on every output of every
gate, i.e. 1,000,000 faults. A good fault simulator collapses the faults;
however the number of faults can still be as high as 70,000. This takes
months of CPU time.
This ISO standard also has an Automotive Safety Integrity Level D (ASIL-D)
requirement for diagnostic coverage; which sets the level of ability to
recover and be failsafe at >90%. This means that the chip must still be
able to recover even if >90% of all possible faults (injected one-by-one)
are triggered.
With the app: Using formal, all the safety fault analysis problems described
above are taken care of automatically. What happens is:
- Fault injection is done automatically (without changing your design).
- The follow-up analysis happens automatically.
- Fault injection is done in parallel, making a task which normally
takes months take only a few hours.
- Segments of design source code are inspected as though many faults were
simultaneously injected, then verifies the chip's recovery. That is,
it goes even further than the inject faults one-by-one testing.
This type of app is used for safety critical designs such as automotive,
aeronautical, satellites, medical, and nuclear power generation chips.
This app can also be used to meet high-reliability requirements which are
not safety critical. That is, if you have good recovery mechanisms on your
chip -- plus if you raise the "Mean Time Before Failure" (MTBF) of your
chip's various parts, it'll nicely be able handle transient errors. This
is important because with the life of cars now in the 10's of years, it's
more likely transient errors will be the most common problem encountered
during those decades instead of catastrophic failures.
7. SECURITY VERIFICATION APP
This is the anti-hacker app. It sniffs around for unexpected data access
paths internal to the chip that go from authorized areas to unauthorized
areas. It also looks for any backdoors into the chip. "Who knew you could
get to the president's bedroom if you took a path through the back kitchen
cellar entrance?"
Without the app: Simulating every possible data access path permutation is
not humanly feasible. There are always going to be paths that you miss.
So companies will often just build the actual chip (or at least an FPGA
prototype), give it to some hackers, and hope they find the flaws.
With the app: The verification engineer specifies the known possible attack
methodologies to the app. For example, designs use encrypted keys for
various purposes. These keys are stored in internal secure registers that
should only be accessible through one specific "read" method. Hackers try
to gain access by looking for a backdoor -- and the chip scan chain is one
such classic vulnerability. Once you specify that these key registers are a
"secure area", the formal tool will exhaustively inspect your design source
code for all possible path permutations of ways your key registers can be
accessed, including the scan path.
Common hardware cyber-security attacks can be in the form of:
- Integrity: operational attacks (e.g. hacking cars, drones, IoT devices)
- Confidentiality: theft of information (e.g. encrypted license keys)
The upside of using security verification apps is that they are automatic
and exhaustive.
8. CLOCK DOMAIN CROSSING (CDC) APP
The CDC app ensures clock signal integrity is maintained across the device.
Large chips now have 100s of clock domains, especially when you look at all
the permutations of derived clocks internal to the chip.
Large sections of a design can be asynchronous relative to each other
and can have random phase and frequency relationships. When a signal
transitions from one clock domain to another, it's a nightmare of race
conditions, meta-stability, and glitches.
Design engineers use double flip-flop (or sometimes even triple flip-flop)
synchronizers at clock domain boundaries to eliminate signal instability
between clock domains.
Without the app: It's humanly impossible to test the 1000's of permutations
of clock phases, frequencies, glitches, and transients. The scary method
is to build the chip with synchronizing circuitry on the clock domain edges
and hope that it works with minimal testing.
With the app: The CDC app examines all chip signals where they cross clock
domain boundaries. Depending on the app two tiers of info may be provided:
- It identifies all signals where they cross clock domain boundaries
that might be subject to instability.
- It analyzes the synchronizers to ensure that for all clock phases,
no signal instability is propagated in the chip.
This app is standard for all design flows of chips with multiple clocks.
9. POWER DOMAIN MANAGEMENT APP
This app tests the sequential switching logic used to turn "on" and "off"
all of the independent power domains, block-by-block on the chip. This is
to reduce power consumption and encourage more "Dark Silicon" on the chip.
Turning "on" a power domain while a chip is running typically requires a
complex "reset" sequence that (hopefully) does not disrupt the normal
operation of the rest of the device.
Without the app: Design teams must ensure that every single power domain
"start" and "stop" sequence is correctly initiated. This is virtually
impossible with Verilog/VHDL simulation due to unpredictable timing and
the sheer number of scenarios that require testing.
With the app: This formal app does an exhaustive time-independent analysis
of all power domain "start" and "stop" sequences. For example, a "reset" on
a power-up sequence is rigorously examined to completely eliminate unknown
states and X propagation issues. And this is all done without a single
power test vector being applied.
This app is only in limited use. The formal tool must look at the whole
design for each power domain, not just pieces, which uses boatloads of
memory. The designs today are so big that it takes weeks to run. Add the
permutation problem of multiple power domains, and the runtime is months.
Further, since software-controlled power domains are becoming more common,
eliminating the need for power switching logic, UPF usage is down.
10. X-PROPAGATION CHECKING APP
This app checks how wires, registers, or flip-flops somehow get into an
unknown state -- it's either a "1" or a "0" but you don't know which. This
is commonly known as an "X" state.
X states can be caused by timing errors, glitches, or insufficient "reset"
wiring/sequences. X states that appear during a Verilog/VHDL simulation run
indicate a possible bug in the design. It gets worse if the X values are
propagated across your chip.
Without the app: RTL simulation suffers from "X-Optimism" where additional
X states are inserted into situations where they shouldn't be. This can
lead to false X propagation issues, which can hide actual bugs in the chip.
With the app: An X-propagation app will automatically, and more reliably,
check the propagation of X-states to areas where they may be harmful in
the design.
For example, you have a flip-flop not controlled by "reset"; on power up,
it goes to an X state. You expect the downstream logic to get rid of the
X state, but for some reason it doesn't. This propagates errors downstream.
This app detects both the X state creation and the propagation problems
in your chip, instead of false X problems in your RTL simulation. In
addition, you don't need RTL simulation vectors to find these errors.
11. ABSTRACT ASSERTION AUTHORING APP
This app is for creating assertions at higher levels of abstraction. This
lets you more easily visualize the intent of your assertions -- to better
understand what you are trying to test.
Without the app: You would only write low-level assertions by hand, which is
done using System Verilog 90% of the time.
With the app: This app loads in the System Verilog libraries, then you
invoke these high level assertion types. These are easier to use because
they look like timing diagrams, which results in an overall 2X to 5X speed
up in assertion creation.
Using these high level SVA libraries to create low level assertion is
similar to UVM -- where you have sequences which drive sets of tests.
12. SIM-TRACE PROPERTY SYNTHESIS APP
A trace is a sequence of events that make up a particular RTL source code
operation leading to an assertion failure. This app is for creating
assertions by using sim-trace property synthesis; also called "behavioral
property synthesis" or "assertion synthesis". By using your existing
Verilog/VHDL simulation tests, this approach reduces the time and expertise
needed to create low level assertions.
This is not a linting tool to test your RTL design code -- instead it's a
method to create assertions from design intent.
Without the app: You would only write low level SVA assertions by hand.
With the app: These apps use simulation traces and RTL design information
to automatically generate assertions. You get FSDB or VCD trace files
from your RTL simulation. You then load in these trace files and your RTL
design code, and the app generates your assertions.
These property synthesis tools convert a single Verilog/VHDL simulation run
into multiple assertions. It expands the same test to more scenarios
without you having to learn the assertion syntax.
Caveat: This method depends on your design and simulation results being
correct. If either are incorrect, then you risk your generated assertions
also being incorrect.
13. PROTOCOL COMPLIANCE APPS
These apps confirm whether your chip design source code complies with common
bus and other protocol standards -- such as AMBA, APB, and AXI.
Without the app: Using behavioral/RTL/gate-level simulation to test for
potential protocol violations takes a very long runtime and it can easily
miss problems due to incomplete, hand-created tests.
With the app: A formal protocol compliance app uses a group of pre-defined
assertions to exhaustively verify your interface for compliance. By using
libraries, you can test for multiple protocols throughout your design. The
app will often also have a library of verification IP to test specific
protocols.
Protocol checking uses formal proofs to answer: "did my source code generate
only standard-compliant correct AXI bus transactions with correct timing?".
In contrast, simulation verification IP uses multiple Verilog/VHDL runs to
try to test if your entire PCIe block complies with the PCI standard.
Using these apps, teams can expect a 2-4X reduction in project verification
time; and more importantly the tests are exhaustive.
14. SEQUENTIAL VERILOG/VHDL RTL EQUIVALENCY CHECKING APP
This app answers "are these two RTL blocks functionally equivalent?". The
app goes beyond just structural equivalency. It also exhaustively searches
for the functional equivalency over time of these two blocks in your design.
It's used to quickly test ECOs/RTL power optimizations/scan-test without
having to run extensive Verilog/VHDL simulation.
Without the app: Typically designers use combinatorial equivalency checking
to verify ASIC synthesis. However, this approach is limited to two code
representations with an unchanged register configuration -- and reports
errors on equivalency differences that may come from changed registers
or other clocked elements -- even if the functionality is the same.
With the app: This app automatically compares two Verilog/VHDL code segments
for full functional equivalence, handling both combinatorial and temporal
equivalency.
The only limitation is state-space equivalency is not infinite -- it only
goes to a certain cycle depth, e.g. 30 clock cycles. This cycle depth is
a differentiator between vendor's apps.
In addition to late ECOs/RTL code optimization, the app is also used when
synthesis tools optimize register configurations, as is typical for FPGAs
and High Level Synthesis (HLS).
15. ARITHMETIC PRECISION ANALYSIS APP
This app reports whether the number representations used throughout your
chip datapath have the correct bit width for the required accuracy. This
is often necessary for abstract algorithm code.
Ignoring the complexity of fixed vs. floating point number systems, and
whether the numbers are signed, etc., a simple DSP example would be:
two 8-bit unsigned integer numbers multiplied together to create a 16-bit
number. You may not need 16-bit accuracy, you may only need the top 8 or
12 bits. Anything more than 16 bits would result in wasted transistors.
The reality is the arithmetic in the logic is extremely complex, as are the
representations of the numbers through the datapath. This app tests all
the number precision representations throughout the algorithmic block,
given the arithmetic performed, any normalization that occurs, etc, and it
ensures a correct and optimal bit-width.
Without the app: Engineers use pencil and paper to go through the design
by hand to make sure the number precision is correct for every number
representation in the datapath.
With the app: The app uses formal verification to test all the number
precision representations throughout an algorithmic block. It eliminates
the possibility of human error, ensuring a correct and optimal bit-width.
- If your bit-width is too large, circuit elements, and therefore
power consumption and chip real estate, will be wasted.
- If the bit-width is too small, overflow can occur leading to
false results.
Untimed algorithmic code, usually written in SystemC/C++ for High Level
Synthesis, typically makes use of signed fixed-point number systems.
---- ---- ---- ---- ---- ---- ----
16. AND THE 3RD PARTY APP MARKETPLACE...
This isn't an app per se, but more about a new business model which makes
formal apps available to the common engineer. For example, you have a guy
who's a serious expert in security flaws in AMBA busses. Instead of having
Mr. AMBA explain these flaws to your verification engineers, Mr. AMBA can
write a special 3rd party app that tests for his exact expertise.
To do this, your formal tool provider needs:
- an API in their formal tool that lets a 3rd party app developer
pass control and property info in and out of it.
- an encrypted licensing scheme so not everyone can use this API.
- OEM agreements and reduced pricing so users who want just the
3rd party app itself don't have the buy the full blown formal
tool, too, just to use it.
- a way to lock the 3rd party app with the formal tool, so the
user doesn't also get a general purpose full copy of the formal
tool for the discounr price of one app.
The idea behind all of this is to open formal apps into a similar 3rd party
market that both Apple and Goggle phone apps now have.
---- ---- ---- ---- ---- ---- ----
In ESNUG 558 #3, I discussed ABV metrics in detail. In ESNUG 558 #5, I show
how both the Apps and major formal ABV vendors fit against these metrics.
- 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
|
|
