fra.h 22.9 KB
Newer Older
Alan Mishchenko committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
/**CFile****************************************************************

  FileName    [fra.h]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [[New FRAIG package.]

  Synopsis    [External declarations.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 30, 2007.]

  Revision    [$Id: fra.h,v 1.00 2007/06/30 00:00:00 alanmi Exp $]

***********************************************************************/

21 22
#ifndef ABC__aig__fra__fra_h
#define ABC__aig__fra__fra_h
Alan Mishchenko committed
23

24

Alan Mishchenko committed
25 26 27 28 29 30 31 32 33
////////////////////////////////////////////////////////////////////////
///                          INCLUDES                                ///
////////////////////////////////////////////////////////////////////////

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>

34 35 36 37 38
#include "misc/vec/vec.h"
#include "aig/aig/aig.h"
#include "opt/dar/dar.h"
#include "sat/bsat/satSolver.h"
#include "aig/ioa/ioa.h"
Alan Mishchenko committed
39 40 41 42 43

////////////////////////////////////////////////////////////////////////
///                         PARAMETERS                               ///
////////////////////////////////////////////////////////////////////////

44 45 46 47


ABC_NAMESPACE_HEADER_START
 
Alan Mishchenko committed
48

Alan Mishchenko committed
49 50 51 52 53
////////////////////////////////////////////////////////////////////////
///                         BASIC TYPES                              ///
////////////////////////////////////////////////////////////////////////

typedef struct Fra_Par_t_   Fra_Par_t;
Alan Mishchenko committed
54
typedef struct Fra_Ssw_t_   Fra_Ssw_t;
Alan Mishchenko committed
55
typedef struct Fra_Sec_t_   Fra_Sec_t;
Alan Mishchenko committed
56
typedef struct Fra_Man_t_   Fra_Man_t;
Alan Mishchenko committed
57 58
typedef struct Fra_Cla_t_   Fra_Cla_t;
typedef struct Fra_Sml_t_   Fra_Sml_t;
Alan Mishchenko committed
59
typedef struct Fra_Bmc_t_   Fra_Bmc_t;
Alan Mishchenko committed
60 61 62 63 64 65 66 67 68 69

// FRAIG parameters
struct Fra_Par_t_
{
    int              nSimWords;         // the number of words in the simulation info
    double           dSimSatur;         // the ratio of refined classes when saturation is reached
    int              fPatScores;        // enables simulation pattern scoring
    int              MaxScore;          // max score after which resimulation is used
    double           dActConeRatio;     // the ratio of cone to be bumped
    double           dActConeBumpMax;   // the largest bump in activity
Alan Mishchenko committed
70
    int              fChoicing;         // enables choicing
Alan Mishchenko committed
71 72 73 74
    int              fSpeculate;        // use speculative reduction
    int              fProve;            // prove the miter outputs
    int              fVerbose;          // verbose output
    int              fDoSparse;         // skip sparse functions
Alan Mishchenko committed
75
    int              fConeBias;         // bias variables in the cone (good for unsat runs)
Alan Mishchenko committed
76 77
    int              nBTLimitNode;      // conflict limit at a node
    int              nBTLimitMiter;     // conflict limit at an output
Alan Mishchenko committed
78
    int              nLevelMax;         // the max level to consider seriously
Alan Mishchenko committed
79
    int              nFramesP;          // the number of timeframes to in the prefix
Alan Mishchenko committed
80
    int              nFramesK;          // the number of timeframes to unroll
Alan Mishchenko committed
81
    int              nMaxImps;          // the maximum number of implications to consider
Alan Mishchenko committed
82
    int              nMaxLevs;          // the maximum number of levels to consider
Alan Mishchenko committed
83
    int              fRewrite;          // use rewriting for constraint reduction
Alan Mishchenko committed
84
    int              fLatchCorr;        // computes latch correspondence only
Alan Mishchenko committed
85
    int              fUseImps;          // use implications
Alan Mishchenko committed
86
    int              fUse1Hot;          // use one-hotness conditions
Alan Mishchenko committed
87
    int              fWriteImps;        // record implications
Alan Mishchenko committed
88
    int              fDontShowBar;      // does not show progressbar during fraiging
Alan Mishchenko committed
89 90
};

