SAT engine

Can you clarify what you mean by "SAT instances"?  In general, formal analysis works very well to verify control logic on small blocks.  Small blocks are relative as recent gains in capacity and performance has allowed larger designs to be consumed and achieve conclusive proofs on the logic.  The limiting factor is the size and complexity fo the logic relative to an assertion.

The major benefit of formal analysis is the ability to flush out nasty corner case bugs early in the design cycle.  All this without the need for a testbench or need to create stimulus.  The formal tool throws everything at it with the bounds of the constraints you supply to the tool.

 This said, it may be worth trying it out on your design types by requesting an application engineer come by to discuss your specific needs.

Hi,

Thanks for your reply!  As far as I know, when you want to verify a design, the assertions and design are converted into a SAT instance (CNF format) and solved by a SAT solver.

As you mentioned, for small blocks such as the control logic of a memory chip, it can take just some seconds to verify, but I know that for other applications you have to set boundaries to specify the proof radius or depth of the cycles so that the verification doesn't take for ever. I also heard that some companies outsource this, meaning that they use a SAT engine with higher processing power to terminate more instances and therefore increase your radius, but I don't know who or how I can research about this service.

Thanks again!

Hi 

SAT is only one type of engine available in IFV. There are many more available and they can be run in parralllel in order to prove assertions.  That said, you do not worry about guessing at proof depths, you just give it an upper time bound to work on each assertion and let the tool worry about the details.  It is not as complicated to setup and run as you have indicated.  In fact, it is very easy to get up and running.  I use it all the time.

I would encourage you to look at doing it yourself.  I have done dynamic simulations for over 15 years now and setting up to run formal, on the good candidate designs, is much easier than constructing dynamic simulation environments.  This said, it is all a function of how difficult it is constrain your inputs.  The more complex the contraints, the longer it will take to get it right, but this is the same for dynamic environments as well.]

Have a great day!!

I should have mentioned this in my previous post.  If you are interested in some service contact your local Cadence AE.  But I think you will be pleasantly surprised to see how easy it is to run yourself.  I run my analysis on existing machines that run simulations and I get very good response times.

Thanks again for the info.

Maybe I should have referred to it as a formal verification engine rather than SAT engine. I was aware about the fact that normally there are several solvers (SAT and BDD) running in parallel. Let me please give you a little bit of background about the info that I want to get.

I am not engineer so I am not familiar with the technical side of verification, SAT algorithms, ... I was told by the head of my division to consider the alternatives of outsourcing verification vs doing it in house. One of our engineers mentioned that given the nature of our designs, assertion checking would take a lot of time and 100% verification would be impossible unless we had some kind of supercomputer. Do you think this can be true?

I was told as well that Cadence has a service to process these instances. I guess that companies send their instances through Internet, but I cannot find it in the website, so I cannot see how I can compare the two alternatives.

Thanks again for your help.

davexpc