State-of-the-art EDA tools largely employ functional circuit models that are inadequate for verifying and emulating design properties related to fault effect and tolerance. In this paper, we derive fully synthesizable fault effect propagation models for formally reasoning about fault-related design behaviors under different types of faults. We associate each signal bit with a binary fault label to reflect its fault attribute. We further derive fine-granularity precise propagation policies and specify these policies as formal models for fault effect analysis using functional EDA tools. Experimental results using IWLS benchmarks have demonstrated that our formal models can be used to measure fault propagation effects and accelerate fault verification through hardware emulation. Our work makes a step towards property driven EDA flows that allow fault tolerance and dependability to be verified alongside functional correctness.

Lingjuan Wu got her PhD degree in Microelectronics and Solid State Electronics from Peking University in 2013. She visited the University of California, San Diego as a research scholar from 2010 to 2012. She is currently an associate professor with the College of Informatics, Huazhong Agricultural University. Her research interests are in hardware security, including secure architecture, formal security verification, side channel analysis and hardware Trojan detection.
 

Fault effect, fault propagation, formal model, property driven EDA.