1 /**CFile****************************************************************
2
3 FileName [giaFx.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Scalable AIG package.]
8
9 Synopsis [Interface to fast_extract 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: giaFx.c,v 1.00 2013/09/29 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "gia.h"
22 #include "bool/kit/kit.h"
23 #include "misc/vec/vecWec.h"
24 #include "bool/dec/dec.h"
25 #include "opt/dau/dau.h"
26 #include "misc/util/utilTruth.h"
27
28 ABC_NAMESPACE_IMPL_START
29
30
31 ////////////////////////////////////////////////////////////////////////
32 /// DECLARATIONS ///
33 ////////////////////////////////////////////////////////////////////////
34
35 ////////////////////////////////////////////////////////////////////////
36 /// FUNCTION DEFINITIONS ///
37 ////////////////////////////////////////////////////////////////////////
38
39 /**Function*************************************************************
40
41 Synopsis [Create GIA for SOP.]
42
43 Description []
44
45 SideEffects []
46
47 SeeAlso []
48
49 ***********************************************************************/
Gia_ManGraphToAig(Gia_Man_t * p,Dec_Graph_t * pGraph)50 int Gia_ManGraphToAig( Gia_Man_t * p, Dec_Graph_t * pGraph )
51 {
52 Dec_Node_t * pNode = NULL; // Suppress "might be used uninitialized"
53 int i, iAnd0, iAnd1;
54 // check for constant function
55 if ( Dec_GraphIsConst(pGraph) )
56 return Abc_LitNotCond( 1, Dec_GraphIsComplement(pGraph) );
57 // check for a literal
58 if ( Dec_GraphIsVar(pGraph) )
59 return Abc_LitNotCond( Dec_GraphVar(pGraph)->iFunc, Dec_GraphIsComplement(pGraph) );
60 // build the AIG nodes corresponding to the AND gates of the graph
61 Dec_GraphForEachNode( pGraph, pNode, i )
62 {
63 iAnd0 = Abc_LitNotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->iFunc, pNode->eEdge0.fCompl );
64 iAnd1 = Abc_LitNotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->iFunc, pNode->eEdge1.fCompl );
65 pNode->iFunc = Gia_ManHashAnd( p, iAnd0, iAnd1 );
66 }
67 // complement the result if necessary
68 return Abc_LitNotCond( pNode->iFunc, Dec_GraphIsComplement(pGraph) );
69 }
Gia_ManSopToAig(Gia_Man_t * p,char * pSop,Vec_Int_t * vLeaves)70 int Gia_ManSopToAig( Gia_Man_t * p, char * pSop, Vec_Int_t * vLeaves )
71 {
72 int i, iAnd, iSum, Value, nFanins;
73 char * pCube;
74 // get the number of variables
75 nFanins = Kit_PlaGetVarNum(pSop);
76 // go through the cubes of the node's SOP
77 iSum = 0;
78 Kit_PlaForEachCube( pSop, nFanins, pCube )
79 {
80 // create the AND of literals
81 iAnd = 1;
82 Kit_PlaCubeForEachVar( pCube, Value, i )
83 {
84 assert( Vec_IntEntry(vLeaves, i) >= 0 );
85 if ( Value == '1' )
86 iAnd = Gia_ManHashAnd( p, iAnd, Vec_IntEntry(vLeaves, i) );
87 else if ( Value == '0' )
88 iAnd = Gia_ManHashAnd( p, iAnd, Abc_LitNot(Vec_IntEntry(vLeaves, i)) );
89 else assert( Value == '-' );
90 }
91 // add to the sum of cubes
92 iSum = Gia_ManHashOr( p, iSum, iAnd );
93 }
94 // decide whether to complement the result
95 if ( Kit_PlaIsComplement(pSop) )
96 iSum = Abc_LitNot(iSum);
97 return iSum;
98 }
Gia_ManFactorGraph(Gia_Man_t * p,Dec_Graph_t * pFForm,Vec_Int_t * vLeaves)99 int Gia_ManFactorGraph( Gia_Man_t * p, Dec_Graph_t * pFForm, Vec_Int_t * vLeaves )
100 {
101 Dec_Node_t * pFFNode;
102 int i, Lit;
103 // assign fanins
104 Dec_GraphForEachLeaf( pFForm, pFFNode, i )
105 {
106 assert( Vec_IntEntry(vLeaves, i) >= 0 );
107 pFFNode->iFunc = Vec_IntEntry(vLeaves, i);
108 }
109 // perform strashing
110 Lit = Gia_ManGraphToAig( p, pFForm );
111 return Lit;
112 }
Gia_ManFactorNode(Gia_Man_t * p,char * pSop,Vec_Int_t * vLeaves)113 int Gia_ManFactorNode( Gia_Man_t * p, char * pSop, Vec_Int_t * vLeaves )
114 {
115 if ( Kit_PlaGetVarNum(pSop) == 0 )
116 return Abc_LitNotCond( 1, Kit_PlaIsConst0(pSop) );
117 assert( Kit_PlaGetVarNum(pSop) == Vec_IntSize(vLeaves) );
118 if ( Kit_PlaGetVarNum(pSop) > 2 && Kit_PlaGetCubeNum(pSop) > 1 )
119 {
120 Dec_Graph_t * pFForm = Dec_Factor( pSop );
121 int Lit = Gia_ManFactorGraph( p, pFForm, vLeaves );
122 Dec_GraphFree( pFForm );
123 return Lit;
124 }
125 return Gia_ManSopToAig( p, pSop, vLeaves );
126 }
127
128 /**Function*************************************************************
129
130 Synopsis [Computing truth tables for the mapped network.]
131
132 Description []
133
134 SideEffects []
135
136 SeeAlso []
137
138 ***********************************************************************/
Gia_ManComputeTruths(Gia_Man_t * p,int nCutSize,int nLutNum,int fReverse)139 Vec_Wrd_t * Gia_ManComputeTruths( Gia_Man_t * p, int nCutSize, int nLutNum, int fReverse )
140 {
141 Vec_Wrd_t * vTruths;
142 Vec_Int_t vLeaves;
143 word * pTruth;
144 int i, k, nWords;
145 nWords = Abc_Truth6WordNum( nCutSize );
146 vTruths = Vec_WrdAlloc( nWords * nLutNum );
147 Gia_ObjComputeTruthTableStart( p, nCutSize );
148 Gia_ManForEachLut( p, i )
149 {
150 // collect and sort fanins
151 vLeaves.nCap = vLeaves.nSize = Gia_ObjLutSize( p, i );
152 vLeaves.pArray = Gia_ObjLutFanins( p, i );
153 assert( Vec_IntCheckUniqueSmall(&vLeaves) );
154 Vec_IntSelectSort( Vec_IntArray(&vLeaves), Vec_IntSize(&vLeaves) );
155 if ( !fReverse )
156 Vec_IntReverseOrder( &vLeaves );
157 // compute truth table
158 pTruth = Gia_ObjComputeTruthTableCut( p, Gia_ManObj(p, i), &vLeaves );
159 for ( k = 0; k < nWords; k++ )
160 Vec_WrdPush( vTruths, pTruth[k] );
161 // Kit_DsdPrintFromTruth( (unsigned *)pTruth, 6 ); printf( "\n" );
162 }
163 Gia_ObjComputeTruthTableStop( p );
164 assert( Vec_WrdCap(vTruths) == 16 || Vec_WrdSize(vTruths) == Vec_WrdCap(vTruths) );
165 return vTruths;
166 }
167
168 /**Function*************************************************************
169
170 Synopsis [Extracts information about the network.]
171
172 Description []
173
174 SideEffects []
175
176 SeeAlso []
177
178 ***********************************************************************/
Gia_ManAssignNumbers(Gia_Man_t * p)179 int Gia_ManAssignNumbers( Gia_Man_t * p )
180 {
181 Gia_Obj_t * pObj;
182 int i, Counter = 0;
183 Gia_ManFillValue( p );
184 Gia_ManForEachCi( p, pObj, i )
185 pObj->Value = Counter++;
186 Gia_ManForEachLut( p, i )
187 Gia_ManObj(p, i)->Value = Counter++;
188 return Counter;
189 }
Gia_ManFxRetrieve(Gia_Man_t * p,Vec_Str_t ** pvCompl,int fReverse)190 Vec_Wec_t * Gia_ManFxRetrieve( Gia_Man_t * p, Vec_Str_t ** pvCompl, int fReverse )
191 {
192 Vec_Wec_t * vCubes;
193 Vec_Wrd_t * vTruths;
194 Vec_Int_t * vCube, * vCover;
195 int nItems, nCutSize, nWords;
196 int i, c, v, Lit, Cube, Counter = 0;
197 // abctime clk = Abc_Clock();
198 nItems = Gia_ManAssignNumbers( p );
199 // compute truth tables
200 nCutSize = Gia_ManLutSizeMax( p );
201 nWords = Abc_Truth6WordNum( nCutSize );
202 vTruths = Gia_ManComputeTruths( p, nCutSize, nItems - Gia_ManCiNum(p), fReverse );
203 vCover = Vec_IntAlloc( 1 << 16 );
204 // collect cubes
205 vCubes = Vec_WecAlloc( 1000 );
206 *pvCompl = Vec_StrStart( nItems );
207 Gia_ManForEachLut( p, i )
208 {
209 Gia_Obj_t * pObj = Gia_ManObj( p, i );
210 int nVars = Gia_ObjLutSize( p, i );
211 int * pVars = Gia_ObjLutFanins( p, i );
212 word * pTruth = Vec_WrdEntryP( vTruths, Counter++ * nWords );
213 int Status = Kit_TruthIsop( (unsigned *)pTruth, nVars, vCover, 1 );
214 if ( Vec_IntSize(vCover) == 0 || (Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover,0) == 0) )
215 {
216 Vec_StrWriteEntry( *pvCompl, pObj->Value, (char)(Vec_IntSize(vCover) == 0) );
217 vCube = Vec_WecPushLevel( vCubes );
218 Vec_IntPush( vCube, pObj->Value );
219 continue;
220 }
221 Vec_StrWriteEntry( *pvCompl, pObj->Value, (char)Status );
222 Vec_IntForEachEntry( vCover, Cube, c )
223 {
224 vCube = Vec_WecPushLevel( vCubes );
225 Vec_IntPush( vCube, pObj->Value );
226 for ( v = 0; v < nVars; v++ )
227 {
228 Lit = 3 & (Cube >> (v << 1));
229 if ( Lit == 1 )
230 Vec_IntPush( vCube, Abc_Var2Lit(Gia_ManObj(p, pVars[v])->Value, 1) );
231 else if ( Lit == 2 )
232 Vec_IntPush( vCube, Abc_Var2Lit(Gia_ManObj(p, pVars[v])->Value, 0) );
233 else if ( Lit != 0 )
234 assert( 0 );
235 }
236 Vec_IntSelectSort( Vec_IntArray(vCube) + 1, Vec_IntSize(vCube) - 1 );
237 }
238 }
239 assert( Counter * nWords == Vec_WrdSize(vTruths) );
240 Vec_WrdFree( vTruths );
241 Vec_IntFree( vCover );
242 // Abc_PrintTime( 1, "Setup time", Abc_Clock() - clk );
243 return vCubes;
244 }
245
246 /**Function*************************************************************
247
248 Synopsis [Generates GIA after factoring the resulting SOPs.]
249
250 Description []
251
252 SideEffects []
253
254 SeeAlso []
255
256 ***********************************************************************/
Gia_ManFxTopoOrder_rec(Vec_Wec_t * vCubes,Vec_Int_t * vFirst,Vec_Int_t * vCount,Vec_Int_t * vVisit,Vec_Int_t * vOrder,int iObj)257 void Gia_ManFxTopoOrder_rec( Vec_Wec_t * vCubes, Vec_Int_t * vFirst, Vec_Int_t * vCount, Vec_Int_t * vVisit, Vec_Int_t * vOrder, int iObj )
258 {
259 int c, v, Lit;
260 int iFirst = Vec_IntEntry( vFirst, iObj );
261 int nCubes = Vec_IntEntry( vCount, iObj );
262 assert( !Vec_IntEntry( vVisit, iObj ) );
263 Vec_IntWriteEntry( vVisit, iObj, 1 );
264 for ( c = 0; c < nCubes; c++ )
265 {
266 Vec_Int_t * vCube = Vec_WecEntry( vCubes, iFirst + c );
267 assert( Vec_IntEntry(vCube, 0) == iObj );
268 Vec_IntForEachEntryStart( vCube, Lit, v, 1 )
269 if ( !Vec_IntEntry( vVisit, Abc_Lit2Var(Lit) ) )
270 Gia_ManFxTopoOrder_rec( vCubes, vFirst, vCount, vVisit, vOrder, Abc_Lit2Var(Lit) );
271 }
272 Vec_IntPush( vOrder, iObj );
273 }
Gia_ManFxTopoOrder(Vec_Wec_t * vCubes,int nInputs,int nStart,Vec_Int_t ** pvFirst,Vec_Int_t ** pvCount)274 Vec_Int_t * Gia_ManFxTopoOrder( Vec_Wec_t * vCubes, int nInputs, int nStart, Vec_Int_t ** pvFirst, Vec_Int_t ** pvCount )
275 {
276 Vec_Int_t * vOrder, * vFirst, * vCount, * vVisit, * vCube;
277 int i, iFanin, nNodeMax = -1;
278 // find the largest index
279 Vec_WecForEachLevel( vCubes, vCube, i )
280 nNodeMax = Abc_MaxInt( nNodeMax, Vec_IntEntry(vCube, 0) );
281 nNodeMax++;
282 // quit if there is no new nodes
283 if ( nNodeMax == nStart )
284 {
285 //printf( "The network is unchanged by fast extract.\n" );
286 return NULL;
287 }
288 // find first cube and how many cubes
289 vFirst = Vec_IntStart( nNodeMax );
290 vCount = Vec_IntStart( nNodeMax );
291 Vec_WecForEachLevel( vCubes, vCube, i )
292 {
293 iFanin = Vec_IntEntry( vCube, 0 );
294 assert( iFanin >= nInputs );
295 if ( Vec_IntEntry(vCount, iFanin) == 0 )
296 Vec_IntWriteEntry( vFirst, iFanin, i );
297 Vec_IntAddToEntry( vCount, iFanin, 1 );
298 }
299 // put all of them in a topo order
300 vOrder = Vec_IntStart( nInputs );
301 vVisit = Vec_IntStart( nNodeMax );
302 for ( i = 0; i < nInputs; i++ )
303 Vec_IntWriteEntry( vVisit, i, 1 );
304 for ( i = nInputs; i < nNodeMax; i++ )
305 if ( !Vec_IntEntry( vVisit, i ) )
306 Gia_ManFxTopoOrder_rec( vCubes, vFirst, vCount, vVisit, vOrder, i );
307 assert( Vec_IntSize(vOrder) == nNodeMax );
308 Vec_IntFree( vVisit );
309 // return topological order of new nodes
310 *pvFirst = vFirst;
311 *pvCount = vCount;
312 return vOrder;
313 }
Gia_ManFxInsert(Gia_Man_t * p,Vec_Wec_t * vCubes,Vec_Str_t * vCompls)314 Gia_Man_t * Gia_ManFxInsert( Gia_Man_t * p, Vec_Wec_t * vCubes, Vec_Str_t * vCompls )
315 {
316 Gia_Man_t * pNew, * pTemp;
317 Gia_Obj_t * pObj; Vec_Str_t * vSop;
318 Vec_Int_t * vOrder, * vFirst, * vCount, * vFanins, * vCover;
319 Vec_Int_t * vCopies, * vCube, * vMap;
320 int k, c, v, Lit, Var, iItem;
321 // abctime clk = Abc_Clock();
322 // prepare the cubes
323 vOrder = Gia_ManFxTopoOrder( vCubes, Gia_ManCiNum(p), Vec_StrSize(vCompls), &vFirst, &vCount );
324 if ( vOrder == NULL )
325 return Gia_ManDup( p );
326 assert( Vec_IntSize(vOrder) > Vec_StrSize(vCompls) );
327 // create new manager
328 pNew = Gia_ManStart( Gia_ManObjNum(p) );
329 pNew->pName = Abc_UtilStrsav( p->pName );
330 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
331 pNew->vLevels = Vec_IntStart( 6*Gia_ManObjNum(p)/5 + 100 );
332 Gia_ManHashStart( pNew );
333 // create primary inputs
334 vMap = Vec_IntStartFull( Vec_IntSize(vOrder) );
335 vCopies = Vec_IntAlloc( Vec_IntSize(vOrder) );
336 Gia_ManForEachCi( p, pObj, k )
337 Vec_IntPush( vCopies, Gia_ManAppendCi(pNew) );
338 Vec_IntFillExtra( vCopies, Vec_IntSize(vOrder), -1 );
339 // add AIG nodes in the topological order
340 vSop = Vec_StrAlloc( 1000 );
341 vCover = Vec_IntAlloc( 1 << 16 );
342 vFanins = Vec_IntAlloc( 100 );
343 Vec_IntForEachEntryStart( vOrder, iItem, k, Gia_ManCiNum(p) )
344 {
345 int iFirst = Vec_IntEntry( vFirst, iItem );
346 int nCubes = Vec_IntEntry( vCount, iItem );
347 // collect fanins
348 Vec_IntClear( vFanins );
349 for ( c = 0; c < nCubes; c++ )
350 {
351 vCube = Vec_WecEntry( vCubes, iFirst + c );
352 Vec_IntForEachEntryStart( vCube, Lit, v, 1 )
353 if ( Vec_IntEntry(vMap, Abc_Lit2Var(Lit)) == -1 )
354 {
355 Vec_IntWriteEntry( vMap, Abc_Lit2Var(Lit), Vec_IntSize(vFanins) );
356 Vec_IntPush( vFanins, Abc_Lit2Var(Lit) );
357 }
358 }
359 if ( Vec_IntSize(vFanins) > 6 )
360 {
361 // create SOP
362 Vec_StrClear( vSop );
363 for ( c = 0; c < nCubes; c++ )
364 {
365 for ( v = 0; v < Vec_IntSize(vFanins); v++ )
366 Vec_StrPush( vSop, '-' );
367 vCube = Vec_WecEntry( vCubes, iFirst + c );
368 Vec_IntForEachEntryStart( vCube, Lit, v, 1 )
369 {
370 Lit = Abc_Lit2LitV( Vec_IntArray(vMap), Lit );
371 assert( Lit >= 0 && Abc_Lit2Var(Lit) < Vec_IntSize(vFanins) );
372 Vec_StrWriteEntry( vSop, Vec_StrSize(vSop) - Vec_IntSize(vFanins) + Abc_Lit2Var(Lit), (char)(Abc_LitIsCompl(Lit)? '0' : '1') );
373 }
374 Vec_StrPush( vSop, ' ' );
375 Vec_StrPush( vSop, '1' );
376 Vec_StrPush( vSop, '\n' );
377 }
378 Vec_StrPush( vSop, '\0' );
379 // collect fanins
380 Vec_IntForEachEntry( vFanins, Var, v )
381 {
382 Vec_IntWriteEntry( vMap, Var, -1 );
383 Vec_IntWriteEntry( vFanins, v, Vec_IntEntry(vCopies, Var) );
384 }
385 // derive new AIG
386 Lit = Gia_ManFactorNode( pNew, Vec_StrArray(vSop), vFanins );
387 }
388 else
389 {
390 word uTruth = 0, uCube;
391 for ( c = 0; c < nCubes; c++ )
392 {
393 uCube = ~(word)0;
394 vCube = Vec_WecEntry( vCubes, iFirst + c );
395 Vec_IntForEachEntryStart( vCube, Lit, v, 1 )
396 {
397 Lit = Abc_Lit2LitV( Vec_IntArray(vMap), Lit );
398 assert( Lit >= 0 && Abc_Lit2Var(Lit) < Vec_IntSize(vFanins) );
399 uCube &= Abc_LitIsCompl(Lit) ? ~s_Truths6[Abc_Lit2Var(Lit)] : s_Truths6[Abc_Lit2Var(Lit)];
400 }
401 uTruth |= uCube;
402 }
403 // complement constant
404 if ( uTruth == 0 )
405 uTruth = ~uTruth;
406 // collect fanins
407 Vec_IntForEachEntry( vFanins, Var, v )
408 {
409 Vec_IntWriteEntry( vMap, Var, -1 );
410 Vec_IntWriteEntry( vFanins, v, Vec_IntEntry(vCopies, Var) );
411 }
412 // create truth table
413 Lit = Dsm_ManTruthToGia( pNew, &uTruth, vFanins, vCover );
414 }
415 // complement if the original SOP was complemented
416 Lit = Abc_LitNotCond( Lit, (iItem < Vec_StrSize(vCompls)) && (Vec_StrEntry(vCompls, iItem) > 0) );
417 // remeber this literal
418 assert( Vec_IntEntry(vCopies, iItem) == -1 );
419 Vec_IntWriteEntry( vCopies, iItem, Lit );
420 }
421 Gia_ManHashStop( pNew );
422 // create primary outputs
423 Gia_ManForEachCo( p, pObj, k )
424 {
425 Lit = Gia_ObjFaninId0p(p, pObj) ? Vec_IntEntry(vCopies, Gia_ObjFanin0(pObj)->Value) : 0;
426 Gia_ManAppendCo( pNew, Abc_LitNotCond( Lit, Gia_ObjFaninC0(pObj) ) );
427 }
428 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
429 // cleanup
430 Vec_IntFree( vOrder );
431 Vec_IntFree( vFirst );
432 Vec_IntFree( vCount );
433 Vec_IntFree( vFanins );
434 Vec_IntFree( vCopies );
435 Vec_IntFree( vMap );
436 Vec_StrFree( vSop );
437 Vec_IntFree( vCover );
438 // remove dangling nodes
439 pNew = Gia_ManCleanup( pTemp = pNew );
440 Gia_ManStop( pTemp );
441 // Abc_PrintTime( 1, "Setdn time", Abc_Clock() - clk );
442 return pNew;
443 }
444
445 /**Function*************************************************************
446
447 Synopsis [Performs classical fast_extract on logic functions.]
448
449 Description []
450
451 SideEffects [Sorts the fanins of each cut in the increasing order.]
452
453 SeeAlso []
454
455 ***********************************************************************/
Gia_ManPerformFx(Gia_Man_t * p,int nNewNodesMax,int LitCountMax,int fReverse,int fVerbose,int fVeryVerbose)456 Gia_Man_t * Gia_ManPerformFx( Gia_Man_t * p, int nNewNodesMax, int LitCountMax, int fReverse, int fVerbose, int fVeryVerbose )
457 {
458 extern int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int LitCountMax, int fCanonDivs, int fVerbose, int fVeryVerbose );
459 Gia_Man_t * pNew = NULL;
460 Vec_Wec_t * vCubes;
461 Vec_Str_t * vCompl;
462 if ( Gia_ManAndNum(p) == 0 )
463 return Gia_ManDup(p);
464 // abctime clk;
465 assert( Gia_ManHasMapping(p) );
466 // collect information
467 vCubes = Gia_ManFxRetrieve( p, &vCompl, fReverse );
468 // call the fast extract procedure
469 // clk = Abc_Clock();
470 Fx_FastExtract( vCubes, Vec_StrSize(vCompl), nNewNodesMax, LitCountMax, 0, fVerbose, fVeryVerbose );
471 // Abc_PrintTime( 1, "Fx runtime", Abc_Clock() - clk );
472 // insert information
473 pNew = Gia_ManFxInsert( p, vCubes, vCompl );
474 Gia_ManTransferTiming( pNew, p );
475 // cleanup
476 Vec_WecFree( vCubes );
477 Vec_StrFree( vCompl );
478 return pNew;
479 }
480
481 ////////////////////////////////////////////////////////////////////////
482 /// END OF FILE ///
483 ////////////////////////////////////////////////////////////////////////
484
485
486 ABC_NAMESPACE_IMPL_END
487
488