| Copyright | Galois, Inc. 2010-2014 |
|---|---|
| License | BSD3 |
| Maintainer | jhendrix@galois.com |
| Stability | experimental |
| Portability | non-portable (language extensions) |
| Safe Haskell | None |
| Language | Haskell98 |
Data.ABC.GIA
Description
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.
- data GIA s
- newGIA :: IO (SomeGraph GIA)
- data Lit s
- true :: Lit s
- false :: Lit s
- proxy :: Proxy Lit GIA
- data LitView a :: * -> *
- litView :: GIA s -> Lit s -> IO (LitView (Lit s))
- readAiger :: FilePath -> IO (Network Lit GIA)
- writeAigerWithLatches :: FilePath -> Network Lit GIA -> Int -> IO ()
- writeCNF :: GIA s -> Lit s -> FilePath -> IO [Int]
- check_exists_forall :: GIA s -> Int -> Lit s -> [Bool] -> CInt -> IO (Either String SatResult)
- data Proxy l g :: (* -> *) -> (* -> *) -> *
- data SomeGraph g :: (* -> *) -> * where
- class IsLit l where
- class IsLit l => IsAIG l g | g -> l where
- withNewGraph :: Proxy l g -> (forall s. g s -> IO a) -> IO a
- newGraph :: Proxy l g -> IO (SomeGraph g)
- aigerNetwork :: Proxy l g -> FilePath -> IO (Network l g)
- trueLit :: g s -> l s
- falseLit :: g s -> l s
- constant :: g s -> Bool -> l s
- asConstant :: g s -> l s -> Maybe Bool
- newInput :: g s -> IO (l s)
- and :: g s -> l s -> l s -> IO (l s)
- ands :: g s -> [l s] -> IO (l s)
- or :: g s -> l s -> l s -> IO (l s)
- eq :: g s -> l s -> l s -> IO (l s)
- implies :: g s -> l s -> l s -> IO (l s)
- xor :: g s -> l s -> l s -> IO (l s)
- mux :: g s -> l s -> l s -> l s -> IO (l s)
- inputCount :: g s -> IO Int
- getInput :: g s -> Int -> IO (l s)
- writeAiger :: FilePath -> Network l g -> IO ()
- checkSat :: g s -> l s -> IO SatResult
- cec :: Network l g -> Network l g -> IO VerifyResult
- evaluator :: g s -> [Bool] -> IO (l s -> Bool)
- evaluate :: Network l g -> [Bool] -> IO [Bool]
- abstractEvaluateAIG :: g s -> (LitView a -> IO a) -> IO (l s -> IO a)
- data Network l g :: (* -> *) -> (* -> *) -> * where
- data SatResult :: *
- = Unsat
- | Sat ![Bool]
- | SatUnknown
- data VerifyResult :: *
- = Valid
- | Invalid [Bool]
- | VerifyUnknown
Documentation
Building lits
Represent a literal.
Inspection
data LitView a :: * -> *
Concrete datatype representing the ways an AIG can be constructed.
litView :: GIA s -> Lit s -> IO (LitView (Lit s)) Source
Return a representation of how lit was constructed.
File 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.
writeCNF :: GIA s -> Lit s -> FilePath -> IO [Int] Source
Write a CNF file to the given path. Returns vector mapping combinational inputs to CNF Variable numbers.
QBF
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.
class IsLit l where
Methods
not :: l s -> l s
Negate a literal.
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.
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, checkSat, cec, evaluator, abstractEvaluateAIG
Methods
Arguments
| :: Proxy l g | A |
| -> (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.
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.
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.
abstractEvaluateAIG :: g s -> (LitView a -> IO a) -> IO (l s -> IO a)
Build an evaluation function over an AIG using the provided view function
data Network l g :: (* -> *) -> (* -> *) -> * where
A network is an and-invertor graph paired with it's outputs, thus representing a complete combinational circuit.
data VerifyResult :: *
Result of a verification check.
Constructors
| Valid | |
| Invalid [Bool] | |
| VerifyUnknown |
Instances