ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
dauGia.c
Go to the documentation of this file.
1
20
21#include "dauInt.h"
22#include "aig/gia/gia.h"
23#include "misc/util/utilTruth.h"
24
25ABC_NAMESPACE_IMPL_START
26
30
31extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
32
33#define DAU_DSD_MAX_VAR 12
34
35static int m_Calls = 0;
36static int m_NonDsd = 0;
37static int m_Non1Step = 0;
38
42
54int Dau_DsdToGiaCompose_rec( Gia_Man_t * pGia, word Func, int * pFanins, int nVars )
55{
56 int t0, t1;
57 if ( Func == 0 )
58 return 0;
59 if ( Func == ~(word)0 )
60 return 1;
61 assert( nVars > 0 );
62 if ( --nVars == 0 )
63 {
64 assert( Func == s_Truths6[0] || Func == s_Truths6Neg[0] );
65 return Abc_LitNotCond( pFanins[0], (int)(Func == s_Truths6Neg[0]) );
66 }
67 if ( !Abc_Tt6HasVar(Func, nVars) )
68 return Dau_DsdToGiaCompose_rec( pGia, Func, pFanins, nVars );
69 t0 = Dau_DsdToGiaCompose_rec( pGia, Abc_Tt6Cofactor0(Func, nVars), pFanins, nVars );
70 t1 = Dau_DsdToGiaCompose_rec( pGia, Abc_Tt6Cofactor1(Func, nVars), pFanins, nVars );
71 if ( pGia->pMuxes )
72 return Gia_ManHashMuxReal( pGia, pFanins[nVars], t1, t0 );
73 else
74 return Gia_ManHashMux( pGia, pFanins[nVars], t1, t0 );
75}
76
88int Dau_DsdToGia2_rec( Gia_Man_t * pGia, char * pStr, char ** p, int * pMatches, int * pLits, Vec_Int_t * vCover )
89{
90 int fCompl = 0;
91 if ( **p == '!' )
92 (*p)++, fCompl = 1;
93 if ( **p >= 'a' && **p < 'a' + DAU_DSD_MAX_VAR ) // var
94 return Abc_LitNotCond( pLits[**p - 'a'], fCompl );
95 if ( **p == '(' ) // and/or
96 {
97 char * q = pStr + pMatches[ *p - pStr ];
98 int Res = 1, Lit;
99 assert( **p == '(' && *q == ')' );
100 for ( (*p)++; *p < q; (*p)++ )
101 {
102 Lit = Dau_DsdToGia2_rec( pGia, pStr, p, pMatches, pLits, vCover );
103 Res = Gia_ManHashAnd( pGia, Res, Lit );
104 }
105 assert( *p == q );
106 return Abc_LitNotCond( Res, fCompl );
107 }
108 if ( **p == '[' ) // xor
109 {
110 char * q = pStr + pMatches[ *p - pStr ];
111 int Res = 0, Lit;
112 assert( **p == '[' && *q == ']' );
113 for ( (*p)++; *p < q; (*p)++ )
114 {
115 Lit = Dau_DsdToGia2_rec( pGia, pStr, p, pMatches, pLits, vCover );
116 if ( pGia->pMuxes )
117 Res = Gia_ManHashXorReal( pGia, Res, Lit );
118 else
119 Res = Gia_ManHashXor( pGia, Res, Lit );
120 }
121 assert( *p == q );
122 return Abc_LitNotCond( Res, fCompl );
123 }
124 if ( **p == '<' ) // mux
125 {
126 int nVars = 0;
127 int Temp[3], * pTemp = Temp, Res;
128 int Fanins[DAU_DSD_MAX_VAR], * pLits2;
129 char * pOld = *p;
130 char * q = pStr + pMatches[ *p - pStr ];
131 // read fanins
132 if ( *(q+1) == '{' )
133 {
134 char * q2;
135 *p = q+1;
136 q2 = pStr + pMatches[ *p - pStr ];
137 assert( **p == '{' && *q2 == '}' );
138 for ( nVars = 0, (*p)++; *p < q2; (*p)++, nVars++ )
139 Fanins[nVars] = Dau_DsdToGia2_rec( pGia, pStr, p, pMatches, pLits, vCover );
140 assert( *p == q2 );
141 pLits2 = Fanins;
142 }
143 else
144 pLits2 = pLits;
145 // read MUX
146 *p = pOld;
147 q = pStr + pMatches[ *p - pStr ];
148 assert( **p == '<' && *q == '>' );
149 // verify internal variables
150 if ( nVars )
151 for ( ; pOld < q; pOld++ )
152 if ( *pOld >= 'a' && *pOld <= 'z' )
153 assert( *pOld - 'a' < nVars );
154 // derive MUX components
155 for ( (*p)++; *p < q; (*p)++ )
156 *pTemp++ = Dau_DsdToGia2_rec( pGia, pStr, p, pMatches, pLits2, vCover );
157 assert( pTemp == Temp + 3 );
158 assert( *p == q );
159 if ( *(q+1) == '{' ) // and/or
160 {
161 char * q = pStr + pMatches[ ++(*p) - pStr ];
162 assert( **p == '{' && *q == '}' );
163 *p = q;
164 }
165 if ( pGia->pMuxes )
166 Res = Gia_ManHashMuxReal( pGia, Temp[0], Temp[1], Temp[2] );
167 else
168 Res = Gia_ManHashMux( pGia, Temp[0], Temp[1], Temp[2] );
169 return Abc_LitNotCond( Res, fCompl );
170 }
171 if ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
172 {
173 Vec_Int_t vLeaves; char * q;
174 word pFunc[DAU_DSD_MAX_VAR > 6 ? (1 << (DAU_DSD_MAX_VAR-6)) : 1];
175 int Fanins[DAU_DSD_MAX_VAR], Res;
176 int i, nVars = Abc_TtReadHex( pFunc, *p );
177 *p += Abc_TtHexDigitNum( nVars );
178 q = pStr + pMatches[ *p - pStr ];
179 assert( **p == '{' && *q == '}' );
180 for ( i = 0, (*p)++; *p < q; (*p)++, i++ )
181 Fanins[i] = Dau_DsdToGia2_rec( pGia, pStr, p, pMatches, pLits, vCover );
182 assert( i == nVars );
183 assert( *p == q );
184// Res = Dau_DsdToGia2Compose_rec( pGia, Func, Fanins, nVars );
185 vLeaves.nCap = nVars;
186 vLeaves.nSize = nVars;
187 vLeaves.pArray = Fanins;
188 Res = Kit_TruthToGia( pGia, (unsigned *)pFunc, nVars, vCover, &vLeaves, 1 );
189 m_Non1Step++;
190 return Abc_LitNotCond( Res, fCompl );
191 }
192 assert( 0 );
193 return 0;
194}
195int Dau_DsdToGia2( Gia_Man_t * pGia, char * p, int * pLits, Vec_Int_t * vCover )
196{
197 int Res;
198 if ( *p == '0' && *(p+1) == 0 )
199 Res = 0;
200 else if ( *p == '1' && *(p+1) == 0 )
201 Res = 1;
202 else
203 Res = Dau_DsdToGia2_rec( pGia, p, &p, Dau_DsdComputeMatches(p), pLits, vCover );
204 assert( *++p == 0 );
205 return Res;
206}
207
219void Dau_DsdAddToArray( Gia_Man_t * pGia, int * pFans, int nFans, int iFan )
220{
221 int i;
222 pFans[nFans] = iFan;
223 if ( nFans == 0 )
224 return;
225 for ( i = nFans; i > 0; i-- )
226 {
227 if ( Gia_ObjLevelId(pGia, Abc_Lit2Var(pFans[i])) <= Gia_ObjLevelId(pGia, Abc_Lit2Var(pFans[i-1])) )
228 return;
229 ABC_SWAP( int, pFans[i], pFans[i-1] );
230 }
231}
232int Dau_DsdBalance( Gia_Man_t * pGia, int * pFans, int nFans, int fAnd )
233{
234 Gia_Obj_t * pObj;
235 int iFan0, iFan1, iFan;
236 if ( nFans == 1 )
237 return pFans[0];
238 assert( nFans > 1 );
239 iFan0 = pFans[--nFans];
240 iFan1 = pFans[--nFans];
241 if ( Vec_IntSize(&pGia->vHTable) == 0 )
242 {
243 if ( fAnd )
244 iFan = Gia_ManAppendAnd2( pGia, iFan0, iFan1 );
245 else if ( pGia->pMuxes )
246 {
247 int fCompl = Abc_LitIsCompl(iFan0) ^ Abc_LitIsCompl(iFan1);
248 iFan = Gia_ManAppendXorReal( pGia, Abc_LitRegular(iFan0), Abc_LitRegular(iFan1) );
249 iFan = Abc_LitNotCond( iFan, fCompl );
250 }
251 else
252 iFan = Gia_ManAppendXor2( pGia, iFan0, iFan1 );
253 }
254 else
255 {
256 if ( fAnd )
257 iFan = Gia_ManHashAnd( pGia, iFan0, iFan1 );
258 else if ( pGia->pMuxes )
259 iFan = Gia_ManHashXorReal( pGia, iFan0, iFan1 );
260 else
261 iFan = Gia_ManHashXor( pGia, iFan0, iFan1 );
262 }
263 pObj = Gia_ManObj(pGia, Abc_Lit2Var(iFan));
264 if ( Gia_ObjIsAnd(pObj) )
265 {
266 if ( fAnd )
267 Gia_ObjSetAndLevel( pGia, pObj );
268 else if ( pGia->pMuxes )
269 Gia_ObjSetXorLevel( pGia, pObj );
270 else
271 {
272 if ( Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) )
273 Gia_ObjSetAndLevel( pGia, Gia_ObjFanin0(pObj) );
274 if ( Gia_ObjIsAnd(Gia_ObjFanin1(pObj)) )
275 Gia_ObjSetAndLevel( pGia, Gia_ObjFanin1(pObj) );
276 Gia_ObjSetAndLevel( pGia, pObj );
277 }
278 }
279 Dau_DsdAddToArray( pGia, pFans, nFans++, iFan );
280 return Dau_DsdBalance( pGia, pFans, nFans, fAnd );
281}
282int Dau_DsdToGia_rec( Gia_Man_t * pGia, char * pStr, char ** p, int * pMatches, int * pLits, Vec_Int_t * vCover )
283{
284 int fCompl = 0;
285 if ( **p == '!' )
286 (*p)++, fCompl = 1;
287 if ( **p >= 'a' && **p < 'a' + DAU_DSD_MAX_VAR ) // var
288 return Abc_LitNotCond( pLits[**p - 'a'], fCompl );
289 if ( **p == '(' ) // and/or
290 {
291 char * q = pStr + pMatches[ *p - pStr ];
292 int pFans[DAU_DSD_MAX_VAR], nFans = 0, Fan;
293 assert( **p == '(' && *q == ')' );
294 for ( (*p)++; *p < q; (*p)++ )
295 {
296 Fan = Dau_DsdToGia_rec( pGia, pStr, p, pMatches, pLits, vCover );
297 Dau_DsdAddToArray( pGia, pFans, nFans++, Fan );
298 }
299 Fan = Dau_DsdBalance( pGia, pFans, nFans, 1 );
300 assert( *p == q );
301 return Abc_LitNotCond( Fan, fCompl );
302 }
303 if ( **p == '[' ) // xor
304 {
305 char * q = pStr + pMatches[ *p - pStr ];
306 int pFans[DAU_DSD_MAX_VAR], nFans = 0, Fan;
307 assert( **p == '[' && *q == ']' );
308 for ( (*p)++; *p < q; (*p)++ )
309 {
310 Fan = Dau_DsdToGia_rec( pGia, pStr, p, pMatches, pLits, vCover );
311 Dau_DsdAddToArray( pGia, pFans, nFans++, Fan );
312 }
313 Fan = Dau_DsdBalance( pGia, pFans, nFans, 0 );
314 assert( *p == q );
315 return Abc_LitNotCond( Fan, fCompl );
316 }
317 if ( **p == '<' ) // mux
318 {
319 Gia_Obj_t * pObj;
320 int nVars = 0;
321 int Temp[3], * pTemp = Temp, Res;
322 int Fanins[DAU_DSD_MAX_VAR], * pLits2;
323 char * pOld = *p;
324 char * q = pStr + pMatches[ *p - pStr ];
325 // read fanins
326 if ( *(q+1) == '{' )
327 {
328 char * q2;
329 *p = q+1;
330 q2 = pStr + pMatches[ *p - pStr ];
331 assert( **p == '{' && *q2 == '}' );
332 for ( nVars = 0, (*p)++; *p < q2; (*p)++, nVars++ )
333 Fanins[nVars] = Dau_DsdToGia_rec( pGia, pStr, p, pMatches, pLits, vCover );
334 assert( *p == q2 );
335 pLits2 = Fanins;
336 }
337 else
338 pLits2 = pLits;
339 // read MUX
340 *p = pOld;
341 q = pStr + pMatches[ *p - pStr ];
342 assert( **p == '<' && *q == '>' );
343 // verify internal variables
344 if ( nVars )
345 for ( ; pOld < q; pOld++ )
346 if ( *pOld >= 'a' && *pOld <= 'z' )
347 assert( *pOld - 'a' < nVars );
348 // derive MUX components
349 for ( (*p)++; *p < q; (*p)++ )
350 *pTemp++ = Dau_DsdToGia_rec( pGia, pStr, p, pMatches, pLits2, vCover );
351 assert( pTemp == Temp + 3 );
352 assert( *p == q );
353 if ( *(q+1) == '{' ) // and/or
354 {
355 char * q = pStr + pMatches[ ++(*p) - pStr ];
356 assert( **p == '{' && *q == '}' );
357 *p = q;
358 }
359 if ( Vec_IntSize(&pGia->vHTable) == 0 )
360 {
361 if ( pGia->pMuxes )
362 Res = Gia_ManAppendMux( pGia, Temp[0], Temp[1], Temp[2] );
363 else
364 Res = Gia_ManAppendMux2( pGia, Temp[0], Temp[1], Temp[2] );
365 }
366 else
367 {
368 if ( pGia->pMuxes )
369 Res = Gia_ManHashMuxReal( pGia, Temp[0], Temp[1], Temp[2] );
370 else
371 Res = Gia_ManHashMux( pGia, Temp[0], Temp[1], Temp[2] );
372 }
373 pObj = Gia_ManObj(pGia, Abc_Lit2Var(Res));
374 if ( Gia_ObjIsAnd(pObj) )
375 {
376 if ( pGia->pMuxes && Vec_IntSize(&pGia->vHTable) )
377 Gia_ObjSetMuxLevel( pGia, pObj );
378 else
379 {
380 if ( Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) )
381 Gia_ObjSetAndLevel( pGia, Gia_ObjFanin0(pObj) );
382 if ( Gia_ObjIsAnd(Gia_ObjFanin1(pObj)) )
383 Gia_ObjSetAndLevel( pGia, Gia_ObjFanin1(pObj) );
384 Gia_ObjSetAndLevel( pGia, pObj );
385 }
386 }
387 return Abc_LitNotCond( Res, fCompl );
388 }
389 if ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
390 {
391 Vec_Int_t vLeaves; char * q;
392 word pFunc[DAU_DSD_MAX_VAR > 6 ? (1 << (DAU_DSD_MAX_VAR-6)) : 1];
393 int Fanins[DAU_DSD_MAX_VAR], Res, nObjOld;
394 int i, nVars = Abc_TtReadHex( pFunc, *p );
395 *p += Abc_TtHexDigitNum( nVars );
396 q = pStr + pMatches[ *p - pStr ];
397 assert( **p == '{' && *q == '}' );
398 for ( i = 0, (*p)++; *p < q; (*p)++, i++ )
399 Fanins[i] = Dau_DsdToGia_rec( pGia, pStr, p, pMatches, pLits, vCover );
400 assert( i == nVars );
401 assert( *p == q );
402 vLeaves.nCap = nVars;
403 vLeaves.nSize = nVars;
404 vLeaves.pArray = Fanins;
405 nObjOld = Gia_ManObjNum(pGia);
406 Res = Kit_TruthToGia( pGia, (unsigned *)pFunc, nVars, vCover, &vLeaves, Vec_IntSize(&pGia->vHTable) != 0 );
407// assert( nVars <= 6 );
408// Res = Dau_DsdToGiaCompose_rec( pGia, pFunc[0], Fanins, nVars );
409 for ( i = nObjOld; i < Gia_ManObjNum(pGia); i++ )
410 Gia_ObjSetGateLevel( pGia, Gia_ManObj(pGia, i) );
411 m_Non1Step++;
412 return Abc_LitNotCond( Res, fCompl );
413 }
414 assert( 0 );
415 return 0;
416}
417int Dau_DsdToGia( Gia_Man_t * pGia, char * p, int * pLits, Vec_Int_t * vCover )
418{
419 int Res;
420 if ( *p == '0' && *(p+1) == 0 )
421 Res = 0;
422 else if ( *p == '1' && *(p+1) == 0 )
423 Res = 1;
424 else
425 Res = Dau_DsdToGia_rec( pGia, p, &p, Dau_DsdComputeMatches(p), pLits, vCover );
426 assert( *++p == 0 );
427 return Res;
428}
429
441int Dsm_ManTruthToGia( void * p, word * pTruth, Vec_Int_t * vLeaves, Vec_Int_t * vCover )
442{
443 int fUseMuxes = 0;
444 int fDelayBalance = 1;
445 Gia_Man_t * pGia = (Gia_Man_t *)p;
446 int nSizeNonDec;
447 char pDsd[DAU_MAX_STR];
448 word pTruthCopy[DAU_MAX_WORD];
449 Abc_TtCopy( pTruthCopy, pTruth, Abc_TtWordNum(Vec_IntSize(vLeaves)), 0 );
450 m_Calls++;
451 assert( Vec_IntSize(vLeaves) <= DAU_DSD_MAX_VAR );
452 if ( Vec_IntSize(vLeaves) == 0 )
453 return (int)(pTruth[0] & 1);
454 if ( Vec_IntSize(vLeaves) == 1 )
455 return Abc_LitNotCond( Vec_IntEntry(vLeaves, 0), (int)(pTruth[0] & 1) );
456 // collect delay information
457 if ( fDelayBalance && fUseMuxes )
458 {
459 int i, iLit, pVarLevels[DAU_DSD_MAX_VAR];
460 Vec_IntForEachEntry( vLeaves, iLit, i )
461 pVarLevels[i] = Gia_ObjLevelId( pGia, Abc_Lit2Var(iLit) );
462 nSizeNonDec = Dau_DsdDecomposeLevel( pTruthCopy, Vec_IntSize(vLeaves), fUseMuxes, 1, pDsd, pVarLevels );
463 }
464 else
465 nSizeNonDec = Dau_DsdDecompose( pTruthCopy, Vec_IntSize(vLeaves), fUseMuxes, 1, pDsd );
466 if ( nSizeNonDec )
467 m_NonDsd++;
468// printf( "%s\n", pDsd );
469 if ( fDelayBalance && pGia->vLevels )
470 return Dau_DsdToGia( pGia, pDsd, Vec_IntArray(vLeaves), vCover );
471 else
472 return Dau_DsdToGia2( pGia, pDsd, Vec_IntArray(vLeaves), vCover );
473}
474
486void Dsm_ManReportStats()
487{
488 printf( "Calls = %d. NonDSD = %d. Non1Step = %d.\n", m_Calls, m_NonDsd, m_Non1Step );
489 m_Calls = m_NonDsd = m_Non1Step = 0;
490}
491
503void * Dsm_ManDeriveGia( void * pGia, int fUseMuxes )
504{
505 Gia_Man_t * p = (Gia_Man_t *)pGia;
506 Gia_Man_t * pNew, * pTemp;
507 Vec_Int_t * vCover, * vLeaves;
508 Gia_Obj_t * pObj;
509 int k, i, iLut, iVar;
510 word * pTruth;
511 assert( Gia_ManHasMapping(p) );
512 // create new manager
513 pNew = Gia_ManStart( 6*Gia_ManObjNum(p)/5 + 100 );
514 pNew->pName = Abc_UtilStrsav( p->pName );
515 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
516 pNew->vLevels = Vec_IntStart( 6*Gia_ManObjNum(p)/5 + 100 );
517 if ( fUseMuxes )
518 pNew->pMuxes = ABC_CALLOC( unsigned, pNew->nObjsAlloc );
519 // map primary inputs
520 Gia_ManFillValue(p);
521 Gia_ManConst0(p)->Value = 0;
522 Gia_ManForEachCi( p, pObj, i )
523 pObj->Value = Gia_ManAppendCi(pNew);
524 // iterate through nodes used in the mapping
525 vLeaves = Vec_IntAlloc( 16 );
526 vCover = Vec_IntAlloc( 1 << 16 );
527 Gia_ManHashStart( pNew );
528 Gia_ObjComputeTruthTableStart( p, Gia_ManLutSizeMax(p) );
529 Gia_ManForEachAnd( p, pObj, iLut )
530 {
531 if ( Gia_ObjIsBuf(pObj) )
532 {
533 pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
534 continue;
535 }
536 if ( !Gia_ObjIsLut(p, iLut) )
537 continue;
538 // collect leaves
539 Vec_IntClear( vLeaves );
540 Gia_LutForEachFanin( p, iLut, iVar, k )
541 Vec_IntPush( vLeaves, iVar );
542 pTruth = Gia_ObjComputeTruthTableCut( p, Gia_ManObj(p, iLut), vLeaves );
543 // collect incoming literals
544 Vec_IntClear( vLeaves );
545 Gia_LutForEachFanin( p, iLut, iVar, k )
546 Vec_IntPush( vLeaves, Gia_ManObj(p, iVar)->Value );
547 Gia_ManObj(p, iLut)->Value = Dsm_ManTruthToGia( pNew, pTruth, vLeaves, vCover );
548 }
549 Gia_ObjComputeTruthTableStop( p );
550 Gia_ManForEachCo( p, pObj, i )
551 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
552 Gia_ManHashStop( pNew );
553 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
554 Vec_IntFree( vLeaves );
555 Vec_IntFree( vCover );
556/*
557 Gia_ManForEachAnd( pNew, pObj, i )
558 {
559 int iLev = Gia_ObjLevelId(pNew, i);
560 int iLev0 = Gia_ObjLevelId(pNew, Gia_ObjFaninId0(pObj, i));
561 int iLev1 = Gia_ObjLevelId(pNew, Gia_ObjFaninId1(pObj, i));
562 assert( iLev == 1 + Abc_MaxInt(iLev0, iLev1) );
563 }
564*/
565 // perform cleanup
566 pNew = Gia_ManCleanup( pTemp = pNew );
567 Gia_ManStop( pTemp );
568 return pNew;
569}
570
571
572
576
577
578ABC_NAMESPACE_IMPL_END
579
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition abc_global.h:253
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Dau_DsdToGia2
int Dau_DsdToGia2(Gia_Man_t *pGia, char *p, int *pLits, Vec_Int_t *vCover)
Definition dauGia.c:195
Dau_DsdAddToArray
void Dau_DsdAddToArray(Gia_Man_t *pGia, int *pFans, int nFans, int iFan)
Definition dauGia.c:219
Dsm_ManTruthToGia
int Dsm_ManTruthToGia(void *p, word *pTruth, Vec_Int_t *vLeaves, Vec_Int_t *vCover)
Definition dauGia.c:441
Dau_DsdBalance
int Dau_DsdBalance(Gia_Man_t *pGia, int *pFans, int nFans, int fAnd)
Definition dauGia.c:232
DAU_DSD_MAX_VAR
#define DAU_DSD_MAX_VAR
Definition dauGia.c:33
Dau_DsdToGia_rec
int Dau_DsdToGia_rec(Gia_Man_t *pGia, char *pStr, char **p, int *pMatches, int *pLits, Vec_Int_t *vCover)
Definition dauGia.c:282
Dsm_ManReportStats
void Dsm_ManReportStats()
Definition dauGia.c:486
Dau_DsdToGia2_rec
int Dau_DsdToGia2_rec(Gia_Man_t *pGia, char *pStr, char **p, int *pMatches, int *pLits, Vec_Int_t *vCover)
Definition dauGia.c:88
Kit_TruthToGia
ABC_NAMESPACE_IMPL_START int Kit_TruthToGia(Gia_Man_t *pMan, unsigned *pTruth, int nVars, Vec_Int_t *vMemory, Vec_Int_t *vLeaves, int fHash)
DECLARATIONS ///.
Definition kitHop.c:80
Dau_DsdToGiaCompose_rec
int Dau_DsdToGiaCompose_rec(Gia_Man_t *pGia, word Func, int *pFanins, int nVars)
FUNCTION DEFINITIONS ///.
Definition dauGia.c:54
Dsm_ManDeriveGia
void * Dsm_ManDeriveGia(void *pGia, int fUseMuxes)
Definition dauGia.c:503
Dau_DsdToGia
int Dau_DsdToGia(Gia_Man_t *pGia, char *p, int *pLits, Vec_Int_t *vCover)
Definition dauGia.c:417
DAU_MAX_WORD
#define DAU_MAX_WORD
Definition dau.h:44
Dau_DsdDecompose
int Dau_DsdDecompose(word *pTruth, int nVarsInit, int fSplitPrime, int fWriteTruth, char *pRes)
Definition dauDsd.c:1912
Dau_DsdDecomposeLevel
int Dau_DsdDecomposeLevel(word *pTruth, int nVarsInit, int fSplitPrime, int fWriteTruth, char *pRes, int *pVarLevels)
Definition dauDsd.c:1936
Dau_DsdComputeMatches
int * Dau_DsdComputeMatches(char *p)
Definition dauDsd.c:80
DAU_MAX_STR
#define DAU_MAX_STR
Definition dau.h:43
p
Cube * p
Definition exorList.c:222
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
Gia_ObjComputeTruthTableCut
word * Gia_ObjComputeTruthTableCut(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vLeaves)
Definition giaTruth.c:628
Gia_ManHashStart
void Gia_ManHashStart(Gia_Man_t *p)
Definition giaHash.c:125
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition gia.h:1214
Gia_ManHashMuxReal
int Gia_ManHashMuxReal(Gia_Man_t *p, int iLitC, int iLit1, int iLit0)
Definition giaHash.c:521
Gia_ManSetRegNum
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition giaMan.c:764
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
FUNCTION DEFINITIONS ///.
Definition giaMan.c:57
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_LutForEachFanin
#define Gia_LutForEachFanin(p, i, iFan, k)
Definition gia.h:1161
Gia_ManHashXor
int Gia_ManHashXor(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:668
Gia_ManFillValue
void Gia_ManFillValue(Gia_Man_t *p)
Definition giaUtil.c:369
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_ManHashMux
int Gia_ManHashMux(Gia_Man_t *p, int iCtrl, int iData1, int iData0)
Definition giaHash.c:692
Gia_ManCleanup
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition giaScl.c:84
Gia_ObjComputeTruthTableStart
void Gia_ObjComputeTruthTableStart(Gia_Man_t *p, int nVarsMax)
Definition giaTruth.c:552
Gia_ManLutSizeMax
int Gia_ManLutSizeMax(Gia_Man_t *p)
Definition giaIf.c:127
Gia_ObjComputeTruthTableStop
void Gia_ObjComputeTruthTableStop(Gia_Man_t *p)
Definition giaTruth.c:568
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:576
Gia_ManHashXorReal
int Gia_ManHashXorReal(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:469
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition gia.h:1236
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition gia.h:1228
Gia_ManHashStop
void Gia_ManHashStop(Gia_Man_t *p)
Definition giaHash.c:149
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
Gia_Man_t_::vLevels
Vec_Int_t * vLevels
Definition gia.h:120
Gia_Man_t_::pMuxes
unsigned * pMuxes
Definition gia.h:106
Gia_Man_t_::pSpec
char * pSpec
Definition gia.h:100
Gia_Man_t_::vHTable
Vec_Int_t vHTable
Definition gia.h:113
Gia_Man_t_::nObjsAlloc
int nObjsAlloc
Definition gia.h:104
Gia_Man_t_::pName
char * pName
Definition gia.h:99
Gia_Obj_t_::Value
unsigned Value
Definition gia.h:89
assert
#define assert(ex)
Definition util_old.h:213
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54