ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
abcRewrite.c
Go to the documentation of this file.
1
20
21#include "base/abc/abc.h"
22#include "opt/rwr/rwr.h"
23#include "bool/dec/dec.h"
24
26
27
28/*
29 The ideas realized in this package are inspired by the paper:
30 Per Bjesse, Arne Boralv, "DAG-aware circuit compression for
31 formal verification", Proc. ICCAD 2004, pp. 42-49.
32*/
33
37
38static Cut_Man_t * Abc_NtkStartCutManForRewrite( Abc_Ntk_t * pNtk );
39static void Abc_NodePrintCuts( Abc_Obj_t * pNode );
40static void Abc_ManShowCutCone( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves );
41
42extern void Abc_PlaceBegin( Abc_Ntk_t * pNtk );
43extern void Abc_PlaceEnd( Abc_Ntk_t * pNtk );
44extern void Abc_PlaceUpdate( Vec_Ptr_t * vAddedCells, Vec_Ptr_t * vUpdatedNets );
45
49
61int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose, int fVeryVerbose, int fPlaceEnable )
62{
63 extern int Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
64 ProgressBar * pProgress;
65 Cut_Man_t * pManCut;
66 Rwr_Man_t * pManRwr;
67 Abc_Obj_t * pNode;
68// Vec_Ptr_t * vAddedCells = NULL, * vUpdatedNets = NULL;
69 Dec_Graph_t * pGraph;
70 int i, nNodes, nGain, fCompl, RetValue = 1;
71 abctime clk, clkStart = Abc_Clock();
72
73 assert( Abc_NtkIsStrash(pNtk) );
74 // cleanup the AIG
76/*
77 {
78 Vec_Vec_t * vParts;
79 vParts = Abc_NtkPartitionSmart( pNtk, 50, 1 );
80 Vec_VecFree( vParts );
81 }
82*/
83
84 // start placement package
85// if ( fPlaceEnable )
86// {
87// Abc_PlaceBegin( pNtk );
88// vAddedCells = Abc_AigUpdateStart( pNtk->pManFunc, &vUpdatedNets );
89// }
90
91 // start the rewriting manager
92 pManRwr = Rwr_ManStart( 0 );
93 if ( pManRwr == NULL )
94 return 0;
95 // compute the reverse levels if level update is requested
96 if ( fUpdateLevel )
98 // start the cut manager
99clk = Abc_Clock();
100 pManCut = Abc_NtkStartCutManForRewrite( pNtk );
101Rwr_ManAddTimeCuts( pManRwr, Abc_Clock() - clk );
102 pNtk->pManCut = pManCut;
103
104 if ( fVeryVerbose )
105 Rwr_ScoresClean( pManRwr );
106
107 // resynthesize each node once
108 pManRwr->nNodesBeg = Abc_NtkNodeNum(pNtk);
109 nNodes = Abc_NtkObjNumMax(pNtk);
110 pProgress = Extra_ProgressBarStart( stdout, nNodes );
111 Abc_NtkForEachNode( pNtk, pNode, i )
112 {
113 Extra_ProgressBarUpdate( pProgress, i, NULL );
114 // stop if all nodes have been tried once
115 if ( i >= nNodes )
116 break;
117 // skip persistant nodes
118 if ( Abc_NodeIsPersistant(pNode) )
119 continue;
120 // skip the nodes with many fanouts
121 if ( Abc_ObjFanoutNum(pNode) > 1000 )
122 continue;
123
124 // for each cut, try to resynthesize it
125 nGain = Rwr_NodeRewrite( pManRwr, pManCut, pNode, fUpdateLevel, fUseZeros, fPlaceEnable );
126 if ( !(nGain > 0 || (nGain == 0 && fUseZeros)) )
127 continue;
128 // if we end up here, a rewriting step is accepted
129
130 // get hold of the new subgraph to be added to the AIG
131 pGraph = (Dec_Graph_t *)Rwr_ManReadDecs(pManRwr);
132 fCompl = Rwr_ManReadCompl(pManRwr);
133
134 // reset the array of the changed nodes
135 if ( fPlaceEnable )
137
138 // complement the FF if needed
139 if ( fCompl ) Dec_GraphComplement( pGraph );
140clk = Abc_Clock();
141 if ( !Dec_GraphUpdateNetwork( pNode, pGraph, fUpdateLevel, nGain ) )
142 {
143 RetValue = -1;
144 break;
145 }
146Rwr_ManAddTimeUpdate( pManRwr, Abc_Clock() - clk );
147 if ( fCompl ) Dec_GraphComplement( pGraph );
148
149 // use the array of changed nodes to update placement
150// if ( fPlaceEnable )
151// Abc_PlaceUpdate( vAddedCells, vUpdatedNets );
152 }
153 Extra_ProgressBarStop( pProgress );
154Rwr_ManAddTimeTotal( pManRwr, Abc_Clock() - clkStart );
155 // print stats
156 pManRwr->nNodesEnd = Abc_NtkNodeNum(pNtk);
157 if ( fVerbose )
158 Rwr_ManPrintStats( pManRwr );
159// Rwr_ManPrintStatsFile( pManRwr );
160 if ( fVeryVerbose )
161 Rwr_ScoresReport( pManRwr );
162 // delete the managers
163 Rwr_ManStop( pManRwr );
164 Cut_ManStop( pManCut );
165 pNtk->pManCut = NULL;
166
167 // start placement package
168// if ( fPlaceEnable )
169// {
170// Abc_PlaceEnd( pNtk );
171// Abc_AigUpdateStop( pNtk->pManFunc );
172// }
173
174 // put the nodes into the DFS order and reassign their IDs
175 {
176// abctime clk = Abc_Clock();
177 Abc_NtkReassignIds( pNtk );
178// ABC_PRT( "time", Abc_Clock() - clk );
179 }
180// Abc_AigCheckFaninOrder( pNtk->pManFunc );
181 // fix the levels
182 if ( RetValue >= 0 )
183 {
184 if ( fUpdateLevel )
186 else
187 Abc_NtkLevel( pNtk );
188 // check
189 if ( !Abc_NtkCheck( pNtk ) )
190 {
191 printf( "Abc_NtkRewrite: The network check has failed.\n" );
192 return 0;
193 }
194 }
195 return RetValue;
196}
197
198
210Cut_Man_t * Abc_NtkStartCutManForRewrite( Abc_Ntk_t * pNtk )
211{
212 static Cut_Params_t Params, * pParams = &Params;
213 Cut_Man_t * pManCut;
214 Abc_Obj_t * pObj;
215 int i;
216 // start the cut manager
217 memset( pParams, 0, sizeof(Cut_Params_t) );
218 pParams->nVarsMax = 4; // the max cut size ("k" of the k-feasible cuts)
219 pParams->nKeepMax = 250; // the max number of cuts kept at a node
220 pParams->fTruth = 1; // compute truth tables
221 pParams->fFilter = 1; // filter dominated cuts
222 pParams->fSeq = 0; // compute sequential cuts
223 pParams->fDrop = 0; // drop cuts on the fly
224 pParams->fVerbose = 0; // the verbosiness flag
225 pParams->nIdsMax = Abc_NtkObjNumMax( pNtk );
226 pManCut = Cut_ManStart( pParams );
227 if ( pParams->fDrop )
229 // set cuts for PIs
230 Abc_NtkForEachCi( pNtk, pObj, i )
231 if ( Abc_ObjFanoutNum(pObj) > 0 )
232 Cut_NodeSetTriv( pManCut, pObj->Id );
233 return pManCut;
234}
235
248{
249 Vec_Ptr_t * vCuts;
250 Cut_Cut_t * pCut;
251 int k;
252
253 printf( "\nNode %s\n", Abc_ObjName(pNode) );
254 vCuts = (Vec_Ptr_t *)pNode->pCopy;
255 Vec_PtrForEachEntry( Cut_Cut_t *, vCuts, pCut, k )
256 {
257 Extra_PrintBinary( stdout, (unsigned *)&pCut->uSign, 16 );
258 printf( " " );
259 Cut_CutPrint( pCut, 0 );
260 printf( "\n" );
261 }
262}
263
264
276void Abc_ManRewritePrintDivs( Vec_Ptr_t * vDivs, int nLeaves )
277{
278 Abc_Obj_t * pFanin, * pNode, * pRoot;
279 int i, k;
280 pRoot = (Abc_Obj_t *)Vec_PtrEntryLast(vDivs);
281 // print the nodes
282 Vec_PtrForEachEntry( Abc_Obj_t *, vDivs, pNode, i )
283 {
284 if ( i < nLeaves )
285 {
286 printf( "%6d : %c\n", pNode->Id, 'a'+i );
287 continue;
288 }
289 printf( "%6d : %2d = ", pNode->Id, i );
290 // find the first fanin
291 Vec_PtrForEachEntry( Abc_Obj_t *, vDivs, pFanin, k )
292 if ( Abc_ObjFanin0(pNode) == pFanin )
293 break;
294 if ( k < nLeaves )
295 printf( "%c", 'a' + k );
296 else
297 printf( "%d", k );
298 printf( "%s ", Abc_ObjFaninC0(pNode)? "\'" : "" );
299 // find the second fanin
300 Vec_PtrForEachEntry( Abc_Obj_t *, vDivs, pFanin, k )
301 if ( Abc_ObjFanin1(pNode) == pFanin )
302 break;
303 if ( k < nLeaves )
304 printf( "%c", 'a' + k );
305 else
306 printf( "%d", k );
307 printf( "%s ", Abc_ObjFaninC1(pNode)? "\'" : "" );
308 if ( pNode == pRoot )
309 printf( " root" );
310 printf( "\n" );
311 }
312 printf( "\n" );
313}
314
327{
328 if ( Abc_NodeIsTravIdCurrent(pNode) )
329 return;
330 Abc_NodeSetTravIdCurrent(pNode);
331 Abc_ManShowCutCone_rec( Abc_ObjFanin0(pNode), vDivs );
332 Abc_ManShowCutCone_rec( Abc_ObjFanin1(pNode), vDivs );
333 Vec_PtrPush( vDivs, pNode );
334}
335
347void Abc_ManShowCutCone( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves )
348{
349 Abc_Ntk_t * pNtk = pNode->pNtk;
350 Abc_Obj_t * pObj;
351 Vec_Ptr_t * vDivs;
352 int i;
353 vDivs = Vec_PtrAlloc( 100 );
354 Abc_NtkIncrementTravId( pNtk );
355 Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pObj, i )
356 {
357 Abc_NodeSetTravIdCurrent( Abc_ObjRegular(pObj) );
358 Vec_PtrPush( vDivs, Abc_ObjRegular(pObj) );
359 }
360 Abc_ManShowCutCone_rec( pNode, vDivs );
361 Abc_ManRewritePrintDivs( vDivs, Vec_PtrSize(vLeaves) );
362 Vec_PtrFree( vDivs );
363}
364
365
377void Abc_RwrExpWithCut_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, int fUseA )
378{
379 if ( Vec_PtrFind(vLeaves, pNode) >= 0 || Vec_PtrFind(vLeaves, Abc_ObjNot(pNode)) >= 0 )
380 {
381 if ( fUseA )
382 Abc_ObjRegular(pNode)->fMarkA = 1;
383 else
384 Abc_ObjRegular(pNode)->fMarkB = 1;
385 return;
386 }
387 assert( Abc_ObjIsNode(pNode) );
388 Abc_RwrExpWithCut_rec( Abc_ObjFanin0(pNode), vLeaves, fUseA );
389 Abc_RwrExpWithCut_rec( Abc_ObjFanin1(pNode), vLeaves, fUseA );
390}
391
403void Abc_RwrExpWithCut( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves )
404{
405 Abc_Obj_t * pObj;
406 int i, CountA, CountB;
407 Abc_RwrExpWithCut_rec( Abc_ObjFanin0(pNode), vLeaves, 1 );
408 Abc_RwrExpWithCut_rec( Abc_ObjFanin1(pNode), vLeaves, 0 );
409 CountA = CountB = 0;
410 Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pObj, i )
411 {
412 CountA += Abc_ObjRegular(pObj)->fMarkA;
413 CountB += Abc_ObjRegular(pObj)->fMarkB;
414 Abc_ObjRegular(pObj)->fMarkA = 0;
415 Abc_ObjRegular(pObj)->fMarkB = 0;
416 }
417 printf( "(%d,%d:%d) ", CountA, CountB, CountA+CountB-Vec_PtrSize(vLeaves) );
418}
419
420
424
425
427
void Abc_NodePrintCuts(Abc_Obj_t *pNode)
Definition abcRewrite.c:247
void Abc_ManShowCutCone(Abc_Obj_t *pNode, Vec_Ptr_t *vLeaves)
Definition abcRewrite.c:347
int Dec_GraphUpdateNetwork(Abc_Obj_t *pRoot, Dec_Graph_t *pGraph, int fUpdateLevel, int nGain)
Definition decAbc.c:240
void Abc_RwrExpWithCut_rec(Abc_Obj_t *pNode, Vec_Ptr_t *vLeaves, int fUseA)
Definition abcRewrite.c:377
void Abc_PlaceUpdate(Vec_Ptr_t *vAddedCells, Vec_Ptr_t *vUpdatedNets)
Definition abcPlace.c:126
void Abc_RwrExpWithCut(Abc_Obj_t *pNode, Vec_Ptr_t *vLeaves)
Definition abcRewrite.c:403
void Abc_ManRewritePrintDivs(Vec_Ptr_t *vDivs, int nLeaves)
Definition abcRewrite.c:276
void Abc_ManShowCutCone_rec(Abc_Obj_t *pNode, Vec_Ptr_t *vDivs)
Definition abcRewrite.c:326
int Abc_NtkRewrite(Abc_Ntk_t *pNtk, int fUpdateLevel, int fUseZeros, int fVerbose, int fVeryVerbose, int fPlaceEnable)
FUNCTION DEFINITIONS ///.
Definition abcRewrite.c:61
void Abc_PlaceBegin(Abc_Ntk_t *pNtk)
Definition abcPlace.c:178
void Abc_PlaceEnd(Abc_Ntk_t *pNtk)
Definition abcPlace.c:241
struct Abc_Obj_t_ Abc_Obj_t
Definition abc.h:116
ABC_DLL void Abc_AigUpdateReset(Abc_Aig_t *pMan)
Definition abcAig.c:1477
ABC_DLL int Abc_NtkCheck(Abc_Ntk_t *pNtk)
FUNCTION DEFINITIONS ///.
Definition abcCheck.c:64
struct Abc_Aig_t_ Abc_Aig_t
Definition abc.h:117
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
Definition abcNames.c:49
struct Abc_Ntk_t_ Abc_Ntk_t
Definition abc.h:115
ABC_DLL void Abc_NtkStopReverseLevels(Abc_Ntk_t *pNtk)
Definition abcTiming.c:1302
ABC_DLL Vec_Int_t * Abc_NtkFanoutCounts(Abc_Ntk_t *pNtk)
Definition abcUtil.c:1741
ABC_DLL int Abc_NtkLevel(Abc_Ntk_t *pNtk)
Definition abcDfs.c:1449
ABC_DLL int Abc_AigCleanup(Abc_Aig_t *pMan)
Definition abcAig.c:194
ABC_DLL void Abc_NtkStartReverseLevels(Abc_Ntk_t *pNtk, int nMaxLevelIncrease)
Definition abcTiming.c:1274
#define Abc_NtkForEachCi(pNtk, pCi, i)
Definition abc.h:518
ABC_DLL void Abc_NtkReassignIds(Abc_Ntk_t *pNtk)
Definition abcUtil.c:1809
#define Abc_NtkForEachNode(pNtk, pNode, i)
Definition abc.h:464
ABC_INT64_T abctime
Definition abc_global.h:332
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
ABC_NAMESPACE_IMPL_START typedef char ProgressBar
Definition bbrNtbdd.c:27
struct Cut_ParamsStruct_t_ Cut_Params_t
Definition cut.h:51
void Cut_NodeSetTriv(Cut_Man_t *p, int Node)
Definition cutApi.c:145
Cut_Man_t * Cut_ManStart(Cut_Params_t *pParams)
FUNCTION DEFINITIONS ///.
Definition cutMan.c:47
struct Cut_ManStruct_t_ Cut_Man_t
BASIC TYPES ///.
Definition cut.h:48
void Cut_CutPrint(Cut_Cut_t *pCut, int fSeq)
Definition cutCut.c:276
void Cut_ManSetFanoutCounts(Cut_Man_t *p, Vec_Int_t *vFanCounts)
Definition cutMan.c:229
struct Cut_CutStruct_t_ Cut_Cut_t
Definition cut.h:50
void Cut_ManStop(Cut_Man_t *p)
Definition cutMan.c:124
struct Dec_Graph_t_ Dec_Graph_t
Definition dec.h:68
void Extra_ProgressBarStop(ProgressBar *p)
ProgressBar * Extra_ProgressBarStart(FILE *pFile, int nItemsTotal)
FUNCTION DEFINITIONS ///.
void Extra_PrintBinary(FILE *pFile, unsigned Sign[], int nBits)
void Rwr_ManAddTimeUpdate(Rwr_Man_t *p, abctime Time)
Definition rwrMan.c:277
Rwr_Man_t * Rwr_ManStart(int fPrecompute)
DECLARATIONS ///.
Definition rwrMan.c:47
void Rwr_ScoresClean(Rwr_Man_t *p)
Definition rwrEva.c:504
void Rwr_ManAddTimeCuts(Rwr_Man_t *p, abctime Time)
Definition rwrMan.c:261
void Rwr_ManAddTimeTotal(Rwr_Man_t *p, abctime Time)
Definition rwrMan.c:293
void Rwr_ScoresReport(Rwr_Man_t *p)
Definition rwrEva.c:550
int Rwr_ManReadCompl(Rwr_Man_t *p)
Definition rwrMan.c:245
void Rwr_ManPrintStats(Rwr_Man_t *p)
Definition rwrMan.c:143
struct Rwr_Man_t_ Rwr_Man_t
Definition rwr.h:47
void Rwr_ManStop(Rwr_Man_t *p)
Definition rwrMan.c:109
int Rwr_NodeRewrite(Rwr_Man_t *p, Cut_Man_t *pManCut, Abc_Obj_t *pNode, int fUpdateLevel, int fUseZeros, int fPlaceEnable)
FUNCTION DEFINITIONS ///.
Definition rwrEva.c:59
void * Rwr_ManReadDecs(Rwr_Man_t *p)
Definition rwrMan.c:213
void * pManFunc
Definition abc.h:191
void * pManCut
Definition abc.h:193
Abc_Ntk_t * pNtk
Definition abc.h:130
int Id
Definition abc.h:132
Abc_Obj_t * pCopy
Definition abc.h:148
unsigned uSign
Definition cut.h:85
int nNodesBeg
Definition rwr.h:82
int nNodesEnd
Definition rwr.h:83
#define assert(ex)
Definition util_old.h:213
char * memset()
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