how to aggregate tests and results

Hi Fred,

before I can think of alternatives I need to understand what you want to achieve. I understand that you wrote properties to check a bus protocol and use formal verification to exhaustively verify the interface. But what is the benefit of splitting and merging the verification? Don't you want to guarantee protocol compliance in all possible scenarioes?

Thanks,
Joerg.

Hi Joerg,


Thanks to help me, I really appreciate it.
Just for clarifyng:
My exact role is to verify and correct the contents of the PSL versus the spec and run them on an already verified IP. So I am not the developper of the PSL but I 'm acting as a reviewer.

So, I understand your questions.
"But what is the benefit of splitting and merging the verification? Don't you want to guarantee protocol compliance in all possible scenarioes?"

The thing is that we use those overcontrains to trigger some assertions that were not triggered without overconstaints. At the end, I want to merge or split all the results whether I am using particular overcontraint or not.

ex :
run without overconstraint
status : 3 properties no triggered
run with set of overcontrains
3 properties are triggered and passing but others are not triggered.

How to merge the results ?


Thanks for your help Joerg !

See you,

Fred

Hi Fred,

I still don't fully understand.

If a property does not trigger in one environment, then it will also not trigger if you add constraints (overconstraint). Only if you remove constraints there is a chance to trigger previously untriggered properties.

If you want to verify a set of protocol properties I recommend to systematically inject errors in the design and test if they are caught by the properties. Other methods include back to back testing. The IFV Advanced Training has a section dedicated to this type of property development and verification.

Regards,
Joerg.

Ok Joerg,

Thanks , it seems I need some IFV training. I will ask cadence for near future.

Best regards,

Fred