/**CFile**************************************************************** FileName [cecInt.h] SystemName [ABC: Logic synthesis and verification system.] PackageName [Combinational equivalence checking.] Synopsis [External declarations.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - June 20, 2005.] Revision [$Id: cecInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ #ifndef ABC__aig__cec__cecInt_h #define ABC__aig__cec__cecInt_h //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// #include "sat/bsat/satSolver.h" #include "misc/bar/bar.h" #include "aig/gia/gia.h" #include "cec.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_HEADER_START //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// // simulation pattern manager typedef struct Cec_ManPat_t_ Cec_ManPat_t; struct Cec_ManPat_t_ { Vec_Int_t * vPattern1; // pattern in terms of primary inputs Vec_Int_t * vPattern2; // pattern in terms of primary inputs Vec_Str_t * vStorage; // storage for compressed patterns int iStart; // position in the array where recent patterns begin int nPats; // total number of recent patterns int nPatsAll; // total number of all patterns int nPatLits; // total number of literals in recent patterns int nPatLitsAll; // total number of literals in all patterns int nPatLitsMin; // total number of literals in minimized recent patterns int nPatLitsMinAll; // total number of literals in minimized all patterns int nSeries; // simulation series int fVerbose; // verbose stats // runtime statistics abctime timeFind; // detecting the pattern abctime timeShrink; // minimizing the pattern abctime timeVerify; // verifying the result of minimisation abctime timeSort; // sorting literals abctime timePack; // packing into sim info structures abctime timeTotal; // total runtime abctime timeTotalSave; // total runtime for saving }; // SAT solving manager typedef struct Cec_ManSat_t_ Cec_ManSat_t; struct Cec_ManSat_t_ { // parameters Cec_ParSat_t * pPars; // AIGs used in the package Gia_Man_t * pAig; // the AIG whose outputs are considered Vec_Int_t * vStatus; // status for each output // SAT solving sat_solver * pSat; // recyclable SAT solver int nSatVars; // the counter of SAT variables int * pSatVars; // mapping of each node into its SAT var Vec_Ptr_t * vUsedNodes; // nodes whose SAT vars are assigned int nRecycles; // the number of times SAT solver was recycled int nCallsSince; // the number of calls since the last recycle Vec_Ptr_t * vFanins; // fanins of the CNF node // counter-examples Vec_Int_t * vCex; // the latest counter-example Vec_Int_t * vVisits; // temporary array for visited nodes // SAT calls statistics int nSatUnsat; // the number of proofs int nSatSat; // the number of failure int nSatUndec; // the number of timeouts int nSatTotal; // the number of calls int nCexLits; // conflicts int nConfUnsat; // conflicts in unsat problems int nConfSat; // conflicts in sat problems int nConfUndec; // conflicts in undec problems // runtime stats int timeSatUnsat; // unsat int timeSatSat; // sat int timeSatUndec; // undecided int timeTotal; // total runtime }; // combinational simulation manager typedef struct Cec_ManSim_t_ Cec_ManSim_t; struct Cec_ManSim_t_ { // parameters Gia_Man_t * pAig; // the AIG to be used for simulation Cec_ParSim_t * pPars; // simulation parameters int nWords; // the number of simulation words // recycable memory int * pSimInfo; // simulation information offsets unsigned * pMems; // allocated simulaton memory int nWordsAlloc; // the number of allocated entries int nMems; // the number of used entries int nMemsMax; // the max number of used entries int MemFree; // next free entry int nWordsOld; // the number of simulation words after previous relink // internal simulation info Vec_Ptr_t * vCiSimInfo; // CI simulation info Vec_Ptr_t * vCoSimInfo; // CO simulation info // counter examples void ** pCexes; // counter-examples for each output int iOut; // first failed output int nOuts; // the number of failed outputs Abc_Cex_t * pCexComb; // counter-example for the first failed output Abc_Cex_t * pBestState; // the state that led to most of the refinements // scoring simulation patterns int * pScores; // counters of refinement for each pattern // temporaries Vec_Int_t * vClassOld; // old class numbers Vec_Int_t * vClassNew; // new class numbers Vec_Int_t * vClassTemp; // temporary storage Vec_Int_t * vRefinedC; // refined const reprs }; // combinational simulation manager typedef struct Cec_ManFra_t_ Cec_ManFra_t; struct Cec_ManFra_t_ { // parameters Gia_Man_t * pAig; // the AIG to be used for simulation Cec_ParFra_t * pPars; // SAT sweeping parameters // simulation patterns Vec_Int_t * vXorNodes; // nodes used in speculative reduction int nAllProved; // total number of proved nodes int nAllDisproved; // total number of disproved nodes int nAllFailed; // total number of failed nodes // runtime stats abctime timeSim; // unsat abctime timePat; // unsat abctime timeSat; // sat abctime timeTotal; // total runtime }; //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// /*=== cecCorr.c ============================================================*/ extern void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, abctime Time ); /*=== cecClass.c ============================================================*/ extern int Cec_ManSimClassRemoveOne( Cec_ManSim_t * p, int i ); extern int Cec_ManSimClassesPrepare( Cec_ManSim_t * p, int LevelMax ); extern int Cec_ManSimClassesRefine( Cec_ManSim_t * p ); extern int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos ); /*=== cecIso.c ============================================================*/ extern int * Cec_ManDetectIsomorphism( Gia_Man_t * p ); /*=== cecMan.c ============================================================*/ extern Cec_ManSat_t * Cec_ManSatCreate( Gia_Man_t * pAig, Cec_ParSat_t * pPars ); extern void Cec_ManSatPrintStats( Cec_ManSat_t * p ); extern void Cec_ManSatStop( Cec_ManSat_t * p ); extern Cec_ManPat_t * Cec_ManPatStart(); extern void Cec_ManPatPrintStats( Cec_ManPat_t * p ); extern void Cec_ManPatStop( Cec_ManPat_t * p ); extern Cec_ManSim_t * Cec_ManSimStart( Gia_Man_t * pAig, Cec_ParSim_t * pPars ); extern void Cec_ManSimStop( Cec_ManSim_t * p ); extern Cec_ManFra_t * Cec_ManFraStart( Gia_Man_t * pAig, Cec_ParFra_t * pPars ); extern void Cec_ManFraStop( Cec_ManFra_t * p ); /*=== cecPat.c ============================================================*/ extern void Cec_ManPatSavePattern( Cec_ManPat_t * pPat, Cec_ManSat_t * p, Gia_Obj_t * pObj ); extern void Cec_ManPatSavePatternCSat( Cec_ManPat_t * pMan, Vec_Int_t * vPat ); extern Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t * pMan, int nInputs, int nWords ); extern Vec_Ptr_t * Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nRegs, int nWordsInit ); /*=== cecSeq.c ============================================================*/ extern int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo ); extern int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Abc_Cex_t * pBestState, int fCheckMiter ); extern void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Abc_Cex_t * pCex ); extern int Cec_ManCountNonConstOutputs( Gia_Man_t * pAig ); extern int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig ); /*=== cecSolve.c ============================================================*/ extern int Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pObj ); extern void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars ); extern void Cec_ManSatSolveCSat( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars ); extern Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats ); extern Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Str_t ** pvStatus ); extern int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj ); extern int Cec_ManSatCheckNodeTwo( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 ); extern void Cec_ManSavePattern( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 ); extern Vec_Int_t * Cec_ManSatReadCex( Cec_ManSat_t * p ); /*=== ceFraeep.c ============================================================*/ extern Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p ); extern int Cec_ManFraClassesUpdate( Cec_ManFra_t * p, Cec_ManSim_t * pSim, Cec_ManPat_t * pPat, Gia_Man_t * pNew ); ABC_NAMESPACE_HEADER_END #endif //////////////////////////////////////////////////////////////////////// /// END OF FILE /// ////////////////////////////////////////////////////////////////////////