diff options
Diffstat (limited to 'src/proof/llb/llbInt.h')
| -rw-r--r-- | src/proof/llb/llbInt.h | 211 |
1 files changed, 211 insertions, 0 deletions
diff --git a/src/proof/llb/llbInt.h b/src/proof/llb/llbInt.h new file mode 100644 index 00000000..d81aadcf --- /dev/null +++ b/src/proof/llb/llbInt.h @@ -0,0 +1,211 @@ +/**CFile**************************************************************** + + FileName [llbInt.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: llbInt.h,v 1.00 2010/05/08 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef ABC__aig__llb__llbInt_h +#define ABC__aig__llb__llbInt_h + + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include <stdio.h> +#include "src/aig/aig/aig.h" +#include "src/aig/saig/saig.h" +#include "src/proof/ssw/ssw.h" +#include "src/misc/extra/extraBdd.h" +#include "llb.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +ABC_NAMESPACE_HEADER_START + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Llb_Man_t_ Llb_Man_t; +typedef struct Llb_Mtr_t_ Llb_Mtr_t; +typedef struct Llb_Grp_t_ Llb_Grp_t; + +struct Llb_Man_t_ +{ + Gia_ParLlb_t * pPars; // parameters + Aig_Man_t * pAigGlo; // initial AIG manager (owned by the caller) + Aig_Man_t * pAig; // derived AIG manager (created in this package) + DdManager * dd; // BDD manager + DdManager * ddG; // BDD manager + DdManager * ddR; // BDD manager + Vec_Int_t * vObj2Var; // mapping AIG ObjId into BDD var index + Vec_Int_t * vVar2Obj; // mapping BDD var index into AIG ObjId + Vec_Ptr_t * vGroups; // group Id into group pointer + Llb_Mtr_t * pMatrix; // dependency matrix + // image computation + Vec_Ptr_t * vRings; // onion rings + Vec_Int_t * vVarBegs; // the first group where the var appears + Vec_Int_t * vVarEnds; // the last group where the var appears + // variable mapping + Vec_Int_t * vNs2Glo; // next state variables into global variables + Vec_Int_t * vCs2Glo; // next state variables into global variables + Vec_Int_t * vGlo2Cs; // global variables into current state variables + Vec_Int_t * vGlo2Ns; // global variables into current state variables + // flow computation +// Vec_Int_t * vMem; +// Vec_Ptr_t * vTops; +// Vec_Ptr_t * vBots; +// Vec_Ptr_t * vCuts; +}; + +struct Llb_Mtr_t_ +{ + int nPis; // number of primary inputs + int nFfs; // number of flip-flops + int nRows; // number of rows + int nCols; // number of columns + int * pColSums; // sum of values in a column + Llb_Grp_t ** pColGrps; // group structure for each col + int * pRowSums; // sum of values in a row + char ** pMatrix; // dependency matrix + Llb_Man_t * pMan; // manager + // partial product + char * pProdVars; // variables in the partial product + int * pProdNums; // var counts in the remaining partitions +}; + +struct Llb_Grp_t_ +{ + int Id; // group ID + Vec_Ptr_t * vIns; // input AIG objs + Vec_Ptr_t * vOuts; // output AIG objs + Vec_Ptr_t * vNodes; // internal AIG objs + Llb_Man_t * pMan; // manager + Llb_Grp_t * pPrev; // previous group + Llb_Grp_t * pNext; // next group +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline int Llb_ObjBddVar( Vec_Int_t * vOrder, Aig_Obj_t * pObj ) { return Vec_IntEntry(vOrder, Aig_ObjId(pObj)); } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== llbConstr.c ======================================================*/ +extern Vec_Int_t * Llb_ManDeriveConstraints( Aig_Man_t * p ); +extern void Llb_ManPrintEntries( Aig_Man_t * p, Vec_Int_t * vCands ); +/*=== llbCore.c ======================================================*/ +extern int Llb_ManModelCheckAig( Aig_Man_t * pAigGlo, Gia_ParLlb_t * pPars, Vec_Int_t * vHints, DdManager ** pddGlo ); +/*=== llbCluster.c ======================================================*/ +extern void Llb_ManCluster( Llb_Mtr_t * p ); +/*=== llbDump.c ======================================================*/ +extern void Llb_ManDumpReached( DdManager * ddG, DdNode * bReached, char * pModel, char * pFileName ); +/*=== llbFlow.c ======================================================*/ +extern Vec_Ptr_t * Llb_ManFlow( Aig_Man_t * p, Vec_Ptr_t * vSources, int * pnFlow ); +/*=== llbHint.c ======================================================*/ +extern int Llb_ManReachabilityWithHints( Llb_Man_t * p ); +extern int Llb_ManModelCheckAigWithHints( Aig_Man_t * pAigGlo, Gia_ParLlb_t * pPars ); +/*=== llbMan.c =======================================================*/ +extern void Llb_ManPrepareVarMap( Llb_Man_t * p ); +extern Llb_Man_t * Llb_ManStart( Aig_Man_t * pAigGlo, Aig_Man_t * pAig, Gia_ParLlb_t * pPars ); +extern void Llb_ManStop( Llb_Man_t * p ); +/*=== llbMatrix.c ====================================================*/ +extern void Llb_MtrVerifyMatrix( Llb_Mtr_t * p ); +extern Llb_Mtr_t * Llb_MtrCreate( Llb_Man_t * p ); +extern void Llb_MtrFree( Llb_Mtr_t * p ); +extern void Llb_MtrPrint( Llb_Mtr_t * p, int fOrder ); +extern void Llb_MtrPrintMatrixStats( Llb_Mtr_t * p ); +/*=== llbPart.c ======================================================*/ +extern Llb_Grp_t * Llb_ManGroupAlloc( Llb_Man_t * pMan ); +extern void Llb_ManGroupStop( Llb_Grp_t * p ); +extern void Llb_ManPrepareGroups( Llb_Man_t * pMan ); +extern Llb_Grp_t * Llb_ManGroupsCombine( Llb_Grp_t * p1, Llb_Grp_t * p2 ); +extern Llb_Grp_t * Llb_ManGroupCreateFromCuts( Llb_Man_t * pMan, Vec_Int_t * vCut1, Vec_Int_t * vCut2 ); +extern void Llb_ManPrepareVarLimits( Llb_Man_t * p ); +/*=== llbPivot.c =====================================================*/ +extern int Llb_ManTracePaths( Aig_Man_t * p, Aig_Obj_t * pPivot ); +extern Vec_Int_t * Llb_ManMarkPivotNodes( Aig_Man_t * p, int fUseInternal ); +/*=== llbReach.c =====================================================*/ +extern int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo ); +/*=== llbSched.c =====================================================*/ +extern void Llb_MtrSchedule( Llb_Mtr_t * p ); + +/*=== llb2Bad.c ======================================================*/ +extern DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, int TimeOut ); +extern DdNode * Llb_BddQuantifyPis( Aig_Man_t * pInit, DdManager * dd, DdNode * bFunc ); +/*=== llb2Core.c ======================================================*/ +extern DdNode * Llb_CoreComputeCube( DdManager * dd, Vec_Int_t * vVars, int fUseVarIndex, char * pValues ); +extern int Llb_CoreExperiment( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars, Vec_Ptr_t * vResult, int TimeTarget ); +/*=== llb2Driver.c ======================================================*/ +extern Vec_Int_t * Llb_DriverCountRefs( Aig_Man_t * p ); +extern Vec_Int_t * Llb_DriverCollectNs( Aig_Man_t * pAig, Vec_Int_t * vDriRefs ); +extern Vec_Int_t * Llb_DriverCollectCs( Aig_Man_t * pAig ); +extern DdNode * Llb_DriverPhaseCube( Aig_Man_t * pAig, Vec_Int_t * vDriRefs, DdManager * dd ); +extern DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs, int TimeTarget ); +/*=== llb2Image.c ======================================================*/ +extern Vec_Ptr_t * Llb_ImgSupports( Aig_Man_t * p, Vec_Ptr_t * vDdMans, Vec_Int_t * vStart, Vec_Int_t * vStop, int fAddPis, int fVerbose ); +extern void Llb_ImgSchedule( Vec_Ptr_t * vSupps, Vec_Ptr_t ** pvQuant0, Vec_Ptr_t ** pvQuant1, int fVerbose ); +extern DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, int TimeTarget ); +extern void Llb_ImgQuantifyFirst( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, Vec_Ptr_t * vQuant0, int fVerbose ); +extern void Llb_ImgQuantifyReset( Vec_Ptr_t * vDdMans ); +extern DdNode * Llb_ImgComputeImage( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, DdManager * dd, DdNode * bInit, + Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQuant1, Vec_Int_t * vDriRefs, + int TimeTarget, int fBackward, int fReorder, int fVerbose ); + +extern DdManager * Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, int * pOrder, int fFirst, int TimeTarget ); +extern DdNode * Llb_NonlinImageCompute( DdNode * bCurrent, int fReorder, int fDrop, int fVerbose, int * pOrder ); +extern void Llb_NonlinImageQuit(); + +/*=== llb3Image.c =======================================================*/ +extern DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, + DdManager * dd, DdNode * bCurrent, int fReorder, int fVerbose, int * pOrder, int Limit, int TimeTarget ); +/*=== llb3Nonlin.c ======================================================*/ +extern DdNode * Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd ); + + +/*=== llb4Cex.c =======================================================*/ +extern Abc_Cex_t * Llb4_Nonlin4TransformCex( Aig_Man_t * pAig, Vec_Ptr_t * vStates, int iCexPo, int fVerbose ); +/*=== llb4Cluster.c =======================================================*/ +//extern void Llb_Nonlin4Cluster( Aig_Man_t * pAig, DdManager ** pdd, Vec_Int_t ** pvOrder, Vec_Ptr_t ** pvGroups, int nBddMax, int fVerbose ); +/*=== llb4Image.c =======================================================*/ +extern DdNode * Llb_Nonlin4Image( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent, Vec_Int_t * vVars2Q ); +extern Vec_Ptr_t * Llb_Nonlin4Group( DdManager * dd, Vec_Ptr_t * vParts, Vec_Int_t * vVars2Q, int nSizeMax ); +/*=== llb4Map.c =========================================================*/ +//extern Vec_Int_t * Llb_AigMap( Aig_Man_t * pAig, int nLutSize, int nLutMin ); +/*=== llb4Nonlin.c ======================================================*/ +//extern int Llb_Nonlin4CoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars ); +/*=== llb4Sweep.c ======================================================*/ +extern void Llb4_Nonlin4Sweep( Aig_Man_t * pAig, int nSweepMax, int nClusterMax, DdManager ** pdd, Vec_Int_t ** pvOrder, Vec_Ptr_t ** pvGroups, int fVerbose ); + + +ABC_NAMESPACE_HEADER_END + + + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + |