1 /**CFile****************************************************************
2
3 FileName [mfsInt.h]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [The good old minimization with complete don't-cares.]
8
9 Synopsis [Internal declarations.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: mfsInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #ifndef ABC__opt__mfs__mfsInt_h
22 #define ABC__opt__mfs__mfsInt_h
23
24
25 ////////////////////////////////////////////////////////////////////////
26 /// INCLUDES ///
27 ////////////////////////////////////////////////////////////////////////
28
29 #include "base/abc/abc.h"
30 #include "mfs.h"
31 #include "aig/aig/aig.h"
32 #include "sat/cnf/cnf.h"
33 #include "sat/bsat/satSolver.h"
34 #include "sat/bsat/satStore.h"
35 #include "bool/bdc/bdc.h"
36 #include "aig/gia/gia.h"
37
38 ////////////////////////////////////////////////////////////////////////
39 /// PARAMETERS ///
40 ////////////////////////////////////////////////////////////////////////
41
42
43
44 ABC_NAMESPACE_HEADER_START
45
46
47 #define MFS_FANIN_MAX 12
48
49 typedef struct Mfs_Man_t_ Mfs_Man_t;
50 struct Mfs_Man_t_
51 {
52 // input data
53 Mfs_Par_t * pPars;
54 Abc_Ntk_t * pNtk;
55 Aig_Man_t * pCare;
56 Vec_Ptr_t * vSuppsInv;
57 int nFaninMax;
58 // intermeditate data for the node
59 Vec_Ptr_t * vRoots; // the roots of the window
60 Vec_Ptr_t * vSupp; // the support of the window
61 Vec_Ptr_t * vNodes; // the internal nodes of the window
62 Vec_Ptr_t * vDivs; // the divisors of the node
63 Vec_Int_t * vDivLits; // the SAT literals of divisor nodes
64 Vec_Int_t * vProjVarsCnf; // the projection variables
65 Vec_Int_t * vProjVarsSat; // the projection variables
66 // intermediate simulation data
67 Vec_Ptr_t * vDivCexes; // the counter-example for dividors
68 int nDivWords; // the number of words
69 int nCexes; // the numbe rof current counter-examples
70 int nSatCalls;
71 int nSatCexes;
72 /*
73 // intermediate AIG data
74 Gia_Man_t * pGia; // replica of the AIG in the new package
75 // Gia_Obj_t ** pSat2Gia; // mapping of PO SAT var into internal GIA nodes
76 Tas_Man_t * pTas; // the SAT solver
77 Vec_Int_t * vCex; // the counter-example
78 Vec_Ptr_t * vGiaLits; // literals given as assumptions
79 */
80 // used for bidecomposition
81 Vec_Int_t * vTruth;
82 Bdc_Man_t * pManDec;
83 int nNodesDec;
84 int nNodesGained;
85 int nNodesGainedLevel;
86 // solving data
87 Aig_Man_t * pAigWin; // window AIG with constraints
88 Cnf_Dat_t * pCnf; // the CNF for the window
89 sat_solver * pSat; // the SAT solver used
90 Int_Man_t * pMan; // interpolation manager;
91 Vec_Int_t * vMem; // memory for intermediate SOPs
92 Vec_Vec_t * vLevels; // levelized structure for updating
93 Vec_Ptr_t * vMfsFanins; // the new set of fanins
94 int nTotConfLim; // total conflict limit
95 int nTotConfLevel; // total conflicts on this level
96 // switching activity
97 Vec_Int_t * vProbs;
98 // the result of solving
99 int nFanins; // the number of fanins
100 int nWords; // the number of words
101 int nCares; // the number of care minterms
102 unsigned uCare[(MFS_FANIN_MAX<=5)?1:1<<(MFS_FANIN_MAX-5)]; // the computed care-set
103 // performance statistics
104 int nTryRemoves; // number of fanin removals
105 int nTryResubs; // number of resubstitutions
106 int nRemoves; // number of fanin removals
107 int nResubs; // number of resubstitutions
108 int nNodesTried;
109 int nNodesResub;
110 int nMintsCare;
111 int nMintsTotal;
112 int nNodesBad;
113 int nTotalDivs;
114 int nTimeOuts;
115 int nTimeOutsLevel;
116 int nDcMints;
117 int nMaxDivs;
118 double dTotalRatios;
119 // node/edge stats
120 int nTotalNodesBeg;
121 int nTotalNodesEnd;
122 int nTotalEdgesBeg;
123 int nTotalEdgesEnd;
124 float TotalSwitchingBeg;
125 float TotalSwitchingEnd;
126 // statistics
127 abctime timeWin;
128 abctime timeDiv;
129 abctime timeAig;
130 abctime timeGia;
131 abctime timeCnf;
132 abctime timeSat;
133 abctime timeInt;
134 abctime timeTotal;
135 };
136
Abc_MfsObjProb(Mfs_Man_t * p,Abc_Obj_t * pObj)137 static inline float Abc_MfsObjProb( Mfs_Man_t * p, Abc_Obj_t * pObj ) { return (p->vProbs && pObj->Id < Vec_IntSize(p->vProbs))? Abc_Int2Float(Vec_IntEntry(p->vProbs,pObj->Id)) : 0.0; }
138
139 ////////////////////////////////////////////////////////////////////////
140 /// BASIC TYPES ///
141 ////////////////////////////////////////////////////////////////////////
142
143 ////////////////////////////////////////////////////////////////////////
144 /// MACRO DEFINITIONS ///
145 ////////////////////////////////////////////////////////////////////////
146
147 ////////////////////////////////////////////////////////////////////////
148 /// FUNCTION DECLARATIONS ///
149 ////////////////////////////////////////////////////////////////////////
150
151 /*=== mfsDiv.c ==========================================================*/
152 extern Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDivMax );
153 /*=== mfsInter.c ==========================================================*/
154 extern sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands, int fInvert );
155 extern Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands );
156 extern int Abc_NtkMfsInterplateEval( Mfs_Man_t * p, int * pCands, int nCands );
157 /*=== mfsMan.c ==========================================================*/
158 extern Mfs_Man_t * Mfs_ManAlloc( Mfs_Par_t * pPars );
159 extern void Mfs_ManStop( Mfs_Man_t * p );
160 extern void Mfs_ManClean( Mfs_Man_t * p );
161 /*=== mfsResub.c ==========================================================*/
162 extern void Abc_NtkMfsPrintResubStats( Mfs_Man_t * p );
163 extern int Abc_NtkMfsEdgeSwapEval( Mfs_Man_t * p, Abc_Obj_t * pNode );
164 extern int Abc_NtkMfsEdgePower( Mfs_Man_t * p, Abc_Obj_t * pNode );
165 extern int Abc_NtkMfsResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode );
166 extern int Abc_NtkMfsResubNode2( Mfs_Man_t * p, Abc_Obj_t * pNode );
167 /*=== mfsSat.c ==========================================================*/
168 extern int Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode );
169 extern int Abc_NtkAddOneHotness( Mfs_Man_t * p );
170 /*=== mfsStrash.c ==========================================================*/
171 extern Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode );
172 extern double Abc_NtkConstraintRatio( Mfs_Man_t * p, Abc_Obj_t * pNode );
173 /*=== mfsWin.c ==========================================================*/
174 extern Vec_Ptr_t * Abc_MfsComputeRoots( Abc_Obj_t * pNode, int nWinTfoMax, int nFanoutLimit );
175
176 /*=== mfsGia.c ==========================================================*/
177 extern void Abc_NtkMfsConstructGia( Mfs_Man_t * p );
178 extern void Abc_NtkMfsDeconstructGia( Mfs_Man_t * p );
179 extern int Abc_NtkMfsTryResubOnceGia( Mfs_Man_t * p, int * pCands, int nCands );
180
181
182
183 ABC_NAMESPACE_HEADER_END
184
185
186
187 #endif
188
189 ////////////////////////////////////////////////////////////////////////
190 /// END OF FILE ///
191 ////////////////////////////////////////////////////////////////////////
192
193