abcBridge-0.15: Bindings for ABC, A System for Sequential Synthesis and Verification

CopyrightGalois, Inc. 2010-2014
Portabilitynon-portable (language extensions)
Safe HaskellNone




Warning: The Data.ABC.AIG module has known bugs (http:/github.comGaloisIncabcBridgeissues/4) for which solutions do not currently exist. Consider using Data.ABC.GIA instead.

Data.ABC.AIG defines a set of higher level functions for manipulating and-inverter graph networks (AIG) directly from ABC. This module should be imported qualified, e.g.

import Data.ABC.AIG (AIG)
import qualified Data.ABC.AIG as AIG



data AIG s Source


newAIG :: IO (SomeGraph AIG) Source

Build a new, empty AIG graph

readAiger :: FilePath -> IO (Network Lit AIG) Source

Read an AIGER file as an AIG network

proxy :: Proxy Lit AIG Source

Proxy for building AIG networks

true :: AIG s -> Lit s Source

false :: AIG s -> Lit s Source

writeAIGManToCNFWithMapping :: Aig_Man_t -> FilePath -> IO (Vector Int) Source

Convert the network referred to by an AIG manager into CNF format and write to a file, returning a mapping from ABC object IDs to CNF variable numbers.

checkSat' :: Ptr Abc_Ntk_t -> IO SatResult Source

Returns true is the literal is satisfiabile.


data Network l g :: (* -> *) -> (* -> *) -> * where

A network is an and-invertor graph paired with it's outputs, thus representing a complete combinational circuit.


Network :: IsAIG l g => g s -> [l s] -> Network l g 

networkInputCount :: Network l g -> IO Int

Get number of inputs associated with current network.

class IsLit l => IsAIG l g | g -> l where

An And-Inverter-Graph is a data structure storing bit-level nodes.

Graphs are and-inverter graphs, which contain a number of input literals and Boolean operations for creating new literals. Every literal is part of a specific graph, and literals from different networks may not be mixed.

Both the types for literals and graphs must take a single phantom type for an arugment that is used to ensure that literals from different networks cannot be used in the same operation.




:: Proxy l g

A Proxy value, used for selecting the concrete implementation typeclass

-> (forall s. g s -> IO a)

The AIG graph computation to run

-> IO a 

Create a temporary graph, and use it to compute a result value.

newGraph :: Proxy l g -> IO (SomeGraph g)

Build a new graph instance, and packge it into the SomeGraph type that remembers the IsAIG implementation.

aigerNetwork :: Proxy l g -> FilePath -> IO (Network l g)

Read an AIG from a file, assumed to be in Aiger format

trueLit :: g s -> l s

Get unique literal in graph representing constant true.

falseLit :: g s -> l s

Get unique literal in graph representing constant false.

constant :: g s -> Bool -> l s

Generate a constant literal value

asConstant :: g s -> l s -> Maybe Bool

Return if the literal is a fixed constant. If the literal is symbolic, return Nothing.

newInput :: g s -> IO (l s)

Generate a fresh input literal

and :: g s -> l s -> l s -> IO (l s)

Compute the logical and of two literals

ands :: g s -> [l s] -> IO (l s)

Build the conjunction of a list of literals

or :: g s -> l s -> l s -> IO (l s)

Compute the logical or of two literals

eq :: g s -> l s -> l s -> IO (l s)

Compute the logical equality of two literals

implies :: g s -> l s -> l s -> IO (l s)

Compute the logical implication of two literals

xor :: g s -> l s -> l s -> IO (l s)

Compute the exclusive or of two literals

mux :: g s -> l s -> l s -> l s -> IO (l s)

Perform a mux (if-then-else on the bits).

inputCount :: g s -> IO Int

Return number of inputs in the graph.

getInput :: g s -> Int -> IO (l s)

Get input at given index in the graph.

writeAiger :: FilePath -> Network l g -> IO ()

Write network out to AIGER file.

writeCNF :: g s -> l s -> FilePath -> IO [Int]

Write network out to DIMACS CNF file. Returns vector mapping combinational inputs to CNF Variable numbers.

checkSat :: g s -> l s -> IO SatResult

Check if literal is satisfiable in network.

cec :: Network l g -> Network l g -> IO VerifyResult

Perform combinational equivalence checking.

evaluator :: g s -> [Bool] -> IO (l s -> Bool)

Evaluate the network on a set of concrete inputs.

evaluate :: Network l g -> [Bool] -> IO [Bool]

Evaluate the network on a set of concrete inputs.

litView :: g s -> l s -> IO (LitView (l s))

Examine the outermost structure of a literal to see how it was constructed

abstractEvaluateAIG :: g s -> (LitView a -> IO a) -> IO (l s -> IO a)

Build an evaluation function over an AIG using the provided view function


class IsLit l where


not :: l s -> l s

Negate a literal.

(===) :: l s -> l s -> Bool

Tests whether two lits are identical. This is only a syntactic check, and may return false even if the two literals represent the same predicate.


data SatResult :: *

Satisfiability check result.


Sat ![Bool] 

data VerifyResult :: *

Result of a verification check.


Invalid [Bool] 

data SomeGraph g :: (* -> *) -> * where

Some graph quantifies over the state phantom variable for a graph.


SomeGraph :: g s -> SomeGraph g