ssw.h 8.75 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
/**CFile****************************************************************

  FileName    [ssw.h] 

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Inductive prover with constraints.]

  Synopsis    [External declarations.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - September 1, 2008.]

  Revision    [$Id: ssw.h,v 1.00 2008/09/01 00:00:00 alanmi Exp $]

***********************************************************************/
Alan Mishchenko committed
20

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

24

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

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

33
ABC_NAMESPACE_HEADER_START
Alan Mishchenko committed
34

Alan Mishchenko committed
35 36 37 38 39 40 41 42 43 44 45
////////////////////////////////////////////////////////////////////////
///                         BASIC TYPES                              ///
////////////////////////////////////////////////////////////////////////

// choicing parameters
typedef struct Ssw_Pars_t_ Ssw_Pars_t;
struct Ssw_Pars_t_
{
    int              nPartSize;     // size of the partition
    int              nOverSize;     // size of the overlap between partitions
    int              nFramesK;      // the induction depth
Alan Mishchenko committed
46
    int              nFramesAddSim; // the number of additional frames to simulate
47 48
    int              fConstrs;      // treat the last nConstrs POs as seq constraints
    int              fMergeFull;    // enables full merge when constraints are used
Alan Mishchenko committed
49 50
    int              nMaxLevs;      // the max number of levels of nodes to consider
    int              nBTLimit;      // conflict limit at a node
Alan Mishchenko committed
51
    int              nBTLimitGlobal;// conflict limit for multiple runs
Alan Mishchenko committed
52
    int              nMinDomSize;   // min clock domain considered for optimization
Alan Mishchenko committed
53
    int              nItersStop;    // stop after the given number of iterations
Alan Mishchenko committed
54 55
    int              fDumpSRInit;   // dumps speculative reduction
    int              nResimDelta;   // the number of nodes to resimulate
56 57
    int              nStepsMax;     // (scorr only) the max number of induction steps
    int              TimeLimit;     // time out in seconds
Alan Mishchenko committed
58 59
    int              fPolarFlip;    // uses polarity adjustment
    int              fLatchCorr;    // perform register correspondence
60
    int              fConstCorr;    // perform constant correspondence
61
    int              fOutputCorr;   // perform 'PO correspondence'
Alan Mishchenko committed
62
    int              fSemiFormal;   // enable semiformal filtering
63
//    int              fUniqueness;   // enable uniqueness constraints
Alan Mishchenko committed
64
    int              fDynamic;      // enable dynamic addition of constraints
Alan Mishchenko committed
65 66 67
    int              fLocalSim;     // enable local simulation simulation
    int              fPartSigCorr;  // uses partial signal correspondence
    int              nIsleDist;     // extends islands by the given distance
Alan Mishchenko committed
68 69
    int              fScorrGia;     // new signal correspondence implementation
    int              fUseCSat;      // new SAT solver using when fScorrGia is selected
Alan Mishchenko committed
70
    int              fVerbose;      // verbose stats
Alan Mishchenko committed
71
    int              fFlopVerbose;  // verbose printout of redundant flops
72
    int              fEquivDump;    // enables dumping equivalences
73
    int              fStopWhenGone; // stop when PO output is not a candidate constant
Alan Mishchenko committed
74
    // optimized latch correspondence
Alan Mishchenko committed
75 76
    int              fLatchCorrOpt; // perform register correspondence (optimized)
    int              nSatVarMax;    // max number of SAT vars before recycling SAT solver (optimized latch corr only)
Alan Mishchenko committed
77
    int              nRecycleCalls; // calls to perform before recycling SAT solver (optimized latch corr only)
Alan Mishchenko committed
78 79 80
    // optimized signal correspondence
    int              nSatVarMax2;   // max number of SAT vars before recycling SAT solver (optimized latch corr only)
    int              nRecycleCalls2;// calls to perform before recycling SAT solver (optimized latch corr only)
Alan Mishchenko committed
81 82
    // internal parameters
    int              nIters;        // the number of iterations performed
Alan Mishchenko committed
83
    int              nConflicts;    // the total number of conflicts performed
84 85 86
    // callback
    void *           pData;
    void *           pFunc;
Alan Mishchenko committed
87 88
};

