summaryrefslogtreecommitdiffstats
path: root/src/aig/fra/fra.h
blob: ee52520a53e8e596c46a41d4571480338123005f (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
/**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 $]

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

#ifndef __FRA_H__
#define __FRA_H__

#ifdef __cplusplus
extern "C" {
#endif 

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

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

#include "vec.h"
#include "dar.h"
#include "satSolver.h"

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

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

typedef struct Fra_Par_t_   Fra_Par_t;
typedef struct Fra_Man_t_   Fra_Man_t;

// 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
    int              fSpeculate;        // use speculative reduction
    int              fProve;            // prove the miter outputs
    int              fVerbose;          // verbose output
    int              fDoSparse;         // skip sparse functions
    int              nBTLimitNode;      // conflict limit at a node
    int              nBTLimitMiter;     // conflict limit at an output
};

// FRAIG manager
struct Fra_Man_t_
{
    // high-level data    
    Fra_Par_t *      pPars;             // parameters governing fraiging
    // AIG managers
    Dar_Man_t *      pManAig;           // the starting AIG manager
    Dar_Man_t *      pManFraig;         // the final AIG manager
    // simulation info
    unsigned *       pSimWords;         // memory for simulation information
    int              nSimWords;         // the number of simulation words
    // counter example storage
    int              nPatWords;         // the number of words in the counter example
    unsigned *       pPatWords;         // the counter example
    int *            pPatScores;        // the scores of each pattern
    // equivalence classes 
    Vec_Ptr_t *      vClasses;          // equivalence classes
    Vec_Ptr_t *      vClasses1;         // equivalence class of Const1 node
    Vec_Ptr_t *      vClassesTemp;      // temporary storage for new classes
    Dar_Obj_t **     pMemClasses;       // memory allocated for equivalence classes
    Dar_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
    // equivalence checking
    sat_solver *     pSat;              // SAT solver
    int              nSatVars;          // the number of variables currently used
    Vec_Ptr_t *      vPiVars;           // the PIs of the cone used 
    sint64           nBTLimitGlobal;    // resource limit
    sint64           nInsLimitGlobal;   // resource limit
    // various data members
    Dar_Obj_t **     pMemFraig;         // memory allocated for points to the fraig nodes
    Dar_Obj_t **     pMemRepr;          // memory allocated for points to the node representatives
    Vec_Ptr_t **     pMemFanins;        // the arrays of fanins
    int *            pMemSatNums;       // the array of SAT numbers
    int              nSizeAlloc;        // allocated size of the arrays
    // statistics
    int              nSimRounds;
    int              nNodesMiter;
    int              nClassesZero;
    int              nClassesBeg;
    int              nClassesEnd;
    int              nPairsBeg;
    int              nPairsEnd;
    int              nSatCalls;
    int              nSatCallsSat;
    int              nSatCallsUnsat;
    int              nSatProof;
    int              nSatFails;
    int              nSatFailsReal;
    // runtime
    int              timeSim;
    int              timeTrav;
    int              timeSat;
    int              timeSatUnsat;
    int              timeSatSat;
    int              timeSatFail;
    int              timeRef;
    int              timeTotal;
    int              time1;
    int              time2;
};

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

static inline unsigned *   Fra_ObjSim( Dar_Obj_t * pObj )   { return ((Fra_Man_t *)pObj->pData)->pSimWords + ((Fra_Man_t *)pObj->pData)->nSimWords * pObj->Id;  }
static inline unsigned     Fra_ObjRandomSim()               { return (rand() << 24) ^ (rand() << 12) ^ rand(); }

static inline Dar_Obj_t *  Fra_ObjFraig( Dar_Obj_t * pObj )                              { return ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id];       }
static inline Dar_Obj_t *  Fra_ObjRepr( Dar_Obj_t * pObj )                               { return ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id];        }
static inline Vec_Ptr_t *  Fra_ObjFaninVec( Dar_Obj_t * pObj )                           { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id];      }
static inline int          Fra_ObjSatNum( Dar_Obj_t * pObj )                             { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id];     }

static inline void         Fra_ObjSetFraig( Dar_Obj_t * pObj, Dar_Obj_t * pNode )        { ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id]   = pNode;    }
static inline void         Fra_ObjSetRepr( Dar_Obj_t * pObj, Dar_Obj_t * pNode )         { ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id]    = pNode;    }
static inline void         Fra_ObjSetFaninVec( Dar_Obj_t * pObj, Vec_Ptr_t * vFanins )   { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id]  = vFanins;  }
static inline void         Fra_ObjSetSatNum( Dar_Obj_t * pObj, int Num )                 { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num;      }

static inline Dar_Obj_t *  Fra_ObjChild0Fra( Dar_Obj_t * pObj ) { assert( !Dar_IsComplement(pObj) ); return Dar_ObjFanin0(pObj)? Dar_NotCond(Fra_ObjFraig(Dar_ObjFanin0(pObj)), Dar_ObjFaninC0(pObj)) : NULL;  }
static inline Dar_Obj_t *  Fra_ObjChild1Fra( Dar_Obj_t * pObj ) { assert( !Dar_IsComplement(pObj) ); return Dar_ObjFanin1(pObj)? Dar_NotCond(Fra_ObjFraig(Dar_ObjFanin1(pObj)), Dar_ObjFaninC1(pObj)) : NULL;  }

////////////////////////////////////////////////////////////////////////
///                         ITERATORS                                ///
////////////////////////////////////////////////////////////////////////

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

/*=== fraAnd.c ========================================================*/
extern void                Fra_Sweep( Fra_Man_t * p );
/*=== fraClass.c ========================================================*/
extern void                Fra_PrintClasses( Fra_Man_t * p );
extern void                Fra_CreateClasses( Fra_Man_t * p );
extern int                 Fra_RefineClasses( Fra_Man_t * p );
extern int                 Fra_RefineClasses1( Fra_Man_t * p );
/*=== fraCnf.c ========================================================*/
extern void                Fra_NodeAddToSolver( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew );
/*=== fraCore.c ========================================================*/
extern Dar_Man_t *         Fra_Perform( Dar_Man_t * pManAig, Fra_Par_t * pParams );
/*=== fraMan.c ========================================================*/
extern void                Fra_ParamsDefault( Fra_Par_t * pParams );
extern Fra_Man_t *         Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pParams );
extern void                Fra_ManPrepare( Fra_Man_t * p );
extern void                Fra_ManStop( Fra_Man_t * p );
extern void                Fra_ManPrint( Fra_Man_t * p );
/*=== fraSat.c ========================================================*/
extern int                 Fra_NodesAreEquiv( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew );
extern int                 Fra_NodeIsConst( Fra_Man_t * p, Dar_Obj_t * pNew );
/*=== fraSim.c ========================================================*/
extern int                 Fra_NodeHasZeroSim( Fra_Man_t * p, Dar_Obj_t * pObj );
extern int                 Fra_NodeCompareSims( Fra_Man_t * p, Dar_Obj_t * pObj0, Dar_Obj_t * pObj1 );
extern void                Fra_SavePattern( Fra_Man_t * p );
extern void                Fra_Simulate( Fra_Man_t * p );
extern void                Fra_Resimulate( Fra_Man_t * p );
extern int                 Fra_CheckOutputSims( Fra_Man_t * p );

#ifdef __cplusplus
}
#endif

#endif

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