diff options
Diffstat (limited to 'src/proof/llb/llbInt.h')
| -rw-r--r-- | src/proof/llb/llbInt.h | 212 |
1 files changed, 0 insertions, 212 deletions
diff --git a/src/proof/llb/llbInt.h b/src/proof/llb/llbInt.h deleted file mode 100644 index e2afe59a..00000000 --- a/src/proof/llb/llbInt.h +++ /dev/null @@ -1,212 +0,0 @@ -/**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 "aig/aig/aig.h" -#include "aig/saig/saig.h" -#include "proof/ssw/ssw.h" -#include "llb.h" - -#include "misc/extra/extraBdd.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, abctime 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, abctime 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, abctime 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, abctime 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, - abctime 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, abctime 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 ); -/*=== 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 /// -//////////////////////////////////////////////////////////////////////// - |