Enhancing ABC for LTL Stabilization Verification of SystemVerilog/VHDL Models

Design and Implementation of Formal Tools and Systems 2011.

计算机科学;

Jiang Long ; Sayak Ray ; Baruch Sterin ; Alan Mishchenko ; Robert Brayton

Others  :  http://ceur-ws.org/Vol-832/paper_2.pdf
PID  :  33674

学科分类：计算机科学（综合）

来源: CEUR

【 摘 要 】

We describe a tool which combines a commercial front-end with a version of the model checker, ABC, enhanced to handle a subset of LTL properties. Our tool, VeriABC, provides a solution at the RTL level and produces models for synthesis and formal verification purposes. We use Verific (a commercial software) as the generic parser platform for SystemVerilog and VHDL designs. VeriABC traverses the Verific netlist database structure and produces a formal model in the AIGER format. LTL can be specified using SVA 2009 constructs that are processed by Verific. VeriABC traverses the resulting SVA parse trees and produces equivalent LTL formulae using the F,G, Until and X operators. The model checker in ABC has been enhanced to handles LTL stabilization properties, an important subset of LTL. The paper presents VeriABC’s implementation strategy, software architecture, tool flow, environment setup for formal verification, use model, the specification of properties in SVA and translation into LTL. Finally the properties are translated into safety properties that can be verified by the ABC model checker.