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

Copyright(c) Galois, Inc. 2010-2014
LicenseBSD3
Maintainerjhendrix@galois.com
Stabilityexperimental
Portabilityportable
Safe HaskellNone
LanguageHaskell98

Data.ABC

Contents

Description

Contains main interface to ABC, a system for sequential synthesis and verification.

ABC provides many functions for manipulating Boolean networks. Internally, ABC provides two different ways of representing them: the older AIG interface, and a newer GIA interface. This library exposes both interfaces, along with a handful of functions for manipulating them.

Synopsis

Library setup and teardown

initialize :: IO () Source #

Initializes the ABC engine. This function may be safely called multiple times. Higher-level functions will automatically call this function, so it is only needed if using the FFI interfaces directly.

unsafeCleanup :: IO () Source #

Deinitializes the ABC engine. ABC operations may not be run after this function is called. Use with care; this may cause ABC datatypes to stop working.

Standard ABC interface

data AIG s Source #

Instances

IsAIG Lit AIG Source # 

Methods

withNewGraph :: Proxy Lit AIG -> (forall s. AIG s -> IO a) -> IO a #

newGraph :: Proxy Lit AIG -> IO (SomeGraph AIG) #

aigerNetwork :: Proxy Lit AIG -> FilePath -> IO (Network Lit AIG) #

trueLit :: AIG s -> Lit s #

falseLit :: AIG s -> Lit s #

constant :: AIG s -> Bool -> Lit s #

asConstant :: AIG s -> Lit s -> Maybe Bool #

newInput :: AIG s -> IO (Lit s) #

and :: AIG s -> Lit s -> Lit s -> IO (Lit s) #

ands :: AIG s -> [Lit s] -> IO (Lit s) #

or :: AIG s -> Lit s -> Lit s -> IO (Lit s) #

eq :: AIG s -> Lit s -> Lit s -> IO (Lit s) #

implies :: AIG s -> Lit s -> Lit s -> IO (Lit s) #

xor :: AIG s -> Lit s -> Lit s -> IO (Lit s) #

mux :: AIG s -> Lit s -> Lit s -> Lit s -> IO (Lit s) #

inputCount :: AIG s -> IO Int #

getInput :: AIG s -> Int -> IO (Lit s) #

writeAiger :: FilePath -> Network Lit AIG -> IO () #

writeCNF :: AIG s -> Lit s -> FilePath -> IO [Int] #

checkSat :: AIG s -> Lit s -> IO SatResult #

cec :: Network Lit AIG -> Network Lit AIG -> IO VerifyResult #

evaluator :: AIG s -> [Bool] -> IO (Lit s -> Bool) #

evaluate :: Network Lit AIG -> [Bool] -> IO [Bool] #

litView :: AIG s -> Lit s -> IO (LitView (Lit s)) #

abstractEvaluateAIG :: AIG s -> (LitView a -> IO a) -> IO (Lit s -> IO a) #

type AIGLit = Lit Source #

aigNetwork :: Proxy AIGLit AIG Source #

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.

Proxy for AIG interface.

newAIG :: IO (SomeGraph AIG) Source #

Build a new, empty AIG graph

readAigerAsAIG :: FilePath -> IO (Network AIGLit AIG) Source #

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.

Read an AIGER file as an AIG network.

New style ABC representation

data GIA s Source #

An and-invertor graph network in GIA form.

Instances

IsAIG Lit GIA Source # 

Methods

withNewGraph :: Proxy Lit GIA -> (forall s. GIA s -> IO a) -> IO a #

newGraph :: Proxy Lit GIA -> IO (SomeGraph GIA) #

aigerNetwork :: Proxy Lit GIA -> FilePath -> IO (Network Lit GIA) #

trueLit :: GIA s -> Lit s #

falseLit :: GIA s -> Lit s #

constant :: GIA s -> Bool -> Lit s #

asConstant :: GIA s -> Lit s -> Maybe Bool #

newInput :: GIA s -> IO (Lit s) #

and :: GIA s -> Lit s -> Lit s -> IO (Lit s) #

ands :: GIA s -> [Lit s] -> IO (Lit s) #

or :: GIA s -> Lit s -> Lit s -> IO (Lit s) #

eq :: GIA s -> Lit s -> Lit s -> IO (Lit s) #

implies :: GIA s -> Lit s -> Lit s -> IO (Lit s) #

xor :: GIA s -> Lit s -> Lit s -> IO (Lit s) #

mux :: GIA s -> Lit s -> Lit s -> Lit s -> IO (Lit s) #

inputCount :: GIA s -> IO Int #

getInput :: GIA s -> Int -> IO (Lit s) #

writeAiger :: FilePath -> Network Lit GIA -> IO () #

writeCNF :: GIA s -> Lit s -> FilePath -> IO [Int] #

checkSat :: GIA s -> Lit s -> IO SatResult #

cec :: Network Lit GIA -> Network Lit GIA -> IO VerifyResult #

evaluator :: GIA s -> [Bool] -> IO (Lit s -> Bool) #

evaluate :: Network Lit GIA -> [Bool] -> IO [Bool] #

litView :: GIA s -> Lit s -> IO (LitView (Lit s)) #

abstractEvaluateAIG :: GIA s -> (LitView a -> IO a) -> IO (Lit s -> IO a) #

type GIALit = Lit Source #

giaNetwork :: Proxy GIALit GIA Source #

Proxy for GIA interface.

newGIA :: IO (SomeGraph GIA) Source #

Build a new empty GIA graph

readAigerAsGIA :: FilePath -> IO (Network GIALit GIA) Source #

Read an AIGER file as a GIA network.

module Data.AIG