1 /**CFile****************************************************************
2
3 FileName [sswCore.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Inductive prover with constraints.]
8
9 Synopsis [The core procedures.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - September 1, 2008.]
16
17 Revision [$Id: sswCore.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "sswInt.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33
34 /**Function*************************************************************
35
36 Synopsis [This procedure sets default parameters.]
37
38 Description []
39
40 SideEffects []
41
42 SeeAlso []
43
44 ***********************************************************************/
Ssw_ManSetDefaultParams(Ssw_Pars_t * p)45 void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
46 {
47 memset( p, 0, sizeof(Ssw_Pars_t) );
48 p->nPartSize = 0; // size of the partition
49 p->nOverSize = 0; // size of the overlap between partitions
50 p->nFramesK = 1; // the induction depth
51 p->nFramesAddSim = 2; // additional frames to simulate
52 p->fConstrs = 0; // treat the last nConstrs POs as seq constraints
53 p->fMergeFull = 0; // enables full merge when constraints are used
54 p->nBTLimit = 1000; // conflict limit at a node
55 p->nBTLimitGlobal = 5000000; // conflict limit for all runs
56 p->nMinDomSize = 100; // min clock domain considered for optimization
57 p->nItersStop = -1; // stop after the given number of iterations
58 p->nResimDelta = 1000; // the internal of nodes to resimulate
59 p->nStepsMax = -1; // (scorr only) the max number of induction steps
60 p->fPolarFlip = 0; // uses polarity adjustment
61 p->fLatchCorr = 0; // performs register correspondence
62 p->fConstCorr = 0; // performs constant correspondence
63 p->fOutputCorr = 0; // perform 'PO correspondence'
64 p->fSemiFormal = 0; // enable semiformal filtering
65 p->fDynamic = 0; // dynamic partitioning
66 p->fLocalSim = 0; // local simulation
67 p->fVerbose = 0; // verbose stats
68 p->fEquivDump = 0; // enables dumping equivalences
69 p->fEquivDump2 = 0; // enables dumping equivalences
70
71 // latch correspondence
72 p->fLatchCorrOpt = 0; // performs optimized register correspondence
73 p->nSatVarMax = 1000; // the max number of SAT variables
74 p->nRecycleCalls = 50; // calls to perform before recycling SAT solver
75 // signal correspondence
76 p->nSatVarMax2 = 5000; // the max number of SAT variables
77 p->nRecycleCalls2 = 250; // calls to perform before recycling SAT solver
78 // return values
79 p->nIters = 0; // the number of iterations performed
80 }
81
82 /**Function*************************************************************
83
84 Synopsis [This procedure sets default parameters.]
85
86 Description []
87
88 SideEffects []
89
90 SeeAlso []
91
92 ***********************************************************************/
Ssw_ManSetDefaultParamsLcorr(Ssw_Pars_t * p)93 void Ssw_ManSetDefaultParamsLcorr( Ssw_Pars_t * p )
94 {
95 Ssw_ManSetDefaultParams( p );
96 p->fLatchCorrOpt = 1;
97 p->nBTLimit = 10000;
98 }
99
100 /**Function*************************************************************
101
102 Synopsis [Reports improvements for property cones.]
103
104 Description []
105
106 SideEffects []
107
108 SeeAlso []
109
110 ***********************************************************************/
Ssw_ReportConeReductions(Ssw_Man_t * p,Aig_Man_t * pAigInit,Aig_Man_t * pAigStop)111 void Ssw_ReportConeReductions( Ssw_Man_t * p, Aig_Man_t * pAigInit, Aig_Man_t * pAigStop )
112 {
113 Aig_Man_t * pAig1, * pAig2, * pAux;
114 pAig1 = Aig_ManDupOneOutput( pAigInit, 0, 1 );
115 pAig1 = Aig_ManScl( pAux = pAig1, 1, 1, 0, -1, -1, 0, 0 );
116 Aig_ManStop( pAux );
117 pAig2 = Aig_ManDupOneOutput( pAigStop, 0, 1 );
118 pAig2 = Aig_ManScl( pAux = pAig2, 1, 1, 0, -1, -1, 0, 0 );
119 Aig_ManStop( pAux );
120
121 p->nNodesBegC = Aig_ManNodeNum(pAig1);
122 p->nNodesEndC = Aig_ManNodeNum(pAig2);
123 p->nRegsBegC = Aig_ManRegNum(pAig1);
124 p->nRegsEndC = Aig_ManRegNum(pAig2);
125
126 Aig_ManStop( pAig1 );
127 Aig_ManStop( pAig2 );
128 }
129
130 /**Function*************************************************************
131
132 Synopsis [Reports one node.]
133
134 Description []
135
136 SideEffects []
137
138 SeeAlso []
139
140 ***********************************************************************/
Ssw_ReportOneOutput(Aig_Man_t * p,Aig_Obj_t * pObj)141 void Ssw_ReportOneOutput( Aig_Man_t * p, Aig_Obj_t * pObj )
142 {
143 if ( pObj == Aig_ManConst1(p) )
144 Abc_Print( 1, "1" );
145 else if ( pObj == Aig_ManConst0(p) )
146 Abc_Print( 1, "0" );
147 else
148 Abc_Print( 1, "X" );
149 }
150
151 /**Function*************************************************************
152
153 Synopsis [Reports improvements for property cones.]
154
155 Description []
156
157 SideEffects []
158
159 SeeAlso []
160
161 ***********************************************************************/
Ssw_ReportOutputs(Aig_Man_t * pAig)162 void Ssw_ReportOutputs( Aig_Man_t * pAig )
163 {
164 Aig_Obj_t * pObj;
165 int i;
166 Saig_ManForEachPo( pAig, pObj, i )
167 {
168 if ( i < Saig_ManPoNum(pAig)-Saig_ManConstrNum(pAig) )
169 Abc_Print( 1, "o" );
170 else
171 Abc_Print( 1, "c" );
172 Ssw_ReportOneOutput( pAig, Aig_ObjChild0(pObj) );
173 }
174 Abc_Print( 1, "\n" );
175 }
176
177 /**Function*************************************************************
178
179 Synopsis [Remove from-equivs that are in the cone of constraints.]
180
181 Description []
182
183 SideEffects []
184
185 SeeAlso []
186
187 ***********************************************************************/
Ssw_ManUpdateEquivs(Ssw_Man_t * p,Aig_Man_t * pAig,int fVerbose)188 void Ssw_ManUpdateEquivs( Ssw_Man_t * p, Aig_Man_t * pAig, int fVerbose )
189 {
190 Vec_Ptr_t * vCones;
191 Aig_Obj_t ** pArray;
192 Aig_Obj_t * pObj;
193 int i, nTotal = 0, nRemoved = 0;
194 // collect the nodes in the cone of constraints
195 pArray = (Aig_Obj_t **)Vec_PtrArray(pAig->vCos);
196 pArray += Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig);
197 vCones = Aig_ManDfsNodes( pAig, pArray, Saig_ManConstrNum(pAig) );
198 // remove all the node that are equiv to something and are in the cones
199 Aig_ManForEachObj( pAig, pObj, i )
200 {
201 if ( !Aig_ObjIsCi(pObj) && !Aig_ObjIsNode(pObj) )
202 continue;
203 if ( pAig->pReprs[i] != NULL )
204 nTotal++;
205 if ( !Aig_ObjIsTravIdCurrent(pAig, pObj) )
206 continue;
207 if ( pAig->pReprs[i] )
208 {
209 if ( p->pPars->fConstrs && !p->pPars->fMergeFull )
210 {
211 pAig->pReprs[i] = NULL;
212 nRemoved++;
213 }
214 }
215 }
216 // collect statistics
217 p->nConesTotal = Aig_ManCiNum(pAig) + Aig_ManNodeNum(pAig);
218 p->nConesConstr = Vec_PtrSize(vCones);
219 p->nEquivsTotal = nTotal;
220 p->nEquivsConstr = nRemoved;
221 Vec_PtrFree( vCones );
222 }
223
224 /**Function*************************************************************
225
226 Synopsis [Performs computation of signal correspondence with constraints.]
227
228 Description []
229
230 SideEffects []
231
232 SeeAlso []
233
234 ***********************************************************************/
Ssw_SignalCorrespondenceRefine(Ssw_Man_t * p)235 Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
236 {
237 int nSatProof, nSatCallsSat, nRecycles, nSatFailsReal, nUniques;
238 Aig_Man_t * pAigNew;
239 int RetValue, nIter = -1;
240 abctime clk, clkTotal = Abc_Clock();
241 // get the starting stats
242 p->nLitsBeg = Ssw_ClassesLitNum( p->ppClasses );
243 p->nNodesBeg = Aig_ManNodeNum(p->pAig);
244 p->nRegsBeg = Aig_ManRegNum(p->pAig);
245 // refine classes using BMC
246 if ( p->pPars->fVerbose )
247 {
248 Abc_Print( 1, "Before BMC: " );
249 Ssw_ClassesPrint( p->ppClasses, 0 );
250 }
251 if ( !p->pPars->fLatchCorr || p->pPars->nFramesK > 1 )
252 {
253 p->pMSat = Ssw_SatStart( 0 );
254 if ( p->pPars->fConstrs )
255 Ssw_ManSweepBmcConstr( p );
256 else
257 Ssw_ManSweepBmc( p );
258 Ssw_SatStop( p->pMSat );
259 p->pMSat = NULL;
260 Ssw_ManCleanup( p );
261 }
262 if ( p->pPars->fVerbose )
263 {
264 Abc_Print( 1, "After BMC: " );
265 Ssw_ClassesPrint( p->ppClasses, 0 );
266 }
267 // apply semi-formal filtering
268 /*
269 if ( p->pPars->fSemiFormal )
270 {
271 Aig_Man_t * pSRed;
272 Ssw_FilterUsingSemi( p, 0, 2000, p->pPars->fVerbose );
273 // Ssw_FilterUsingSemi( p, 1, 100000, p->pPars->fVerbose );
274 pSRed = Ssw_SpeculativeReduction( p );
275 Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL );
276 Aig_ManStop( pSRed );
277 }
278 */
279 if ( p->pPars->pFunc )
280 {
281 ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData );
282 ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData );
283 }
284 if ( p->pPars->nStepsMax == 0 )
285 {
286 Abc_Print( 1, "Stopped signal correspondence after BMC.\n" );
287 goto finalize;
288 }
289 // refine classes using induction
290 nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = nUniques = 0;
291 for ( nIter = 0; ; nIter++ )
292 {
293 if ( p->pPars->nStepsMax == nIter )
294 {
295 Abc_Print( 1, "Stopped signal correspondence after %d refiment iterations.\n", nIter );
296 goto finalize;
297 }
298 if ( p->pPars->nItersStop >= 0 && p->pPars->nItersStop == nIter )
299 {
300 Aig_Man_t * pSRed = Ssw_SpeculativeReduction( p );
301 Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL );
302 Aig_ManStop( pSRed );
303 Abc_Print( 1, "Iterative refinement is stopped before iteration %d.\n", nIter );
304 Abc_Print( 1, "The network is reduced using candidate equivalences.\n" );
305 Abc_Print( 1, "Speculatively reduced miter is saved in file \"%s\".\n", "srm.blif" );
306 Abc_Print( 1, "If the miter is SAT, the reduced result is incorrect.\n" );
307 break;
308 }
309
310 clk = Abc_Clock();
311 p->pMSat = Ssw_SatStart( 0 );
312 if ( p->pPars->fLatchCorrOpt )
313 {
314 RetValue = Ssw_ManSweepLatch( p );
315 if ( p->pPars->fVerbose )
316 {
317 Abc_Print( 1, "%3d : C =%7d. Cl =%7d. Pr =%6d. Cex =%5d. R =%4d. F =%4d. ",
318 nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
319 p->nSatProof-nSatProof, p->nSatCallsSat-nSatCallsSat,
320 p->nRecycles-nRecycles, p->nSatFailsReal-nSatFailsReal );
321 ABC_PRT( "T", Abc_Clock() - clk );
322 }
323 }
324 else
325 {
326 if ( p->pPars->fConstrs )
327 RetValue = Ssw_ManSweepConstr( p );
328 else if ( p->pPars->fDynamic )
329 RetValue = Ssw_ManSweepDyn( p );
330 else
331 RetValue = Ssw_ManSweep( p );
332
333 p->pPars->nConflicts += p->pMSat->pSat->stats.conflicts;
334 if ( p->pPars->fVerbose )
335 {
336 Abc_Print( 1, "%3d : C =%7d. Cl =%7d. LR =%6d. NR =%6d. ",
337 nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
338 p->nConstrReduced, Aig_ManNodeNum(p->pFrames) );
339 if ( p->pPars->fDynamic )
340 {
341 Abc_Print( 1, "Cex =%5d. ", p->nSatCallsSat-nSatCallsSat );
342 Abc_Print( 1, "R =%4d. ", p->nRecycles-nRecycles );
343 }
344 Abc_Print( 1, "F =%5d. %s ", p->nSatFailsReal-nSatFailsReal,
345 (Saig_ManPoNum(p->pAig)==1 && Ssw_ObjIsConst1Cand(p->pAig,Aig_ObjFanin0(Aig_ManCo(p->pAig,0))))? "+" : "-" );
346 ABC_PRT( "T", Abc_Clock() - clk );
347 }
348 // if ( p->pPars->fDynamic && p->nSatCallsSat-nSatCallsSat < 100 )
349 // p->pPars->nBTLimit = 10000;
350
351 if ( p->pPars->fStopWhenGone && Saig_ManPoNum(p->pAig) == 1 && !Ssw_ObjIsConst1Cand(p->pAig,Aig_ObjFanin0(Aig_ManCo(p->pAig,0))) )
352 {
353 printf( "Iterative refinement is stopped after iteration %d\n", nIter );
354 printf( "because the property output is no longer a candidate constant.\n" );
355 // prepare to quite
356 p->nLitsEnd = p->nLitsBeg;
357 p->nNodesEnd = p->nNodesBeg;
358 p->nRegsEnd = p->nRegsBeg;
359 // cleanup
360 Ssw_SatStop( p->pMSat );
361 p->pMSat = NULL;
362 Ssw_ManCleanup( p );
363 // cleanup
364 Aig_ManSetPhase( p->pAig );
365 Aig_ManCleanMarkB( p->pAig );
366 return Aig_ManDupSimple( p->pAig );
367 }
368 }
369 nSatProof = p->nSatProof;
370 nSatCallsSat = p->nSatCallsSat;
371 nRecycles = p->nRecycles;
372 nSatFailsReal = p->nSatFailsReal;
373 nUniques = p->nUniques;
374
375 p->nVarsMax = Abc_MaxInt( p->nVarsMax, p->pMSat->nSatVars );
376 p->nCallsMax = Abc_MaxInt( p->nCallsMax, p->pMSat->nSolverCalls );
377 Ssw_SatStop( p->pMSat );
378 p->pMSat = NULL;
379 Ssw_ManCleanup( p );
380 if ( !RetValue )
381 break;
382 if ( p->pPars->pFunc )
383 ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData );
384 }
385
386 finalize:
387 p->pPars->nIters = nIter + 1;
388 p->timeTotal = Abc_Clock() - clkTotal;
389
390 Ssw_ManUpdateEquivs( p, p->pAig, p->pPars->fVerbose );
391 pAigNew = Aig_ManDupRepr( p->pAig, 0 );
392 Aig_ManSeqCleanup( pAigNew );
393 //Ssw_ClassesPrint( p->ppClasses, 1 );
394 // get the final stats
395 p->nLitsEnd = Ssw_ClassesLitNum( p->ppClasses );
396 p->nNodesEnd = Aig_ManNodeNum(pAigNew);
397 p->nRegsEnd = Aig_ManRegNum(pAigNew);
398 // cleanup
399 Aig_ManSetPhase( p->pAig );
400 Aig_ManCleanMarkB( p->pAig );
401 return pAigNew;
402 }
403
404 /**Function*************************************************************
405
406 Synopsis [Performs computation of signal correspondence with constraints.]
407
408 Description []
409
410 SideEffects []
411
412 SeeAlso []
413
414 ***********************************************************************/
Ssw_SignalCorrespondence(Aig_Man_t * pAig,Ssw_Pars_t * pPars)415 Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
416 {
417 Ssw_Pars_t Pars;
418 Aig_Man_t * pAigNew;
419 Ssw_Man_t * p;
420 assert( Aig_ManRegNum(pAig) > 0 );
421 // reset random numbers
422 Aig_ManRandom( 1 );
423 // if parameters are not given, create them
424 if ( pPars == NULL )
425 Ssw_ManSetDefaultParams( pPars = &Pars );
426 // consider the case of empty AIG
427 if ( Aig_ManNodeNum(pAig) == 0 )
428 {
429 pPars->nIters = 0;
430 // Ntl_ManFinalize() needs the following to satisfy an assertion
431 Aig_ManReprStart( pAig,Aig_ManObjNumMax(pAig) );
432 return Aig_ManDupOrdered(pAig);
433 }
434 // check and update parameters
435 if ( pPars->fLatchCorrOpt )
436 {
437 pPars->fLatchCorr = 1;
438 pPars->nFramesAddSim = 0;
439 if ( (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0) )
440 return Ssw_SignalCorrespondencePart( pAig, pPars );
441 }
442 else
443 {
444 assert( pPars->nFramesK > 0 );
445 // perform partitioning
446 if ( (pPars->nPartSize > 0 && pPars->nPartSize < Aig_ManRegNum(pAig))
447 || (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0) )
448 return Ssw_SignalCorrespondencePart( pAig, pPars );
449 }
450
451 if ( pPars->fScorrGia )
452 {
453 if ( pPars->fLatchCorrOpt )
454 {
455 extern Aig_Man_t * Cec_LatchCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat );
456 return Cec_LatchCorrespondence( pAig, pPars->nBTLimit, pPars->fUseCSat );
457 }
458 else
459 {
460 extern Aig_Man_t * Cec_SignalCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat );
461 return Cec_SignalCorrespondence( pAig, pPars->nBTLimit, pPars->fUseCSat );
462 }
463 }
464
465 // start the induction manager
466 p = Ssw_ManCreate( pAig, pPars );
467 // compute candidate equivalence classes
468 // p->pPars->nConstrs = 1;
469 if ( p->pPars->fConstrs )
470 {
471 // create trivial equivalence classes with all nodes being candidates for constant 1
472 p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs );
473 Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_SmlObjIsConstBit, Ssw_SmlObjsAreEqualBit );
474 // derive phase bits to satisfy the constraints
475 if ( Ssw_ManSetConstrPhases( pAig, p->pPars->nFramesK + 1, &p->vInits ) != 0 )
476 {
477 Abc_Print( 1, "Ssw_SignalCorrespondence(): The init state does not satisfy the constraints!\n" );
478 p->pPars->fVerbose = 0;
479 Ssw_ManStop( p );
480 return NULL;
481 }
482 // perform simulation of the first timeframes
483 Ssw_ManRefineByConstrSim( p );
484 }
485 else
486 {
487 // perform one round of seq simulation and generate candidate equivalence classes
488 p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->nFramesK, pPars->fLatchCorr, pPars->fConstCorr, pPars->fOutputCorr, pPars->nMaxLevs, pPars->fVerbose );
489 // p->ppClasses = Ssw_ClassesPrepareTargets( pAig );
490 if ( pPars->fLatchCorrOpt )
491 p->pSml = Ssw_SmlStart( pAig, 0, 2, 1 );
492 else if ( pPars->fDynamic )
493 p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + p->pPars->nFramesAddSim, 1 );
494 else
495 p->pSml = Ssw_SmlStart( pAig, 0, 1 + p->pPars->nFramesAddSim, 1 );
496 Ssw_ClassesSetData( p->ppClasses, p->pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord );
497 }
498 // allocate storage
499 if ( p->pPars->fLocalSim && p->pSml )
500 p->pVisited = ABC_CALLOC( int, Ssw_SmlNumFrames( p->pSml ) * Aig_ManObjNumMax(p->pAig) );
501 // perform refinement of classes
502 pAigNew = Ssw_SignalCorrespondenceRefine( p );
503 // Ssw_ReportOutputs( pAigNew );
504 if ( pPars->fConstrs && pPars->fVerbose )
505 Ssw_ReportConeReductions( p, pAig, pAigNew );
506 // cleanup
507 Ssw_ManStop( p );
508 return pAigNew;
509 }
510
511 /**Function*************************************************************
512
513 Synopsis [Performs computation of latch correspondence.]
514
515 Description []
516
517 SideEffects []
518
519 SeeAlso []
520
521 ***********************************************************************/
Ssw_LatchCorrespondence(Aig_Man_t * pAig,Ssw_Pars_t * pPars)522 Aig_Man_t * Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
523 {
524 Aig_Man_t * pRes;
525 Ssw_Pars_t Pars;
526 if ( pPars == NULL )
527 Ssw_ManSetDefaultParamsLcorr( pPars = &Pars );
528 pRes = Ssw_SignalCorrespondence( pAig, pPars );
529 // if ( pPars->fConstrs && pPars->fVerbose )
530 // Ssw_ReportConeReductions( pAig, pRes );
531 return pRes;
532 }
533
534
535 ////////////////////////////////////////////////////////////////////////
536 /// END OF FILE ///
537 ////////////////////////////////////////////////////////////////////////
538
539
540 ABC_NAMESPACE_IMPL_END
541