Formal Verification at ARM

Formal Verification at ARM
by Paul McLellan on 12-20-2012 at 4:34 pm

There are two primary microprocessor companies in the world these days: Intel and ARM. Of course there are many others but Intel is dominant on the PC desktop (including Macs) and ARM is dominant in mobile (including tablets).

One of the keynotes at last month’s Jasper User Group (JUG, not the greatest of acronyms) was by Bob… Read More


Formal Analysis of Security Data Paths

Formal Analysis of Security Data Paths
by Paul McLellan on 12-05-2012 at 5:07 pm

One challenge with security in systems is to ensure that there are not backdoors, either accidentally or maliciously inserted. Intel, ARM and others have various forms of trusted execution technology. Under the hood these are implemented by dividing the design into two parts, normal and secure, and implementing them with physical… Read More


Jasper User Group Keynotes

Jasper User Group Keynotes
by Paul McLellan on 11-13-2012 at 1:31 pm

I attended the Jasper User Group this week, at least the keynotes, the first by Kathryn Kranen the CEO of Jasper and the second by Bob Bentley of Intel.

Kathryn went over some history, going back to when the company was started (under the name Tempus Fugit) back in August 2002 with a single product for protocol verification. Now, since… Read More


Jasper Apps White Paper

Jasper Apps White Paper
by Paul McLellan on 11-01-2012 at 7:30 pm

Just in time for the Jasper User Group meeting, Jasper have a new white paper explaining the concept of JasperGold Apps.

First the User Group Meeting. It is in Cupertino at the Cypress Hotel November 12-13th. For more details and to register, go here. The meeting is free for qualified attendees (aka users). One thing I noticed at the… Read More


Jasper Property Synthesis Apps

Jasper Property Synthesis Apps
by Paul McLellan on 10-29-2012 at 7:00 am

Jasper restructured JasperGold so that it could deliver its formal technology more flexibly by having a base system and a porfolio of apps. This would also make it easier to upgrade capabilities by creating new apps. Today, Jasper announced two new apps:

  • JasperGold Structural Property Synthesis (SPS)
  • JasperGold Behavioral
Read More

Brian Bailey Interviews Kathryn Kranen

Brian Bailey Interviews Kathryn Kranen
by Paul McLellan on 10-25-2012 at 6:23 pm

Brian Bailey at EETimes has an interesting interview with Kathryn Kranen. He says that the interview will be published in installments but the first one is up here. This first installment is mostly about how long-lived EDA companies (and others) have become since it takes a long time to build up enough revenue to be able to IPO.

She… Read More


Jasper User Group

Jasper User Group
by Paul McLellan on 09-25-2012 at 1:19 pm

The Jasper User Group meeting has been announced. It will take place on November 12th and 13th. As last year, it will be at the Cypress Hotel at 10050 De Anza Boulevard in Cupertino. The user group meeting is free for qualified Jasper customers.

Topics to be covered are, of course, all things verification:

  • SoC subsystems verification
Read More

Jasper Customer Videos

Jasper Customer Videos
by Paul McLellan on 07-25-2012 at 2:28 pm

Increasingly at DAC and other shows, EDA companies such as Jasper are having their customers present their experiences with the products. Everyone has seen marketing people present wonderful visions of the future that turn out not to materialize. But a customer speaking about their own experiences has a credibility that an EDA… Read More


Formal Going Mainstream

Formal Going Mainstream
by Paul McLellan on 07-10-2012 at 7:29 pm

In Mike Muller’s keynote at DAC he wanted to make formal approaches an integral part of writing RTL. After all, formal captures design intent and then, at least much of the time, can verify whether the RTL written actually matches that intent. Today, formal is not used that way and is typically something served “on the side” by specialist… Read More


Finding RTL Bugs Live Using Formal Techniques

Finding RTL Bugs Live Using Formal Techniques
by Daniel Payne on 06-24-2012 at 8:10 pm

Most of what you see at DAC is canned PowerPoint presentations, however on Tuesday afternoon I spotted a company called Oski Technology that was doing something almost unheard of – they had an engineer debugging a digital design from Nvidia using formal tools live. I later found out the engineer found 4 bugs in just three days… Read More