Data.ABC.GIA

GIA defines a set of functions for manipulating scalable and-inverter graph networks directly from ABC. This module should be imported qualified, e.g.

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

Scalable and-inverter graphs are briefly described at the Berkeley Verification and Synthesis Research Center's website. http://bvsrc.org/research.html#AIG%20Package It is a more memory efficient method of storing AIG graphs.

Documentation

data GIA s

An and-invertor graph network in GIA form.

Instances

IsAIG Lit GIA

newGIA :: IO (SomeGraph GIA)

Build a new empty GIA graph

Building lits

data Lit s

Represent a literal.

Instances

Traceable Lit

IsLit Lit

IsAIG Lit GIA

Eq (Lit s)

Ord (Lit s)

Storable (Lit s)

true :: Lit s

Constant true node.

false :: Lit s

Constant false node

proxy :: Proxy Lit GIA

Inspection

data LitView a :: * -> *

Concrete datatype representing the ways an AIG can be constructed.

Constructors

And !a !a

NotAnd !a !a

Input !Int

NotInput !Int

TrueLit

FalseLit

Instances

Functor LitView

Foldable LitView

Traversable LitView

TraceOutput l g x => TraceOutput l g (LitView x)

Eq a => Eq (LitView a)

Ord a => Ord (LitView a)

Show a => Show (LitView a)

File IO

readAiger :: FilePath -> IO (Network Lit GIA)

Read an AIGER file into a GIA graph

writeAigerWithLatches

Arguments

:: FilePath

-> Network Lit GIA

-> Int

Number of latches.

-> IO ()

Write an AIGER file with the given number of latches. If the number of latches is denoted by "n", then the last n inputs and last n outputs are treated as the latch input and outputs respectively. The other inputs and outputs represent primary inputs and outputs.

QBF

check_exists_forall

Arguments

:: GIA s

The GIA network used to store the terms.

-> Int

The number of existential variables.

-> Lit s

The proposition to verify.

-> [Bool]

Initial value to use in search for universal variables. (should equal number of universal variables.).

-> CInt

Number of iterations to try solver.

-> IO (Either String SatResult)

Check a formula of the form Ex.Ay p(x,y). This function takes a network where input variables are used to represent both the existentially and the universally quantified variables. The existentially quantified variables must precede the universally quantified variables, and the number of extential variables is defined by an extra Int@ paramter.

Re-exports

data Proxy l g :: (* -> *) -> (* -> *) -> *

A proxy is used to identify a specific AIG instance when calling methods that create new AIGs.

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

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

Constructors

SomeGraph :: g s -> SomeGraph g

class IsLit l where

Methods

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.

Instances

IsLit Lit

IsLit Lit

IsLit l => IsLit (TraceLit l)

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.

Minimal complete definition

aigerNetwork, trueLit, falseLit, newInput, and, inputCount, getInput, writeAiger, writeCNF, checkSat, cec, evaluator, litView, abstractEvaluateAIG

Methods

withNewGraph

Arguments

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

Instances

IsAIG Lit AIG

IsAIG Lit GIA

(IsAIG l g, Traceable l) => IsAIG (TraceLit l) (TraceGraph l g)

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

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

Constructors

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

data SatResult :: *

Satisfiability check result.

Constructors

Unsat

Sat ![Bool]

SatUnknown

Instances

Eq SatResult

Show SatResult

TraceOutput l g SatResult

data VerifyResult :: *

Result of a verification check.

Constructors

Valid

Invalid [Bool]

VerifyUnknown

Instances

Eq VerifyResult

Show VerifyResult

TraceOutput l g VerifyResult