( ESNUG 558 Item 1 ) -------------------------------------------- [02/19/16]
From: [ Jim Hogan of Vista Ventures LLC ]
Subject: Jim Hogan on how "this is not your father's formal verification"
Hi, John,
First, some U.S. cultural history for your non-U.S. readers (and for those
U.S. engineers born after 1980). Back before Facebook and the Internet, the
way most Americans got their news was from printed magazines and newspapers.
This 1988 ad is where the "this is not your father's..." meme came from.
I'm showing your readers this old print ad because the one big takeaway I
want them to get from this report is how dramatically formal verification
has grown over the last 20 years. This is not their father's formal.
---- ---- ---- ---- ---- ---- ----
Our present day way of verifying chips all started when Cadence acquired
Gateway DA back in 1989 -- and it started selling the Verilog-XL simulator.
Prior to 1989, the closest thing to chip simulation was an old 1973 FORTRAN
program from U. Berkeley called "SPICE1", but it only did nodal analysis
of analog circuits. Cadence Verilog-XL was the world's first digital HW
simulator that worked at the digital gate-level (or higher).
At first, Verilog simulation was used to do simple design assurance testing,
making sure your chip's RTL code functionally matched the original design
intent as described in your chip spec. "This is a simple adder. If I feed
it 2 + 2 as inputs in my Verilog simulation, does it output 4?"
As design sizes grew, engineers began "bug-hunting" in Verilog by creating
directed tests to uncover bugs for problematic corner cases.
Then Synopsys created Design Compiler, which automatically converted your
chip's Verilog RTL source code directly into gates. And it had everyone
asking:
"How do I know that my Design Compiler output in gates is functionally
the same as the Verilog RTL source code that I fed into it?"
And this is where, for most chip designers, formal tools first appeared on
the scene in 1999 as the Verplex Conformal LEC logic equivalence checker.
But for many chip designers, having any formal tool say "that chip is OK"
didn't help at all. Why? Formal was considered to be rocket science that
worked using peculiar mathematical interpretations. Engineers like to
understand what's going on "under the hood" of a tool, and formal felt like
a black art.
Instead of answering the "do I trust this Design Compiler output?" question,
it just moved the problem into a "do I trust this formal tool" question.
But engineers are practical.
As time went on they learned to trust formal because it worked. If a tool
makes their life easier, they will use it.
---- ---- ---- ---- ---- ---- ----
Over the past 20 years formal has grown in chip design verification due to:
- Assertions and properties are an accepted part of verification. Also
since the early days of 12 assertion types (ESNUG 487 #3), the chip
verification community has de facto standardized on roughly 90% SVA
use and 10% PSL use.
- Exhaustive state-space testing is something chip designers really
like. Verilog/VHDL simulation plus debug tools plus linting is still
useful for chasing bugs -- but they're not exhaustive. Formal is.
- Formal plays nice with simulation. Engineers can use formal output
in VCS/QuestaSim/Incisive and vice versa. Formal complements sim.
- Formal Apps make using formal easy for non-formal users. Now you don't
even need to write assertions because some app will do it for you.
- Faster CPUs and there are more new formal algorithms than before. Formal
is now even used to detect unauthorized accesses from one part of your
chip to another part of your chip -- something unheard of 20 years ago.
These factors have made formal common. In the old days Jasper shipped an AE
with every product. Now you no longer need a guru on staff to use formal.
Here's how formal has grown from the mid 1990's to 2016:
To drive home my point again, this is not your father's formal.
---- ---- ---- ---- ---- ---- ----
EC, F-ABV, AND APPS
The 3 major sections where formal is used in chip verification today are:
1. Equivalency Checking (EC)
2. Formal Assertion Based Verification (F-ABV)
3. Formal Apps
Below are quick engineering backgrounders for these 3 divisions of formal.
EQUIVALENCY CHECKING (EC)
Equivalency checking (EC) involves formally comparing one representation of
a design against another to verify that the functionality is the same. Some
key ways equivalency checking is used today:
- Comparing design representations for functional equivalency at different
design abstraction levels. EC can further be distinguished by:
- RTL-to-ASIC Gate Level. Checking your RTL code against your
post-synthesis gate level code of an ASIC design. Since neither
Design Compiler nor Genus ASIC synthesis changes your register
configurations -- your formal tool only focuses on the
combinational logic between registers.
- RTL-to-FPGA Gate Level. Checking your RTL code against the post-
synthesis gate level code of your FPGA design. Here, Synopsys
Synplify, Xilinx Vivado, and Altera Quartus FPGA synthesis change
the register configuration -- and your formal tool must also take
the timing differences into account when checking functionality.
This is known as "sequential" EC.
- C-to-RTL. Checking your SystemC/C/C++ code against your RTL code
following high level synthesis (HLS) to see if your design intent
is upheld. SystemC designs usually have very limited timing
information -- they rely on Cadence Stratus or Mentor Catapult HLS
to add timing detail to your final synthesized RTL code. As such,
this is also a sequential operation. Calypto SLEC is commonly used
here, but it's rumored that OneSpin is also working on SystemC
sequential EC also.
Throughout these changes, you need to make sure that your design's
behavioral intent is maintained/honored.
- Comparing different RTL code or gate level code of the same design to
make sure they have the same functionality.
- RTL-to-RTL EC or Gate-to-Gate EC. Used after code optimizations.
For example when you do power optimizations, make small ECOs, or
add scan test logic. Cadence Conformal and Synopsys Formality
are typically used to do this.
In addition, sequential equivalency checking is often needed here,
as your register configuration may have been altered along the way.
This is where Mentor SLEC and OneSpin EC-RTL, JasperGold, and
Synopsys Hector come into play.
EC was formal's first commercial "killer app", starting with the founding of
Verplex in 1997.
FORMAL ASSERTION BASED VERIFICATION (F-ABV)
The goal of Formal Assertion Based Verification (F-ABV) is to make sure:
- your design (or code segment) functions according to the spec, and
- your entire spec has been fully implemented.
F-ABV verifies that the properties of your design source code functionality
match those described in your spec. These properties of your design are
described using assertions written in either SVA or PSL.
Formal ABV is also used to verify design intent under all implementations.
That is, it tests to see if your original design functionality is still
maintained regardless of any micro architecture changes.
Formal ABV is about asking design functionality questions, such as "Can my
code do X?" or "Will my code ever do Y?" -- which the formal tool will
answer by examining the entire state-space of the design.
For example:
Q: If block 1 sends a "request" to block 2, will block 2 always send
an "acknowledgment" signal within X cycles?
A: The formal tool can tell you one of two possibilities:
- yes (or yes within the number of clock cycles that can be checked)
- no (and shows an example where this will not occur)
In its early days, formal assertion-based verification was mostly limited to
verification engineers doing corner-case testing -- in situations where it
was hard to create intricate scenarios using Verilog simulation.
Today F-ABV is used by all engineers for directed testing, functional block
tests, IP integration, protocol compliance, safety critical designs, etc.
FORMAL APPS
Writing assertions is a complicated and time consuming task for designers.
To their delight, there are now formal apps which, for specific situations,
automatically create assertions. Some formal app categories:
- General Design Issues like register checking, connectivity checking,
structural property generating, unreachability, scoreboarding.
- Safety/Security like fault analysis, unauthorized accesses.
- Structural Operation like CDC, power management, X-propagation.
- Assertion Creation like sim-trace, protocol compliance,
arithmetic precision, equivalence checking.
For an app example, let's look at a typical "Register Checking" formal app.
Registers are sets of flip-flops buried all over your design code. For a
large design, you may have 100s or 1000s of registers.
- Each register is uniquely identified using a unique address.
- All registers and their addresses are defined in a register
(or memory) map - a file which is 100s of lines long.
- The actual register locations must be consistent with the map file
to ensure consistency between hardware and software; it's common to
make a mistake between the different versions of HW or SW.
The "Register Checking" formal app reads in your Verilog/VHDL design source
code and your map file, then automatically:
- Generates appropriate assertions (this may or may not be hidden)
- Uses a formal engine to test that each register is at its expected
location and is operating as expected.
Careful note: RTL simulation is not even used here. It's purely formal.
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
C-BASED DESIGN, CARS, POWER, AGILE, PROTOCOLS, AND SAFETY
There are six major drivers pushing more use of formal tools today:
- C-Based Design for algorithm and hardware/software implementation
lends itself to that spec being transcribed into assertions and
applied directly to the C code with a formal engine.
- Automotive Chips need formal to create high-reliability and to
be able to recover from transient errors as the car runs.
- Lower Power Chips (like for cell phones) use formal for clock
switching, managing Dark Silicon, and "reset" sequences.
- Agile Chip Design Teams have a lot of pressure to "shift left"
on catching bugs early in the design cycle. Lots of formal!
- Yet Another Protocol means that there's alway 27 new IP and/or
bus interface standards that need formal compliance checks on.
- Security & Safety means doing exhaustive formal proofs so your
nuclear powerplant controller can only be accessed by the good
guys -- and not the bad guys. No secret unauthorized access paths!
BTW this stop-unauthorized-accesses is a major new growth area for formal.
Anyway, since equivalence checking is already well-understood by most chip
designers, I'm focusing this rest of this report on F-ABV (ESNUG 558 #2)
and Formal Apps (ESNUG 558 #3) -- the two segments where I expect the most
expansion for formal.
- 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
|
|
