-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.
We present an integrated tool flow for liveness model
checking using industry hardware description languages (HDLs) and
SystemVerilog Assertions: (i) VeriABC: a front-end to read in
hardware models expressed in HDLs, and (ii) capability of
model checking a subset of liveness properties. VeriABC is
able to read in hardware models expressed in SystemVerilog
or VHDL. SystemVerilog and VHDL languages are the most
popular HDLs being used in industry today for digital designs.
VeriABC generates a formal model in the AIGER[
In a typical use model, a user will develop a hardware design in SystemVerilog or VHDL, and specify its correctness requirements in the property specification language SystemVerilog Assertion (SVA). SVA has been adopted into IEEE SystemVerilog standard and is supported by major commercial tools in simulation, synthesis and verification. The SVA language in SystemVerilog 2009 standard contains liveness constructs that allow full specification of liveness properties as those defined in LTL formulas. In our framework, a user can specify both safety properties and liveness properties (stabilization properties, to be precise). In this paper, we detail its liveness capabilities.
After reading in a design, VeriABC bit-blasts it into a
bitlevel netlist and converts the SVA stabilization properties into
an intermediate LTL representation. Then the LTL properties
are folded into the bit-level netlist in an appropriate way
(using an extended liveness-to-safety conversion, explained
later in Section IV). The resulting bit-level netlist represents
a formal model of the design, represented as an and-inverter
graph (AIG). And-inverter graphs are concise representations
of finite state machines. The AIGER[
Although parsing and elaborating RTL languages are a
standard practice for commercial EDA products, it is a daunting
task for academics due to language complexity and continuous
language evolution over the years. Although, vl2mv[
Our choice of a commercial and stable front-end Verific, allows academics to get around the language barrier to access real-world designs.
Liveness-to-safety conversion was first proposed in [
As illustrated in Figure 1, we combine a commercial frontend, Verific, with a version of our model checker, ABC, enhanced to handle a subset of LTL properties. Our tool processes the Verific output, conducts various modeling procedures on the design, compiles SVA into LTL formulas, then the enhanced ABC processes the LTL formulas for liveness model checking. We detail the software architecture, tool flow, formal model construction, SVA compilation and downstream LTL modeling checking.
DEBUG
RTL+SVA Verific Netlist Databse AIGER + LTL Formula
AIGER Proven
Error Trace
Verific Parser Platform VeriABC L2S ABC Backend Engines
We first discuss the capabilities of the Verific parser platform. In Section III we describe the architecture, formal modeling of VeriABC and translation of SVA into LTL. In Section IV the stabilization properties are described in further detail. Section V describes the liveness-to-safety conversion for stabilization properties. Experimental results are presented in Section VI.
II. BACKGROUND: VERIFIC PARSER PLATFORM
Verific Design Automation[
Figure 2 shows the architecture of the Verific parser frontend. The main commands we use in Verific library are analyze and elaborate. Analyze creates parse-trees and performs type-inferencing to resolve the meaning of identifiers. The Parser/Analyzer supports the entire SystemVerilog IEEE 1800, VHDL IEEE 1076-1993, and Verilog IEEE 1364-1995/2001 languages, without any restrictions. The resulting parse tree comes with an extensive API.
Elaborate supports both static elaboration and RTL elaboration. Static elaboration elaborates the entire language, and specifically binds instances to modules, resolves library references, propagates defparams, unrolls generate statements, and checks all hierarchical names and function/task calls. The result after static elaboration is an elaborated parse tree, appropriate for simulation like applications. RTL elaboration is limited to the synthesizable subset of the language. In addition to the static elaboration tasks for this subset, it generates sequential networks through flipflop and latch detection, and Boolean extraction. The result after RTL elaboration is a netlist database, appropriate to applications such as logic synthesis and formal verification. This netlist database is the starting point of VeriABC and we utilize Verific provided C++ APIs to access the database.
In this Section, we use Verilog terminology to present Verific’s netlist database structures. The netlist database is rather intuitive and adheres to the module definitions. Shown in Table I, there is a one-to-one correspondence between the C++ API class definitions and Verilog constructs.
A N etlist corresponds to module definitions in Verilog while an Instance object corresponds to module instantiation, Verific Database C++ API Class
Netlist Instance
Port
Net PortRef
Verilog RTL Objects
Module definition
Module instantiation Module port declarations
wire/reg/assign
Port to Net connectivity after the module’s parameters have been characterized. An Instance is a thin copy of the N etlist plus a pointer to its parent netlist. A N etlist contains a set of P orts, N ets and Instances for its internal logic structure. A P ort corresponds to the Verilog port definitions which can be input, output or inout. A N et is a named component, intuitively a wire. P ortRef contains the connectivity between a P ort and a N et. The direction of the P ortRef can be in, out, or inout depending on the type of P ort it contains. Using these C++ objects, the Verific netlist database defines a directed hypergraph and encapsulates the following types of information:
Design hierarchy is captured as an instance tree by the parent pointers in the Instance with a top-level netlist as the root.
Unique Hierarchical Name
Following the design hierarchy through the instance tree, each internal object is assigned a unique hierarchical name.
Connectivity
A directed hyper-graph is defined through P ort, N et and P ortRef : P ort being the node, N et being the edge, and P ortRef containing the connectivity and direction information between pairs of a P ort and a N et. As an edge in the hyper-graph, a N et can be referenced in multiple P ortRef objects.
Logic Definition
At the leaf of the design hierarchy, a N etlist of primitive operator types such as and, or, adder, flipflop, latches etc defines the basic logic operators.
Recursively, the functional behavior of the design is captured through the directed hierarchical hyper-graph with basic logic operators at its leaf level.
VeriABC traverses the above netlist database and transforms it into a monolithic AIG which can be treated as a directed acyclic graph (DAG). The AIG contains primary input, primary output, register nodes and and-inverter nodes. Each named P ort and N et in the Verific netlist has a mapped node in the AIG graph. Additional book-keeping information such as hash tables are created that map the hierarchical name to the corresponding AIG node. The down-stream model checker ABC then reads in this AIG to conduct formal analysis.
A hyper-graph is rather hard to traverse and conduct analysis/transformation at the same time.
As shown in Figure 3, we employ a two phase approach. First we construct an intermediate netlist graph, a DAG with extra annotated node types representing logic structure and connectivity of the flattened design. In addition to the simple node types in and-inverter graphs, extra node types contain annotations for language constructs such as tri states, flipflops and latches etc. For example, flipflops contain set/reset pins and driving d-pins; latches contain additional gated-clock definitions. By language definition, a design can specify any signal for the clock and reset signals. Design behavior is defined by event-driven semantics. Further analysis needs be done to determine if there is an AIG representation that can capture the original design semantics. The intermediate netlist is a DAG for which various traversal algorithms can be conducted for the later analysis. For this step, VeriABC only traverses the design hierarchy and hyper-graph in the Verific netlist database to gather information and construct the intermediate DAG representation without conducting any design style checking or transformation.
Verific Netlist
Database Intermediate Netlist Graph
AIG
The end result of VeriABC is an AIG model that is consistent with the original RTL design semantics. AIG is recognized as a finite state machine model. Compared to the event-driven semantics in HDL language, the execution semantics of an AIG is synchronous with an implicit universal clock that ticks at every step of the execution. The register loads in its driver value at the beginning of each step. The semantics inferred from the Verific netlist structure is more complex, such as its flip-flop can have arbitrary reset logic and clock network. The task in formal modeling is to transform the above design components into AIG registers with additional glue logic so that it maintains the consistency. In its simplest form, the following check determines if the design can be readily represented by an AIG.
All registers are clocked by the same primary input signal which does not fanout to other nodes.
Reset/Set signals are primary inputs
No multiple drivers per node
More complex design modeling and transformations can be achieved by identifying certain patterns by traversing the intermediate netlist graph. Our current implementation supports the above form and produces a design style summary for debugging purposes. Though capacity and performance depends on the type of individual transformation and analysis, for the above ones, the transformation and design style checking is very fast, as it conducts only a few traversals of the intermediate netlist graph. After design style checking, a final traversal of the intermediate netlist graph generates an AIGER file representing the formal model.
VeriABC implementation utilizes the Tcl command interface shipped with the Verific library distribution. The following is the list of commands implemented to manage the environment setup for formal verification.
veriabc analyze
This command constructs the intermediate netlist graph in Figure 3 and conducts design style checking. veriabc set reset
Although a reset signal can be automatically detected in certain situations, this command provides the user with the option to specify the length of the reset sequence and phase of the reset condition. A user can also specify the initial value of the registers through a VCD waveform or textual file. In the generated formal model, the initial value of the registers will be valued at the end of the reset sequence and the reset condition will be disabled after reset. veriabc set clock
A user can specify the clock periods and relationships in the situation when multi-clocks are in the design. A phase-counter network will be created in the formal model to generate the corresponding clock signals. veriabc set cutpoint
This command will prune the cone-of-influence at cutpoint signal and treat it as free input. veriabc set constant
This command sets either an input or a cut-point signal to a constant value. veriabc set assume
This constrains the design signal to be a constant. veriabc write
write out the final formal model in AIGER format. The above commands give the user flexibility to model the environment with constraints and conduct design abstractions during verification.
Figure 4 are the templates for matching the basic LTL operators used in the set of stabilization properties. For stabilization properties, in our current implementation, we restrict the p and q to be Boolean expressions which seems to be sufficient in practice. The SVA verification directive assume is used to specify a fairness constraint, while assert is used to specify the target LTL properties.
property Until(p,q);
p s_until q; endproperty property GF(p);
always (s_eventually p); endproperty property FG(p);
s_eventually (always p); endproperty property X(p);
s_nexttime (p); endproperty Fig. 4. SVA Liveness Template
Verific also processes SVA constructs into the netlist database structure, essentially a corresponding parse tree is integrated into the netlist. We conduct traversals of the parse tree, identify specific liveness constructs and map them into the corresponding LTL formula. At the end of the procedure, along with the AIGER file generated, a separate file containing the LTL formulas are generated indicating target liveness assertions and fairness constraints. The support signals referred to in the LTL formulas are named output signals in the AIGER file. Although we currently only support stabilization properties in LTL, the full LTL language using X, F , G, U operators can be specified fully and translated through SVA constructs. In doing so, this completes the formal model generation and SVA compilation at the RTL level.
IV. LIVENESS MODEL CHECKING IN VERIABC
In the FSM modeling formalism, the most intuitive notion
of stabilization states that the system will always reach a
particular state and stay there forever, no matter which state the
system started from or which path it took. Relaxing this notion
a bit, stabilization means that the system will eventually reach
and stay within a given subset of states. Also, stabilization may
denote conditions on the input and output signals of a system
when it attains a stable state. Applications of stabilization
properties have been demonstrated in [
In SystemVerilg 2009 standard, a rich set of LTL operators
are added into SVA language. The SVA properties shown in
Familiarity is assumed with LTL, basic model checking
algorithms, and related terminology like Kripke structures and
Bu¨chi automata. For further details, see [
Definition 1 (GF-atom): Any LTL formula of the form GFp or FGp, where p is some atomic proposition or some Boolean formula involving atomic propositions only, will be called a ‘GF-atom’.
Stabilization properties are defined as the family of LTL formulas that are Boolean combinations of GF-atoms. Formally:
Definition 2 (Stabilization Property): The set of stabilization properties is the syntactic subset of LTL defined as follows: any GF-atom is a stabilization property if is a stabilization property, then so is : if and are stabilization properties, then so are ^ and _
Example 1: FGp, GFp ) GFq, FGp ^ FGq ) FGr, and FGp ) FGq _ (FGr ^ GFs) are stabilization properties where p; q; r, and s are atomic propositions or Boolean formulas involving atomic propositions only and a ) b is the usual shorthand for :a _ b. However, G(r ) Fg) is an LTL liveness property but not a stabilization property.
Needless to say, these are all liveness properties. But not
all of them specify so-called system stabilization directly.
Properties like FGp and FGp ^ FGq ) FGr (or its
generalk
ization ^i=1FGpi ) FGq) are perhaps the most elementary
stabilization properties. FGp means that the system eventually
will reach a state from where p will always hold, i.e. the
system will eventually ‘stabilize’ at p. FGp ^ FGq ) FGr
means that if the system stabilizes at p and also at q (at
perhaps some other time), then it will stabilize eventually
at r. Hence, semantics of these properties are close to the
intuitive notion of stabilization. [
The main motivation behind considering this broader subset
of LTL is that we offer a short-cut L2S conversion,
avoiding Bu¨chi automaton construction, in a uniform way (due
to the duality between FG and GF operators). The most
significant applications of this class that we have encountered
is “stabilization verification”, and hence the name is coined
for the family. (This name was inspired by [
The class of LTL properties defined as stabilization
properties in this paper is a very important class of temporal
properties extensively studied in the literature. It is related
to so-called fairness specifications. Operators GF and FG
are often called infinitary operators [
V. L2S CONVERSION FOR STABILIZATION PROPERTIES It is important to understand that any counterexample to a liveness property (which must be an infinite trace) can be seen as a “lasso” like configuration with a finite handle and a finite loop. Therefore a liveness counter-example is a lasso which does not satisfy the property on the loop but satisfies all imposed fairness constraints on the loop.
In general, a liveness problem is converted to a safety
problem by adding a loop-detection logic and property-detection
logic on top of the product of the FSM of the original system
and the Bu¨chi automaton of the property to be verified. The
loop-detection logic consists of a set of shadow registers,
comparator logic, and an ‘oracle’. The oracle saves the system
state in the shadow registers at a non-deterministically chosen
time. In all subsequent time frames, the current state of the
system is compared to the state in the shadow registers.
Whenever these two states match, the system has completed a
loop. The non-deterministic nature of the oracle allows all such
loops to be explored. The property verification logic checks if
any of the liveness conditions are violated in any such loop
and all fairness conditions always hold in the loop. This check
is done as a safety obligation. For a more detailed exposition,
see [
As mentioned, for some simple properties L2S conversion
can be achieved while avoiding explicit Bu¨chi automata
construction. This is done by adding more functionality to the
property detection logic. As presented in [
In the next paragraph, we describe how this construction
verifies Fp. In Section V-A we explain how to extend the ideas
of Figure 5 for stabilization properties. Instead of presenting
the liveness-to-safety conversion through Kripke
structurebased representations (i.e. through explicit state machines
based representations), we present the idea in terms of an
actual circuit construction (i.e. through symbolic representation
of the state space). Also, although we do not discuss it further,
the same mechanism handles fairness constraints, which are
always stabilization properties, so they just entail adding
additional logic to the circuit for the monitor. For Kripke
structure-based descriptions of liveness-to-safety conversion,
see [
In Figure 5, save represents an additional primary input added to the circuit. This plays the role of the ‘oracle’. When save is asserted for the first time, the current state of the circuit is saved in the set of shadow registers, and register saved is set. saved thus remembers that input save has been asserted and allows any further activity on save to be ignored. For subsequent time frames, saved enables the equality detection between the current state of the circuit and the state in the shadow registers. Clearly, signal looped is asserted iff the system has completed a loop. Signal live remembers if the signal p has ever been asserted. The safety property that the circuit verifies is, therefore, looped ) live. (In general this would be looped & fair ) live.) The block marked with “*” represents this logical implication - the direction of the arrow distinguishes the antecedent signal from the consequent signal of the implication.
In [
Consider a simple stabilization property of the form FGa ) FGb + FGc. An L2S converted circuit for this is shown in Figure 6. (For simplicity, we do not show any fairness constraints in the example.) Note that, signal live in Figure 5 monitors if signal p has ever been asserted from the very initial time frame. But for verifying GFp, we need to monitor whether signal p has been asserted between the time when saved is set and the time when looped becomes true. Using this fact, the duality between FG and GF operators, and the Boolean structure Xa ) Xb+Xc of the given formula, we can derive the circuit of Figure 6. Logic that captures the Boolean structure of is marked with a dotted triangle in Figure 6. Hence, for any arbitrary stabilization property, we need to create monitors for individual GF-atoms and a crown of combinational logic on top of these monitors that captures the Boolean structure of the property. We can formulate the following theorem.
Theorem 1: For any stabilization property, the given procedure finds one counter-example if one exists.
(Proof Sketch) Any stabilization property can be transformed into another stabilization property with GF operators only. Let f be the Boolean structure in the negation of the given stabilization property. The procedure described above will create a monitor that will search for a lasso-loop where f is violated inside the loop. Since the procedure implicitly enumerates all possible cycles in the state space, it will detect a violating cycle if one such exists.
We implemented our L2S scheme for general stabilization
properties in ABC and experimented with several designs of
communication fabrics from industry. Our objective was to
verify all stabilization properties defined for every structural
primitive of the XMAS framework [
We found that the ABC based L2S implementation has
much better scalability than NuSMV. NuSMV can solve only
toy designs while on the large designs of interest, it fails
to produce a result. On the other hand, our tool works well
even on large designs. For most cases, it produces a result
almost immediately. For a few cases, initial trials could not
produce a proof, but with the latest version of ABC using
simplification, abstraction, speculative reduction, and property
directed reachability (PDR) analysis [
Experimental results are shown below. Among all the local
properties that the XMAS compiler generated, we provide
results for the most challenging one. Call this property ; it
is defined for a FIFO buffer, and has the following LTL form
:= FG(:a) ) FG(:b) _ FG(c)
where a; b; and c are appropriate design signals (i.e. interface
signals of a FIFO buffer). Table 1, 2, and 3 compare the
performance of ABC with NuSMV on small examples. These
examples are instances of communication fabrics or
submodules thereof, and are explained in full detail in [
Since is defined for a FIFO buffer and the XMAS compiler created one instance of for each FIFO buffer, the Fig. 5.
Liveness-to-safety transformation for Fp . ..
Save
Verification state bits .. .
Saved ....
Save
Verification a b c . state bits .. .
Saved 0 1 0 1 0 1 0 1 = Shadow Registers Live Looped
Prop # 0 1 2 3
ABC (sec) 0.03 0.12 0.8 0.8 number of instances is the same as the number of FIFO buffers. For example, the designs corresponding to Table 1, 2, and 3 above have 3, 6, and 4 FIFO buffers, respectively.
We also experimented on two large communication fabrics
of practical interest [
We have developed a tool, VeriABC, which allows us to access real industrial designs written in SystemVerilog or VHDL and to process them into the AIGER format. The result can be used for synthesis and verification using a tool like ABC. We described how the RTL processing is done using the commercial front-end, Verific. SVA assertions are also processed by Verific, and VeriABC creates a separate file of equivalent LTL formulas. We showed an application of this to property checking, where ABC was enhanced to convert a subset of LTL into a circuit structure, thus effectively allowing liveness checking in ABC.
The use of a stable, supported and complete language processing tool like Verific, allows academics access to real industrial designs, without going through the hassle and daunting task of building their own equivalent tool. Liveness property checking is a growing interest in industry, and our enhanced ABC with a front end that automatically converts to a circuit structure for liveness checking, can use the advanced safety property methods of ABC.
In the future, the development of VeriABC will allow us to extract higher level constructs from SystemVerilog and VHDL by accessing Verific’s parse trees. These constructs can be passed on using an extended AIGER format to an enhanced ABC, which will use this information in synthesis and verification.