Properties first? a new design methodology for hardware, and its perspectives in safety analysis
Joakim Urdahl, Shrinidhi Udupi, Tobias Ludwig, Dominik Stoffel, Wolfgang Kunz · 2016
This paper discusses the possible role of formal verification techniques in system-level design flows. It is argued that the role of formal verification techniques should not be limited to “bug hunting” alone. Instead, formal technology should be applied in such a way that a formal relationship is provided between an abstract system model and its concrete implementation at the Register Transfer Level (RTL). In order to avoid the high efforts associated with verification by property checking this paper advocates for a top-down methodology where abstract properties are automatically generated from a system-level description and are later refined along the design process. One advantage of this methodology is to obtain a formally verified design at lower costs when compared to conventional property checking. Moreover, the proposed approach can be beneficial also when analyzing non-functional design targets. The paper demonstrates this for safety. We present experimental results that show how the effects of Single Event Upsets (SEUs) at the gate level of an SoC module can be related to safety requirements at the system's transaction level with formal precision.