( ESNUG 558 Item 6 ) ---------------------------------------------- [02/25/16]

Subject: OneSpin CEO cites 8 "insufficiencies" in Jim Hogan's Formal Guide

  EDITOR'S NOTE I: What is this with German engineers?  Whenever it comes
  to tech talk they have absolutely no sense of fear whatsoever.  - John

 EDITOR'S NOTE II: I love it when Jim's own guys take him to school! - 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.

     - from http://www.deepchip.com/items/0558-01.html

From: [ Raik Brinkmann of OneSpin ]

Hi, John,

I'm taking a risk here.  Although Jim Hogan is on my Board of Directors,
I must correct these 8 shortfalls which Jim had in his formal user's guide.

For the record, these are not errors, but insufficiencies where Jim should
have said more if he's explaining formal tools to beginners.

    - Raik Brinkmann
      OneSpin Solutions GmbH                     Munich, Germany

         ----    ----    ----    ----    ----    ----    ----

1. FORMAL DRIVERS - JIM MISSED A BIG ONE

     - from http://www.deepchip.com/items/0558-01.html

Jim missed the most important, 7th driver behind increased formal use.  It's
two parts really.

The first part is, if used alongside simulation, Formal improves both your
overall verification quality *and* speeds your verification schedule.

OK, I know we've all heard this for a long time so you might ask: "if this
is such a big driver then why are we only seeing formal now?".  It's because
Formal was always seen as hard to use and was therefore relegated to complex
bug hunting late in the verification process.  This is changing now as the
formal tools mature, become easier to use, and engineers realize what they
can do with it. 

As verification gets harder and the tools get easier, a tipping point will
be reached, and it looks like we have hit it!

The Mentor Wilson Research Group 2014 verification study shows that property
checking is now used on 26% of projects (along with with RTL simulation),
while formal apps usage grew 80% over 2 years. 

Check papers at DVCon, DAC, etc. -- formal teams (not just individuals) are
thriving in companies all over the world. 

    "We believe that in the next ten years formal will become the default
     verification strategy in the verification flow, routinely used to
     sign-off at the unit level."

         - Oski Decoding Formal Group 2015, with Apple, ARM, Broadcom,
           Ericsson, Google, Imagination, Microsoft, Nvidia

Just Google the terms:

    "Formal Verification Engineer" plus any of these above companies

and you'll find that they're all actively hiring today, now, to fill a sea
of Formal verification jobs.

And now that second part...

THAT OTHER BIG NEW FORMAL DRIVER WHICH JIM MISSED

So what's the real driver here?  A shift is taking place where Formal is
being placed at the beginning of the verification process -- and it is
taking on more of the core verification task -- as Ram Narayan of Oracle
Labs puts it doing "design assurance testing".   There are actually three
basic drivers (which Jim did describe):

    1. The use of Formal Apps.  Not just to avoid writing assertions,
       but because these apps show just how effective the tools are,
       spurring engineering interest to do more.

    2. Assertions are becoming understood.  Engineers write them more
       easily, but also have figured out how to use them effectively.

    3. Formal tools are more mature.  Like other EDA tools that use
       multiple algorithms, it takes experience on real chip designs
       to make them work, and this takes time.

Again, the engineering sea change that Jim failed to mention is that instead
of being a bug hunter near the end of the project, with all the new advances
Formal has now moved up to the start of the verification task.  That's big.

         ----    ----    ----    ----    ----    ----    ----

2. JIM MISSED THAT ASSERTION SYNTHESIS HAS PROBLEMS

     - from http://www.deepchip.com/items/0558-02.html

Jim should have dug deeper into which of these assertion-authoring methods
actually work for real designs.

Yes, formal tools can synthesize structural, safety, and activation checks
based on your design source code.  That much works.

However, doing "behavioral property synthesis" or some such jargon, while
appearing attractive, completely falls down in real life.  Here's why:

  - It can only be applied late in the process, when you have sim data
  - It has a limited or no relationship to the original specification
    and is too tied to the final design to provide a good test
  - It usually generates massive amounts of properties that takes time
    to wade through manually to find useful ones
  - An incorrect design or sim trace result in an incorrect assertion

This "assertion synthesis" has some merits for very specific cases, but in
no way lives up to the hype.

