abc70930: src/aig/fra/fra.h Source File

00001 
00021 #ifndef __FRA_H__
00022 #define __FRA_H__
00023 
00024 #ifdef __cplusplus
00025 extern "C" {
00026 #endif 
00027 
00031 
00032 #include <stdio.h>
00033 #include <stdlib.h>
00034 #include <string.h>
00035 #include <assert.h>
00036 #include <time.h>
00037 
00038 #include "vec.h"
00039 #include "aig.h"
00040 #include "dar.h"
00041 #include "satSolver.h"
00042 #include "bar.h"
00043 
00047 
00051 
00052 typedef struct Fra_Par_t_   Fra_Par_t;
00053 typedef struct Fra_Man_t_   Fra_Man_t;
00054 typedef struct Fra_Cla_t_   Fra_Cla_t;
00055 typedef struct Fra_Sml_t_   Fra_Sml_t;
00056 typedef struct Fra_Bmc_t_   Fra_Bmc_t;
00057 
00058 // FRAIG parameters
00059 struct Fra_Par_t_
00060 {
00061     int              nSimWords;         // the number of words in the simulation info
00062     double           dSimSatur;         // the ratio of refined classes when saturation is reached
00063     int              fPatScores;        // enables simulation pattern scoring
00064     int              MaxScore;          // max score after which resimulation is used
00065     double           dActConeRatio;     // the ratio of cone to be bumped
00066     double           dActConeBumpMax;   // the largest bump in activity
00067     int              fChoicing;         // enables choicing
00068     int              fSpeculate;        // use speculative reduction
00069     int              fProve;            // prove the miter outputs
00070     int              fVerbose;          // verbose output
00071     int              fDoSparse;         // skip sparse functions
00072     int              fConeBias;         // bias variables in the cone (good for unsat runs)
00073     int              nBTLimitNode;      // conflict limit at a node
00074     int              nBTLimitMiter;     // conflict limit at an output
00075     int              nFramesP;          // the number of timeframes to in the prefix
00076     int              nFramesK;          // the number of timeframes to unroll
00077     int              nMaxImps;          // the maximum number of implications to consider
00078     int              fRewrite;          // use rewriting for constraint reduction
00079     int              fLatchCorr;        // computes latch correspondence only
00080     int              fUseImps;          // use implications
00081     int              fWriteImps;        // record implications
00082 };
00083 
00084 // FRAIG equivalence classes
00085 struct Fra_Cla_t_
00086 {
00087     Aig_Man_t *      pAig;              // the original AIG manager
00088     Aig_Obj_t **     pMemRepr;          // pointers to representatives of each node
00089     Vec_Ptr_t *      vClasses;          // equivalence classes
00090     Vec_Ptr_t *      vClasses1;         // equivalence class of Const1 node
00091     Vec_Ptr_t *      vClassesTemp;      // temporary storage for new classes
00092     Aig_Obj_t **     pMemClasses;       // memory allocated for equivalence classes
00093     Aig_Obj_t **     pMemClassesFree;   // memory allocated for equivalence classes to be used
00094     Vec_Ptr_t *      vClassOld;         // old equivalence class after splitting
00095     Vec_Ptr_t *      vClassNew;         // new equivalence class(es) after splitting
00096     int              nPairs;            // the number of pairs of nodes
00097     int              fRefinement;       // set to 1 when refinement has happened
00098     Vec_Int_t *      vImps;             // implications
00099     // procedures used for class refinement
00100     int (*pFuncNodeHash)     (Aig_Obj_t *, int);         // returns has key of the node
00101     int (*pFuncNodeIsConst)  (Aig_Obj_t *);              // returns 1 if the node is a constant
00102     int (*pFuncNodesAreEqual)(Aig_Obj_t *, Aig_Obj_t *); // returns 1 if nodes are equal up to a complement
00103 };
00104 
00105 // simulation manager
00106 struct Fra_Sml_t_
00107 {
00108     Aig_Man_t *      pAig;              // the original AIG manager
00109     int              nPref;             // the number of times frames in the prefix
00110     int              nFrames;           // the number of times frames 
00111     int              nWordsFrame;       // the number of words in each time frame
00112     int              nWordsTotal;       // the total number of words at a node
00113     int              nWordsPref;        // the number of word in the prefix
00114     int              fNonConstOut;      // have seen a non-const-0 output during simulation
00115     int              nSimRounds;        // statistics
00116     int              timeSim;           // statistics
00117     unsigned         pData[0];          // simulation data for the nodes
00118 };
00119 
00120 // FRAIG manager
00121 struct Fra_Man_t_
00122 {
00123     // high-level data    
00124     Fra_Par_t *      pPars;             // parameters governing fraiging
00125     // AIG managers
00126     Aig_Man_t *      pManAig;           // the starting AIG manager
00127     Aig_Man_t *      pManFraig;         // the final AIG manager
00128     // mapping AIG into FRAIG
00129     int              nFramesAll;        // the number of timeframes used
00130     Aig_Obj_t **     pMemFraig;         // memory allocated for points to the fraig nodes
00131     int              nSizeAlloc;        // allocated size of the arrays for timeframe nodes
00132     // equivalence classes 
00133     Fra_Cla_t *      pCla;              // representation of (candidate) equivalent nodes
00134     // simulation info
00135     Fra_Sml_t *      pSml;              // simulation manager
00136     // bounded model checking manager
00137     Fra_Bmc_t *      pBmc;
00138     // counter example storage
00139     int              nPatWords;         // the number of words in the counter example
00140     unsigned *       pPatWords;         // the counter example
00141     Vec_Int_t *      vCex;
00142     // satisfiability solving
00143     sat_solver *     pSat;              // SAT solver
00144     int              nSatVars;          // the number of variables currently used
00145     Vec_Ptr_t *      vPiVars;           // the PIs of the cone used 
00146     sint64           nBTLimitGlobal;    // resource limit
00147     sint64           nInsLimitGlobal;   // resource limit
00148     Vec_Ptr_t **     pMemFanins;        // the arrays of fanins for some FRAIG nodes
00149     int *            pMemSatNums;       // the array of SAT numbers for some FRAIG nodes
00150     int              nMemAlloc;         // allocated size of the arrays for FRAIG varnums and fanins
00151     Vec_Ptr_t *      vTimeouts;         // the nodes, for which equivalence checking timed out
00152     // statistics
00153     int              nSimRounds;
00154     int              nNodesMiter;
00155     int              nLitsBeg;
00156     int              nLitsEnd;
00157     int              nNodesBeg;
00158     int              nNodesEnd;
00159     int              nRegsBeg;
00160     int              nRegsEnd;
00161     int              nSatCalls;
00162     int              nSatCallsSat;
00163     int              nSatCallsUnsat;
00164     int              nSatProof;
00165     int              nSatFails;
00166     int              nSatFailsReal;
00167     int              nSpeculs;   
00168     int              nChoices;
00169     int              nChoicesFake;
00170     int              nSatCallsRecent;
00171     int              nSatCallsSkipped;
00172     // runtime
00173     int              timeSim;
00174     int              timeTrav;
00175     int              timeRwr;
00176     int              timeSat;
00177     int              timeSatUnsat;
00178     int              timeSatSat;
00179     int              timeSatFail;
00180     int              timeRef;
00181     int              timeTotal;
00182     int              time1;
00183     int              time2;
00184 };
00185 
00189 
00190 static inline unsigned *   Fra_ObjSim( Fra_Sml_t * p, int Id )                           { return p->pData + p->nWordsTotal * Id; }
00191 static inline unsigned     Fra_ObjRandomSim()                                            { return (rand() << 24) ^ (rand() << 12) ^ rand();                                                   }
00192 
00193 static inline Aig_Obj_t *  Fra_ObjFraig( Aig_Obj_t * pObj, int i )                       { return ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i];  }
00194 static inline void         Fra_ObjSetFraig( Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i] = pNode; }
00195 
00196 static inline Vec_Ptr_t *  Fra_ObjFaninVec( Aig_Obj_t * pObj )                           { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id];      }
00197 static inline void         Fra_ObjSetFaninVec( Aig_Obj_t * pObj, Vec_Ptr_t * vFanins )   { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id] = vFanins;   }
00198 
00199 static inline int          Fra_ObjSatNum( Aig_Obj_t * pObj )                             { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id];     }
00200 static inline void         Fra_ObjSetSatNum( Aig_Obj_t * pObj, int Num )                 { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num;      }
00201 
00202 static inline Aig_Obj_t *  Fra_ClassObjRepr( Aig_Obj_t * pObj )                          { return ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id];  }
00203 static inline void         Fra_ClassObjSetRepr( Aig_Obj_t * pObj, Aig_Obj_t * pNode )    { ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id] = pNode; }
00204 
00205 static inline Aig_Obj_t *  Fra_ObjChild0Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL;  }
00206 static inline Aig_Obj_t *  Fra_ObjChild1Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL;  }
00207 
00208 static inline int          Fra_ImpLeft( int Imp )                                        { return Imp & 0xFFFF;         }
00209 static inline int          Fra_ImpRight( int Imp )                                       { return Imp >> 16;            }
00210 static inline int          Fra_ImpCreate( int Left, int Right )                          { return (Right << 16) | Left; }
00211 
00215 
00219 
00220 /*=== fraClass.c ========================================================*/
00221 extern int                 Fra_BmcNodeIsConst( Aig_Obj_t * pObj );
00222 extern int                 Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
00223 extern void                Fra_BmcStop( Fra_Bmc_t * p );
00224 extern void                Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth );
00225 /*=== fraClass.c ========================================================*/
00226 extern Fra_Cla_t *         Fra_ClassesStart( Aig_Man_t * pAig );
00227 extern void                Fra_ClassesStop( Fra_Cla_t * p );
00228 extern void                Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed );
00229 extern void                Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose );
00230 extern void                Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr );
00231 extern int                 Fra_ClassesRefine( Fra_Cla_t * p );
00232 extern int                 Fra_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped );
00233 extern int                 Fra_ClassesCountLits( Fra_Cla_t * p );
00234 extern int                 Fra_ClassesCountPairs( Fra_Cla_t * p );
00235 extern void                Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 );
00236 extern void                Fra_ClassesLatchCorr( Fra_Man_t * p );
00237 extern void                Fra_ClassesPostprocess( Fra_Cla_t * p );
00238 extern void                Fra_ClassesSelectRepr( Fra_Cla_t * p );
00239 extern Aig_Man_t *         Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK );
00240 /*=== fraCnf.c ========================================================*/
00241 extern void                Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
00242 /*=== fraCore.c ========================================================*/
00243 extern void                Fra_FraigSweep( Fra_Man_t * pManAig );
00244 extern int                 Fra_FraigMiterStatus( Aig_Man_t * p );
00245 extern Aig_Man_t *         Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars );
00246 extern Aig_Man_t *         Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax );
00247 extern Aig_Man_t *         Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax );
00248 /*=== fraImp.c ========================================================*/
00249 extern Vec_Int_t *         Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr );
00250 extern void                Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums );
00251 extern int                 Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, int Pos );
00252 extern int                 Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps );
00253 extern void                Fra_ImpCompactArray( Vec_Int_t * vImps );
00254 extern double              Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p );
00255 extern int                 Fra_ImpVerifyUsingSimulation( Fra_Man_t * p );
00256 extern void                Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew );
00257 /*=== fraInd.c ========================================================*/
00258 extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter );
00259 /*=== fraLcr.c ========================================================*/
00260 extern Aig_Man_t *         Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter );
00261 /*=== fraMan.c ========================================================*/
00262 extern void                Fra_ParamsDefault( Fra_Par_t * pParams );
00263 extern void                Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
00264 extern Fra_Man_t *         Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pParams );
00265 extern void                Fra_ManClean( Fra_Man_t * p, int nNodesMax );
00266 extern Aig_Man_t *         Fra_ManPrepareComb( Fra_Man_t * p );
00267 extern void                Fra_ManFinalizeComb( Fra_Man_t * p );
00268 extern void                Fra_ManStop( Fra_Man_t * p );
00269 extern void                Fra_ManPrint( Fra_Man_t * p );
00270 /*=== fraSat.c ========================================================*/
00271 extern int                 Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
00272 extern int                 Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR );
00273 extern int                 Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew );
00274 /*=== fraSec.c ========================================================*/
00275 extern int                 Fra_FraigSec( Aig_Man_t * p, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose );
00276 /*=== fraSim.c ========================================================*/
00277 extern int                 Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize );
00278 extern int                 Fra_SmlNodeIsConst( Aig_Obj_t * pObj );
00279 extern int                 Fra_SmlNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
00280 extern int                 Fra_SmlNodeNotEquWeight( Fra_Sml_t * p, int Left, int Right );
00281 extern int                 Fra_SmlCheckOutput( Fra_Man_t * p );
00282 extern void                Fra_SmlSavePattern( Fra_Man_t * p );
00283 extern void                Fra_SmlSimulate( Fra_Man_t * p, int fInit );
00284 extern void                Fra_SmlResimulate( Fra_Man_t * p );
00285 extern Fra_Sml_t *         Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame );
00286 extern void                Fra_SmlStop( Fra_Sml_t * p );
00287 extern Fra_Sml_t *         Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords );
00288 extern Fra_Sml_t *         Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords );
00289 
00290 
00291 #ifdef __cplusplus
00292 }
00293 #endif
00294 
00295 #endif
00296 
00300