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

Copyright(c) Galois, Inc. 2010
LicenseBSD3
Maintainerjhendrix@galois.com
Stabilityexperimental
Portabilitynot portable (c2hs, language extensions)
Safe HaskellSafe
LanguageHaskell98

Data.ABC.Internal.ABCGlobal

Contents

Description

Incomplete. Binding of misc/util/abc_global.h which contains miscellaneous functions for ABC, including a counterexample datastructure and error handling mechanisms.

Synopsis

Counterexamples

data Abc_Cex_t_ Source

Constructors

Abc_Cex_t_ 

Fields

iPo'Abc_Cex :: Int

the zero-based number of PO, for which verification failed

iFrame'Abc_Cex :: Int

the zero-based number of the time-frame, for which verificaiton failed

nRegs'Abc_Cex :: Int

the number of registers in the miter

nPis'Abc_Cex :: Int

the number of primary inputs in the miter

nBits'Abc_Cex :: Int

the number of words of bit data used (ezyang: where by words they actually mean bits)

pData'regs'Abc_Cex :: [Bool]

The cex bit data (the number of bits: nRegs + (iFrame+1) * nPis) The format of the data is as such:

  • First, the initial values for all registers
  • Then, the iFrame+1 sets of inputs, which represent what we inputted into the network at each timestep. For a combinational network, this means there is only 1 set.
pData'inputs'Abc_Cex :: [[Bool]]

outer length: iFrame+1; inner length: nPis

peekAbcCex :: Abc_Cex_t -> IO Abc_Cex_t_ Source

Peek into the value of a Abc_Cex_t.