BUT USING A HIGHER-LEVEL APPROACH WORKS

Jim should have focused more on UVM abstract assertion entry, and let the
engineers focus on the higher-level intent without the lower-level detail.
This way the original spec can be used to drive the tests, which are much
easier to write.

  "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."

       - from http://www.deepchip.com/items/0558-02.html

Our Operational Assertions use a timing diagram style description which
engineers are familiar with, and is based on a non-proprietary standard
System Verilog library -- but with a simpler/smaller syntax than full SVA.

        property my_prop
           state == busy && transfer == 1
        implies
           ## 1 (read_access_o && !write_access_o) [*2];
           ## 1 (!read_access_o && write_access_o) [*2];
        endproperty

You can code up the transactions you need based on your spec, and let the
library do the work.  It's independent of your design, so it can be started
early in the process.  The general idea is similar to UVM sequences, in that
you can think about your tests without worrying about the UVC detail.

As I said earlier, Formal has changed.  It is moving to the beginning of the
verification process.  This is a perfect example of that change.

         ----    ----    ----    ----    ----    ----    ----

3. JIM MISSED THE DESIGN-TO-VERIFICATION RELATIONSHIP

     - from http://www.deepchip.com/items/0558-02.html

That underlined testbench generation part above is huge.  It's good that Jim
noted it, but it deserves a big section on its own.

Chip designers are under a lot of pressure to do more verification prior to
code hand-off to synthesis and PnR, and need a tool that requires much less
stimulus coding than simulation.  They are just starting to realize that
formal can help.  But some tools (like ours) can go a lot further.

For designers, formal now can (for example):

  - Show a likely sequence of outputs with minimal or no input
  - Weed out coding mistakes that will (not might) cause a bug
  - Check the design works the same after optimizations
  - Test for reset issues, protocol faults, data transport
    issues, connection and register errors, etc, etc.

All this can now be done in formal without a human needing to write a single
assertion nor any simulation stimulus.  Formal fits perfectly into the AGILE
design manifesto. 

EVERYBODY LOVES GENERATED TESTBENCHES

So this is all good, but what about this testbench generation stuff?  Well
some tools can generate a trace, known as a "witness", of design operation
that looks like a waveform display.  OneSpin's tool can write the witness
out into a testbench that can be used with a simulator.  This allows the
traces to be reused in downstream verification, as well as to document the
intent of the design test.

Here's a typical code hand-off conversation:

           Chip Designer: "Hey here is the latest code for the
                           SuperFragalistic Controller."

   Verification Engineer: "Did you check it works this time?"

           Chip Designer: "Oh sure I ran a few interactive sims
                           and it looked OK."

   Verification Engineer: "You know that last bug cost me a weekend."

           Chip Designer: "Yea well sorry.  Hey did you watch the
                           Super Bowl over that weekend?"

Now with less work for everybody, the chip designer could say:

  "Hey I ran that whizbang new formal thingy.  It showed me my whole
   SuperFragalistic Controller operating, as well as checking its code.
   Here's the tests that you can include in your sign-off testbench.
   I'll buy the beer and we can both watch the Super Bowl this weekend."

Or it can work the other way around as well:

   Verification Engineer: "Hey I found a bug in your code.
                           Can you track it down?"

           Chip Designer: "OK, where is the problem?"

   Verification Engineer: "Don't know.  I got this check failing,
                           but I don't know why."

           Chip Designer: "That could be anything.  I'll have to
                           spend the weekend figuring it out."

   Verification Engineer: "Have fun.  I'll be watching the Super Bowl."

Now with less work for everybody, the verification engineer could say:

  "Hey, I had an assertion fail.  The formal tool traced down a counter-
   example waveform and identified the problem back in your code.  It
   generated a testbench so you can run it and see exactly where you
   #^@#*$ up!  Should be fixed in time for our Superbowl party though."

These are engineering conversations that go on every day.  Solving these
bi-directional handoff problems is a key upside of using formal.

         ----    ----    ----    ----    ----    ----    ----

4. JIM GOT FORMAL ENGINE SELECTION WRONG

     - from http://www.deepchip.com/items/0558-03.html

Jim was inaccurate on heuristic-based engine selection.  It's not "still in
development" (at least at OneSpin.  We've had it for years, and it's really
important!)

