summaryrefslogtreecommitdiffstats
path: root/src/proof/ssw/ssw.h
blob: cd65fc67da010f3be7fa07a915942262b5286609 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
/**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 $]

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

#ifndef ABC__aig__ssw__ssw_h
#define ABC__aig__ssw__ssw_h


////////////////////////////////////////////////////////////////////////
///                          INCLUDES                                ///
////////////////////////////////////////////////////////////////////////

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

ABC_NAMESPACE_HEADER_START

////////////////////////////////////////////////////////////////////////
///                         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
    int              nFramesAddSim; // the number of additional frames to simulate
    int              fConstrs;      // treat the last nConstrs POs as seq constraints
    int              fMergeFull;    // enables full merge when constraints are used
    int              nMaxLevs;      // the max number of levels of nodes to consider
    int              nBTLimit;      // conflict limit at a node
    int              nBTLimitGlobal;// conflict limit for multiple runs
    int              nMinDomSize;   // min clock domain considered for optimization
    int              nItersStop;    // stop after the given number of iterations
    int              fDumpSRInit;   // dumps speculative reduction
    int              nResimDelta;   // the number of nodes to resimulate
    int              nStepsMax;     // (scorr only) the max number of induction steps
    int              TimeLimit;     // time out in seconds
    int              fPolarFlip;    // uses polarity adjustment
    int              fLatchCorr;    // perform register correspondence
    int              fConstCorr;    // perform constant correspondence
    int              fOutputCorr;   // perform 'PO correspondence'
    int              fSemiFormal;   // enable semiformal filtering
//    int              fUniqueness;   // enable uniqueness constraints
    int              fDynamic;      // enable dynamic addition of constraints
    int              fLocalSim;     // enable local simulation simulation
    int              fPartSigCorr;  // uses partial signal correspondence
    int              nIsleDist;     // extends islands by the given distance
    int              fScorrGia;     // new signal correspondence implementation
    int              fUseCSat;      // new SAT solver using when fScorrGia is selected
    int              fVerbose;      // verbose stats
    int              fFlopVerbose;  // verbose printout of redundant flops
    int              fEquivDump;    // enables dumping equivalences
    int              fStopWhenGone; // stop when PO output is not a candidate constant
    // optimized latch correspondence
    int              fLatchCorrOpt; // perform register correspondence (optimized)
    int              nSatVarMax;    // max number of SAT vars before recycling SAT solver (optimized latch corr only)
    int              nRecycleCalls; // calls to perform before recycling SAT solver (optimized latch corr only)
    // 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)
    // internal parameters
    int              nIters;        // the number of iterations performed
    int              nConflicts;    // the total number of conflicts performed
    // callback
    void *           pData;
    void *           pFunc;
};

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;
    int              fSilent;
    int              fDropSatOuts;
    int              fMiter;
    int              fUseCex;
    int              fLatchOnly;
    int              fUseFfGrouping;
    int              nSolved;
    Abc_Cex_t *      pCex;
    int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode
};

typedef struct Ssw_Sml_t_ Ssw_Sml_t; // sequential simulation manager

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

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

/*=== sswBmc.c ==========================================================*/
extern int           Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbose, int * piFrame );
/*=== sswConstr.c ==========================================================*/
extern int           Ssw_ManSetConstrPhases( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits );
/*=== sswCore.c ==========================================================*/
extern void          Ssw_ManSetDefaultParams( Ssw_Pars_t * p );
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 );
/*=== 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 );
/*=== sswMiter.c ===================================================*/
/*=== sswPart.c ==========================================================*/
extern Aig_Man_t *   Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
/*=== sswPairs.c ===================================================*/
extern int           Ssw_MiterStatus( Aig_Man_t * p, int fVerbose );
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 );
extern int           Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars );
/*=== sswRarity.c ===================================================*/
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 );
/*=== sswSim.c ===================================================*/
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 );
extern void          Ssw_SmlInitializeSpecial( Ssw_Sml_t * p, Vec_Int_t * vInit );
extern int           Ssw_SmlCheckNonConstOutputs( Ssw_Sml_t * p );
extern Vec_Ptr_t *   Ssw_SmlSimDataPointers( Ssw_Sml_t * p );


ABC_NAMESPACE_HEADER_END

#endif

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