1 /**CFile****************************************************************
2
3 FileName [fsimSim.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Fast sequential AIG simulator.]
8
9 Synopsis [Simulation procedures.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: fsimSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "fsimInt.h"
22 #include "aig/ssw/ssw.h"
23
24 ABC_NAMESPACE_IMPL_START
25
26
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30
31 ////////////////////////////////////////////////////////////////////////
32 /// FUNCTION DEFINITIONS ///
33 ////////////////////////////////////////////////////////////////////////
34
35 /**Function*************************************************************
36
37 Synopsis []
38
39 Description []
40
41 SideEffects []
42
43 SeeAlso []
44
45 ***********************************************************************/
Fsim_ManSimInfoRandom(Fsim_Man_t * p,unsigned * pInfo)46 static inline void Fsim_ManSimInfoRandom( Fsim_Man_t * p, unsigned * pInfo )
47 {
48 int w;
49 for ( w = p->nWords-1; w >= 0; w-- )
50 pInfo[w] = Aig_ManRandom( 0 );
51 }
52
53 /**Function*************************************************************
54
55 Synopsis []
56
57 Description []
58
59 SideEffects []
60
61 SeeAlso []
62
63 ***********************************************************************/
Fsim_ManSimInfoZero(Fsim_Man_t * p,unsigned * pInfo)64 static inline void Fsim_ManSimInfoZero( Fsim_Man_t * p, unsigned * pInfo )
65 {
66 int w;
67 for ( w = p->nWords-1; w >= 0; w-- )
68 pInfo[w] = 0;
69 }
70
71 /**Function*************************************************************
72
73 Synopsis [Returns index of the first pattern that failed.]
74
75 Description []
76
77 SideEffects []
78
79 SeeAlso []
80
81 ***********************************************************************/
Fsim_ManSimInfoIsZero(Fsim_Man_t * p,unsigned * pInfo)82 static inline int Fsim_ManSimInfoIsZero( Fsim_Man_t * p, unsigned * pInfo )
83 {
84 int w;
85 for ( w = p->nWords-1; w >= 0; w-- )
86 if ( pInfo[w] )
87 return 32*(w-1) + Aig_WordFindFirstBit( pInfo[w] );
88 return -1;
89 }
90
91 /**Function*************************************************************
92
93 Synopsis []
94
95 Description []
96
97 SideEffects []
98
99 SeeAlso []
100
101 ***********************************************************************/
Fsim_ManSimInfoOne(Fsim_Man_t * p,unsigned * pInfo)102 static inline void Fsim_ManSimInfoOne( Fsim_Man_t * p, unsigned * pInfo )
103 {
104 int w;
105 for ( w = p->nWords-1; w >= 0; w-- )
106 pInfo[w] = ~0;
107 }
108
109 /**Function*************************************************************
110
111 Synopsis []
112
113 Description []
114
115 SideEffects []
116
117 SeeAlso []
118
119 ***********************************************************************/
Fsim_ManSimInfoCopy(Fsim_Man_t * p,unsigned * pInfo,unsigned * pInfo0)120 static inline void Fsim_ManSimInfoCopy( Fsim_Man_t * p, unsigned * pInfo, unsigned * pInfo0 )
121 {
122 int w;
123 for ( w = p->nWords-1; w >= 0; w-- )
124 pInfo[w] = pInfo0[w];
125 }
126
127 /**Function*************************************************************
128
129 Synopsis []
130
131 Description []
132
133 SideEffects []
134
135 SeeAlso []
136
137 ***********************************************************************/
Fsim_ManSimulateCi(Fsim_Man_t * p,int iNode,int iCi)138 static inline void Fsim_ManSimulateCi( Fsim_Man_t * p, int iNode, int iCi )
139 {
140 unsigned * pInfo = Fsim_SimData( p, iNode % p->nFront );
141 unsigned * pInfo0 = Fsim_SimDataCi( p, iCi );
142 int w;
143 for ( w = p->nWords-1; w >= 0; w-- )
144 pInfo[w] = pInfo0[w];
145 }
146
147 /**Function*************************************************************
148
149 Synopsis []
150
151 Description []
152
153 SideEffects []
154
155 SeeAlso []
156
157 ***********************************************************************/
Fsim_ManSimulateCo(Fsim_Man_t * p,int iCo,int iFan0)158 static inline void Fsim_ManSimulateCo( Fsim_Man_t * p, int iCo, int iFan0 )
159 {
160 unsigned * pInfo = Fsim_SimDataCo( p, iCo );
161 unsigned * pInfo0 = Fsim_SimData( p, Fsim_Lit2Var(iFan0) % p->nFront );
162 int w;
163 if ( Fsim_LitIsCompl(iFan0) )
164 for ( w = p->nWords-1; w >= 0; w-- )
165 pInfo[w] = ~pInfo0[w];
166 else //if ( !Fsim_LitIsCompl(iFan0) )
167 for ( w = p->nWords-1; w >= 0; w-- )
168 pInfo[w] = pInfo0[w];
169 }
170
171 /**Function*************************************************************
172
173 Synopsis []
174
175 Description []
176
177 SideEffects []
178
179 SeeAlso []
180
181 ***********************************************************************/
Fsim_ManSimulateNode(Fsim_Man_t * p,int iNode,int iFan0,int iFan1)182 static inline void Fsim_ManSimulateNode( Fsim_Man_t * p, int iNode, int iFan0, int iFan1 )
183 {
184 unsigned * pInfo = Fsim_SimData( p, iNode % p->nFront );
185 unsigned * pInfo0 = Fsim_SimData( p, Fsim_Lit2Var(iFan0) % p->nFront );
186 unsigned * pInfo1 = Fsim_SimData( p, Fsim_Lit2Var(iFan1) % p->nFront );
187 int w;
188 if ( Fsim_LitIsCompl(iFan0) && Fsim_LitIsCompl(iFan1) )
189 for ( w = p->nWords-1; w >= 0; w-- )
190 pInfo[w] = ~(pInfo0[w] | pInfo1[w]);
191 else if ( Fsim_LitIsCompl(iFan0) && !Fsim_LitIsCompl(iFan1) )
192 for ( w = p->nWords-1; w >= 0; w-- )
193 pInfo[w] = ~pInfo0[w] & pInfo1[w];
194 else if ( !Fsim_LitIsCompl(iFan0) && Fsim_LitIsCompl(iFan1) )
195 for ( w = p->nWords-1; w >= 0; w-- )
196 pInfo[w] = pInfo0[w] & ~pInfo1[w];
197 else //if ( !Fsim_LitIsCompl(iFan0) && !Fsim_LitIsCompl(iFan1) )
198 for ( w = p->nWords-1; w >= 0; w-- )
199 pInfo[w] = pInfo0[w] & pInfo1[w];
200 }
201
202 /**Function*************************************************************
203
204 Synopsis []
205
206 Description []
207
208 SideEffects []
209
210 SeeAlso []
211
212 ***********************************************************************/
Fsim_ManSimInfoInit(Fsim_Man_t * p)213 static inline void Fsim_ManSimInfoInit( Fsim_Man_t * p )
214 {
215 int iPioNum, i;
216 Vec_IntForEachEntry( p->vCis2Ids, iPioNum, i )
217 {
218 if ( iPioNum < p->nPis )
219 Fsim_ManSimInfoRandom( p, Fsim_SimDataCi(p, i) );
220 else
221 Fsim_ManSimInfoZero( p, Fsim_SimDataCi(p, i) );
222 }
223 }
224
225 /**Function*************************************************************
226
227 Synopsis []
228
229 Description []
230
231 SideEffects []
232
233 SeeAlso []
234
235 ***********************************************************************/
Fsim_ManSimInfoTransfer(Fsim_Man_t * p)236 static inline void Fsim_ManSimInfoTransfer( Fsim_Man_t * p )
237 {
238 int iPioNum, i;
239 Vec_IntForEachEntry( p->vCis2Ids, iPioNum, i )
240 {
241 if ( iPioNum < p->nPis )
242 Fsim_ManSimInfoRandom( p, Fsim_SimDataCi(p, i) );
243 else
244 Fsim_ManSimInfoCopy( p, Fsim_SimDataCi(p, i), Fsim_SimDataCo(p, p->nPos+iPioNum-p->nPis) );
245 }
246 }
247
248 /**Function*************************************************************
249
250 Synopsis []
251
252 Description []
253
254 SideEffects []
255
256 SeeAlso []
257
258 ***********************************************************************/
Fsim_ManRestoreNum(Fsim_Man_t * p)259 static inline int Fsim_ManRestoreNum( Fsim_Man_t * p )
260 {
261 int ch, i, x = 0;
262 for ( i = 0; (ch = *p->pDataCur++) & 0x80; i++ )
263 x |= (ch & 0x7f) << (7 * i);
264 assert( p->pDataCur - p->pDataAig < p->nDataAig );
265 return x | (ch << (7 * i));
266 }
267
268 /**Function*************************************************************
269
270 Synopsis []
271
272 Description []
273
274 SideEffects []
275
276 SeeAlso []
277
278 ***********************************************************************/
Fsim_ManRestoreObj(Fsim_Man_t * p,Fsim_Obj_t * pObj)279 static inline int Fsim_ManRestoreObj( Fsim_Man_t * p, Fsim_Obj_t * pObj )
280 {
281 int iValue = Fsim_ManRestoreNum( p );
282 if ( (iValue & 3) == 3 ) // and
283 {
284 pObj->iNode = (iValue >> 2) + p->iNodePrev;
285 pObj->iFan0 = (pObj->iNode << 1) - Fsim_ManRestoreNum( p );
286 pObj->iFan1 = pObj->iFan0 - Fsim_ManRestoreNum( p );
287 p->iNodePrev = pObj->iNode;
288 }
289 else if ( (iValue & 3) == 1 ) // ci
290 {
291 pObj->iNode = (iValue >> 2) + p->iNodePrev;
292 pObj->iFan0 = 0;
293 pObj->iFan1 = 0;
294 p->iNodePrev = pObj->iNode;
295 }
296 else // if ( (iValue & 1) == 0 ) // co
297 {
298 pObj->iNode = 0;
299 pObj->iFan0 = ((p->iNodePrev << 1) | 1) - (iValue >> 1);
300 pObj->iFan1 = 0;
301 }
302 return 1;
303 }
304
305 /**Function*************************************************************
306
307 Synopsis []
308
309 Description []
310
311 SideEffects []
312
313 SeeAlso []
314
315 ***********************************************************************/
Fsim_ManSimulateRound2(Fsim_Man_t * p)316 static inline void Fsim_ManSimulateRound2( Fsim_Man_t * p )
317 {
318 Fsim_Obj_t * pObj;
319 int i, iCis = 0, iCos = 0;
320 if ( Aig_ObjRefs(Aig_ManConst1(p->pAig)) )
321 Fsim_ManSimInfoOne( p, Fsim_SimData(p, 1) );
322 Fsim_ManForEachObj( p, pObj, i )
323 {
324 if ( pObj->iFan0 == 0 )
325 Fsim_ManSimulateCi( p, pObj->iNode, iCis++ );
326 else if ( pObj->iFan1 == 0 )
327 Fsim_ManSimulateCo( p, iCos++, pObj->iFan0 );
328 else
329 Fsim_ManSimulateNode( p, pObj->iNode, pObj->iFan0, pObj->iFan1 );
330 }
331 assert( iCis == p->nCis );
332 assert( iCos == p->nCos );
333 }
334
335 /**Function*************************************************************
336
337 Synopsis []
338
339 Description []
340
341 SideEffects []
342
343 SeeAlso []
344
345 ***********************************************************************/
Fsim_ManSimulateRound(Fsim_Man_t * p)346 static inline void Fsim_ManSimulateRound( Fsim_Man_t * p )
347 {
348 int * pCur, * pEnd;
349 int iCis = 0, iCos = 0;
350 if ( p->pDataAig2 == NULL )
351 {
352 Fsim_ManSimulateRound2( p );
353 return;
354 }
355 if ( Aig_ObjRefs(Aig_ManConst1(p->pAig)) )
356 Fsim_ManSimInfoOne( p, Fsim_SimData(p, 1) );
357 pCur = p->pDataAig2 + 6;
358 pEnd = p->pDataAig2 + 3 * p->nObjs;
359 while ( pCur < pEnd )
360 {
361 if ( pCur[1] == 0 )
362 Fsim_ManSimulateCi( p, pCur[0], iCis++ );
363 else if ( pCur[2] == 0 )
364 Fsim_ManSimulateCo( p, iCos++, pCur[1] );
365 else
366 Fsim_ManSimulateNode( p, pCur[0], pCur[1], pCur[2] );
367 pCur += 3;
368 }
369 assert( iCis == p->nCis );
370 assert( iCos == p->nCos );
371 }
372
373 /**Function*************************************************************
374
375 Synopsis []
376
377 Description []
378
379 SideEffects []
380
381 SeeAlso []
382
383 ***********************************************************************/
Fsim_ManSimulateRoundTest(Fsim_Man_t * p)384 void Fsim_ManSimulateRoundTest( Fsim_Man_t * p )
385 {
386 Fsim_Obj_t * pObj;
387 int i;
388 clock_t clk = clock();
389 Fsim_ManForEachObj( p, pObj, i )
390 {
391 }
392 // ABC_PRT( "Unpacking time", p->pPars->nIters * (clock() - clk) );
393 }
394
395 /**Function*************************************************************
396
397 Synopsis [Returns index of the PO and pattern that failed it.]
398
399 Description []
400
401 SideEffects []
402
403 SeeAlso []
404
405 ***********************************************************************/
Fsim_ManCheckPos(Fsim_Man_t * p,int * piPo,int * piPat)406 static inline int Fsim_ManCheckPos( Fsim_Man_t * p, int * piPo, int * piPat )
407 {
408 int i, iPat;
409 for ( i = 0; i < p->nPos; i++ )
410 {
411 iPat = Fsim_ManSimInfoIsZero( p, Fsim_SimDataCo(p, i) );
412 if ( iPat >= 0 )
413 {
414 *piPo = i;
415 *piPat = iPat;
416 return 1;
417 }
418 }
419 return 0;
420 }
421
422 /**Function*************************************************************
423
424 Synopsis [Returns the counter-example.]
425
426 Description []
427
428 SideEffects []
429
430 SeeAlso []
431
432 ***********************************************************************/
Fsim_ManGenerateCounter(Aig_Man_t * pAig,int iFrame,int iOut,int nWords,int iPat,Vec_Int_t * vCis2Ids)433 Abc_Cex_t * Fsim_ManGenerateCounter( Aig_Man_t * pAig, int iFrame, int iOut, int nWords, int iPat, Vec_Int_t * vCis2Ids )
434 {
435 Abc_Cex_t * p;
436 unsigned * pData;
437 int f, i, w, iPioId, Counter;
438 p = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), iFrame+1 );
439 p->iFrame = iFrame;
440 p->iPo = iOut;
441 // fill in the binary data
442 Aig_ManRandom( 1 );
443 Counter = p->nRegs;
444 pData = ABC_ALLOC( unsigned, nWords );
445 for ( f = 0; f <= iFrame; f++, Counter += p->nPis )
446 for ( i = 0; i < Aig_ManPiNum(pAig); i++ )
447 {
448 iPioId = Vec_IntEntry( vCis2Ids, i );
449 if ( iPioId >= p->nPis )
450 continue;
451 for ( w = nWords-1; w >= 0; w-- )
452 pData[w] = Aig_ManRandom( 0 );
453 if ( Aig_InfoHasBit( pData, iPat ) )
454 Aig_InfoSetBit( p->pData, Counter + iPioId );
455 }
456 ABC_FREE( pData );
457 return p;
458 }
459
460 /**Function*************************************************************
461
462 Synopsis []
463
464 Description []
465
466 SideEffects []
467
468 SeeAlso []
469
470 ***********************************************************************/
Fsim_ManSimulate(Aig_Man_t * pAig,Fsim_ParSim_t * pPars)471 int Fsim_ManSimulate( Aig_Man_t * pAig, Fsim_ParSim_t * pPars )
472 {
473 Fsim_Man_t * p;
474 Sec_MtrStatus_t Status;
475 int i, iOut, iPat;
476 clock_t clk, clkTotal = clock(), clk2, clk2Total = 0;
477 assert( Aig_ManRegNum(pAig) > 0 );
478 if ( pPars->fCheckMiter )
479 {
480 Status = Sec_MiterStatus( pAig );
481 if ( Status.nSat > 0 )
482 {
483 printf( "Miter is trivially satisfiable (output %d).\n", Status.iOut );
484 return 1;
485 }
486 if ( Status.nUndec == 0 )
487 {
488 printf( "Miter is trivially unsatisfiable.\n" );
489 return 0;
490 }
491 }
492 // create manager
493 clk = clock();
494 p = Fsim_ManCreate( pAig );
495 p->nWords = pPars->nWords;
496 if ( pPars->fVerbose )
497 {
498 printf( "Obj = %8d (%8d). Cut = %6d. Front = %6d. FrtMem = %7.2f MB. ",
499 p->nObjs, p->nCis + p->nNodes, p->nCrossCutMax, p->nFront,
500 4.0*p->nWords*(p->nFront)/(1<<20) );
501 ABC_PRT( "Time", clock() - clk );
502 }
503 // create simulation frontier
504 clk = clock();
505 Fsim_ManFront( p, pPars->fCompressAig );
506 if ( pPars->fVerbose )
507 {
508 printf( "Max ID = %8d. Log max ID = %2d. AigMem = %7.2f MB (%5.2f byte/obj). ",
509 p->iNumber, Aig_Base2Log(p->iNumber),
510 1.0*(p->pDataCur-p->pDataAig)/(1<<20),
511 1.0*(p->pDataCur-p->pDataAig)/p->nObjs );
512 ABC_PRT( "Time", clock() - clk );
513 }
514 // perform simulation
515 Aig_ManRandom( 1 );
516 assert( p->pDataSim == NULL );
517 p->pDataSim = ABC_ALLOC( unsigned, p->nWords * p->nFront );
518 p->pDataSimCis = ABC_ALLOC( unsigned, p->nWords * p->nCis );
519 p->pDataSimCos = ABC_ALLOC( unsigned, p->nWords * p->nCos );
520 Fsim_ManSimInfoInit( p );
521 for ( i = 0; i < pPars->nIters; i++ )
522 {
523 Fsim_ManSimulateRound( p );
524 if ( pPars->fVerbose )
525 {
526 printf( "Frame %4d out of %4d and timeout %3d sec. ", i+1, pPars->nIters, pPars->TimeLimit );
527 printf( "Time = %7.2f sec\r", (1.0*clock()-clkTotal)/CLOCKS_PER_SEC );
528 }
529 if ( pPars->fCheckMiter && Fsim_ManCheckPos( p, &iOut, &iPat ) )
530 {
531 assert( pAig->pSeqModel == NULL );
532 pAig->pSeqModel = Fsim_ManGenerateCounter( pAig, i, iOut, p->nWords, iPat, p->vCis2Ids );
533 if ( pPars->fVerbose )
534 printf( "Miter is satisfiable after simulation (output %d).\n", iOut );
535 break;
536 }
537 if ( (clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit )
538 break;
539 clk2 = clock();
540 if ( i < pPars->nIters - 1 )
541 Fsim_ManSimInfoTransfer( p );
542 clk2Total += clock() - clk2;
543 }
544 if ( pAig->pSeqModel == NULL )
545 printf( "No bug detected after %d frames with time limit %d seconds.\n", i+1, pPars->TimeLimit );
546 if ( pPars->fVerbose )
547 {
548 printf( "Maxcut = %8d. AigMem = %7.2f MB. SimMem = %7.2f MB. ",
549 p->nCrossCutMax,
550 p->pDataAig2? 12.0*p->nObjs/(1<<20) : 1.0*(p->pDataCur-p->pDataAig)/(1<<20),
551 4.0*p->nWords*(p->nFront+p->nCis+p->nCos)/(1<<20) );
552 ABC_PRT( "Sim time", clock() - clkTotal );
553
554 // ABC_PRT( "Additional time", clk2Total );
555 // Fsim_ManSimulateRoundTest( p );
556 // Fsim_ManSimulateRoundTest2( p );
557 }
558 Fsim_ManDelete( p );
559 return pAig->pSeqModel != NULL;
560
561 }
562
563 ////////////////////////////////////////////////////////////////////////
564 /// END OF FILE ///
565 ////////////////////////////////////////////////////////////////////////
566
567
568 ABC_NAMESPACE_IMPL_END
569
570