It's all about Methodology
You need your best, sharpest pencils but not every pencil will be used to draw everything you would like. Having a clear sense of proportion, measurement and a clear understanding of requirements is essential to get the best out of your toolkit.
With formal verification that is what is needed. A good understanding of methodologies that underpin successful deployment of formal is needed, something that is very often missing from most formal verification training programmes. If you look around, most formal verification training programmes focus on one hand too much on the assertion languages used, their latest and greatest syntactical enhancements, or on the other too much focus on the EDA toolkit and its features.
The Formal Paradox
Due to this nature of formal verification training and the lack of focus on good methodology, the end user of formal ends up using formal at extremities resulting in the formal paradox which is totally unhealthy. On the one hand you will find Formal Gurus in most organizations working on deep formal – end-to-end verification and on the other a team of engineers using formal apps only exercising the fully automated aspects of the tool.
Unfortunately, neither of these use models result in a comprehensive deployment of formal that exploits the full potential in finding corner case bugs and being able to prove exhaustively properties of the design that may be often needed. There is also a part in the middle of this spectrum where you see teams of engineers exploiting assertions but this is mostly not well organised and not systematically deployed with often assertions being used being simple point-based assertions that check very simple behaviour, again not fully exploiting the full potential of formal.
At Axiomise, we focus on mitigating the gap shown above which is much needed to solve the mainstream functional verification challenges with formal. We specialise in methodologies that allow formal to scale for huge designs.
Scalable formal verification is not the story of the legends requiring PhDs; it can be learnt and applied properly through a combination of good training, consulting and services model. What we have seen in the field is that once an engineer is well trained in the basic and advanced skills of formal verification methodology they can begin well on a project, however in many cases they need follow on mentoring, support and help with verification planning, strategy and detailed execution. Axiomise offers multi-pronged approach to enabling formal verification through its combination of training, consulting and services.
Axiomise provides this opportunity to help you scope out the place of formal in your business, understand what your needs are, and advise you accordingly on what is suitable for your needs. For Axiomise, your business comes first, and we would like to support you in your challenges with using formal. We understand that though training engineers in the skills of formal and methodology is a useful first step, one typically also needs ongoing support and advice before and after the training to get the most out of formal.
Learn more on our consulting promise.
In some cases, organizations simply do not have the necessary head count to take the first step with formal verification training and execution. In such cases, Axiomise offers the possibility of using its own services to undertake turnkey project execution. Find out more about our services.