基于形式验证的毛刺检测技术

Glitch detection method based on formal verification

为解决SoC(system on chip)设计中无法在RTL(register transfer level)阶段验证毛刺存在及其影响问题,提出一种使用形式验证技术在RTL级检测毛刺的方法,同时提出RTL级毛刺故障注入方法。通过检测逻辑门输入同时翻转的原理设计毛刺检测电路,使用形式验证中断言实现检测电路;基于毛刺检测电路和毛刺在时序逻辑的影响,设计其影响等价电路,实现RTL级毛刺故障注入。实验结果表明,该方法能够准确检测毛刺存在并通过毛刺注入分析,进一步发现毛刺对电路功能的影响,将对毛刺的检测和影响分析提前到RTL级,减少了因后期毛刺故障带来的设计迭代和周期成本。

In the design of SoC(system on chip),to solve the problem that it is difficult to detect glitch and its impact in RTL(register transfer level),a method using formal verification to detect glitch was proposed.At the same time,a RTL glitch fault injection method was proposed.A glitch detection circuit was designed by detecting the logic gate input flip at the same time,and the detection circuit was realized by assertion in formal verification.Based on glitch detection circuit and glitch propagation analysis in sequential logic circuits,an equivalent circuit of glitch was designed to achieve RTL fault injection.Experimental results show that the proposed method can accurately detect the glitches and the glitch fault injection can help detect the effect of glitch on RTL function.The glitch detection and effect analysis are brought forward to RTL,reducing the design iteration and time cost caused by glitch fault in late stage.