Feed on
Posts
Comments

OneSpin formal verification

I had my first brush with formal methods about 11 years ago when I started my PhD. I was asked to look at the Z language, which would let you write a specification that could be formally proven to be correct. The downside was that, at any given time, there would only be three people on the planet with large enough brains to use it. Part of the complexity of Z was down to the fact that English characters were not allowed (that would have been too easy) - only Greek symbols by the looks of things. I’m not sure how you were meant to type it into a text editor, and I didn’t pursue it far enough to find out.

I had high hopes when I heard about SVA. I thought that an industry backed attempt at specifying a formal language would be usable. However, casually browsing through some real assertions written in SVA leaves me a bit disappointed. Simple? Yeah - right! If any of the Enigma code breakers from Bletchley park are still with us, I think SVA could earn them a nice retirement income.

Please don’t get me wrong. In the right hands, SVA will be excellent. However, I think that it holds sufficient traps and gotchas for the casual user (such as designers who seem to be permanently context switching between SV for design, DesignCompiler, PrimeTime, DFT, DFM, DFV, unit level testbenches, yadda yadda), that we’ll see a lot of mistakes, error escapes and wasted time. I spoke to a couple of people whose teams were using SVA and they admitted that they were only using it for very simple assertions. That’s still good, but perhaps a simpler input language would allow more people access to the inherent power of formal?

That’s why I was happy to speak to the guys from OneSpin today. At last - a simple way to write formal properties. Their ITL language lets you specify a property in stages, and in either a VHDL or Verilog like syntax. They look something like this (and apologies if I get the syntax a bit wrong - I was frantically taking notes. This is broadly right though):


property Foo is
assume:
  at t: state = IDLE;
prove
  at t+1: if (bar = '1') then
             state = BAR;
          else
             state = IDLE;
          end if;

  during [t, t+2] : my_output = '0';
end property;

Now that’s easy to use! Oh, and if I remember correctly, their tool will dump these as Verilog or VHDL checkers so that you can use them in simulations.

OneSpin were here at DAC demoing their “new” 360MV formal verification tool. I put “new” in quotes, because these guys have been doing this for absolutely ages first as part of Siemens, and then as part of Infineon. So while the company is new, the technology is old. I have some (non OneSpin) friends who have been using this on projects for years and they only have good things to say about it.

It’s not all sunshine and roses for OneSpin though. I spoke to three people who had already had the demo, but they had come away with some strange conceptions about what it was all about. From what I have seen and the real user feedback I’ve had, I think OneSpin have an easy to use tool here that could prove to be very popular. I also think that their marketing department has a lot more work to do explaining what they actually have.

David

Comments are closed.

Work For Verilab