The second DIFTS (Design and Implementation of Formal Tools and Systems) workshop was held at Portland, Oregon on Oct 19, 2013, co-located with Formal Methods in ComputerAided Design Conference (FMCAD), and Formal Methods and Models for Co-design (MEMOCODE). The workshop emphasized the insightful experiences in tool and system design. The goal of the workshop is to provide a forum for sharing challenges and solutions that are original with ground breaking results. The workshop provided an opportunity for discussing engineering aspects and various design decisions required to put such formal tools and systems into practical use. It took a broad view of the formal tools/systems area, and solicited contributions from hardware and software domains such as decision procedures, verification, testing, validation, diagnosis, debugging, and synthesis.
The workshop received 10 original submissions, out of which 3 were chosen under tool category, and 3 were chosen under system category. There were also three invited talks: first was given by Rance Cleaveland, Reactive Systems Inc., USA on “Approximate Formal verification using Model-based Testing”, second was given by Masahiro Fujita, University of Tokyo on “Diagnosis and correction of buggy hardware/software with formal approaches”, and third talk was given by Dhiraj Goswami, Synopsys Inc. on “Stimulus generation, enhancement and debug in constraint random verification.”
First of all, we thank FMCAD’s steering committee for their continual support. We also thank FMCAD chairs Sandip Ray and Barbara Jobstmann, and MEMOCODE chairs Marly Roncken and Fei Xie for a seamless organization. We also thank Joe Leslie-Hurd for his help in local arrangements. We thank Boğaziçi University, Turkey for hosting the DIFTS website. We sincerely thank the program committee members and sub reviewers for selecting the papers and providing candid review feedbacks to the authors. Last but not least, we thank all the authors for contributing to the workshop and to all the participants of the workshop.
Malay K. Ganai and Alper Sen Program Chairs DIFTS 2013
Additional Reviewers
Diagnosis and Correction of Buggy Hardware/Software with Formal Approaches . . . . . . . . . .
Masahiro Fujita (Invited speaker) Stimulus generation, enhancement and debug in constraint random verification . . . . . . . . . . .
Dhiraj Goswami (Invited speaker) A Fast Reparameterization Procedure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Niklas Een and Alan Mishchenko LEC: Learning driven data-path equivalence checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Jiang Long, Robert Brayton and Michael Case 1 2 3 4 9 Trading-off Incrementality and Dynamic Restart of Multiple Solvers in IC3 . . . . . . . . . . . . . . 19
Marco Palena, Gianpiero Cabodi and Alan Mishchenko Approximate Formal Verification using Model-based Testing
Rance Cleaveland
University of Maryland, USA Abstract: In model-based testing, (semi-)formal models of systems are used to drive the derivation of test cases to be applied to the system-under-test (SUT). The technology has long been a part of the traditional hardware-design workflows, and it is beginning to find application in embedded-software development processes also. In automotive and land-vehicle controlsystem design in particular, models in languages such as MATLAB® / Simulink® /Stateflow® are used to drive the testing of the software used to control vehicle behavior, with tools like Reactis®, developed by a team including the speaker, providing automated test-case generation support for this endeavor. This talk will discuss how test-case generation capabilities may also be used to help verify that models meet formal specifications of their behavior. The method we advocate, Instrumentation-Based Verification (IBV), involves the formalizaton of behavior specifications as models that are used to instrument the model to be verified, and the use of coverage testing of the instrumented model to search for specification violations. The presentation will discuss the foundations of IBV, the test-generation approach and other features in Reactis® that are used to support IBV, and the results of several case studies involving the use of the methods. Diagnosis and Correction of Buggy Hardware/Software with Formal Approaches
Masahiro Fujita
University of Tokyo, Japan Abstract: There have been intensive researches on debugging hardware as well as software. Some are very ad-hoc and based on simple heuristics, but others utilize formal methods and are mathematically modeled. In this talk, we first review various proposals on debugging from historical viewpoints, and then summarize the state-of-the-art in terms of both diagnosis and automatic correction of designs. In particular we show various approaches with SAT-based formulations of diagnosis and correction problems. We also discuss about them in relation to manufacturing test techniques. That is, if the design errors are within the pre-determined types and/or areas, there could be very efficient ways to formally verify, diagnosis and correction methods with small numbers of test vectors. In the last part of the talk, future perspectives including post-silicon issues are discussed. Stimulus Generation, Enhancements and Debug in Constraint Random Verification
Dhiraj Goswami
Synopsys, USA Abstract: Verification cost in an IC design team occupies 60-80% of the entire working resources and efforts. Functional verification, posed at the foremost stage of the IC design flow, determines the customers' ability to find bugs quickly and thereby their time-to-results (TTR) and cost-of-results (COR). Consequently, functional verification has been the focus of the EDA industry for the last several decades.
Constrained random simulation methodologies have become increasingly popular for functional verification of complex designs, as an alternative to directed-test based simulation. In a constrained random simulation methodology, random vectors are generated to satisfy certain operating constraints of the design. These constraints are usually specified as part of a testbench program (using industry-standard testbench languages, like SystemVerilog from Synopsys, e from Cadence, OpenVera, etc.). The testbench automation tool (TBA) is then expected to generate random solutions for specified random variables, such that all the specified constraints over these random variables are satisfied. These random solutions are then used to generate valid random stimulus for the Design Under Verification (DUV). This stimulus is simulated using industry-standard simulation tools, like VCS from Synopsys, NC-Verilog from Cadence, etc. The results of simulation are then typically examined within the testbench program to monitor functional coverage, which gives a measure of confidence on the verification quality and completeness.
In this talk we will review the challenges of stimulus and configuration generation using constraint random verification methodology. We will also explore why state-of-the-art debug solutions are important to handle complexity and improve the quality of stimulus.
Niklas Een, Alan Mishchenko Berkeley Verification and Synthesis Research Center
EECS Department University of California, Berkeley, USA.
Abstract. Reparameterization, also known as range preserving logic synthesis, replaces a logic cone by another logic cone, which has fewer inputs while producing the same output combinations as the original cone. It is expected that a smaller circuit leads to a shorter verification time. This paper describes an approach to reparameterization, which is faster but not as general as the previous work. The new procedure is particularly well-suited for circuits derived by localization abstraction. 1
The use of reparameterization as a circuit transformation in the verification flow was pioneered by Baumgartner et. al. in [1]. In their work, new positions for the primary inputs (PIs) are determined by finding a minimum cut between the current PI positions and the next-state variables (flop inputs). BDDs are then used to compute the range (or image) on the cut. Finally, a new logic cone with the same range (but fewer PIs), is synthesized from the BDDs and grafted onto the original design in place of the current logic cone. This is a very powerful transformation, but it has potential drawbacks: (i) the BDDs may blow up and exhaust the memory, (ii) the extracted circuit may be larger than the logic it replaces, and (iii) the runtime overhead may be too high.
In contrast, the proposed approach is based on greedy
local transformations, capturing only a subset of optimization
opportunities. However, memory consumption is modest,
runtimes are very low, and the resulting design is always
smaller, or of the same size, as the original design. It is
shown experimentally that the proposed method leads to
sizeble reductions when applied for circuits produced by
localization abstraction [
The fast reparameterization algorithm is based on the following observation: if a node dominates1 a set of PIs, and those PIs are sufficient to force both a zero and a one at that node, regardless of the values given to the other PIs and state variables, then that node can be replaced by a new primary input, while the unused logic cone driving 1A node n dominates another node m iff every path from m to a primary output goes through node n. the original node can be removed. The old primary inputs dominated by the given node are also removed by this procedure.
Example. Suppose a design contains inputs x1, x2, and a gate Xor(x1, x2); and that furthermore, x1 has no other fanouts besides this Xor-gate. Then, no matter which value x2 takes, both a zero and a one can be forced at the output of the Xor by setting x1 appropriately, and thus the Xor-gate can, for verification purposes, be replaced by a primary input.
The proposed method to find similar situations starts by computing all dominators of the netlist graph, then for each candidate node dominating at least one PI the following quantification problem is solved: “for each assignment to the non-dominated gates, does there exist a pair of assignments to the dominated PIs that results in a zero and a one at the candidate node”. More formally, assuming that x represents non-dominated gates (“external inputs”) and yi represents dominated PIs (“internal inputs”), the following is always true for the node’s function φ:
∀x ∃y0, y1 . ¬φ(x, y0) ∧ φ(x, y1) Important features of this approach are: (i) It is circuit based, while early work on reparameterization was based on transition relations [4]. (ii) In its simplest form, the proposed restructuring replaces some internal nodes by new primary inputs and remove dangling logic. (iii) The analysis is completely combinational: no information on the reachable state-space is used. (iv) If the property was disproved after reparametrization, it is straight-forward to remap the resulting counterexample to depend on the original primary inputs. It is important to realize that by analyzing and applying reductions in topological order from PIs to POs, regions amenable to reparameterization are gradually reduced to contain fewer gates and PIs. By this process, the result of repeatedly applying local transformations can lead to a substantial global reduction. In the current implementation, the above formula is evaluated by exhaustive simulation of [cand]
& & ! ! & ? the logic cone rooted in the given node while the cone is limited to 8 inputs. Limiting the scope to cones with 8 inputs and simulating 256 bit patterns (or eight 32-bit words) seems to be enough to saturate the reduction achievable on the benchmarks where the method is applicable.
Some typical reductions are shown in Figure 1. The graphs should be understood as sub-circuits of a netlist being reparameterized. The exclamation marks denote “internal” PIs dominated by the top-node, and hence under our control; and the question marks denote gates with fanouts outside the displayed logic cone, for which no assumption on their values can be made. The full algorithm is described in Figure 2.
Counterexample reconstruction. There are several ways that a trace on the reduced netlist can be lifted to the original netlist. For instance, the removed logic between the new PIs and the old PIs can be stored in a separate netlist. The trace on the reduced netlist can then be pro− Compute dominators. For a DAG with bounded in-degree (such as an And-Inverter-Graph), this is a linear operation in the number of nodes (see Figure 3). − For each PI, add all its dominators to the set of “candidates”. − For each candidate c, in topological order from inputs to outputs: - Compute the set D of nodes dominated by c (Figure 4). - Denote the PIs in D “internal” inputs. - Denote any node outside D, but being a direct fanin of a node inside D, an “external” input (may be any gate type). - Simulate all possible assignments to the internal and external inputs. If for all external assignments there exists an internal assignment that gives a 0 at c, and another internal assignment that gives a 1 at c, then substitute c by a new primary input. Compute Dominators − Initialize all POs to dominate themselves − Traverse the netlist in reverse topological order (from POs to PIs), and mark the children of each node as being dominated by the same dominator as yourself unless the child has already been assigned a dominator − For already marked children, compute the “meet” of the two dominators, i.e. find the first common dominator. If there is no common dominator, mark the node as dominating itself.
Compute Dominated Area area = {w dom} count = [0, 0, . . ., 0] for w ∈ area: for v ∈ faninsOf (w ): count[v ]++ if count[v ] == num of fanouts[v ]: area = area ∪ {v } – init. set of gates to the dominator – count is a map “gate → integer” jected onto the original PIs by rerunning the simulation used to produce the reparameterized circuit, and for each candidate pick an assignment that gives the correct value.
3
The algorithm described in the previous section replaces internal nodes with inputs, and thus only removes logic. If we are prepared to forgo this admittedly nice property and occasionally add a bit of new logic, then nodes that are not completely controllable by their dominated inputs can still be reparameterized by the following method: for node with function φ(x, y), where x are external inputs and y are internal inputs, compute the following two functions: φ0(x) ≡ ∀y.¬φ(x, y) φ1(x) ≡ ∀y.φ (x, y)
¬φ0(x) ∧ (φ1(x) ∨ ynew) In other words, if two or more inputs are dominated by the node φ, a reduction in the number of inputs is guaranteed. Depending on the shape of the original logic, and how well new logic for φ0 and φ1 is synthesized, the number of logic gates may either increase or decrease. In our implementation, logic for φ0 and φ1 is created by the fast irredundant sum-of-product (“isop”) proposed by Shin-ichi
for all nodes with two or more dominated PIs, even if it leads to a blow-up in logic size. To counter such cases, fast logic synthesis can be applied after the reparameterization.
4
Another possible improvement to the method is extending the reparameterization algorithm to work for multi-output cones. As an example, consider a two-output cone where the outputs can be forced to all four combinations {00, 01, 10, 11} by choosing appropriate values for dominated inputs. In such a case, the cone can be replaced by two free inputs. If some of the four combinations at the outputs are impossible under conditions expressed in terms of non-controllable signals, a logic cone can be constructed to characterize these conditions and reduce the number of PIs by adding logic similar to the case of a single-output cone. 5
As part of the experimental evaluation, all benchmarks
from the single-property track of the Hardware
Modelchecking Competition 2012 were considered. Localization
abstraction [
table Table 1. All those models were given to the reparameterization engine, both in weak mode and strong mode, the latter using the improvements described in section 3.
a quick simplification method called “shrink” which is part
of the ABC package [
ning an industrial implementation of the BDD based algorithm of [1]. Because runtimes are significantly longer with this algorithm, they are given their own column. These results were given to us from IBM, and according to their statement “are not tweaked as much as they could be”.
rected Reachability [
previous work in the runtime of the reparameterization algorithm itself, with comparable quality of results for the application under consideration (models resulting from localization abstraction). This means the algorithm can always be applied without the need for careful orchestration.
tion times when applying reparameterization in conjunction with PDR, which is also the best overall engine on these examples. For two benchmarks, 6s121 and 6s150, BDD reachability do substantially better than PDR, and for the latter (where runtimes are meaningful) the speedup due to reparameterization is greater than 3x. Furthermore, for BDD reachability one can see that on several occasions (6s30 in particular), reparameterization is completely crucial for performance. Finally, interpolation based modelchecking (IMC) seems to be largely unaffected by reparameterization.
2Benchmarks from HWMCC’12 are quite small. For comparison: running reparameterization on a 7 million gate design from one of our industrial collaborators took 4.1 s. Design !! #And 6s102 !! 6,594 6s121 !! 1,636 6s132 !! 1,216 6s144 !! 41,862 6s150 !! 5,448 6s159 !! 1,469 6s164 !! 1,095 6s189 !! 36,851 6s194 !! 12,049 6s30 !! 1,043,139 6s43 !! 7,408 6s50 !! 16,700 6s51 !! 16,701 bob05 !! 18,043 bob1u05cu !! 32,063 ! ! ! Design !! #And 6s102 !! 6,594 6s121 !! 1,636 6s132 !! 1,216 6s144 !! 41,862 6s150 !! 5,448 6s159 !! 1,469 6s164 !! 1,077 6s189 !! 36,851 6s194 !! 12,049 6s30 !! 102,535 6s43 !! 7,408 6s50 !! 16,700 6s51 !! 16,701 bob05 !! 18,043 bob1u05cu !! 32,063 1,137 !! 1,247 408 !! 627 120 !! 1,108 3,580 !! 10,172 867 !! 3,062 247 !! 116 196 !! 661 2,654 !! 10,033 2,723 !! 1,366 34,061 !! 1,508
685 !! 3,451 4,470 !! 1,841 4,468 !! 1,828 2,358 !! 1,618 4,455 !! 1,618 #PI
#FF ! ! ! Strong !! NoRep.
!
!
!
Strong !! NoRep.
[
Proc. of SASIMI, 1992.
[
ABC-ZZ: A C++ framework for verification & synthesis. https://bitbucket.org/niklaseen/abc-zz. LEC: Learning-Driven Data-path Equivalence
Checking Jiang Long , Robert K. Brayton , Michael Casey
EECS Department, UC-Berkeley fjlong, braytong@eecs.berkeley.edu yCalypto Design Systems Abstract—
In the LEC system, we employ a learning-driven approach for solving combinational data-path equivalence checking problems.
The data-path logic is specified using Boolean and word-level operators in VHDL/Verilog. The targeted application area are Cto-RTL equivalence checking problems found in an industrial setting. These are difficult because of the algebraic transformations done on the data-path logic for highly optimized implementations.
Without high level knowledge, existing techniques in bit-level equivalence checking and QF BV SMT solving are unable to solve these problems effectively. It is crucial to reverse engineer such transformations to bring more similarity between the two sides of the logic. However, it is difficult to extract algebraic logic embedded in a cloud of Boolean and word-level arithmetic operators. To address this, LEC uses a compositional proof methodology and analysis beyond the bit and word level by incorporating algebraic reasoning through polynomial reconstruction.
LEC’s open architecture allows new solver techniques to be integrated progressively. It builds sub-model trees, recursively transformating the sub-problems to simplify and expose the actual bottleneck arithmetic logic. In addition to rewriting rules that normalize the arithmetic operators, LEC supports conditional rewriting, where the application of a rule is dependent on the existence of invariants in the design itself. LEC utilizes both functional and structural information of the data-path logic to recognize and reconstruct algebraic transformations. A case-study illustrates the steps used to extract the arithmetic embedded in a data-path design as a linear sum of signed integers, and shows the procedures that collaboratively led to a successful compositional proof.
I. INTRODUCTION
With the increasing popularity of high-level design
methodologies there is renewed interest in data-path equivalence
checking [3][
The data-path logic targeted in this paper is specified
using Verilog/VHDL. The bit and word-level operators in
Verilog/VHDL have the same semantic expressiveness as SMT
QF BV theory[
Boolean bit-wise arithmetic extract concat comparator shifter
Verilog operators &&; k; !; ; mux &; j; ; ; mux +; ; ; =; % [] fg <; >; ; ;
SMT QF BV operators
and; or; not; xor; ite bvand; bvor; bvnot; bvxor; bvite bvadd; bvsub; bvmul; bvdiv; bvmod extract concat bvugt; bvult; bvuge; bvule
bvshl; bvshr
The differences between the two data-path logics under equivalence checking are introduced by various arithmetic transformations for timing, area and power optimizations.
These optimizations are domain specific and can be very specialized towards a particular data-path design and underlying technology. They have the following characteristics:
The two sides of the miter logic are architecturally different and have no internal match points.
Many expensive operators such as adders and multipliers are converted to cheaper but more complex implementations and the order of computations are changed. It is not a scalable solution to rely on SAT solving on the bit-blasted model.
The parts of the transformed portion are embedded in
a cloud of bit and word level operators. Algebraic
extraction [
Word-level rewriting uses local transformation. Without high-level information, local rewriting is not able to make the two sides of the miter logic structurally more similar.
Lacking high-level knowledge of the data-path logic, the equivalence problems can be very difficult for gate-level equivalence checking and general QF BV SMT solvers. Strategically, LEC views the bottleneck of such problems as having been introduced by high-level optimizations and employs a collaborative approach to isolate, recognize and reconstruct the high-level transformations to simplify the miter model by bringing in more structural similarities.
B. Contributions
The LEC system incorporates compositional proof strategies, uses rewriting to normalize arithmetic operators, and conducts analysis beyond bit and word level. The collaborating procedures help to expose the actual bottleneck in a proof of equivalence. The novel aspects of this system are: 1) It uses global algebraic reasoning through polynomial reconstruction. In the case-study, it uses the functional information of the design to reverse engineer the arithmetic expression as a linear sum and also uses a structural skeleton of the original data-path to achieve the equivalence proof. 2) It supports conditional rewriting and proves required
invariants as pre-conditions. 3) It uses recursive transformations that target making both sides of the miter logic structurally more similar and hence more amenable to bit-level SAT sweeping. 4) It has an open architecture, allowing new solver tech
niques to be integrated progressively.
Through a case study, we demonstrate the steps that were used to reconstruct the arithmetic embedded in a data-path design as a linear sum of signed integers, as well as all the procedures that compositionally led to a successful equivalence proof. The experimental results demonstrate the effectiveness of these collaborating procedures.
C. Overview
The overall tool flow is described in Section II. Learning techniques and system integration are presented in Section III and IV. A case study is presented in Section V. Experimental results is presented in Section VI followed by a comparison with related work and conclusion.
II. TOOL FLOW
LEC takes Verilog/VHDL as the input language for the datapath logic under comparison. Internally, a miter network, as in Figure 2(a), is constructed comparing combinational logic functions F and G. Figure 1 illustrates the overall tool flow.
First, the Verific RTL parser front-end[
new miter target Verific Parser Frontend
VeriABC SSA Network Bit−level
AIG ABC solvers SAT
UNSAT
Learning−based Transformations
Transformed
RTL Fig. 1. Overall tool flow
LEC tries to solve the miter directly using random
simulation on the word-level simulator or by ABC[1]’s equivalence
checking procedure dcec, which is a re-implementation of
iprove[
III. LEARNING TECHNIQUES
In this section, we present the techniques implemented in LEC. Even though some are simple and intuitive, they are powerful when integrated together as demonstrated in the experimental results. All techniques are essential bdecause LEC may not achieve a final proof if any one is omitted.
Their interactions are illustrated in the case-study in Section V.
F(x̄)
G(̄x)
F(x̄)
G(̄x)
F(x̄)
G(̄x) red blue red
blue miter F=G purple input :̄x (a)miter network
(b)structurally hashed Fig. 2. Miter network A. Structural information
An SSA netlist is a DAG of bit and word-level operators annotated with bit-width and sign information. In the tool flow, both Verific and VeriABC perform simple structural hashing at the SSA level, merging common sub-expressions. After merging, the miter logic is divided into three colored regions using cone of influence (COI) relations, as in Figure 2 (b).
Red: if the node is in the COI of F only Blue: if the node is in the COI of G only Purple: the node is in the COI of both sides of the miter i.e. common logic The purple region is the portion of the miter logic that has been proved equivalent already, while the red and blue regions are the unresolved ones. LEC makes progress by reducing the red/blue regions and increasing the purple region.
The common logic constrains the logic for the red and blue regions, which may be abstracted (see Section III-E) to reduce redundancy and possibly expose the real bottleneck in a proof.
B. Simulation model
Two word-level simulators are generated from the SSA network. One is a native interpreted model. The other uses the open-source Verilator[29] for compiled simulation. From the SSA network, LEC automatically generates C++ code for pseudo-random input drivers and for monitoring design behavior. Verilator compiles the Verilog miter logic, links in the generated C++ code and produces a simulator as a standalone executable. Efficient and effective simulation is crucial in our current flow in capturing potential constants and potential internal equivalent points at the SSA level. Simulation is also used to reduce common logic in the abstraction computation procedure.
C. Bit-level model
As shown in Figure 1, an AIG is created from the SSA network by bit-blasting. LEC calls ABC[1]’s SAT sweeping procedure dcec to perform direct solving at the bit level. Using the AIG model, the native SAT solver embedded in LEC can be used to obtain a formal proof for a particular query. Typical queries are for extracting constant nodes, proving suspected equivalent pairs of points or conducting particular learning for rewriting. Book-keeping information between the SSA nodes and the AIG nodes allows queries to be constructed at the word-level and verified at the bit-level. The result is then used to simplify the SSA network.
D. Constants and Potential Equivalent Points (PEPs)
At the word-level, candidates for constants and PEPs are identified through simulation and SAT queries are posed. Each such SAT query is constructed and checked at the bit-level.
SAT-solving is configured at a low-effort level (run for a few seconds) for these types of queries. Proven constants and PEPs are used immediately to simplify the SSA network, leading to a new sub-model of less complexity. LEC then continues to process the sub-model. In the presence of unproven PEPs, LEC can choose one as the next miter target, normally the smallest in terms of the number of nodes in its COI. The proof progresses as constants and PEPs are identified and used to simplify the miter model.
E. Abstraction
As illustrated in Figure 2 (c), in computing an abstraction, LEC computes a cut in the purple region (common logic), and removes the logic between the cut and the inputs. An abstract model is formed by replacing the cut signals with free inputs x0. If this abstracted miter is UNSAT, then the original miter is UNSAT. In our current implementation, LEC traverses the SSA network in topological order from the inputs. As each node is tentatively replaced with new PIs, simulation is used to validate the replacement. If successful, the node is omitted and replaced with the new PIs and the next node is processed similarly.
A successful abstraction step removes irrelevant logic and exposes a smaller unresolved region of the miter logic, allowing LEC to continue using other procedures. In addition, as seen from experimental results, the reduction of common logic can reduce significantly the amount of complexity for downstream SAT-solving, e.g. when common multipliers being removed from the miter logic. An unsuccessful abstraction when the abstract miter becomes SAT, indicates the existence of a rare event not being captured during random simulations.
Often, this gives hints for selecting case-splitting candidates.
F. Rewriting
Similar to [
If two multipliers from opposite sides of the miter are matched exactly, LEC can simplify the miter through structural hashing and treat them as common logic. This is most effective when combined with the abstraction procedure as the common multiplier can now be totally removed.
In LEC, a few rules are hard-coded through pattern matching applied to the SSA network. The goal is to process multiplications so that they can be matched exactly. This rewriting is implementation specific; for illustration purposes, we list a few rewriting rules in Table II using Verilog notation and the semantics of the operators.
The first rule is the normalization of multiplier operands. If a multiplier uses a partial product generator and a compressor tree, switching the operands of the multiplication becomes a very hard SAT problem because at the bit level the implementation is not symmetrical. It is almost imperative to apply this rule whenever possible. The second and third rules use the distributive laws of multiplication and multiplexing. Rules 4 and 5 remove the shift operator when it is used with extract and concat because it is hard for multiplication to be restructured through the operator. Rule 6 distributes multiplication through the concat of two bit vectors using +. It uses the fact that the concatenation fa; b[n 1 : 0]g is equivalent to a 2n + b[n 1 : 0].
The following is a more complex rule that distributes + over the extract operator. The right hand side is corrected with a third term, which is the carry bit from adding the lower n bits of a and b.
(a + b)[m : n] = a[m : n] + b[m : n] + (a[n 1 : 0] + b[n 1 : 0])[n] (1)
After implemented to trace back from the sel port of a mux node mux(condb; d0a c; d1 c) through its Boolean fanins and choose the candidates that have mux(cond; d0[m : n]; d1[m : n]) the highest controllability.
f (m-n)’b0, a[m:n] g Another advantage of case-splitting is that the co-factored
a[m : n] sub-models contain new candidates for constants and PEPs, a c n + b[n 1 : 0] c which lead to other down-stream transformations not possible before. Case-splitting also reduces the amount of Boolean logic in the SSA network and exposes the data-path logic to high-level learning such as polynomial construction.
Repeatedly applying the above rules, LEC transforms the SSA network and keeps only the and + operators, enhancing the possibility of multipliers to be matched. Note that the above rule (1) and Rule 4-6 in Table II are correct for unsigned operators. Currently, for signed operators, due to sign extension and the two’s complement representation of the operands, we have not implemented a good set of rewriting rules.
1) Conditional rewriting: The following equation (a c) b = (a b) c
(2) reduces the bit-width of a multiplier on the left hand side to a smaller one on the right. It is correct if a, b, c are integers but incorrect in Verilog semantics, which uses modulo integer arithmetic. However, if the following is true within the miter model in modulo integer semantics ( (a c) c) == a
(3) then equation (2) is valid. In such a situation, LEC identifies the pattern on the left hand side of (2) in the SSA network and executes a SAT query concerning (3) using the AIG model through bit-level solvers. The transformation to the left hand side of (2) is carried out only if the query is proven to be an invariant. Such a transformation may produce an exact match of a b afterwards, which can be crucial for achieving the final proof.
G. Case-split
Case-splitting on a binary signal, cofactors the original model into two sub-models. The miter is proven if both submodels are proven, or falsified if any sub-model is falsified. Although exponential in nature, if many signals are chosen, casesplitting can simplify the underlying bit-level SAT solving significantly. For example, it is difficult to prove the following miter structure directly through bit-blasting and SAT solving at the AIG level (x + y) (x + y) == x x + 2 x y + y y
(4) where x is a 32-bit integer and y a single binary signal.
However, it can be proven easily if case-splitting is done on y = 0 and y = 1. After constant propagation, the bit-level solver can prove both sub-models easily.
The current case-splitting mechanism supports cofactoring on an input bit or input bit-vector. In verifying the test cases experienced so far, the case splits are conducted on a bit, a bit-vector equal to zero or not, or on the lsb or msb of a bit-vector equals to zero or not. A heuristic procedure can be H. Polynomial construction
Reasoning at the word-level, rewriting rules are based on the arithmetic properties of the corresponding operators such as the commutative law of integer multiplication. However, rewriting applies only local transformations and does not have a global view. In situations when the miter logic is constructed from arithmetic optimization at the polynomial level, local rewriting is not able to bring similarity into the miter for further simplification. In such a situation, LEC tries to reconstruct the polynomial of the whole miter model to establish equivalence through arithmetic or algebraic equivalences and then use high level transformations to prove the equivalence of the original miter.
As a generic procedure, LEC follows four steps to prove a miter network F (x) = G(x) where F and G are the top level signals being compared, and x is the vector of input variables (bit-vectors): 1) Conjecture (possibly by design knowledge) about the algebraic domain of the polynomial, e.g. signed vs. unsigned integer, modulo integer arithmetic, the order of the polynomial etc. These conjectures set up the framework and semantics for polynomial reconstruction as illustrated in the case-study of Section V. 2) Determine a polynomial f and create a logic network
F 0 such that the following can be proved formally.
How f is constructed is domain and test-case dependent.
In the case-study of Section V, we use simulation patterns to probe for the coefficients of a linear function. 3) Determine a polynomial g and create a logic network
G0 such that the following can be proved formally.
F 0 implements f miter
F 0 = F G0 implements g miter
G0 = G f = g (5) (6) (7) (8) (9) 4) Establish the following equivalence formally at the al
gebraic level.
The combination of Items 2, 3, and 4 establishes the equivalence proof of the original miter model F = G. In constructing F 0 and G0, we try to make them as structurally similar to F and G as possible. Details are given in Section V.
IV. SYSTEM INTEGRATION
The above learning techniques are integrated in LEC as a set of logically independent procedures. Each procedure produces one or more sub-models, illustrated as a tree in Figure 3.
The root node is the current targeted Verilog miter model.
It has eight children. The simulator and AIG models are the ones described in Figure 1. The simplif ied sub-model is generated by constant propagation and merging proven PEPs.
The abstraction and rewrite sub-models are created by the abstraction and rewrite procedures in the previous section.
The case-split sub-model consists of a set of sub-models, corresponding to the cofactoring variables selected. In the current implementation, the user needs to input the set of signals to case-split on; eventually they will be selected by heuristics. The linear-construction node has two sub-models which will be explained in detail in Section V. When PEPs are identified through simulation, a P EP node is create with the set of unproven-PEPs as sub-models.
Verilog Miter Model simulator AIG simplified abstraction rewrite case-split linear-construction PEP pep0 pep1 ... pepm case0 case1 ... casen caseF caseG
LEC Fig. 3. Branching sub-model tree
Two nodes in the sub-model tree are terminal. One is the simulator model which can falsify the miter through random simulation. The other is the AIG model where ABC’s bit-level dcec procedure is applied. The rest of the leaf models (in bold font) are generated as Verilog miter models, which have the same format as the root node. LEC procedures can be applied recursively to these leaf nodes to extend the sub-model trees to simpler ones. The LEC proof process progresses by expanding the sub-model tree. A sub-model is resolved as SAT or UNSAT from its sub-models’ proof results.
Since there are no logical dependencies between sibling sub-models, any branch can be chosen to continue the proof process. Sibling sub-models can be forked in parallel from a parent process. A node in the sub-model tree determines its proof result from its children. Table III gives the possible return values from the first level sub-models. SIMPLIFY is returned by a P EP node to its parent model when at least one of its sub-models, pepi, is proven UNSAT, notifying the parent node to simplify further with the newly proved pepi.
Depending on the logical relationships between a parent and its immediate sub-models, a node is either disjunctive or conjunctive in semantics. In Figure 3, a Verilog miter model node Sub-model simulator
AIG simplified abstraction rewrite case-split linear construction
PEP
Return
SAT SAT/UNSAT SAT/UNSAT
UNSAT SAT/UNSAT SAT/UNSAT SAT/UNSAT
SIMPLIFY is disjunctive, which includes the root and all the leaf nodes in bold font. The case-split and linear construction nodes are conjunctive; a P EP node is disjunctive. The semantics, shown in the following tables, are used to resolve the proof result of the parent model from its immediate sub-models. To complete the calculus, we introduced two values: CON and BOT, where CON stands for an internal conflict indicating a potential LEC software bug and BOT is the bottom of the value lattice and acts like an uninitialized value.
Tables IV and V are the truth tables for the disjunction and conjunction semantics of the return values, in which UNS, UNK, SMP stand for UNSAT, UNKNOWN, and SIMPLIFY.
Assuming a bug free situation, at a disjunctive node, if either SAT or UNSAT is returned from a sub-model, this is the final proof result for the parent. In conjunction, the parent must wait until all sub-models are resolved as UNSAT before deciding that its result is UNSAT, while any SAT sub-model implies the current model is SAT. A P EP node returns SIMPLIFY to its parent if one of its sub-models, say pepi, is proven UNSAT. In this case, the parent model can apply another round of simplification to obtain a new simplif ied sub-model by merging the node pair in the just-proved pepi. The proof log in Figure VI is a sample sub-model tree where only the branches that contributed to the final proof are shown. Indentation indicates the parent-child relationship. Recursively, the proof result of the top level target is evaluated as UNSAT. "case split": { "case_0": "UNSAT by AIG" "case_1": { "simplified": { "abstraction": { "case split": { "case_00": "UNSAT by AIG", "case_01": "UNSAT by AIG", "case_10": "UNSAT by AIG", "case_11": "UNSAT by AIG" },
}, }, },
}, } ------------------------------------Miter proof result: [Resolved: UNSAT] ------------------------------------Fig. 4. Illustration of proof log
Using this sub-model tree infrastructure, any new procedures discovered in the future can be plugged into the system easily. Also, the system is fully parallelizable in that siblings can be executed at the same time. The proof process can be retrieved from the expanded sub-model tree.
V. CASE STUDY three numbers on the right are the node counts in the red, blue and purple regions (common logic) of the SSA network as distinguished in Figure 2(a). Only those sub-models that contributed to the final proof are shown in the figure. Others are ignored. As seen in Figure 5, the case-split procedure is
The design in this case-study is an industrial example taken applied twice, at lines 2 and 9. Both models have a singlefrom the image processing domain. We verify specification bit input port, which was selected for cofactoring. ABC[1] = implementation where the “specification” is a manually- immediately proved the first cofactored case, case 0 (3 and specified high-level description of the design. “Implemen- 10) , using the AIG model at 4 and 11. The time-out for the tation” is a machine-generated and highly optimized RTL dcec run was set to two seconds. Abstraction was applied at 8, implementation of the same design using[2]. The miter logic significantly reducing the common logic from 675 to 29 SSA is obtained through SLEC[3]. Therefore, the miter problem nodes, and effectively removing all the comparator logic. We is verifying that the high-level synthesis (HLS) tool did not tried abstraction on the original model without the case-split modify the design behavior. procedure and it failed to produce any result. The case-split at
This miter is sequential in nature, but here we examine a 2 removed enough Boolean logic and eliminated some corner bounded model checking (BMC) problem which checks the cases such that the abstraction procedure was able to produce correctness of the implementation at cycle N. This renders the an abstract model successfully. problem combinational. This is industrially relevant because Model 15 is the smallest unproved PEP from model 13. the sequential problem is too hard to solve in general, and It is proved using the linear construction procedure at 16, even the BMC problem at cycle N becomes too difficult for which we shall describe in detail in Section V-A. Model industrial tools. 21 is the simplified model of model 13 after merging the
The original design (specification) consists of 150 lines just-proved pep0. After simplification, most of the logic in of C++. It went through the Calypto frontend[3] and was model 21 became common logic through structural hashing, synthesized into a word-level netlist in Verilog. The generated leaving only 10 nodes in each of the blue and red regions. miter model has 1090 lines of structural Verilog code with 36 Model 21 was proved quickly by ABC which concludes the input ports: 29 of which are 7 bits wide, 2 are 9 bits, 4 are proof of the original miter. In this case, the linear-construction 28 bits and one is a single-bit wire. The miter is comparing procedure was crucial in attaining the proof. However, the two 28-bit values. We do not have knowledge about what the case-split, simplification, abstraction, and PEP models also are design does except through structural statistics: no multipliers, very important because they collaborate in removing Boolean, many adders, subtractors, comparators, shifters etc., together mux and comparator logic etc, but keeping only the part of the with Boolean logic. From a schematic produced from the original miter logic which constitutes a linear function. Only Verilog, there seems to be a sorting network implemented at this point, can a proof by the linear construction procedure using comparators, but we can not tell anything further. succeed.
Figure 5 illustrates the compositional proof produced by the LEC system by showing the sub-model tree created during A. Linear construction the proof process. Indentations indicate parent and sub-model For model 15 in Figure 5, the SSA network contains many relations and are listed in the order they were created. The +, , and operators along with extract and concat operators, but contains no Boolean operators or muxes. The input ports consist of twenty-five 7-bit or 12-bit wide ports. The miter is comparing two 15-bit wide output ports. At this point, simplification and abstraction can not simplify the model further. Also, there are no good candidates for case-splitting.
The local rewriting rules can not be applied effectively without having some global information to help converge the two sides of the miter logic. High-level information must be extracted and applied to prove this miter model.
After the linear construction procedure through LEC, the miter logic is found to be implementing the following linear sum in the signed integer domain using two’s complement representation: 16 x0 + 2 +2 x1 + 2 x6 + 2 x2 + 2 x7 + 2 x3 + 2 x7 + 2 +2 x10 + x11 + x12 + 2
x13 + 2 +2 x16 + 2 x17 + 2 x18 + 2 x19 2 x4 + 2 x8 + 2 x14 + 2 x20 + 2 x5 x9 x15 x21 +2 x22 + 2 x23 + 2
x24 + 14 One side of the miter implements the above sum as a plain linear adder chain (Figure 6(a)), the other side is a highly optimized implementation using a balanced binary tree structure (Figure 6(b)) and optimization tricks, which we don’t fully understand. This is a hard problem for bit-level engines because
...
(a)linear adder chain Fig. 6. Addition implementation
...
(b) balanced adder tree there are no internal match points to utilize. Therefore, LEC resorts to trying a high-level method to establish equivalence at the polynomial level. The following are the detailed steps for this specific case.
1) The conjecture: Assume the miter logic is F (x) = G(x) as in Figure 2(a). LEC conjectures the following for the arithmetic domain.
Signed integer arithmetic. The numbers are in 2’s complement representation.
Assume F (x) and G(x) are implementing the linear sums f and g of the forms f (x) = X ai xi + b g(x) = X a0i xi + b0 2) Determining the coefficients of f , g and proving f = g algebraically: Given the data-path logic F (x) and the linear sum formula (10), it takes n + 1 simulation patterns on the n input variables to compute the coefficients:
b = F (0; 0; :::; 0) a0 = F (1; 0; :::; 0) a1 = F (0; 1; :::; 0) ::: an 1 = F (0; 0; :::; 1) b b b Another round of random simulation on both the logic and the polynomial can be done to increase the likelihood of the conjecture. The same is repeated for G(x) to obtain g(x).
In integer arithmetic, f is equal to g if and only if the coefficients match exactly for each term: f = g <=> 8 i ai = a0 i and b = b0
(12)
So checking of f = g is trivial in this case. In other algebraic
domains, domain specific reasoning may have to be applied
to derive algebraic equivalence e.g. in [
3) Synthesizing implementations F 0=G0 for f (f =g), structurally similar to F =G: We want to find a Verilog implementation F 0(x) of f such that 1) F 0 implements f 2) F 0 is structurally similar to F To do this, all nodes in the SSA network with arithmetic operators +, are marked, and edges connecting single bits are removed. A reduced graph is then created from the marked nodes in the remaining graph maintaining the input/output relations between marked nodes. This graph is a skeleton of the implementation structure of F . For each of its nodes, we annotate it with a conjectured linear sum computed in the same way as in the above steps. The root node F is annotated with f and internal nodes annotated with linear sums fs, ft, etc. For illustration purposes, Figure 7(a) shows such an annotated reduced graph for node w. For an arbitrary node w
w=f w(̄x) s=f s(̄x) + u=...
+ + +
v=... + t=f t(̄x ) x ̄ (a)annotated reduced graph Fig. 7. Annotated reduced graph
u=... w=cs⋅s+ct⋅t + f st (̄x)
+ s=... t=...
+ + +
+ v=... x ̄ (b) substituted annotation in the reduced graph with inputs from nodes s and t, from the annotation we have the following: s = fs(x) t = ft(x) w = fw(x) (10) (11)
We would like to substitute fw with variable s and t, such that w is a function of s and t in order to follow the structure of the skeleton reduced graph. Because all the functions are linear sums, we can compute, using algebraic division, two constants cs and ct such that the following holds: w = cs s + ct t + fst(x)
Given a l -term (UF symbol) f and a corresponding hash table r( f ). Rule I, the initialization rule, initializes r( f ) with all non-parameterized function applications on f . Rule C corresponds to the function congruence axiom and is applied whenever we add a function application g(a0; : : : ; an) to r( f ). Rule B is a consistency check w.r.t. the current assignment s , i.e., for every function application s in r( f ), we check if the assignment of s (al (s)) corresponds to the assignment evaluated by the partially b -reduced term lx¯[x0na0; : : : ; xnnan]p. Finally, rule P represents a crucial optimization of consistentl , as it avoids unnecessary conflicts while checking B. If P applies, both function applications s and t have the same arguments.
As function application s 2 r(lx¯), rule C implies that s = lx¯(a0; : : : ; an). Therefore, function applications s and t must produce the same function value as t := lx¯[x0na0; : : : ; xnnan]p = ly¯[x0na0; : : : ; xnnan]p, i.e., function application t must be equal to the result of applying partial b -reduction to function application s.
Assume we encode t and add it to the formula. If DPB guesses an assignment s.t. s (al (t)) 6= s (al (s)) holds, we have a conflict and need to add a lemma. However, this conflict is unnecessary, as we know from the start that both function applications must map to the same function value in order to be consistent. We avoid this conflict by propagating s to r(g).
Figure 6 illustrates our consistency checking algorithm consistentl , which takes the preprocessed input formula p and a current assignment s as arguments, and proceeds as follows. First, we initialize stack S with all non-parameterized function applications in formula p (cf. nonparam_apps(p)) and order them top-down, according to their appearance in the DAG representation of p. The top-most function application then represents the top of stack S, which consists of tuples (g; f (a0; : : : ; an)), where f and g are initially equal and f (a0; : : : ; an) denotes the function application propagated to function g. In the main consistency checking procedure consistentl (p; s )
S nonparam_apps ( p ) w h i l(eg;Sf6 =(a00/; : : : ; an)) pop ( S ) encode ( f (a0; : : : ; an) ) / c h e c k r u l e C / i f not congruent ( g; f (a0; : : : ; an) )
r e t u r n ? add ( f (a0; : : : ; an); r(g) ) i f is_UF ( g ) c o n t i n u e encode ( g ) / c h e c k r u l e B / t g[x0na0; : : : ; xnnan]p i f assigned ( t )
i f s (t) 6= s (al ( f (a0; : : : ; an))) e l i f t = hr(ae0t;u: :r:n; an?) / c h e c k r u l e P / push ( S; (h; f (a0; : : : ; an)) ) c o n t i n u e e l s e apps f resh apps(t) f o r a 2 apps
encode ( a ) i f eval ( t ) 6= s (al ( f (a0; : : : ; an)))
r e t u r n ? f o r h(b0; : : : ; bm) 2 apps
push ( S; (h; h(b0; : : : ; bm)) ) r e t u r n >
Fig. 6: Procedure consistentl in pseudo-code. loop, we check rules C and B for each tuple as follows.
First we check if f (a0; : : : ; an) violates the function congruence axiom EUF w.r.t. function g and return ? if this is the case. Note that for checking rule C, we require an assignment for arguments a0; : : : ; an, hence we encode them on-the-fly. If rule C is not violated and function f is an uninterpreted function, we continue to check the next tuple on stack S. However, if f is a l -term we still need to check rule B, i.e., we need to check if the assignment s (al ( f (a0; : : : ; an))) is consistent with the value produced by g[x0na0; : : : ; xnnan]p. Therefore, we first encode all non-parameterized expressions in the scope of partial b -reduction bp(g) (cf. encode(g)) before applying partial b -reduction with arguments a0; : : : ; an, which yields term t. If term t has an assignment, we can immediately check if it differs from assignment s (al ( f (a0; : : : ; an))) and return ? if this is the case. However, if term t does not have an assignment, which is the case when t has been instantiated from a parameterized expression, we have to compute the value for term t. Note that we could also encode term t to get an assignment s (t), but this might add a considerable amount of superfluous clauses to the SAT solver. Before computing a value for t we check if rule P applies and propagate f (a0; : : : ; an) to h if applicable.
Otherwise, we need to compute a value for t and check if t contains any function applications that were instantiated and not yet encoded (cf. fresh_apps(t)) and encode them if necessary. Finally, we compute the value for t (cf. eval(t)) and compare it to the we run DPB on al (y1) and it returns a satisfying assignment of al ( f (a0; : : : ; an)). If the values differ, assignment s such that s (i) 6= s ( j), s (ai) = s (a j), we found an inconsistency and return ?. Otherwise, s (i) < 0 and s (ai) 6= s ( i). First, we check conwe continue consistency checking the newly encoded sistency for lx(i) and check rule C, which is not function applications apps. We conclude with >, if all rvuiolelaBte.dWase sap(pi)ly6=psar(tija)l, ban-rdedcuocnttiionnueanwditohbtcahinectkeirnmg function applications have been checked successfully t := lx[x=i]p = ly(i) (since s (i) < 0) for which rule P and no inconsistencies have been found. is applicable. We propagate lx(i) to ly, check if lx(i) is consistent w.r.t. ly, apply partial b -reduction, obtain A. Lemma generation t := ly[y=i]p = i and find an inconsistency according proFcoeldlouwreinlgem[m3]a,l ,wwehiicnhtrogdenuecreataes lae msymmabogleicnelermatimona ttsoh(atruiiln)e. tWhBe:ensgeex(nateii)rtae6=treatslieo(mn mDi)aBbPiu<rtetw0uer!nsoabaita=nienwedis.asAti(ssafsyiu)imn=ge whenever our consistency checker detects an inconsis- assignment s such that s (i) 6= s ( j), s (ai) = s (a j), tency. Depending on whether rule C or B was violated, s (i) < 0, s (ai) = s ( i) and s ( j) > s ( i). We first we generate a symbolic lemma as follows. Assume check consistency for lx(i), which is consistent due to that rule C was violated by function applications s := the lemma we previously generated. Next, we check g(a0; : : : ; an); t := h(b0; : : : ; bn) 2 r( f ). We first collect rule C for lx( j), which is not violated since s (i) 6= all conditions that lead to the conflict as follows. s ( j), and continue with checking rule B. We apply 1) Find the shortest possible propagation path ps (pt ) (psairntciael sb(-jr)ed>ucsti(oni)anadndosbt(aii)n<te0r)mantd:=finldx[axn= ji]npc=on-j from function application s (t) to function f . sistency as s (ai) = s ( i), s (ai) = s (a j) and s ( j) > 2) Collect all ite conditions cs0; : : : ; csj (ct0; : : : ; ctl) on s ( i), but s (a j) = s ( j). We then generate lemma path ps (pt ) that were > under given assignment s . j > 0 ! a j = j. 3) Collect all ite conditions cs0; : : : ; csk (ct0; : : : ; ctm) on
path ps (pt ) that were ? under given assignment s . VIII. EXPERIMENTS We generate the following (in general symbolic) lemma: j k ^ cis ^ ^ i=0 i=0
l m :cis ^ ^ cti ^ ^ i=0 i=0
n :cti ^ ^ ai = bi ! s = t
i=0
Assume that rule B was violated by a function application s := ly¯(a0; : : : ; an) 2 r(lx¯). We obtained t := lx¯[x0na0; : : : ; xnnan]p and collect all conditions that lead to the conflict as follows. 1) Collect ite conditions cs0; : : : ; csj and cs0; : : : ; csk for s
as in steps 1-3 above. 2) Collect all ite conditions ct0; : : : ; ctl that evaluated to > under current assignment s when partially b reducing lx¯ to obtain t. 3) Collect all ite conditions ct0; : : : ; ctm that evaluated to ? under current assignment s when partially b reducing lx¯ to obtain t.
We generate the following (in general symbolic) lemma: j
k ^ cis ^ ^ i=0 i=0
l m :cis ^ ^ cti ^ ^ :cti ! s = t
i=0 i=0
Example 5: Consider formula y1 and its preprocessed formula abstraction al (y1) from Ex. 1. For the sake of better readability, we will use lx and ly to denote functions f and g, and further use ai and a j as a shorthand for al (applyi) and al (applyj). Assume
We applied our lemmas on demand approach for l -terms on three different benchmark categories: (1) crafted, (2) SMT’12, and (3) application. For the crafted category, we generated benchmarks using SMT-LIB v2 macros, where the instances of the first benchmark set (macro blow-up) tend to blow up in formula size if SMT-LIB v2 macros are treated as C-style macros.
The benchmark sets fisher-yates SAT and fisher-yates
UNSAT encode an incorrect and correct but naive
implementation of the Fisher-Yates shuffle algorithm [
We performed all experiments on 2.83GHz Intel Core
2 Quad machines with 8GB of memory running Ubuntu
12.04.2 setting a memory limit of 7GB and a time limit
for the crafted and the SMT’12 benchmarks of 1200
seconds. For the application benchmarks, as in [
Boolector tse BBoooolleeccttoorrnbop -raeyh STA CVC4 sfi SMOaNthOSALTAR
Z3
Boolector s Boolectornop t-eay STA BCoVoCle4ctorb r seh UN SMOaNthOSALTAR fi
Z3 we used a time limit of 60 seconds. We evaluated four different versions of Boolector: (1) our lemmas on demand for l -terms approach DPl (Boolector), (2) DPl without optimization rule P (Boolectornop), (3) DPl with full b -reduction (Boolectorb ), and (4) the version submitted to the SMT competition 2012 (Boolectorsc12). For comparison we used the following SMT solvers: CVC4 1.2, MathSAT 5.2.6, SONOLAR 2013-05-15, STP 1673 (svn revision), and Z3 4.3.1.
Note that we limited the set of solvers to those which currently support SMT-LIB v2 macros and the theory of fixed-size bit vectors. As a consequence, we did not compare our approach to UCLID (no bit vector support) and Yices, which both have native l -term support, but lack support for the SMT-LIB v2 standard.
As indicated in Tables I, II and III, we measured the number of solved instances (Solved), timeouts (TO), memory outs (MO), total CPU time (Time), and total memory consumption (Space) required by each solver for solving an instance. If a solver ran into a timeout, 1200 seconds (60 seconds for category application) were added to the total time as a penalty. In case of a memory out, 1200 seconds (60 seconds for application) and 7GB were added to the total CPU time and total memory consumption, respectively. mark set is SONOLAR. However, it is not clear how SONOLAR handles SMT-LIB v2 macros. Surprisingly, on these benchmarks Boolectornop performs better than Boolector with optimization rule P, which needs further investigation. On the fisher-yates SAT benchmarks Boolector not only solves the most instances, but requires 107 seconds for the first 6 instances, for which Boolectorb , MathSAT and Z3 need more than 300 seconds each. Boolectornop does not perform as well as Boolector due to the fact that on these benchmarks optimization rule P is heavily applied. In fact, on these benchmarks, rule P applies to approx. 90% of all propagated function applications on average. On the fisheryates UNSAT benchmarks Z3 and Boolectorb solve the most instances, whereas Boolector and Boolectornop do not perform so well. This is mostly due to the fact that these benchmarks can be simplified significantly when macros are eagerly eliminated, whereas partial b -reduction does not yield as much simplifications.
We measured overhead of b -reduction in Boolector on these benchmarks and it turned out that for the macro blow-up and fisher-yates UNSAT instances the overhead is negligible (max. 3% of total run time), whereas for the fisher-yates SAT instances b -reduction requires over 50% of total run time.
Table II summarizes the results of running all four Boolector versions on the SMT’12 benchmark set. We compared our three approaches Boolector, Boolectornop, and Boolectorb to Boolectorsc12, which won the QF AUFBV track in the SMT competition 2012. In comparison to Boolectorb , Boolector solves 5 unique instances, whereas Boolectorb solves 3 unique instances. In comparison to Boolectorsc12, both solvers combined solve 2 unique instances. Overall, on the SMT’12 benchmarks Boolectorsc12 still outperforms the other approaches. However, our results still look promising since none of the approaches Boolector, Boolectornop and Boolectorb are heavily optimized yet.
On these benchmarks, the overhead of b -reduction in Boolector is around 7% of the total run time. 37 35 44 39 44 37 35 45 n Boolector tio Boolectornop tia Boolectorb ta Boolectorsc12 n in STP s
Boolector
a Boolectornop
bd Boolectorb
new approaches to STP, the same version of the solver
that outperformed all other solvers on these benchmarks
in the experimental evaluation of [
Boolectorsc12 and STP do not support l -terms as arrays and therefore were not able to participate on this benchmark set. By exploiting the native l -term support for arrays in Boolectorb , in comparison to the instantiation benchmarks we achieve even better results. Note that on the lambda (instantiation) benchmarks, the overhead in Boolectorb for applying full b -reduction was around 15% (less than 2%) of the total run time.
Benchmarks, binaries of Boolector and all log files of our experiments can be found at: http://fmv.jku.at/
IX. CONCLUSION
In this paper, we introduced a new decision procedure for handling non-recursive and non-extensional l -terms as a generalization of the array decision procedure presented in [3]. We showed how arrays, array operations and SMT-LIB v2 macros are represented in Boolector and evaluated our new approach with 3 different benchmark categories: crafted, SMT’12 and application. The crafted category showed the benefit of lazily handling SMT-LIB v2 macros where eager macro elimination tends to blow-up the formula in size.
We further compared our new implementation to the version of Boolector that won the QF AUFBV track 0 0 0 0 0 0 0 0
Time [s] 576 673 138 535 141 594 709 52
Space [MB] 235 196 961 308 3814 236 166 676 in the SMT competition 2012. With the application benchmarks, we demonstrated the potential of native l -term support within an SMT solver. Our experiments look promising even though we employ a rather naive implementation of b -reduction in Boolector and also do not incorporate any l -term specific rewriting rules except full b -reduction.
In future work we will address the performance bottleneck of the b -reduction implementation and will further add l -term specific rewriting rules. We will analyze the impact of various b -reduction strategies on our lemmas on demand procedure and will further add support for extensionality over l -terms. Finally, with the recent and ongoing discussion within the SMT-LIB community to add support for recursive functions, we consider extending our approach to recursive l -terms.
X. ACKNOWLEDGEMENTS
We would like to thank Stephan Falke, Florian Merz and Carsten Sinz for sharing benchmarks and Bruno Duterte for explaining the implementation and limits of lambdas in SMT solvers, and more specifically in Yices. CHIMP: a Tool for Assertion-Based Dynamic
Verification of SystemC Models Sonali Dutta
Rice University Email:Sonali.Dutta@rice.edu
Deian Tabakov
Schlumberger Email:deian@dtabakov.com
Moshe Y. Vardi
Rice University Email:vardi@cs.rice.edu
Abstract—CHIMP is a tool for assertion-based dynamic verification of SystemC models. The various features of CHIMP include automatic generation of monitors from temporal assertions, automatic instrumentation of the model-under-verification (MUV), and three-way communication among the MUV, the generated monitors, and the SystemC simulation kernel during the monitored execution of the instrumented MUV. Empirical results show that CHIMP puts minimal runtime overhead on the monitored execution of the MUV.
A newly added path in CHIMP results in a significant (over 75%) reduction of average monitor generation and compilation time. The average size of the monitors is reduced by over 60%, without increasing runtime overhead.
SystemC (IEEE Standard 1666-2005) has emerged as a de facto standard for modeling of hardware/software systems [4], supporting different levels of abstraction, iterative model refinement, and execution of the model during each design stage. SystemC is implemented as a C++ library with macros and base classes for modeling processes, modules, channels, signals, ports, and the like, while an event-driven simulation kernel allows efficient simulation of concurrent models. Thus, on one hand, SystemC leverages the natural object-oriented encapsulation, data hiding, and well-defined inheritance mechanism of C++, and, on the other hand, it allows modeling and efficient simulation of hardware/software designs by its simulation kernel and predefined hardwarespecific macros and classes. The SystemC code is available as open source, including a single-core reference simulation kernel, referred to as the OSCI kernel; see http://www.accellera.org/downloads/standards/systemc.
Work supported in part by NSF grants CNS 1049862 and CCF1139011, by NSF Expeditions in Computing project ”ExCAPE: Expeditions in Computer Augmented Program Engineering”, by BSF grant 9800096, and by gift from Intel.
The growing popularity of SystemC has motivated
research aimed at assertion-based dynamic verification
(ABDV) of SystemC models [
The monitors observe the execution of the MUV and
report if the observed behavior is consistent with the
specified behavior. For discussion of related work in
ABDV of SystemC see [
CHIMP, available as an open-source tool1,
implements the monitoring framework for temporal SystemC
properties described in [
CHIMP takes the MUV and a set of temporal
assertions about the behavior of that MUV as inputs,
1www.sourceforge.net/projects/chimp-rice
Fig. 1. CHIMP components
and outputs “FAILED” or “NOT FAILED”, for each
assertion. CHIMP performs white-box validation of user
code and black-box validation of library code. (If a user
wishes to do white-box validation of library code, it can
be accomplished by treating the library code as part of
the user code.) The two main features of CHIMP are: (1)
CHIMP generates C++ monitors, one for each assertion
to be verified, and (2) CHIMP automatically instruments
the user model [
A recently added path in CHIMP from LTL to monitor can bypass the old performance bottleneck, Automaton-1.1, and improves the monitor generation and compilation time by a significant amount. It also reduces the size of the generated monitors notably. This entirely removes the dependency of CHIMP on Automaton-1.1.
The theoretical and algorithmic foundations of
CHIMP were described in [
Section IV describes the C++ monitor generated by CHIMP. Section V describes the new improved path in CHIMP and its improved performance. Finally, Section VI presents a summary and talks about future work.
ASSERTIONS: SYNTAX AND SEMANTICS
CHIMP accepts input assertions, defined using the
temporal specification framework for SystemC described
in [
Several of the additional Boolean variables
proposed in [
CHIMP is also able to sample the execution at various key locations, e.g., function calls and function returns.
This gives the user the flexibility to write assertions at different levels of abstraction, from the level of individual C++ statements to the level of SystemC kernel phases.
The Boolean primitives supported by CHIMP are
summarized below; see, [
Function primitives: Let f() be a C++ function in the user or library code. The Boolean primitives f:call and f:return refer to locations in the source code that contain the function call, and to locations immediately after the function call, respectively. The primitives f:entry and f:exit refer to the locations immediately before the first executable statement and immediately after the last executable statement in f(), respectively. If f() is a library function then the entry and exit primitives are not supported (black-box verification model for libraries).
Value primitives: If a function f() has k arguments, CHIMP defines variables f : 1; : : : ; f : k, where the value and type of f : i are equal to the value and type of the ith parameter of function f() before executing the first statement in the definition of f(). CHIMP also defines the variable f : 0, whose value and type are equal to the value and type of the object that f() returns. For example, if the function int divide(int dividend, int divisor) is defined in the MUV, then the formula G (division:entry -> “division:2 != 0”) asserts that the divisor is nonzero whenever division function starts execution.
Phase primitives: The user can refer to the 18
predefined kernel states [
Event primitives: For each SystemC event E, CHIMP provides a Boolean primitive E.notified that is true only when the OSCI kernel actually notifies E. For example, the assertion G (s.value changed event().notified) @MON UPDATE PHASE END says that the signal s changes value at the end of every update phase.
USAGE, IMPLEMENTATION AND PERFORMANCE
Running CHIMP consists of three steps: (1) In the first step, the user writes a configuration file containing all assertions to be verified, as well as other necessary information. The user can also provide inputs through command-line switches. For each LTL assertion in the configuration file, MONASGEN first generates a nondeterministic Bu¨chi automaton on words (NBW) using SPOT, then converts that NBW to a minimal deterministic finite automaton on words (DFW), using the Automaton-1.11 tool for determinization and minimization. Then, MONASGEN generates the C++ monitors from the DFW, one monitor for each assertion (Fig. 2). (2) MONASGEN produces an aspect-advice file that is then used by AspectC++ to generate the instrumented MUV (Fig. 3). (3) Finally, the monitors and the instrumented MUV are compiled together and linked to the patched OSCI kernel, and the code is then run to execute the simulation with inputs provided by user. The inputs can be generated using any standard stimuli-generation technique. For every assertion, CHIMP produces output indicating if the assertion held or failed for that particular input (Fig. 4).
For experimental evaluation we used a SystemC model with about 3,000 LOC, implementing a system for reserving and purchasing airplane tickets. The users Fig. 2. Monitor generation flow Fig. 3. MUV instrumentation flow of the system submit requests and the system uses a randomly generated flight database to find a direct flight or a sequence of up to three connecting flights. Those are returned to the user for approval, payment and booking.
This model is intended to run forever. It is inspired by actual request/grant subsystems currently used in hardware design.
We used a patched version of the 2.2.0 OSCI kernel and compiled it using the default settings in the Makefile.
The empirical results below were measured on a Pentium
4, 3.20GHz CPU, 1 GB RAM machine running GNU
Fig. 4. Running instrumented MUV with monitors using patched
OSCI kernel
Linux. To assess runtime overhead imposed by the
monitors, we measured the effect of running with different
assertions and also increasing number of assertions [
In each case we first ran the model without monitors and user-code instrumentation to establish the baseline, and then ran several simulations with instrumentation and an increasing number of copies of the same monitor. The results report runtime overhead per monitor as a percentage of the baseline. (For these experiments monitors were constructed manually.)
The first property we checked is a safety property asserting that whenever the event new requests nonfull is notified, the corresponding queue new planning requests must have space for at least one request.
G "new_planning_requests.size() < capacity" @ new_requests_nonfull.notified
The second property says that the system must propagate each request through each channel (or through each module) within 5 cycles of the slow clock. This property is a conjunction of 16 bounded liveness assertions similar to the one shown here. ... // Propagate through module within 5 clock ticks ALWAYS (io_module_receive_transaction($1) -> ( within [5 slow_clock.pos()]
io_module_send_to_master($2) & ($1 == $2) ) AND ...
Fig. 5 presents the runtime overhead of monitoring (1) (2) 2 x 10−4 ll1.8 a c r1.6 e p d1.4 a e rh1.2 e v o 1 e tag0.8 n ce0.6 r e P0.4
Property 1 (safety) Property 2 (liveness)
Both properties 102 Number of monitors
103 Fig. 5. Run time overhead for monitoring Properties (1) and (2)
1.5 2 2.5 3 Number of monitor calls 3.5
4.5 x 105 Fig. 6. Instrumentation overhead per monitor call as a percentage of the baseline run time. Y axis is ((instrumentation overhead baseline)=(baseline number of monitors)) 100% the above two properties as a percentage of the baseline.
Checking Property 2 is relatively expensive because it requires a lot of communication from the model to the monitor. It is shown in [1] that the finite state monitors have less runtime overhead than transaction-based monitors generated by tools like Synopsys VCS.
We also evaluated the cost of instrumentation
separately by simulating one million SystemC clock cycles
with focus on the overhead of instrumentation [
Another testbench we used is an Adder model that implements the squaring function by repeated increment by 1. It uses all three kinds of event notifications. It is scalable as it spawns a SystemC thread for each addition in the squaring function. We monitored several properties of the Adder model using CHIMP.
To study the effect of monitor encoding on runtime
overhead, Tabakov and Vardi [
IV. CHIMP MONITORS
In CHIMP, the LT L f ormula in every assertion hLT L f ormulai @ hclock expressioni is converted into a C++ monitor class. Each C++ monitor has a step() function that implements the transition function of the DFW generated from the LT L f ormula (as described in Fig. 9). This step() function is called at every sampling point defined by clock expression. The monitor.h and monitor.cc files, generated by MONASGEN, contains one monitor class for every assertion and a class called local_observer that is responsible for invoking the callback function, which invokes step() function of the appropriate monitor class at the right sampling point during the monitored simulation. Different encodings have been explored for writing the monitor’s step() function. For the new flow of CHIMP (described below), Fig. 13 shows that front det ifelse encoding is the best among all of them in terms of runtime overhead.
In front det ifelse encoding, the C++ monitor produced is deterministic in terms of transitions. This means from one state, either one or no transition is possible. If no transition is possible from a state, the monitor rejects and outputs ”FAILED”. Else, the monitor keeps executing until the end of simulation and outputs ”NOT FAILED”.
In front det ifelse encoding, each state of the monitor is encoded as an integer, from 0 upto the total number of states. The step() function of the monitor uses an outer if-elseif statement block to determine the next state. The Fig. 7. The DFW generated by MONASGEN from the LTL formula G(a ! Xb). All the states are accepting. The DFW rejects bad prefixes by no available transition. State 0 is the initial state. possible transitions from each state are encoded using an inner if-elseif block, the condition statement being the guard on a transition.
As a running example, we show how the monitor step() function is encoded for an assertion G(a ! Xb) @ clk. clk here is some boolean expression specifying when the step() function needs to be called during the simulation.
This assertion asserts that, always, if a is true, then in the next clock cycle b has to be true. The DFW generated by CHIMP for this assertion is shown in Fig. 7.
Listing 1 shows the step() function of the C++ monitor generated by CHIMP for the assertion G(a ! Xb) @ clk. The variables current_state and next_state are member variables of the monitor class and store the current automaton state and next automaton state respectively. If next state becomes 1 after the execution of the step() function, it means that no transition can be made from the current state. In this case, the monitor outputs ”FAILED”. The initial state 0 of the monitor is assigned to the variable current_state inside the constructor of the monitor class as shown in Listing 2.
Listing 1. The step() function of the monitor for G(a ! Xb) /
S i m u l a t e a s t e p o f t h e m o n i t o r .
/ v o i d m o n i t o r 0 : : s t e p ( ) f / / I f t h e p r o p e r t y h a s n o t f a i l e d y e t i f ( s t a t u s == NOT FAILED ) f / / number o f s t e p s e x e c u t e d s o f a r n u m s t e p s + + ; / / a s s i g n n e x t s t a t e t o c u r r e n t s t a t e c u r r e n t s t a t e = n e x t s t a t e ; / / make n e x t s t a t e i n v a l i d n e x t s t a t e = 1; i f ( c u r r e n t s t a t e == 0 ) f i f ( ! ( a ) )
f n e x t s t a t e = 0 ; g e l s e i f ( ( a ) )
f n e x t s t a t e = 1 ; g g / / i f ( c u r r e n t s t a t e == 0 ) e l s e i f ( c u r r e n t s t a t e == 1 ) f i f ( ( b ) && ! ( a ) )
f n e x t s t a t e = 0 ; g e l s e i f ( ( a ) && ( b ) )
f n e x t s t a t e = 1 ; g g / / i f ( c u r r e n t s t a t e == 1 ) / / FAILED i f no t r a n s i t i o n p o s s i b l e b o o l n o t s t u c k = ( n e x t s t a t e ! = i f ( ! n o t s t u c k ) f p r o p e r t y f a i l e d ( ) ;
1); g g / / i f ( s t a t u s == NOT FAILED ) g / / s t e p ( ) Listing 2. The constructor of the monitor for G(a ! Xb) /
The sampling points can be kernel phases, e.g., MON DELTA CYCLE END, or event notification, e.g., E.notified (E is an event). In such cases, the OSCI kernel needs to communicate with the local_observer at the right time (when a delta cycle ends or when event E is notified) to call the step() function of the monitor. This communication is done by the patch, put on OSCI kernel. This patch contains a class called mon_observer, which communicates with the local_observer class on behalf of the OSCI kernel.
V. EVOLUTION OF CHIMP
Fig. 8 shows the old path of generating C++ monitor from an LTL property in CHIMP. First, MONASGEN Fig. 8. Old LTL to monitor path in CHIMP Fig. 9. New LTL to monitor path in CHIMP uses SPOT to convert the LTL formula to a nondeterministic Bu¨chi Automaton (NBW). Then MONASGEN prunes the NBW to remove all states that do not lead to any accepting state, and generate the corresponding nondeterministic finite automaton (NFW), see [2]. MONASGEN then uses the Automaton Tool to determinize and minimize the NFW to generate minimal deterministic finite automaton (DFW). Finally MONASGEN converts the DFW to C++ monitor.
The main bottleneck in this flow was minimization and determination of NFW using the Automaton tool as it consumes 90% of total monitor generation and compilation time. Also, the Automaton tool may generate multiple edges between two states, resulting in quite large monitors. The newest version of CHIMP introduces a new path as shown in Fig. 9, which bypasses Automaton tool completely and uses only SPOT. So the component Automaton-1.11 in Fig. 1 is not needed by CHIMP anymore. This new path leverages the new functionality of SPOT-1.1.1 to convert an LTL formula to a minimal DFW that explicitly rejects all bad prefixes.
After replacing the Automaton Tool by SPOT to
convert the NBW to minimal DFW, the improvement in
compilation time and monitor size is evident. This new
flow results in 75.93% improvement in monitor
generation and compilation time. To evaluate the performance of
the revised CHIMP, we use the same set of 162 pattern
formulas and 1200 random formulas as mentioned in [
The scatter plot on Fig. 10 shows the comparison of monitor generation and compilation time of the new flow vs the old flow. Most of the points are above the line with slope 1, which indicates that for most of the monitors, the generation and compilation time by old CHIMP is more than by new CHIMP. Fig. 10 - Fig. 14 are all scatter plots2 and interpreted in the same way.
The new flow also merges multiple edges between two states into one edge guarded by the disjunction of the guards on all edges between the states. In this way the average reduction in monitor size in bytes is 61.27%.
Fig. 11 shows the comparison of the size in bytes of the monitors generated by the new flow vs the old flow.
Since the main focus of CHIMP has always been minimizing runtime overhead, we need to ensure that this new flow does not incur more runtime overhead compared to the old flow as a cost of reduced monitor generation and compilation time. So we ran the same set of 162 pattern formulas and 1200 random formulas as mentioned above, to compare the runtime overhead incurred by the new flow vs the old flow. Fig. 12 shows that the runtime overhead of CHIMP using the new flow has been reduced compared to the old flow. The reduction is 7.97% on average.
As CHIMP has evolved to follow a different and more
efficient path and the monitors have been reduced in size,
it was not clear a priori which monitor encoding is the
best. We conducted the same experiment as in [
Fig. 13 shows that the new best encoding in terms of runtime overhead is now front det ifelse. Fig. 14 shows that the new best encoding in terms of monitor generation and compilation time is back ass alpha. CHIMP now provides two configurations for monitor generation, best runtime, which has minimum runtime overhead and best compiletime, which has minimum monitor generation and compilation time. Since the bigger concern is usually runtime overhead, best runtime is the default configuration, given that its monitor generation and compilation time is very close to that of best compiletime.
VI. CONCLUSION
We present CHIMP, an Assertion-Based Dynamic Verification tool for SystemC models, and show that it puts minimal overhead on the runtime of the MUV. We show how the new path in CHIMP results in significant reduction of monitor generation and compilation time and monitor size, as well as runtime overhead. In the future 2http://en.wikipedia.org/wiki/Scatter plot Fig. 10. Comparison of monitor generation and compilation time of the old CHIMP vs new CHIMP Fig. 11. Comparison of monitor size (bytes) generated by the old CHIMP vs new CHIMP we plan to look at the possibility of verifying parametric properties, for example G(send(id) ! F (receive(id))) where one can pass a parameter (here id), to the variables in the LTL formula of the assertion. The above property means that always if the message with ID id is sent, it should be received eventually. Also at present the user needs to know the system architecture to declare an assertion. We would like to make CHIMP work with assertions that are declared in the elaboration phase. Fig. 12. Comparison of runtime overhead incurred by old CHIMP vs new CHIMP
C. Helmstetter, F. Maraninchi, L. Maillet-Contoz, and M. Moy.
Automatic generation of schedulings for improving the test coverage of Systems-on-a-Chip. In FMCAD ’06: Proceedings of the Formal Methods in Computer Aided Design, pages 171– 178, Washington, DC, USA, 2006. IEEE Computer Society.
A. Møller. http://www.brics.dk/automaton/, 2004.
dk.brics.automaton.
O. Spinczyk, A. Gal, and W. Schro¨ der-Preikschat. AspectC++: an aspect-oriented extension to the C++ programming language. In CRPIT ’02: Proceedings of the Fortieth International Conference on Tools Pacific, pages 53–60, Darlinghurst, Australia, Australia, 2002. Australian Computer Society, Inc.
D. Tabakov. Dynamic Assertion-Based Verification for SystemC. PhD thesis, Rice University, Houston, 2010.
D. Tabakov, K. Rozier, and M. Y. Vardi. Optimized temporal monitors for SystemC. Formal Methods in System Design, 41(3):236–268, 2012.
D. Tabakov and M. Vardi. Monitoring temporal SystemC properties. In Proc. 8th Int’l Conf. on Formal Methods and Models for Codesign, pages 123–132. IEEE, July 2010.
Fig. 13. Comparison of runtime overhead of front det ifelse
encoding vs all other encodings
Fig. 14. Comparison of monitor generation time and
compile time overhead of back ass alpha encoding vs all other
encodings
[
D. Tabakov, M. Vardi, G. Kamhi, and E. Singerman. A temporal language for SystemC. In FMCAD ’08: Proc. Int.
Conf. on Formal Methods in Computer-Aided Design, pages 1–9. IEEE Press, 2008.
D. Tabakov and M. Y. Vardi. Automatic aspectization of SystemC. In Proceedings of the 2012 workshop on Modularity in Systems Software, MISS ’12, pages 9–14, New York, NY, USA, 2012. ACM. Abstraction-Based Livelock/Deadlock Checking for Hardware Verification
In-Ho Moon and Kevin Harer
Synopsys Inc.
{mooni, kevinh}@synopsys.com ABSTRACT Livelock/deadlock is a well known and important problem in both hardware and software systems. In hardware verification, a livelock is a situation where the state of a design changes within only a smaller subset of the states reachable from the initial states of the design. Deadlock is a special case in which there is only one state in a livelock. However, livelock/deadlock checking has never been actively used in hardware verification in practice, mainly due to the complexity of the computation which involves finding strongly connected components.
This paper presents a practical abstraction-based livelock/deadlock checking algorithm for hardware verification.
The proposed livelock/deadlock checking works on FSMs rather than the whole design. For each FSM, we make an abstract machine of manageable size from the cone of influence of the FSM. Once a livelock is found on an abstract machine, the livelock is justified on the concrete machine with trace concretization. Experimental results shows that the proposed abstraction-based livelock checking finds real livelock errors in industrial designs. 1. INTRODUCTION
Livelock/deadlock is a well known and important problem in both hardware and software systems. In hardware verification, a livelock is a situation where the state of a design changes within only a subset of the states reachable from the initial states of the design. In a state transition graph, a livelock is a set of states from which there is no path going to any other states that are reachable from the initial state.
Since deadlock is a special case in which there is only one state in a livelock, deadlock checking can be done by livelock checking. Thus, livelock implies both livelock and deadlock in this paper. However, livelock checking1 has never been actively used in hardware verification in practice, mainly due to the complexity of the computation which involves finding SCCs (Strongly Connected Components). Thus, livelock checking has been on hardware designer’s wish list to verify their designs.
There have been many approaches on finding SCCs [
In a state transition graph, a TSCC is an SCC that does not have any outgoing edges to any state outside the SCC.
Thus, a TSCC becomes a livelock group when the TSCC
has any incoming edges to the SCC in the state
transition graph representing a hardware design. However, even
though the method in [
In this paper, we first present an improved BDD-based
algorithm finding TSCCs from[
First, initial state is taken into account in finding TSCCs.
Especially, the improved algorithm handles multiple initial
states efficiently. Secondly, unreachable TSCCs are
distinguished from reachable TSCCs which are more interesting to
designers. Thirdly, we provide more intuitive state
classification as main, transient, and livelock groups as opposed to
transient and recurrence classes in [
This paper also presents a practical approach for checking
livelock using abstraction techniques. The proposed
livelock checking works on FSMs(Finite State Machines)2 rather
than the whole design. For each FSM, we make an abstract
machine (by localization reduction [
Once an FSM is given, its COI is first computed. Then,
an abstract machine is computed by finding N in uential
latches from the COI. Influential latches are the latches that
are likely related with the FSM. N is either pre-defined or a
user-defined number of latches in the abstract machine, or
1Livelock checking is different from liveness checking and
the difference will be explained in Section 2.3.
2FSMs are either automatically extracted [
There is another important hardware property called toggle deadlock. A state variable has a toggle deadlock if the state variable initially toggles and the state variable becomes a constant after a certain number of transitions. However, notice that this is not a constant variable since it initially toggles. Toggle deadlock may or may not happen depending on input stimuli in simulation. Therefore, toggle deadlock is also an important property to check with formal approaches.
Experimental results shows that the proposed abstractionbased approach finds real livelock and toggle deadlock errors from industrial designs.
The contributions of this paper are in the three aspects. • Improved algorithm for livelock checking
The proposed algorithm improved the existing
algorithm [
This paper presents theories and an implementation on abstraction-based livelock checking to handle large designs in practice. • Toggle deadlock checking
To the best of our knowledge, this paper presents the first method to solve toggle deadlock problem.
The remainder of this paper is organized as follows. Section 2 briefly recapitulates finding SCCs and TSCCs, and describes related work. Section 3 describes our improved algorithm for finding TSCCs. Section 4 explains how livelock is checked on FSM using abstraction. Section 5 describes how to check toggle deadlocks. Experimental results are presented and discussed in Section 6. We conclude with Section 7.
PRELIMINARIES
Finding SCCs
Given a graph, G = (V; E) where G is an infinite transition
system of the Kripke structure [
Finding SCCs has a variety of applications in formal
verification such as Buchi emptiness [
The traditional approach to find SCCs is to use Tarjan’s
method [
To overcome this state explosion problem in explicit
algorithms, there have been many publications on symbolic
algorithms. Ravi et al. [
Finding TSCCs
Even though TSCCs are a subset of SCCs in the states of a design, the algorithms for finding TSCCs can be significantly optimized since not all SCCs are of interest.
This section recapitulates the work on finding TSCCs by
Xie and Beeral [
Definition 1. The forward set of state i ∈ S, denoted by F (i), is the set of states that have a path from i. That is, F (i) = {j ∈ S | i → j}. Similarly, the backward set of state i, denoted by B(i), is the set of states that have a path to i.
That is, B(i) = {j ∈ S | j → i}.
Lemma 1. Let i; j ∈ S. If j ∈ F (i), then F (j) ⊆ F (i).
Similarly, if j ∈ B(i), then B(j) ⊆ B(i).
Theorem 1. A state i ∈ S is recurrent if and only if F (i) ⊆ B(i). In other words, i is transient if and only if F (i) * B(i).
Theorem 2. If state i ∈ S is transient, then states in B(i) are all transient. If state i is recurrent, on the other hand, states in F (i) are all recurrent. In the latter case, set F (i) is a recurrence class, and set B(i)\F (i) (if not empty) contains only transient states.
Lemma 1, Theorem 1 and 2 are from [
There are two types of properties in model checking; safety
and liveness properties [
Livelock checking is different from liveness checking in the sense that liveness checking requires a liveness property to work on a design, whereas livelock checking does not require any property and works on a design directly.
There have been many publications on finding all SCCs [
Hachtel et al. [
Qadeer et al. [
Xie and Beeral proposed a reachability-based algorithm
to find all TSCCs iteratively [
None of the above previous work on finding TSCCs was used in real designs in practice, due to the design sizes. Our abstraction-based approach is the first in publication to handle large designs in practice.
Case et al. [
The state classification in [
We propose a new state classification that is shown in Figure 1, assuming that there is one single initial state. Handling multiple initial states is explained in Section 3.3.
Definition 2. STSCC is a sink TSCC that has incoming edges from any states outside the TSCC.
We first define sink TSCC (in short, STSCC) in
Definition 2. The new state classification consists of main group,
transient group, livelock groups (reachable STSCCs) and
unreachable TSCCs for a given initial state. The transient
class in [
l j
Unreachable TSCC m g o n
i d e f h
Livelock Group
Transient Group (Reachable STSCC)
In Figure 1, there are states a through o and a is the initial state that is marked with thick circle. Among all states, the reachable states are a through i inside the dotted rectangle. The unreachable states are j through o outside the dotted rectangle. There are five SCCs that are {a; b; c}; {e; f; g}; {h; i}; {j; k; l}; and{m; n; o}. Since a is the initial state, {a; b; c} becomes the main group. {h; i} and {m; n; o} are TSCCs and only {h; i} is a livelock group (reachable STSCC) since it is reachable from a. {m; n; o} is called an unreachable TSCC. The rest states, {d; e; f; g; j; k; l}, belong to the transient group in which the states are contained in neither the main group nor the TSCCs.
Definition 3. Let x = {x1; : : : ; xn}, y = {y1; : : : ; yn}, and w = {w1; : : : ; wp} be sets of variables ranging over B = {0; 1}. A ( nite state) machine is a pair of boolean functions ⟨Q(x; w; y); I(x)⟩, where Q : B2n+p → B is 1 if and only if there is a transition from the state encoded by x to the state encoded by y under the input encoded by w. I : Bn → B is 1 if the state encoded by x is an initial state. Q(x; w; y) is called transition relation. The sets x, y, and w are called the present state, next state, and input variables, respectively.
The procedure ComputeF orwardSet in Figure 2 is a
modified version of the procedure f orward set in [
The minimized transition relation is denoted by Q˜. In Line
7, y ← x represents that y variables are replaced by x
variables by BDD substitution. Early termination is another
big difference from f orward set in [
F (s) = ZERO; Q˜(x; w; y) = Q(x; w; y) ⇓ careSet; frontier(x) = s; Put s in O; while (frontier(x) ̸= ZERO) { image(y) = ∃x; w: Q˜(x; w; y) ∧ frontier(x); image(x) = image(y)|y x; F (s) = F (s) ∨ image(x); frontier = image(x) ∧ ¬F (s); Put frontier in O; if (BddIteConstant(frontier, stop, ZERO) != ZERO)
break; } return (F (s), O);
Figure 2: Computing forward set.
ComputeBackwardSet is a dual procedure to Compute F orwardSet, except not using stop and not computing the onion rings O.
Figure 3 is a procedure for finding TSCCs from the given
set of states S. The procedure F indT SCCs is a modified
version of the procedure State classif ication in [
PREFIX(SUFFIX) means to trim out the lasso prefix(suffix)
states. This is the same technique used in finding SCCs [
Finally, F indT SCCs returns R (a set of TSCCs) and T (a set of transient states). 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 FindTSCCs(Q, S) {
R = { }; T = ZERO; careSet = S; while (careSet ̸= ZERO) { s = PickOneState(careSet); B(s) = ComputeBackwardSet(Q, careSet, s); F (s) = ComputeForwardSet(Q, careSet, s, ¬B(s)); if (F (s) ⊆ B(s)) {
R = R ∪ F (s); T = T ∨ (B(s) ∧ ¬F (s)); careSet = careSet ∧ ¬B(s);
TrimTransient(Q, careSet, T , PREFIX); } else {
T = T ∨ (s ∨ B(s)); careSet = careSet ∧ ¬(s ∨ B(s));
TrimTransient(Q, careSet, T , BOTH); } return (R; T );
FindLivelock(Q, S, s) { (F (s), O) = ComputeForwardSet(Q, S, s, ZERO); B(s) = ComputeBackwardSet(Q, S, s); reached = F (s) ∨ s; if (F (s) ⊆ B(s)) {
M = F (s); R = { };
T = ZERO; } else {
M = F (s) ∧ B(s); careSet = F (s) ∧ ¬(M ∨ s); TrimTransient(Q, careSet, T , PREFIX); (R, TR) = FindTSCCs(Q, careSet); if (s ∈= M)
TR = TR ∨ s; TU = B(s) ∧ ¬M;
T = TR ∨ TU ; } return (M; R; T; reached; O);
Figure 4 shows the procedure to perform our new state classification. As explained in Section 3.1, we find main group (M ), transient group (T ), and livelock groups (R) from the given initial state (s) within the given care states (S). F indLivelock starts computing forward set F (s) and backward set B(s) in Line 1 and 2. In Line 3, reached is the reached states from s in S. If F (s) ⊆ B(s) in Line 4, there is no livelock in S. In this case, F (s) becomes the main group and both R and T are set to empty in Line 5-7. If F (s) * B(s) in Line 8, there must exist at least one livelock group. In this case, M is computed by intersecting F (s) and B(s) in Line 9. careSet is set to a subset of F (s) in Line 10. The lasso prefix states in careSet are trimmed out in Line 11. TR represents the set of transient states that are reachable from s. In Line 12, R and TR are computed by calling F indT SCCs with careSet. If s ∈= M (means that the main group is empty), s is added to TR in Line 13-14.
TU represents the set of transient states that are unreachable from s and TU is computed in Line 15. T is computed by union of TR and TU in Line 16.
It is possible for a design to have multiple initial states when some of the state variables do not have concrete initial values. In the presence of multiple initial states, finding livelock groups has to be devised correctly to avoid false positives and redundant computations.
Figure 5 shows an example with multiple initial states.
In this example, there are six states, S = {a; b; c; d; e; f }.
There are two SCCs, {a; b; c} and {d; e; f }. We can see that {d; e; f } is a TSCC. a and d are initial states, I = {a; d}, as shown with thick circles. Suppose that we compute livelock by calling F indLivelock(Q; S; I). Then, we get F (I) = B(I) = M = {a; b; c; d; e; f } and R = {} which is not correct since there is a reachable TSCC. Now, let us try to call F indLivelock for each single initial state.
First for the initial state a, we get F (a) = {a; b; c; d; e; f } and B(a) = {a; b; c}. This gives us Ma = {a; b; c} and Ra = {d; e; f }. There is a livelock group Ra for the initial state a. Now, for the initial state d, F (d) = {d; e; f } and B(d) = {a; b; c; d; e; f }. This gives us Md = {d; e; f } and Rd = {} and TU = {a; b; c}. There is no livelock group for the initial state d. Therefore, we can see that livelock checking has to be applied for each single initial state separately in the presence of multiple initial states.
f b d
e
Theorem 3. When there are two initial states (i0 and i1), if i1 is included in the reached states from i0, the livelock groups from i1 are a subset of the livelock groups from i0.
Proof. Since i1 is included in the reached states from i0, i1 is in either main, transient, or livelock groups from i0. When i1 is in the main group, the same livelock groups from i1 are obtained. When i1 is in the transient group, all or a subset of the livelock groups i1 is obtained. When i1 is in one of the livelock groups, the livelock group including i1 becomes the main group from i1, and no livelock group exists from i1 since the other livelock groups from i0 become unreachable TSCCs from i1. From the above three cases, no new livelock group is obtained from i1 compared to the ones from i0. Therefore, the livelock groups from i1 are a subset of the livelock groups from i0.
Theorem 3 says that when there is large number of initial states, we can skip livelock checking for any initial states that are already in the forward sets of other initial states.
In Figure 5, livelock checking for the initial state d can be skipped because of d ∈ F (a), assuming that a is used first.
However, there is an order dependency on which initial state is used first. If d is used first, we still need to run livelock checking with a. In practice, the number of calls to F indLivelock is greatly reduced because of Theorem 3 in the presence of multiple initial states.
Figure 6 is the top-level procedure that checks livelock with multiple initial states. CheckLivelock takes transition relation(Q), a set of states(S), a set of initial states(I), and a concrete machine(C) as procedure inputs. The use of C is explained in Section 4. CheckLivelock first finds livelock groups in the reachable states in Line 1-17 and then it finds TSCCs in the unreachable states in Line 18-23. The while loop (Line 6-17) performs livelock checking for a current initial state s until all initial states are covered with iteration index k. For this, remaining is initially set to I in Line 3 and updated by eliminating the newly reached states reachedk from remaining in Line 13. reached is the reached states from all initial states. reached is initially set to ZERO in Line 1 and updated by adding reachedk that is the reached states from s in Line 12. Then, the next initial state is chosen from remaining in Line 15. TU is the union of unreachable transient states from each initial state. TU is initially set to ZERO in Line 2 and updated by adding the unreachable states of Tk in Line 14. For the current initial state s, F indLivelock is called in Line 7. |Rk| represents the number of livelock groups in Rk in Line 8. For each Rkj, a trace tracejk is generated in Line 9 and the livelock is reported with the trace in Line 10. Generating trace is explained in Section 4.2 and reporting livelock is explained in Section 4.3.
CheckLivelock(Q, S, I, C) { reached = ZERO; TU = ZERO; remaining = I; k = 0; s = PickOneState(I); while (s ̸= ZERO) { (Mk; Rk; Tk; reachedk; Ok) = FindLivelock(Q, S, s); for (j = 0; j < |Rk|; j++) { tracejk = GenerateTrace(C, Rkj, s, Ok); ReportLivelock(s, Mk, Rk, Tk, tracejk);
j } reached = reached ∨ reachedk; remaining = remaining ∧ ¬reachedk; TU = TU ∨ (Tk ∧ ¬reachedk); s = PickOneState(remaining); k++; } careSet = ¬(reached ∨ TU ); if (careSet ̸= ZERO) {
Rk = FindTSCCs(Q, careSet); for (j = 0; j < |Rk|; j++)
ReportUnreachLivelock(Rkj); 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23
Figure 6: Checking livelock.
Once all reachable livelock groups are found, we next find unreachable TSCCs. We set the care states careSet to the negation of all visited states so far in Line 18, then call F indT SCCs with careSet in Line 20. If there is any unreachable TSCC, the TSCC is reported in Line 22.
To check whether a livelock exists in a design or not, the checking should be done on the whole design. However, this is infeasible due to the size of the design in practice. Thus, we propose a practical method for checking livelock on FSMs on the design.
Even when we check livelock on an FSM, the entire COI logic of the FSM must be considered in order to get an exact result on livelock. However, this is still computationally very expensive or not feasible, in most real designs. Thus, we propose a framework for abstraction-based livelock checking on an abstracted COI of the FSM. Once we find a livelock on the abstract machine, we justify whether the livelock exists on the concrete machine. Notice that a livelock on the abstract machine can be mapped into more than one livelock on the concrete machine.
Figure 7 shows how an abstract machine is obtained from the COI of an FSM. Suppose an FSM that has two state variables f and g. Then, we compute the COI of the FSM.
Suppose that there are state variables {a; b; c; d; e} in the COI of the FSM. The size of the abstract machine is predefined and let us suppose that the size is N . Then, a set of influential latches from the COI is computed from the FSM variables. The minimum abstract machine is the FSM itself and the maximum abstract machine is the concrete machine. In this example, N =4 and we get the abstract machine {f; g; d; e}.
COI of FSM a b c d e
FSM f g
Figure 7: Abstract machine.
Theorem 4. If any state in a livelock group on an abstract machine is reachable from the initial state on the concrete machine, the livelock exists on the concrete machine.
Proof. Since the abstraction is an over-approximation, the set of all transitions on the abstract machine is a superset of the set of all transitions on the concrete machine. Since there is no path from any state in the livelock group to any state in the main group on the abstract machine, there is still no path from any projected states of the livelock group on the concrete machine to any projected states of the main group on the concrete machine. Now, suppose that the livelock does not exist on the concrete machine. In order for the livelock not to exist on the concrete machine, the only condition is that there is no path from the projected main group to the projected livelock group on the concrete machine. In other words, the projected livelock group has to be unreachable from the initial state. However, this contradicts the assumption that any state of the livelock group is reachable from the initial state on the concrete machine. Therefore, the livelock group still exists on the concrete machine.
Thanks to Theorem 4, this abstraction-based livelock finds a livelock on small abstract machine using BDD-based symbolic method, then justifies the existence of the livelock on the concrete machine by trace concretization in Section 4.2, by using SAT techniques that can handle large designs. The abstraction-based livelock checking is an incomplete method in the sense that it does not provide the proof of no livelock unless the checking is performed on a concrete machine. No livelock on an abstract machine does not guarantee no livelock on the concrete machine. However, the abstractionbased livelock checking enables finding real livelock errors on industrial large designs. 4.1
Let V be the set of state variables in an abstract machine for livelock checking. Suppose that R(V ) is the reached states in the abstract machine and L(V ) is a livelock group containing a TSCC. Also, suppose that v is a state variable in V . We are interested in whether v contributes to the livelock as in Definition 4. This is called variable causality.
Definition 4. When a livelock exists in the abstract machine, a variable v in V contributes to the livelock if the livelock disappears by eliminating v from the abstract machine.
In other words, there is no livelock in another abstract machine that is composed of the variables, V \v.
Equation 1 shows a condition for existence of livelock.
L(V )
R(V )
Now, let R˜ be the quantified reached states and L˜ be the quantified livelock states with respect to a state variable v, as shown in Equation 2 and 3.
R~(V nv) = 9v: R(V )
L~(V nv) = 9v: L(V )
Then, it is determined by Equation 4 to check whether the variable v contributes to the livelock. Theorem 5 says that if Equation 4 holds, v contributes to the livelock.
L~(V nv)
R~(V nv)
Theorem 5. When a livelock group is found on an abstract machine (L(V ) ⊂ R(V )), if L˜(V \v) ⊂ R˜(V \v) holds for a variable v, the variable v contributes to the livelock.
Proof. Let M1 be the machine consisting of V and suppose that a livelock group exists in M1. Let M2 be the machine consisting of (V \v) by eliminating v from M1. Also, let T1 (T2) be the set of transitions in M1 (M2), respectively.
Since M2 is an over-approximated machine from M1, M2 has more transitions than M1 (T1 ⊂ T2). Let Td be the difference between T1 and T2. If there is any transition (in Td) that makes a path from any state in the livelock to any state in the main group in M2, the livelock group merges into the main group and both groups become a single SCC, yielding L˜(V \v) = R˜(V \v). Thus, M2 becomes a machine without the livelock. This means that v is a necessary variable to have the livelock in M1. Therefore, if L˜(V \v) = R˜(V \v), v contributes to the livelock.
This causality checking can also be applied to a set of variables, especially with FSM variables, in order to report whether the livelocks are related with the FSM. Let F be the set of variables in an FSM and C be the set of variables in the COI of the FSM. Suppose that R(F; C) is the reached states in the abstract machine and L(F; C) is a livelock group containing a TSCC. The quantified reached states and the quantified livelock states are computed in Equation 5 and 6 with respect to the FSM variables, respectively.
R~(C) = 9F : R(F; C)
L~(C) = 9F : L(F; C)
Then, Equation 7 shows the causality checking with the FSM variables to check whether the FSM variables contribute to the livelock.
L~(C) = R~(C) 4.2
Trace concretization
Once a livelock group is found on an abstract machine, we
need to justify whether the livelock group is reachable on the
concrete machine. This can be done by the following three
steps. The first step is to pick a target state in the livelock
group. The target state is chosen randomly from the livelock
group, but is one of the closest states to the initial states by
using the onion rings Ok in Figure 6. The second step is to
generate an abstract trace. Starting from the target state,
an abstract trace can be computed by applying BDD-based
pre-image computation iteratively until the initial state is
reached. The third step is to generate a concrete trace by
making a BMC (Bounded Model Checking [2]) problem from
the abstract trace, in order to see whether the livelock group
is reachable on the concrete machine. An efficient approach
for concretization was proposed in [
Once a concrete trace is generated for a livelock group, the livelock is real on the concrete machine. We report the livelock group with the state classification mentioned in Section 3.1. A livelock group is reported with its initial state, the main group, transient group, and the unreachable states in terms of the number of states and the percentage in each group on the abstract machine.
By looking at the transient and livelock groups, we can see what fraction of the state space is in problematic zone.
A good design is expected to have only one main group per one initial state without any transient and livelock groups, unless the design has an intended reset sequence to a normal mode.
TOGGLE DEADLOCK CHECKING
There is another important design property, called toggle deadlock that is related to livelock. A livelock may occur for multiple state variables of a design, whereas a toggle deadlock may occur on a single state variable. A state variable has a toggle deadlock if the variable initially toggles, but the variable gets stuck at a constant value after a certain number of cycles.
Figure 8 shows an example of toggle deadlock. There are two state variables {a; b} and four states {s0; s1; s2; s3} as in the example. Provided that s0 is the initial state, the main group is {s0; s1} and the livelock group is {s2; s3}. Once the state transition reaches to s2 that is a state in the livelock group, the value of b gets stuck at 1, whereas a still toggles.
Thus, we say that b has a toggle deadlock.
a=0, b=0 s0 s1 a=1, b=0 a=0, b=1 s3 s2 a=1, b=1
Theorem 6. If there is no STSCC in a design, there is no toggle deadlock on any variable.
Proof. To be a toggle deadlock, a variable is supposed to toggle at a cycle and to hold the value forever from the cycle.
No STSCC implies that there is only main group in the design. If a variable appears as constant in the main group, the variable is a constant. However, the main group does not have any prefix behavior. This means it is not possible for the variable to get toggled before the main group. Therefore, no STSCC implies no toggle deadlock.
Theorem 6 shows that toggle deadlock occurs in the presence of a livelock. It is also possible that there is no toggle deadlock on a design that has a livelock. Thus, toggle deadlock on a state variable can be computed by two steps. First, Design D1 D2 1163 1330 385 352 25 Statistics
F D3-F1 D3-F2 32541 32541 912 912 2 4 30 60 90 120 30 60 68 30 4 30
Llk
Dlk 1 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 we find STSCCs on an abstract machine from the state variable. The abstract machine is made in the same way as in livelock checking on FSM. Secondly, we evaluate the value of the state variable in the livelock if the livelock exists.
Figure 9 shows the procedure that checks toggle deadlock on a given state variable t. CheckT oggleDeadlock takes transition relation (Q), a set of states (S), a set of initial states (I), a concrete machine (C), and the state variable (t) as procedure inputs. CheckT oggleDeadlock is similar to CheckLivelock in Figure 6. For each reachable livelock group Rkj in Line 6, T estT oggleDeadlock checks whether the value of t toggles or not in the livelock group and returns dlk and c in Line 7. dlk represents whether the state variable is in toggle deadlock or not, and c is the constant value (0 or 1) in the case of toggle deadlock.
CheckToggleDeadlock(Q, S, I, C, t) { remaining = I; k = 0; s = PickOneState(I); while (s ̸= ZERO) { (Rk; reachedk; Ok) = FindLivelock(Q, S, s); for (j = 0; j < |Rk|; j++) { (dlk, c) = TestToggleDeadlock(Rkj, t); if (dlk) { tracejk = GenerateTrace(C, Rkj, s, Ok); ReportToggleDeadlock(s, Rk, tracejk, c);
j } remaining = remaining ∧ ¬reachedk; s = PickOneState(remaining); k++; 6. EXPERIMENTAL RESULTS
We have implemented the proposed livelock checking and toggle deadlock checking algorithms. Table 1 shows our experimental results on livelock and toggle deadlock checking, generated on a 1.4 GHz Intel processor machine with 4 GB memory running Red Hat Linux.
The first column lists the design names. The next five columns present the statistics on the designs, in terms of the number of latches (L), the number of inputs (I), the number of latches in FSM (F ), the number of toggle signals to check (T ), and the number of latches in the COI of either FSM and a toggle signal (COI). The next three columns show the results on livelock and toggle deadlock checking. The column with N shows how many latches were in the abstract machine. The column with Llk shows how many livelock groups are found and the column with Dlk shows how many toggle deadlock are found. The next six columns compare the performance between two methods (N ew1 and N ew2), in terms of time(T ime), memory(M em), and the number of image/pre-image computations(Ops). N ew1 is the proposed method without the trimming technique, whereas N ew2 is the proposed method with the trimming technique. The times are in the form of hh:mm:ss and the memory consumptions are in M-byte. The final two columns(T raceGen) show the results on trace generation on concrete machine for the livelock or toggle deadlock found by N ew2, and T ime shows the time spent for trace generation and Len shows the trace length.
We have chosen 3 industrial designs (D1, D2, and D3).
For each design, we have run livelock or toggle deadlock checking on several sizes of abstract machines with the multiples of 30 latches. We have set the maximum run time to 24 CPU hours.
In D1, there is one FSM automatically extracted. The FSM consists of 7 latches and contains 632 latches in its COI.
We can see that the run time is exponentially increased, depending on the size of the abstract machine. On this design, the livelock checking became infeasible when N =120.
In D2, there is also one FSM that was user-specified. The FSM consists of 25 latches and contains only 68 latches in its COI. This design has a livelock group. However, the livelock was not detected when N=30 and N=60. The livelock was detected only when all the latches in the COI were included in the abstract machine. In other words, the abstract machine is the concrete machine at the FSM point of view. Since the livelock was found on the concrete machine, trace concretization is not required since the abstract trace in Section 4.2 is already a concrete trace.
D2 is the only design showing a significant performance difference between N ew1 and N ew2 in the table. This is because this design has many transient states as well as many livelock groups. In this case, the trimming technique significantly reduced the number of image/pre-image operations from 386K to 70K (5.5X reduction) that gave big speed-up from 5 hours to 1 hour (5X speed-up). This shows that the trimming technique helps the performance when there are many transient states. When there is no transient states, the trimming technique becomes a pure overhead as shown in D3. However, the overhead is almost negligible from the experiment.
In D3, there are two FSMs (F 1 and F 2). F 1 is composed of 2 latches and a livelock was found with N =30 within 49 seconds. The livelock was justified by trace concretization that took 397 seconds, and the trace length was 66. F 2 is composed of 4 latches and a livelock was found with N =4 (the FSM itself) in 9 seconds. The livelock was also justified by trace concretization that took 114 seconds, and the trace length was 14. We have also tried the toggle deadlock checking on F 2 separately from the livelock checking.
A toggle deadlock was found in 90 seconds and the concrete trace was generated in 131 seconds. D3 shows the value of abstraction-based livelock and toggle deadlock checking.
Table 2 shows a comparison on finding all SCCs with four
algorithms (XB [
Time
Memory
Ops
SCCs
States 84:07:56 45:55:53 26:01:54 1:39:47 1013333 2590724 2609008 102990
2.08e8 Method XB Lockstep Skeleton IXB
We have presented a framework for abstraction-based livelock and toggle deadlock checking, in order to handle large designs in practice. Since exact livelock and toggle deadlock checking is infeasible on real designs directly, our approach is to check livelock and toggle deadlock on abstract machine of either an FSM or a toggle signal. Once we find a livelock or toggle deadlock, we justify the livelock or toggle deadlock on the concrete machine by concretizing the abstract trace on the concrete machine.
Even though the proposed approach does not prove the non-existence of livelock or toggle deadlock on a design unless the design is small enough to handle, this approach finds livelocks or toggle deadlocks on the design if there exists.
To the best of our knowledge, it is the first approach to use the abstraction-based livelock checking and also the first approach for checking toggle deadlock. The experimental results showed that the abstraction-based approach finds livelock errors on the real designs.
As future work, we are interested in improving the concretization, finding more accurate influential latches, and optimizing the computations with multiple FSMs or toggle signals by considering the overlaps in their COIs.
REFERENCES [1] A. Biere, C. Artho, and V. Schuppan. Liveness checking as safety checking. In International Workshop in Formal
Methods for Industrial Critical Systems, pages 160–177, 2002. [2] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Fifth International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'99), pages 193–207, Amsterdam, The
Netherlands, Mar. 1999. LNCS 1579. [3] R. Bloem, H. Gabow, and F. Somenzi. An algorithm for strongly connected component analysis in n log n symbolic steps. In Formal Methods in Computer Aided Design, pages 37–54, 2000. [4] R. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, Aug. 1986. abstraction abstraction-based assertion
reparameterization
SMT synthesis systemC
9 46 38 19 4 9 9 4 19 28
4 38 Een, Niklas Harer, Kevin Niemetz, Aina Palena, Marco Preiner, Mathias 28
9 19 9 1 38