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.
With the increasing popularity of high-level design
methodologies there is renewed interest in data-path equivalence
checking [
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.
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 techniques 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.
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.
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[
(b)structurally hashed
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
Original miter Word−level Simulator miter F=G input:̄x new miter target Verific Parser Frontend
VeriABC SSA Network Bit−level
AIG ABC solvers SAT
UNSAT
Learning−based Transformations
Transformed
RTL
LEC tries to solve the miter directly using random
simulation on the word-level simulator or by ABC[
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 miter F=G kept abstract input x̄' redundant input:x̄ (c)abstraction
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.
Two word-level simulators are generated from the SSA
network. One is a native interpreted model. The other uses
the open-source Verilator[
As shown in Figure 1, an AIG is created from the SSA
network by bit-blasting. LEC calls ABC[
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.
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.
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])[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.
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
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.
4) Establish the following equivalence formally at the algebraic 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. (5) (6) (7) (8) (9)
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.
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[
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[
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 input variables to compute the coefficients: 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, b = F (0; 0; :::; 0) simplification and abstraction can not simplify the model a0 = F (1; 0; :::; 0) b further. Also, there are no good candidates for case-splitting. a1 = F (0; 1; :::; 0) b The local rewriting rules can not be applied effectively without ::: ohfavtihneg msoimteer glologbica.l Hinifgohrm-leavtieolni ntofohremlpatcioonnvmerugset tbhee tewxotrascidteeds an 1 = F (0; 0; :::; 1) b 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: 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: 16 x0 + 2 x1 + 2 x2 + 2 x3 + 2 x4 + 2 x5 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 f = g <=> 8 i ai = a0i 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) ...
(a)linear adder chain Fig. 6. Addition implementation 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) = g(x) =
X ai xi + b
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 cs is the quotient of fw=fs and ct = (fw cs fs)=ft, while fst is the remainder of the previous division. The substitution is conducted in one topological traversal from the inputs to the miter output. After substitution, the annotated reduced graph is essentially a multi-level implementation of the above linear sum. Because the linear sum annotated at each node in the reduced graph is only a conjecture, it may not be exactly the same function as in the original miter logic. However, in reimplementing f using this structure, certain similarities are still captured through the construction process.
This multi-level circuit is implemented by traversing the substituted reduced graph, and creating a corresponding Verilog file for F 0. It is generated by allocating a bit-vector at each internal node with its bit-width equivalent to output port of F . The same can be done for G to obtain G0. The reason why LEC goes through so much trouble to obtain separate RTL implementations for F 0 and G0 (even though they are both implementing f ), is that we need to prove F = F 0 and G = G0 separately next. Without the structural similarities created through this procedure, proving equivalence with an arbitrary F 0 and G0 would be as difficult as proving the original F = G. Generally, only with these extra similarities injected, can the miter model be simplified enough to allow SAT sweeping to succeed for F = F 0 and G = G0.
4) Proving F = F 0 and G = G0 : We construct two miter models F = F 0 and G = G0 as caseF and caseG in Figure 3, and apply LEC separately to each. By construction, each miter should be simpler than the original F = G because of the increased structural similarity between the two sides of the miter. Another round of LEC might reduce this miter logic, if not prove it directly through bit-level solvers. In the present case, F = F 0 was proven instantly because F is a simple linear adder chain, and so is F 0. Proving G = G0 takes more time using ABCs dcec because G is a highly optimized implementation of f and the multi-level implementation from the annotated reduced graph only captures part of the similarity.
But, the injected similarity was sufficient enough to reduce the complexity to be within dcec’s capacity.
5) Proving that F 0=G0 implements f =g : To complete the proof, we still have the proof obligation that F 0 and G0 implement f and g respectively. By construction from the reduced graph, the generated Verilog is a verbatim translation from the multi-level form of f . However, we need to bridge the gap between Verilog’s bit-vector arithmetic vs. the integer arithmetic of the linear sum. To do so, we created SVA assertions to check that every Verilog statement captures the integer value in full without losing precision due to underflows or overflows.
c[n : 0] =a[n assert (a[n : 0] == (c[n : 0] b[m : 0])[n : 0]) c[m : 0] =fa[n : 0]g[m : 0]; assert a[n : 0] == f(n m) fc[m
1]g; c[m : 0]g The first two sets of assertions ensure there is no overflow of signed integer add and no non-zero remainder of division.
The third one ensures that extraction does not change the
value in two’s complement representation. The SVA checkers
are formally verified separately using the VeriABC[
From the above procedures, we established the following:
f (x) = g(x)
(13) (14) (15) (16) (17) Altogether they establish the proof for F = G.
Combining the above procedures into a single run, LEC took
about 10 minutes on an i7 processor to complete the full proof.
Roughly 80% of the time is spent on compiling and running
random simulation, the rest are used for SAT solving. In table
VI, we also compare this run-time against Boolector[
Miter model 1
Boolector time-out
Z3 time-out iprove time-out
LEC 10min In summary, polynomial reconstruction was a key technique to prove the underlying miter problem. The casestudy illustrates the major steps and the proof obligations encountered during the process. The actual techniques used for different domains of the underlying arithmetic would differ. Each algebraic domain would require special purpose heuristics and automated proof procedures to guarantee the correctness of the reconstructions and transformations used in the method. The goal of the linear construction procedure was to inject increased structural similarity by using global algebraic transformations.
Table VI shows the experimental results comparing
Boolector[
The miter d1, extracted from a PEP sub-model, is a demonstration of rewrite rule 6 in Table II using 32-bit multiplication. As both Boolector and Z3 fail to prove equivalence within the time-limit, they likely do not have this rewriting rule implemented.
To prove d2, LEC conducts conditional rewriting using rule (2) by first statically proving an invariant in the form of (3). After the transformation, the multipliers are matched exactly on both sides of the miter and removed in the subsequent abstract model. The final miter model is proved instantly by ABC on the bit level AIG.
The miter model d3 has part of its logic similar to mul 64 64 embedded inside. LEC proves d3 by first applying rewriting rules repeatedly until no more rewriting is possible. Then, LEC computes a reduced model through abstraction. In the reduced model, LEC conducts a case-split on a one-bit input. The case-0 AIG model is proven instantly, while case-1 is proven in about 10 minutes by ABC.
The miter d4 is proven by first conducting a case-split of two bit-vector inputs: cofactoring on whether the bit-vector equals zero or not. Three of the four cofactored cases are proven instantly. The one unresolved goes through a round of simplification and abstraction. On the then obtained sub-model, three one-bit inputs are identified and cofactored through case-split procedures. LEC prove all eight cases quickly within a few seconds.
Miter d5 is extracted from model 15 in Figure 5 which contains the purely linear sum miter described in the casestudy section. For this simpler miter, Z3 is able to prove it in 9 hours while both iprove and Boolector time out. This shows that LEC’s transformations through collaborating procedures successfully reduce the surrounding logic in the original model, which was preventing Z3 to prove it in 24 hours.
The above experiments demonstrate the effectiveness of LEC’s collaborating procedures of simplification, rewriting, case-splitting and abstraction computations. The LEC architecture allows these procedures to be applied recursively through a sub-model tree: the model obtained by one procedure introduces new opportunities for applying other procedures in the next iteration. As exemplified in miter d4, the initial case-split gives rise to new opportunities for simplification as new constants are introduced by cofactoring. Then a new round of abstraction is able to remove enough common logic and expose three one-bit inputs as case-split candidates in the reduced model, which in turn gives rise to another casesplit transformation that leads to the final proof. None of this is possible without the transformations being applied in sequence.
In bit-level equivalence-checking procedures [
SMT solving is relevant because a data-path is a subset
of QF BV theory. Methods such as [
The techniques in [
In conducting consistency checking between C and Verilog
RTL, the work [
In terms of tool architecture, [
In LEC, we build a system of collaborating procedures for data-path equivalence-checking problems found from an industrial setting. The strategy is to utilize Boolean level solvers, conduct the transformations at the word-level and to synthesize internal similarities by lifting the reasoning to the algebraic level . Using a real industrial case-study, we demonstrated the applicability of the sub-tree infrastructure for integrating a compositional proof methodology using LEC.