summaryrefslogtreecommitdiffstats
path: root/src/proof/ssw/ssw.h
blob: 4680f6fb931b78c9040670d23661e20902d23985 (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
/**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
    // 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_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 int           Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
extern int           Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose );
/*=== 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                                ///
////////////////////////////////////////////////////////////////////////