Formal Has Its Day

As new technologies receive more mainstream attention, it is common for the experts in the area to provide a critical mass of enthusiasm. Formal is in this mode with multiple meetings throughout the year and around the globe. Perhaps one of the most successful of these is the annual Formal Day event put on by Test & Verification Solutions (TVS) based in the UK. This live and online event is now in its fourth year and attracts expert and new users alike, with presentations from a range of users, academics and vendors.

The 2016 event took place June 17 and attracted 183 registrants, 130 of whom were online from 77 countries! What’s great is that TVS posts videos and slides on the TVS Formal Day website of almost all the talks. It’s a great information pool of practical experience and new techniques all available for free!

Mike Bartley, the founder and CEO of TVS, is one of the leading promoters of this approach and his knowledge of verification in general, together with his insights into formal applications, makes him a perfect host for this one-day event.

A quick recap of the day

John Colley from the University of Southampton in the UK kicked off the event with a deep dive into model-based safety and security analysis in, as he put it, “High Consequence” System Development. John, who is well-known in EDA circles after holding senior positions at TransEDA and Imperas, has spent time researching formal methods for use in aeronautical systems.

After some useful definitions, including a look at the various standards governing this electronics industry sector, he examined a model-based approach for specifying safety requirements, considering them as a control rather than a reliability problem. He considered a real life example of this and dug into the actual specification of the example problem, a landing gear door subsystem.

He went on to describe “System Theoretic Early Concept Analysis” and how a model-based approach may be used to specify aircraft trajectory and other factors. This was a fascinating presentation and his ideas could be applied in a number of areas of semiconductor and electronics system design as we continue to consider how requirements might be described in a more machine readable, verifiable fashion.

John’s keynote was followed by another notable formal expert, Elchanan Rapport of GilaLogic, who has consulted for multiple companies on formal verification solutions including IBM, ARM, and TI. Elchanan penned an article for FormalWorld just a few months ago on evaluating formal tools. At this event, he talked about security issues and the use of formal to exhaustively test vulnerabilities in devices. He used a string of case studies to examine how sensitive information propagation may be analyzed using model-checking techniques.

Holgar Busch, the well-known formal verification expert from Infineon, gave an interesting talk around safety compliance verification, an area in which he is particularly expert. In this presentation, he focused on hardware safety mechanisms for registers and register files, and how these could be verified under ISO 26262 conditions. He described various techniques to add error correction to registers and then demonstrated how formal might be used, along with fault injection, to ensure any fault could be trapped and handled up to the ASIL D level describe in the ISO standard.

Ashish Darbari is another well-known formal expert, this time from Imagination. He followed with a presentation on work that he with the rest of his team at Imagination had performed on the use of model abstractions to improve their formal-based methodology. Ashish discussed various forms of model abstractions, starting with the relatively simple case of an abstract FIFO model then moved to more complex examples. He was able to demonstrate how abstraction, together with techniques such as assume-guarantee, could provide exhaustive proofs of a range of design types.

Finally, Alex Orr of Broadcom gave an excellent talk on his experience coming to grips with formal. At last year’s event, Alex talked about his experience as a new user of the technology in one of the most entertaining presentations on the subject that I have seen. Alex, as a self-described “DAVE” (Design And Verification Engineer), talked about his experiences one year on, and did not disappoint. In a highly realistic, practical fashion, Alex dug into his use of the tools, leveraging them on smaller as well as bigger tasks, helping designers reduce implementation bugs, and other formal perspectives in general.

Throughout the day, sponsoring EDA vendors (OneSpin, Cadence, Synopsys and Mentor) presented ideas around their own tools and experiences. OneSpin’s Christian Burisch discussed layering formal into simulation environments and new techniques to help general verification engineers use the tools, including advanced new coverage techniques. Asa Ben-Tzur of Cadence talked about deep state bug hunting, explaining various bug-hunting strategies and how to apply them. Hans-Jorg Peter from Synopsys discussed formal closure and mechanisms available to achieve it. Abdelouahab Ayari from Mentor Graphics provided a primer on formal engines.

TVS continues to host one of the most informative formal events, freely available to engineering teams. A look at the presentations and videos on the website is time well spent for anyone involved in verification.

See you at Formal Day 2017!