Stats

  • Locked Locked
  • Replies 5
  • Subscribers 65
  • Views 14772
  • Members are here 0
This discussion has been locked.
You can no longer post new replies to this discussion. If you have a question you can start a new discussion

SAT engine

davexpc

Hi there!

I am exploring the possibility to include formal verification in our design flow.  I've been told by one of our engineers that the SAT instances for our designs would take ages to process. We can't afford to buy some kind of supercomputer for this but would be willing ot explore the possibility to outsource the processing to Cadence or other EDA vendor instead of solving the instances locally. Do you know of any vendor who on top of the SW offer some sort of SAT engine service?

Thanks

 

 

Parents

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

Reply

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

Children
No Data

Community Guidelines

The Cadence Design Communities support Cadence users and technologists interacting to exchange ideas, news, technical information, and best practices to solve problems and get the most from Cadence technology. The community is open to everyone, and to provide the most value, we require participants to follow our Community Guidelines that facilitate a quality exchange of ideas and information. By accessing, contributing, using or downloading any materials from the site, you agree to be bound by the full Community Guidelines.