Alan Mishchenko committed
91
// seq SAT sweeping parameters
Alan Mishchenko committed
92 93 94 95 96 97 98 99
struct Fra_Ssw_t_
{
    int              nPartSize;         // size of the partition
    int              nOverSize;         // size of the overlap between partitions
    int              nFramesP;          // number of frames in the prefix
    int              nFramesK;          // number of frames for induction (1=simple) 
    int              nMaxImps;          // max implications to consider
    int              nMaxLevs;          // max levels to consider
Alan Mishchenko committed
100
    int              nMinDomSize;       // min clock domain considered for optimization
Alan Mishchenko committed
101 102 103 104 105 106 107
    int              fUseImps;          // use implications  
    int              fRewrite;          // enable rewriting of the specualatively reduced model
    int              fFraiging;         // enable comb SAT sweeping as preprocessing 
    int              fLatchCorr;        // perform register correspondence
    int              fWriteImps;        // write implications into a file
    int              fUse1Hot;          // use one-hotness constraints
    int              fVerbose;          // enable verbose output 
Alan Mishchenko committed
108
    int              fSilent;           // disable any output 
Alan Mishchenko committed
109
    int              nIters;            // the number of iterations performed
Alan Mishchenko committed
110
    float            TimeLimit;         // the runtime budget for this call
Alan Mishchenko committed
111 112
};

Alan Mishchenko committed
113 114 115 116 117 118
// SEC parametesr
struct Fra_Sec_t_
{
    int              fTryComb;          // try CEC call as a preprocessing step
    int              fTryBmc;           // try BMC call as a preprocessing step 
    int              nFramesMax;        // the max number of frames used for induction
Alan Mishchenko committed
119 120
    int              nBTLimit;          // the conflict limit at a node
    int              nBTLimitGlobal;    // the global conflict limit
Alan Mishchenko committed
121 122
    int              nBTLimitInter;     // the conflict limit for interpolation
    int              nBddVarsMax;       // the state space limit for BDD reachability
Alan Mishchenko committed
123 124
    int              nBddMax;           // the max number of BDD nodes
    int              nBddIterMax;       // the limit on the number of BDD iterations
125
    int              nPdrTimeout;       // the timeout for PDR in the end
Alan Mishchenko committed
126 127 128 129
    int              fPhaseAbstract;    // enables phase abstraction
    int              fRetimeFirst;      // enables most-forward retiming at the beginning
    int              fRetimeRegs;       // enables min-register retiming at the beginning
    int              fFraiging;         // enables fraiging at the beginning
Alan Mishchenko committed
130
    int              fInduction;        // enable the use of induction
Alan Mishchenko committed
131
    int              fInterpolation;    // enables interpolation
Alan Mishchenko committed
132
    int              fInterSeparate;    // enables interpolation for each outputs separately
Alan Mishchenko committed
133
    int              fReachability;     // enables BDD based reachability
Alan Mishchenko committed
134
    int              fReorderImage;     // enables BDD reordering during image computation
Alan Mishchenko committed
135
    int              fStopOnFirstFail;  // enables stopping after first output of a miter has failed to prove
Alan Mishchenko committed
136
    int              fUseNewProver;     // the new prover
137
    int              fUsePdr;           // the PDR
Alan Mishchenko committed
138
    int              fSilent;           // disables all output
Alan Mishchenko committed
139 140 141
    int              fVerbose;          // enables verbose reporting of statistics
    int              fVeryVerbose;      // enables very verbose reporting  
    int              TimeLimit;         // enables the timeout
Alan Mishchenko committed
142 143
    int              fReadUnsolved;     // inserts the unsolved model back
    int              nSMnumber;         // the number of model written
Alan Mishchenko committed
144 145 146 147 148
    // internal parameters
    int              fRecursive;        // set to 1 when SEC is called recursively
    int              fReportSolution;   // enables report solution in a special form
};