If you buy a BMW, you know what's under the hood even though you may never
open it.  In modern formal there are powerful engines at work as well.  The
majority of engineers don't need (or want) to open that hood, but in formal
(like with cars) there are a few enthusiasts who want to explore.

Whether enthusiast or regular driver, you do need to know the horsepower is
available when you need it, so maybe open the hood once before buying!

Using the right formal algorithm is crucial.  Your formal tool selects the
best engine/algorithm for each assertion -- based on your design code.
Getting these algorithms and the selection mechanism right can only be done
by running many 100s of designs.  As such, formal tool optimization is based
on experience (as well as some very smart tool developers).

SNPS AND MENT PLAYING CATCH UP

In the old days, formal engines were selected by hand.  Automating this now
is an important aspect of making formal easy.

We developed and have kept developing experienced-based heuristic formal
engine selection continiously for years.  Jim failed to warn that Synopsys
(who is just now restarting their formal development) and Mentor (who
limited their investment to old 0-In technology) will have trouble because
of their weak formal engine selection abilities.

Simply put, a mature formal tool with lots of continious development-years
under its belt will:

  - use the right formal algorithms to operate faster and leaner
  - quickly converge on a result rather than flying off into cyber-limbo
  - provide deeper formal proofs over more clock cycles

And do this automatically so you don't have to go messing under the hood.

         ----    ----    ----    ----    ----    ----    ----

5. JIM MISSED THE CONE-OF-INFLUENCE COVERAGE PROBLEMS

     - from http://www.deepchip.com/items/0558-03.html

Two basic approaches to coverage are being worked on today:

  - Cone of Influence (COI), ala Cadence Proof Core
  - Mutation Analysis, ala OneSpin Observation Coverage 

The COI approach has problems.  Let's look at a trivial example:

Assume a shift register:
                         s[2] <= s[1];
                         s[1] <= s[0];
                         s[0] <= input;

is tested with the assertion:

                         s[1] |=> s[2];

(i.e. assert that s[2] takes the value of s[1] on the next clock cycle).

With COI coverage, all statements would be in the "influence cone" of the
assertion (i.e. the logic that drives, or influences, s[2]) and therefore
is assumed to be covered.

However:
                         s[2] <= s[1];

is actually the only thing being verified by this assertion.

Observation Coverage shows this by swapping s[1] for a free variable (a new
variable inserted by the coverage tool):

                      s[2] <= free_variable;

by making this substitution, the assertion would fail as S[2] will not now
take the state of s[1].  The coverage tool knows that the assertion covers
this statement, so the statement is therefore marked as covered.

Now if the coverage tool then swaps s[0] for a free variable with:

                      s[1] <= free_variable;

the original assertion will hold, i.e. this substitution will not trigger
the assertion to fail because s[2] will still take the value of s[1].
Therefore, in observation coverage (but not COI) this line will be marked
as NOT covered, which of course is quite correct.

So this tells the engineer what's really covered by the formal property set.

Cadence Proof Core coverage is improved CIO coverage, but it still fails to
show if a coverage location is really observed by the assertion.

         ----    ----    ----    ----    ----    ----    ----

6. JIM MISSED THE PAINFUL C/C++/SYSTEMC ISSUES

     - from http://www.deepchip.com/items/0558-04.html

Jim touches here and there on using formal for High Level Synthesis (HLS),
but it should have had its own section.  HLS is a silent trend, driven by
increased data processing needs.

HLS has found a hot niche -- algorithm coding without cycle-level timing.

It's a lot easier to get the untimed algorithm right first, and then add
the timing later using HLS.

However, verification around an HLS flow is a mess!  Why?  SystemC.

Today SystemC verification with class library simulation sucks because:

    - Lack of effective SystemC debug
    - Cryptic SystemC error messages
    - Dog slow performance of timed SystemC functions
    - SystemC does not have an "unknown" or "X" state
    - SystemC has write-write races between its threads

So engineers have to verify post-synthesized timed RTL code.  This kills the
benefit of HLS -- and makes debugging the original SystemC code difficult.
So you want to verify as much as possible at the untimed C++/SystemC level.

