Abstract
Completion Optimization searches the legal completions of a Partially Defined Boolean Function (PDBF) before conventional circuit optimization. Ordinary RTL blocks, however, are normally written as fully specified local functions. This paper shows how contextual reachability can expose partiality that is hidden by that local view. For an internal RTL block, only the local input terms reachable from the surrounding design are behaviorally constrained; unreachable local terms form contextual don't-care conditions. The reachable input/output relation therefore defines a Contextual PDBF and a corresponding Legal Completion Opportunity Space. We formulate the contextual-equivalence principle, distinguish independent from correlated reachability, and describe an extraction methodology that can be implemented by exhaustive, symbolic, SAT-, BDD-, or formal-reachability techniques. The experimental study combines five RTL-derived demonstrations with a broader controlled suite of 15 source-independent RTL-structured Contextual PDBFs. For the reported ABC experiments, unspecified contextual terms are fixed to zero before conventional optimization; GT Completion Optimization instead searches legal completions before circuit optimization. In the controlled 15-case suite, three ABC optimization flows were evaluated after zero completion, their Pareto-best outcomes were retained, and every benchmark has at least one GT implementation that Pareto-dominates the reported ABC Pareto set. Across the complete validation artifact set, all 73 implementations (28 GT and 45 ABC) satisfy every specified care assignment, and all 45 ABC artifacts evaluate to the all-zero output vector on every omitted input assignment. These results are evidence for the value of preserving completion freedom, not a universal tool-performance claim. They support a synthesis methodology in which contextual partiality is discovered first, the resulting PDBF is optimized second, and the selected circuit is optimized third.
Index Terms—logic synthesis, RTL, partially defined Boolean functions, don't-care conditions, reachability, completion optimization, Boolean optimization.
I. Introduction
Logic synthesis conventionally begins with a specified Boolean function and seeks an efficient implementation of that function. Completion Optimization adds an earlier decision: when the specification is partial, it searches the set of fully defined Boolean functions that satisfy the specified terms and selects a favorable Legal Completion before conventional circuit optimization. This changes the optimization problem from “how should this fixed function be implemented?” to “which legal function should be implemented, and then how should it be implemented?”
The apparent obstacle to applying this idea to ordinary RTL is that RTL blocks are normally treated as completely specified. A local combinational block may define an output for every possible local input vector. Yet that local truth table can overstate what the complete design actually requires. Inputs to an internal block are produced by upstream logic, protocol constraints, state encoding, arbitration rules, decode structure, or other surrounding circuitry. Consequently, many combinations in the block’s nominal local input space may never occur in the design context.
This paper calls the resulting incompletely constrained relation a Contextual Partially Defined Boolean Function (Contextual PDBF). Its care set consists of the local input/output terms that are reachable in the complete design context. Local terms that cannot occur are contextual don’t-care conditions: changing the block’s behavior on those terms cannot alter observable design behavior, provided the operating context that establishes unreachability is preserved.
The experimental study has two layers. The first uses five RTL-derived demonstrations representing secure ingress, instruction control, DMA transaction control, protocol control, and resource arbitration. These examples contain 18–24 local inputs but only 128–1,002 reachable care terms, leaving more than 99.86% of each nominal local input space contextually unconstrained. The second layer is a controlled suite of 15 source-independent RTL-structured Contextual PDBFs spanning decoding, control, arbitration, routing, FIFO, cache, DMA, protocol, privilege, address decode, hazard, CSR, and packet-routing structures. The controlled suite is not claimed to be a provenance-qualified projection of specific upstream RTL; it is used to test the synthesis hypothesis broadly under unchanged PDBF passports.
The central experimental comparison is deliberately narrower than a general comparison of synthesis systems. In the reported conventional flow, the sparse Contextual PDBF is converted to a fully defined zero completion by assigning zero to unspecified contextual terms and is then optimized by ABC. GT Completion Optimization instead searches the Legal Completion Opportunity Space before implementation optimization. The experiment therefore asks whether preserving and searching contextual partiality can expose implementations that are missed after one Legal Completion has already been fixed.
Principal contributions
- A formulation of hidden contextual don’t-care conditions in ordinary RTL designs.
- A definition of Contextual PDBFs and a contextual-equivalence principle based on reachable local behavior.
- A reachability-based extraction methodology, including independent and correlated reachability.
- A synthesis framework that separates discovery of contextual partiality, optimization of the Legal Completion Opportunity Space, and circuit optimization.
- An experimental study combining five RTL-derived demonstrations with a controlled 15-benchmark RTL-structured PDBF suite, including multiple zero-completion ABC flows, Pareto comparison, and exhaustive passport validation.
First Discover the Contextual PDBF. Then Optimize the PDBF. Then Optimize the Circuit.
II. Background
A. Partially Defined Boolean Functions
A Partially Defined Boolean Function specifies required output values only for a subset of its input terms. The remaining terms are unspecified. Assigning values to all unspecified terms without changing any specified term produces a Fully Defined Boolean Function. Each such function is a Legal Completion of the PDBF.
The set of all Legal Completions forms an Opportunity Space. Different completions can have different structural properties and therefore admit different implementation costs even though every completion satisfies the same partial specification. This is the Boolean-function-level opportunity exploited by Completion Optimization.
B. Completion Optimization
Completion Optimization searches the Legal Completion Opportunity Space according to an implementation objective. Once a completion is selected, conventional synthesis can optimize the implementation of that fully defined function. The distinction between completion selection and circuit optimization is important: circuit optimization operates after the Boolean function has been fixed, whereas Completion Optimization can change unspecified values while the specification still permits those choices.
C. PDBF Passport Library
A PDBF Passport records the identity and structure of a PDBF together with optimized implementations and measured characteristics. The Passport Library provides a mechanism for recognizing previously encountered PDBFs and reusing implementations or optimization knowledge. Contextual PDBFs extend the potential scope of this mechanism because partial functions need not originate as explicitly incomplete specifications; they can be discovered inside ordinary RTL contexts.
III. Contextual Partiality in RTL Designs
Consider an internal combinational block B with n local inputs. Its isolated RTL description defines a function over 2n local input combinations. In the complete design, however, the local input vector of B is generated by surrounding logic. Let RB denote the set of local input vectors that can actually reach B under the considered primary-input, state, and environmental constraints. In general, RB may be a strict subset of the nominal local domain.
If x is not in RB, the complete design never presents x to B under the stated context. The value assigned by the isolated RTL description at x is therefore not required to preserve contextual behavior. Such points are hidden contextual don’t-care conditions. The local RTL is syntactically fully specified, but the behavior required by the complete design is partial.
A. Contextual PDBF
The definition is relative to a context. If architectural assumptions, state constraints, upstream logic, or environmental conditions change, the reachable set may change and the Contextual PDBF must be reconsidered. Contextual don’t-cares are therefore derived constraints, not arbitrary designer annotations.
B. Contextual Equivalence
This principle is the correctness basis for Completion Optimization of a Contextual PDBF. A Legal Completion may assign arbitrary values outside the reachable care set, but it must preserve every reachable local input/output relation.
IV. Reachability and Contextual PDBF Extraction
The essential extraction problem is to determine the reachable local input set of a candidate block and associate each reachable local input with the output required by the original RTL. A conceptually direct procedure is: select an internal block; explore the legal behavior of the surrounding design; record each local input term presented to the block and its required output; remove duplicates; preserve those terms as the care set; and mark all remaining local terms as unspecified.
For bounded demonstrations, exploration can be exhaustive. Larger designs require scalable techniques such as symbolic simulation, SAT solving, BDDs, formal reachability, compositional analysis, abstraction, or hybrid methods. The contribution here is not a universal reachability engine; it is the synthesis abstraction that results once contextual reachability has been determined.
A. Independent Reachability
Independent Reachability occurs when components of a block’s local input vector are generated from independent upstream dependencies and may be combined as a Cartesian product of their reachable values. In this case, local reachability can sometimes be constructed compositionally without enumerating every global input assignment.
B. Correlated Reachability
Correlated Reachability occurs when incoming values share upstream dependencies, protocol relationships, state, or other constraints. Values that are individually reachable need not be jointly reachable. The care set must therefore preserve the correlations induced by the complete design. This case is particularly important because assuming independence can introduce spurious care terms and destroy valid contextual don’t-care opportunities.
V. Synthesis Methodology and Experimental Question
After extraction, a Contextual PDBF can be handled in two fundamentally different ways. The first fixes one Legal Completion, thereby converting the partial relation into a fully specified Boolean function, and then applies conventional logic synthesis. In the ABC experiments reported here, that fixed function is specifically the zero completion: every unspecified contextual term is assigned the all-zero output vector before optimization. The second flow retains the partial relation long enough to search among Legal Completions before optimizing the resulting implementation.
| Flow | Transformation | Optimization freedom |
|---|---|---|
| Zero-completion baseline | Contextual PDBF → fix unspecified terms to zero → ABC synthesis | Circuit optimization after one Legal Completion is fixed |
| Completion-optimization flow | Contextual PDBF → search Legal Completion Opportunity Space → GT synthesis | Completion selection plus implementation optimization |
This framing avoids attributing every observed difference to the downstream synthesis engine. The experiment is specifically about the value of preserving Legal Completion freedom. Once a completion has been fixed, a conventional synthesizer is no longer permitted to alter the function on those formerly unspecified points unless equivalent don’t-care information is separately supplied and retained.
Accordingly, the reported ABC numbers should be interpreted as zero-completion baselines for the evaluated Contextual PDBFs, not as a claim about the best result ABC could obtain if equivalent incompletely specified-function freedom were explicitly preserved. For the controlled 15-case suite, three conventional ABC optimization paths were evaluated from the same zero completion: deepsyn, independent transtoch, and chained deepsyn → transtoch. The Pareto-best ABC outcomes across these flows are retained. Likewise, the present data do not constitute a controlled comparison against synthesis of the original RTL in a common technology library; such a baseline is reserved for future evaluation.
VI. RTL Demonstrations
Five Contextual PDBFs were extracted from structurally different RTL control contexts. The demonstrations were selected to test whether contextual partiality appears across domains rather than only in a single arithmetic or encoding pattern. Table II summarizes the local interfaces and reachable care domains.
| Demo / Context | PI | PO | Care terms | Nominal local space | Care fraction | Contextual DC |
|---|---|---|---|---|---|---|
| #1 Secure Ingress | 18 | 6 | 343 | 262,144 | 0.13084% | 99.8692% |
| #2 Instruction Control | 22 | 8 | 327 | 4,194,304 | 0.007796% | 99.9922% |
| #3 DMA Transaction Control | 24 | 8 | 1,002 | 16,777,216 | 0.005972% | 99.9940% |
| #4 Protocol Control | 18 | 6 | 128 | 262,144 | 0.04883% | 99.9512% |
| #5 Resource Arbiter | 20 | 7 | 256 | 1,048,576 | 0.02441% | 99.9756% |
The dominant feature of Table II is not merely that the functions are incomplete; it is the scale of the incompleteness. Even the densest example, Secure Ingress, constrains only 343 of 262,144 nominal local input combinations. Instruction Control constrains 327 of 4,194,304 combinations, and the 24-input DMA example constrains 1,002 of 16,777,216. The local RTL interface therefore hides a very large completion space when viewed only as a fully specified truth table.
A. Primary Worked Example: Instruction Control
The 22-input, 8-output Instruction Control block is the primary worked example because it makes the contextual-partiality argument especially clear. In isolation, a 22-input combinational interface has 4,194,304 possible local input combinations. Within the surrounding RTL context represented by the extracted PDBF, only 327 local terms are reachable and therefore behaviorally constrained. The remaining 4,193,977 combinations—99.9922% of the nominal local domain—are contextual don’t-care terms.
A conventional fully specified representation assigns outputs to all of those unreachable combinations even though the surrounding RTL never exercises them. Fixing one Legal Completion makes those assignments part of the Boolean function presented to downstream synthesis. Completion Optimization instead treats the 327 reachable terms as invariants and retains freedom over the remaining terms while searching for a favorable implementation.
For this demonstration, the fixed-completion ABC baseline is 107 gates at 12 logic levels. GT Completion Optimization reports an implementation of 10 gates at 3 levels. Relative to that specific baseline, the reported gate count is 90.7% lower and the reported depth is 75.0% lower. The scientific significance is not the percentage alone; it is that both implementations satisfy the same 327 reachable care terms while the GT flow is allowed to choose a different completion of the 22-input function.
B. Secure Ingress
Secure Ingress provides a second detailed example from a different control domain. Its local interface has 18 inputs and 6 outputs, corresponding to 262,144 nominal local input combinations. Only 343 combinations are retained as reachable care terms, leaving 261,801 combinations, or 99.8692% of the nominal domain, contextually unspecified.
The fixed-completion ABC baseline for this Contextual PDBF is 202 gates at 22 levels, while the reported GT result is 20 gates at 5 levels. The two flows therefore illustrate the same methodological distinction as Instruction Control on a separate RTL context: one commits to a complete Boolean function before synthesis; the other searches the legal completion space while preserving the reachable behavior.
C. Cross-Domain Demonstrations
DMA Transaction Control, Protocol Control, and Resource Arbiter provide cross-domain corroboration. The 24-input DMA example has the largest nominal domain, 16,777,216 combinations, but only 1,002 reachable care terms. Protocol Control contains 128 care terms in an 18-input domain, and Resource Arbiter contains 256 care terms in a 20-input domain. These examples show that sparse contextual care domains are not limited to one particular interface width or control structure.
VII. Experimental Results
Table III reports the paired gate/level measurements used in the five-demonstration comparison. Each ABC value corresponds to conventional synthesis of the zero completion of the same Contextual PDBF. Each GT value corresponds to Completion Optimization with the reachable care relation preserved while Legal Completions are searched. Section VII-C then broadens the evaluation to 15 controlled RTL-structured PDBFs and retains the ABC Pareto set across three conventional optimization flows.
| Contextual PDBF | ABC fixed completion Gates / Levels | GT completion optimization Gates / Levels | Gate reduction* | Level reduction* |
|---|---|---|---|---|
| #1 Secure Ingress | 202 / 22 | 20 / 5 | 90.1% | 77.3% |
| #2 Instruction Control | 107 / 12 | 10 / 3 | 90.7% | 75.0% |
| #3 DMA Transaction Control | 208 / 21 | 19 / 4 | 90.9% | 81.0% |
| #4 Protocol Control | 128 / 19 | 21 / 5 | 83.6% | 73.7% |
| #5 Resource Arbiter | 121 / 13 | 19 / 7 | 84.3% | 46.2% |
Across the five demonstrations, the fixed-completion ABC baselines range from 107 to 208 gates and 12 to 22 levels. The reported GT implementations range from 10 to 21 gates and 3 to 7 levels. Relative to the paired fixed-completion baselines, gate-count reductions range from 83.6% to 90.9%, and level reductions range from 46.2% to 81.0%.
The consistency of the direction of the result across all five examples is encouraging, but the interpretation must remain controlled. The data demonstrate that the evaluated Legal Completion search found implementations substantially smaller and shallower than the evaluated fixed completions after ABC synthesis. They do not establish that GT universally outperforms ABC, nor do they isolate the contribution of completion choice from every implementation-level difference between the flows.
A. Additional DMA Corroboration
An additional 22-input DMA Transaction Control experiment was also evaluated outside the five primary package rows. For that Contextual PDBF, the fixed-completion ABC result is 126 gates at 18 levels, while the GT result is 20 gates at 4 levels. This additional point is retained as corroboration rather than mixed into the primary table because the principal DMA package used in the five-demo study is the final 24-input version.
B. What the Results Test
The experiment tests a specific hypothesis: committing early to one legal completion can remove Boolean-function-level optimization freedom. If a favorable implementation requires values on contextual don’t-care terms that differ from those in the fixed completion, conventional optimization of that fixed function cannot reach the alternative without being given equivalent don’t-care freedom. Completion Optimization searches that freedom explicitly before the circuit is finalized.
The size data in Table II make this hypothesis plausible in the evaluated RTL contexts. Each PDBF constrains only a tiny fraction of its nominal local domain. The remaining combinations create a large Legal Completion Opportunity Space. The synthesis problem is therefore not merely to simplify a fixed truth table; it is to choose how an overwhelmingly unconstrained portion of that truth table should be completed.
C. Controlled RTL-Structured PDBF Validation
To test whether the observed effect extends beyond the five primary demonstrations, a controlled suite of 15 source-independent RTL-structured Contextual PDBFs was evaluated. These cases model common RTL structures but are not claimed to be provenance-qualified reachable projections of particular upstream designs. Each original PLA is treated as the unchanged PDBF passport: every specified care assignment must be preserved, while omitted assignments remain free for Completion Optimization.
For each controlled PDBF, conventional ABC synthesis was evaluated only after the unspecified terms had been fixed to zero. Three optimization paths were retained: repeated deepsyn, independent transtoch from a fresh read of the original PLA, and chained deepsyn → transtoch. Rather than selecting one ABC recipe, the Pareto-best gate/level outcomes across all three flows are reported. GT was evaluated on the original PDBF and therefore retained freedom to search Legal Completions before circuit optimization.
| Controlled PDBF | PI/PO | Care | Contextual DC | ABC Pareto Gates/Levels | GT Gates/Levels |
|---|---|---|---|---|---|
| Instruction Decoder | 10/6 | 39 | 96.1914% | 27/4; 25/6 | 7/2 |
| ALU Control | 8/5 | 42 | 83.5938% | 22/4; 20/6 | 10/4 |
| Interrupt Priority | 8/4 | 108 | 57.8125% | 17/7 | 12/5 |
| FSM Next-State | 8/6 | 21 | 91.7969% | 32/9; 29/11 | 13/5 |
| Round-Robin Arbiter | 8/5 | 80 | 68.7500% | 32/8; 24/12 | 18/7 |
| Crossbar Route | 8/5 | 80 | 68.7500% | 14/6 | 13/5 |
| FIFO Control | 7/8 | 41 | 67.9688% | 42/8; 37/20 | 35/8 |
| Cache Controller | 8/6 | 14 | 94.5312% | 30/8; 26/9 | 12/4 |
| DMA Channel Control | 10/6 | 337 | 67.0898% | 25/9; 23/10 | 19/6 |
| AXI-Lite Protocol | 11/11 | 20 | 99.0234% | 47/7; 39/16; 38/17 | 15/3 |
| Privilege Access | 9/3 | 63 | 87.6953% | 28/7 | 14/6 |
| Address Decoder | 10/5 | 448 | 56.2500% | 14/6 | 7/2 |
| Pipeline Hazard | 11/4 | 425 | 79.2480% | 31/7 | 20/6 |
| CSR Control | 9/5 | 144 | 71.8750% | 19/5; 18/9 | 10/4 |
| Packet Router VC | 10/5 | 161 | 84.2773% | 18/7 | 3/3 |
Exhaustive functional validation was performed against the unchanged original PDBF passports. All 73 reported implementation artifacts—28 GT and 45 ABC—produce zero mismatches on every specified care assignment. In addition, every omitted input assignment was exhaustively evaluated for all 45 ABC artifacts; every such assignment produces the all-zero output vector. This independently confirms that the evaluated ABC artifacts implement the zero completion of the sparse PDBFs. Across all 15 controlled benchmarks, at least one reported GT implementation Pareto-dominates every reported ABC Pareto point in both gate count and logic depth (allowing equality in one metric where applicable).
This result should not be read as a generic GT-versus-ABC tool comparison. It compares conventional optimization after contextual freedom has been fixed to one Legal Completion—specifically the zero completion—with a flow that searches that Legal Completion freedom before circuit optimization. The controlled suite therefore isolates the methodological question more directly: can completion search expose implementations that are unavailable once the contextual don't-care space has been compiled away?
VIII. Discussion
A. Contextual Partiality as an RTL Property
The experiments support the central observation that a fully specified RTL block can induce a highly partial effective Boolean specification inside a complete design. The partiality is not introduced by weakening externally visible requirements. It follows from reachability: the surrounding design never requests behavior on the unreachable local terms.
B. Why Completion Must Precede Circuit Optimization
If contextual don’t-care terms are filled before synthesis, the selected values become part of a fully defined Boolean function. A conventional optimizer can then restructure the circuit while preserving that function, but it cannot generally reconsider the values that were fixed on formerly unspecified terms. Completion Optimization moves that decision ahead of circuit optimization and treats it as an optimization variable.
Discover contextual freedom before accidentally compiling it away.
C. Correctness and Verification
The contextual-equivalence principle requires agreement on every reachable local term, not on the entire nominal local truth table. Verification should therefore be performed with respect to the reachability assumptions that generated the Contextual PDBF. A replacement that differs from the isolated RTL on an unreachable term is legal only while that term remains unreachable in the deployed context.
This dependence on context makes extraction correctness critical. Under-approximating the reachable set could incorrectly classify a legal behavior as don’t-care. Practical flows should therefore use exact reachability when feasible or conservative over-approximations that may sacrifice optimization opportunity but do not remove required behavior.
D. Limitations of the Present Evaluation
The present study remains a feasibility evaluation. It combines five RTL-derived demonstrations with a controlled suite of 15 source-independent RTL-structured PDBFs; the latter are controlled synthesis experiments rather than provenance-qualified projections of particular upstream RTL designs. Gate count and logic levels are structural metrics and are not substitutes for technology-mapped area, timing, power, routing, or physical-design measurements. The current dataset also does not include a controlled “original RTL synthesis” baseline under a common library and constraint set. Consequently, the results should not be interpreted as end-to-end claims about production RTL synthesis.
A second limitation is that the comparison intentionally contrasts two different optimization freedoms: ABC optimizes a fully defined zero completion, whereas GT searches Legal Completions and then optimizes an implementation. The controlled 15-case experiment reduces concern about dependence on a single ABC script by retaining Pareto-best outcomes across deepsyn, independent transtoch, and chained deepsyn → transtoch, but it does not show what ABC or another synthesizer could achieve if given and allowed to retain the original incompletely specified-function freedom. Future work should compare completion-search strategies under common downstream mapping and technology constraints.
E. PDBF Passports and Reuse
Contextual PDBFs also create a reuse opportunity. Once a contextual care relation has been identified, optimized completions and their implementation characteristics can be recorded in a PDBF Passport. Repeated or structurally equivalent contextual functions could then reuse prior optimization results rather than restarting completion search from the beginning.
IX. Future Research
The immediate research agenda is to turn the demonstrated methodology into a scalable RTL synthesis flow. Important directions include:
- Symbolic, SAT-, BDD-, and formal-reachability extraction for larger sequential RTL designs.
- Automatic selection of internal blocks whose contextual care domains are likely to provide useful completion freedom.
- Hierarchical and compositional Contextual PDBFs that preserve correlations across block boundaries.
- Conservative reachability approximations with explicit correctness guarantees.
- Controlled synthesis of original RTL, fixed completions, and optimized completions under identical technology libraries and timing constraints.
- Technology mapping and physical evaluation using area, delay, power, fan-out, wiring, and routability objectives.
- Automatic PDBF Passport matching, reuse, and library growth.
A particularly important next experiment is the missing end-to-end baseline: synthesize the original RTL, a defined set of fixed Legal Completions, and GT-selected completions through the same mapping and technology flow. That experiment would separate contextual extraction, completion selection, logic optimization, and technology mapping more cleanly than the present structural comparison.
X. Conclusion
This paper extends Completion Optimization toward ordinary RTL designs by showing that fully specified local RTL can contain hidden contextual partiality. An internal block may define behavior for every nominal local input combination while the complete design reaches only a small subset. Preserving the reachable local input/output relation and leaving the unreachable terms unspecified produces a Contextual PDBF.
Five RTL-derived demonstrations make the scale of this opportunity explicit. Their nominal local spaces contain 262,144 to 16,777,216 combinations, while only 128 to 1,002 terms are reachable and constrained. The resulting contextual don't-care fractions exceed 99.86% in every example. A broader controlled suite of 15 RTL-structured PDBFs then tests the same synthesis hypothesis across a wider range of control structures.
The experimental comparison distinguishes conventional synthesis after fixing one Legal Completion from Completion Optimization that searches the Legal Completion Opportunity Space before circuit optimization. In the reported ABC flows, the fixed completion is the zero completion. For the controlled 15-case suite, three ABC optimization paths were evaluated and their Pareto-best results retained; every benchmark still has at least one GT point that Pareto-dominates the reported ABC Pareto set. All 73 implementation artifacts satisfy every specified care term, and all 45 ABC artifacts were independently confirmed to produce all-zero outputs on every omitted assignment. These results establish feasibility and broaden the evidence for completion optimization; they are not presented as a universal comparison of synthesis tools.
The larger implication is methodological. Context can reveal Boolean freedom that disappears when an internal RTL block is treated as an isolated, completely specified function. A synthesis flow that discovers this freedom before fixing the function can optimize at a level that conventional circuit optimization alone does not address.
First Discover the Contextual PDBF. Then Optimize the PDBF. Then Optimize the Circuit.
XI. References
- G. Toms, “Completion Optimization of Partially Defined Boolean Functions,” manuscript in preparation / submitted version.
- R. K. Brayton and A. Mishchenko, “ABC: An Academic Industrial-Strength Verification Tool,” in Proc. CAV, 2010.