Alan Mishchenko committed
149 150 151 152 153 154 155 156 157 158 159 160 161 162
// FRAIG equivalence classes
struct Fra_Cla_t_
{
    Aig_Man_t *      pAig;              // the original AIG manager
    Aig_Obj_t **     pMemRepr;          // pointers to representatives of each node
    Vec_Ptr_t *      vClasses;          // equivalence classes
    Vec_Ptr_t *      vClasses1;         // equivalence class of Const1 node
    Vec_Ptr_t *      vClassesTemp;      // temporary storage for new classes
    Aig_Obj_t **     pMemClasses;       // memory allocated for equivalence classes
    Aig_Obj_t **     pMemClassesFree;   // memory allocated for equivalence classes to be used
    Vec_Ptr_t *      vClassOld;         // old equivalence class after splitting
    Vec_Ptr_t *      vClassNew;         // new equivalence class(es) after splitting
    int              nPairs;            // the number of pairs of nodes
    int              fRefinement;       // set to 1 when refinement has happened
Alan Mishchenko committed
163
    Vec_Int_t *      vImps;             // implications
Alan Mishchenko committed
164 165 166 167
    // procedures used for class refinement
    int (*pFuncNodeHash)     (Aig_Obj_t *, int);         // returns has key of the node
    int (*pFuncNodeIsConst)  (Aig_Obj_t *);              // returns 1 if the node is a constant
    int (*pFuncNodesAreEqual)(Aig_Obj_t *, Aig_Obj_t *); // returns 1 if nodes are equal up to a complement
Alan Mishchenko committed
168 169 170 171 172 173
};

// simulation manager
struct Fra_Sml_t_
{
    Aig_Man_t *      pAig;              // the original AIG manager
Alan Mishchenko committed
174 175
    int              nPref;             // the number of times frames in the prefix
    int              nFrames;           // the number of times frames 
Alan Mishchenko committed
176 177
    int              nWordsFrame;       // the number of words in each time frame
    int              nWordsTotal;       // the total number of words at a node
Alan Mishchenko committed
178
    int              nWordsPref;        // the number of word in the prefix
Alan Mishchenko committed
179
    int              fNonConstOut;      // have seen a non-const-0 output during simulation
Alan Mishchenko committed
180 181 182
    int              nSimRounds;        // statistics
    int              timeSim;           // statistics
    unsigned         pData[0];          // simulation data for the nodes
Alan Mishchenko committed
183 184 185 186 187 188 189 190
};