89 90 91 92 93 94 95 96 97 98 99 100 101 102 103
typedef struct Ssw_RarPars_t_ Ssw_RarPars_t;
struct Ssw_RarPars_t_
{
    int              nFrames;
    int              nWords;
    int              nBinSize;
    int              nRounds;
    int              nRestart;
    int              nRandSeed;
    int              TimeOut;
    int              TimeOutGap;
    int              fSolveAll;
    int              fSetLastState;
    int              fVerbose;
    int              fNotVerbose;
104
    int              fSilent;
105 106 107 108
    int              fDropSatOuts;
    int              fMiter;
    int              fUseCex;
    int              fLatchOnly;
109
    int              fUseFfGrouping;
110
    int              nSolved;
111
    Abc_Cex_t *      pCex;
112
    int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode
113 114
};

Alan Mishchenko committed
115 116
typedef struct Ssw_Sml_t_ Ssw_Sml_t; // sequential simulation manager

Alan Mishchenko committed
117 118 119 120 121 122 123 124
////////////////////////////////////////////////////////////////////////
///                      MACRO DEFINITIONS                           ///
////////////////////////////////////////////////////////////////////////

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

Alan Mishchenko committed
125 126
/*=== sswBmc.c ==========================================================*/
extern int           Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbose, int * piFrame );
127 128
/*=== sswConstr.c ==========================================================*/
extern int           Ssw_ManSetConstrPhases( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits );
Alan Mishchenko committed
129 130
/*=== sswCore.c ==========================================================*/
extern void          Ssw_ManSetDefaultParams( Ssw_Pars_t * p );
Alan Mishchenko committed
131 132 133
extern void          Ssw_ManSetDefaultParamsLcorr( Ssw_Pars_t * p );
extern Aig_Man_t *   Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
extern Aig_Man_t *   Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
Alan Mishchenko committed
134 135 136
/*=== sswIslands.c ==========================================================*/
extern int           Ssw_SecWithSimilarityPairs( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs, Ssw_Pars_t * pPars );
extern int           Ssw_SecWithSimilarity( Aig_Man_t * p0, Aig_Man_t * p1, Ssw_Pars_t * pPars );
Alan Mishchenko committed
137
/*=== sswMiter.c ===================================================*/
Alan Mishchenko committed
138 139
/*=== sswPart.c ==========================================================*/
extern Aig_Man_t *   Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
Alan Mishchenko committed
140
/*=== sswPairs.c ===================================================*/
Alan Mishchenko committed
141
extern int           Ssw_MiterStatus( Aig_Man_t * p, int fVerbose );
Alan Mishchenko committed
142 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 );
extern int           Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars );
Alan Mishchenko committed
144
extern int           Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars );
145
/*=== sswRarity.c ===================================================*/
146 147 148
extern void          Ssw_RarSetDefaultParams( Ssw_RarPars_t * p );
extern int           Ssw_RarSignalFilter( Aig_Man_t * pAig, Ssw_RarPars_t * pPars );
extern int           Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars );
Alan Mishchenko committed
149
/*=== sswSim.c ===================================================*/
Alan Mishchenko committed
150 151 152 153 154 155 156 157
extern Ssw_Sml_t *   Ssw_SmlSimulateComb( Aig_Man_t * pAig, int nWords );
extern Ssw_Sml_t *   Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords );
extern void          Ssw_SmlUnnormalize( Ssw_Sml_t * p );
extern void          Ssw_SmlStop( Ssw_Sml_t * p );
extern int           Ssw_SmlNumFrames( Ssw_Sml_t * p );
extern int           Ssw_SmlNumWordsTotal( Ssw_Sml_t * p );
extern unsigned *    Ssw_SmlSimInfo( Ssw_Sml_t * p, Aig_Obj_t * pObj );
extern int           Ssw_SmlObjsAreEqualWord( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
158
extern void          Ssw_SmlInitializeSpecial( Ssw_Sml_t * p, Vec_Int_t * vInit );
159
extern int           Ssw_SmlCheckNonConstOutputs( Ssw_Sml_t * p );
160 161
extern Vec_Ptr_t *   Ssw_SmlSimDataPointers( Ssw_Sml_t * p );

162 163 164

ABC_NAMESPACE_HEADER_END

Alan Mishchenko committed
165 166 167 168 169 170
#endif

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