ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
mpmAbc.c
Go to the documentation of this file.
1
20
21#include "aig/gia/gia.h"
22#include "mpmInt.h"
23
25
26
30
34
47{
48 Gia_Obj_t * pObj;
49 int i;
50 assert( Mig_ManObjNum(pMig) == Gia_ManObjNum(p) );
51 assert( Vec_IntSize(&pMig->vSibls) == 0 );
52 Vec_IntFill( &pMig->vSibls, Gia_ManObjNum(p), 0 );
54 Gia_ManForEachObj( p, pObj, i )
55 {
56 Gia_ObjSetPhase( p, pObj );
57 assert( Abc_Lit2Var(pObj->Value) == i );
58 Mig_ObjSetPhase( Mig_ManObj(pMig, i), pObj->fPhase );
59 if ( Gia_ObjSibl(p, i) && pObj->fMark0 )
60 {
61 Gia_Obj_t * pSibl, * pPrev;
62 for ( pPrev = pObj, pSibl = Gia_ObjSiblObj(p, i); pSibl; pPrev = pSibl, pSibl = Gia_ObjSiblObj(p, Gia_ObjId(p, pSibl)) )
63 Mig_ObjSetSiblId( Mig_ManObj(pMig, Abc_Lit2Var(pPrev->Value)), Abc_Lit2Var(pSibl->Value) );
64 pMig->nChoices++;
65 }
66 }
68}
69
81static inline int Mig_ObjFanin0Copy( Gia_Obj_t * pObj ) { return Abc_LitNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) ); }
82static inline int Mig_ObjFanin1Copy( Gia_Obj_t * pObj ) { return Abc_LitNotCond( Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj) ); }
83Mig_Man_t * Mig_ManCreate( void * pGia )
84{
85 Gia_Man_t * p = (Gia_Man_t *)pGia;
86 Mig_Man_t * pNew;
87 Gia_Obj_t * pObj;
88 int i;
89 pNew = Mig_ManStart();
90 pNew->pName = Abc_UtilStrsav( p->pName );
91 Gia_ManConst0(p)->Value = 0;
92 Gia_ManForEachObj1( p, pObj, i )
93 {
94 if ( Gia_ObjIsMuxId(p, i) )
95 pObj->Value = Mig_ManAppendMux( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj), Gia_ObjFanin2Copy(p, pObj) );
96 else if ( Gia_ObjIsXor(pObj) )
97 pObj->Value = Mig_ManAppendXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
98 else if ( Gia_ObjIsAnd(pObj) )
99 pObj->Value = Mig_ManAppendAnd( pNew, Mig_ObjFanin0Copy(pObj), Mig_ObjFanin1Copy(pObj) );
100 else if ( Gia_ObjIsCi(pObj) )
101 pObj->Value = Mig_ManAppendCi( pNew );
102 else if ( Gia_ObjIsCo(pObj) )
103 pObj->Value = Mig_ManAppendCo( pNew, Mig_ObjFanin0Copy(pObj) );
104 else assert( 0 );
105 }
106 Mig_ManSetRegNum( pNew, Gia_ManRegNum(p) );
107 if ( Gia_ManHasChoices(p) )
108 Mig_ManCreateChoices( pNew, p );
109 return pNew;
110}
111
123static inline unsigned Mpm_CutDataInt( Mpm_Cut_t * pCut ) { return pCut->hNext; }
124static inline void Mpm_CutSetDataInt( Mpm_Cut_t * pCut, int Data ) { pCut->hNext = Data; }
125int Mpm_ManNodeIfToGia_rec( Gia_Man_t * pNew, Mpm_Man_t * pMan, Mig_Obj_t * pObj, Vec_Ptr_t * vVisited, int fHash )
126{
127 Mig_Obj_t * pTemp;
128 Mpm_Cut_t * pCut;
129 int iFunc, iFunc0, iFunc1, iFunc2 = 0;
130 assert( fHash == 0 );
131 // get the best cut
132 pCut = Mpm_ObjCutBestP( pMan, pObj );
133 // if the cut is visited, return the result
134 if ( Mpm_CutDataInt(pCut) )
135 return Mpm_CutDataInt(pCut);
136 // mark the node as visited
137 Vec_PtrPush( vVisited, pCut );
138 // insert the worst case
139 Mpm_CutSetDataInt( pCut, ~0 );
140 // skip in case of primary input
141 if ( Mig_ObjIsCi(pObj) )
142 return Mpm_CutDataInt(pCut);
143 // compute the functions of the children
144 for ( pTemp = pObj; pTemp; pTemp = Mig_ObjSibl(pTemp) )
145 {
146 iFunc0 = Mpm_ManNodeIfToGia_rec( pNew, pMan, Mig_ObjFanin0(pTemp), vVisited, fHash );
147 if ( iFunc0 == ~0 )
148 continue;
149 iFunc1 = Mpm_ManNodeIfToGia_rec( pNew, pMan, Mig_ObjFanin1(pTemp), vVisited, fHash );
150 if ( iFunc1 == ~0 )
151 continue;
152 if ( Mig_ObjIsNode3(pTemp) )
153 {
154 iFunc2 = Mpm_ManNodeIfToGia_rec( pNew, pMan, Mig_ObjFanin2(pTemp), vVisited, fHash );
155 if ( iFunc2 == ~0 )
156 continue;
157 iFunc2 = Abc_LitNotCond(iFunc2, Mig_ObjFaninC2(pTemp));
158 }
159 iFunc0 = Abc_LitNotCond(iFunc0, Mig_ObjFaninC0(pTemp));
160 iFunc1 = Abc_LitNotCond(iFunc1, Mig_ObjFaninC1(pTemp));
161 // both branches are solved
162 if ( fHash )
163 {
164 if ( Mig_ObjIsMux(pTemp) )
165 iFunc = Gia_ManHashMux( pNew, iFunc2, iFunc1, iFunc0 );
166 else if ( Mig_ObjIsXor(pTemp) )
167 iFunc = Gia_ManHashXor( pNew, iFunc0, iFunc1 );
168 else
169 iFunc = Gia_ManHashAnd( pNew, iFunc0, iFunc1 );
170 }
171 else
172 {
173 if ( Mig_ObjIsMux(pTemp) )
174 iFunc = Gia_ManAppendMux( pNew, iFunc2, iFunc1, iFunc0 );
175 else if ( Mig_ObjIsXor(pTemp) )
176 iFunc = Gia_ManAppendXor( pNew, iFunc0, iFunc1 );
177 else
178 iFunc = Gia_ManAppendAnd( pNew, iFunc0, iFunc1 );
179 }
180 if ( Mig_ObjPhase(pTemp) != Mig_ObjPhase(pObj) )
181 iFunc = Abc_LitNot(iFunc);
182 Mpm_CutSetDataInt( pCut, iFunc );
183 break;
184 }
185 return Mpm_CutDataInt(pCut);
186}
187int Mpm_ManNodeIfToGia( Gia_Man_t * pNew, Mpm_Man_t * pMan, Mig_Obj_t * pObj, Vec_Int_t * vLeaves, int fHash )
188{
189 Mpm_Cut_t * pCut;
190 Mig_Obj_t * pFanin;
191 int i, iRes;
192 // get the best cut
193 pCut = Mpm_ObjCutBestP( pMan, pObj );
194 assert( pCut->nLeaves > 1 );
195 // set the leaf variables
196 Mpm_CutForEachLeaf( pMan->pMig, pCut, pFanin, i )
197 Mpm_CutSetDataInt( Mpm_ObjCutBestP(pMan, pFanin), Vec_IntEntry(vLeaves, i) );
198 // recursively compute the function while collecting visited cuts
199 Vec_PtrClear( pMan->vTemp );
200 iRes = Mpm_ManNodeIfToGia_rec( pNew, pMan, pObj, pMan->vTemp, fHash );
201 if ( iRes == ~0 )
202 {
203 Abc_Print( -1, "Mpm_ManNodeIfToGia(): Computing local AIG has failed.\n" );
204 return ~0;
205 }
206 // clean the cuts
207 Mpm_CutForEachLeaf( pMan->pMig, pCut, pFanin, i )
208 Mpm_CutSetDataInt( Mpm_ObjCutBestP(pMan, pFanin), 0 );
209 Vec_PtrForEachEntry( Mpm_Cut_t *, pMan->vTemp, pCut, i )
210 Mpm_CutSetDataInt( pCut, 0 );
211 return iRes;
212}
214{
215 Gia_Man_t * pNew;
216 Mpm_Cut_t * pCutBest;
217 Mig_Obj_t * pObj, * pFanin;
218 Vec_Int_t * vMapping, * vMapping2, * vPacking = NULL;
219 Vec_Int_t * vLeaves, * vLeaves2, * vCover;
220 word uTruth, * pTruth = &uTruth;
221 int i, k, Entry, iLitNew = 0;
222// assert( !pMan->pPars->fDeriveLuts || pMan->pPars->fTruth );
223 // start mapping and packing
224 vMapping = Vec_IntStart( Mig_ManObjNum(pMan->pMig) );
225 vMapping2 = Vec_IntStart( 1 );
226 if ( 0 ) // pMan->pPars->fDeriveLuts && pMan->pPars->pLutStruct )
227 {
228 vPacking = Vec_IntAlloc( 1000 );
229 Vec_IntPush( vPacking, 0 );
230 }
231 // create new manager
232 pNew = Gia_ManStart( Mig_ManObjNum(pMan->pMig) );
233 // iterate through nodes used in the mapping
234 vCover = Vec_IntAlloc( 1 << 16 );
235 vLeaves = Vec_IntAlloc( 16 );
236 vLeaves2 = Vec_IntAlloc( 16 );
237 Mig_ManCleanCopy( pMan->pMig );
238 Mig_ManForEachObj( pMan->pMig, pObj )
239 {
240 if ( !Mpm_ObjMapRef(pMan, pObj) && !Mig_ObjIsTerm(pObj) )
241 continue;
242 if ( Mig_ObjIsNode(pObj) )
243 {
244 // collect leaves of the best cut
245 Vec_IntClear( vLeaves );
246 pCutBest = Mpm_ObjCutBestP( pMan, pObj );
247 Mpm_CutForEachLeaf( pMan->pMig, pCutBest, pFanin, k )
248 Vec_IntPush( vLeaves, Mig_ObjCopy(pFanin) );
249 if ( pMan->pPars->fDeriveLuts && (pMan->pPars->fUseTruth || pMan->pPars->fUseDsd) )
250 {
251 extern int Gia_ManFromIfLogicNode( void * p, Gia_Man_t * pNew, int iObj, Vec_Int_t * vLeaves, Vec_Int_t * vLeavesTemp,
252 word * pRes, char * pStr, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2, Vec_Int_t * vPacking, int fCheck75, int fCheck44e );
253 if ( pMan->pPars->fUseTruth )
254 pTruth = Mpm_CutTruth(pMan, Abc_Lit2Var(pCutBest->iFunc));
255 else
256 uTruth = Mpm_CutTruthFromDsd( pMan, pCutBest, Abc_Lit2Var(pCutBest->iFunc) );
257// Kit_DsdPrintFromTruth( pTruth, Vec_IntSize(vLeaves) ); printf( "\n" );
258 // perform decomposition of the cut
259 iLitNew = Gia_ManFromIfLogicNode( NULL, pNew, Mig_ObjId(pObj), vLeaves, vLeaves2, pTruth, NULL, vCover, vMapping, vMapping2, vPacking, 0, 0 );
260 iLitNew = Abc_LitNotCond( iLitNew, pCutBest->fCompl ^ Abc_LitIsCompl(pCutBest->iFunc) );
261 }
262 else
263 {
264 // perform one of the two types of mapping: with and without structures
265 iLitNew = Mpm_ManNodeIfToGia( pNew, pMan, pObj, vLeaves, 0 );
266 // write mapping
267 Vec_IntSetEntry( vMapping, Abc_Lit2Var(iLitNew), Vec_IntSize(vMapping2) );
268 Vec_IntPush( vMapping2, Vec_IntSize(vLeaves) );
269 Vec_IntForEachEntry( vLeaves, Entry, k )
270 assert( Abc_Lit2Var(Entry) < Abc_Lit2Var(iLitNew) );
271 Vec_IntForEachEntry( vLeaves, Entry, k )
272 Vec_IntPush( vMapping2, Abc_Lit2Var(Entry) );
273 Vec_IntPush( vMapping2, Abc_Lit2Var(iLitNew) );
274 }
275 }
276 else if ( Mig_ObjIsCi(pObj) )
277 iLitNew = Gia_ManAppendCi(pNew);
278 else if ( Mig_ObjIsCo(pObj) )
279 iLitNew = Gia_ManAppendCo( pNew, Abc_LitNotCond(Mig_ObjCopy(Mig_ObjFanin0(pObj)), Mig_ObjFaninC0(pObj)) );
280 else if ( Mig_ObjIsConst0(pObj) )
281 {
282 iLitNew = 0;
283 // create const LUT
284 Vec_IntWriteEntry( vMapping, 0, Vec_IntSize(vMapping2) );
285 Vec_IntPush( vMapping2, 0 );
286 Vec_IntPush( vMapping2, 0 );
287 }
288 else assert( 0 );
289 Mig_ObjSetCopy( pObj, iLitNew );
290 }
291 Vec_IntFree( vCover );
292 Vec_IntFree( vLeaves );
293 Vec_IntFree( vLeaves2 );
294// printf( "Mapping array size: IfMan = %d. Gia = %d. Increase = %.2f\n",
295// Mig_ManObjNum(pMan), Gia_ManObjNum(pNew), 1.0 * Gia_ManObjNum(pNew) / Mig_ManObjNum(pMan) );
296 // finish mapping
297 if ( Vec_IntSize(vMapping) > Gia_ManObjNum(pNew) )
298 Vec_IntShrink( vMapping, Gia_ManObjNum(pNew) );
299 else
300 Vec_IntFillExtra( vMapping, Gia_ManObjNum(pNew), 0 );
301 assert( Vec_IntSize(vMapping) == Gia_ManObjNum(pNew) );
302 Vec_IntForEachEntry( vMapping, Entry, i )
303 if ( Entry > 0 )
304 Vec_IntAddToEntry( vMapping, i, Gia_ManObjNum(pNew) );
305 Vec_IntAppend( vMapping, vMapping2 );
306 Vec_IntFree( vMapping2 );
307 // attach mapping and packing
308 assert( pNew->vMapping == NULL );
309 assert( pNew->vPacking == NULL );
310 pNew->vMapping = vMapping;
311 pNew->vPacking = vPacking;
312 // verify that COs have mapping
313 {
314 Gia_Obj_t * pObj;
315 Gia_ManForEachCo( pNew, pObj, i )
316 assert( !Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) || Gia_ObjIsLut(pNew, Gia_ObjFaninId0p(pNew, pObj)) );
317 }
318 return pNew;
319}
320
332/*
333void Mig_ManTest2( Gia_Man_t * pGia )
334{
335 extern int Gia_ManSuppSizeTest( Gia_Man_t * p );
336 Mig_Man_t * p;
337 Gia_ManSuppSizeTest( pGia );
338 p = Mig_ManCreate( pGia );
339 Mig_ManSuppSizeTest( p );
340 Mig_ManStop( p );
341}
342*/
343
347
348
350
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Cube * p
Definition exorList.c:222
int Gia_ManFromIfLogicNode(void *pIfMan, Gia_Man_t *pNew, int iObj, Vec_Int_t *vLeaves, Vec_Int_t *vLeavesTemp, word *pRes, char *pStr, Vec_Int_t *vCover, Vec_Int_t *vMapping, Vec_Int_t *vMapping2, Vec_Int_t *vPacking, int fCheck75, int fCheck44e)
Definition giaIf.c:1189
void Gia_ObjSetPhase(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition giaUtil.c:387
Gia_Man_t * Gia_ManStart(int nObjsMax)
FUNCTION DEFINITIONS ///.
Definition giaMan.c:57
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
int Gia_ManHashXor(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:668
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
#define Gia_ManForEachObj1(p, pObj, i)
Definition gia.h:1192
int Gia_ManHashMux(Gia_Man_t *p, int iCtrl, int iData1, int iData0)
Definition giaHash.c:692
void Gia_ManCleanMark0(Gia_Man_t *p)
Definition giaUtil.c:256
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:576
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition gia.h:1190
#define Gia_ManForEachCo(p, pObj, i)
Definition gia.h:1236
void Gia_ManMarkFanoutDrivers(Gia_Man_t *p)
Definition giaUtil.c:1779
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
int Mpm_ManNodeIfToGia(Gia_Man_t *pNew, Mpm_Man_t *pMan, Mig_Obj_t *pObj, Vec_Int_t *vLeaves, int fHash)
Definition mpmAbc.c:187
ABC_NAMESPACE_IMPL_START void Mig_ManCreateChoices(Mig_Man_t *pMig, Gia_Man_t *p)
DECLARATIONS ///.
Definition mpmAbc.c:46
int Mpm_ManNodeIfToGia_rec(Gia_Man_t *pNew, Mpm_Man_t *pMan, Mig_Obj_t *pObj, Vec_Ptr_t *vVisited, int fHash)
Definition mpmAbc.c:125
void * Mpm_ManFromIfLogic(Mpm_Man_t *pMan)
Definition mpmAbc.c:213
Mig_Man_t * Mig_ManCreate(void *pGia)
FUNCTION DECLARATIONS ///.
Definition mpmAbc.c:83
word Mpm_CutTruthFromDsd(Mpm_Man_t *pMan, Mpm_Cut_t *pCut, int iClass)
Definition mpmDsd.c:883
#define Mpm_CutForEachLeaf(p, pCut, pLeaf, i)
Definition mpmInt.h:222
struct Mpm_Man_t_ Mpm_Man_t
Definition mpmInt.h:94
struct Mpm_Cut_t_ Mpm_Cut_t
BASIC TYPES ///.
Definition mpmInt.h:61
ABC_NAMESPACE_IMPL_START Mig_Man_t * Mig_ManStart()
DECLARATIONS ///.
Definition mpmMig.c:45
struct Mig_Obj_t_ Mig_Obj_t
Definition mpmMig.h:54
#define Mig_ManForEachObj(p, pObj)
MACRO DEFINITIONS ///.
Definition mpmMig.h:304
struct Mig_Man_t_ Mig_Man_t
Definition mpmMig.h:60
Vec_Int_t * vPacking
Definition gia.h:141
Vec_Int_t * vMapping
Definition gia.h:136
unsigned Value
Definition gia.h:89
unsigned fPhase
Definition gia.h:87
unsigned fMark0
Definition gia.h:81
Vec_Int_t vSibls
Definition mpmMig.h:77
char * pName
Definition mpmMig.h:63
int nChoices
Definition mpmMig.h:66
int hNext
Definition mpmInt.h:64
unsigned fCompl
Definition mpmInt.h:66
unsigned nLeaves
Definition mpmInt.h:68
unsigned iFunc
Definition mpmInt.h:65
Mig_Man_t * pMig
Definition mpmInt.h:97
Vec_Ptr_t * vTemp
Definition mpmInt.h:116
Mpm_Par_t * pPars
Definition mpmInt.h:98
int fUseDsd
Definition mpm.h:65
int fUseTruth
Definition mpm.h:64
int fDeriveLuts
Definition mpm.h:68
#define assert(ex)
Definition util_old.h:213
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55