// FRAIG manager
struct Fra_Man_t_
{
    // high-level data    
    Fra_Par_t *      pPars;             // parameters governing fraiging
    // AIG managers
Alan Mishchenko committed
191 192
    Aig_Man_t *      pManAig;           // the starting AIG manager
    Aig_Man_t *      pManFraig;         // the final AIG manager
Alan Mishchenko committed
193
    // mapping AIG into FRAIG
Alan Mishchenko committed
194
    int              nFramesAll;        // the number of timeframes used
Alan Mishchenko committed
195
    Aig_Obj_t **     pMemFraig;         // memory allocated for points to the fraig nodes
Alan Mishchenko committed
196
    int              nSizeAlloc;        // allocated size of the arrays for timeframe nodes
Alan Mishchenko committed
197 198
    // equivalence classes 
    Fra_Cla_t *      pCla;              // representation of (candidate) equivalent nodes
Alan Mishchenko committed
199
    // simulation info
Alan Mishchenko committed
200
    Fra_Sml_t *      pSml;              // simulation manager
Alan Mishchenko committed
201 202
    // bounded model checking manager
    Fra_Bmc_t *      pBmc;
Alan Mishchenko committed
203 204 205
    // counter example storage
    int              nPatWords;         // the number of words in the counter example
    unsigned *       pPatWords;         // the counter example
Alan Mishchenko committed
206
    Vec_Int_t *      vCex;
Alan Mishchenko committed
207 208
    // one-hotness conditions
    Vec_Int_t *      vOneHots;          
Alan Mishchenko committed
209
    // satisfiability solving
Alan Mishchenko committed
210 211 212
    sat_solver *     pSat;              // SAT solver
    int              nSatVars;          // the number of variables currently used
    Vec_Ptr_t *      vPiVars;           // the PIs of the cone used 
Alan Mishchenko committed
213 214
    ABC_INT64_T           nBTLimitGlobal;    // resource limit
    ABC_INT64_T           nInsLimitGlobal;   // resource limit
Alan Mishchenko committed
215 216
    Vec_Ptr_t **     pMemFanins;        // the arrays of fanins for some FRAIG nodes
    int *            pMemSatNums;       // the array of SAT numbers for some FRAIG nodes
Alan Mishchenko committed
217
    int              nMemAlloc;         // allocated size of the arrays for FRAIG varnums and fanins
Alan Mishchenko committed
218
    Vec_Ptr_t *      vTimeouts;         // the nodes, for which equivalence checking timed out
Alan Mishchenko committed
219 220 221
    // statistics
    int              nSimRounds;
    int              nNodesMiter;
Alan Mishchenko committed
222 223 224 225 226 227
    int              nLitsBeg;
    int              nLitsEnd;
    int              nNodesBeg;
    int              nNodesEnd;
    int              nRegsBeg;
    int              nRegsEnd;
Alan Mishchenko committed
228 229 230 231 232 233
    int              nSatCalls;
    int              nSatCallsSat;
    int              nSatCallsUnsat;
    int              nSatProof;
    int              nSatFails;
    int              nSatFailsReal;
Alan Mishchenko committed
234 235 236
    int              nSpeculs;   
    int              nChoices;
    int              nChoicesFake;
Alan Mishchenko committed
237 238
    int              nSatCallsRecent;
    int              nSatCallsSkipped;
Alan Mishchenko committed
239
    // runtime
240 241 242 243 244 245 246 247 248 249 250
    clock_t          timeSim;
    clock_t          timeTrav;
    clock_t          timeRwr;
    clock_t          timeSat;
    clock_t          timeSatUnsat;
    clock_t          timeSatSat;
    clock_t          timeSatFail;
    clock_t          timeRef;
    clock_t          timeTotal;
    clock_t          time1;
    clock_t          time2;
Alan Mishchenko committed
251 252 253 254 255 256
};

////////////////////////////////////////////////////////////////////////
///                      MACRO DEFINITIONS                           ///
////////////////////////////////////////////////////////////////////////

Alan Mishchenko committed
257
static inline unsigned *   Fra_ObjSim( Fra_Sml_t * p, int Id )                           { return p->pData + p->nWordsTotal * Id; }
Alan Mishchenko committed
258
static inline unsigned     Fra_ObjRandomSim()                                            { return Aig_ManRandom(0);               }
Alan Mishchenko committed
259

Alan Mishchenko committed
260 261
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];  }
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; }
Alan Mishchenko committed
262

Alan Mishchenko committed
263 264
static inline Vec_Ptr_t *  Fra_ObjFaninVec( Aig_Obj_t * pObj )                           { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id];      }
static inline void         Fra_ObjSetFaninVec( Aig_Obj_t * pObj, Vec_Ptr_t * vFanins )   { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id] = vFanins;   }
Alan Mishchenko committed
265

Alan Mishchenko committed
266 267
static inline int          Fra_ObjSatNum( Aig_Obj_t * pObj )                             { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id];     }
static inline void         Fra_ObjSetSatNum( Aig_Obj_t * pObj, int Num )                 { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num;      }
Alan Mishchenko committed
268

Alan Mishchenko committed
269 270
static inline Aig_Obj_t *  Fra_ClassObjRepr( Aig_Obj_t * pObj )                          { return ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id];  }
static inline void         Fra_ClassObjSetRepr( Aig_Obj_t * pObj, Aig_Obj_t * pNode )    { ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id] = pNode; }
Alan Mishchenko committed
271

Alan Mishchenko committed
272 273
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;  }
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;  }
Alan Mishchenko committed
274

Alan Mishchenko committed
275 276 277 278
static inline int          Fra_ImpLeft( int Imp )                                        { return Imp & 0xFFFF;         }
static inline int          Fra_ImpRight( int Imp )                                       { return Imp >> 16;            }
static inline int          Fra_ImpCreate( int Left, int Right )                          { return (Right << 16) | Left; }

