There are a number of events in the Formal Verification calendar where the latest thinking on this technology gets highlighted. The Test & Verification Services (TVS) Formal Day is particularly interesting as it combines hard-core formal technology advances with practical usage examples from both Formal vendors and users alike. It has something for the experts as well as new adopters, and everyone in between.
It’s not surprising, given its heritage. 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.
The annual TVS Formal Day has been running for four years now, and every year it gets a little larger and attracts more people. The 2016 Formal Day did not disappoint, with presentations from all the main vendors and a good group of user experts. All the presentations may be found on the TVS Formal Day website.
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 electronic 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 (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, the ideas of which might be applied in a number of areas of semiconductor and electronic 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 Rappaport 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 a very 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, but then moving 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 getting 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 this author has 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 the tools, leveraging them on smaller as well as bigger tasks, helping the designers reduce implementation bugs, and other Formal perspectives in general.
Throughout the day the 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.