ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
ivyMulti.c
Go to the documentation of this file.
1
20
21#include "ivy.h"
22
24
25
29
30#define IVY_EVAL_LIMIT 128
31
32typedef struct Ivy_Eva_t_ Ivy_Eva_t;
34{
35 Ivy_Obj_t * pArg; // the argument node
36 unsigned Mask; // the mask of covered nodes
37 int Weight; // the number of covered nodes
38};
39
40static void Ivy_MultiPrint( Ivy_Man_t * p, Ivy_Eva_t * pEvals, int nLeaves, int nEvals );
41static int Ivy_MultiCover( Ivy_Man_t * p, Ivy_Eva_t * pEvals, int nLeaves, int nEvals, int nLimit, Vec_Ptr_t * vSols );
42
46
58int Ivy_MultiPlus( Ivy_Man_t * p, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Ivy_Type_t Type, int nLimit, Vec_Ptr_t * vSols )
59{
60 static Ivy_Eva_t pEvals[IVY_EVAL_LIMIT];
61 Ivy_Eva_t * pEval, * pFan0, * pFan1;
62 Ivy_Obj_t * pObj = NULL; // Suppress "might be used uninitialized"
63 Ivy_Obj_t * pTemp;
64 int nEvals, nEvalsOld, i, k, x, nLeaves;
65 unsigned uMaskAll;
66
67 // consider special cases
68 nLeaves = Vec_PtrSize(vLeaves);
69 assert( nLeaves > 2 );
70 if ( nLeaves > 32 || nLeaves + Vec_PtrSize(vCone) > IVY_EVAL_LIMIT )
71 return 0;
72// if ( nLeaves == 1 )
73// return Vec_PtrEntry( vLeaves, 0 );
74// if ( nLeaves == 2 )
75// return Ivy_Oper( Vec_PtrEntry(vLeaves, 0), Vec_PtrEntry(vLeaves, 1), Type );
76
77 // set the leaf entries
78 uMaskAll = ((1 << nLeaves) - 1);
79 nEvals = 0;
80 Vec_PtrForEachEntry( Ivy_Obj_t *, vLeaves, pObj, i )
81 {
82 pEval = pEvals + nEvals;
83 pEval->pArg = pObj;
84 pEval->Mask = (1 << nEvals);
85 pEval->Weight = 1;
86 // mark the leaf
87 Ivy_Regular(pObj)->TravId = nEvals;
88 nEvals++;
89 }
90
91 // propagate masks through the cone
92 Vec_PtrForEachEntry( Ivy_Obj_t *, vCone, pObj, i )
93 {
94 pObj->TravId = nEvals + i;
95 if ( Ivy_ObjIsBuf(pObj) )
96 pEvals[pObj->TravId].Mask = pEvals[Ivy_ObjFanin0(pObj)->TravId].Mask;
97 else
98 pEvals[pObj->TravId].Mask = pEvals[Ivy_ObjFanin0(pObj)->TravId].Mask | pEvals[Ivy_ObjFanin1(pObj)->TravId].Mask;
99 }
100
101 // set the internal entries
102 Vec_PtrForEachEntry( Ivy_Obj_t *, vCone, pObj, i )
103 {
104 if ( i == Vec_PtrSize(vCone) - 1 )
105 break;
106 // skip buffers
107 if ( Ivy_ObjIsBuf(pObj) )
108 continue;
109 // skip nodes without external fanout
110 if ( Ivy_ObjRefs(pObj) == 0 )
111 continue;
112 assert( !Ivy_IsComplement(pObj) );
113 pEval = pEvals + nEvals;
114 pEval->pArg = pObj;
115 pEval->Mask = pEvals[pObj->TravId].Mask;
116 pEval->Weight = Extra_WordCountOnes(pEval->Mask);
117 // mark the node
118 pObj->TravId = nEvals;
119 nEvals++;
120 }
121
122 // find the available nodes
123 nEvalsOld = nEvals;
124 for ( i = 1; i < nEvals; i++ )
125 for ( k = 0; k < i; k++ )
126 {
127 pFan0 = pEvals + i;
128 pFan1 = pEvals + k;
129 pTemp = Ivy_TableLookup(p, Ivy_ObjCreateGhost(p, pFan0->pArg, pFan1->pArg, Type, IVY_INIT_NONE));
130 // skip nodes in the cone
131 if ( pTemp == NULL || pTemp->fMarkB )
132 continue;
133 // skip the leaves
134 for ( x = 0; x < nLeaves; x++ )
135 if ( pTemp == Ivy_Regular((Ivy_Obj_t *)vLeaves->pArray[x]) )
136 break;
137 if ( x < nLeaves )
138 continue;
139 pEval = pEvals + nEvals;
140 pEval->pArg = pTemp;
141 pEval->Mask = pFan0->Mask | pFan1->Mask;
142 pEval->Weight = (pFan0->Mask & pFan1->Mask) ? Extra_WordCountOnes(pEval->Mask) : pFan0->Weight + pFan1->Weight;
143 // save the argument
144 pObj->TravId = nEvals;
145 nEvals++;
146 // quit if the number of entries exceeded the limit
147 if ( nEvals == IVY_EVAL_LIMIT )
148 goto Outside;
149 // quit if we found an acceptable implementation
150 if ( pEval->Mask == uMaskAll )
151 goto Outside;
152 }
153Outside:
154
155// Ivy_MultiPrint( pEvals, nLeaves, nEvals );
156 if ( !Ivy_MultiCover( p, pEvals, nLeaves, nEvals, nLimit, vSols ) )
157 return 0;
158 assert( Vec_PtrSize( vSols ) > 0 );
159 return 1;
160}
161
173void Ivy_MultiPrint( Ivy_Man_t * p, Ivy_Eva_t * pEvals, int nLeaves, int nEvals )
174{
175 Ivy_Eva_t * pEval;
176 int i, k;
177 for ( i = nLeaves; i < nEvals; i++ )
178 {
179 pEval = pEvals + i;
180 printf( "%2d (id = %5d) : |", i-nLeaves, Ivy_ObjId(pEval->pArg) );
181 for ( k = 0; k < nLeaves; k++ )
182 {
183 if ( pEval->Mask & (1 << k) )
184 printf( "+" );
185 else
186 printf( " " );
187 }
188 printf( "| Lev = %d.\n", Ivy_ObjLevel(pEval->pArg) );
189 }
190}
191
203static inline int Ivy_MultiWeight( unsigned uMask, int nMaskOnes, unsigned uFound )
204{
205 assert( uMask & ~uFound );
206 if ( (uMask & uFound) == 0 )
207 return nMaskOnes;
208 return Extra_WordCountOnes( uMask & ~uFound );
209}
210
222int Ivy_MultiCover( Ivy_Man_t * p, Ivy_Eva_t * pEvals, int nLeaves, int nEvals, int nLimit, Vec_Ptr_t * vSols )
223{
224 int fVerbose = 0;
225 Ivy_Eva_t * pEval;
226 Ivy_Eva_t * pEvalBest = NULL; // Suppress "might be used uninitialized"
227 unsigned uMaskAll, uFound, uTemp;
228 int i, k, BestK;
229 int WeightBest = -1; // Suppress "might be used uninitialized"
230 int WeightCur;
231 int LevelBest = -1; // Suppress "might be used uninitialized"
232 int LevelCur;
233 uMaskAll = (nLeaves == 32)? (~(unsigned)0) : ((1 << nLeaves) - 1);
234 uFound = 0;
235 // solve the covering problem
236 if ( fVerbose )
237 printf( "Solution: " );
238 Vec_PtrClear( vSols );
239 for ( i = 0; i < nLimit; i++ )
240 {
241 BestK = -1;
242 for ( k = nEvals - 1; k >= 0; k-- )
243 {
244 pEval = pEvals + k;
245 if ( (pEval->Mask & ~uFound) == 0 )
246 continue;
247 if ( BestK == -1 )
248 {
249 BestK = k;
250 pEvalBest = pEval;
251 WeightBest = Ivy_MultiWeight( pEvalBest->Mask, pEvalBest->Weight, uFound );
252 LevelBest = Ivy_ObjLevel( Ivy_Regular(pEvalBest->pArg) );
253 continue;
254 }
255 // compare BestK and the new one (k)
256 WeightCur = Ivy_MultiWeight( pEval->Mask, pEval->Weight, uFound );
257 LevelCur = Ivy_ObjLevel( Ivy_Regular(pEval->pArg) );
258 if ( WeightBest < WeightCur ||
259 (WeightBest == WeightCur && LevelBest > LevelCur) )
260 {
261 BestK = k;
262 pEvalBest = pEval;
263 WeightBest = WeightCur;
264 LevelBest = LevelCur;
265 }
266 }
267 assert( BestK != -1 );
268 // if the cost is only 1, take the leaf
269 if ( WeightBest == 1 && BestK >= nLeaves )
270 {
271 uTemp = (pEvalBest->Mask & ~uFound);
272 for ( k = 0; k < nLeaves; k++ )
273 if ( uTemp & (1 << k) )
274 break;
275 assert( k < nLeaves );
276 BestK = k;
277 pEvalBest = pEvals + BestK;
278 }
279 if ( fVerbose )
280 {
281 if ( BestK < nLeaves )
282 printf( "L(%d) ", BestK );
283 else
284 printf( "%d ", BestK - nLeaves );
285 }
286 // update the found set
287 Vec_PtrPush( vSols, pEvalBest->pArg );
288 uFound |= pEvalBest->Mask;
289 if ( uFound == uMaskAll )
290 break;
291 }
292 if ( uFound == uMaskAll )
293 {
294 if ( fVerbose )
295 printf( " Found \n\n" );
296 return 1;
297 }
298 else
299 {
300 if ( fVerbose )
301 printf( " Not found \n\n" );
302 return 0;
303 }
304}
305
309
310
312
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
Cube * p
Definition exorList.c:222
struct Ivy_Eva_t_ Ivy_Eva_t
Definition ivyMulti.c:32
#define IVY_EVAL_LIMIT
DECLARATIONS ///.
Definition ivyMulti.c:30
int Ivy_MultiPlus(Ivy_Man_t *p, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vCone, Ivy_Type_t Type, int nLimit, Vec_Ptr_t *vSols)
FUNCTION DEFINITIONS ///.
Definition ivyMulti.c:58
typedefABC_NAMESPACE_HEADER_START struct Ivy_Man_t_ Ivy_Man_t
INCLUDES ///.
Definition ivy.h:46
@ IVY_INIT_NONE
Definition ivy.h:66
Ivy_Obj_t * Ivy_TableLookup(Ivy_Man_t *p, Ivy_Obj_t *pObj)
FUNCTION DEFINITIONS ///.
Definition ivyTable.c:71
struct Ivy_Obj_t_ Ivy_Obj_t
Definition ivy.h:47
Ivy_Type_t
Definition ivy.h:52
unsigned Mask
Definition ivyMulti.c:36
int Weight
Definition ivyMulti.c:37
Ivy_Obj_t * pArg
Definition ivyMulti.c:35
unsigned fMarkB
Definition ivy.h:79
int TravId
Definition ivy.h:76
#define assert(ex)
Definition util_old.h:213
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55