# 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/networkFormat:

- 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.