diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-01-21 04:30:10 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-01-21 04:30:10 -0800 |
commit | 8014f25f6db719fa62336f997963532a14c568f6 (patch) | |
tree | c691ee91a3a2d452a2bd24ac89a8c717beaa7af7 /src/proof/llb/llb.h | |
parent | c44cc5de9429e6b4f1c05045fcf43c9cb96437b5 (diff) | |
download | abc-8014f25f6db719fa62336f997963532a14c568f6.tar.gz abc-8014f25f6db719fa62336f997963532a14c568f6.tar.bz2 abc-8014f25f6db719fa62336f997963532a14c568f6.zip |
Major restructuring of the code.
Diffstat (limited to 'src/proof/llb/llb.h')
-rw-r--r-- | src/proof/llb/llb.h | 96 |
1 files changed, 96 insertions, 0 deletions
diff --git a/src/proof/llb/llb.h b/src/proof/llb/llb.h new file mode 100644 index 00000000..a9bfd891 --- /dev/null +++ b/src/proof/llb/llb.h @@ -0,0 +1,96 @@ +/**CFile**************************************************************** + + FileName [llb.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [BDD-based reachability.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 8, 2010.] + + Revision [$Id: llb.h,v 1.00 2010/05/08 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef ABC__aig__llb__llb_h +#define ABC__aig__llb__llb_h + + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_HEADER_START + + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Gia_ParLlb_t_ Gia_ParLlb_t; +struct Gia_ParLlb_t_ +{ + int nBddMax; // maximum BDD size + int nIterMax; // maximum iteration count + int nClusterMax; // maximum cluster size + int nHintDepth; // the number of times to cofactor + int HintFirst; // the number of first hint to use + int fUseFlow; // use flow computation + int nVolumeMax; // the largest volume + int nVolumeMin; // the smallest volume + int nPartValue; // partitioning value + int fBackward; // enable backward reachability + int fReorder; // enable dynamic variable reordering + int fIndConstr; // extract inductive constraints + int fUsePivots; // use internal pivot variables + int fCluster; // use partition clustering + int fSchedule; // use cluster scheduling + int fDumpReached; // dump reached states into a file + int fVerbose; // print verbose information + int fVeryVerbose; // print dependency matrices + int fSilent; // do not print any infomation + int fSkipReach; // skip reachability (preparation phase only) + int fSkipOutCheck; // does not check the property output + int TimeLimit; // time limit for one reachability run + int TimeLimitGlo; // time limit for all reachability runs + // internal parameters + int TimeTarget; // the time to stop + int iFrame; // explored up to this frame +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== llbCore.c ==========================================================*/ +extern void Llb_ManSetDefaultParams( Gia_ParLlb_t * pPars ); +/*=== llb4Nonlin.c ==========================================================*/ +extern int Llb_Nonlin4CoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars ); + + + +ABC_NAMESPACE_HEADER_END + + + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + |