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
|
/**CFile****************************************************************
FileName [mfxInt.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [The good old minimization with complete don't-cares.]
Synopsis [Internal declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: mfxInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __MFX_INT_H__
#define __MFX_INT_H__
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include "nwk.h"
#include "mfx.h"
#include "aig.h"
#include "cnf.h"
#include "satSolver.h"
#include "satStore.h"
#include "bdc.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
#ifdef __cplusplus
extern "C" {
#endif
#define MFX_FANIN_MAX 12
typedef struct Mfx_Man_t_ Mfx_Man_t;
struct Mfx_Man_t_
{
// input data
Mfx_Par_t * pPars;
Nwk_Man_t * pNtk;
Aig_Man_t * pCare;
Vec_Ptr_t * vSuppsInv;
int nFaninMax;
// intermeditate data for the node
Vec_Ptr_t * vRoots; // the roots of the window
Vec_Ptr_t * vSupp; // the support of the window
Vec_Ptr_t * vNodes; // the internal nodes of the window
Vec_Ptr_t * vDivs; // the divisors of the node
Vec_Int_t * vDivLits; // the SAT literals of divisor nodes
Vec_Int_t * vProjVars; // the projection variables
// intermediate simulation data
Vec_Ptr_t * vDivCexes; // the counter-example for dividors
int nDivWords; // the number of words
int nCexes; // the numbe rof current counter-examples
int nSatCalls;
int nSatCexes;
// used for bidecomposition
Vec_Int_t * vTruth;
Bdc_Man_t * pManDec;
int nNodesDec;
int nNodesGained;
int nNodesGainedLevel;
// solving data
Aig_Man_t * pAigWin; // window AIG with constraints
Cnf_Dat_t * pCnf; // the CNF for the window
sat_solver * pSat; // the SAT solver used
Int_Man_t * pMan; // interpolation manager;
Vec_Int_t * vMem; // memory for intermediate SOPs
Vec_Vec_t * vLevels; // levelized structure for updating
Vec_Ptr_t * vFanins; // the new set of fanins
int nTotConfLim; // total conflict limit
int nTotConfLevel; // total conflicts on this level
// switching activity
Vec_Int_t * vProbs;
// the result of solving
int nFanins; // the number of fanins
int nWords; // the number of words
int nCares; // the number of care minterms
unsigned uCare[(MFX_FANIN_MAX<=5)?1:1<<(MFX_FANIN_MAX-5)]; // the computed care-set
// performance statistics
int nNodesTried;
int nNodesResub;
int nMintsCare;
int nMintsTotal;
int nNodesBad;
int nTotalDivs;
int nTimeOuts;
int nTimeOutsLevel;
int nDcMints;
double dTotalRatios;
// node/edge stats
int nTotalNodesBeg;
int nTotalNodesEnd;
int nTotalEdgesBeg;
int nTotalEdgesEnd;
// statistics
int timeWin;
int timeDiv;
int timeAig;
int timeCnf;
int timeSat;
int timeInt;
int timeTotal;
};
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== mfxDiv.c ==========================================================*/
extern Vec_Ptr_t * Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, float tArrivalMax );
/*=== mfxInter.c ==========================================================*/
extern sat_solver * Mfx_CreateSolverResub( Mfx_Man_t * p, int * pCands, int nCands, int fInvert );
extern Hop_Obj_t * Mfx_Interplate( Mfx_Man_t * p, int * pCands, int nCands );
extern int Mfx_InterplateEval( Mfx_Man_t * p, int * pCands, int nCands );
/*=== mfxMan.c ==========================================================*/
extern Mfx_Man_t * Mfx_ManAlloc( Mfx_Par_t * pPars );
extern void Mfx_ManStop( Mfx_Man_t * p );
extern void Mfx_ManClean( Mfx_Man_t * p );
/*=== mfxResub.c ==========================================================*/
extern void Mfx_PrintResubStats( Mfx_Man_t * p );
extern int Mfx_EdgePower( Mfx_Man_t * p, Nwk_Obj_t * pNode );
extern int Mfx_EdgeSwapEval( Mfx_Man_t * p, Nwk_Obj_t * pNode );
extern int Mfx_ResubNode( Mfx_Man_t * p, Nwk_Obj_t * pNode );
extern int Mfx_ResubNode2( Mfx_Man_t * p, Nwk_Obj_t * pNode );
/*=== mfxSat.c ==========================================================*/
extern int Mfx_SolveSat( Mfx_Man_t * p, Nwk_Obj_t * pNode );
/*=== mfxStrash.c ==========================================================*/
extern Aig_Man_t * Mfx_ConstructAig( Mfx_Man_t * p, Nwk_Obj_t * pNode );
extern double Mfx_ConstraintRatio( Mfx_Man_t * p, Nwk_Obj_t * pNode );
/*=== mfxWin.c ==========================================================*/
extern Vec_Ptr_t * Mfx_ComputeRoots( Nwk_Obj_t * pNode, int nWinTfoMax, int nFanoutLimit );
#ifdef __cplusplus
}
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
|
