Community Functional Verification incorrect output of multiplication in jaspergold

Stats

  • Locked Locked
  • Replies 2
  • Subscribers 65
  • Views 4733
  • 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

incorrect output of multiplication in jaspergold

Anubhav8136

I want to use jaspergold to formally verify functionality of my custom multiplier. I am computing the expected result using A*B to check against output of my multiplier. Here, A and B are two logic signed operands. However, jaspergold is performing the operation A*B incorrectly.

I have reproduced this issue using the attached example. JasperGold compiles and elaborates the module and subsequently runs a formal proof. The tool raises a counterexample to assertion whose screenshot is attached below:

I simulated the same example using xrun and it was giving the correct product output in simvision waveform. Please help me resolve this issue. I am using 2023.03 version of Jasper Apps.

Thanks and regards

Anubhav Agarwal

  • Hi Anubhav. We cannot provide proper tool support in this forum, please could you login to support.cadence.com and file a service request along with a testcase that can reproduce the issue. The support team can then work with you to understand whether the behaviour you're seeing is expected or not, and work with R&D to get a fix if the behaviour of the tool isn't correct. 

  • Anubhav-- A common issue that may cause your observation is the fact that Jasper elaboration automatically blackboxes multipliers (ignoring all their internal logic)-- this is because multiplication is often very difficult to verify in model checking tools, and usually the user is trying to verify the control logic around the multiplier rather than the multiplication op itself.   

    For some small examples you might be OK though.   To prevent your multiply from being blackboxed, you can elaborate with the added option "-bbox_mul <N>" to force the tool to only blackbox multipliers above size <N>.

    (For full verification of datapath operations, it's usually better to use Jasper C2RTL.  See https://www.cadence.com/en_US/home/tools/system-design-and-verification/formal-and-static-verification/jasper-c-formal-verification.html for more info.)

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.