( DAC'20 Item 04a ) ----------------------------------------------- [03/09/21]
Subject: OneSpin's "going where Cadence isn't" approach is Best of 2020 #4a
WHERE THE BIG GUYS AREN'T: Years ago, I remember being on an EDA panel with
the then CEO of Mentor Graphics, Wally Rhines, and during the Q&A someone
asked Wally how can a small EDA start-up could succeed in an EDA world
dominated by SNPS, CDNS, and MENT. He answered:
"For an EDA start-up to succeed, it has to go where the Big Guys
aren't. Develop tools in niches where the Big 3 aren't helping.
Solve those problems for the chip designers and verifiers, and
you'll make good money."
- Wally Rhines, Mentor CEO (some time back in 2010 or 2012)
It turns out that OneSpin CEO Raik Brinkmann agreed with Wally's advice and
Raik made it his start-up's guiding philosophy. And it REALLY paid off:
"OneSpin has had a 50 percent compounded growth rate over the
last 4 or 5 years -- every year."
- Raik Brinkmann, OneSpin CEO in ESNUG 588 #14 at DAC'2019
ALMOST FULL BLOWN TOOLS: What makes this even more interesting, is that
OneSpin seems to be going to town on the features in their unique apps;
approaching their apps more like full-on products than as an 'app'.
|
|
|
|
GapFree app
|
RISC-V app
|
security apps
|
Brett Cline, of former SystemC "chicken suit" fame, backs this with:
"Our typical OneSpin customer comes to me to buy an app or
apps to solve a specific problem like RISC-V verification,
or detecting HW security Trojans, or FPGA migration."
- Brett Cline, VP of OneSpin Sales, (DC 03/05/2021)
Last year, users reported on Safety Critical, SystemC/C++, Floating Point
Unit, and EC-FPGA OneSpin apps -- they were industry firsts at the time.
This year, users reported on 3 more unique apps: RISC-V, GapFree, and
FPGA Retargeting -- plus a mess more users commented on the Security,
ARM AXI compliance, X-Propagation, and FPGA equivalency checking apps.
"Like a fine wine, formal tools easily take decades to mature."
- Jim Hogan, EDA industry luminary (1951 - 2021)
"I've known Raik for close to 15 years.
I am amazed how he and Jim Hogan took a failed OneSpin and not
only brought OneSpin back to life, but remade it into a successful
standalone EDA start-up in its own right."
- An Anon Formal User from DAC'20 #4c
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
QUESTION ASKED:
Q: "What were the 3 or 4 most INTERESTING specific EDA tools
you've seen in 2020? WHY did they interest you?"
---- ---- ---- ---- ---- ---- ----
OneSpin RISC-V formal app
The OneSpin RISC-V formal app does exhaustive formal verification on
a RISC-V processor to determine whether your RISC-V implementation
meets the expected RISC-V instruction set architecture specs.
Our team uses it on RISC-V processor cores supplied to us by our DoD
customers. It confirms ISA compliance.
Our main objective is to ensure whether the RISC-V core meets the ISA
specifications. However, any failing checks can be used to search for
potential hardware trojans or unintended functionality.
OneSpin's RISC-V app inputs consist of reading in the target IP,
extracting the design ISA and microarchitecture, and then performing
automatic pipeline and register mapping. It can take up to 2-3 hours
to set up.
The RISC-V app then generates specifications for the ISA and the
specifications are checked. Any failing checks are closely examined
and debugged.
The largest RISC-V design we ran on the OneSpin RISC-V app on had more
than 4 million gates. Once the setup was complete, running checks
took around 2 hours.
Prior to getting OneSpin RISC-V app, our verification efforts were based
on dynamic simulation and HW emulation.
- It took us several hours to develop suitable testbenches.
- And setting up the testbenches, makefiles, and scripts for
the simulator and emulator often took much longer than
setting up OneSpin's RISC-V formal verification environment.
On top of exhaustive verification of a RISC-V processor implementation,
it also gives us detailed information on the RISC-V microarchitecture,
pipeline structure and registers used by that processor implementation.
The app's biggest advantage over other verification methodologies is its
ability to perform *rapid* functional and security verification.
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
OneSpin Gap-Free app
It confirms the completeness of your formal verification.
UVM involves a lot of random simulations, with 'coverage' as its metric
for deciding when you're reasonably done. Full coverage is the point
where you feel you've exercised all the lines of code in your design.
With formal verification, you write assertions and use them with a
formal tool to verify that your design works as described in your
requirements specification. For the assertions that you write,
your checks are exhaustive.
The drawback is that you may have missing requirements, i.e., you may
not have checked everything in your design. You could have subtle
mistakes in the way you wrote your assertions.
These mistakes typically have to do with antecedents and consequences.
Your assertions will say, "IF my design has reached this particular
case, THEN these other things should be true."
Your design might have:
1. Over-constrained antecedents, where you look for very
specific cases, e.g. "IF condition 1 and condition 2,
THEN something happens."
"IF it's evening/dark and I'm home, THEN I turn on the porch
light." It's over constrained because I'm not checking for
the case where it's dark but I'm not home.
2. Under-constrained consequents that occur when you write the
"IF" portion correctly the but the 'THEN' portion doesn't
check everything.
"IF it's evening/dark, THEN I turn on the porch light" does
not check to see if you also closed the garage door.
3. Your assertions can also have unintentional mistakes where it
could result in *both* of the above.
If you know that you have these verification deficiencies it costs you
review effort to correct them.
How Gap-Free Verification Works
When you only use a formal ABV tool like OneSpin DV-Verify, you write
the assertions, check them against your design formally, and DV-Verify
will tell you if it meets that or not.
GapFree-verification goes one step above that. It does an automated,
formal check on the assertions you've written to ensure you haven't
forgotten to write any properties.
And because it's a formal check, you know it's a proof of correctness.
That is, if Gap-Free tells you that you passed, then you can be *very*
sure that you haven't missed anything.
I haven't seen this functionality from anyone else.
GapFree requires two inputs:
1. A completeness spec. This is easy for the user to create and
takes less than a day. You describe:
- Design inputs
- Design outputs
- Assertions to describe the resets
- A property graph <-- the list of assertions that you already
have. Then, at startup, you indicate which assertions that
can take effect, and the next assertions that can follow.
This is the set of operations in that can happen in the design.
- Exceptions <-- during a specific operation, my design's output
doesn't matter.
2. Your assertions.
Your assertions must be written in a certain way -- using OneSpin's
"Tidal Library" of System Verilog functions.
It is a proprietary library and a bit more constrained than normal
SVA; i.e., there are some things that you can do in SVA, that you're
not allowed in this library.
If you *start* out by writing your properties a little differently in
this way, it's not that different. If you already have existing SV
that took you 5 days to write, it might take you an additional day
to translate it.
Some restrictions:
- You must call the properties certain things for reset.
- Certain operators are not allowed.
- There's a certain way of doing things for storing information.
- You must follow the guidelines for how to write titles.
Gap free verification checks for and reports on:
- Missing requirements you're not verifying
- Over-constrained antecedents
- Under-constrained consequences
You then figure out why it's telling you there's a problem and the kind
of fix needed. There is a certain level of understanding you need to
figure out what the results means and how to debug them -- it is a bit
different from the traditional debugging.
OneSpin GapFree also demonstrates the absence of hardware bugs and
Trojans ambiguities.
- These can occur in the case where your assertions all pass, but
there are other cases that you're not checking for, where there
is a hidden functionality in your design that you didn't know
about. (i.e. an accidental state transition you didn't intend.)
- It could be something your engineer in there purely for debug or
testing, but maybe it could still be exploited later.
- If your assertions don't fully describe your design, or there's
a behavior in your design that is not caught by your assertions
this GapFree completeness check will flag it for you.
Good for High-Consequence Systems
GapFree is ideal for any high consequence system where you *must* have
a complete verification -- as opposed to wanting to only check certain
things. It takes a little bit more effort; let's say a couple days
more time, but we get a lot for the effort.
The runtime to check on your assertions in GapFree is quick -- only a
matter of minutes or so. The effort is preparing your assertions and
the completeness spec, feeding them to the tool, and then debugging
the result. That's where the time effort is.
If you need a complete verification, GapFree is probably the only tool
that can do a check like that and give you some guarantee that you
haven't missed anything.
I also like OneSpin's customer support. It is one of the reasons I've
used their tools for years.
---- ---- ---- ---- ---- ---- ----
We say the OneSpin GapFree tool should be a "Best of 2020" winner.
---- ---- ---- ---- ---- ---- ----
Our mgmt doesn't tolerate bugs getting through. The OneSpin Gap-Free
has changed how we verify our SoC's.
---- ---- ---- ---- ---- ---- ----
My verification guys really like the OneSpin GapFree app because
with it we know we have no holes in our verification.
---- ---- ---- ---- ---- ---- ----
Biggest lie?
What's the difference between OneSpin doing Gap-Free formal verification
and users just doing a full blown formal ABV proof run?
(I suspect it's a marketing game.)
---- ---- ---- ---- ---- ---- ----
It's not a new tool. It's probably 10 or 12 years old. But we like
using Gap-Free from One-Spin as a final sanity check of our overall
verification flow.
---- ---- ---- ---- ---- ---- ----
We use best in class.
Cadence Palladium, Excelium & VCS, JasperGold ABV, OneSpin GapFree
---- ---- ---- ---- ---- ---- ----
GapFree is perfectly tuned for our type of designs (processors).
---- ---- ---- ---- ---- ---- ----
OneSpin GF discovered a surprise functionality in our chip.
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
OneSpin Security app(s)
The OneSpin HW Metrics app
Our design isn't certified until management is happy with our LFM,
SPFM, and PMHF numbers.
---- ---- ---- ---- ---- ---- ----
OneSpin HMC, FDA, FPA, GapFree for us.
We're paranoid about Trojans in our chips.
---- ---- ---- ---- ---- ---- ----
We looked at the JasperGold security apps. We estimate that they're
between 6 to 8 EDA-years behind what the OneSpin guys have.
---- ---- ---- ---- ---- ---- ----
Raik's right about his Security apps.
---- ---- ---- ---- ---- ---- ----
OneSpin Trust apps kick ass when it comes to security checking,
but with one exception being the JasperGold Security Path app.
I'm surprised Raik left that glaring hole inside his otherwise
excellent formal toolset.
---- ---- ---- ---- ---- ---- ----
It's really obscure, but OneSpin's FCA app helped us partition our
SoC to be more security and fault aware.
---- ---- ---- ---- ---- ---- ----
We're an ISO 26262 house.
We jump between OneSpin FDA/FPA and HMC all the time.
---- ---- ---- ---- ---- ---- ----
I got into a big knock down, drag out fight with my boss on what's
a reasonable run time for the FPA app to run in "deep mode" for.
Thanks, OneSpin.
---- ---- ---- ---- ---- ---- ----
Biggest lie?
The OneSpin FPA app is fast and accurate. (Lie.) The truth is
it's fast because it skips over waaaaaay too many faults.
You MUST run FPA in "deep" mode to get accurate results.
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
OneSpin 360 EC-FPGA
OneSpin 360 EC-FPGA formally proves the logical equivalence of two
designs, in RTL and/or netlist form, for all stimulus. We use it as
part of our standard FPGA verification flow.
- The tool is remarkably valuable for evaluating the correctness
of our home-grown EDA tools -- where we are concerned with
validating circuit manipulations we perform on our designs to
ensure we don't have bugs that affect design function.
- It also lets us establish the trust our government customers
require for our 3rd-party synthesis, map, place, and route
tool outputs. We need to be able to assure our US government
customers that the tools did not purposefully, or accidentally,
modify the intent of our trusted designers (as described by our
source RTL).
In particular, we are interested in knowing if the netlists generated
by any of our tools is adding, removing, or modifying the intended
functions in a design.
Set Up
We can completely setup a new 360 EC-FPGA environment and import two
designs for comparison in only a few minutes. This is because a large
part or our setup is fully automated through Tcl scripting provided by
OneSpin.
We primarily use it with Verilog and SystemVerilog languages.
Performance/Capacity
We've used 360 EC-FPGA on telecommunications (e.g., routers, switches),
SoC designs, and 3rd party IP cores.
We use it to verify FPGA netlists with 10s of 1000s to 100s of 1000s of
components. If there are no mapping issues between the two designs, we
can often confirm equivalency in only minutes.
For more complex scenarios (such as comparing RTL to a gate-level
netlist or comparing two netlists with dramatically different
implementations) the process requires some human intervention. It can
take a few extra hours to days for us to work through the various
mapping issues and counterexamples if we are working at a netlist level.
The result is worth our time investment.
- If 360-EC proves equivalency, we are assured that the two
designs are logically identical for all possible stimulus.
- If the designs are not proven to be equivalent, the tool
provides counterexamples that assist us in isolating EDA bugs
or hardware Trojans.
I've used OneSpin 360 EC-FPGA on designs up to roughly 600K LUTs/flops.
If the I/O and black-box mappings are all sound, then it can prove
equivalence in less than an hour -- with some variability based upon the
similarity of the two designs being compared.
For example, two gate-level netlists produced from one RTL source set
by two separate runs through a synthesis tool will prove equivalent in
only minutes. The times go up as the gate-level implementations of the
two designs diverge or if you are comparing RTL to a synthesized
netlist.
Formal Equivalence Checks
Some examples of the formal equivalence checking OneSpin 360 EC-FPGA
covers are:
Incorrectly coded pipelines; Bus connecting ordering; Incorrect BRAM
parameter settings; Wrong FSM re-encoding; Issues with P&R connections;
Identification of added, unspecified logic, such as a bug or Trojan.
Formally Validating FPGA Synthesis Optimization
I've used 360 EC-FPGA to formally validate our FPGA synthesis
optimization gate representations, such as: Stuck-at registers, Register
duplication & merging, TMR optimizations, Asynchronous feedback loops
(you need to cut these loops to finish FEC), DSP & SRL optimizations,
RAM / ROM, including distributed & block RAMs, Fixed gated clocks (the
tool will flag them & prove they work as intended), and Pipelining.
It also validates your power optimizations. In theory, these don't
impacr "logic function". We use the tool to validate logical
equivalence; not that the power features do anything in the power
domain.
OneSpin also formally validates advanced synthesis optimizations like
complex sequential retiming. This is seamless and not much extra effort
is required to handle the scenarios.
As long as your primary inputs/outputs to and from the design are
mapped, EC-FPGA's formal equivalence checking goes fairly smoothly.
Occasionally, you will need to provide some guidance to the tool for RTL
to netlist mapping. For netlist-to-netlist comparisons, you can address
such issues by strategically black-boxing larger FPGA components (e.g.
DSPs, block memories, etc.).
Debug
EC-FPGA is a great tool for uncovering EDA synthesis, place, and route
tool bugs or scenarios where your RTL may not be getting interpreted in
the ways you might expect. We find bugs with it all the time.
OneSpin's debugger takes some getting used to -- it's a bit dated and
clunky. Part of this is getting used to looking at counterexamples and
wrapping your head around how those scenarios can occur.
Caveat: We are primarily looking at netlists without naming references.
It's less of a 360-EC issue, but does expose display issues with the
debugger.
Conclusion
OneSpin's EC-FPGA is invaluable for our EDA tool development.
For large modern FPGA designs, it is almost a necessity. It's just not
practical to apply a complex RTL simulation environment to a gate-level
netlist in many cases. Applying 360-EC FPGA to these cases can prove
that your source design behaves exactly as your implemented product.
It's also handy for cases where you might resynthesize a design to
improve power or timing performance -- and want to make sure those
improvements have not affected function.
---- ---- ---- ---- ---- ---- ----
The OneSpin EC-FPGA formal verification tool does RTL-to-netlist and
netlist-to-netlist equivalency checking for FPGA devices. We've used
it for three years now; it is part of our standard flow for our
development process -- simulation alone is not enough.
- For RTL code, EC-FPGA is complementary to simulation; we use
both methods.
- For netlists, we only use OneSpin EC-FPGA; it is more
targeted and easier to get the equivalencies than simulation.
Simulation is more painstaking and less automated; especially
when doing netlist transformations.
We make FPGAs and develop software to program them. EC-FPGA makes
sure our netlist changes are fully verified, and that the software
we develop to program the FPGAs produces the right results.
For example, we use it to verify that the bitstream we generate is
equivalent to the original user specification.
We used EC-FPGA for equivalence checking for:
- Bus connecting ordering
- Wrong FSM re-encoding
- Undriven or unconnected wires
- Clock gating for low power
- P&R connections
- Additional, unspecified logic (e.g. if trojans have been
added to our software)
Some post-synthesis optimization checks we use EC-FPGA for are:
- Retiming
- Stuck-at registers
- Register duplication & merging
- FSMs with safe & unknown encodings
- Triple modular redundancy optimization
- IO cells & different bus resolution schemes
- DSP48 optimizations
- Power optimizations
The biggest strength of OneSpin EC-FPGA is its speed and functionality.
We've run it on designs with 10s of thousands to 100s of thousands of
gates. The runtime varies with application -- it can be minutes for
a small block to a few hours for large designs.
I'd recommend it. We've had no issues with the tool, and OneSpin is
always responsive and their support is great.
---- ---- ---- ---- ---- ---- ----
OneSpin EC-FPGA checks functional equivalency between our HDL and
post-optimization/compilation gate-level Verilog. We have a fully
automated flow, so the tool has minimal setup.
We use it to:
- Verify the functional correctness of our FPGA compiles. We use it
with Verilog, VHDL, and System Verilog languages, including all
their versions.
- Complement gate-level simulation. WARNING: EC-FPGA does *not*
replace simulation because it is not robust enough to work with
all random designs. It is too slow to quickly test 1,000's of
random designs, and it is missing features/functions that
simulation can detect.
We've run both small and large designs through EC-FPGA ranging from
toy designs (few 100 Lookup tables and registers) to the largest
block/design with 1 million+ lookup tables and 1.5 million+ registers.
The longest that OneSpin EC-FPGA took was 7 days; where it just hung
with open states. We worked with OneSpin and were able to reduce the
runtime to 1.5 days (which is still a long time, but it worked).
OneSpin EC-FPGA lets us check for: incorrect FSM re-encoding; undriven/
unconnected wires; bus connection orderings; P&R connections; and
unspecified logic.
We also use it to verify post-FPGA synthesis optimization gate
representations such as: FSMs with safe -- and unknown encodings;
Asynchronous feedback loops; Stuck-at registers; DSP optimization;
Register duplication & merge; I/O cells & different bus resolution
schemes; Fixed gated clocks; SRL Optimizations, such as asynchronously
resettable register chains and RAM / ROM, including both distributed
and block RAM.
WARNING: it only supports *basic* retiming optimizations. It does NOT
natively/robustly support control signal demuxing during retiming,
NOR retiming while ignoring initial conditions, NOR retiming during
large multiplier decomposition. So, we use other means to formally
verify these aspects of retiming and cover the rest with simulation.
OneSpin's debugger is handy and useful to "root cause" a functional
failure -- especially their counter examples. But we still use other
netlist viewers and text editors for our more intense debugging.
Needs improvement: It still has bugs, which adds R&D time. It has
missing features such as debugging capability for complex sequential
optimization such as SRL to RAM and retiming. Finally, we do get
several false positives.
Despite that, we use OneSpin EC-FPGA regularly and highly recommend
it. Its biggest strength is its exhaustive proofs and ability to
"root cause" functional failures. This saves us a lot of time.
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
OneSpin X-Propagation app
The X state refers to an incorrect value, which is not 0 or 1. If there
is an X state in RTL, it will affect the normal function of RTL in
digital circuits; it would be hard to find the root cause in functional
testing.
The OneSpin X-Propagation app analyzes the "X" state of signals in RTL,
and checks whether the "X" state will be passed to an output port. If
there is a problem, the OneSpin app will show the location in the
source code and the value of the related signals.
I recommend the OneSpin X-Prop app. It's simple to use and practical.
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
OneSpin Protocol Compliance app
Our designs have a lot of IP blocks, all with AXI interfaces. We use
the OneSpin Protocol Compliance app to test inter-block communication.
- Inputs: RTL files with the interface of bus protocols
- Outputs: Results of protocol assertion checks
It's easy to use -- we just compile the related RTL files, choose the
type of bus protocol, run the app, and view the results. When we open
OneSpin's debug to analyze the failures, all the related signals are
automatically added to the waveform.
I recommend it.
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
OneSpin FPGA Retargeting app
We retargeted 22 designs from multiple obsolete Altera devices over to
two state-of-the-art FPGAs with it. (Sorry, I can't name which exact
FPGAs we went to.) This let us to take advantage of all the new safety,
security, and power benefits the new FPGAs offer -- and to reduce our
safety re-certification effort.
OneSpin's FPGA retargeting and equivalence checking apps let us
exhaustively prove the new FPGA implementations were functionally
equivalent to our older Altera devices. Their flow supports Xilinx
and Altera devices.
It takes around 4 hours to set it up unless there is an issue. The
app's inputs are the legacy netlist and cell libraries. The output
is the ported netlist. The OneSpin EC app then checks if the legacy
FPGA netlist is equivalent to the ported netlist. All of our designs
were relatively small and ran within minutes.
OneSpin's support was top-notch. They even did some last-minute ECOs
that we needed. They quickly answered our questions; and even gave
us additional library cells so we could meet our deadlines.
I would recommend this if you're simply porting an old FPGA design
from a part that is going obsolete over to a new one. I would *not*
recommend it if you plan to make design changes (unless you obtain
all the legacy libraries from OneSpin.)
---- ---- ---- ---- ---- ---- ----
Related Articles
OneSpin's "going where Cadence isn't" approach is Best of 2020 #4a
Users say Jasper's 200K register block signoff is Best of 2020 #4b
OneSpin extensible ABV plus formal linting is the Best of 2020 #4c
Join
Index
Next->Item
|
|