Alan Mishchenko committed
279 280 281 282 283 284 285 286
////////////////////////////////////////////////////////////////////////
///                         ITERATORS                                ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                    FUNCTION DECLARATIONS                         ///
////////////////////////////////////////////////////////////////////////

Alan Mishchenko committed
287
/*=== fraCec.c ========================================================*/
288
extern int                 Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
Alan Mishchenko committed
289 290
extern int                 Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose );
extern int                 Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose );
Alan Mishchenko committed
291
/*=== fraClass.c ========================================================*/
Alan Mishchenko committed
292 293 294 295
extern int                 Fra_BmcNodeIsConst( Aig_Obj_t * pObj );
extern int                 Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
extern void                Fra_BmcStop( Fra_Bmc_t * p );
extern void                Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth );
Alan Mishchenko committed
296
extern void                Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRewrite, int fVerbose );
Alan Mishchenko committed
297
/*=== fraClass.c ========================================================*/
Alan Mishchenko committed
298 299 300
extern Fra_Cla_t *         Fra_ClassesStart( Aig_Man_t * pAig );
extern void                Fra_ClassesStop( Fra_Cla_t * p );
extern void                Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed );
Alan Mishchenko committed
301
extern void                Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose );
Alan Mishchenko committed
302
extern void                Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs );
Alan Mishchenko committed
303
extern int                 Fra_ClassesRefine( Fra_Cla_t * p );
Alan Mishchenko committed
304
extern int                 Fra_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped );
Alan Mishchenko committed
305
extern int                 Fra_ClassesCountLits( Fra_Cla_t * p );
Alan Mishchenko committed
306 307
extern int                 Fra_ClassesCountPairs( Fra_Cla_t * p );
extern void                Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 );
Alan Mishchenko committed
308
extern void                Fra_ClassesLatchCorr( Fra_Man_t * p );
Alan Mishchenko committed
309
extern void                Fra_ClassesPostprocess( Fra_Cla_t * p );
Alan Mishchenko committed
310 311
extern void                Fra_ClassesSelectRepr( Fra_Cla_t * p );
extern Aig_Man_t *         Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK );
Alan Mishchenko committed
312
/*=== fraCnf.c ========================================================*/
Alan Mishchenko committed
313
extern void                Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
Alan Mishchenko committed
314
/*=== fraCore.c ========================================================*/
Alan Mishchenko committed
315
extern void                Fra_FraigSweep( Fra_Man_t * pManAig );
Alan Mishchenko committed
316
extern int                 Fra_FraigMiterStatus( Aig_Man_t * p );
Alan Mishchenko committed
317
extern int                 Fra_FraigMiterAssertedOutput( Aig_Man_t * p );
Alan Mishchenko committed
318
extern Aig_Man_t *         Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars );
Alan Mishchenko committed
319
extern Aig_Man_t *         Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax, int nLevelMax );
Alan Mishchenko committed
320
extern Aig_Man_t *         Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve );
Alan Mishchenko committed
321 322 323 324 325 326 327 328
/*=== fraHot.c ========================================================*/
extern Vec_Int_t *         Fra_OneHotCompute( Fra_Man_t * p, Fra_Sml_t * pSim );
extern void                Fra_OneHotAssume( Fra_Man_t * p, Vec_Int_t * vOneHots );
extern void                Fra_OneHotCheck( Fra_Man_t * p, Vec_Int_t * vOneHots );
extern int                 Fra_OneHotRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vOneHots );
extern int                 Fra_OneHotCount( Fra_Man_t * p, Vec_Int_t * vOneHots );
extern void                Fra_OneHotEstimateCoverage( Fra_Man_t * p, Vec_Int_t * vOneHots );
extern Aig_Man_t *         Fra_OneHotCreateExdc( Fra_Man_t * p, Vec_Int_t * vOneHots );
Alan Mishchenko committed
329
extern void                Fra_OneHotAddKnownConstraint( Fra_Man_t * p, Vec_Ptr_t * vOnehots );
Alan Mishchenko committed
330 331 332 333 334 335
/*=== fraImp.c ========================================================*/
extern Vec_Int_t *         Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr );
extern void                Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums );
extern int                 Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, int Pos );
extern int                 Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps );
extern void                Fra_ImpCompactArray( Vec_Int_t * vImps );
Alan Mishchenko committed
336 337 338
extern double              Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p );
extern int                 Fra_ImpVerifyUsingSimulation( Fra_Man_t * p );
extern void                Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew );
Alan Mishchenko committed
339
/*=== fraInd.c ========================================================*/
Alan Mishchenko committed
340
extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, Fra_Ssw_t * pPars );
Alan Mishchenko committed
341 342
/*=== fraIndVer.c =====================================================*/
extern int                 Fra_InvariantVerify( Aig_Man_t * p, int nFrames, Vec_Int_t * vClauses, Vec_Int_t * vLits );
Alan Mishchenko committed
343
/*=== fraLcr.c ========================================================*/
Alan Mishchenko committed
344
extern Aig_Man_t *         Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter, float TimeLimit );
Alan Mishchenko committed
345 346
/*=== fraMan.c ========================================================*/
extern void                Fra_ParamsDefault( Fra_Par_t * pParams );
Alan Mishchenko committed
347
extern void                Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
Alan Mishchenko committed
348
extern Fra_Man_t *         Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pParams );
Alan Mishchenko committed
349
extern void                Fra_ManClean( Fra_Man_t * p, int nNodesMax );
Alan Mishchenko committed
350 351
extern Aig_Man_t *         Fra_ManPrepareComb( Fra_Man_t * p );
extern void                Fra_ManFinalizeComb( Fra_Man_t * p );
Alan Mishchenko committed
352 353 354
extern void                Fra_ManStop( Fra_Man_t * p );
extern void                Fra_ManPrint( Fra_Man_t * p );
/*=== fraSat.c ========================================================*/
Alan Mishchenko committed
355
extern int                 Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
Alan Mishchenko committed
356
extern int                 Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR );
Alan Mishchenko committed
357
extern int                 Fra_NodesAreClause( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR );
Alan Mishchenko committed
358
extern int                 Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew );
Alan Mishchenko committed
359
/*=== fraSec.c ========================================================*/
Alan Mishchenko committed
360
extern void                Fra_SecSetDefaultParams( Fra_Sec_t * p );
Alan Mishchenko committed
361
extern int                 Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec, Aig_Man_t ** ppResult );
Alan Mishchenko committed
362
/*=== fraSim.c ========================================================*/
Alan Mishchenko committed
363 364 365 366
extern int                 Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize );
extern int                 Fra_SmlNodeIsConst( Aig_Obj_t * pObj );
extern int                 Fra_SmlNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
extern int                 Fra_SmlNodeNotEquWeight( Fra_Sml_t * p, int Left, int Right );
Alan Mishchenko committed
367
extern int                 Fra_SmlNodeCountOnes( Fra_Sml_t * p, Aig_Obj_t * pObj );
Alan Mishchenko committed
368 369
extern int                 Fra_SmlCheckOutput( Fra_Man_t * p );
extern void                Fra_SmlSavePattern( Fra_Man_t * p );
Alan Mishchenko committed
370 371
extern void                Fra_SmlSimulate( Fra_Man_t * p, int fInit );
extern void                Fra_SmlResimulate( Fra_Man_t * p );
Alan Mishchenko committed
372
extern Fra_Sml_t *         Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame );
Alan Mishchenko committed
373
extern void                Fra_SmlStop( Fra_Sml_t * p );
374 375
extern Fra_Sml_t *         Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords, int fCheckMiter );
extern Fra_Sml_t *         Fra_SmlSimulateCombGiven( Aig_Man_t * pAig, char * pFileName, int fCheckMiter, int fVerbose );
Alan Mishchenko committed
376
extern Fra_Sml_t *         Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords, int fCheckMiter );
377 378 379 380 381 382
extern Abc_Cex_t *         Fra_SmlGetCounterExample( Fra_Sml_t * p );
extern Abc_Cex_t *         Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel );

ABC_NAMESPACE_HEADER_END


Alan Mishchenko committed
383 384 385 386 387 388 389

#endif

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////