From RTL Liveness Assertions to Cost-Effective Hardware Checkers
Ranganathan Hariharan, Tara Ghasempouri, Behrad Niazmand, Jaan Raik · 2018
This paper proposes a methodology for producing a set of high quality hardware checkers from Register-Transfer Level (RTL) assertions. Assertion Based Verification (ABV) has become a highly popular area in design verification. On the other hand, extreme down-scaling of modern technologies has significantly increased the probability of faults occurring during the life-time of the system. To overcome this, concurrent cost-effective checker circuitry is required in order to enable fault resilience of systems. Currently, designing such checker infrastructure is a manual and error-prone work. A possible solution to automate the synthesis of concurrent error checkers is to derive them from verification assertions. However, the number of assertions is generally far too high to allow for area-efficient checking infrastructure. Moreover, the number of liveness assertions generated by automated methods may be too high even for verification purposes. Therefore, there is a need for qualification and minimization of liveness assertions with a prospect of reusing them as hardware safety checkers. In order to derive low-area, high fault coverage hardware safety checkers from a large number of liveness assertions, this paper proposes for the first time a framework for selecting a set of high-quality and minimized liveness assertions by combining a new data mining technique with fault analysis approaches along with assertion conversion methodology that converts liveness assertions into safety assertions. The framework then synthesizes these safety assertions into hardware checkers to be evaluated at the gate level to provide a cost-effective checking infrastructure. Experimental results support the effectiveness of the proposed framework.