June 27, 2005
Kathryn Kranen- Jasper Design Automation
Please note that contributed articles, blog entries, and comments posted on EDACafe.com are the views and opinion of the author and do not necessarily represent the views and opinions of the management and staff of Internet Business Systems and its subsidiary web-sites.
| by Jack Horgan - Contributing Editor
Posted anew every four weeks or so, the EDA WEEKLY delivers to its readers information concerning the latest happenings in the EDA industry, covering vendors, products, finances and new developments. Frequently, feature articles on selected public or private EDA companies are presented. Brought to you by EDACafe.com. If we miss a story or subject that you feel deserves to be included, or you just want to suggest a future topic, please contact us! Questions? Feedback? Click here. Thank you!
What is the difference between high level requirements and low level assertions? If one uses your tool does it ensure that the system handles conditions like FIFO overflow?
Those would be called implementation specific assertions. Yes, our tool very handily proofs them very quickly. We are focused squarely on user defined assertions. There are lint kind of tools that are focused on the automatic extraction of properties. Those are handy and useful. But you can't make a company out of just that capability. We are not there. We are focused on making sure that your design meets its spec. Back to the FIFO question, if you have a one hot state machine or FIFO overflow all of these assertions would be low level. A high level requirement would be independent of the implementation. My favorite example of HLR is data integrity. If you are doing a router or
switch or anything that transports data (just about everything transports data) you could prove one high level requirement called data integrity that says I'm, going to look at the data going in all the way to the data going out. Actually formal looks at in reverse in case you're interested. It says is there any way that a bit or packet of data gets lost or duplicated or corrupted. If there is any way whatsoever that any of these things could happen is detected. If you have a retry buffer in your switch, if the package is getting acknowledged, is going to send it again. Maybe something goes haywire in the retry buffer in your control logic and you end up sending the packet twice.
That would be a duplicate packet.
.. There are so many things that could go wrong. Yet if the symptom at the other end was that anything at all went wrong with the data, it would be found. One single elegant HLR, data integrity. Imagine the confidence you have when it turns out that there is nothing in the world that can cause the data to not move through it correctly. With that assurance your job is almost all done. You get such high leverage and high coverage with HLR.
If the product reports that you didn't have data integrity, to what extent does it help you pinpoint the cause?
I'm glad you asked. It comes back and helps you down to the line of RTL code. It tells you exactly what's wrong. You have some typo or subexpression. It will highlight it right there on the screen. The system will come back and show you a counter example. It shows that I was able to come up with a scenario that dropped a packet. This is the neat thing about formal, if you bring formal high level requirements instead of some of the itty bitty stuff that's going on in formal. If you are able to get formal up to this level, this is what's so good about it. With simulation you would have to dream up every scenario that could break the design. You think this would cause a problem.
Well that didn't. Let's see if this will. That didn't. And so forth. With formal there are no scenarios. You simply tell it the rule that no data should be dropped or corrupted. From there it is the tool's challenge to come up with a scenario to break it. It comes back with this set of inputs and this set of events that were able to create this situation where that packet got corrupted or dropped or something. It shows you the waveform and then you click on the waveform and ask “Why is this signal that value?”. The source code browser is open in the same window and highlights that line of code. You can click either on the code, the subexpression in the code or the
waveform. Why it did that. It takes you back layers and layers and suddenly it gets to that root cause. This all happens within seconds; very, very quickly. In a few minutes the designer is down to the single line of code that is broken. This is something you do not get with simulation. With simulation you are simulating something that is a black box. You see at the very end the packet didn't come out correctly but you are not aware of the line of code where it is broken unless you had specifically, physically invoked an assertion that triggered and gave an observation. In the case of formal you don't need those assertions. We actually operate on assertions. That's a natural
stepping stone for users who already have them in their designs. With HLR the tool automatically isolates the line of code that is broken without any assertion being present inside the code.
I see that you introduced JasperGold Express, a push-button version of JasperGold for ABV in May. How much of a missionary sale are you still involved with convincing people to express their designs in HLRs? To what extent would customers have to modify their design flow in order to exploit your capabilities?
They do have to modify their design flows and that's what makes this missionary. I wouldn't be any other place. The great value is and the great fun for me. Our customers as seen on our website publicly and officially like NVIDIA, Sony and SUN were early ones before the Jasper Express product. So they are the ones who adopted HLR and embraced them and are fully proving their blocks, are using the tool to fully prove their blocks are free of bugs before they check them into RTL freeze. With the Jasper Express that allows us to go down market a little bit, to go after customers who are already comfortable with assertions because they are simulating and they want to have a way to find
bugs faster before they start simulating. You don't have to wait around until you have simulation running to just operate static formal verification on these assertions. What we believe is that this will give people confidence in formal verification technology. They will become comfortable; they got instant gratification, found bugs without having to lift a hand because the operations on these assertions are already there. From that will be our customers and will either want one or two things of those assertions that would not prove statically with a push button because they required too much of the design to be realized, They will either care about those assertions and want to
complete them. For that they can use the big brother tool JasperGold, use design tunneling techniques to complete those assertions which is what our original tools did.
That's the breakthrough. It is not a feature it is an architecture. I joined this company because of its ability to scale proof to 100%, unbounded proof. They will be able to take the assertions that didn't run but they cared about and go ahead and scale with Jasper Gold which is the full heavy duty product or then because they are learning methodology from us ands see that they get comfortable with over time they would rather just quit simulating the blocks and fully prove them formally. They will move to HLR with confidence because they have already used the low level assertions.
Whom do you see as competition?
What we see right now is that the formal market is kind of segmented into three buckets. The automatically extracted properties that we spoke of earlier. There are companies that have this as their specialty. Maybe they don't do only that but that is what people buy them for. This is great but we are not focused on that. In fact many of the big companies have packaged those capabilities with equivalence because it is not about the specification but it is about some implementation detail being lost. Then there is the middle which Jasper Express is aimed at. There's a push-button proof when you can and unbounded partial proofs when you can't and rely on simulation for the rest. That's
where a large portion of the formal market rests. We believe that we are the only ones offering the capability among all of our competitors. We are certain that only we offer 100% actual coverage. We are the only ones that give you a tool to get to 100% on your block. The main competition that we see is the middle band. Synopsys whose Dynamic Formal with Magellan still has a heavy reliance on simulation. Cadence came out with the new Incisive tool. They have been on the market a long, long time. We've benchmarked them with them and we seem to out perform them in the cases we have received the results
of. We used to see 0-In a bit but their Checkware is the big popular product there. Most people are not using their static formal capabilities at least that we know off. It seems that the big three are the competition. The customer will either want to go for the paradigm shift of full formal verification or want to sit back and do a little better than they can with simulation and go ahead with a little bit of formal to enhance their simulation dominant methodology. Ours is a vision of flow change meaning if you want much higher productivity at the designer level and have
clean blocks being verified in half the time and being checked before physical situation. If you didn't have the vision you would probably take one of the big three tools that doesn't do as much but you can mix it in with your license mix at very low cost or free. But we are gong with customers that have a vision of really competing based on their verification ability.
You can find the full EDACafe event calendar here
To read more news, click here
-- Jack Horgan, EDACafe.com Contributing Editor.
Be the first to review this article