GT AND Sequential Synthesis: Exploiting Native Sequential Device PDBFs

1. Introduction

Logic synthesis has traditionally been formulated as the optimization of completely specified Boolean functions derived from a sequential specification. Once the state encoding and transition functions have been determined, conventional synthesis algorithms seek an implementation with reduced area, delay, or power while preserving specified behavior.

This formulation implicitly assumes that every combination of current state and primary inputs defines meaningful behavior. Sequential systems fundamentally differ: only a subset of all mathematically possible state/input combinations is ever reachable. The remaining combinations do not contribute to observable behavior and therefore do not constrain implementation.

Sequential logic is inherently partially defined.

GT AND Sequential Synthesis exploits this intrinsic property. Instead of immediately assigning values to unreachable behavior and optimizing one completed Boolean function, GT searches Legal Completions that preserve all reachable behavior. Conventional synthesis is then applied to the selected completion.

2. Native Sequential Device PDBFs

2.1 Sequential Specifications

A deterministic sequential device is described by a finite set of states, primary inputs, a next-state function, and an output function. Only a subset of the Cartesian state/input space is reachable during correct execution.

2.2 Reachable and Unreachable Regions

Behavior over R determines observable functionality. Behavior over U is never exercised and therefore remains unspecified.

3. Reachability Reveals the Sequential Device PDBF

Conventional reachability analysis is commonly used to eliminate unreachable states, simplify state encodings, compute sequential don’t-cares, or reduce verification complexity. GT gives reachability a broader role: it exposes the partial definition already present in the specification.

ONLY reachable behavior defines correctness.
Unreachable behavior defines optimization freedom.

4. GT AND Sequential Synthesis

1. Reachability Analysis: compute R from the specification, initial conditions, and permitted environment.
2. Sequential Device PDBF Construction: preserve next-state and output behavior over R; represent U as unspecified.
3. Completion Optimization: search SOS(SP) for Legal Completions satisfying structural objectives.
4. Logic Synthesis: optimize the selected completed Boolean representation.
5. Technology Mapping: map the optimized network to gates, standard cells, or FPGA resources.

5. Illustrative Example

5.1 Three-State Controller

The controller uses present-state bits A and B, primary input I, next-state bits A_next and B_next, and Moore output Y. State 11 is unused and unreachable.

5.2 PLA Representation

.i 3
.o 3
.ilb A B I
.ob A_next B_next Y
.type fr
.p 8
000 000
001 010
010 001
011 100
100 000
101 100
110 ---
111 ---
.e

5.3 Functional Interpretation

On every reachable combination, Y=B. GT can therefore complete the unreachable rows so that Y is implemented as a direct state-bit connection. A favorable completion for A_next is consistent with A_next=I(A+B), while B_next=IĀB̄ over reachable behavior.

5.4 Results

Relative to deepsyn, GT reduces gates by 42.9%, depth by 33.3%, and wires by 35.3%. Relative to transtoch, GT reduces gates by 33.3%, depth by 50.0%, and wires by 26.7%.

6. Experimental Evaluation on Real RTL Control Logic

6.1 Controlled Comparison

To test whether Completion Optimization remains advantageous against conventional synthesis of source-derived logic, five independently sourced control-logic candidates were evaluated under three controlled paths:

The RTL projections and contextual PDBFs were validated on their specified care domains before synthesis. The DMA, ROM-controller, and PicoRV32 proofs covered 240/240, 448/448, and 112/112 care rows, respectively; the previously completed Ibex and AXI validations were likewise exhaustive over their specified care sets. To avoid conflating representation with optimization, the zero-completion and source-derived RTL paths use conventional ABC optimization, while the GT path alone searches Legal Completions.

6.2 Pareto Results

For every evaluated candidate, at least one implementation obtained through Legal Completion search strictly Pareto-dominates every available conventional RTL-to-ABC Pareto point in both AIG AND count and maximum logic depth. Ibex improves from the conventional frontier {22/5, 16/6} to 5/2; AXI from {29/6, 27/7} to 12/4; DMA from {43/6, 39/12} to 32/5; ROM controller from {66/11, 52/18} to a GT frontier containing 43/6 and 35/17; and PicoRV32 from 13/4 to 5/3.

6.3 Comparison with the Source-Derived RTL Control

The control comparison is important because the gains cannot be attributed merely to extracting a smaller contextual Boolean problem. For OpenTitan DMA and ROM controller, ABC synthesis of the source-derived RTL produces Pareto points that are better than ABC synthesis of the fixed zero completion. For PicoRV32, the two conventional routes converge to the identical 13-AND, 4-level point. Legal Completion search nevertheless produces 32/5, 43/6, and 5/3, respectively. The additional improvement therefore appears only when the unspecified region is treated as completion freedom rather than fixed to one arbitrary assignment.

6.4 Interpretation

The five-candidate study strengthens the traffic-light proof of concept in two ways. First, the effect is reproduced across processor control, routing, DMA byte-enable generation, an encoded safety-oriented FSM, and memory-request control. Second, the source-derived RTL baseline separates the benefit of Completion Optimization from ordinary synthesis quality. The experimental result is not simply that GT beats one ABC script; rather, the Legal Completion stage exposes implementations outside the Pareto front recovered by conventional optimization of the validated source-derived logic.

7. Relationship to Completion Optimization

