1 /**CFile**************************************************************** 2 3 FileName [ssw.h] 4 5 SystemName [ABC: Logic synthesis and verification system.] 6 7 PackageName [Inductive prover with constraints.] 8 9 Synopsis [External declarations.] 10 11 Author [Alan Mishchenko] 12 13 Affiliation [UC Berkeley] 14 15 Date [Ver. 1.0. Started - September 1, 2008.] 16 17 Revision [$Id: ssw.h,v 1.00 2008/09/01 00:00:00 alanmi Exp $] 18 19 ***********************************************************************/ 20 21 #ifndef ABC__aig__ssw__ssw_h 22 #define ABC__aig__ssw__ssw_h 23 24 25 //////////////////////////////////////////////////////////////////////// 26 /// INCLUDES /// 27 //////////////////////////////////////////////////////////////////////// 28 29 //////////////////////////////////////////////////////////////////////// 30 /// PARAMETERS /// 31 //////////////////////////////////////////////////////////////////////// 32 33 ABC_NAMESPACE_HEADER_START 34 35 //////////////////////////////////////////////////////////////////////// 36 /// BASIC TYPES /// 37 //////////////////////////////////////////////////////////////////////// 38 39 // choicing parameters 40 typedef struct Ssw_Pars_t_ Ssw_Pars_t; 41 struct Ssw_Pars_t_ 42 { 43 int nPartSize; // size of the partition 44 int nOverSize; // size of the overlap between partitions 45 int nFramesK; // the induction depth 46 int nFramesAddSim; // the number of additional frames to simulate 47 int fConstrs; // treat the last nConstrs POs as seq constraints 48 int fMergeFull; // enables full merge when constraints are used 49 int nMaxLevs; // the max number of levels of nodes to consider 50 int nBTLimit; // conflict limit at a node 51 int nBTLimitGlobal;// conflict limit for multiple runs 52 int nMinDomSize; // min clock domain considered for optimization 53 int nItersStop; // stop after the given number of iterations 54 int fDumpSRInit; // dumps speculative reduction 55 int nResimDelta; // the number of nodes to resimulate 56 int nStepsMax; // (scorr only) the max number of induction steps 57 int TimeLimit; // time out in seconds 58 int fPolarFlip; // uses polarity adjustment 59 int fLatchCorr; // perform register correspondence 60 int fConstCorr; // perform constant correspondence 61 int fOutputCorr; // perform 'PO correspondence' 62 int fSemiFormal; // enable semiformal filtering 63 // int fUniqueness; // enable uniqueness constraints 64 int fDynamic; // enable dynamic addition of constraints 65 int fLocalSim; // enable local simulation simulation 66 int fPartSigCorr; // uses partial signal correspondence 67 int nIsleDist; // extends islands by the given distance 68 int fScorrGia; // new signal correspondence implementation 69 int fUseCSat; // new SAT solver using when fScorrGia is selected 70 int fVerbose; // verbose stats 71 int fFlopVerbose; // verbose printout of redundant flops 72 int fEquivDump; // enables dumping equivalences 73 int fEquivDump2; // enables dumping equivalences 74 int fStopWhenGone; // stop when PO output is not a candidate constant 75 // optimized latch correspondence 76 int fLatchCorrOpt; // perform register correspondence (optimized) 77 int nSatVarMax; // max number of SAT vars before recycling SAT solver (optimized latch corr only) 78 int nRecycleCalls; // calls to perform before recycling SAT solver (optimized latch corr only) 79 // optimized signal correspondence 80 int nSatVarMax2; // max number of SAT vars before recycling SAT solver (optimized latch corr only) 81 int nRecycleCalls2;// calls to perform before recycling SAT solver (optimized latch corr only) 82 // internal parameters 83 int nIters; // the number of iterations performed 84 int nConflicts; // the total number of conflicts performed 85 // callback 86 void * pData; 87 void * pFunc; 88 }; 89 90 typedef struct Ssw_RarPars_t_ Ssw_RarPars_t; 91 struct Ssw_RarPars_t_ 92 { 93 int nFrames; 94 int nWords; 95 int nBinSize; 96 int nRounds; 97 int nRestart; 98 int nRandSeed; 99 int TimeOut; 100 int TimeOutGap; 101 int fSolveAll; 102 int fSetLastState; 103 int fVerbose; 104 int fNotVerbose; 105 int fSilent; 106 int fDropSatOuts; 107 int fMiter; 108 int fUseCex; 109 int fLatchOnly; 110 int fUseFfGrouping; 111 int nSolved; 112 Abc_Cex_t * pCex; 113 int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode 114 }; 115 116 typedef struct Ssw_Sml_t_ Ssw_Sml_t; // sequential simulation manager 117 118 //////////////////////////////////////////////////////////////////////// 119 /// MACRO DEFINITIONS /// 120 //////////////////////////////////////////////////////////////////////// 121 122 //////////////////////////////////////////////////////////////////////// 123 /// FUNCTION DECLARATIONS /// 124 //////////////////////////////////////////////////////////////////////// 125 126 /*=== sswBmc.c ==========================================================*/ 127 extern int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbose, int * piFrame ); 128 /*=== sswConstr.c ==========================================================*/ 129 extern int Ssw_ManSetConstrPhases( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits ); 130 /*=== sswCore.c ==========================================================*/ 131 extern void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ); 132 extern void Ssw_ManSetDefaultParamsLcorr( Ssw_Pars_t * p ); 133 extern Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ); 134 extern Aig_Man_t * Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ); 135 /*=== sswIslands.c ==========================================================*/ 136 extern int Ssw_SecWithSimilarityPairs( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs, Ssw_Pars_t * pPars ); 137 extern int Ssw_SecWithSimilarity( Aig_Man_t * p0, Aig_Man_t * p1, Ssw_Pars_t * pPars ); 138 /*=== sswMiter.c ===================================================*/ 139 /*=== sswPart.c ==========================================================*/ 140 extern Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars ); 141 /*=== sswPairs.c ===================================================*/ 142 extern int Ssw_MiterStatus( Aig_Man_t * p, int fVerbose ); 143 extern int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars ); 144 extern int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars ); 145 extern int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars ); 146 /*=== sswRarity.c ===================================================*/ 147 extern void Ssw_RarSetDefaultParams( Ssw_RarPars_t * p ); 148 extern int Ssw_RarSignalFilter( Aig_Man_t * pAig, Ssw_RarPars_t * pPars ); 149 extern int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars ); 150 /*=== sswSim.c ===================================================*/ 151 extern Ssw_Sml_t * Ssw_SmlSimulateComb( Aig_Man_t * pAig, int nWords ); 152 extern Ssw_Sml_t * Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords ); 153 extern void Ssw_SmlUnnormalize( Ssw_Sml_t * p ); 154 extern void Ssw_SmlStop( Ssw_Sml_t * p ); 155 extern int Ssw_SmlNumFrames( Ssw_Sml_t * p ); 156 extern int Ssw_SmlNumWordsTotal( Ssw_Sml_t * p ); 157 extern unsigned * Ssw_SmlSimInfo( Ssw_Sml_t * p, Aig_Obj_t * pObj ); 158 extern int Ssw_SmlObjsAreEqualWord( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ); 159 extern void Ssw_SmlInitializeSpecial( Ssw_Sml_t * p, Vec_Int_t * vInit ); 160 extern int Ssw_SmlCheckNonConstOutputs( Ssw_Sml_t * p ); 161 extern Vec_Ptr_t * Ssw_SmlSimDataPointers( Ssw_Sml_t * p ); 162 163 164 ABC_NAMESPACE_HEADER_END 165 166 #endif 167 168 //////////////////////////////////////////////////////////////////////// 169 /// END OF FILE /// 170 //////////////////////////////////////////////////////////////////////// 171 172