/**CFile**************************************************************** FileName [abs.h] SystemName [ABC: Logic synthesis and verification system.] PackageName [Abstraction package.] Synopsis [External declarations.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - June 20, 2005.] Revision [$Id: abs.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ #ifndef ABC__proof_abs__Abs_h #define ABC__proof_abs__Abs_h //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// #include "aig/gia/gia.h" #include "aig/gia/giaAig.h" #include "aig/saig/saig.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_HEADER_START //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// // abstraction parameters typedef struct Abs_Par_t_ Abs_Par_t; struct Abs_Par_t_ { int nFramesMax; // maximum frames int nFramesStart; // starting frame int nFramesPast; // overlap frames int nConfLimit; // conflict limit int nLearnedMax; // max number of learned clauses int nLearnedStart; // max number of learned clauses int nLearnedDelta; // delta increase of learned clauses int nLearnedPerce; // percentage of clauses to leave int nTimeOut; // timeout in seconds int nRatioMin; // stop when less than this % of object is unabstracted int nRatioMin2; // stop when less than this % of object is unabstracted during refinement int nRatioMax; // restart when the number of abstracted object is more than this int fUseTermVars; // use terminal variables int fUseRollback; // use rollback to the starting number of frames int fPropFanout; // propagate fanout implications int fAddLayer; // refinement strategy by adding layers int fNewRefine; // uses new refinement heuristics int fUseSkip; // skip proving intermediate timeframes int fUseSimple; // use simple CNF construction int fSkipHash; // skip hashing CNF while unrolling int fUseFullProof; // use full proof for UNSAT cores int fDumpVabs; // dumps the abstracted model int fDumpMabs; // dumps the original AIG with abstraction map int fCallProver; // calls the prover int fSimpProver; // calls simplification before prover char * pFileVabs; // dumps the abstracted model into this file int fVerbose; // verbose flag int fVeryVerbose; // print additional information int iFrame; // the number of frames covered int iFrameProved; // the number of frames proved int nFramesNoChange; // the number of last frames without changes int nFramesNoChangeLim; // the number of last frames without changes to dump abstraction }; // old abstraction parameters typedef struct Gia_ParAbs_t_ Gia_ParAbs_t; struct Gia_ParAbs_t_ { int Algo; // the algorithm to be used int nFramesMax; // timeframes for PBA int nConfMax; // conflicts for PBA int fDynamic; // dynamic unfolding for PBA int fConstr; // use constraints int nFramesBmc; // timeframes for BMC int nConfMaxBmc; // conflicts for BMC int nStableMax; // the number of stable frames to quit int nRatio; // ratio of flops to quit int TimeOut; // approximate timeout in seconds int TimeOutVT; // approximate timeout in seconds int nBobPar; // Bob's parameter int fUseBdds; // use BDDs to refine abstraction int fUseDprove; // use 'dprove' to refine abstraction int fUseStart; // use starting frame int fVerbose; // verbose output int fVeryVerbose; // printing additional information int Status; // the problem status int nFramesDone; // the number of frames covered }; //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// static inline int Ga2_ObjOffset( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vMapping, Gia_ObjId(p, pObj)); } static inline int Ga2_ObjLeaveNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj)); } static inline int * Ga2_ObjLeavePtr( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntryP(p->vMapping, Ga2_ObjOffset(p, pObj) + 1); } static inline unsigned Ga2_ObjTruth( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 1); } static inline int Ga2_ObjRefNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 2); } static inline Vec_Int_t * Ga2_ObjLeaves( Gia_Man_t * p, Gia_Obj_t * pObj ) { static Vec_Int_t v; v.nSize = Ga2_ObjLeaveNum(p, pObj), v.pArray = Ga2_ObjLeavePtr(p, pObj); return &v; } //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// /*=== abs.c =========================================================*/ /*=== absDup.c =========================================================*/ extern Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses ); extern Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses ); extern void Gia_ManGlaCollect( Gia_Man_t * p, Vec_Int_t * vGateClasses, Vec_Int_t ** pvPis, Vec_Int_t ** pvPPis, Vec_Int_t ** pvFlops, Vec_Int_t ** pvNodes ); extern void Gia_ManPrintFlopClasses( Gia_Man_t * p ); extern void Gia_ManPrintObjClasses( Gia_Man_t * p ); extern void Gia_ManPrintGateClasses( Gia_Man_t * p ); /*=== absGla.c =========================================================*/ extern int Gia_ManPerformGla( Gia_Man_t * p, Abs_Par_t * pPars ); /*=== absGlaOld.c =========================================================*/ extern int Gia_ManPerformGlaOld( Gia_Man_t * p, Abs_Par_t * pPars, int fStartVta ); /*=== absIter.c =========================================================*/ extern Gia_Man_t * Gia_ManShrinkGla( Gia_Man_t * p, int nFrameMax, int nTimeOut, int fUsePdr, int fUseSat, int fUseBdd, int fVerbose ); /*=== absPth.c =========================================================*/ extern void Gia_GlaProveAbsracted( Gia_Man_t * p, int fSimpProver, int fVerbose ); extern void Gia_GlaProveCancel( int fVerbose ); extern int Gia_GlaProveCheck( int fVerbose ); /*=== absVta.c =========================================================*/ extern int Gia_VtaPerform( Gia_Man_t * pAig, Abs_Par_t * pPars ); /*=== absUtil.c =========================================================*/ extern void Abs_ParSetDefaults( Abs_Par_t * p ); extern Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta ); extern Vec_Int_t * Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames ); extern Vec_Int_t * Gia_FlaConvertToGla( Gia_Man_t * p, Vec_Int_t * vFla ); extern Vec_Int_t * Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla ); extern int Gia_GlaCountFlops( Gia_Man_t * p, Vec_Int_t * vGla ); extern int Gia_GlaCountNodes( Gia_Man_t * p, Vec_Int_t * vGla ); /*=== absRpm.c =========================================================*/ extern Gia_Man_t * Abs_RpmPerform( Gia_Man_t * p, int nCutMax, int fVerbose, int fVeryVerbose ); /*=== absRpmOld.c =========================================================*/ extern Gia_Man_t * Abs_RpmPerformOld( Gia_Man_t * p, int fVerbose ); extern void Gia_ManAbsSetDefaultParams( Gia_ParAbs_t * p ); extern Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars ); /*=== absOldCex.c ==========================================================*/ extern Vec_Int_t * Saig_ManCbaFilterFlops( Aig_Man_t * pAig, Abc_Cex_t * pAbsCex, Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAdd, int nFfsToSelect ); extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose ); /*=== absOldRef.c ==========================================================*/ extern int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose ); /*=== absOldSat.c ==========================================================*/ extern Vec_Int_t * Saig_ManExtendCounterExampleTest3( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose ); /*=== absOldSim.c ==========================================================*/ extern Vec_Int_t * Saig_ManExtendCounterExampleTest2( Aig_Man_t * p, int iFirstPi, Abc_Cex_t * pCex, int fVerbose ); ABC_NAMESPACE_HEADER_END #endif //////////////////////////////////////////////////////////////////////// /// END OF FILE /// ////////////////////////////////////////////////////////////////////////