1 /**CFile****************************************************************
2
3 FileName [dauTree.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [DAG-aware unmapping.]
8
9 Synopsis [Canonical DSD package.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: dauTree.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "dauInt.h"
22 #include "misc/mem/mem.h"
23 #include "misc/util/utilTruth.h"
24
25 ABC_NAMESPACE_IMPL_START
26
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30
31 typedef struct Dss_Fun_t_ Dss_Fun_t;
32 struct Dss_Fun_t_
33 {
34 unsigned iDsd : 26; // DSD literal
35 unsigned nFans : 6; // fanin count
36 unsigned char pFans[0]; // fanins
37 };
38
39 typedef struct Dss_Ent_t_ Dss_Ent_t;
40 struct Dss_Ent_t_
41 {
42 Dss_Fun_t * pFunc;
43 Dss_Ent_t * pNext;
44 unsigned iDsd0 : 27; // dsd entry
45 unsigned nWords : 5; // total word count (struct + shared)
46 unsigned iDsd1 : 27; // dsd entry
47 unsigned nShared: 5; // shared count
48 unsigned char pShared[0]; // shared literals
49 };
50
51 typedef struct Dss_Obj_t_ Dss_Obj_t;
52 struct Dss_Obj_t_
53 {
54 unsigned Id; // node ID
55 unsigned Type : 3; // node type
56 unsigned nSupp : 8; // variable
57 unsigned iVar : 8; // variable
58 unsigned nWords : 6; // variable
59 unsigned fMark0 : 1; // user mark
60 unsigned fMark1 : 1; // user mark
61 unsigned nFans : 5; // fanin count
62 unsigned pFans[0]; // fanins
63 };
64
65 typedef struct Dss_Ntk_t_ Dss_Ntk_t;
66 struct Dss_Ntk_t_
67 {
68 int nVars; // the number of variables
69 int nMem; // memory used
70 int nMemAlloc; // memory allocated
71 word * pMem; // memory array
72 Dss_Obj_t * pRoot; // root node
73 Vec_Ptr_t * vObjs; // internal nodes
74 };
75
76 struct Dss_Man_t_
77 {
78 int nVars; // variable number
79 int nNonDecLimit; // limit on non-dec size
80 int nBins; // table size
81 unsigned * pBins; // hash table
82 Mem_Flex_t * pMem; // memory for nodes
83 Vec_Ptr_t * vObjs; // objects
84 Vec_Int_t * vNexts; // next pointers
85 Vec_Int_t * vLeaves; // temp
86 Vec_Int_t * vCopies; // temp
87 word ** pTtElems; // elementary TTs
88 Dss_Ent_t ** pCache; // decomposition cache
89 int nCache; // size of decomposition cache
90 Mem_Flex_t * pMemEnts; // memory for cache entries
91 int nCacheHits[2];
92 int nCacheMisses[2];
93 int nCacheEntries[2];
94 abctime timeBeg;
95 abctime timeDec;
96 abctime timeLook;
97 abctime timeEnd;
98 };
99
Dss_Regular(Dss_Obj_t * p)100 static inline Dss_Obj_t * Dss_Regular( Dss_Obj_t * p ) { return (Dss_Obj_t *)((ABC_PTRUINT_T)(p) & ~01); }
Dss_Not(Dss_Obj_t * p)101 static inline Dss_Obj_t * Dss_Not( Dss_Obj_t * p ) { return (Dss_Obj_t *)((ABC_PTRUINT_T)(p) ^ 01); }
Dss_NotCond(Dss_Obj_t * p,int c)102 static inline Dss_Obj_t * Dss_NotCond( Dss_Obj_t * p, int c ) { return (Dss_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c)); }
Dss_IsComplement(Dss_Obj_t * p)103 static inline int Dss_IsComplement( Dss_Obj_t * p ) { return (int)((ABC_PTRUINT_T)(p) & 01); }
104
Dss_EntWordNum(Dss_Ent_t * p)105 static inline int Dss_EntWordNum( Dss_Ent_t * p ) { return sizeof(Dss_Ent_t) / 8 + p->nShared / 4 + ((p->nShared & 3) > 0); }
Dss_FunWordNum(Dss_Fun_t * p)106 static inline int Dss_FunWordNum( Dss_Fun_t * p ) { assert(p->nFans >= 2); return (p->nFans + 4) / 8 + (((p->nFans + 4) & 7) > 0); }
Dss_ObjWordNum(int nFans)107 static inline int Dss_ObjWordNum( int nFans ) { return sizeof(Dss_Obj_t) / 8 + nFans / 2 + ((nFans & 1) > 0); }
Dss_ObjTruth(Dss_Obj_t * pObj)108 static inline word * Dss_ObjTruth( Dss_Obj_t * pObj ) { return (word *)pObj + pObj->nWords; }
109
Dss_ObjClean(Dss_Obj_t * pObj)110 static inline void Dss_ObjClean( Dss_Obj_t * pObj ) { memset( pObj, 0, sizeof(Dss_Obj_t) ); }
Dss_ObjId(Dss_Obj_t * pObj)111 static inline int Dss_ObjId( Dss_Obj_t * pObj ) { return pObj->Id; }
Dss_ObjType(Dss_Obj_t * pObj)112 static inline int Dss_ObjType( Dss_Obj_t * pObj ) { return pObj->Type; }
Dss_ObjSuppSize(Dss_Obj_t * pObj)113 static inline int Dss_ObjSuppSize( Dss_Obj_t * pObj ) { return pObj->nSupp; }
Dss_ObjFaninNum(Dss_Obj_t * pObj)114 static inline int Dss_ObjFaninNum( Dss_Obj_t * pObj ) { return pObj->nFans; }
Dss_ObjFaninC(Dss_Obj_t * pObj,int i)115 static inline int Dss_ObjFaninC( Dss_Obj_t * pObj, int i ) { assert(i < (int)pObj->nFans); return Abc_LitIsCompl(pObj->pFans[i]); }
116
Dss_VecObj(Vec_Ptr_t * p,int Id)117 static inline Dss_Obj_t * Dss_VecObj( Vec_Ptr_t * p, int Id ) { return (Dss_Obj_t *)Vec_PtrEntry(p, Id); }
Dss_VecConst0(Vec_Ptr_t * p)118 static inline Dss_Obj_t * Dss_VecConst0( Vec_Ptr_t * p ) { return Dss_VecObj( p, 0 ); }
Dss_VecVar(Vec_Ptr_t * p,int v)119 static inline Dss_Obj_t * Dss_VecVar( Vec_Ptr_t * p, int v ) { return Dss_VecObj( p, v+1 ); }
Dss_VecLitSuppSize(Vec_Ptr_t * p,int iLit)120 static inline int Dss_VecLitSuppSize( Vec_Ptr_t * p, int iLit ) { return Dss_VecObj( p, Abc_Lit2Var(iLit) )->nSupp; }
121
Dss_Obj2Lit(Dss_Obj_t * pObj)122 static inline int Dss_Obj2Lit( Dss_Obj_t * pObj ) { return Abc_Var2Lit(Dss_Regular(pObj)->Id, Dss_IsComplement(pObj)); }
Dss_Lit2Obj(Vec_Ptr_t * p,int iLit)123 static inline Dss_Obj_t * Dss_Lit2Obj( Vec_Ptr_t * p, int iLit ) { return Dss_NotCond(Dss_VecObj(p, Abc_Lit2Var(iLit)), Abc_LitIsCompl(iLit)); }
Dss_ObjFanin(Vec_Ptr_t * p,Dss_Obj_t * pObj,int i)124 static inline Dss_Obj_t * Dss_ObjFanin( Vec_Ptr_t * p, Dss_Obj_t * pObj, int i ) { assert(i < (int)pObj->nFans); return Dss_VecObj(p, Abc_Lit2Var(pObj->pFans[i])); }
Dss_ObjChild(Vec_Ptr_t * p,Dss_Obj_t * pObj,int i)125 static inline Dss_Obj_t * Dss_ObjChild( Vec_Ptr_t * p, Dss_Obj_t * pObj, int i ) { assert(i < (int)pObj->nFans); return Dss_Lit2Obj(p, pObj->pFans[i]); }
126
127 #define Dss_VecForEachObj( vVec, pObj, i ) \
128 Vec_PtrForEachEntry( Dss_Obj_t *, vVec, pObj, i )
129 #define Dss_VecForEachObjVec( vLits, vVec, pObj, i ) \
130 for ( i = 0; (i < Vec_IntSize(vLits)) && ((pObj) = Dss_Lit2Obj(vVec, Vec_IntEntry(vLits,i))); i++ )
131 #define Dss_VecForEachNode( vVec, pObj, i ) \
132 Vec_PtrForEachEntry( Dss_Obj_t *, vVec, pObj, i ) \
133 if ( pObj->Type == DAU_DSD_CONST0 || pObj->Type == DAU_DSD_VAR ) {} else
134 #define Dss_ObjForEachFanin( vVec, pObj, pFanin, i ) \
135 for ( i = 0; (i < Dss_ObjFaninNum(pObj)) && ((pFanin) = Dss_ObjFanin(vVec, pObj, i)); i++ )
136 #define Dss_ObjForEachChild( vVec, pObj, pFanin, i ) \
137 for ( i = 0; (i < Dss_ObjFaninNum(pObj)) && ((pFanin) = Dss_ObjChild(vVec, pObj, i)); i++ )
138
Dss_WordCountOnes(unsigned uWord)139 static inline int Dss_WordCountOnes( unsigned uWord )
140 {
141 uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
142 uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333);
143 uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F);
144 uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
145 return (uWord & 0x0000FFFF) + (uWord>>16);
146 }
147
Dss_Lit2Lit(int * pMapLit,int Lit)148 static inline int Dss_Lit2Lit( int * pMapLit, int Lit ) { return Abc_Var2Lit( Abc_Lit2Var(pMapLit[Abc_Lit2Var(Lit)]), Abc_LitIsCompl(Lit) ^ Abc_LitIsCompl(pMapLit[Abc_Lit2Var(Lit)]) ); }
149
150 ////////////////////////////////////////////////////////////////////////
151 /// FUNCTION DEFINITIONS ///
152 ////////////////////////////////////////////////////////////////////////
153
154 #if 0
155
156 /**Function*************************************************************
157
158 Synopsis [Check decomposability for 666.]
159
160 Description []
161
162 SideEffects []
163
164 SeeAlso []
165
166 ***********************************************************************/
167 // recursively collects 6-feasible supports
168 int Dss_ObjCheck666_rec( Dss_Ntk_t * p, Dss_Obj_t * pObj, Vec_Int_t * vSupps )
169 {
170 Dss_Obj_t * pFanin;
171 int i, uSupp = 0;
172 assert( !Dss_IsComplement(pObj) );
173 if ( pObj->Type == DAU_DSD_VAR )
174 {
175 assert( pObj->iVar >= 0 && pObj->iVar < 30 );
176 return (1 << pObj->iVar);
177 }
178 if ( pObj->Type == DAU_DSD_AND || pObj->Type == DAU_DSD_XOR )
179 {
180 int c0, c1, c2, uSuppTemp;
181 int uSuppVars[16];
182 int nSuppVars = 0;
183 int nFanins = Dss_ObjFaninNum(pObj);
184 int uSupps[16], nSuppSizes[16];
185 Dss_ObjForEachFanin( p->vObjs, pObj, pFanin, i )
186 {
187 uSupps[i] = Dss_ObjCheck666_rec( p, pFanin, vSupps );
188 nSuppSizes[i] = Dss_WordCountOnes( uSupps[i] );
189 uSupp |= uSupps[i];
190 if ( nSuppSizes[i] == 1 )
191 uSuppVars[nSuppVars++] = uSupps[i];
192 }
193 // iterate through the permutations
194 for ( c0 = 0; c0 < nFanins; c0++ )
195 if ( nSuppSizes[c0] > 1 && nSuppSizes[c0] < 6 )
196 {
197 uSuppTemp = uSupps[c0];
198 for ( i = 0; i < nSuppVars; i++ )
199 if ( nSuppSizes[c0] + i < 6 )
200 uSuppTemp |= uSuppVars[i];
201 else
202 break;
203 if ( Dss_WordCountOnes(uSuppTemp) <= 6 )
204 Vec_IntPush( vSupps, uSuppTemp );
205
206 for ( c1 = c0 + 1; c1 < nFanins; c1++ )
207 if ( nSuppSizes[c1] > 1 && nSuppSizes[c1] < 6 )
208 {
209 if ( nSuppSizes[c0] + nSuppSizes[c1] <= 6 )
210 Vec_IntPush( vSupps, uSupps[c0] | uSupps[c1] );
211
212 uSuppTemp = uSupps[c0] | uSupps[c1];
213 for ( i = 0; i < nSuppVars; i++ )
214 if ( nSuppSizes[c0] + nSuppSizes[c1] + i < 6 )
215 uSuppTemp |= uSuppVars[i];
216 else
217 break;
218 if ( Dss_WordCountOnes(uSuppTemp) <= 6 )
219 Vec_IntPush( vSupps, uSuppTemp );
220
221 for ( c2 = c1 + 1; c2 < nFanins; c2++ )
222 if ( nSuppSizes[c2] > 1 && nSuppSizes[c2] < 6 )
223 {
224 if ( nSuppSizes[c0] + nSuppSizes[c1] + nSuppSizes[c2] <= 6 )
225 Vec_IntPush( vSupps, uSupps[c0] | uSupps[c1] | uSupps[c2] );
226 assert( nSuppSizes[c0] + nSuppSizes[c1] + nSuppSizes[c2] >= 6 );
227 }
228 }
229 }
230 if ( nSuppVars > 1 && nSuppVars <= 6 )
231 {
232 uSuppTemp = 0;
233 for ( i = 0; i < nSuppVars; i++ )
234 uSuppTemp |= uSuppVars[i];
235 Vec_IntPush( vSupps, uSuppTemp );
236 }
237 else if ( nSuppVars > 6 && nSuppVars <= 12 )
238 {
239 uSuppTemp = 0;
240 for ( i = 0; i < 6; i++ )
241 uSuppTemp |= uSuppVars[i];
242 Vec_IntPush( vSupps, uSuppTemp );
243
244 uSuppTemp = 0;
245 for ( i = 6; i < nSuppVars; i++ )
246 uSuppTemp |= uSuppVars[i];
247 Vec_IntPush( vSupps, uSuppTemp );
248 }
249 }
250 else if ( pObj->Type == DAU_DSD_MUX || pObj->Type == DAU_DSD_PRIME )
251 {
252 Dss_ObjForEachFanin( p->vObjs, pObj, pFanin, i )
253 uSupp |= Dss_ObjCheck666_rec( p, pFanin, vSupps );
254 }
255 if ( Dss_WordCountOnes( uSupp ) <= 6 )
256 Vec_IntPush( vSupps, uSupp );
257 return uSupp;
258 }
259 int Dss_ObjCheck666( Dss_Ntk_t * p )
260 {
261 Vec_Int_t * vSupps;
262 int i, k, SuppI, SuppK;
263 int nSupp = Dss_ObjSuppSize(Dss_Regular(p->pRoot));
264 if ( nSupp <= 6 )
265 return 1;
266 // compute supports
267 vSupps = Vec_IntAlloc( 100 );
268 Dss_ObjCheck666_rec( p, Dss_Regular(p->pRoot), vSupps );
269 Vec_IntUniqify( vSupps );
270 Vec_IntForEachEntry( vSupps, SuppI, i )
271 {
272 k = Dss_WordCountOnes(SuppI);
273 assert( k > 0 && k <= 6 );
274 /*
275 for ( k = 0; k < 16; k++ )
276 if ( (SuppI >> k) & 1 )
277 printf( "%c", 'a' + k );
278 else
279 printf( "-" );
280 printf( "\n" );
281 */
282 }
283 // consider support pairs
284 Vec_IntForEachEntry( vSupps, SuppI, i )
285 Vec_IntForEachEntryStart( vSupps, SuppK, k, i+1 )
286 {
287 if ( SuppI & SuppK )
288 continue;
289 if ( Dss_WordCountOnes(SuppI | SuppK) + 4 >= nSupp )
290 {
291 Vec_IntFree( vSupps );
292 return 1;
293 }
294 }
295 Vec_IntFree( vSupps );
296 return 0;
297 }
298 void Dau_DsdTest_()
299 {
300 /*
301 extern Dss_Ntk_t * Dss_NtkCreate( char * pDsd, int nVars, word * pTruth );
302 extern void Dss_NtkFree( Dss_Ntk_t * p );
303
304 // char * pDsd = "(!(amn!(bh))[cdeij]!(fklg)o)";
305 char * pDsd = "<[(ab)(cd)(ef)][(gh)(ij)(kl)](mn)>";
306 Dss_Ntk_t * pNtk = Dss_NtkCreate( pDsd, 16, NULL );
307 int Status = Dss_ObjCheck666( pNtk );
308 Dss_NtkFree( pNtk );
309 */
310 }
311
312 abctime if_dec_time;
313
314 void Dau_DsdCheckStructOne( word * pTruth, int nVars, int nLeaves )
315 {
316 extern Dss_Ntk_t * Dss_NtkCreate( char * pDsd, int nVars, word * pTruth );
317 extern void Dss_NtkFree( Dss_Ntk_t * p );
318
319 static abctime timeTt = 0;
320 static abctime timeDsd = 0;
321 abctime clkTt, clkDsd;
322
323 char pDsd[1000];
324 word Truth[1024];
325 Dss_Ntk_t * pNtk;
326 int Status, nNonDec;
327
328 if ( pTruth == NULL )
329 {
330 Abc_PrintTime( 1, "TT runtime", timeTt );
331 Abc_PrintTime( 1, "DSD runtime", timeDsd );
332 Abc_PrintTime( 1, "Total ", if_dec_time );
333
334 if_dec_time = 0;
335 timeTt = 0;
336 timeDsd = 0;
337 return;
338 }
339
340 Abc_TtCopy( Truth, pTruth, Abc_TtWordNum(nVars), 0 );
341 nNonDec = Dau_DsdDecompose( Truth, nVars, 0, 0, pDsd );
342 if ( nNonDec > 0 )
343 return;
344
345 pNtk = Dss_NtkCreate( pDsd, 16, NULL );
346
347 // measure DSD runtime
348 clkDsd = Abc_Clock();
349 Status = Dss_ObjCheck666( pNtk );
350 timeDsd += Abc_Clock() - clkDsd;
351
352 Dss_NtkFree( pNtk );
353
354 // measure TT runtime
355 clkTt = Abc_Clock();
356 {
357 #define CLU_VAR_MAX 16
358
359 // decomposition
360 typedef struct If_Grp_t_ If_Grp_t;
361 struct If_Grp_t_
362 {
363 char nVars;
364 char nMyu;
365 char pVars[CLU_VAR_MAX];
366 };
367
368
369 int nLutLeaf = 6;
370 int nLutLeaf2 = 6;
371 int nLutRoot = 6;
372
373 If_Grp_t G;
374 If_Grp_t G2, R;
375 word Func0, Func1, Func2;
376
377 {
378 extern If_Grp_t If_CluCheck3( void * p, word * pTruth0, int nVars, int nLutLeaf, int nLutLeaf2, int nLutRoot,
379 If_Grp_t * pR, If_Grp_t * pG2, word * pFunc0, word * pFunc1, word * pFunc2 );
380 G = If_CluCheck3( NULL, pTruth, nLeaves, nLutLeaf, nLutLeaf2, nLutRoot, &R, &G2, &Func0, &Func1, &Func2 );
381 }
382
383 }
384 timeTt += Abc_Clock() - clkTt;
385 }
386
387 #endif
388
389
390 /**Function*************************************************************
391
392 Synopsis [Elementary truth tables.]
393
394 Description []
395
396 SideEffects []
397
398 SeeAlso []
399
400 ***********************************************************************/
Dss_ManTtElems()401 static inline word ** Dss_ManTtElems()
402 {
403 static word TtElems[DAU_MAX_VAR+1][DAU_MAX_WORD], * pTtElems[DAU_MAX_VAR+1] = {NULL};
404 if ( pTtElems[0] == NULL )
405 {
406 int v;
407 for ( v = 0; v <= DAU_MAX_VAR; v++ )
408 pTtElems[v] = TtElems[v];
409 Abc_TtElemInit( pTtElems, DAU_MAX_VAR );
410 }
411 return pTtElems;
412 }
413
414 /**Function*************************************************************
415
416 Synopsis [Creating DSD network.]
417
418 Description []
419
420 SideEffects []
421
422 SeeAlso []
423
424 ***********************************************************************/
Dss_ObjAllocNtk(Dss_Ntk_t * p,int Type,int nFans,int nTruthVars)425 Dss_Obj_t * Dss_ObjAllocNtk( Dss_Ntk_t * p, int Type, int nFans, int nTruthVars )
426 {
427 Dss_Obj_t * pObj;
428 pObj = (Dss_Obj_t *)(p->pMem + p->nMem);
429 Dss_ObjClean( pObj );
430 pObj->nFans = nFans;
431 pObj->nWords = Dss_ObjWordNum( nFans );
432 pObj->Type = Type;
433 pObj->Id = Vec_PtrSize( p->vObjs );
434 pObj->iVar = 31;
435 Vec_PtrPush( p->vObjs, pObj );
436 p->nMem += pObj->nWords + (nTruthVars ? Abc_TtWordNum(nTruthVars) : 0);
437 assert( p->nMem < p->nMemAlloc );
438 return pObj;
439 }
Dss_ObjCreateNtk(Dss_Ntk_t * p,int Type,Vec_Int_t * vFaninLits)440 Dss_Obj_t * Dss_ObjCreateNtk( Dss_Ntk_t * p, int Type, Vec_Int_t * vFaninLits )
441 {
442 Dss_Obj_t * pObj;
443 int i, Entry;
444 pObj = Dss_ObjAllocNtk( p, Type, Vec_IntSize(vFaninLits), Type == DAU_DSD_PRIME ? Vec_IntSize(vFaninLits) : 0 );
445 Vec_IntForEachEntry( vFaninLits, Entry, i )
446 {
447 pObj->pFans[i] = Entry;
448 pObj->nSupp += Dss_VecLitSuppSize(p->vObjs, Entry);
449 }
450 assert( i == (int)pObj->nFans );
451 return pObj;
452 }
Dss_NtkAlloc(int nVars)453 Dss_Ntk_t * Dss_NtkAlloc( int nVars )
454 {
455 Dss_Ntk_t * p;
456 Dss_Obj_t * pObj;
457 int i;
458 p = ABC_CALLOC( Dss_Ntk_t, 1 );
459 p->nVars = nVars;
460 p->nMemAlloc = DAU_MAX_STR;
461 p->pMem = ABC_ALLOC( word, p->nMemAlloc );
462 p->vObjs = Vec_PtrAlloc( 100 );
463 Dss_ObjAllocNtk( p, DAU_DSD_CONST0, 0, 0 );
464 for ( i = 0; i < nVars; i++ )
465 {
466 pObj = Dss_ObjAllocNtk( p, DAU_DSD_VAR, 0, 0 );
467 pObj->iVar = i;
468 pObj->nSupp = 1;
469 }
470 return p;
471 }
Dss_NtkFree(Dss_Ntk_t * p)472 void Dss_NtkFree( Dss_Ntk_t * p )
473 {
474 Vec_PtrFree( p->vObjs );
475 ABC_FREE( p->pMem );
476 ABC_FREE( p );
477 }
Dss_NtkPrint_rec(Dss_Ntk_t * p,Dss_Obj_t * pObj)478 void Dss_NtkPrint_rec( Dss_Ntk_t * p, Dss_Obj_t * pObj )
479 {
480 char OpenType[7] = {0, 0, 0, '(', '[', '<', '{'};
481 char CloseType[7] = {0, 0, 0, ')', ']', '>', '}'};
482 Dss_Obj_t * pFanin;
483 int i;
484 assert( !Dss_IsComplement(pObj) );
485 if ( pObj->Type == DAU_DSD_VAR )
486 { printf( "%c", 'a' + pObj->iVar ); return; }
487 if ( pObj->Type == DAU_DSD_PRIME )
488 Abc_TtPrintHexRev( stdout, Dss_ObjTruth(pObj), pObj->nFans );
489 printf( "%c", OpenType[pObj->Type] );
490 Dss_ObjForEachFanin( p->vObjs, pObj, pFanin, i )
491 {
492 printf( "%s", Dss_ObjFaninC(pObj, i) ? "!":"" );
493 Dss_NtkPrint_rec( p, pFanin );
494 }
495 printf( "%c", CloseType[pObj->Type] );
496 }
Dss_NtkPrint(Dss_Ntk_t * p)497 void Dss_NtkPrint( Dss_Ntk_t * p )
498 {
499 if ( Dss_Regular(p->pRoot)->Type == DAU_DSD_CONST0 )
500 printf( "%d", Dss_IsComplement(p->pRoot) );
501 else
502 {
503 printf( "%s", Dss_IsComplement(p->pRoot) ? "!":"" );
504 if ( Dss_Regular(p->pRoot)->Type == DAU_DSD_VAR )
505 printf( "%c", 'a' + Dss_Regular(p->pRoot)->iVar );
506 else
507 Dss_NtkPrint_rec( p, Dss_Regular(p->pRoot) );
508 }
509 printf( "\n" );
510 }
511
512 /**Function*************************************************************
513
514 Synopsis [Creating DSD network from SOP.]
515
516 Description []
517
518 SideEffects []
519
520 SeeAlso []
521
522 ***********************************************************************/
Dau_DsdMergeMatches(char * pDsd,int * pMatches)523 static inline void Dau_DsdMergeMatches( char * pDsd, int * pMatches )
524 {
525 int pNested[DAU_MAX_VAR];
526 int i, nNested = 0;
527 for ( i = 0; pDsd[i]; i++ )
528 {
529 pMatches[i] = 0;
530 if ( pDsd[i] == '(' || pDsd[i] == '[' || pDsd[i] == '<' || pDsd[i] == '{' )
531 pNested[nNested++] = i;
532 else if ( pDsd[i] == ')' || pDsd[i] == ']' || pDsd[i] == '>' || pDsd[i] == '}' )
533 pMatches[pNested[--nNested]] = i;
534 assert( nNested < DAU_MAX_VAR );
535 }
536 assert( nNested == 0 );
537 }
Dss_NtkCreate_rec(char * pStr,char ** p,int * pMatches,Dss_Ntk_t * pNtk,word * pTruth)538 int Dss_NtkCreate_rec( char * pStr, char ** p, int * pMatches, Dss_Ntk_t * pNtk, word * pTruth )
539 {
540 int fCompl = 0;
541 if ( **p == '!' )
542 {
543 fCompl = 1;
544 (*p)++;
545 }
546 while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
547 (*p)++;
548 /*
549 if ( **p == '<' )
550 {
551 char * q = pStr + pMatches[ *p - pStr ];
552 if ( *(q+1) == '{' )
553 *p = q+1;
554 }
555 */
556 if ( **p >= 'a' && **p <= 'z' ) // var
557 return Abc_Var2Lit( Dss_ObjId(Dss_VecVar(pNtk->vObjs, **p - 'a')), fCompl );
558 if ( **p == '(' || **p == '[' || **p == '<' || **p == '{' ) // and/or/xor
559 {
560 Dss_Obj_t * pObj;
561 Vec_Int_t * vFaninLits = Vec_IntAlloc( 10 );
562 char * q = pStr + pMatches[ *p - pStr ];
563 int Type = 0;
564 if ( **p == '(' )
565 Type = DAU_DSD_AND;
566 else if ( **p == '[' )
567 Type = DAU_DSD_XOR;
568 else if ( **p == '<' )
569 Type = DAU_DSD_MUX;
570 else if ( **p == '{' )
571 Type = DAU_DSD_PRIME;
572 else assert( 0 );
573 assert( *q == **p + 1 + (**p != '(') );
574 for ( (*p)++; *p < q; (*p)++ )
575 Vec_IntPush( vFaninLits, Dss_NtkCreate_rec(pStr, p, pMatches, pNtk, pTruth) );
576 assert( *p == q );
577 if ( Type == DAU_DSD_PRIME )
578 {
579 Vec_Int_t * vFaninLitsNew;
580 word pTemp[DAU_MAX_WORD];
581 char pCanonPerm[DAU_MAX_VAR];
582 int i, uCanonPhase, nFanins = Vec_IntSize(vFaninLits);
583 Abc_TtCopy( pTemp, pTruth, Abc_TtWordNum(nFanins), 0 );
584 uCanonPhase = Abc_TtCanonicize( pTemp, nFanins, pCanonPerm );
585 fCompl = (uCanonPhase >> nFanins) & 1;
586 vFaninLitsNew = Vec_IntAlloc( nFanins );
587 for ( i = 0; i < nFanins; i++ )
588 Vec_IntPush( vFaninLitsNew, Abc_LitNotCond(Vec_IntEntry(vFaninLits, pCanonPerm[i]), (uCanonPhase>>i)&1) );
589 pObj = Dss_ObjCreateNtk( pNtk, DAU_DSD_PRIME, vFaninLitsNew );
590 Abc_TtCopy( Dss_ObjTruth(pObj), pTemp, Abc_TtWordNum(nFanins), 0 );
591 Vec_IntFree( vFaninLitsNew );
592 }
593 else
594 pObj = Dss_ObjCreateNtk( pNtk, Type, vFaninLits );
595 Vec_IntFree( vFaninLits );
596 return Abc_LitNotCond( Dss_Obj2Lit(pObj), fCompl );
597 }
598 assert( 0 );
599 return -1;
600 }
Dss_NtkCreate(char * pDsd,int nVars,word * pTruth)601 Dss_Ntk_t * Dss_NtkCreate( char * pDsd, int nVars, word * pTruth )
602 {
603 int fCompl = 0;
604 Dss_Ntk_t * pNtk = Dss_NtkAlloc( nVars );
605 if ( *pDsd == '!' )
606 pDsd++, fCompl = 1;
607 if ( Dau_DsdIsConst(pDsd) )
608 pNtk->pRoot = Dss_VecConst0(pNtk->vObjs);
609 else if ( Dau_DsdIsVar(pDsd) )
610 pNtk->pRoot = Dss_VecVar(pNtk->vObjs, Dau_DsdReadVar(pDsd));
611 else
612 {
613 int iLit, pMatches[DAU_MAX_STR];
614 Dau_DsdMergeMatches( pDsd, pMatches );
615 iLit = Dss_NtkCreate_rec( pDsd, &pDsd, pMatches, pNtk, pTruth );
616 pNtk->pRoot = Dss_Lit2Obj( pNtk->vObjs, iLit );
617 }
618 if ( fCompl )
619 pNtk->pRoot = Dss_Not(pNtk->pRoot);
620 return pNtk;
621 }
622
623 /**Function*************************************************************
624
625 Synopsis [Comparing two DSD nodes.]
626
627 Description []
628
629 SideEffects []
630
631 SeeAlso []
632
633 ***********************************************************************/
Dss_ObjCompare(Vec_Ptr_t * p,Dss_Obj_t * p0i,Dss_Obj_t * p1i)634 int Dss_ObjCompare( Vec_Ptr_t * p, Dss_Obj_t * p0i, Dss_Obj_t * p1i )
635 {
636 Dss_Obj_t * p0 = Dss_Regular(p0i);
637 Dss_Obj_t * p1 = Dss_Regular(p1i);
638 Dss_Obj_t * pChild0, * pChild1;
639 int i, Res;
640 if ( Dss_ObjType(p0) < Dss_ObjType(p1) )
641 return -1;
642 if ( Dss_ObjType(p0) > Dss_ObjType(p1) )
643 return 1;
644 if ( Dss_ObjType(p0) < DAU_DSD_AND )
645 return 0;
646 if ( Dss_ObjFaninNum(p0) < Dss_ObjFaninNum(p1) )
647 return -1;
648 if ( Dss_ObjFaninNum(p0) > Dss_ObjFaninNum(p1) )
649 return 1;
650 for ( i = 0; i < Dss_ObjFaninNum(p0); i++ )
651 {
652 pChild0 = Dss_ObjChild( p, p0, i );
653 pChild1 = Dss_ObjChild( p, p1, i );
654 Res = Dss_ObjCompare( p, pChild0, pChild1 );
655 if ( Res != 0 )
656 return Res;
657 }
658 if ( Dss_IsComplement(p0i) < Dss_IsComplement(p1i) )
659 return -1;
660 if ( Dss_IsComplement(p0i) > Dss_IsComplement(p1i) )
661 return 1;
662 return 0;
663 }
Dss_ObjSort(Vec_Ptr_t * p,Dss_Obj_t ** pNodes,int nNodes,int * pPerm)664 void Dss_ObjSort( Vec_Ptr_t * p, Dss_Obj_t ** pNodes, int nNodes, int * pPerm )
665 {
666 int i, j, best_i;
667 for ( i = 0; i < nNodes-1; i++ )
668 {
669 best_i = i;
670 for ( j = i+1; j < nNodes; j++ )
671 if ( Dss_ObjCompare(p, pNodes[best_i], pNodes[j]) == 1 )
672 best_i = j;
673 if ( i == best_i )
674 continue;
675 ABC_SWAP( Dss_Obj_t *, pNodes[i], pNodes[best_i] );
676 if ( pPerm )
677 ABC_SWAP( int, pPerm[i], pPerm[best_i] );
678 }
679 }
680
681 /**Function*************************************************************
682
683 Synopsis []
684
685 Description []
686
687 SideEffects []
688
689 SeeAlso []
690
691 ***********************************************************************/
Dss_NtkCheck(Dss_Ntk_t * p)692 void Dss_NtkCheck( Dss_Ntk_t * p )
693 {
694 Dss_Obj_t * pObj, * pFanin;
695 int i, k;
696 Dss_VecForEachNode( p->vObjs, pObj, i )
697 {
698 Dss_ObjForEachFanin( p->vObjs, pObj, pFanin, k )
699 {
700 if ( pObj->Type == DAU_DSD_AND && pFanin->Type == DAU_DSD_AND )
701 assert( Dss_ObjFaninC(pObj, k) );
702 else if ( pObj->Type == DAU_DSD_XOR )
703 assert( pFanin->Type != DAU_DSD_XOR );
704 else if ( pObj->Type == DAU_DSD_MUX )
705 assert( !Dss_ObjFaninC(pObj, 0) );
706 }
707 }
708 }
Dss_NtkCollectPerm_rec(Dss_Ntk_t * p,Dss_Obj_t * pObj,int * pPermDsd,int * pnPerms)709 int Dss_NtkCollectPerm_rec( Dss_Ntk_t * p, Dss_Obj_t * pObj, int * pPermDsd, int * pnPerms )
710 {
711 Dss_Obj_t * pChild;
712 int k, fCompl = Dss_IsComplement(pObj);
713 pObj = Dss_Regular( pObj );
714 if ( pObj->Type == DAU_DSD_VAR )
715 {
716 pPermDsd[*pnPerms] = Abc_Var2Lit(pObj->iVar, fCompl);
717 pObj->iVar = (*pnPerms)++;
718 return fCompl;
719 }
720 Dss_ObjForEachChild( p->vObjs, pObj, pChild, k )
721 if ( Dss_NtkCollectPerm_rec( p, pChild, pPermDsd, pnPerms ) )
722 pObj->pFans[k] = (unsigned char)Abc_LitRegular((int)pObj->pFans[k]);
723 return 0;
724 }
Dss_NtkTransform(Dss_Ntk_t * p,int * pPermDsd)725 void Dss_NtkTransform( Dss_Ntk_t * p, int * pPermDsd )
726 {
727 Dss_Obj_t * pChildren[DAU_MAX_VAR];
728 Dss_Obj_t * pObj, * pChild;
729 int i, k, nPerms;
730 if ( Dss_Regular(p->pRoot)->Type == DAU_DSD_CONST0 )
731 return;
732 Dss_VecForEachNode( p->vObjs, pObj, i )
733 {
734 if ( pObj->Type == DAU_DSD_MUX || pObj->Type == DAU_DSD_PRIME )
735 continue;
736 Dss_ObjForEachChild( p->vObjs, pObj, pChild, k )
737 pChildren[k] = pChild;
738 Dss_ObjSort( p->vObjs, pChildren, Dss_ObjFaninNum(pObj), NULL );
739 for ( k = 0; k < Dss_ObjFaninNum(pObj); k++ )
740 pObj->pFans[k] = Dss_Obj2Lit( pChildren[k] );
741 }
742 nPerms = 0;
743 if ( Dss_NtkCollectPerm_rec( p, p->pRoot, pPermDsd, &nPerms ) )
744 p->pRoot = Dss_Regular(p->pRoot);
745 assert( nPerms == (int)Dss_Regular(p->pRoot)->nSupp );
746 }
747
748
749 /**Function*************************************************************
750
751 Synopsis []
752
753 Description []
754
755 SideEffects []
756
757 SeeAlso []
758
759 ***********************************************************************/
Dss_ObjAlloc(Dss_Man_t * p,int Type,int nFans,int nTruthVars)760 Dss_Obj_t * Dss_ObjAlloc( Dss_Man_t * p, int Type, int nFans, int nTruthVars )
761 {
762 int nWords = Dss_ObjWordNum(nFans) + (nTruthVars ? Abc_TtWordNum(nTruthVars) : 0);
763 Dss_Obj_t * pObj = (Dss_Obj_t *)Mem_FlexEntryFetch( p->pMem, sizeof(word) * nWords );
764 Dss_ObjClean( pObj );
765 pObj->Type = Type;
766 pObj->nFans = nFans;
767 pObj->nWords = Dss_ObjWordNum(nFans);
768 pObj->Id = Vec_PtrSize( p->vObjs );
769 pObj->iVar = 31;
770 Vec_PtrPush( p->vObjs, pObj );
771 Vec_IntPush( p->vNexts, 0 );
772 return pObj;
773 }
Dss_ObjCreate(Dss_Man_t * p,int Type,Vec_Int_t * vFaninLits,word * pTruth)774 Dss_Obj_t * Dss_ObjCreate( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits, word * pTruth )
775 {
776 Dss_Obj_t * pObj, * pFanin, * pPrev = NULL;
777 int i, Entry;
778 // check structural canonicity
779 assert( Type != DAU_DSD_MUX || Vec_IntSize(vFaninLits) == 3 );
780 assert( Type != DAU_DSD_MUX || !Abc_LitIsCompl(Vec_IntEntry(vFaninLits, 0)) );
781 assert( Type != DAU_DSD_MUX || !Abc_LitIsCompl(Vec_IntEntry(vFaninLits, 1)) || !Abc_LitIsCompl(Vec_IntEntry(vFaninLits, 2)) );
782 // check that leaves are in good order
783 if ( Type == DAU_DSD_AND || Type == DAU_DSD_XOR )
784 Dss_VecForEachObjVec( vFaninLits, p->vObjs, pFanin, i )
785 {
786 assert( Type != DAU_DSD_AND || Abc_LitIsCompl(Vec_IntEntry(vFaninLits, i)) || Dss_ObjType(pFanin) != DAU_DSD_AND );
787 assert( Type != DAU_DSD_XOR || Dss_ObjType(pFanin) != DAU_DSD_XOR );
788 assert( pPrev == NULL || Dss_ObjCompare(p->vObjs, pPrev, pFanin) <= 0 );
789 pPrev = pFanin;
790 }
791 // create new node
792 pObj = Dss_ObjAlloc( p, Type, Vec_IntSize(vFaninLits), Type == DAU_DSD_PRIME ? Vec_IntSize(vFaninLits) : 0 );
793 if ( Type == DAU_DSD_PRIME )
794 Abc_TtCopy( Dss_ObjTruth(pObj), pTruth, Abc_TtWordNum(Vec_IntSize(vFaninLits)), 0 );
795 assert( pObj->nSupp == 0 );
796 Vec_IntForEachEntry( vFaninLits, Entry, i )
797 {
798 pObj->pFans[i] = Entry;
799 pObj->nSupp += Dss_VecLitSuppSize(p->vObjs, Entry);
800 }
801 /*
802 {
803 extern void Dss_ManPrintOne( Dss_Man_t * p, int iDsdLit, int * pPermLits );
804 Dss_ManPrintOne( p, Dss_Obj2Lit(pObj), NULL );
805 }
806 */
807 return pObj;
808 }
809
810 /**Function*************************************************************
811
812 Synopsis []
813
814 Description []
815
816 SideEffects []
817
818 SeeAlso []
819
820 ***********************************************************************/
Dss_ManHashProfile(Dss_Man_t * p)821 void Dss_ManHashProfile( Dss_Man_t * p )
822 {
823 Dss_Obj_t * pObj;
824 unsigned * pSpot;
825 int i, Counter;
826 for ( i = 0; i < p->nBins; i++ )
827 {
828 Counter = 0;
829 for ( pSpot = p->pBins + i; *pSpot; pSpot = (unsigned *)Vec_IntEntryP(p->vNexts, pObj->Id), Counter++ )
830 pObj = Dss_VecObj( p->vObjs, *pSpot );
831 if ( Counter )
832 printf( "%d ", Counter );
833 }
834 printf( "\n" );
835 }
Dss_ObjHashKey(Dss_Man_t * p,int Type,Vec_Int_t * vFaninLits,word * pTruth)836 static inline unsigned Dss_ObjHashKey( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits, word * pTruth )
837 {
838 static int s_Primes[8] = { 1699, 4177, 5147, 5647, 6343, 7103, 7873, 8147 };
839 int i, Entry;
840 unsigned uHash = Type * 7873 + Vec_IntSize(vFaninLits) * 8147;
841 Vec_IntForEachEntry( vFaninLits, Entry, i )
842 uHash += Entry * s_Primes[i & 0x7];
843 assert( (Type == DAU_DSD_PRIME) == (pTruth != NULL) );
844 if ( pTruth )
845 {
846 unsigned char * pTruthC = (unsigned char *)pTruth;
847 int nBytes = Abc_TtByteNum(Vec_IntSize(vFaninLits));
848 for ( i = 0; i < nBytes; i++ )
849 uHash += pTruthC[i] * s_Primes[i & 0x7];
850 }
851 return uHash % p->nBins;
852 }
Dss_ObjHashLookup(Dss_Man_t * p,int Type,Vec_Int_t * vFaninLits,word * pTruth)853 unsigned * Dss_ObjHashLookup( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits, word * pTruth )
854 {
855 Dss_Obj_t * pObj;
856 unsigned * pSpot = p->pBins + Dss_ObjHashKey(p, Type, vFaninLits, pTruth);
857 for ( ; *pSpot; pSpot = (unsigned *)Vec_IntEntryP(p->vNexts, pObj->Id) )
858 {
859 pObj = Dss_VecObj( p->vObjs, *pSpot );
860 if ( (int)pObj->Type == Type &&
861 (int)pObj->nFans == Vec_IntSize(vFaninLits) &&
862 !memcmp(pObj->pFans, Vec_IntArray(vFaninLits), sizeof(int)*pObj->nFans) &&
863 (pTruth == NULL || !memcmp(Dss_ObjTruth(pObj), pTruth, (size_t)Abc_TtByteNum(pObj->nFans))) ) // equal
864 return pSpot;
865 }
866 return pSpot;
867 }
Dss_ObjFindOrAdd(Dss_Man_t * p,int Type,Vec_Int_t * vFaninLits,word * pTruth)868 Dss_Obj_t * Dss_ObjFindOrAdd( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits, word * pTruth )
869 {
870 Dss_Obj_t * pObj;
871 unsigned * pSpot = Dss_ObjHashLookup( p, Type, vFaninLits, pTruth );
872 if ( *pSpot )
873 return Dss_VecObj( p->vObjs, *pSpot );
874 *pSpot = Vec_PtrSize( p->vObjs );
875 pObj = Dss_ObjCreate( p, Type, vFaninLits, pTruth );
876 return pObj;
877 }
878
879 /**Function*************************************************************
880
881 Synopsis [Cache for decomposition calls.]
882
883 Description []
884
885 SideEffects []
886
887 SeeAlso []
888
889 ***********************************************************************/
Dss_ManCacheAlloc(Dss_Man_t * p)890 void Dss_ManCacheAlloc( Dss_Man_t * p )
891 {
892 assert( p->nCache == 0 );
893 p->nCache = Abc_PrimeCudd( 100000 );
894 p->pCache = ABC_CALLOC( Dss_Ent_t *, p->nCache );
895 }
Dss_ManCacheFree(Dss_Man_t * p)896 void Dss_ManCacheFree( Dss_Man_t * p )
897 {
898 if ( p->pCache == NULL )
899 return;
900 assert( p->nCache != 0 );
901 p->nCache = 0;
902 ABC_FREE( p->pCache );
903 }
Dss_ManCacheHashKey(Dss_Man_t * p,Dss_Ent_t * pEnt)904 static inline unsigned Dss_ManCacheHashKey( Dss_Man_t * p, Dss_Ent_t * pEnt )
905 {
906 static int s_Primes[8] = { 1699, 4177, 5147, 5647, 6343, 7103, 7873, 8147 };
907 int i;
908 unsigned uHash = pEnt->nShared * 7103 + pEnt->iDsd0 * 7873 + pEnt->iDsd1 * 8147;
909 for ( i = 0; i < 2*(int)pEnt->nShared; i++ )
910 uHash += pEnt->pShared[i] * s_Primes[i & 0x7];
911 return uHash % p->nCache;
912 }
Dss_ManCacheProfile(Dss_Man_t * p)913 void Dss_ManCacheProfile( Dss_Man_t * p )
914 {
915 Dss_Ent_t ** pSpot;
916 int i, Counter;
917 for ( i = 0; i < p->nCache; i++ )
918 {
919 Counter = 0;
920 for ( pSpot = p->pCache + i; *pSpot; pSpot = &(*pSpot)->pNext, Counter++ )
921 ;
922 if ( Counter )
923 printf( "%d ", Counter );
924 }
925 printf( "\n" );
926 }
Dss_ManCacheLookup(Dss_Man_t * p,Dss_Ent_t * pEnt)927 Dss_Ent_t ** Dss_ManCacheLookup( Dss_Man_t * p, Dss_Ent_t * pEnt )
928 {
929 Dss_Ent_t ** pSpot = p->pCache + Dss_ManCacheHashKey( p, pEnt );
930 for ( ; *pSpot; pSpot = &(*pSpot)->pNext )
931 {
932 if ( (*pSpot)->iDsd0 == pEnt->iDsd0 &&
933 (*pSpot)->iDsd1 == pEnt->iDsd1 &&
934 (*pSpot)->nShared == pEnt->nShared &&
935 !memcmp((*pSpot)->pShared, pEnt->pShared, sizeof(char)*2*pEnt->nShared) ) // equal
936 {
937 p->nCacheHits[pEnt->nShared!=0]++;
938 return pSpot;
939 }
940 }
941 p->nCacheMisses[pEnt->nShared!=0]++;
942 return pSpot;
943 }
Dss_ManCacheCreate(Dss_Man_t * p,Dss_Ent_t * pEnt0,Dss_Fun_t * pFun0)944 Dss_Ent_t * Dss_ManCacheCreate( Dss_Man_t * p, Dss_Ent_t * pEnt0, Dss_Fun_t * pFun0 )
945 {
946 Dss_Ent_t * pEnt = (Dss_Ent_t *)Mem_FlexEntryFetch( p->pMemEnts, sizeof(word) * pEnt0->nWords );
947 Dss_Fun_t * pFun = (Dss_Fun_t *)Mem_FlexEntryFetch( p->pMemEnts, sizeof(word) * Dss_FunWordNum(pFun0) );
948 memcpy( pEnt, pEnt0, sizeof(word) * pEnt0->nWords );
949 memcpy( pFun, pFun0, sizeof(word) * Dss_FunWordNum(pFun0) );
950 pEnt->pFunc = pFun;
951 pEnt->pNext = NULL;
952 p->nCacheEntries[pEnt->nShared!=0]++;
953 return pEnt;
954 }
955
956 /**Function*************************************************************
957
958 Synopsis []
959
960 Description []
961
962 SideEffects []
963
964 SeeAlso []
965
966 ***********************************************************************/
Dss_ManAlloc(int nVars,int nNonDecLimit)967 Dss_Man_t * Dss_ManAlloc( int nVars, int nNonDecLimit )
968 {
969 Dss_Man_t * p;
970 p = ABC_CALLOC( Dss_Man_t, 1 );
971 p->nVars = nVars;
972 p->nNonDecLimit = nNonDecLimit;
973 p->nBins = Abc_PrimeCudd( 1000000 );
974 p->pBins = ABC_CALLOC( unsigned, p->nBins );
975 p->pMem = Mem_FlexStart();
976 p->vObjs = Vec_PtrAlloc( 10000 );
977 p->vNexts = Vec_IntAlloc( 10000 );
978 Dss_ObjAlloc( p, DAU_DSD_CONST0, 0, 0 );
979 Dss_ObjAlloc( p, DAU_DSD_VAR, 0, 0 )->nSupp = 1;
980 p->vLeaves = Vec_IntAlloc( 32 );
981 p->vCopies = Vec_IntAlloc( 32 );
982 p->pTtElems = Dss_ManTtElems();
983 p->pMemEnts = Mem_FlexStart();
984 // Dss_ManCacheAlloc( p );
985 return p;
986 }
Dss_ManFree(Dss_Man_t * p)987 void Dss_ManFree( Dss_Man_t * p )
988 {
989 Abc_PrintTime( 1, "Time begin ", p->timeBeg );
990 Abc_PrintTime( 1, "Time decomp", p->timeDec );
991 Abc_PrintTime( 1, "Time lookup", p->timeLook );
992 Abc_PrintTime( 1, "Time end ", p->timeEnd );
993
994 // Dss_ManCacheProfile( p );
995 Dss_ManCacheFree( p );
996 Mem_FlexStop( p->pMemEnts, 0 );
997 Vec_IntFreeP( &p->vCopies );
998 Vec_IntFreeP( &p->vLeaves );
999 Vec_IntFreeP( &p->vNexts );
1000 Vec_PtrFreeP( &p->vObjs );
1001 Mem_FlexStop( p->pMem, 0 );
1002 ABC_FREE( p->pBins );
1003 ABC_FREE( p );
1004 }
Dss_ManPrint_rec(FILE * pFile,Dss_Man_t * p,Dss_Obj_t * pObj,int * pPermLits,int * pnSupp)1005 void Dss_ManPrint_rec( FILE * pFile, Dss_Man_t * p, Dss_Obj_t * pObj, int * pPermLits, int * pnSupp )
1006 {
1007 char OpenType[7] = {0, 0, 0, '(', '[', '<', '{'};
1008 char CloseType[7] = {0, 0, 0, ')', ']', '>', '}'};
1009 Dss_Obj_t * pFanin;
1010 int i;
1011 assert( !Dss_IsComplement(pObj) );
1012 if ( pObj->Type == DAU_DSD_CONST0 )
1013 { fprintf( pFile, "0" ); return; }
1014 if ( pObj->Type == DAU_DSD_VAR )
1015 {
1016 int iPermLit = pPermLits ? pPermLits[(*pnSupp)++] : Abc_Var2Lit((*pnSupp)++, 0);
1017 fprintf( pFile, "%s%c", Abc_LitIsCompl(iPermLit)? "!":"", 'a' + Abc_Lit2Var(iPermLit) );
1018 return;
1019 }
1020 if ( pObj->Type == DAU_DSD_PRIME )
1021 Abc_TtPrintHexRev( pFile, Dss_ObjTruth(pObj), pObj->nFans );
1022 fprintf( pFile, "%c", OpenType[pObj->Type] );
1023 Dss_ObjForEachFanin( p->vObjs, pObj, pFanin, i )
1024 {
1025 fprintf( pFile, "%s", Dss_ObjFaninC(pObj, i) ? "!":"" );
1026 Dss_ManPrint_rec( pFile, p, pFanin, pPermLits, pnSupp );
1027 }
1028 fprintf( pFile, "%c", CloseType[pObj->Type] );
1029 }
Dss_ManPrintOne(FILE * pFile,Dss_Man_t * p,int iDsdLit,int * pPermLits)1030 void Dss_ManPrintOne( FILE * pFile, Dss_Man_t * p, int iDsdLit, int * pPermLits )
1031 {
1032 int nSupp = 0;
1033 fprintf( pFile, "%6d : ", Abc_Lit2Var(iDsdLit) );
1034 fprintf( pFile, "%2d ", Dss_VecLitSuppSize(p->vObjs, iDsdLit) );
1035 fprintf( pFile, "%s", Abc_LitIsCompl(iDsdLit) ? "!" : "" );
1036 Dss_ManPrint_rec( pFile, p, Dss_VecObj(p->vObjs, Abc_Lit2Var(iDsdLit)), pPermLits, &nSupp );
1037 fprintf( pFile, "\n" );
1038 assert( nSupp == (int)Dss_VecObj(p->vObjs, Abc_Lit2Var(iDsdLit))->nSupp );
1039 }
Dss_ManCheckNonDec_rec(Dss_Man_t * p,Dss_Obj_t * pObj)1040 int Dss_ManCheckNonDec_rec( Dss_Man_t * p, Dss_Obj_t * pObj )
1041 {
1042 Dss_Obj_t * pFanin;
1043 int i;
1044 assert( !Dss_IsComplement(pObj) );
1045 if ( pObj->Type == DAU_DSD_CONST0 )
1046 return 0;
1047 if ( pObj->Type == DAU_DSD_VAR )
1048 return 0;
1049 if ( pObj->Type == DAU_DSD_PRIME )
1050 return 1;
1051 Dss_ObjForEachFanin( p->vObjs, pObj, pFanin, i )
1052 if ( Dss_ManCheckNonDec_rec( p, pFanin ) )
1053 return 1;
1054 return 0;
1055 }
Dss_ManDump(Dss_Man_t * p)1056 void Dss_ManDump( Dss_Man_t * p )
1057 {
1058 char * pFileName = "dss_tts.txt";
1059 FILE * pFile;
1060 word Temp[DAU_MAX_WORD];
1061 Dss_Obj_t * pObj;
1062 int i;
1063 pFile = fopen( pFileName, "wb" );
1064 if ( pFile == NULL )
1065 {
1066 printf( "Cannot open file \"%s\".\n", pFileName );
1067 return;
1068 }
1069 Dss_VecForEachObj( p->vObjs, pObj, i )
1070 {
1071 if ( pObj->Type != DAU_DSD_PRIME )
1072 continue;
1073 Abc_TtCopy( Temp, Dss_ObjTruth(pObj), Abc_TtWordNum(pObj->nFans), 0 );
1074 Abc_TtStretch6( Temp, pObj->nFans, p->nVars );
1075 fprintf( pFile, "0x" );
1076 Abc_TtPrintHexRev( pFile, Temp, p->nVars );
1077 fprintf( pFile, "\n" );
1078
1079 // printf( "%6d : ", i );
1080 // Abc_TtPrintHexRev( stdout, Temp, p->nVars );
1081 // printf( " " );
1082 // Dau_DsdPrintFromTruth( stdout, Temp, p->nVars );
1083 }
1084 fclose( pFile );
1085 }
Dss_ManPrint(char * pFileName,Dss_Man_t * p)1086 void Dss_ManPrint( char * pFileName, Dss_Man_t * p )
1087 {
1088 Dss_Obj_t * pObj;
1089 int CountNonDsd = 0, CountNonDsdStr = 0;
1090 int i, clk = Abc_Clock();
1091 FILE * pFile;
1092 pFile = pFileName ? fopen( pFileName, "wb" ) : stdout;
1093 if ( pFileName && pFile == NULL )
1094 {
1095 printf( "cannot open output file\n" );
1096 return;
1097 }
1098 Dss_VecForEachObj( p->vObjs, pObj, i )
1099 {
1100 CountNonDsd += (pObj->Type == DAU_DSD_PRIME);
1101 CountNonDsdStr += Dss_ManCheckNonDec_rec( p, pObj );
1102 }
1103 fprintf( pFile, "Total number of objects = %8d\n", Vec_PtrSize(p->vObjs) );
1104 fprintf( pFile, "Non-DSD objects (max =%2d) = %8d\n", p->nNonDecLimit, CountNonDsd );
1105 fprintf( pFile, "Non-DSD structures = %8d\n", CountNonDsdStr );
1106 fprintf( pFile, "Memory used for objects = %6.2f MB.\n", 1.0*Mem_FlexReadMemUsage(p->pMem)/(1<<20) );
1107 fprintf( pFile, "Memory used for array = %6.2f MB.\n", 1.0*sizeof(void *)*Vec_PtrCap(p->vObjs)/(1<<20) );
1108 fprintf( pFile, "Memory used for hash table = %6.2f MB.\n", 1.0*sizeof(int)*p->nBins/(1<<20) );
1109 fprintf( pFile, "Memory used for cache = %6.2f MB.\n", 1.0*Mem_FlexReadMemUsage(p->pMemEnts)/(1<<20) );
1110 fprintf( pFile, "Cache hits = %8d %8d\n", p->nCacheHits[0], p->nCacheHits[1] );
1111 fprintf( pFile, "Cache misses = %8d %8d\n", p->nCacheMisses[0], p->nCacheMisses[1] );
1112 fprintf( pFile, "Cache entries = %8d %8d\n", p->nCacheEntries[0], p->nCacheEntries[1] );
1113 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1114 // Dss_ManHashProfile( p );
1115 // Dss_ManDump( p );
1116 // return;
1117 Dss_VecForEachObj( p->vObjs, pObj, i )
1118 {
1119 if ( i == 50 )
1120 break;
1121 Dss_ManPrintOne( pFile, p, Dss_Obj2Lit(pObj), NULL );
1122 }
1123 fprintf( pFile, "\n" );
1124 if ( pFileName )
1125 fclose( pFile );
1126 }
1127
1128 /**Function*************************************************************
1129
1130 Synopsis []
1131
1132 Description []
1133
1134 SideEffects []
1135
1136 SeeAlso []
1137
1138 ***********************************************************************/
Dss_ManComputeTruth_rec(Dss_Man_t * p,Dss_Obj_t * pObj,int nVars,word * pRes,int * pPermLits,int * pnSupp)1139 void Dss_ManComputeTruth_rec( Dss_Man_t * p, Dss_Obj_t * pObj, int nVars, word * pRes, int * pPermLits, int * pnSupp )
1140 {
1141 Dss_Obj_t * pChild;
1142 int nWords = Abc_TtWordNum(nVars);
1143 int i, fCompl = Dss_IsComplement(pObj);
1144 pObj = Dss_Regular(pObj);
1145 if ( pObj->Type == DAU_DSD_VAR )
1146 {
1147 int iPermLit = pPermLits[(*pnSupp)++];
1148 assert( (*pnSupp) <= nVars );
1149 Abc_TtCopy( pRes, p->pTtElems[Abc_Lit2Var(iPermLit)], nWords, fCompl ^ Abc_LitIsCompl(iPermLit) );
1150 return;
1151 }
1152 if ( pObj->Type == DAU_DSD_AND || pObj->Type == DAU_DSD_XOR )
1153 {
1154 word pTtTemp[DAU_MAX_WORD];
1155 if ( pObj->Type == DAU_DSD_AND )
1156 Abc_TtConst1( pRes, nWords );
1157 else
1158 Abc_TtConst0( pRes, nWords );
1159 Dss_ObjForEachChild( p->vObjs, pObj, pChild, i )
1160 {
1161 Dss_ManComputeTruth_rec( p, pChild, nVars, pTtTemp, pPermLits, pnSupp );
1162 if ( pObj->Type == DAU_DSD_AND )
1163 Abc_TtAnd( pRes, pRes, pTtTemp, nWords, 0 );
1164 else
1165 Abc_TtXor( pRes, pRes, pTtTemp, nWords, 0 );
1166 }
1167 if ( fCompl ) Abc_TtNot( pRes, nWords );
1168 return;
1169 }
1170 if ( pObj->Type == DAU_DSD_MUX ) // mux
1171 {
1172 word pTtTemp[3][DAU_MAX_WORD];
1173 Dss_ObjForEachChild( p->vObjs, pObj, pChild, i )
1174 Dss_ManComputeTruth_rec( p, pChild, nVars, pTtTemp[i], pPermLits, pnSupp );
1175 assert( i == 3 );
1176 Abc_TtMux( pRes, pTtTemp[0], pTtTemp[1], pTtTemp[2], nWords );
1177 if ( fCompl ) Abc_TtNot( pRes, nWords );
1178 return;
1179 }
1180 if ( pObj->Type == DAU_DSD_PRIME ) // function
1181 {
1182 word pFanins[DAU_MAX_VAR][DAU_MAX_WORD];
1183 Dss_ObjForEachChild( p->vObjs, pObj, pChild, i )
1184 Dss_ManComputeTruth_rec( p, pChild, nVars, pFanins[i], pPermLits, pnSupp );
1185 Dau_DsdTruthCompose_rec( Dss_ObjTruth(pObj), pFanins, pRes, pObj->nFans, nWords );
1186 if ( fCompl ) Abc_TtNot( pRes, nWords );
1187 return;
1188 }
1189 assert( 0 );
1190
1191 }
Dss_ManComputeTruth(Dss_Man_t * p,int iDsd,int nVars,int * pPermLits)1192 word * Dss_ManComputeTruth( Dss_Man_t * p, int iDsd, int nVars, int * pPermLits )
1193 {
1194 Dss_Obj_t * pObj = Dss_Lit2Obj(p->vObjs, iDsd);
1195 word * pRes = p->pTtElems[DAU_MAX_VAR];
1196 int nWords = Abc_TtWordNum( nVars );
1197 int nSupp = 0;
1198 assert( nVars <= DAU_MAX_VAR );
1199 if ( iDsd == 0 )
1200 Abc_TtConst0( pRes, nWords );
1201 else if ( iDsd == 1 )
1202 Abc_TtConst1( pRes, nWords );
1203 else if ( Dss_Regular(pObj)->Type == DAU_DSD_VAR )
1204 {
1205 int iPermLit = pPermLits[nSupp++];
1206 Abc_TtCopy( pRes, p->pTtElems[Abc_Lit2Var(iPermLit)], nWords, Abc_LitIsCompl(iDsd) ^ Abc_LitIsCompl(iPermLit) );
1207 }
1208 else
1209 Dss_ManComputeTruth_rec( p, pObj, nVars, pRes, pPermLits, &nSupp );
1210 assert( nSupp == (int)Dss_Regular(pObj)->nSupp );
1211 return pRes;
1212 }
1213
1214
1215 /**Function*************************************************************
1216
1217 Synopsis []
1218
1219 Description []
1220
1221 SideEffects []
1222
1223 SeeAlso []
1224
1225 ***********************************************************************/
1226 // returns literal of non-shifted tree in p, corresponding to pObj in pNtk, which may be compl
Dss_NtkRebuild_rec(Dss_Man_t * p,Dss_Ntk_t * pNtk,Dss_Obj_t * pObj)1227 int Dss_NtkRebuild_rec( Dss_Man_t * p, Dss_Ntk_t * pNtk, Dss_Obj_t * pObj )
1228 {
1229 Dss_Obj_t * pChildren[DAU_MAX_VAR];
1230 Dss_Obj_t * pChild, * pObjNew;
1231 int i, k, fCompl = Dss_IsComplement(pObj);
1232 pObj = Dss_Regular(pObj);
1233 if ( pObj->Type == DAU_DSD_VAR )
1234 return Abc_Var2Lit( 1, fCompl );
1235 Dss_ObjForEachChild( pNtk->vObjs, pObj, pChild, k )
1236 {
1237 pChildren[k] = Dss_Lit2Obj( p->vObjs, Dss_NtkRebuild_rec( p, pNtk, pChild ) );
1238 if ( pObj->Type == DAU_DSD_XOR && Dss_IsComplement(pChildren[k]) )
1239 pChildren[k] = Dss_Not(pChildren[k]), fCompl ^= 1;
1240 }
1241 // normalize MUX
1242 if ( pObj->Type == DAU_DSD_MUX )
1243 {
1244 if ( Dss_IsComplement(pChildren[0]) )
1245 {
1246 pChildren[0] = Dss_Not(pChildren[0]);
1247 ABC_SWAP( Dss_Obj_t *, pChildren[1], pChildren[2] );
1248 }
1249 if ( Dss_IsComplement(pChildren[1]) )
1250 {
1251 pChildren[1] = Dss_Not(pChildren[1]);
1252 pChildren[2] = Dss_Not(pChildren[2]);
1253 fCompl ^= 1;
1254 }
1255 }
1256 // shift subgraphs
1257 Vec_IntClear( p->vLeaves );
1258 for ( i = 0; i < k; i++ )
1259 Vec_IntPush( p->vLeaves, Dss_Obj2Lit(pChildren[i]) );
1260 // create new graph
1261 pObjNew = Dss_ObjFindOrAdd( p, pObj->Type, p->vLeaves, pObj->Type == DAU_DSD_PRIME ? Dss_ObjTruth(pObj) : NULL );
1262 return Abc_Var2Lit( pObjNew->Id, fCompl );
1263 }
Dss_NtkRebuild(Dss_Man_t * p,Dss_Ntk_t * pNtk)1264 int Dss_NtkRebuild( Dss_Man_t * p, Dss_Ntk_t * pNtk )
1265 {
1266 assert( p->nVars == pNtk->nVars );
1267 if ( Dss_Regular(pNtk->pRoot)->Type == DAU_DSD_CONST0 )
1268 return Dss_IsComplement(pNtk->pRoot);
1269 if ( Dss_Regular(pNtk->pRoot)->Type == DAU_DSD_VAR )
1270 return Abc_Var2Lit( Dss_Regular(pNtk->pRoot)->iVar + 1, Dss_IsComplement(pNtk->pRoot) );
1271 return Dss_NtkRebuild_rec( p, pNtk, pNtk->pRoot );
1272 }
1273
1274 /**Function*************************************************************
1275
1276 Synopsis [Performs DSD operation on the two literals.]
1277
1278 Description [Returns the perm of the resulting literals. The perm size
1279 is equal to the number of support variables. The perm variables are 0-based
1280 numbers of pLits[0] followed by nLits[0]-based numbers of pLits[1].]
1281
1282 SideEffects []
1283
1284 SeeAlso []
1285
1286 ***********************************************************************/
Dss_ManOperation(Dss_Man_t * p,int Type,int * pLits,int nLits,unsigned char * pPerm,word * pTruth)1287 int Dss_ManOperation( Dss_Man_t * p, int Type, int * pLits, int nLits, unsigned char * pPerm, word * pTruth )
1288 {
1289 Dss_Obj_t * pChildren[DAU_MAX_VAR];
1290 Dss_Obj_t * pObj, * pChild;
1291 int i, k, nChildren = 0, fCompl = 0, fComplFan;
1292
1293 assert( Type == DAU_DSD_AND || pPerm == NULL );
1294 if ( Type == DAU_DSD_AND && pPerm != NULL )
1295 {
1296 int pBegEnd[DAU_MAX_VAR];
1297 int j, nSSize = 0;
1298 for ( k = 0; k < nLits; k++ )
1299 {
1300 pObj = Dss_Lit2Obj(p->vObjs, pLits[k]);
1301 if ( Dss_IsComplement(pObj) || pObj->Type != DAU_DSD_AND )
1302 {
1303 fComplFan = (Dss_Regular(pObj)->Type == DAU_DSD_VAR && Dss_IsComplement(pObj));
1304 if ( fComplFan )
1305 pObj = Dss_Regular(pObj);
1306 pBegEnd[nChildren] = (nSSize << 16) | (fComplFan << 8) | (nSSize + Dss_Regular(pObj)->nSupp);
1307 nSSize += Dss_Regular(pObj)->nSupp;
1308 pChildren[nChildren++] = pObj;
1309 }
1310 else
1311 Dss_ObjForEachChild( p->vObjs, pObj, pChild, i )
1312 {
1313 fComplFan = (Dss_Regular(pChild)->Type == DAU_DSD_VAR && Dss_IsComplement(pChild));
1314 if ( fComplFan )
1315 pChild = Dss_Regular(pChild);
1316 pBegEnd[nChildren] = (nSSize << 16) | (fComplFan << 8) | (nSSize + Dss_Regular(pChild)->nSupp);
1317 nSSize += Dss_Regular(pChild)->nSupp;
1318 pChildren[nChildren++] = pChild;
1319 }
1320 }
1321 Dss_ObjSort( p->vObjs, pChildren, nChildren, pBegEnd );
1322 // create permutation
1323 for ( j = i = 0; i < nChildren; i++ )
1324 for ( k = (pBegEnd[i] >> 16); k < (pBegEnd[i] & 0xFF); k++ )
1325 pPerm[j++] = (unsigned char)Abc_Var2Lit( k, (pBegEnd[i] >> 8) & 1 );
1326 assert( j == nSSize );
1327 }
1328 else if ( Type == DAU_DSD_AND )
1329 {
1330 for ( k = 0; k < nLits; k++ )
1331 {
1332 pObj = Dss_Lit2Obj(p->vObjs, pLits[k]);
1333 if ( Dss_IsComplement(pObj) || pObj->Type != DAU_DSD_AND )
1334 pChildren[nChildren++] = pObj;
1335 else
1336 Dss_ObjForEachChild( p->vObjs, pObj, pChild, i )
1337 pChildren[nChildren++] = pChild;
1338 }
1339 Dss_ObjSort( p->vObjs, pChildren, nChildren, NULL );
1340 }
1341 else if ( Type == DAU_DSD_XOR )
1342 {
1343 for ( k = 0; k < nLits; k++ )
1344 {
1345 fCompl ^= Abc_LitIsCompl(pLits[k]);
1346 pObj = Dss_Lit2Obj(p->vObjs, Abc_LitRegular(pLits[k]));
1347 if ( pObj->Type != DAU_DSD_XOR )
1348 pChildren[nChildren++] = pObj;
1349 else
1350 Dss_ObjForEachChild( p->vObjs, pObj, pChild, i )
1351 {
1352 assert( !Dss_IsComplement(pChild) );
1353 pChildren[nChildren++] = pChild;
1354 }
1355 }
1356 Dss_ObjSort( p->vObjs, pChildren, nChildren, NULL );
1357 }
1358 else if ( Type == DAU_DSD_MUX )
1359 {
1360 if ( Abc_LitIsCompl(pLits[0]) )
1361 {
1362 pLits[0] = Abc_LitNot(pLits[0]);
1363 ABC_SWAP( int, pLits[1], pLits[2] );
1364 }
1365 if ( Abc_LitIsCompl(pLits[1]) )
1366 {
1367 pLits[1] = Abc_LitNot(pLits[1]);
1368 pLits[2] = Abc_LitNot(pLits[2]);
1369 fCompl ^= 1;
1370 }
1371 for ( k = 0; k < nLits; k++ )
1372 pChildren[nChildren++] = Dss_Lit2Obj(p->vObjs, pLits[k]);
1373 }
1374 else if ( Type == DAU_DSD_PRIME )
1375 {
1376 for ( k = 0; k < nLits; k++ )
1377 pChildren[nChildren++] = Dss_Lit2Obj(p->vObjs, pLits[k]);
1378 }
1379 else assert( 0 );
1380
1381 // shift subgraphs
1382 Vec_IntClear( p->vLeaves );
1383 for ( i = 0; i < nChildren; i++ )
1384 Vec_IntPush( p->vLeaves, Dss_Obj2Lit(pChildren[i]) );
1385 // create new graph
1386 pObj = Dss_ObjFindOrAdd( p, Type, p->vLeaves, pTruth );
1387 return Abc_Var2Lit( pObj->Id, fCompl );
1388 }
Dss_ManOperationFun(Dss_Man_t * p,int * iDsd,int nFansTot)1389 Dss_Fun_t * Dss_ManOperationFun( Dss_Man_t * p, int * iDsd, int nFansTot )
1390 {
1391 static char Buffer[100];
1392 Dss_Fun_t * pFun = (Dss_Fun_t *)Buffer;
1393 pFun->iDsd = Dss_ManOperation( p, DAU_DSD_AND, iDsd, 2, pFun->pFans, NULL );
1394 //printf( "%d %d -> %d ", iDsd[0], iDsd[1], pFun->iDsd );
1395 pFun->nFans = nFansTot;
1396 assert( (int)pFun->nFans == Dss_VecLitSuppSize(p->vObjs, pFun->iDsd) );
1397 return pFun;
1398 }
1399
1400 /**Function*************************************************************
1401
1402 Synopsis []
1403
1404 Description []
1405
1406 SideEffects []
1407
1408 SeeAlso []
1409
1410 ***********************************************************************/
Dss_EntPrint(Dss_Ent_t * p,Dss_Fun_t * pFun)1411 void Dss_EntPrint( Dss_Ent_t * p, Dss_Fun_t * pFun )
1412 {
1413 int i;
1414 printf( "%d %d ", p->iDsd0, p->iDsd1 );
1415 for ( i = 0; i < (int)p->nShared; i++ )
1416 printf( "%d=%d ", p->pShared[2*i], p->pShared[2*i+1] );
1417 printf( "-> %d ", pFun->iDsd );
1418 }
1419
1420 /**Function*************************************************************
1421
1422 Synopsis [Performs AND on two DSD functions with support overlap.]
1423
1424 Description [Returns the perm of the resulting literals. The perm size
1425 is equal to the number of support variables. The perm variables are 0-based
1426 numbers of pLits[0] followed by nLits[0]-based numbers of pLits[1].]
1427
1428 SideEffects []
1429
1430 SeeAlso []
1431
1432 ***********************************************************************/
Dss_ManBooleanAnd(Dss_Man_t * p,Dss_Ent_t * pEnt,int Counter)1433 Dss_Fun_t * Dss_ManBooleanAnd( Dss_Man_t * p, Dss_Ent_t * pEnt, int Counter )
1434 {
1435 static char Buffer[100];
1436 Dss_Fun_t * pFun = (Dss_Fun_t *)Buffer;
1437 Dss_Ntk_t * pNtk;
1438 word * pTruthOne, pTruth[DAU_MAX_WORD];
1439 char pDsd[DAU_MAX_STR];
1440 int pMapDsd2Truth[DAU_MAX_VAR];
1441 int pPermLits[DAU_MAX_VAR];
1442 int pPermDsd[DAU_MAX_VAR];
1443 int i, nNonDec, nSuppSize = 0;
1444 int nFans[2];
1445 nFans[0] = Dss_VecLitSuppSize( p->vObjs, pEnt->iDsd0 );
1446 nFans[1] = Dss_VecLitSuppSize( p->vObjs, pEnt->iDsd1 );
1447 // create first truth table
1448 for ( i = 0; i < nFans[0]; i++ )
1449 {
1450 pMapDsd2Truth[nSuppSize] = i;
1451 pPermLits[i] = Abc_Var2Lit( nSuppSize++, 0 );
1452 }
1453 pTruthOne = Dss_ManComputeTruth( p, pEnt->iDsd0, p->nVars, pPermLits );
1454 Abc_TtCopy( pTruth, pTruthOne, Abc_TtWordNum(p->nVars), 0 );
1455 if ( Counter )
1456 {
1457 //Kit_DsdPrintFromTruth( pTruthOne, p->nVars ); printf( "\n" );
1458 }
1459 // create second truth table
1460 for ( i = 0; i < nFans[1]; i++ )
1461 pPermLits[i] = -1;
1462 for ( i = 0; i < (int)pEnt->nShared; i++ )
1463 pPermLits[pEnt->pShared[2*i+0]] = pEnt->pShared[2*i+1];
1464 for ( i = 0; i < nFans[1]; i++ )
1465 if ( pPermLits[i] == -1 )
1466 {
1467 pMapDsd2Truth[nSuppSize] = nFans[0] + i;
1468 pPermLits[i] = Abc_Var2Lit( nSuppSize++, 0 );
1469 }
1470 pTruthOne = Dss_ManComputeTruth( p, pEnt->iDsd1, p->nVars, pPermLits );
1471 if ( Counter )
1472 {
1473 //Kit_DsdPrintFromTruth( pTruthOne, p->nVars ); printf( "\n" );
1474 }
1475 Abc_TtAnd( pTruth, pTruth, pTruthOne, Abc_TtWordNum(p->nVars), 0 );
1476 // perform decomposition
1477 nNonDec = Dau_DsdDecompose( pTruth, nSuppSize, 0, 0, pDsd );
1478 if ( p->nNonDecLimit && nNonDec > p->nNonDecLimit )
1479 return NULL;
1480 // derive network and convert it into the manager
1481 pNtk = Dss_NtkCreate( pDsd, p->nVars, nNonDec ? pTruth : NULL );
1482 //Dss_NtkPrint( pNtk );
1483 Dss_NtkCheck( pNtk );
1484 Dss_NtkTransform( pNtk, pPermDsd );
1485 //Dss_NtkPrint( pNtk );
1486 pFun->iDsd = Dss_NtkRebuild( p, pNtk );
1487 Dss_NtkFree( pNtk );
1488 // pPermDsd maps vars of iDsdRes into literals of pTruth
1489 // translate this map into the one that maps vars of iDsdRes into literals of cut
1490 pFun->nFans = Dss_VecLitSuppSize( p->vObjs, pFun->iDsd );
1491 for ( i = 0; i < (int)pFun->nFans; i++ )
1492 pFun->pFans[i] = (unsigned char)Abc_Lit2LitV( pMapDsd2Truth, pPermDsd[i] );
1493
1494 // Dss_EntPrint( pEnt, pFun );
1495 return pFun;
1496 }
1497
1498 /**Function*************************************************************
1499
1500 Synopsis []
1501
1502 Description []
1503
1504 SideEffects []
1505
1506 SeeAlso []
1507
1508 ***********************************************************************/
1509 // returns mapping of variables of dsd1 into literals of dsd0
Dss_ManSharedMap(Dss_Man_t * p,int * iDsd,int * nFans,int ** pFans,unsigned uSharedMask)1510 Dss_Ent_t * Dss_ManSharedMap( Dss_Man_t * p, int * iDsd, int * nFans, int ** pFans, unsigned uSharedMask )
1511 {
1512 static char Buffer[100];
1513 Dss_Ent_t * pEnt = (Dss_Ent_t *)Buffer;
1514 pEnt->iDsd0 = iDsd[0];
1515 pEnt->iDsd1 = iDsd[1];
1516 pEnt->nShared = 0;
1517 if ( uSharedMask )
1518 {
1519 int i, g, pMapGtoL[DAU_MAX_VAR] = {-1};
1520 for ( i = 0; i < nFans[0]; i++ )
1521 pMapGtoL[ Abc_Lit2Var(pFans[0][i]) ] = Abc_Var2Lit( i, Abc_LitIsCompl(pFans[0][i]) );
1522 for ( i = 0; i < nFans[1]; i++ )
1523 {
1524 g = Abc_Lit2Var( pFans[1][i] );
1525 if ( (uSharedMask >> g) & 1 )
1526 {
1527 assert( pMapGtoL[g] >= 0 );
1528 pEnt->pShared[2*pEnt->nShared+0] = (unsigned char)i;
1529 pEnt->pShared[2*pEnt->nShared+1] = (unsigned char)Abc_LitNotCond( pMapGtoL[g], Abc_LitIsCompl(pFans[1][i]) );
1530 pEnt->nShared++;
1531 }
1532 }
1533 }
1534 pEnt->nWords = Dss_EntWordNum( pEnt );
1535 return pEnt;
1536 }
1537
1538 // merge two DSD functions
Dss_ManMerge(Dss_Man_t * p,int * iDsd,int * nFans,int ** pFans,unsigned uSharedMask,int nKLutSize,unsigned char * pPermRes,word * pTruth)1539 int Dss_ManMerge( Dss_Man_t * p, int * iDsd, int * nFans, int ** pFans, unsigned uSharedMask, int nKLutSize, unsigned char * pPermRes, word * pTruth )
1540 {
1541 int fVerbose = 0;
1542 int fCheck = 0;
1543 static int Counter = 0;
1544 // word pTtTemp[DAU_MAX_WORD];
1545 word * pTruthOne;
1546 int pPermResInt[DAU_MAX_VAR];
1547 Dss_Ent_t * pEnt, ** ppSpot;
1548 Dss_Fun_t * pFun;
1549 int i;
1550 abctime clk;
1551 Counter++;
1552 if ( DAU_MAX_VAR < nKLutSize )
1553 {
1554 printf( "Paramater DAU_MAX_VAR (%d) smaller than LUT size (%d).\n", DAU_MAX_VAR, nKLutSize );
1555 return -1;
1556 }
1557 assert( iDsd[0] <= iDsd[1] );
1558
1559 if ( fVerbose )
1560 {
1561 Dss_ManPrintOne( stdout, p, iDsd[0], pFans[0] );
1562 Dss_ManPrintOne( stdout, p, iDsd[1], pFans[1] );
1563 }
1564
1565 // constant argument
1566 if ( iDsd[0] == 0 ) return 0;
1567 if ( iDsd[0] == 1 ) return iDsd[1];
1568 if ( iDsd[1] == 0 ) return 0;
1569 if ( iDsd[1] == 1 ) return iDsd[0];
1570
1571 // no overlap
1572 clk = Abc_Clock();
1573 assert( nFans[0] == Dss_VecLitSuppSize(p->vObjs, iDsd[0]) );
1574 assert( nFans[1] == Dss_VecLitSuppSize(p->vObjs, iDsd[1]) );
1575 assert( nFans[0] + nFans[1] <= nKLutSize + Dss_WordCountOnes(uSharedMask) );
1576 // create map of shared variables
1577 pEnt = Dss_ManSharedMap( p, iDsd, nFans, pFans, uSharedMask );
1578 p->timeBeg += Abc_Clock() - clk;
1579 // check cache
1580 if ( p->pCache == NULL )
1581 {
1582 clk = Abc_Clock();
1583 if ( uSharedMask == 0 )
1584 pFun = Dss_ManOperationFun( p, iDsd, nFans[0] + nFans[1] );
1585 else
1586 pFun = Dss_ManBooleanAnd( p, pEnt, 0 );
1587 if ( pFun == NULL )
1588 return -1;
1589 assert( (int)pFun->nFans == Dss_VecLitSuppSize(p->vObjs, pFun->iDsd) );
1590 assert( (int)pFun->nFans <= nKLutSize );
1591 p->timeDec += Abc_Clock() - clk;
1592 }
1593 else
1594 {
1595 clk = Abc_Clock();
1596 ppSpot = Dss_ManCacheLookup( p, pEnt );
1597 p->timeLook += Abc_Clock() - clk;
1598 clk = Abc_Clock();
1599 if ( *ppSpot == NULL )
1600 {
1601 if ( uSharedMask == 0 )
1602 pFun = Dss_ManOperationFun( p, iDsd, nFans[0] + nFans[1] );
1603 else
1604 pFun = Dss_ManBooleanAnd( p, pEnt, 0 );
1605 if ( pFun == NULL )
1606 return -1;
1607 assert( (int)pFun->nFans == Dss_VecLitSuppSize(p->vObjs, pFun->iDsd) );
1608 assert( (int)pFun->nFans <= nKLutSize );
1609 // create cache entry
1610 *ppSpot = Dss_ManCacheCreate( p, pEnt, pFun );
1611 }
1612 pFun = (*ppSpot)->pFunc;
1613 p->timeDec += Abc_Clock() - clk;
1614 }
1615
1616 clk = Abc_Clock();
1617 for ( i = 0; i < (int)pFun->nFans; i++ )
1618 if ( pFun->pFans[i] < 2 * nFans[0] ) // first dec
1619 pPermRes[i] = (unsigned char)Dss_Lit2Lit( pFans[0], pFun->pFans[i] );
1620 else
1621 pPermRes[i] = (unsigned char)Dss_Lit2Lit( pFans[1], pFun->pFans[i] - 2 * nFans[0] );
1622 // perform support minimization
1623 if ( uSharedMask && pFun->nFans > 1 )
1624 {
1625 int pVarPres[DAU_MAX_VAR];
1626 int nSupp = 0;
1627 for ( i = 0; i < p->nVars; i++ )
1628 pVarPres[i] = -1;
1629 for ( i = 0; i < (int)pFun->nFans; i++ )
1630 pVarPres[ Abc_Lit2Var(pPermRes[i]) ] = i;
1631 for ( i = 0; i < p->nVars; i++ )
1632 if ( pVarPres[i] >= 0 )
1633 pPermRes[pVarPres[i]] = Abc_Var2Lit( nSupp++, Abc_LitIsCompl(pPermRes[pVarPres[i]]) );
1634 assert( nSupp == (int)pFun->nFans );
1635 }
1636
1637 for ( i = 0; i < (int)pFun->nFans; i++ )
1638 pPermResInt[i] = pPermRes[i];
1639 p->timeEnd += Abc_Clock() - clk;
1640
1641 if ( fVerbose )
1642 {
1643 Dss_ManPrintOne( stdout, p, pFun->iDsd, pPermResInt );
1644 printf( "\n" );
1645 }
1646
1647 if ( Counter == 43418 )
1648 {
1649 // int s = 0;
1650 // Dss_ManPrint( NULL, p );
1651 }
1652
1653
1654 if ( fCheck )
1655 {
1656 pTruthOne = Dss_ManComputeTruth( p, pFun->iDsd, p->nVars, pPermResInt );
1657 if ( !Abc_TtEqual( pTruthOne, pTruth, Abc_TtWordNum(p->nVars) ) )
1658 {
1659 int s;
1660 // Kit_DsdPrintFromTruth( pTruthOne, p->nVars ); printf( "\n" );
1661 // Kit_DsdPrintFromTruth( pTruth, p->nVars ); printf( "\n" );
1662 printf( "Verification failed.\n" );
1663 s = 0;
1664 }
1665 }
1666 return pFun->iDsd;
1667 }
1668
1669
1670 /**Function*************************************************************
1671
1672 Synopsis []
1673
1674 Description []
1675
1676 SideEffects []
1677
1678 SeeAlso []
1679
1680 ***********************************************************************/
Dss_ManSharedMapDerive(Dss_Man_t * p,int iDsd0,int iDsd1,Vec_Str_t * vShared)1681 Dss_Ent_t * Dss_ManSharedMapDerive( Dss_Man_t * p, int iDsd0, int iDsd1, Vec_Str_t * vShared )
1682 {
1683 static char Buffer[100];
1684 Dss_Ent_t * pEnt = (Dss_Ent_t *)Buffer;
1685 pEnt->iDsd0 = iDsd0;
1686 pEnt->iDsd1 = iDsd1;
1687 pEnt->nShared = Vec_StrSize(vShared)/2;
1688 memcpy( pEnt->pShared, (unsigned char *)Vec_StrArray(vShared), sizeof(char) * Vec_StrSize(vShared) );
1689 pEnt->nWords = Dss_EntWordNum( pEnt );
1690 return pEnt;
1691 }
1692
Mpm_FuncCompute(Dss_Man_t * p,int iDsd0,int iDsd1,Vec_Str_t * vShared,int * pPerm,int * pnLeaves)1693 int Mpm_FuncCompute( Dss_Man_t * p, int iDsd0, int iDsd1, Vec_Str_t * vShared, int * pPerm, int * pnLeaves )
1694 {
1695 int fVerbose = 0;
1696 // int fCheck = 0;
1697 Dss_Ent_t * pEnt, ** ppSpot;
1698 Dss_Fun_t * pFun;
1699 int iDsd[2] = { iDsd0, iDsd1 };
1700 int i;
1701 abctime clk;
1702
1703 assert( iDsd0 <= iDsd1 );
1704 if ( DAU_MAX_VAR < *pnLeaves )
1705 {
1706 printf( "Paramater DAU_MAX_VAR (%d) smaller than LUT size (%d).\n", DAU_MAX_VAR, *pnLeaves );
1707 return -1;
1708 }
1709 if ( fVerbose )
1710 {
1711 Dss_ManPrintOne( stdout, p, iDsd0, NULL );
1712 Dss_ManPrintOne( stdout, p, iDsd1, NULL );
1713 }
1714
1715 clk = Abc_Clock();
1716 pEnt = Dss_ManSharedMapDerive( p, iDsd0, iDsd1, vShared );
1717 ppSpot = Dss_ManCacheLookup( p, pEnt );
1718 p->timeLook += Abc_Clock() - clk;
1719
1720 clk = Abc_Clock();
1721 if ( *ppSpot == NULL )
1722 {
1723 if ( Vec_StrSize(vShared) == 0 )
1724 pFun = Dss_ManOperationFun( p, iDsd, *pnLeaves );
1725 else
1726 pFun = Dss_ManBooleanAnd( p, pEnt, 0 );
1727 if ( pFun == NULL )
1728 return -1;
1729 assert( (int)pFun->nFans == Dss_VecLitSuppSize(p->vObjs, pFun->iDsd) );
1730 assert( (int)pFun->nFans <= *pnLeaves );
1731 // create cache entry
1732 *ppSpot = Dss_ManCacheCreate( p, pEnt, pFun );
1733 }
1734 pFun = (*ppSpot)->pFunc;
1735 p->timeDec += Abc_Clock() - clk;
1736
1737 *pnLeaves = (int)pFun->nFans;
1738 for ( i = 0; i < (int)pFun->nFans; i++ )
1739 pPerm[i] = (int)pFun->pFans[i];
1740
1741 if ( fVerbose )
1742 {
1743 Dss_ManPrintOne( stdout, p, pFun->iDsd, NULL );
1744 printf( "\n" );
1745 }
1746
1747 /*
1748 if ( fCheck )
1749 {
1750 pTruthOne = Dss_ManComputeTruth( p, pFun->iDsd, p->nVars, pPermResInt );
1751 if ( !Abc_TtEqual( pTruthOne, pTruth, Abc_TtWordNum(p->nVars) ) )
1752 {
1753 int s;
1754 // Kit_DsdPrintFromTruth( pTruthOne, p->nVars ); printf( "\n" );
1755 // Kit_DsdPrintFromTruth( pTruth, p->nVars ); printf( "\n" );
1756 printf( "Verification failed.\n" );
1757 s = 0;
1758 }
1759 }
1760 */
1761 return pFun->iDsd;
1762 }
1763
1764
1765 /**Function*************************************************************
1766
1767 Synopsis []
1768
1769 Description []
1770
1771 SideEffects []
1772
1773 SeeAlso []
1774
1775 ***********************************************************************/
Dss_ObjCheckTransparent(Dss_Man_t * p,Dss_Obj_t * pObj)1776 int Dss_ObjCheckTransparent( Dss_Man_t * p, Dss_Obj_t * pObj )
1777 {
1778 Dss_Obj_t * pFanin;
1779 int i;
1780 if ( pObj->Type == DAU_DSD_VAR )
1781 return 1;
1782 if ( pObj->Type == DAU_DSD_AND )
1783 return 0;
1784 if ( pObj->Type == DAU_DSD_XOR )
1785 {
1786 Dss_ObjForEachFanin( p->vObjs, pObj, pFanin, i )
1787 if ( Dss_ObjCheckTransparent( p, pFanin ) )
1788 return 1;
1789 return 0;
1790 }
1791 if ( pObj->Type == DAU_DSD_MUX )
1792 {
1793 pFanin = Dss_ObjFanin( p->vObjs, pObj, 1 );
1794 if ( !Dss_ObjCheckTransparent(p, pFanin) )
1795 return 0;
1796 pFanin = Dss_ObjFanin( p->vObjs, pObj, 2 );
1797 if ( !Dss_ObjCheckTransparent(p, pFanin) )
1798 return 0;
1799 return 1;
1800 }
1801 assert( pObj->Type == DAU_DSD_PRIME );
1802 return 0;
1803 }
1804
1805 /**Function*************************************************************
1806
1807 Synopsis []
1808
1809 Description []
1810
1811 SideEffects []
1812
1813 SeeAlso []
1814
1815 ***********************************************************************/
Dau_DsdTest__()1816 void Dau_DsdTest__()
1817 {
1818 int nVars = 8;
1819 // char * pDsd = "[(ab)(cd)]";
1820 char * pDsd = "(!(a!(bh))[cde]!(fg))";
1821 Dss_Ntk_t * pNtk = Dss_NtkCreate( pDsd, nVars, NULL );
1822 // Dss_NtkPrint( pNtk );
1823 // Dss_NtkCheck( pNtk );
1824 // Dss_NtkTransform( pNtk );
1825 // Dss_NtkPrint( pNtk );
1826 Dss_NtkFree( pNtk );
1827 nVars = 0;
1828 }
1829
1830 /**Function*************************************************************
1831
1832 Synopsis []
1833
1834 Description []
1835
1836 SideEffects []
1837
1838 SeeAlso []
1839
1840 ***********************************************************************/
Dau_DsdTest()1841 void Dau_DsdTest()
1842 {
1843 int nVars = 8;
1844 Vec_Vec_t * vFuncs;
1845 Vec_Int_t * vOne, * vTwo, * vRes;//, * vThree;
1846 Dss_Man_t * p;
1847 int pEntries[3];
1848 int iLit, e0, e1;//, e2;
1849 int i, k, s;//, j;
1850
1851 return;
1852
1853 vFuncs = Vec_VecStart( nVars+1 );
1854 assert( nVars < DAU_MAX_VAR );
1855 p = Dss_ManAlloc( nVars, 0 );
1856
1857 // init
1858 Vec_VecPushInt( vFuncs, 1, Dss_Obj2Lit(Dss_VecVar(p->vObjs,0)) );
1859
1860 // enumerate
1861 for ( s = 2; s <= nVars; s++ )
1862 {
1863 vRes = Vec_VecEntryInt( vFuncs, s );
1864 for ( i = 1; i < s; i++ )
1865 for ( k = i; k < s; k++ )
1866 if ( i + k == s )
1867 {
1868 vOne = Vec_VecEntryInt( vFuncs, i );
1869 vTwo = Vec_VecEntryInt( vFuncs, k );
1870 Vec_IntForEachEntry( vOne, pEntries[0], e0 )
1871 Vec_IntForEachEntry( vTwo, pEntries[1], e1 )
1872 {
1873 int fAddInv0 = !Dss_ObjCheckTransparent( p, Dss_VecObj(p->vObjs, Abc_Lit2Var(pEntries[0])) );
1874 int fAddInv1 = !Dss_ObjCheckTransparent( p, Dss_VecObj(p->vObjs, Abc_Lit2Var(pEntries[1])) );
1875
1876 iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL, NULL );
1877 assert( !Abc_LitIsCompl(iLit) );
1878 Vec_IntPush( vRes, iLit );
1879
1880 if ( fAddInv0 )
1881 {
1882 pEntries[0] = Abc_LitNot( pEntries[0] );
1883 iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL, NULL );
1884 pEntries[0] = Abc_LitNot( pEntries[0] );
1885 assert( !Abc_LitIsCompl(iLit) );
1886 Vec_IntPush( vRes, iLit );
1887 }
1888
1889 if ( fAddInv1 )
1890 {
1891 pEntries[1] = Abc_LitNot( pEntries[1] );
1892 iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL, NULL );
1893 pEntries[1] = Abc_LitNot( pEntries[1] );
1894 assert( !Abc_LitIsCompl(iLit) );
1895 Vec_IntPush( vRes, iLit );
1896 }
1897
1898 if ( fAddInv0 && fAddInv1 )
1899 {
1900 pEntries[0] = Abc_LitNot( pEntries[0] );
1901 pEntries[1] = Abc_LitNot( pEntries[1] );
1902 iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL, NULL );
1903 pEntries[0] = Abc_LitNot( pEntries[0] );
1904 pEntries[1] = Abc_LitNot( pEntries[1] );
1905 assert( !Abc_LitIsCompl(iLit) );
1906 Vec_IntPush( vRes, iLit );
1907 }
1908
1909 iLit = Dss_ManOperation( p, DAU_DSD_XOR, pEntries, 2, NULL, NULL );
1910 assert( !Abc_LitIsCompl(iLit) );
1911 Vec_IntPush( vRes, Abc_LitRegular(iLit) );
1912 }
1913 }
1914 /*
1915 for ( i = 1; i < s; i++ )
1916 for ( k = 1; k < s; k++ )
1917 for ( j = 1; j < s; j++ )
1918 if ( i + k + j == s )
1919 {
1920 vOne = Vec_VecEntryInt( vFuncs, i );
1921 vTwo = Vec_VecEntryInt( vFuncs, k );
1922 vThree = Vec_VecEntryInt( vFuncs, j );
1923 Vec_IntForEachEntry( vOne, pEntries[0], e0 )
1924 Vec_IntForEachEntry( vTwo, pEntries[1], e1 )
1925 Vec_IntForEachEntry( vThree, pEntries[2], e2 )
1926 {
1927 int fAddInv0 = !Dss_ObjCheckTransparent( p, Dss_VecObj(p->vObjs, Abc_Lit2Var(pEntries[0])) );
1928 int fAddInv1 = !Dss_ObjCheckTransparent( p, Dss_VecObj(p->vObjs, Abc_Lit2Var(pEntries[1])) );
1929 int fAddInv2 = !Dss_ObjCheckTransparent( p, Dss_VecObj(p->vObjs, Abc_Lit2Var(pEntries[2])) );
1930
1931 if ( !fAddInv0 && k > j )
1932 continue;
1933
1934 iLit = Dss_ManOperation( p, DAU_DSD_MUX, pEntries, 3, NULL, NULL );
1935 assert( !Abc_LitIsCompl(iLit) );
1936 Vec_IntPush( vRes, iLit );
1937
1938 if ( fAddInv1 )
1939 {
1940 pEntries[1] = Abc_LitNot( pEntries[1] );
1941 iLit = Dss_ManOperation( p, DAU_DSD_MUX, pEntries, 3, NULL, NULL );
1942 pEntries[1] = Abc_LitNot( pEntries[1] );
1943 assert( !Abc_LitIsCompl(iLit) );
1944 Vec_IntPush( vRes, iLit );
1945 }
1946
1947 if ( fAddInv2 )
1948 {
1949 pEntries[2] = Abc_LitNot( pEntries[2] );
1950 iLit = Dss_ManOperation( p, DAU_DSD_MUX, pEntries, 3, NULL, NULL );
1951 pEntries[2] = Abc_LitNot( pEntries[2] );
1952 assert( !Abc_LitIsCompl(iLit) );
1953 Vec_IntPush( vRes, iLit );
1954 }
1955 }
1956 }
1957 */
1958 Vec_IntUniqify( vRes );
1959 }
1960 Dss_ManPrint( "_npn/npn/dsdcanon.txt", p );
1961
1962 Dss_ManFree( p );
1963 Vec_VecFree( vFuncs );
1964 }
1965
1966
1967 /**Function*************************************************************
1968
1969 Synopsis []
1970
1971 Description []
1972
1973 SideEffects []
1974
1975 SeeAlso []
1976
1977 ***********************************************************************/
Dau_DsdTest444()1978 void Dau_DsdTest444()
1979 {
1980 Dss_Man_t * p = Dss_ManAlloc( 6, 0 );
1981 int iLit1[3] = { 2, 4 };
1982 int iLit2[3] = { 2, 4, 6 };
1983 int iRes[5];
1984 int nFans[2] = { 4, 3 };
1985 int pPermLits1[4] = { 0, 2, 5, 6 };
1986 int pPermLits2[5] = { 2, 9, 10 };
1987 int * pPermLits[2] = { pPermLits1, pPermLits2 };
1988 unsigned char pPermRes[6];
1989 int pPermResInt[6];
1990 unsigned uMaskShared = 2;
1991 int i;
1992
1993 iRes[0] = 1 ^ Dss_ManOperation( p, DAU_DSD_AND, iLit1, 2, NULL, NULL );
1994 iRes[1] = iRes[0];
1995 iRes[2] = 1 ^ Dss_ManOperation( p, DAU_DSD_AND, iRes, 2, NULL, NULL );
1996 iRes[3] = Dss_ManOperation( p, DAU_DSD_AND, iLit2, 3, NULL, NULL );
1997
1998 Dss_ManPrintOne( stdout, p, iRes[0], NULL );
1999 Dss_ManPrintOne( stdout, p, iRes[2], NULL );
2000 Dss_ManPrintOne( stdout, p, iRes[3], NULL );
2001
2002 Dss_ManPrintOne( stdout, p, iRes[2], pPermLits1 );
2003 Dss_ManPrintOne( stdout, p, iRes[3], pPermLits2 );
2004
2005 iRes[4] = Dss_ManMerge( p, iRes+2, nFans, pPermLits, uMaskShared, 6, pPermRes, NULL );
2006
2007 for ( i = 0; i < 6; i++ )
2008 pPermResInt[i] = pPermRes[i];
2009
2010 Dss_ManPrintOne( stdout, p, iRes[4], NULL );
2011 Dss_ManPrintOne( stdout, p, iRes[4], pPermResInt );
2012
2013 Dss_ManFree( p );
2014 }
2015
2016 ////////////////////////////////////////////////////////////////////////
2017 /// END OF FILE ///
2018 ////////////////////////////////////////////////////////////////////////
2019
2020
2021 ABC_NAMESPACE_IMPL_END
2022
2023