summaryrefslogtreecommitdiffstats
path: root/src/aig/ssw/sswInt.h
blob: faa3a87d33d4f9e130cf575a2d1551989e16590d (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
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
/**CFile****************************************************************

  FileName    [sswInt.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: sswInt.h,v 1.00 2008/09/01 00:00:00 alanmi Exp $]

***********************************************************************/
 
#ifndef __SSW_INT_H__
#define __SSW_INT_H__

#ifdef __cplusplus
extern "C" {
#endif

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

#include "saig.h"
#include "satSolver.h"
#include "ssw.h"

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

////////////////////////////////////////////////////////////////////////
///                         BASIC TYPES                              ///
////////////////////////////////////////////////////////////////////////

typedef struct Ssw_Man_t_ Ssw_Man_t; // signal correspondence manager
typedef struct Ssw_Cla_t_ Ssw_Cla_t; // equivalence classe manager
typedef struct Ssw_Sml_t_ Ssw_Sml_t; // sequential simulation manager

struct Ssw_Man_t_
{
    // parameters
    Ssw_Pars_t *     pPars;          // parameters
    int              nFrames;        // for quick lookup
    // AIGs used in the package
    Aig_Man_t *      pAig;           // user-given AIG
    Aig_Man_t *      pFrames;        // final AIG
    Aig_Obj_t **     pNodeToFrames;  // mapping of AIG nodes into FRAIG nodes
    // equivalence classes
    Ssw_Cla_t *      ppClasses;      // equivalence classes of nodes
    int              fRefined;       // is set to 1 when refinement happens
    int              nRefUse;        // the number of equivalences used
    int              nRefSkip;       // the number of equivalences skipped  
    // SAT solving
    sat_solver *     pSat;           // recyclable SAT solver
    int              nSatVars;       // the counter of SAT variables
    int *            pSatVars;       // mapping of each node into its SAT var
    int              nSatVarsTotal;  // the total number of SAT vars created
    Vec_Ptr_t *      vFanins;        // fanins of the CNF node
    // SAT solving (latch corr only)
    Vec_Ptr_t *      vUsedNodes;     // the nodes with SAT variables
    Vec_Ptr_t *      vUsedPis;       // the PIs with SAT variables
    Vec_Ptr_t *      vSimInfo;       // simulation information for the framed PIs
    int              nPatterns;      // the number of patterns saved
    int              nSimRounds;     // the number of simulation rounds performed
    int              nCallsCount;    // the number of calls in this round
    int              nCallsDelta;    // the number of calls to skip
    int              nCallsSat;      // the number of SAT calls in this round
    int              nCallsUnsat;    // the number of UNSAT calls in this round
    int              nRecycleCalls;  // the number of calls since last recycling
    int              nRecycles;      // the number of time SAT solver was recycled
    int              nConeMax;       // the maximum cone size
    // sequential simulator
    Ssw_Sml_t *      pSml;
    // counter example storage
    int              nPatWords;      // the number of words in the counter example
    unsigned *       pPatWords;      // the counter example
    // constraints
    int              nConstrTotal;   // the number of total constraints
    int              nConstrReduced; // the number of reduced constraints
    int              nStrangers;     // the number of strange situations
    // SAT calls statistics
    int              nSatCalls;      // the number of SAT calls
    int              nSatProof;      // the number of proofs
    int              nSatFailsReal;  // the number of timeouts
    int              nSatFailsTotal; // the number of timeouts
    int              nSatCallsUnsat; // the number of unsat SAT calls
    int              nSatCallsSat;   // the number of sat SAT calls
    // node/register/lit statistics
    int              nLitsBeg;
    int              nLitsEnd;
    int              nNodesBeg;
    int              nNodesEnd;
    int              nRegsBeg;
    int              nRegsEnd;
    // runtime stats
    int              timeBmc;        // bounded model checking
    int              timeReduce;     // speculative reduction
    int              timeMarkCones;  // marking the cones not to be refined
    int              timeSimSat;     // simulation of the counter-examples
    int              timeSat;        // solving SAT
    int              timeSatSat;     // sat
    int              timeSatUnsat;   // unsat
    int              timeSatUndec;   // undecided
    int              timeOther;      // other runtime
    int              timeTotal;      // total runtime
};

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

static inline int  Ssw_ObjSatNum( Ssw_Man_t * p, Aig_Obj_t * pObj )             { return p->pSatVars[pObj->Id]; }
static inline void Ssw_ObjSetSatNum( Ssw_Man_t * p, Aig_Obj_t * pObj, int Num ) { p->pSatVars[pObj->Id] = Num;  }

static inline int  Ssw_ObjIsConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) 
{
    return Aig_ObjRepr(pAig, pObj) == Aig_ManConst1(pAig);
}
static inline void Ssw_ObjSetConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) 
{
    assert( !Ssw_ObjIsConst1Cand( pAig, pObj ) );
    Aig_ObjSetRepr( pAig, pObj, Aig_ManConst1(pAig) );
}

