1 /**CFile****************************************************************
2
3 FileName [abcFraig.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Network and node package.]
8
9 Synopsis [Procedures interfacing with the FRAIG 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: abcFraig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "base/abc/abc.h"
22 #include "proof/fraig/fraig.h"
23 #include "base/main/main.h"
24
25 ABC_NAMESPACE_IMPL_START
26
27
28 ////////////////////////////////////////////////////////////////////////
29 /// DECLARATIONS ///
30 ////////////////////////////////////////////////////////////////////////
31
32 extern Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
33 static Abc_Ntk_t * Abc_NtkFromFraig2( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
34 static Abc_Obj_t * Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFraig );
35 static void Abc_NtkFromFraig2_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Ptr_t * vNodeReprs );
36 extern Fraig_Node_t * Abc_NtkToFraigExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtkMain, Abc_Ntk_t * pNtkExdc );
37 static void Abc_NtkFraigRemapUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
38
39 static int Abc_NtkFraigTrustCheck( Abc_Ntk_t * pNtk );
40 static void Abc_NtkFraigTrustOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
41 static Abc_Obj_t * Abc_NodeFraigTrust( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode );
42
43 ////////////////////////////////////////////////////////////////////////
44 /// FUNCTION DEFINITIONS ///
45 ////////////////////////////////////////////////////////////////////////
46
47 /**Function*************************************************************
48
49 Synopsis [Interfaces the network with the FRAIG package.]
50
51 Description []
52
53 SideEffects []
54
55 SeeAlso []
56
57 ***********************************************************************/
Abc_NtkFraig(Abc_Ntk_t * pNtk,void * pParams,int fAllNodes,int fExdc)58 Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc )
59 {
60 Fraig_Params_t * pPars = (Fraig_Params_t *)pParams;
61 Abc_Ntk_t * pNtkNew;
62 Fraig_Man_t * pMan;
63 // check if EXDC is present
64 if ( fExdc && pNtk->pExdc == NULL )
65 fExdc = 0, printf( "Warning: Networks has no EXDC.\n" );
66 // perform fraiging
67 pMan = (Fraig_Man_t *)Abc_NtkToFraig( pNtk, pParams, fAllNodes, fExdc );
68 // add algebraic choices
69 // if ( pPars->fChoicing )
70 // Fraig_ManAddChoices( pMan, 0, 6 );
71 // prove the miter if asked to
72 if ( pPars->fTryProve )
73 Fraig_ManProveMiter( pMan );
74 // reconstruct FRAIG in the new network
75 if ( fExdc )
76 pNtkNew = Abc_NtkFromFraig2( pMan, pNtk );
77 else
78 pNtkNew = Abc_NtkFromFraig( pMan, pNtk );
79 Fraig_ManFree( pMan );
80 if ( pNtk->pExdc )
81 pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
82 // make sure that everything is okay
83 if ( !Abc_NtkCheck( pNtkNew ) )
84 {
85 printf( "Abc_NtkFraig: The network check has failed.\n" );
86 Abc_NtkDelete( pNtkNew );
87 return NULL;
88 }
89 return pNtkNew;
90 }
91
92 /**Function*************************************************************
93
94 Synopsis [Transforms the strashed network into FRAIG.]
95
96 Description []
97
98 SideEffects []
99
100 SeeAlso []
101
102 ***********************************************************************/
Abc_NtkToFraig(Abc_Ntk_t * pNtk,void * pParams,int fAllNodes,int fExdc)103 void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc )
104 {
105 int fInternal = ((Fraig_Params_t *)pParams)->fInternal;
106 Fraig_Man_t * pMan;
107 ProgressBar * pProgress = NULL;
108 Vec_Ptr_t * vNodes;
109 Abc_Obj_t * pNode;
110 int i;
111
112 assert( Abc_NtkIsStrash(pNtk) );
113
114 // create the FRAIG manager
115 pMan = Fraig_ManCreate( (Fraig_Params_t *)pParams );
116
117 // map the constant node
118 Abc_NtkCleanCopy( pNtk );
119 Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Fraig_ManReadConst1(pMan);
120 // create PIs and remember them in the old nodes
121 Abc_NtkForEachCi( pNtk, pNode, i )
122 pNode->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, i);
123
124 // perform strashing
125 vNodes = Abc_AigDfs( pNtk, fAllNodes, 0 );
126 if ( !fInternal )
127 pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
128 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
129 {
130 if ( Abc_ObjFaninNum(pNode) == 0 )
131 continue;
132 if ( pProgress )
133 Extra_ProgressBarUpdate( pProgress, i, NULL );
134 pNode->pCopy = (Abc_Obj_t *)Fraig_NodeAnd( pMan,
135 Fraig_NotCond( Abc_ObjFanin0(pNode)->pCopy, (int)Abc_ObjFaninC0(pNode) ),
136 Fraig_NotCond( Abc_ObjFanin1(pNode)->pCopy, (int)Abc_ObjFaninC1(pNode) ) );
137 }
138 if ( pProgress )
139 Extra_ProgressBarStop( pProgress );
140 Vec_PtrFree( vNodes );
141
142 // use EXDC to change the mapping of nodes into FRAIG nodes
143 if ( fExdc )
144 Abc_NtkFraigRemapUsingExdc( pMan, pNtk );
145
146 // set the primary outputs
147 Abc_NtkForEachCo( pNtk, pNode, i )
148 Fraig_ManSetPo( pMan, (Fraig_Node_t *)Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ) );
149 return pMan;
150 }
151
152 /**Function*************************************************************
153
154 Synopsis [Derives EXDC node for the given network.]
155
156 Description [Assumes that EXDCs of all POs are the same.
157 Returns the EXDC of the first PO.]
158
159 SideEffects []
160
161 SeeAlso []
162
163 ***********************************************************************/
Abc_NtkToFraigExdc(Fraig_Man_t * pMan,Abc_Ntk_t * pNtkMain,Abc_Ntk_t * pNtkExdc)164 Fraig_Node_t * Abc_NtkToFraigExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtkMain, Abc_Ntk_t * pNtkExdc )
165 {
166 Abc_Ntk_t * pNtkStrash;
167 Abc_Obj_t * pObj;
168 Fraig_Node_t * gResult;
169 char ** ppNames;
170 int i, k;
171 // strash the EXDC network
172 pNtkStrash = Abc_NtkStrash( pNtkExdc, 0, 0, 0 );
173 Abc_NtkCleanCopy( pNtkStrash );
174 Abc_AigConst1(pNtkStrash)->pCopy = (Abc_Obj_t *)Fraig_ManReadConst1(pMan);
175 // set the mapping of the PI nodes
176 ppNames = Abc_NtkCollectCioNames( pNtkMain, 0 );
177 Abc_NtkForEachCi( pNtkStrash, pObj, i )
178 {
179 for ( k = 0; k < Abc_NtkCiNum(pNtkMain); k++ )
180 if ( strcmp( Abc_ObjName(pObj), ppNames[k] ) == 0 )
181 {
182 pObj->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, k);
183 break;
184 }
185 assert( pObj->pCopy != NULL );
186 }
187 ABC_FREE( ppNames );
188 // build FRAIG for each node
189 Abc_AigForEachAnd( pNtkStrash, pObj, i )
190 pObj->pCopy = (Abc_Obj_t *)Fraig_NodeAnd( pMan,
191 Fraig_NotCond( Abc_ObjFanin0(pObj)->pCopy, (int)Abc_ObjFaninC0(pObj) ),
192 Fraig_NotCond( Abc_ObjFanin1(pObj)->pCopy, (int)Abc_ObjFaninC1(pObj) ) );
193 // get the EXDC to be returned
194 pObj = Abc_NtkPo( pNtkStrash, 0 );
195 gResult = Fraig_NotCond( Abc_ObjFanin0(pObj)->pCopy, (int)Abc_ObjFaninC0(pObj) );
196 Abc_NtkDelete( pNtkStrash );
197 return gResult;
198 }
199
200
201 /**Function*************************************************************
202
203 Synopsis [Changes mapping of the old nodes into FRAIG nodes using EXDC.]
204
205 Description []
206
207 SideEffects []
208
209 SeeAlso []
210
211 ***********************************************************************/
Abc_NtkFraigRemapUsingExdc(Fraig_Man_t * pMan,Abc_Ntk_t * pNtk)212 void Abc_NtkFraigRemapUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
213 {
214 Fraig_Node_t * gNodeNew, * gNodeExdc;
215 stmm_table * tTable;
216 stmm_generator * gen;
217 Abc_Obj_t * pNode, * pNodeBest;
218 Abc_Obj_t * pClass, ** ppSlot;
219 Vec_Ptr_t * vNexts;
220 int i;
221
222 // get the global don't-cares
223 assert( pNtk->pExdc );
224 gNodeExdc = Abc_NtkToFraigExdc( pMan, pNtk, pNtk->pExdc );
225
226 // save the next pointers
227 vNexts = Vec_PtrStart( Abc_NtkObjNumMax(pNtk) );
228 Abc_NtkForEachNode( pNtk, pNode, i )
229 Vec_PtrWriteEntry( vNexts, pNode->Id, pNode->pNext );
230
231 // find the classes of AIG nodes which have FRAIG nodes assigned
232 Abc_NtkCleanNext( pNtk );
233 tTable = stmm_init_table(stmm_ptrcmp,stmm_ptrhash);
234 Abc_NtkForEachNode( pNtk, pNode, i )
235 if ( pNode->pCopy )
236 {
237 gNodeNew = Fraig_NodeAnd( pMan, (Fraig_Node_t *)pNode->pCopy, Fraig_Not(gNodeExdc) );
238 if ( !stmm_find_or_add( tTable, (char *)Fraig_Regular(gNodeNew), (char ***)&ppSlot ) )
239 *ppSlot = NULL;
240 pNode->pNext = *ppSlot;
241 *ppSlot = pNode;
242 }
243
244 // for reach non-trival class, find the node with minimum level, and replace other nodes by it
245 Abc_AigSetNodePhases( pNtk );
246 stmm_foreach_item( tTable, gen, (char **)&gNodeNew, (char **)&pClass )
247 {
248 if ( pClass->pNext == NULL )
249 continue;
250 // find the node with minimum level
251 pNodeBest = pClass;
252 for ( pNode = pClass->pNext; pNode; pNode = pNode->pNext )
253 if ( pNodeBest->Level > pNode->Level )
254 pNodeBest = pNode;
255 // remap the class nodes
256 for ( pNode = pClass; pNode; pNode = pNode->pNext )
257 pNode->pCopy = Abc_ObjNotCond( pNodeBest->pCopy, pNode->fPhase ^ pNodeBest->fPhase );
258 }
259 stmm_free_table( tTable );
260
261 // restore the next pointers
262 Abc_NtkCleanNext( pNtk );
263 Abc_NtkForEachNode( pNtk, pNode, i )
264 pNode->pNext = (Abc_Obj_t *)Vec_PtrEntry( vNexts, pNode->Id );
265 Vec_PtrFree( vNexts );
266 }
267
268 /**Function*************************************************************
269
270 Synopsis [Transforms FRAIG into strashed network with choices.]
271
272 Description []
273
274 SideEffects []
275
276 SeeAlso []
277
278 ***********************************************************************/
Abc_NtkFromFraig(Fraig_Man_t * pMan,Abc_Ntk_t * pNtk)279 Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
280 {
281 ProgressBar * pProgress;
282 Abc_Ntk_t * pNtkNew;
283 Abc_Obj_t * pNode, * pNodeNew;
284 int i;
285 // create the new network
286 pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
287 // make the mapper point to the new network
288 Abc_NtkForEachCi( pNtk, pNode, i )
289 Fraig_NodeSetData1( Fraig_ManReadIthVar(pMan, i), (Fraig_Node_t *)pNode->pCopy );
290 // set the constant node
291 Fraig_NodeSetData1( Fraig_ManReadConst1(pMan), (Fraig_Node_t *)Abc_AigConst1(pNtkNew) );
292 // process the nodes in topological order
293 pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
294 Abc_NtkForEachCo( pNtk, pNode, i )
295 {
296 Extra_ProgressBarUpdate( pProgress, i, NULL );
297 pNodeNew = Abc_NodeFromFraig_rec( pNtkNew, Fraig_ManReadOutputs(pMan)[i] );
298 Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
299 }
300 Extra_ProgressBarStop( pProgress );
301 Abc_NtkReassignIds( pNtkNew );
302 return pNtkNew;
303 }
304
305 /**Function*************************************************************
306
307 Synopsis [Transforms into AIG one node.]
308
309 Description []
310
311 SideEffects []
312
313 SeeAlso []
314
315 ***********************************************************************/
Abc_NodeFromFraig_rec(Abc_Ntk_t * pNtkNew,Fraig_Node_t * pNodeFraig)316 Abc_Obj_t * Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFraig )
317 {
318 Abc_Obj_t * pRes, * pRes0, * pRes1, * pResMin, * pResCur;
319 Fraig_Node_t * pNodeTemp, * pNodeFraigR = Fraig_Regular(pNodeFraig);
320 void ** ppTail;
321 // check if the node was already considered
322 if ( (pRes = (Abc_Obj_t *)Fraig_NodeReadData1(pNodeFraigR)) )
323 return Abc_ObjNotCond( pRes, Fraig_IsComplement(pNodeFraig) );
324 // solve the children
325 pRes0 = Abc_NodeFromFraig_rec( pNtkNew, Fraig_NodeReadOne(pNodeFraigR) );
326 pRes1 = Abc_NodeFromFraig_rec( pNtkNew, Fraig_NodeReadTwo(pNodeFraigR) );
327 // derive the new node
328 pRes = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, pRes0, pRes1 );
329 pRes->fPhase = Fraig_NodeReadSimInv( pNodeFraigR );
330 // if the node has an equivalence class, find its representative
331 if ( Fraig_NodeReadRepr(pNodeFraigR) == NULL && Fraig_NodeReadNextE(pNodeFraigR) != NULL )
332 {
333 // go through the FRAIG nodes belonging to this equivalence class
334 // and find the representative node (the node with the smallest level)
335 pResMin = pRes;
336 for ( pNodeTemp = Fraig_NodeReadNextE(pNodeFraigR); pNodeTemp; pNodeTemp = Fraig_NodeReadNextE(pNodeTemp) )
337 {
338 assert( Fraig_NodeReadData1(pNodeTemp) == NULL );
339 pResCur = Abc_NodeFromFraig_rec( pNtkNew, pNodeTemp );
340 if ( pResMin->Level > pResCur->Level )
341 pResMin = pResCur;
342 }
343 // link the nodes in such a way that representative goes first
344 ppTail = &pResMin->pData;
345 if ( pRes != pResMin )
346 {
347 *ppTail = pRes;
348 ppTail = &pRes->pData;
349 }
350 for ( pNodeTemp = Fraig_NodeReadNextE(pNodeFraigR); pNodeTemp; pNodeTemp = Fraig_NodeReadNextE(pNodeTemp) )
351 {
352 pResCur = (Abc_Obj_t *)Fraig_NodeReadData1(pNodeTemp);
353 assert( pResCur );
354 if ( pResMin == pResCur )
355 continue;
356 *ppTail = pResCur;
357 ppTail = &pResCur->pData;
358 }
359 assert( *ppTail == NULL );
360
361 // update the phase of the node
362 pRes = Abc_ObjNotCond( pResMin, (pRes->fPhase ^ pResMin->fPhase) );
363 }
364 Fraig_NodeSetData1( pNodeFraigR, (Fraig_Node_t *)pRes );
365 return Abc_ObjNotCond( pRes, Fraig_IsComplement(pNodeFraig) );
366 }
367
368 /**Function*************************************************************
369
370 Synopsis [Transforms FRAIG into strashed network without choices.]
371
372 Description []
373
374 SideEffects []
375
376 SeeAlso []
377
378 ***********************************************************************/
Abc_NtkFromFraig2(Fraig_Man_t * pMan,Abc_Ntk_t * pNtk)379 Abc_Ntk_t * Abc_NtkFromFraig2( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
380 {
381 ProgressBar * pProgress;
382 stmm_table * tTable;
383 Vec_Ptr_t * vNodeReprs;
384 Abc_Ntk_t * pNtkNew;
385 Abc_Obj_t * pNode, * pRepr, ** ppSlot;
386 int i;
387
388 // map the nodes into their lowest level representives
389 tTable = stmm_init_table(stmm_ptrcmp,stmm_ptrhash);
390 pNode = Abc_AigConst1(pNtk);
391 if ( !stmm_find_or_add( tTable, (char *)Fraig_Regular(pNode->pCopy), (char ***)&ppSlot ) )
392 *ppSlot = pNode;
393 Abc_NtkForEachCi( pNtk, pNode, i )
394 if ( !stmm_find_or_add( tTable, (char *)Fraig_Regular(pNode->pCopy), (char ***)&ppSlot ) )
395 *ppSlot = pNode;
396 Abc_NtkForEachNode( pNtk, pNode, i )
397 if ( pNode->pCopy )
398 {
399 if ( !stmm_find_or_add( tTable, (char *)Fraig_Regular(pNode->pCopy), (char ***)&ppSlot ) )
400 *ppSlot = pNode;
401 else if ( (*ppSlot)->Level > pNode->Level )
402 *ppSlot = pNode;
403 }
404 // save representatives for each node
405 vNodeReprs = Vec_PtrStart( Abc_NtkObjNumMax(pNtk) );
406 Abc_NtkForEachNode( pNtk, pNode, i )
407 if ( pNode->pCopy )
408 {
409 if ( !stmm_lookup( tTable, (char *)Fraig_Regular(pNode->pCopy), (char **)&pRepr ) )
410 assert( 0 );
411 if ( pNode != pRepr )
412 Vec_PtrWriteEntry( vNodeReprs, pNode->Id, pRepr );
413 }
414 stmm_free_table( tTable );
415
416 // create the new network
417 pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
418
419 // perform strashing
420 Abc_AigSetNodePhases( pNtk );
421 Abc_NtkIncrementTravId( pNtk );
422 pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
423 Abc_NtkForEachCo( pNtk, pNode, i )
424 {
425 Extra_ProgressBarUpdate( pProgress, i, NULL );
426 Abc_NtkFromFraig2_rec( pNtkNew, Abc_ObjFanin0(pNode), vNodeReprs );
427 }
428 Extra_ProgressBarStop( pProgress );
429 Vec_PtrFree( vNodeReprs );
430
431 // finalize the network
432 Abc_NtkFinalize( pNtk, pNtkNew );
433 return pNtkNew;
434 }
435
436
437 /**Function*************************************************************
438
439 Synopsis [Transforms into AIG one node.]
440
441 Description []
442
443 SideEffects []
444
445 SeeAlso []
446
447 ***********************************************************************/
Abc_NtkFromFraig2_rec(Abc_Ntk_t * pNtkNew,Abc_Obj_t * pNode,Vec_Ptr_t * vNodeReprs)448 void Abc_NtkFromFraig2_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Ptr_t * vNodeReprs )
449 {
450 Abc_Obj_t * pRepr;
451 // skip the PIs and constants
452 if ( Abc_ObjFaninNum(pNode) < 2 )
453 return;
454 // if this node is already visited, skip
455 if ( Abc_NodeIsTravIdCurrent( pNode ) )
456 return;
457 // mark the node as visited
458 Abc_NodeSetTravIdCurrent( pNode );
459 assert( Abc_ObjIsNode( pNode ) );
460 // get the node's representative
461 if ( (pRepr = (Abc_Obj_t *)Vec_PtrEntry(vNodeReprs, pNode->Id)) )
462 {
463 Abc_NtkFromFraig2_rec( pNtkNew, pRepr, vNodeReprs );
464 pNode->pCopy = Abc_ObjNotCond( pRepr->pCopy, pRepr->fPhase ^ pNode->fPhase );
465 return;
466 }
467 Abc_NtkFromFraig2_rec( pNtkNew, Abc_ObjFanin0(pNode), vNodeReprs );
468 Abc_NtkFromFraig2_rec( pNtkNew, Abc_ObjFanin1(pNode), vNodeReprs );
469 pNode->pCopy = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) );
470 }
471
472
473
474 /**Function*************************************************************
475
476 Synopsis [Interfaces the network with the FRAIG package.]
477
478 Description []
479
480 SideEffects []
481
482 SeeAlso []
483
484 ***********************************************************************/
Abc_NtkFraigTrust(Abc_Ntk_t * pNtk)485 Abc_Ntk_t * Abc_NtkFraigTrust( Abc_Ntk_t * pNtk )
486 {
487 Abc_Ntk_t * pNtkNew;
488
489 if ( !Abc_NtkIsSopLogic(pNtk) )
490 {
491 printf( "Abc_NtkFraigTrust: Trust mode works for netlists and logic SOP networks.\n" );
492 return NULL;
493 }
494
495 if ( !Abc_NtkFraigTrustCheck(pNtk) )
496 {
497 printf( "Abc_NtkFraigTrust: The network does not look like an AIG with choice nodes.\n" );
498 return NULL;
499 }
500
501 // perform strashing
502 pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
503 Abc_NtkFraigTrustOne( pNtk, pNtkNew );
504 Abc_NtkFinalize( pNtk, pNtkNew );
505 Abc_NtkReassignIds( pNtkNew );
506
507 // print a warning about choice nodes
508 printf( "Warning: The resulting AIG contains %d choice nodes.\n", Abc_NtkGetChoiceNum( pNtkNew ) );
509
510 // make sure that everything is okay
511 if ( !Abc_NtkCheck( pNtkNew ) )
512 {
513 printf( "Abc_NtkFraigTrust: The network check has failed.\n" );
514 Abc_NtkDelete( pNtkNew );
515 return NULL;
516 }
517 return pNtkNew;
518 }
519
520 /**Function*************************************************************
521
522 Synopsis [Checks whether the node can be processed in the trust mode.]
523
524 Description []
525
526 SideEffects []
527
528 SeeAlso []
529
530 ***********************************************************************/
Abc_NtkFraigTrustCheck(Abc_Ntk_t * pNtk)531 int Abc_NtkFraigTrustCheck( Abc_Ntk_t * pNtk )
532 {
533 Abc_Obj_t * pNode;
534 int i, nFanins;
535 Abc_NtkForEachNode( pNtk, pNode, i )
536 {
537 nFanins = Abc_ObjFaninNum(pNode);
538 if ( nFanins < 2 )
539 continue;
540 if ( nFanins == 2 && Abc_SopIsAndType((char *)pNode->pData) )
541 continue;
542 if ( !Abc_SopIsOrType((char *)pNode->pData) )
543 return 0;
544 }
545 return 1;
546 }
547
548 /**Function*************************************************************
549
550 Synopsis [Interfaces the network with the FRAIG package.]
551
552 Description []
553
554 SideEffects []
555
556 SeeAlso []
557
558 ***********************************************************************/
Abc_NtkFraigTrustOne(Abc_Ntk_t * pNtk,Abc_Ntk_t * pNtkNew)559 void Abc_NtkFraigTrustOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
560 {
561 ProgressBar * pProgress;
562 Vec_Ptr_t * vNodes;
563 Abc_Obj_t * pNode, * pNodeNew, * pObj;
564 int i;
565
566 // perform strashing
567 vNodes = Abc_NtkDfs( pNtk, 0 );
568 pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
569 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
570 {
571 Extra_ProgressBarUpdate( pProgress, i, NULL );
572 // get the node
573 assert( Abc_ObjIsNode(pNode) );
574 // strash the node
575 pNodeNew = Abc_NodeFraigTrust( pNtkNew, pNode );
576 // get the old object
577 if ( Abc_NtkIsNetlist(pNtk) )
578 pObj = Abc_ObjFanout0( pNode ); // the fanout net
579 else
580 pObj = pNode; // the node itself
581 // make sure the node is not yet strashed
582 assert( pObj->pCopy == NULL );
583 // mark the old object with the new AIG node
584 pObj->pCopy = pNodeNew;
585 }
586 Vec_PtrFree( vNodes );
587 Extra_ProgressBarStop( pProgress );
588 }
589
590 /**Function*************************************************************
591
592 Synopsis [Transforms one node into a FRAIG in the trust mode.]
593
594 Description []
595
596 SideEffects []
597
598 SeeAlso []
599
600 ***********************************************************************/
Abc_NodeFraigTrust(Abc_Ntk_t * pNtkNew,Abc_Obj_t * pNode)601 Abc_Obj_t * Abc_NodeFraigTrust( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode )
602 {
603 Abc_Obj_t * pSum, * pFanin;
604 void ** ppTail;
605 int i, nFanins, fCompl;
606
607 assert( Abc_ObjIsNode(pNode) );
608 // get the number of node's fanins
609 nFanins = Abc_ObjFaninNum( pNode );
610 assert( nFanins == Abc_SopGetVarNum((char *)pNode->pData) );
611 // check if it is a constant
612 if ( nFanins == 0 )
613 return Abc_ObjNotCond( Abc_AigConst1(pNtkNew), Abc_SopIsConst0((char *)pNode->pData) );
614 if ( nFanins == 1 )
615 return Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_SopIsInv((char *)pNode->pData) );
616 if ( nFanins == 2 && Abc_SopIsAndType((char *)pNode->pData) )
617 return Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc,
618 Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, !Abc_SopGetIthCareLit((char *)pNode->pData,0) ),
619 Abc_ObjNotCond( Abc_ObjFanin1(pNode)->pCopy, !Abc_SopGetIthCareLit((char *)pNode->pData,1) ) );
620 assert( Abc_SopIsOrType((char *)pNode->pData) );
621 fCompl = Abc_SopGetIthCareLit((char *)pNode->pData,0);
622 // get the root of the choice node (the first fanin)
623 pSum = Abc_ObjFanin0(pNode)->pCopy;
624 // connect other fanins
625 ppTail = &pSum->pData;
626 Abc_ObjForEachFanin( pNode, pFanin, i )
627 {
628 if ( i == 0 )
629 continue;
630 *ppTail = pFanin->pCopy;
631 ppTail = &pFanin->pCopy->pData;
632 // set the complemented bit of this cut
633 if ( fCompl ^ Abc_SopGetIthCareLit((char *)pNode->pData, i) )
634 pFanin->pCopy->fPhase = 1;
635 }
636 assert( *ppTail == NULL );
637 return pSum;
638 }
639
640
641
642
643 /**Function*************************************************************
644
645 Synopsis [Interfaces the network with the FRAIG package.]
646
647 Description []
648
649 SideEffects []
650
651 SeeAlso []
652
653 ***********************************************************************/
Abc_NtkFraigStore(Abc_Ntk_t * pNtkAdd)654 int Abc_NtkFraigStore( Abc_Ntk_t * pNtkAdd )
655 {
656 Vec_Ptr_t * vStore;
657 Abc_Ntk_t * pNtk;
658 // create the network to be stored
659 pNtk = Abc_NtkStrash( pNtkAdd, 0, 0, 0 );
660 if ( pNtk == NULL )
661 {
662 printf( "Abc_NtkFraigStore: Initial strashing has failed.\n" );
663 return 0;
664 }
665 // get the network currently stored
666 vStore = Abc_FrameReadStore();
667 if ( Vec_PtrSize(vStore) > 0 )
668 {
669 // check that the networks have the same PIs
670 extern int Abc_NodeCompareCiCo( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew );
671 if ( !Abc_NodeCompareCiCo(pNtk, (Abc_Ntk_t *)Vec_PtrEntry(vStore, 0)) )
672 {
673 // reorder PIs of pNtk2 according to pNtk1
674 if ( !Abc_NtkCompareSignals( pNtk, (Abc_Ntk_t *)Vec_PtrEntry(vStore, 0), 1, 1 ) )
675 {
676 printf( "Trying to store the network with different primary inputs.\n" );
677 printf( "The previously stored networks are deleted and this one is added.\n" );
678 Abc_NtkFraigStoreClean();
679 }
680 }
681 }
682 Vec_PtrPush( vStore, pNtk );
683 // printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pNtk) );
684 return 1;
685 }
686
687 /**Function*************************************************************
688
689 Synopsis [Interfaces the network with the FRAIG package.]
690
691 Description []
692
693 SideEffects []
694
695 SeeAlso []
696
697 ***********************************************************************/
Abc_NtkFraigRestore(int nPatsRand,int nPatsDyna,int nBTLimit)698 Abc_Ntk_t * Abc_NtkFraigRestore( int nPatsRand, int nPatsDyna, int nBTLimit )
699 {
700 extern Abc_Ntk_t * Abc_NtkFraigPartitioned( Vec_Ptr_t * vStore, void * pParams );
701 Fraig_Params_t Params;
702 Vec_Ptr_t * vStore;
703 Abc_Ntk_t * pNtk, * pFraig;
704 int nWords1, nWords2, nWordsMin;
705 // abctime clk = Abc_Clock();
706
707 // get the stored network
708 vStore = Abc_FrameReadStore();
709 if ( Vec_PtrSize(vStore) == 0 )
710 {
711 printf( "There are no network currently in storage.\n" );
712 return NULL;
713 }
714 // printf( "Currently stored %d networks will be fraiged.\n", Vec_PtrSize(vStore) );
715 pNtk = (Abc_Ntk_t *)Vec_PtrEntry( vStore, 0 );
716
717 // swap the first and last network
718 // this should lead to the primary choice being "better" because of synthesis
719 if ( Vec_PtrSize(vStore) > 1 )
720 {
721 pNtk = (Abc_Ntk_t *)Vec_PtrPop( vStore );
722 Vec_PtrPush( vStore, Vec_PtrEntry(vStore,0) );
723 Vec_PtrWriteEntry( vStore, 0, pNtk );
724 }
725
726 // to determine the number of simulation patterns
727 // use the following strategy
728 // at least 64 words (32 words random and 32 words dynamic)
729 // no more than 256M for one circuit (128M + 128M)
730 nWords1 = 32;
731 nWords2 = (1<<27) / (Abc_NtkNodeNum(pNtk) + Abc_NtkCiNum(pNtk));
732 nWordsMin = Abc_MinInt( nWords1, nWords2 );
733
734 // set parameters for fraiging
735 Fraig_ParamsSetDefault( &Params );
736 Params.nPatsRand = nPatsRand ? nPatsRand : nWordsMin * 32; // the number of words of random simulation info
737 Params.nPatsDyna = nPatsDyna ? nPatsDyna : nWordsMin * 32; // the number of words of dynamic simulation info
738 Params.nBTLimit = nBTLimit; // the max number of backtracks to perform
739 Params.fFuncRed = 1; // performs only one level hashing
740 Params.fFeedBack = 1; // enables solver feedback
741 Params.fDist1Pats = 1; // enables distance-1 patterns
742 Params.fDoSparse = 1; // performs equiv tests for sparse functions
743 Params.fChoicing = 1; // enables recording structural choices
744 Params.fTryProve = 0; // tries to solve the final miter
745 Params.fInternal = 1; // does not show progress bar
746 Params.fVerbose = 0; // the verbosiness flag
747
748 // perform partitioned computation of structural choices
749 pFraig = Abc_NtkFraigPartitioned( vStore, &Params );
750 Abc_NtkFraigStoreClean();
751 //ABC_PRT( "Total choicing time", Abc_Clock() - clk );
752 return pFraig;
753 }
754
755 /**Function*************************************************************
756
757 Synopsis [Interfaces the network with the FRAIG package.]
758
759 Description []
760
761 SideEffects []
762
763 SeeAlso []
764
765 ***********************************************************************/
Abc_NtkFraigStoreClean()766 void Abc_NtkFraigStoreClean()
767 {
768 Vec_Ptr_t * vStore;
769 Abc_Ntk_t * pNtk;
770 int i;
771 vStore = Abc_FrameReadStore();
772 Vec_PtrForEachEntry( Abc_Ntk_t *, vStore, pNtk, i )
773 Abc_NtkDelete( pNtk );
774 Vec_PtrClear( vStore );
775 }
776
777 /**Function*************************************************************
778
779 Synopsis [Checks the correctness of stored networks.]
780
781 Description []
782
783 SideEffects []
784
785 SeeAlso []
786
787 ***********************************************************************/
Abc_NtkFraigStoreCheck(Abc_Ntk_t * pFraig)788 void Abc_NtkFraigStoreCheck( Abc_Ntk_t * pFraig )
789 {
790 Abc_Obj_t * pNode0, * pNode1;
791 int nPoOrig, nPoFinal, nStored;
792 int i, k;
793 // check that the PO functions are correct
794 nPoFinal = Abc_NtkPoNum(pFraig);
795 nStored = Abc_FrameReadStoreSize();
796 assert( nPoFinal % nStored == 0 );
797 nPoOrig = nPoFinal / nStored;
798 for ( i = 0; i < nPoOrig; i++ )
799 {
800 pNode0 = Abc_ObjFanin0( Abc_NtkPo(pFraig, i) );
801 for ( k = 1; k < nStored; k++ )
802 {
803 pNode1 = Abc_ObjFanin0( Abc_NtkPo(pFraig, k*nPoOrig+i) );
804 if ( pNode0 != pNode1 )
805 printf( "Verification for PO #%d of network #%d has failed. The PO function is not used.\n", i+1, k+1 );
806 }
807 }
808 }
809
810 ////////////////////////////////////////////////////////////////////////
811 /// END OF FILE ///
812 ////////////////////////////////////////////////////////////////////////
813
814
815 ABC_NAMESPACE_IMPL_END
816
817