Speaker
Mr
Mark Handover
(Mentor, A Siemens Business)
Description
In recent years, Formal verification has moved beyond a tool solely for use by experts and into the mainstream. Now, targeted formal apps’ are lowering the barrier to entry for formal, enabling its use in automated design checking, clock domain crossing analysis and coverage closure to name a few.
This session will briefly discuss a range of formal apps’ available before focusing on one particular use case - how automated, formal-based Sequential Logic Equivalency Checking (SLEC) techniques can exhaustively verify the effectiveness of the Single Event Upset (SEU) mitigation logic vs. transient/SEU events — as well as stuck-at and bridging faults. To illustrate this, a case study describing fault analysis of a Triple Modular Redundancy (TMR) element will be presented; including fault population reduction, fault injection, checking and classification, and collection of metrics. Finally, we will compare formal results and run time against those obtained using dynamic simulation techniques, and show how formal is able to minimize the analysis effort required.
Primary author
Mr
Mark Handover
(Mentor, A Siemens Business)