Jim also missed that the safety checks used for RTL are even more effective
here.  With formal at the SystemC level you can identify unknown state
propagation, trap possible races, and perform other useful checks which seem
to crop up more at this level (array out of bounds, divide by zero, etc.)
People used to working with SystemC get this immediately!

Algorithm designers used to C++ need help when converting from SW thinking
(e.g. integers of any size) to HW thinking (e.g. fixed bit-width number
systems).  It's for these guys that the formal arithmetic app is so useful.

This isn't just a formal arithmetic check.  It's a verification bridge both
for the algorithm C++ and the hardware RTL folks working at this level. 

         ----    ----    ----    ----    ----    ----    ----

7. JIM MISSED SAFETY FAULT PROPAGATION

     - from http://www.deepchip.com/items/0558-04.html

However, there is more.  The propagation of all safety faults in your design
must be understood.  This requires even more fault analysis and is a huge
burden on your fault simulation methods.  Here's a conceptual map of how all
"fail-safe" designs must work:

If at any moment your chip suddenly fails, it must automatically jump to its
"safety function" to correct the chip's functioning -- or instead have the
fault swallowed up in your chip's logic.

When using a fault simulator, every fault that is inserted must have a test
that activates and propagates it.  So, after your entire chip is simulated,
if there are a number of faults that were inserted but did not make it to
the "safety function", then you must understand why.  Did they get swallowed
by the design logic or were there simply simulation vectors missing?

The ISO 26262 standard requires you to specify if any fault in your chip is
harmless (safe) -- or not.  Proving this with fault simulation is difficult
and takes a lot of effort.  Anyone familiar with using fault simulation for
manufacturing test analysis will know this issue. 

In addition to it's other functions, the safety app reports all faults that
cannot propagate elsewhere in your chip (and are therefore "safe").  This
saves days of debug and simulation time.

         ----    ----    ----    ----    ----    ----    ----

8. JIM GLOSSED OVER VERIFICATION IP (VIP) & PROTOCOL COMPLIANCE

     - from http://www.deepchip.com/items/0558-04.html

Jim neglected to mention that there are two types of VIP:

    - formal VIP which uses formal to verify
    - simulation VIP which uses simulation vectors to verify

The smart verification teams use both.

Formal VIP is good at checking for the correct implementation of control
and data transport logic in your chip.  It's useful for a lot of common
communication standard VIP blocks.  It is important that any VIP block
you use is written using standard System Verilog Assertions -- so your
project does not get tied down to individual tools for future revisions.

VIP blocks available from SNPS/CDNS/MENT and claim to work with formal:

    AMBA, PCI Express, USB, MIPI, DDR, DFI, LPDDR, HDMI, Ethernet,
    OCP, SATA/SAS, SDRAM, Fibre Channel.

At OneSpin we offer the same Formal VIP.

Verification consultants are also a great source of formal VIP.  We work
with our Spinnaker consulting partners who have created a range of VIP
blocks, for example, Boost Valley, CVC, MethodsToBusiness, and TVS.  

         ----    ----    ----    ----    ----    ----    ----

9. BUT JIM NAILED THE FORMAL APP DEVELOPMENT MARKET

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.

     - from http://www.deepchip.com/items/0558-04.html

This part that Jim wrote about we really liked at OneSpin.

This is the idea behind our LaunchPad platform that allows domain experts
build an app for their markets without their own formal technology.  As the
platform only works with their tool, they can price the app for their
market.  Plus they can load the app in an iTunes style library for companies
who do own the formal tools already (like an iPhone).

An obvious example domain-expert app is in the area of security.  There are
companies with experts that live and breathe security issues.  Here it makes
more sense to work with them.  So we partnered with Tortuga Logic, a group
of expert security PhDs, so they can sell a killer HW security app at the
right price point for their own market.

So our LaunchPad is more than a tool.  It opens entire markets for tool,
IP providers, and even internal customer groups -- to build and market
formal apps with none of the technical and business entry barriers.

Well spotted, Jim!

    - Raik Brinkmann
      OneSpin Solutions GmbH                     Munich, Germany

         ----    ----    ----    ----    ----    ----    ----

Related Articles

    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
    Jasper case study on formally verifying secure on-chip datapaths

   !!!     "It's not a BUG,
  /o o\  /  it's a FEATURE!"
 (  >  )
  \ - / 
  _] [_     (jcooley 1991)