1 /**CFile****************************************************************
2
3 FileName [resCore.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Resynthesis package.]
8
9 Synopsis [Top-level resynthesis procedure.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - January 15, 2007.]
16
17 Revision [$Id: resCore.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "base/abc/abc.h"
22 #include "resInt.h"
23 #include "bool/kit/kit.h"
24 #include "sat/bsat/satStore.h"
25
26 ABC_NAMESPACE_IMPL_START
27
28
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32
33 typedef struct Res_Man_t_ Res_Man_t;
34 struct Res_Man_t_
35 {
36 // general parameters
37 Res_Par_t * pPars;
38 // specialized manager
39 Res_Win_t * pWin; // windowing manager
40 Abc_Ntk_t * pAig; // the strashed window
41 Res_Sim_t * pSim; // simulation manager
42 Sto_Man_t * pCnf; // the CNF of the SAT problem
43 Int_Man_t * pMan; // interpolation manager;
44 Vec_Int_t * vMem; // memory for intermediate SOPs
45 Vec_Vec_t * vResubs; // resubstitution candidates of the AIG
46 Vec_Vec_t * vResubsW; // resubstitution candidates of the window
47 Vec_Vec_t * vLevels; // levelized structure for updating
48 // statistics
49 int nWins; // the number of windows tried
50 int nWinNodes; // the total number of window nodes
51 int nDivNodes; // the total number of divisors
52 int nWinsTriv; // the total number of trivial windows
53 int nWinsUsed; // the total number of useful windows (with at least one candidate)
54 int nConstsUsed; // the total number of constant nodes under ODC
55 int nCandSets; // the total number of candidates
56 int nProvedSets; // the total number of proved groups
57 int nSimEmpty; // the empty simulation info
58 int nTotalNets; // the total number of nets
59 int nTotalNodes; // the total number of nodess
60 int nTotalNets2; // the total number of nets
61 int nTotalNodes2; // the total number of nodess
62 // runtime
63 abctime timeWin; // windowing
64 abctime timeDiv; // divisors
65 abctime timeAig; // strashing
66 abctime timeSim; // simulation
67 abctime timeCand; // resubstitution candidates
68 abctime timeSatTotal; // SAT solving total
69 abctime timeSatSat; // SAT solving (sat calls)
70 abctime timeSatUnsat; // SAT solving (unsat calls)
71 abctime timeSatSim; // SAT solving (simulation)
72 abctime timeInt; // interpolation
73 abctime timeUpd; // updating
74 abctime timeTotal; // total runtime
75 };
76
77 extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
78
79 extern abctime s_ResynTime;
80
81 ////////////////////////////////////////////////////////////////////////
82 /// FUNCTION DEFINITIONS ///
83 ////////////////////////////////////////////////////////////////////////
84
85 /**Function*************************************************************
86
87 Synopsis [Allocate resynthesis manager.]
88
89 Description []
90
91 SideEffects []
92
93 SeeAlso []
94
95 ***********************************************************************/
Res_ManAlloc(Res_Par_t * pPars)96 Res_Man_t * Res_ManAlloc( Res_Par_t * pPars )
97 {
98 Res_Man_t * p;
99 p = ABC_ALLOC( Res_Man_t, 1 );
100 memset( p, 0, sizeof(Res_Man_t) );
101 assert( pPars->nWindow > 0 && pPars->nWindow < 100 );
102 assert( pPars->nCands > 0 && pPars->nCands < 100 );
103 p->pPars = pPars;
104 p->pWin = Res_WinAlloc();
105 p->pSim = Res_SimAlloc( pPars->nSimWords );
106 p->pMan = Int_ManAlloc();
107 p->vMem = Vec_IntAlloc( 0 );
108 p->vResubs = Vec_VecStart( pPars->nCands );
109 p->vResubsW = Vec_VecStart( pPars->nCands );
110 p->vLevels = Vec_VecStart( 32 );
111 return p;
112 }
113
114 /**Function*************************************************************
115
116 Synopsis [Deallocate resynthesis manager.]
117
118 Description []
119
120 SideEffects []
121
122 SeeAlso []
123
124 ***********************************************************************/
Res_ManFree(Res_Man_t * p)125 void Res_ManFree( Res_Man_t * p )
126 {
127 if ( p->pPars->fVerbose )
128 {
129 printf( "Reduction in nodes = %5d. (%.2f %%) ",
130 p->nTotalNodes-p->nTotalNodes2,
131 100.0*(p->nTotalNodes-p->nTotalNodes2)/p->nTotalNodes );
132 printf( "Reduction in edges = %5d. (%.2f %%) ",
133 p->nTotalNets-p->nTotalNets2,
134 100.0*(p->nTotalNets-p->nTotalNets2)/p->nTotalNets );
135 printf( "\n" );
136
137 printf( "Winds = %d. ", p->nWins );
138 printf( "Nodes = %d. (Ave = %5.1f) ", p->nWinNodes, 1.0*p->nWinNodes/p->nWins );
139 printf( "Divs = %d. (Ave = %5.1f) ", p->nDivNodes, 1.0*p->nDivNodes/p->nWins );
140 printf( "\n" );
141 printf( "WinsTriv = %d. ", p->nWinsTriv );
142 printf( "SimsEmpt = %d. ", p->nSimEmpty );
143 printf( "Const = %d. ", p->nConstsUsed );
144 printf( "WindUsed = %d. ", p->nWinsUsed );
145 printf( "Cands = %d. ", p->nCandSets );
146 printf( "Proved = %d.", p->nProvedSets );
147 printf( "\n" );
148
149 ABC_PRTP( "Windowing ", p->timeWin, p->timeTotal );
150 ABC_PRTP( "Divisors ", p->timeDiv, p->timeTotal );
151 ABC_PRTP( "Strashing ", p->timeAig, p->timeTotal );
152 ABC_PRTP( "Simulation ", p->timeSim, p->timeTotal );
153 ABC_PRTP( "Candidates ", p->timeCand, p->timeTotal );
154 ABC_PRTP( "SAT solver ", p->timeSatTotal, p->timeTotal );
155 ABC_PRTP( " sat ", p->timeSatSat, p->timeTotal );
156 ABC_PRTP( " unsat ", p->timeSatUnsat, p->timeTotal );
157 ABC_PRTP( " simul ", p->timeSatSim, p->timeTotal );
158 ABC_PRTP( "Interpol ", p->timeInt, p->timeTotal );
159 ABC_PRTP( "Undating ", p->timeUpd, p->timeTotal );
160 ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
161 }
162 Res_WinFree( p->pWin );
163 if ( p->pAig ) Abc_NtkDelete( p->pAig );
164 Res_SimFree( p->pSim );
165 if ( p->pCnf ) Sto_ManFree( p->pCnf );
166 Int_ManFree( p->pMan );
167 Vec_IntFree( p->vMem );
168 Vec_VecFree( p->vResubs );
169 Vec_VecFree( p->vResubsW );
170 Vec_VecFree( p->vLevels );
171 ABC_FREE( p );
172 }
173
174 /**Function*************************************************************
175
176 Synopsis [Incrementally updates level of the nodes.]
177
178 Description []
179
180 SideEffects []
181
182 SeeAlso []
183
184 ***********************************************************************/
Res_UpdateNetwork(Abc_Obj_t * pObj,Vec_Ptr_t * vFanins,Hop_Obj_t * pFunc,Vec_Vec_t * vLevels)185 void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc, Vec_Vec_t * vLevels )
186 {
187 Abc_Obj_t * pObjNew, * pFanin;
188 int k;
189
190 // create the new node
191 pObjNew = Abc_NtkCreateNode( pObj->pNtk );
192 pObjNew->pData = pFunc;
193 Vec_PtrForEachEntry( Abc_Obj_t *, vFanins, pFanin, k )
194 Abc_ObjAddFanin( pObjNew, pFanin );
195 // replace the old node by the new node
196 //printf( "Replacing node " ); Abc_ObjPrint( stdout, pObj );
197 //printf( "Inserting node " ); Abc_ObjPrint( stdout, pObjNew );
198 // update the level of the node
199 Abc_NtkUpdate( pObj, pObjNew, vLevels );
200 }
201
202 /**Function*************************************************************
203
204 Synopsis [Entrace into the resynthesis package.]
205
206 Description []
207
208 SideEffects []
209
210 SeeAlso []
211
212 ***********************************************************************/
Abc_NtkResynthesize(Abc_Ntk_t * pNtk,Res_Par_t * pPars)213 int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars )
214 {
215 ProgressBar * pProgress;
216 Res_Man_t * p;
217 Abc_Obj_t * pObj;
218 Hop_Obj_t * pFunc;
219 Kit_Graph_t * pGraph;
220 Vec_Ptr_t * vFanins;
221 unsigned * puTruth;
222 int i, k, RetValue, nNodesOld, nFanins, nFaninsMax;
223 abctime clk, clkTotal = Abc_Clock();
224
225 // start the manager
226 p = Res_ManAlloc( pPars );
227 p->nTotalNets = Abc_NtkGetTotalFanins(pNtk);
228 p->nTotalNodes = Abc_NtkNodeNum(pNtk);
229 nFaninsMax = Abc_NtkGetFaninMax(pNtk);
230 if ( nFaninsMax > 8 )
231 nFaninsMax = 8;
232
233 // perform the network sweep
234 Abc_NtkSweep( pNtk, 0 );
235
236 // convert into the AIG
237 if ( !Abc_NtkToAig(pNtk) )
238 {
239 fprintf( stdout, "Converting to BDD has failed.\n" );
240 Res_ManFree( p );
241 return 0;
242 }
243 assert( Abc_NtkHasAig(pNtk) );
244
245 // set the number of levels
246 Abc_NtkLevel( pNtk );
247 Abc_NtkStartReverseLevels( pNtk, pPars->nGrowthLevel );
248
249 // try resynthesizing nodes in the topological order
250 nNodesOld = Abc_NtkObjNumMax(pNtk);
251 pProgress = Extra_ProgressBarStart( stdout, nNodesOld );
252 Abc_NtkForEachObj( pNtk, pObj, i )
253 {
254 Extra_ProgressBarUpdate( pProgress, i, NULL );
255 if ( !Abc_ObjIsNode(pObj) )
256 continue;
257 if ( Abc_ObjFaninNum(pObj) > 8 )
258 continue;
259 if ( pObj->Id > nNodesOld )
260 break;
261
262 // create the window for this node
263 clk = Abc_Clock();
264 RetValue = Res_WinCompute( pObj, p->pPars->nWindow/10, p->pPars->nWindow%10, p->pWin );
265 p->timeWin += Abc_Clock() - clk;
266 if ( !RetValue )
267 continue;
268 p->nWinsTriv += Res_WinIsTrivial( p->pWin );
269
270 if ( p->pPars->fVeryVerbose )
271 {
272 printf( "%5d (lev=%2d) : ", pObj->Id, pObj->Level );
273 printf( "Win = %3d/%3d/%4d/%3d ",
274 Vec_PtrSize(p->pWin->vLeaves),
275 Vec_PtrSize(p->pWin->vBranches),
276 Vec_PtrSize(p->pWin->vNodes),
277 Vec_PtrSize(p->pWin->vRoots) );
278 }
279
280 // collect the divisors
281 clk = Abc_Clock();
282 Res_WinDivisors( p->pWin, Abc_ObjRequiredLevel(pObj) - 1 );
283 p->timeDiv += Abc_Clock() - clk;
284
285 p->nWins++;
286 p->nWinNodes += Vec_PtrSize(p->pWin->vNodes);
287 p->nDivNodes += Vec_PtrSize( p->pWin->vDivs);
288
289 if ( p->pPars->fVeryVerbose )
290 {
291 printf( "D = %3d ", Vec_PtrSize(p->pWin->vDivs) );
292 printf( "D+ = %3d ", p->pWin->nDivsPlus );
293 }
294
295 // create the AIG for the window
296 clk = Abc_Clock();
297 if ( p->pAig ) Abc_NtkDelete( p->pAig );
298 p->pAig = Res_WndStrash( p->pWin );
299 p->timeAig += Abc_Clock() - clk;
300
301 if ( p->pPars->fVeryVerbose )
302 {
303 printf( "AIG = %4d ", Abc_NtkNodeNum(p->pAig) );
304 printf( "\n" );
305 }
306
307 // prepare simulation info
308 clk = Abc_Clock();
309 RetValue = Res_SimPrepare( p->pSim, p->pAig, Vec_PtrSize(p->pWin->vLeaves), 0 ); //p->pPars->fVerbose );
310 p->timeSim += Abc_Clock() - clk;
311 if ( !RetValue )
312 {
313 p->nSimEmpty++;
314 continue;
315 }
316
317 // consider the case of constant node
318 if ( p->pSim->fConst0 || p->pSim->fConst1 )
319 {
320 p->nConstsUsed++;
321
322 pFunc = p->pSim->fConst1? Hop_ManConst1((Hop_Man_t *)pNtk->pManFunc) : Hop_ManConst0((Hop_Man_t *)pNtk->pManFunc);
323 vFanins = Vec_VecEntry( p->vResubsW, 0 );
324 Vec_PtrClear( vFanins );
325 Res_UpdateNetwork( pObj, vFanins, pFunc, p->vLevels );
326 continue;
327 }
328
329 // printf( " " );
330
331 // find resub candidates for the node
332 clk = Abc_Clock();
333 if ( p->pPars->fArea )
334 RetValue = Res_FilterCandidates( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW, nFaninsMax, 1 );
335 else
336 RetValue = Res_FilterCandidates( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW, nFaninsMax, 0 );
337 p->timeCand += Abc_Clock() - clk;
338 p->nCandSets += RetValue;
339 if ( RetValue == 0 )
340 continue;
341
342 // printf( "%d(%d) ", Vec_PtrSize(p->pWin->vDivs), RetValue );
343
344 p->nWinsUsed++;
345
346 // iterate through candidate resubstitutions
347 Vec_VecForEachLevel( p->vResubs, vFanins, k )
348 {
349 if ( Vec_PtrSize(vFanins) == 0 )
350 break;
351
352 // solve the SAT problem and get clauses
353 clk = Abc_Clock();
354 if ( p->pCnf ) Sto_ManFree( p->pCnf );
355 p->pCnf = (Sto_Man_t *)Res_SatProveUnsat( p->pAig, vFanins );
356 if ( p->pCnf == NULL )
357 {
358 p->timeSatSat += Abc_Clock() - clk;
359 // printf( " Sat\n" );
360 // printf( "-" );
361 continue;
362 }
363 p->timeSatUnsat += Abc_Clock() - clk;
364 // printf( "+" );
365
366 p->nProvedSets++;
367 // printf( " Unsat\n" );
368 // continue;
369 // printf( "Proved %d.\n", k );
370
371 // write it into a file
372 // Sto_ManDumpClauses( p->pCnf, "trace.cnf" );
373
374 // interpolate the problem if it was UNSAT
375 clk = Abc_Clock();
376 nFanins = Int_ManInterpolate( p->pMan, p->pCnf, 0, &puTruth );
377 p->timeInt += Abc_Clock() - clk;
378 if ( nFanins != Vec_PtrSize(vFanins) - 2 )
379 continue;
380 assert( puTruth );
381 // Extra_PrintBinary( stdout, puTruth, 1 << nFanins ); printf( "\n" );
382
383 // transform interpolant into the AIG
384 pGraph = Kit_TruthToGraph( puTruth, nFanins, p->vMem );
385
386 // derive the AIG for the decomposition tree
387 pFunc = Kit_GraphToHop( (Hop_Man_t *)pNtk->pManFunc, pGraph );
388 Kit_GraphFree( pGraph );
389
390 // update the network
391 clk = Abc_Clock();
392 Res_UpdateNetwork( pObj, Vec_VecEntry(p->vResubsW, k), pFunc, p->vLevels );
393 p->timeUpd += Abc_Clock() - clk;
394 break;
395 }
396 // printf( "\n" );
397 }
398 Extra_ProgressBarStop( pProgress );
399 Abc_NtkStopReverseLevels( pNtk );
400
401 p->timeSatSim += p->pSim->timeSat;
402 p->timeSatTotal = p->timeSatSat + p->timeSatUnsat + p->timeSatSim;
403
404 p->nTotalNets2 = Abc_NtkGetTotalFanins(pNtk);
405 p->nTotalNodes2 = Abc_NtkNodeNum(pNtk);
406
407 // quit resubstitution manager
408 p->timeTotal = Abc_Clock() - clkTotal;
409 Res_ManFree( p );
410
411 s_ResynTime += Abc_Clock() - clkTotal;
412 // check the resulting network
413 if ( !Abc_NtkCheck( pNtk ) )
414 {
415 fprintf( stdout, "Abc_NtkResynthesize(): Network check has failed.\n" );
416 return 0;
417 }
418 return 1;
419 }
420
421 ////////////////////////////////////////////////////////////////////////
422 /// END OF FILE ///
423 ////////////////////////////////////////////////////////////////////////
424
425
426 ABC_NAMESPACE_IMPL_END
427
428