Mark Eslinger - Mentor, A Siemens Business
Jin Hou - Mentor, A Siemens Business
This time yesterday you kicked off a formal analysis – and it is still running!
You are starting to receive aggressive messages from your grid monitoring software and/or the on-call IT Manager, threatening to pull the plug if you don’t explicitly order the job to continue.
On one hand, it would be a shame to waste 24 hours-worth of compute resources by arbitrarily killing the job, especially since the analysis could still be making progress. After all, the DUT and the formal testbench are rather large. But then again, maybe the job has passed the point of diminishing returns and it should be terminated now for the benefit of all concerned?
In this workshop we will show the steps you can take to make an informed decision to forge ahead, or cut your losses and regroup. Specifically, we will describe:
* How you can set yourself up for success before you kick off the run by writing assertions, constraints, and cover properties in a “formal friendly” coding style
* What types of logic in your DUT will likely lead to trouble (in particular, deep state space creators like counters and RAMs), and how to effectively handle them via non-destructive black boxing or remodeling
* Matching the run-time multicore configuration and formal engine specifications to the available compute resources
* Once the job(s) start, how to monitor the formal engines’ “health” in real time
* Confirm the relevance of the logic “pulled in” by your constraints
* Show how a secure mobile app can be employed to monitor formal runs when you are away from your workstation
* Examine whether a run’s behavior is consistent with the expected alignment between the DUT’s structure and the formal engines’ algorithmic strengths
* Leverage all of the above to make the final “continue or start over” decision
Thank you to our Sponsor: