1 /**CFile****************************************************************
2
3 FileName [extraUtilMult.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [extra]
8
9 Synopsis [Simple BDD package.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - May 23, 2018.]
16
17 Revision [$Id: extraUtilMult.c,v 1.0 2018/05/23 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include <stdio.h>
22 #include <stdlib.h>
23 #include <string.h>
24 #include <assert.h>
25 #include "misc/vec/vec.h"
26 #include "aig/gia/gia.h"
27
28 ABC_NAMESPACE_IMPL_START
29
30 ////////////////////////////////////////////////////////////////////////
31 /// DECLARATIONS ///
32 ////////////////////////////////////////////////////////////////////////
33
34 typedef struct Abc_BddMan_ Abc_BddMan;
35 struct Abc_BddMan_
36 {
37 int nVars; // the number of variables
38 int nObjs; // the number of nodes used
39 int nObjsAlloc; // the number of nodes allocated
40 int * pUnique; // unique table for nodes
41 int * pNexts; // next pointer for nodes
42 int * pCache; // array of triples <arg0, arg1, AND(arg0, arg1)>
43 int * pObjs; // array of pairs <cof0, cof1> for each node
44 unsigned char * pVars; // array of variables for each node
45 unsigned char * pMark; // array of marks for each BDD node
46 unsigned nUniqueMask; // selection mask for unique table
47 unsigned nCacheMask; // selection mask for computed table
48 int nCacheLookups; // the number of computed table lookups
49 int nCacheMisses; // the number of computed table misses
50 word nMemory; // total amount of memory used (in bytes)
51 };
52
Abc_BddIthVar(int i)53 static inline int Abc_BddIthVar( int i ) { return Abc_Var2Lit(i + 1, 0); }
Abc_BddHash(int Arg0,int Arg1,int Arg2)54 static inline unsigned Abc_BddHash( int Arg0, int Arg1, int Arg2 ) { return 12582917 * Arg0 + 4256249 * Arg1 + 741457 * Arg2; }
55
Abc_BddVar(Abc_BddMan * p,int i)56 static inline int Abc_BddVar( Abc_BddMan * p, int i ) { return (int)p->pVars[Abc_Lit2Var(i)]; }
Abc_BddThen(Abc_BddMan * p,int i)57 static inline int Abc_BddThen( Abc_BddMan * p, int i ) { return Abc_LitNotCond(p->pObjs[Abc_LitRegular(i)], Abc_LitIsCompl(i)); }
Abc_BddElse(Abc_BddMan * p,int i)58 static inline int Abc_BddElse( Abc_BddMan * p, int i ) { return Abc_LitNotCond(p->pObjs[Abc_LitRegular(i)+1], Abc_LitIsCompl(i)); }
59
Abc_BddMark(Abc_BddMan * p,int i)60 static inline int Abc_BddMark( Abc_BddMan * p, int i ) { return (int)p->pMark[Abc_Lit2Var(i)]; }
Abc_BddSetMark(Abc_BddMan * p,int i,int m)61 static inline void Abc_BddSetMark( Abc_BddMan * p, int i, int m ){ p->pMark[Abc_Lit2Var(i)] = m; }
62
63 ////////////////////////////////////////////////////////////////////////
64 /// FUNCTION DEFINITIONS ///
65 ////////////////////////////////////////////////////////////////////////
66
67 /**Function*************************************************************
68
69 Synopsis [Creating new node.]
70
71 Description []
72
73 SideEffects []
74
75 SeeAlso []
76
77 ***********************************************************************/
Abc_BddUniqueCreateInt(Abc_BddMan * p,int Var,int Then,int Else)78 static inline int Abc_BddUniqueCreateInt( Abc_BddMan * p, int Var, int Then, int Else )
79 {
80 int *q = p->pUnique + (Abc_BddHash(Var, Then, Else) & p->nUniqueMask);
81 for ( ; *q; q = p->pNexts + *q )
82 if ( (int)p->pVars[*q] == Var && p->pObjs[*q+*q] == Then && p->pObjs[*q+*q+1] == Else )
83 return Abc_Var2Lit(*q, 0);
84 if ( p->nObjs == p->nObjsAlloc )
85 printf( "Aborting because the number of nodes exceeded %d.\n", p->nObjsAlloc ), fflush(stdout);
86 assert( p->nObjs < p->nObjsAlloc );
87 *q = p->nObjs++;
88 p->pVars[*q] = Var;
89 p->pObjs[*q+*q] = Then;
90 p->pObjs[*q+*q+1] = Else;
91 // printf( "Added node %3d: Var = %3d. Then = %3d. Else = %3d\n", *q, Var, Then, Else );
92 assert( !Abc_LitIsCompl(Else) );
93 return Abc_Var2Lit(*q, 0);
94 }
Abc_BddUniqueCreate(Abc_BddMan * p,int Var,int Then,int Else)95 static inline int Abc_BddUniqueCreate( Abc_BddMan * p, int Var, int Then, int Else )
96 {
97 assert( Var >= 0 && Var < p->nVars );
98 assert( Var < Abc_BddVar(p, Then) );
99 assert( Var < Abc_BddVar(p, Else) );
100 if ( Then == Else )
101 return Else;
102 if ( !Abc_LitIsCompl(Else) )
103 return Abc_BddUniqueCreateInt( p, Var, Then, Else );
104 return Abc_LitNot( Abc_BddUniqueCreateInt(p, Var, Abc_LitNot(Then), Abc_LitNot(Else)) );
105 }
106
107 /**Function*************************************************************
108
109 Synopsis []
110
111 Description []
112
113 SideEffects []
114
115 SeeAlso []
116
117 ***********************************************************************/
Abc_BddCacheLookup(Abc_BddMan * p,int Arg1,int Arg2)118 static inline int Abc_BddCacheLookup( Abc_BddMan * p, int Arg1, int Arg2 )
119 {
120 int * pEnt = p->pCache + 3*(Abc_BddHash(0, Arg1, Arg2) & p->nCacheMask);
121 p->nCacheLookups++;
122 return (pEnt[0] == Arg1 && pEnt[1] == Arg2) ? pEnt[2] : -1;
123 }
Abc_BddCacheInsert(Abc_BddMan * p,int Arg1,int Arg2,int Res)124 static inline int Abc_BddCacheInsert( Abc_BddMan * p, int Arg1, int Arg2, int Res )
125 {
126 int * pEnt = p->pCache + 3*(Abc_BddHash(0, Arg1, Arg2) & p->nCacheMask);
127 pEnt[0] = Arg1; pEnt[1] = Arg2; pEnt[2] = Res;
128 p->nCacheMisses++;
129 assert( Res >= 0 );
130 return Res;
131 }
132
133
134 /**Function*************************************************************
135
136 Synopsis []
137
138 Description []
139
140 SideEffects []
141
142 SeeAlso []
143
144 ***********************************************************************/
Abc_BddManAlloc(int nVars,int nObjs)145 Abc_BddMan * Abc_BddManAlloc( int nVars, int nObjs )
146 {
147 Abc_BddMan * p; int i;
148 p = ABC_CALLOC( Abc_BddMan, 1 );
149 p->nVars = nVars;
150 p->nObjsAlloc = nObjs;
151 p->nUniqueMask = (1 << Abc_Base2Log(nObjs)) - 1;
152 p->nCacheMask = (1 << Abc_Base2Log(nObjs)) - 1;
153 p->pUnique = ABC_CALLOC( int, p->nUniqueMask + 1 );
154 p->pNexts = ABC_CALLOC( int, p->nObjsAlloc );
155 p->pCache = ABC_CALLOC( int, 3*(p->nCacheMask + 1) );
156 p->pObjs = ABC_CALLOC( int, 2*p->nObjsAlloc );
157 p->pMark = ABC_CALLOC( unsigned char, p->nObjsAlloc );
158 p->pVars = ABC_CALLOC( unsigned char, p->nObjsAlloc );
159 p->pVars[0] = 0xff;
160 p->nObjs = 1;
161 for ( i = 0; i < nVars; i++ )
162 Abc_BddUniqueCreate( p, i, 1, 0 );
163 assert( p->nObjs == nVars + 1 );
164 p->nMemory = sizeof(Abc_BddMan)/4 +
165 p->nUniqueMask + 1 + p->nObjsAlloc +
166 (p->nCacheMask + 1) * 3 * sizeof(int)/4 +
167 p->nObjsAlloc * 2 * sizeof(int)/4;
168 return p;
169 }
Abc_BddManFree(Abc_BddMan * p)170 void Abc_BddManFree( Abc_BddMan * p )
171 {
172 printf( "BDD stats: Var = %d Obj = %d Alloc = %d Hit = %d Miss = %d ",
173 p->nVars, p->nObjs, p->nObjsAlloc, p->nCacheLookups-p->nCacheMisses, p->nCacheMisses );
174 printf( "Mem = %.2f MB\n", 4.0*(int)(p->nMemory/(1<<20)) );
175 ABC_FREE( p->pUnique );
176 ABC_FREE( p->pNexts );
177 ABC_FREE( p->pCache );
178 ABC_FREE( p->pObjs );
179 ABC_FREE( p->pVars );
180 ABC_FREE( p );
181 }
182
183 /**Function*************************************************************
184
185 Synopsis [Boolean AND.]
186
187 Description []
188
189 SideEffects []
190
191 SeeAlso []
192
193 ***********************************************************************/
Abc_BddAnd(Abc_BddMan * p,int a,int b)194 int Abc_BddAnd( Abc_BddMan * p, int a, int b )
195 {
196 int r0, r1, r;
197 if ( a == 0 ) return 0;
198 if ( b == 0 ) return 0;
199 if ( a == 1 ) return b;
200 if ( b == 1 ) return a;
201 if ( a == b ) return a;
202 if ( a > b ) return Abc_BddAnd( p, b, a );
203 if ( (r = Abc_BddCacheLookup(p, a, b)) >= 0 )
204 return r;
205 if ( Abc_BddVar(p, a) < Abc_BddVar(p, b) )
206 r0 = Abc_BddAnd( p, Abc_BddElse(p, a), b ),
207 r1 = Abc_BddAnd( p, Abc_BddThen(p, a), b );
208 else if ( Abc_BddVar(p, a) > Abc_BddVar(p, b) )
209 r0 = Abc_BddAnd( p, a, Abc_BddElse(p, b) ),
210 r1 = Abc_BddAnd( p, a, Abc_BddThen(p, b) );
211 else // if ( Abc_BddVar(p, a) == Abc_BddVar(p, b) )
212 r0 = Abc_BddAnd( p, Abc_BddElse(p, a), Abc_BddElse(p, b) ),
213 r1 = Abc_BddAnd( p, Abc_BddThen(p, a), Abc_BddThen(p, b) );
214 r = Abc_BddUniqueCreate( p, Abc_MinInt(Abc_BddVar(p, a), Abc_BddVar(p, b)), r1, r0 );
215 return Abc_BddCacheInsert( p, a, b, r );
216 }
Abc_BddOr(Abc_BddMan * p,int a,int b)217 int Abc_BddOr( Abc_BddMan * p, int a, int b )
218 {
219 return Abc_LitNot( Abc_BddAnd(p, Abc_LitNot(a), Abc_LitNot(b)) );
220 }
221
222 /**Function*************************************************************
223
224 Synopsis [Counting nodes.]
225
226 Description []
227
228 SideEffects []
229
230 SeeAlso []
231
232 ***********************************************************************/
Abc_BddCount_rec(Abc_BddMan * p,int i)233 int Abc_BddCount_rec( Abc_BddMan * p, int i )
234 {
235 if ( i < 2 )
236 return 0;
237 if ( Abc_BddMark(p, i) )
238 return 0;
239 Abc_BddSetMark( p, i, 1 );
240 return 1 + Abc_BddCount_rec(p, Abc_BddElse(p, i)) + Abc_BddCount_rec(p, Abc_BddThen(p, i));
241 }
Abc_BddUnmark_rec(Abc_BddMan * p,int i)242 void Abc_BddUnmark_rec( Abc_BddMan * p, int i )
243 {
244 if ( i < 2 )
245 return;
246 if ( !Abc_BddMark(p, i) )
247 return;
248 Abc_BddSetMark( p, i, 0 );
249 Abc_BddUnmark_rec( p, Abc_BddElse(p, i) );
250 Abc_BddUnmark_rec( p, Abc_BddThen(p, i) );
251 }
Abc_BddCountNodes(Abc_BddMan * p,int i)252 int Abc_BddCountNodes( Abc_BddMan * p, int i )
253 {
254 int Count = Abc_BddCount_rec( p, i );
255 Abc_BddUnmark_rec( p, i );
256 return Count;
257 }
Abc_BddCountNodesArray(Abc_BddMan * p,Vec_Int_t * vNodes)258 int Abc_BddCountNodesArray( Abc_BddMan * p, Vec_Int_t * vNodes )
259 {
260 int i, a, Count = 0;
261 Vec_IntForEachEntry( vNodes, a, i )
262 Count += Abc_BddCount_rec( p, a );
263 Vec_IntForEachEntry( vNodes, a, i )
264 Abc_BddUnmark_rec( p, a );
265 return Count;
266 }
Abc_BddCountNodesArray2(Abc_BddMan * p,Vec_Int_t * vNodes)267 int Abc_BddCountNodesArray2( Abc_BddMan * p, Vec_Int_t * vNodes )
268 {
269 int i, a, Count = 0;
270 Vec_IntForEachEntry( vNodes, a, i )
271 {
272 Count += Abc_BddCount_rec( p, a );
273 Abc_BddUnmark_rec( p, a );
274 }
275 return Count;
276 }
277
278
279
280 /**Function*************************************************************
281
282 Synopsis [Printing BDD.]
283
284 Description []
285
286 SideEffects []
287
288 SeeAlso []
289
290 ***********************************************************************/
Abc_BddPrint_rec(Abc_BddMan * p,int a,int * pPath)291 void Abc_BddPrint_rec( Abc_BddMan * p, int a, int * pPath )
292 {
293 if ( a == 0 )
294 return;
295 if ( a == 1 )
296 {
297 int i;
298 for ( i = 0; i < p->nVars; i++ )
299 if ( pPath[i] == 0 || pPath[i] == 1 )
300 printf( "%c%d", pPath[i] ? '+' : '-', i );
301 printf( " " );
302 return;
303 }
304 pPath[Abc_BddVar(p, a)] = 0;
305 Abc_BddPrint_rec( p, Abc_BddElse(p, a), pPath );
306 pPath[Abc_BddVar(p, a)] = 1;
307 Abc_BddPrint_rec( p, Abc_BddThen(p, a), pPath );
308 pPath[Abc_BddVar(p, a)] = -1;
309 }
Abc_BddPrint(Abc_BddMan * p,int a)310 void Abc_BddPrint( Abc_BddMan * p, int a )
311 {
312 int * pPath = ABC_FALLOC( int, p->nVars );
313 printf( "BDD %d = ", a );
314 Abc_BddPrint_rec( p, a, pPath );
315 ABC_FREE( pPath );
316 printf( "\n" );
317 }
Abc_BddPrintTest(Abc_BddMan * p)318 void Abc_BddPrintTest( Abc_BddMan * p )
319 {
320 int bVarA = Abc_BddIthVar(0);
321 int bVarB = Abc_BddIthVar(1);
322 int bVarC = Abc_BddIthVar(2);
323 int bVarD = Abc_BddIthVar(3);
324 int bAndAB = Abc_BddAnd( p, bVarA, bVarB );
325 int bAndCD = Abc_BddAnd( p, bVarC, bVarD );
326 int bFunc = Abc_BddOr( p, bAndAB, bAndCD );
327 Abc_BddPrint( p, bFunc );
328 printf( "Nodes = %d\n", Abc_BddCountNodes(p, bFunc) );
329 }
330
331
332 /**Function*************************************************************
333
334 Synopsis []
335
336 Description []
337
338 SideEffects []
339
340 SeeAlso []
341
342 ***********************************************************************/
Abc_BddGiaTest2(Gia_Man_t * pGia,int fVerbose)343 void Abc_BddGiaTest2( Gia_Man_t * pGia, int fVerbose )
344 {
345 Abc_BddMan * p = Abc_BddManAlloc( 10, 100 );
346 Abc_BddPrintTest( p );
347 Abc_BddManFree( p );
348 }
349
Abc_BddGiaTest(Gia_Man_t * pGia,int fVerbose)350 void Abc_BddGiaTest( Gia_Man_t * pGia, int fVerbose )
351 {
352 Abc_BddMan * p;
353 Vec_Int_t * vNodes;
354 Gia_Obj_t * pObj; int i;
355 p = Abc_BddManAlloc( Gia_ManCiNum(pGia), 1 << 20 ); // 30 B/node
356 Gia_ManFillValue( pGia );
357 Gia_ManConst0(pGia)->Value = 0;
358 Gia_ManForEachCi( pGia, pObj, i )
359 pObj->Value = Abc_BddIthVar( i );
360 vNodes = Vec_IntAlloc( Gia_ManAndNum(pGia) );
361 Gia_ManForEachAnd( pGia, pObj, i )
362 {
363 int Cof0 = Abc_LitNotCond(Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj));
364 int Cof1 = Abc_LitNotCond(Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj));
365 pObj->Value = Abc_BddAnd( p, Cof0, Cof1 );
366 }
367 Gia_ManForEachCo( pGia, pObj, i )
368 pObj->Value = Abc_LitNotCond(Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj));
369 Gia_ManForEachCo( pGia, pObj, i )
370 {
371 if ( fVerbose )
372 Abc_BddPrint( p, pObj->Value );
373 Vec_IntPush( vNodes, pObj->Value );
374 }
375 printf( "Shared nodes = %d.\n", Abc_BddCountNodesArray2(p, vNodes) );
376 Vec_IntFree( vNodes );
377 Abc_BddManFree( p );
378 }
379
380 /*
381 abc 04> c.aig; &get; &test
382 Shared nodes = 80.
383 BDD stats: Var = 23 Obj = 206 Alloc = 1048576 Hit = 59 Miss = 216 Mem = 28.00 MB
384
385 abc 05> c.aig; clp -r; ps
386 c : i/o = 23/ 2 lat = 0 nd = 2 edge = 46 bdd = 80 lev = 1
387 */
388
389 ////////////////////////////////////////////////////////////////////////
390 /// END OF FILE ///
391 ////////////////////////////////////////////////////////////////////////
392
393
394 ABC_NAMESPACE_IMPL_END
395
396