Once reachability partitions the sequential state/input space into R and U, the optimization problem becomes a multi-output Completion Optimization problem. Paper I provides the optimization engine. Paper II demonstrates contextual extraction in combinational RTL. Paper III establishes that sequential specifications inherently provide their own Native Sequential Device PDBFs.

8. Discussion

8.1 Scientific Contributions

The central contribution of this work is conceptual rather than merely algorithmic. Conventional sequential synthesis treats unreachable behavior primarily as a verification artifact or as information for state reduction and local simplification. GT AND Sequential Synthesis interprets unreachable behavior as functional optimization freedom that exists before logic synthesis begins.

This viewpoint identifies a previously underemphasized property of sequential specifications: partial definition is intrinsic. The Sequential Device PDBF is not generated by GT and is not an approximation. It is the exact specification restricted to behavior that can actually occur.

8.2 Compatibility with Existing Synthesis Flows

GT modifies only the completion stage. Existing synthesis engines, optimization passes, verification tools, and technology mappers require no change; they receive a more favorable completely specified Boolean representation. GT AND Sequential Synthesis therefore extends, rather than replaces, conventional sequential synthesis.

8.3 Scalability

The traffic-light controller is intentionally small and serves as a transparent proof-of-concept example. The five-candidate RTL evaluation extends that demonstration to larger real control slices while retaining exhaustive care-domain validation. For still larger controllers, explicit enumeration of the complete state/input space may be impractical. However, the methodology is independent of the reachability engine. Symbolic simulation, SAT, BDDs, formal model checking, abstraction, and compositional analysis can expose R and U without exhaustive enumeration.

The potential Sequential Opportunity Space may be extremely large because unreachable state/input combinations contribute multiple unspecified next-state and output values. Directed Search Strategies are therefore essential, as in combinational Completion Optimization. The practical cost is expected to depend on the structure and sparsity of reachable behavior rather than only on the nominal size of the complete state/input space.

8.4 Future Research

• Expansion to broader standard FSM and sequential benchmark suites.
• Protocol-aware optimization for AXI, PCI Express, USB, Ethernet, UART, SPI, I²C, CAN, and DDR controllers.
• Simultaneous optimization of state assignment, next-state logic, output logic, and unreachable behavior.
• Symbolic, SAT-based, BDD-based, and formal reachability extraction.
• Integration with the PDBF Passport Library for recognition and reuse of optimized sequential functions.
• FPGA and ASIC evaluation using technology-mapped area, delay, power, fan-out, and wiring metrics.
• Machine-learning-guided exploration of large Sequential Opportunity Spaces.
• Optimization of processor control, pipeline control, memory systems, accelerators, and safety controllers.

Native PDBFs fundamentally change the role of reachability.

9. Conclusions

This paper introduced GT AND Sequential Synthesis, a methodology that exploits optimization freedom naturally present within sequential specifications.

The central observation is that deterministic sequential systems are inherently partially defined. Only reachable state/input combinations determine observable behavior, while unreachable combinations remain unspecified. These combinations form a Sequential Device PDBF and provide optimization freedom before conventional logic synthesis begins.

Reachability analysis therefore does not create optimization opportunities. It reveals the specified reachable region R and the unspecified unreachable region U that already exist within the sequential specification. Completion Optimization can then search the resulting Sequential Opportunity Space to identify implementations with reduced logic complexity while preserving all observable behavior.

The three-state controller illustrates the mechanism. Despite containing only two unreachable state/input combinations, GT reduced the implementation from seven to four logic gates while simultaneously reducing logic depth and wiring complexity. The five-candidate RTL evaluation then provides a stronger control: in every candidate, at least one GT implementation strictly Pareto-dominates the available source-derived RTL-to-ABC Pareto front in both AIG AND count and maximum logic depth. DMA and ROM further show that source-derived RTL can outperform a fixed zero completion under ABC, while PicoRV32 makes the two conventional routes coincide at 13/4; GT still improves these cases to 32/5, 43/6, and 5/3. These observations isolate Legal Completion search as the additional optimization stage responsible for the measured structural gains.

More broadly, this work establishes a unified perspective on GT Synthesis. Paper I introduced Completion Optimization for PDBFs. Paper II showed that contextual constraints reveal PDBFs in RTL specifications. This paper demonstrates that sequential logic inherently defines Sequential Device PDBFs through unreachable behavior.

The principal conclusion is therefore not merely the introduction of a new synthesis methodology, but the recognition of a fundamental property of sequential systems.

Sequential logic is inherently partially defined.

ONLY reachable behavior defines correctness.
Unreachable behavior defines optimization freedom.

By recognizing and exploiting this intrinsic property, GT AND Sequential Synthesis introduces a new optimization stage that complements conventional synthesis while remaining compatible with established industrial design flows.

References

1. G. Toms, “Completion Optimization for Partially Defined Boolean Functions,” manuscript.
2. G. Toms, “Extending Completion Optimization to RTL Designs Through Contextual Partially Defined Boolean Functions,” manuscript.
3. R. K. Brayton and A. Mishchenko, “ABC: An Academic Industrial-Strength Verification Tool,” CAV, 2010.
4. “Finite State Machines,” All About Circuits, traffic-light controller example used as the basis for the illustrative state table.
5. lowRISC, “Ibex RISC-V Core,” RTL source project.
6. alexforencich, “Verilog AXI Stream Components,” RTL source project.
7. lowRISC, “OpenTitan,” DMA and ROM controller RTL source project.
8. YosysHQ, “PicoRV32,” RTL source project.