static inline Aig_Obj_t * Ssw_ObjFrame( Ssw_Man_t * p, Aig_Obj_t * pObj, int i )                       { return p->pNodeToFrames[p->nFrames*pObj->Id + i];  }
static inline void        Ssw_ObjSetFrame( Ssw_Man_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { p->pNodeToFrames[p->nFrames*pObj->Id + i] = pNode; }

static inline Aig_Obj_t * Ssw_ObjChild0Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Ssw_ObjFrame(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)) : NULL;  }
static inline Aig_Obj_t * Ssw_ObjChild1Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Ssw_ObjFrame(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)) : NULL;  }

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

/*=== sswAig.c ===================================================*/
extern Aig_Man_t *   Ssw_FramesWithClasses( Ssw_Man_t * p );
/*=== sswClass.c =================================================*/
extern Ssw_Cla_t *   Ssw_ClassesStart( Aig_Man_t * pAig );
extern void          Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData,
                         unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *),
                         int (*pFuncNodeIsConst)(void *,Aig_Obj_t *),
                         int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) );
extern void          Ssw_ClassesStop( Ssw_Cla_t * p );
extern Vec_Ptr_t *   Ssw_ClassesGetRefined( Ssw_Cla_t * p );
extern void          Ssw_ClassesClearRefined( Ssw_Cla_t * p );
extern int           Ssw_ClassesCand1Num( Ssw_Cla_t * p );
extern int           Ssw_ClassesClassNum( Ssw_Cla_t * p );
extern int           Ssw_ClassesLitNum( Ssw_Cla_t * p );
extern Aig_Obj_t **  Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize );
extern void          Ssw_ClassesCollectClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, Vec_Ptr_t * vClass );
extern void          Ssw_ClassesCheck( Ssw_Cla_t * p );
extern void          Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose );
extern void          Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj );
extern Ssw_Cla_t *   Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs, int fVerbose );
extern Ssw_Cla_t *   Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs );
extern Ssw_Cla_t *   Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses );
extern int           Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive );
extern int           Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive );
extern int           Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive );
extern int           Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive );
/*=== sswCnf.c ===================================================*/
extern void          Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj );
/*=== sswCore.c ===================================================*/
extern Aig_Man_t *   Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p );
/*=== sswLcorr.c ==========================================================*/
extern int           Ssw_ManSweepLatch( Ssw_Man_t * p );
/*=== sswMan.c ===================================================*/
extern Ssw_Man_t *   Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
extern void          Ssw_ManCleanup( Ssw_Man_t * p );
extern void          Ssw_ManStop( Ssw_Man_t * p );
extern void          Ssw_ManStartSolver( Ssw_Man_t * p );
/*=== sswSat.c ===================================================*/
extern int           Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
extern int           Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
/*=== sswSim.c ===================================================*/
extern unsigned      Ssw_SmlObjHashWord( Ssw_Sml_t * p, Aig_Obj_t * pObj );
extern int           Ssw_SmlObjIsConstWord( 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 int           Ssw_SmlObjIsConstBit( void * p, Aig_Obj_t * pObj );
extern int           Ssw_SmlObjsAreEqualBit( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
extern Ssw_Sml_t *   Ssw_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame );
extern void          Ssw_SmlClean( Ssw_Sml_t * p );
extern void          Ssw_SmlStop( Ssw_Sml_t * p );
extern void          Ssw_SmlObjAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame );
extern void          Ssw_SmlObjSetWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, unsigned Word, int iWord, int iFrame );
extern void          Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat );
extern void          Ssw_SmlSimulateOne( Ssw_Sml_t * p );
extern void          Ssw_SmlSimulateOneFrame( Ssw_Sml_t * p );
extern Ssw_Sml_t *   Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords );
/*=== sswSimSat.c ===================================================*/
extern void          Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr );
extern void          Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f );
/*=== sswSweep.c ===================================================*/
extern int           Ssw_ManSweepBmc( Ssw_Man_t * p );
extern int           Ssw_ManSweep( Ssw_Man_t * p );


#ifdef __cplusplus
}
#endif

#endif

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