PV5 ⊧ ABCversatile verification and synthesis arsenal

A System for Sequential Synthesis and Verification

Application domain/field

• Sequential logic circuits
• Hardware design
• And-Inverter Graphs (AIGs)
• Sequential synthesis
• Combinational synthesis
• Binary logic circuits
• Model checking
• Equivalence checking

Type of tool

Framework for synthesis and verification of Boolean networks

Expected input

Binary logic circuit/network

Format:

• binary BLIF
• binary PLA
• BENCH format
• subset of EDIF
• subet of Synopsys equation format
• subset of structural Verilog

Expected output

The output can be given in many different formats:

• binary BLIF
• binary PLA
• BENCH format
• Synopsys equation format
• CNF
• DOT format
• GML format

Internals

ABC implements several different techniques including:

• Equivalence checking: Can be used to check if the design after synthesis is equal to the initial design.
• Model checking: Can be used to check safety properties
• Logic synthesis: transforms a Boolean network to satisfy some criteria, e.g. reduce the number of nodes.

All of this is applied to boolean networks, i.e. directed acyclic graphs (DAGs).