1 /**CFile****************************************************************
2
3 FileName [kliveness.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Liveness property checking.]
8
9 Synopsis [Main implementation module of the algorithm k-Liveness ]
10 [invented by Koen Claessen, Niklas Sorensson. Implements]
11 [the code for 'kcs'. 'kcs' pre-processes based on switch]
12 [and then runs the (absorber circuit >> pdr) loop ]
13
14 Author [Sayak Ray]
15
16 Affiliation [UC Berkeley]
17
18 Date [Ver. 1.0. Started - October 31, 2012.]
19
20 ***********************************************************************/
21
22 #include <stdio.h>
23 #include "base/main/main.h"
24 #include "aig/aig/aig.h"
25 #include "aig/saig/saig.h"
26 #include <string.h>
27 #include "base/main/mainInt.h"
28 #include "proof/pdr/pdr.h"
29 #include <time.h>
30
31 //#define WITHOUT_CONSTRAINTS
32
33 ABC_NAMESPACE_IMPL_START
34
35 /***************** Declaration of standard ABC related functions ********************/
36 extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
37 extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
38 extern Abc_Ntk_t * Abc_NtkMakeOnePo( Abc_Ntk_t * pNtk, int Output, int nRange );
39 extern void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName, Vec_Ptr_t * vPiNames, Vec_Ptr_t * vPoNames );
40 /***********************************************************************************/
41
42 /***************** Declaration of kLiveness related functions **********************/
43 //function defined in kLiveConstraints.c
44 extern Aig_Man_t *generateWorkingAig( Aig_Man_t *pAig, Abc_Ntk_t *pNtk, int *pIndex0Live );
45
46 //function defined in arenaViolation.c
47 extern Aig_Man_t *generateWorkingAigWithDSC( Aig_Man_t *pAig, Abc_Ntk_t *pNtk, int *pIndex0Live, Vec_Ptr_t *vMasterBarriers );
48
49 //function defined in disjunctiveMonotone.c
50 extern Vec_Ptr_t *findDisjunctiveMonotoneSignals( Abc_Ntk_t *pNtk );
51 extern Vec_Int_t *createSingletonIntVector( int i );
52 /***********************************************************************************/
53 extern Aig_Man_t *generateDisjunctiveTester( Abc_Ntk_t *pNtk, Aig_Man_t *pAig, int combN, int combK );
54 extern Aig_Man_t *generateGeneralDisjunctiveTester( Abc_Ntk_t *pNtk, Aig_Man_t *pAig, int combK );
55
56 //Definition of some macros pertaining to modes/switches
57 #define SIMPLE_kCS 0
58 #define kCS_WITH_SAFETY_INVARIANTS 1
59 #define kCS_WITH_DISCOVER_MONOTONE_SIGNALS 2
60 #define kCS_WITH_SAFETY_AND_DCS_INVARIANTS 3
61 #define kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS 4
62
63 //unused function
64 #if 0
65 Aig_Obj_t *readTargetPinSignal(Aig_Man_t *pAig, Abc_Ntk_t *pNtk)
66 {
67 Aig_Obj_t *pObj;
68 int i;
69
70 Saig_ManForEachPo( pAig, pObj, i )
71 {
72 if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "0Liveness_" ) != NULL )
73 {
74 //return Aig_ObjFanin0(pObj);
75 return Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj));
76 }
77 }
78
79 return NULL;
80 }
81 #endif
82
readLiveSignal_0(Aig_Man_t * pAig,int liveIndex_0)83 Aig_Obj_t *readLiveSignal_0( Aig_Man_t *pAig, int liveIndex_0 )
84 {
85 Aig_Obj_t *pObj;
86
87 pObj = Aig_ManCo( pAig, liveIndex_0 );
88 return Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj));
89 }
90
readLiveSignal_k(Aig_Man_t * pAig,int liveIndex_k)91 Aig_Obj_t *readLiveSignal_k( Aig_Man_t *pAig, int liveIndex_k )
92 {
93 Aig_Obj_t *pObj;
94
95 pObj = Aig_ManCo( pAig, liveIndex_k );
96 return Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj));
97 }
98
99 //unused funtion
100 #if 0
101 Aig_Obj_t *readTargetPoutSignal(Aig_Man_t *pAig, Abc_Ntk_t *pNtk, int nonFirstIteration)
102 {
103 Aig_Obj_t *pObj;
104 int i;
105
106 if( nonFirstIteration == 0 )
107 return NULL;
108 else
109 Saig_ManForEachPo( pAig, pObj, i )
110 {
111 if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "kLiveness_" ) != NULL )
112 {
113 //return Aig_ObjFanin0(pObj);
114 return Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj));
115 }
116 }
117
118 return NULL;
119 }
120 #endif
121
122 //unused function
123 #if 0
124 void updateNewNetworkNameManager_kCS( Abc_Ntk_t *pNtk, Aig_Man_t *pAig, Vec_Ptr_t *vPiNames,
125 Vec_Ptr_t *vLoNames, Vec_Ptr_t *vPoNames, Vec_Ptr_t *vLiNames )
126 {
127 Aig_Obj_t *pObj;
128 Abc_Obj_t *pNode;
129 int i, ntkObjId;
130
131 pNtk->pManName = Nm_ManCreate( Abc_NtkCiNum( pNtk ) );
132
133 if( vPiNames )
134 {
135 Saig_ManForEachPi( pAig, pObj, i )
136 {
137 ntkObjId = Abc_NtkCi( pNtk, i )->Id;
138 Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), (char *)Vec_PtrEntry(vPiNames, i), NULL );
139 }
140 }
141 if( vLoNames )
142 {
143 Saig_ManForEachLo( pAig, pObj, i )
144 {
145 ntkObjId = Abc_NtkCi( pNtk, Saig_ManPiNum( pAig ) + i )->Id;
146 Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), (char *)Vec_PtrEntry(vLoNames, i), NULL );
147 }
148 }
149
150 if( vPoNames )
151 {
152 Saig_ManForEachPo( pAig, pObj, i )
153 {
154 ntkObjId = Abc_NtkCo( pNtk, i )->Id;
155 Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), (char *)Vec_PtrEntry(vPoNames, i), NULL );
156 }
157 }
158
159 if( vLiNames )
160 {
161 Saig_ManForEachLi( pAig, pObj, i )
162 {
163 ntkObjId = Abc_NtkCo( pNtk, Saig_ManPoNum( pAig ) + i )->Id;
164 Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), (char *)Vec_PtrEntry(vLiNames, i), NULL );
165 }
166 }
167
168 // assign latch input names
169 Abc_NtkForEachLatch(pNtk, pNode, i)
170 if ( Nm_ManFindNameById(pNtk->pManName, Abc_ObjFanin0(pNode)->Id) == NULL )
171 Abc_ObjAssignName( Abc_ObjFanin0(pNode), Abc_ObjName(Abc_ObjFanin0(pNode)), NULL );
172 }
173 #endif
174
introduceAbsorberLogic(Aig_Man_t * pAig,int * pLiveIndex_0,int * pLiveIndex_k,int nonFirstIteration)175 Aig_Man_t *introduceAbsorberLogic( Aig_Man_t *pAig, int *pLiveIndex_0, int *pLiveIndex_k, int nonFirstIteration )
176 {
177 Aig_Man_t *pNewAig;
178 Aig_Obj_t *pObj, *pObjAbsorberLo, *pPInNewArg, *pPOutNewArg;
179 Aig_Obj_t *pPIn = NULL, *pPOut = NULL, *pPOutCo = NULL;
180 Aig_Obj_t *pFirstAbsorberOr, *pSecondAbsorberOr;
181 int i;
182 int piCopied = 0, loCreated = 0, loCopied = 0, liCreated = 0, liCopied = 0;
183 int nRegCount;
184
185 assert(*pLiveIndex_0 != -1);
186 if(nonFirstIteration == 0)
187 assert( *pLiveIndex_k == -1 );
188 else
189 assert( *pLiveIndex_k != -1 );
190
191 //****************************************************************
192 // Step1: create the new manager
193 // Note: The new manager is created with "2 * Aig_ManObjNumMax(p)"
194 // nodes, but this selection is arbitrary - need to be justified
195 //****************************************************************
196 pNewAig = Aig_ManStart( Aig_ManObjNumMax(pAig) );
197 pNewAig->pName = (char *)malloc( strlen( pAig->pName ) + strlen("_kCS") + 1 );
198 sprintf(pNewAig->pName, "%s_%s", pAig->pName, "kCS");
199 pNewAig->pSpec = NULL;
200
201 //****************************************************************
202 // reading the signal pIn, and pOut
203 //****************************************************************
204
205 pPIn = readLiveSignal_0( pAig, *pLiveIndex_0 );
206 if( *pLiveIndex_k == -1 )
207 pPOut = NULL;
208 else
209 pPOut = readLiveSignal_k( pAig, *pLiveIndex_k );
210
211 //****************************************************************
212 // Step 2: map constant nodes
213 //****************************************************************
214 pObj = Aig_ManConst1( pAig );
215 pObj->pData = Aig_ManConst1( pNewAig );
216
217 //****************************************************************
218 // Step 3: create true PIs
219 //****************************************************************
220 Saig_ManForEachPi( pAig, pObj, i )
221 {
222 piCopied++;
223 pObj->pData = Aig_ObjCreateCi(pNewAig);
224 }
225
226 //****************************************************************
227 // Step 5: create register outputs
228 //****************************************************************
229 Saig_ManForEachLo( pAig, pObj, i )
230 {
231 loCopied++;
232 pObj->pData = Aig_ObjCreateCi(pNewAig);
233 }
234
235 //****************************************************************
236 // Step 6: create "D" register output for the ABSORBER logic
237 //****************************************************************
238 loCreated++;
239 pObjAbsorberLo = Aig_ObjCreateCi( pNewAig );
240
241 nRegCount = loCreated + loCopied;
242
243 //********************************************************************
244 // Step 7: create internal nodes
245 //********************************************************************
246 Aig_ManForEachNode( pAig, pObj, i )
247 {
248 pObj->pData = Aig_And( pNewAig, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
249 }
250
251 //****************************************************************
252 // Step 8: create the two OR gates of the OBSERVER logic
253 //****************************************************************
254 if( nonFirstIteration == 0 )
255 {
256 assert(pPIn);
257
258 pPInNewArg = !Aig_IsComplement(pPIn)?
259 (Aig_Obj_t *)((Aig_Regular(pPIn))->pData) :
260 Aig_Not((Aig_Obj_t *)((Aig_Regular(pPIn))->pData));
261
262 pFirstAbsorberOr = Aig_Or( pNewAig, Aig_Not(pPInNewArg), pObjAbsorberLo );
263 pSecondAbsorberOr = Aig_Or( pNewAig, pPInNewArg, Aig_Not(pObjAbsorberLo) );
264 }
265 else
266 {
267 assert( pPOut );
268
269 pPInNewArg = !Aig_IsComplement(pPIn)?
270 (Aig_Obj_t *)((Aig_Regular(pPIn))->pData) :
271 Aig_Not((Aig_Obj_t *)((Aig_Regular(pPIn))->pData));
272 pPOutNewArg = !Aig_IsComplement(pPOut)?
273 (Aig_Obj_t *)((Aig_Regular(pPOut))->pData) :
274 Aig_Not((Aig_Obj_t *)((Aig_Regular(pPOut))->pData));
275
276 pFirstAbsorberOr = Aig_Or( pNewAig, Aig_Not(pPOutNewArg), pObjAbsorberLo );
277 pSecondAbsorberOr = Aig_Or( pNewAig, pPInNewArg, Aig_Not(pObjAbsorberLo) );
278 }
279
280 //********************************************************************
281 // Step 9: create primary outputs
282 //********************************************************************
283 Saig_ManForEachPo( pAig, pObj, i )
284 {
285 pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
286 if( i == *pLiveIndex_k )
287 pPOutCo = (Aig_Obj_t *)(pObj->pData);
288 }
289
290 //create new po
291 if( nonFirstIteration == 0 )
292 {
293 assert(pPOutCo == NULL);
294 pPOutCo = Aig_ObjCreateCo( pNewAig, pSecondAbsorberOr );
295
296 *pLiveIndex_k = i;
297 }
298 else
299 {
300 assert( pPOutCo != NULL );
301 //pPOutCo = Aig_ObjCreateCo( pNewAig, pSecondAbsorberOr );
302 //*pLiveIndex_k = Saig_ManPoNum(pAig);
303
304 Aig_ObjPatchFanin0( pNewAig, pPOutCo, pSecondAbsorberOr );
305 }
306
307 Saig_ManForEachLi( pAig, pObj, i )
308 {
309 liCopied++;
310 Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
311 }
312
313 //create new li
314 liCreated++;
315 Aig_ObjCreateCo( pNewAig, pFirstAbsorberOr );
316
317 Aig_ManSetRegNum( pNewAig, nRegCount );
318 Aig_ManCleanup( pNewAig );
319
320 assert( Aig_ManCheck( pNewAig ) );
321
322 assert( *pLiveIndex_k != - 1);
323 return pNewAig;
324 }
325
modifyAigToApplySafetyInvar(Aig_Man_t * pAig,int csTarget,int safetyInvarPO)326 void modifyAigToApplySafetyInvar(Aig_Man_t *pAig, int csTarget, int safetyInvarPO)
327 {
328 Aig_Obj_t *pObjPOSafetyInvar, *pObjSafetyInvar;
329 Aig_Obj_t *pObjPOCSTarget, *pObjCSTarget;
330 Aig_Obj_t *pObjCSTargetNew;
331
332 pObjPOSafetyInvar = Aig_ManCo( pAig, safetyInvarPO );
333 pObjSafetyInvar = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPOSafetyInvar), Aig_ObjFaninC0(pObjPOSafetyInvar));
334 pObjPOCSTarget = Aig_ManCo( pAig, csTarget );
335 pObjCSTarget = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPOCSTarget), Aig_ObjFaninC0(pObjPOCSTarget));
336
337 pObjCSTargetNew = Aig_And( pAig, pObjSafetyInvar, pObjCSTarget );
338 Aig_ObjPatchFanin0( pAig, pObjPOCSTarget, pObjCSTargetNew );
339 }
340
flipConePdr(Aig_Man_t * pAig,int directive,int targetCSPropertyIndex,int safetyInvariantPOIndex,int absorberCount)341 int flipConePdr( Aig_Man_t *pAig, int directive, int targetCSPropertyIndex, int safetyInvariantPOIndex, int absorberCount )
342 {
343 int RetValue, i;
344 Aig_Obj_t *pObjTargetPo;
345 Aig_Man_t *pAigDupl;
346 Pdr_Par_t Pars, * pPars = &Pars;
347 Abc_Cex_t * pCex = NULL;
348
349 char *fileName;
350
351 fileName = (char *)malloc(sizeof(char) * 50);
352 sprintf(fileName, "%s_%d.%s", "kLive", absorberCount, "blif" );
353
354 if( directive == kCS_WITH_SAFETY_INVARIANTS || directive == kCS_WITH_SAFETY_AND_DCS_INVARIANTS || directive == kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS )
355 {
356 assert( safetyInvariantPOIndex != -1 );
357 modifyAigToApplySafetyInvar(pAig, targetCSPropertyIndex, safetyInvariantPOIndex);
358 }
359
360 pAigDupl = pAig;
361 pAig = Aig_ManDupSimple( pAigDupl );
362
363 for( i=0; i<Saig_ManPoNum(pAig); i++ )
364 {
365 pObjTargetPo = Aig_ManCo( pAig, i );
366 Aig_ObjChild0Flip( pObjTargetPo );
367 }
368
369 Pdr_ManSetDefaultParams( pPars );
370 pPars->fVerbose = 1;
371 pPars->fNotVerbose = 1;
372 pPars->fSolveAll = 1;
373 pAig->vSeqModelVec = NULL;
374
375 Aig_ManCleanup( pAig );
376 assert( Aig_ManCheck( pAig ) );
377
378 Pdr_ManSolve( pAig, pPars );
379
380 if( pAig->vSeqModelVec )
381 {
382 pCex = (Abc_Cex_t *)Vec_PtrEntry( pAig->vSeqModelVec, targetCSPropertyIndex );
383 if( pCex == NULL )
384 {
385 RetValue = 1;
386 }
387 else
388 RetValue = 0;
389 }
390 else
391 {
392 RetValue = -1;
393 exit(0);
394 }
395
396 free(fileName);
397
398 for( i=0; i<Saig_ManPoNum(pAig); i++ )
399 {
400 pObjTargetPo = Aig_ManCo( pAig, i );
401 Aig_ObjChild0Flip( pObjTargetPo );
402 }
403
404 Aig_ManStop( pAig );
405 return RetValue;
406 }
407
408 //unused function
409 #if 0
410 int read0LiveIndex( Abc_Ntk_t *pNtk )
411 {
412 Abc_Obj_t *pObj;
413 int i;
414
415 Abc_NtkForEachPo( pNtk, pObj, i )
416 {
417 if( strstr( Abc_ObjName( pObj ), "0Liveness_" ) != NULL )
418 return i;
419 }
420
421 return -1;
422 }
423 #endif
424
collectSafetyInvariantPOIndex(Abc_Ntk_t * pNtk)425 int collectSafetyInvariantPOIndex(Abc_Ntk_t *pNtk)
426 {
427 Abc_Obj_t *pObj;
428 int i;
429
430 Abc_NtkForEachPo( pNtk, pObj, i )
431 {
432 if( strstr( Abc_ObjName( pObj ), "csSafetyInvar_" ) != NULL )
433 return i;
434 }
435
436 return -1;
437 }
438
collectUserGivenDisjunctiveMonotoneSignals(Abc_Ntk_t * pNtk)439 Vec_Ptr_t *collectUserGivenDisjunctiveMonotoneSignals( Abc_Ntk_t *pNtk )
440 {
441 Abc_Obj_t *pObj;
442 int i;
443 Vec_Ptr_t *monotoneVector;
444 Vec_Int_t *newIntVector;
445
446 monotoneVector = Vec_PtrAlloc(0);
447 Abc_NtkForEachPo( pNtk, pObj, i )
448 {
449 if( strstr( Abc_ObjName( pObj ), "csLevel1Stabil_" ) != NULL )
450 {
451 newIntVector = createSingletonIntVector(i);
452 Vec_PtrPush(monotoneVector, newIntVector);
453 }
454 }
455
456 if( Vec_PtrSize(monotoneVector) > 0 )
457 return monotoneVector;
458 else
459 return NULL;
460
461 }
462
deallocateMasterBarrierDisjunctInt(Vec_Ptr_t * vMasterBarrierDisjunctsArg)463 void deallocateMasterBarrierDisjunctInt(Vec_Ptr_t *vMasterBarrierDisjunctsArg)
464 {
465 Vec_Int_t *vInt;
466 int i;
467
468 if(vMasterBarrierDisjunctsArg)
469 {
470 Vec_PtrForEachEntry(Vec_Int_t *, vMasterBarrierDisjunctsArg, vInt, i)
471 {
472 Vec_IntFree(vInt);
473 }
474 Vec_PtrFree(vMasterBarrierDisjunctsArg);
475 }
476 }
477
deallocateMasterBarrierDisjunctVecPtrVecInt(Vec_Ptr_t * vMasterBarrierDisjunctsArg)478 void deallocateMasterBarrierDisjunctVecPtrVecInt(Vec_Ptr_t *vMasterBarrierDisjunctsArg)
479 {
480 Vec_Int_t *vInt;
481 Vec_Ptr_t *vPtr;
482 int i, j, k, iElem;
483
484 if(vMasterBarrierDisjunctsArg)
485 {
486 Vec_PtrForEachEntry(Vec_Ptr_t *, vMasterBarrierDisjunctsArg, vPtr, i)
487 {
488 assert(vPtr);
489 Vec_PtrForEachEntry( Vec_Int_t *, vPtr, vInt, j )
490 {
491 //Vec_IntFree(vInt);
492 Vec_IntForEachEntry( vInt, iElem, k )
493 printf("%d - ", iElem);
494 //printf("Chung Chang j = %d\n", j);
495 }
496 Vec_PtrFree(vPtr);
497 }
498 Vec_PtrFree(vMasterBarrierDisjunctsArg);
499 }
500 }
501
getVecOfVecFairness(FILE * fp)502 Vec_Ptr_t *getVecOfVecFairness(FILE *fp)
503 {
504 Vec_Ptr_t *masterVector = Vec_PtrAlloc(0);
505 //Vec_Ptr_t *currSignalVector;
506 char stringBuffer[100];
507 //int i;
508
509 while(fgets(stringBuffer, 50, fp))
510 {
511 if(strstr(stringBuffer, ":"))
512 {
513
514 }
515 else
516 {
517
518 }
519 }
520
521 return masterVector;
522 }
523
524
Abc_CommandCS_kLiveness(Abc_Frame_t * pAbc,int argc,char ** argv)525 int Abc_CommandCS_kLiveness( Abc_Frame_t * pAbc, int argc, char ** argv )
526 {
527 Abc_Ntk_t * pNtk, * pNtkTemp;
528 Aig_Man_t * pAig, *pAigCS, *pAigCSNew;
529 int absorberCount;
530 int absorberLimit = 500;
531 int RetValue;
532 int liveIndex_0 = -1, liveIndex_k = -1;
533 int fVerbose = 1;
534 int directive = -1;
535 int c;
536 int safetyInvariantPO = -1;
537 abctime beginTime, endTime;
538 double time_spent;
539 Vec_Ptr_t *vMasterBarrierDisjuncts = NULL;
540 Aig_Man_t *pWorkingAig;
541 //FILE *fp;
542
543 pNtk = Abc_FrameReadNtk(pAbc);
544
545 //fp = fopen("propFile.txt", "r");
546 //if( fp )
547 // getVecOfVecFairness(fp);
548 //exit(0);
549
550 /*************************************************
551 Extraction of Command Line Argument
552 *************************************************/
553 if( argc == 1 )
554 {
555 assert( directive == -1 );
556 directive = SIMPLE_kCS;
557 }
558 else
559 {
560 Extra_UtilGetoptReset();
561 while ( ( c = Extra_UtilGetopt( argc, argv, "cmCgh" ) ) != EOF )
562 {
563 switch( c )
564 {
565 case 'c':
566 directive = kCS_WITH_SAFETY_INVARIANTS;
567 break;
568 case 'm':
569 directive = kCS_WITH_DISCOVER_MONOTONE_SIGNALS;
570 break;
571 case 'C':
572 directive = kCS_WITH_SAFETY_AND_DCS_INVARIANTS;
573 break;
574 case 'g':
575 directive = kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS;
576 break;
577 case 'h':
578 goto usage;
579 break;
580 default:
581 goto usage;
582 }
583 }
584 }
585 /*************************************************
586 Extraction of Command Line Argument Ends
587 *************************************************/
588
589 if( !Abc_NtkIsStrash( pNtk ) )
590 {
591 printf("The input network was not strashed, strashing....\n");
592 pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
593 pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
594 }
595 else
596 {
597 pAig = Abc_NtkToDar( pNtk, 0, 1 );
598 pNtkTemp = pNtk;
599 }
600
601 if( directive == kCS_WITH_SAFETY_INVARIANTS )
602 {
603 safetyInvariantPO = collectSafetyInvariantPOIndex(pNtkTemp);
604 assert( safetyInvariantPO != -1 );
605 }
606
607 if(directive == kCS_WITH_DISCOVER_MONOTONE_SIGNALS)
608 {
609 beginTime = Abc_Clock();
610 vMasterBarrierDisjuncts = findDisjunctiveMonotoneSignals( pNtk );
611 endTime = Abc_Clock();
612 time_spent = (double)(endTime - beginTime)/CLOCKS_PER_SEC;
613 printf("pre-processing time = %f\n",time_spent);
614 return 0;
615 }
616
617 if(directive == kCS_WITH_SAFETY_AND_DCS_INVARIANTS)
618 {
619 safetyInvariantPO = collectSafetyInvariantPOIndex(pNtkTemp);
620 assert( safetyInvariantPO != -1 );
621
622 beginTime = Abc_Clock();
623 vMasterBarrierDisjuncts = findDisjunctiveMonotoneSignals( pNtk );
624 endTime = Abc_Clock();
625 time_spent = (double)(endTime - beginTime)/CLOCKS_PER_SEC;
626 printf("pre-processing time = %f\n",time_spent);
627
628 assert( vMasterBarrierDisjuncts != NULL );
629 assert( Vec_PtrSize(vMasterBarrierDisjuncts) > 0 );
630 }
631
632 if(directive == kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS)
633 {
634 safetyInvariantPO = collectSafetyInvariantPOIndex(pNtkTemp);
635 assert( safetyInvariantPO != -1 );
636
637 beginTime = Abc_Clock();
638 vMasterBarrierDisjuncts = collectUserGivenDisjunctiveMonotoneSignals( pNtk );
639 endTime = Abc_Clock();
640 time_spent = (double)(endTime - beginTime)/CLOCKS_PER_SEC;
641 printf("pre-processing time = %f\n",time_spent);
642
643 assert( vMasterBarrierDisjuncts != NULL );
644 assert( Vec_PtrSize(vMasterBarrierDisjuncts) > 0 );
645 }
646
647 if(directive == kCS_WITH_SAFETY_AND_DCS_INVARIANTS || directive == kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS)
648 {
649 assert( vMasterBarrierDisjuncts != NULL );
650 pWorkingAig = generateWorkingAigWithDSC( pAig, pNtk, &liveIndex_0, vMasterBarrierDisjuncts );
651 pAigCS = introduceAbsorberLogic(pWorkingAig, &liveIndex_0, &liveIndex_k, 0);
652 }
653 else
654 {
655 pWorkingAig = generateWorkingAig( pAig, pNtk, &liveIndex_0 );
656 pAigCS = introduceAbsorberLogic(pWorkingAig, &liveIndex_0, &liveIndex_k, 0);
657 }
658
659 Aig_ManStop(pWorkingAig);
660
661 for( absorberCount=1; absorberCount<absorberLimit; absorberCount++ )
662 {
663 //printf( "\nindex of the liveness output = %d\n", liveIndex_k );
664 RetValue = flipConePdr( pAigCS, directive, liveIndex_k, safetyInvariantPO, absorberCount );
665
666 if ( RetValue == 1 )
667 {
668 Abc_Print( 1, "k = %d, Property proved\n", absorberCount );
669 break;
670 }
671 else if ( RetValue == 0 )
672 {
673 if( fVerbose )
674 {
675 Abc_Print( 1, "k = %d, Property DISPROVED\n", absorberCount );
676 }
677 }
678 else if ( RetValue == -1 )
679 {
680 Abc_Print( 1, "Property UNDECIDED with k = %d.\n", absorberCount );
681 }
682 else
683 assert( 0 );
684
685 pAigCSNew = introduceAbsorberLogic(pAigCS, &liveIndex_0, &liveIndex_k, absorberCount);
686 Aig_ManStop(pAigCS);
687 pAigCS = pAigCSNew;
688 }
689
690 Aig_ManStop(pAigCS);
691 Aig_ManStop(pAig);
692
693 if(directive == kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS)
694 {
695 deallocateMasterBarrierDisjunctInt(vMasterBarrierDisjuncts);
696 }
697 else
698 {
699 //if(vMasterBarrierDisjuncts)
700 // Vec_PtrFree(vMasterBarrierDisjuncts);
701 //deallocateMasterBarrierDisjunctVecPtrVecInt(vMasterBarrierDisjuncts);
702 deallocateMasterBarrierDisjunctInt(vMasterBarrierDisjuncts);
703 }
704 return 0;
705
706 usage:
707 fprintf( stdout, "usage: kcs [-cmgCh]\n" );
708 fprintf( stdout, "\timplements Claessen-Sorensson's k-Liveness algorithm\n" );
709 fprintf( stdout, "\t-c : verification with constraints, looks for POs prefixed with csSafetyInvar_\n");
710 fprintf( stdout, "\t-m : discovers monotone signals\n");
711 fprintf( stdout, "\t-g : verification with user-supplied barriers, looks for POs prefixed with csLevel1Stabil_\n");
712 fprintf( stdout, "\t-C : verification with discovered monotone signals\n");
713 fprintf( stdout, "\t-h : print usage\n");
714 return 1;
715
716 }
717
Abc_CommandNChooseK(Abc_Frame_t * pAbc,int argc,char ** argv)718 int Abc_CommandNChooseK( Abc_Frame_t * pAbc, int argc, char ** argv )
719 {
720 Abc_Ntk_t * pNtk, * pNtkTemp, *pNtkCombStabil;
721 Aig_Man_t * pAig, *pAigCombStabil;
722 int directive = -1;
723 int c;
724 int parameterizedCombK;
725
726 pNtk = Abc_FrameReadNtk(pAbc);
727
728
729 /*************************************************
730 Extraction of Command Line Argument
731 *************************************************/
732 if( argc == 1 )
733 {
734 assert( directive == -1 );
735 directive = SIMPLE_kCS;
736 }
737 else
738 {
739 Extra_UtilGetoptReset();
740 while ( ( c = Extra_UtilGetopt( argc, argv, "cmCgh" ) ) != EOF )
741 {
742 switch( c )
743 {
744 case 'c':
745 directive = kCS_WITH_SAFETY_INVARIANTS;
746 break;
747 case 'm':
748 directive = kCS_WITH_DISCOVER_MONOTONE_SIGNALS;
749 break;
750 case 'C':
751 directive = kCS_WITH_SAFETY_AND_DCS_INVARIANTS;
752 break;
753 case 'g':
754 directive = kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS;
755 break;
756 case 'h':
757 goto usage;
758 break;
759 default:
760 goto usage;
761 }
762 }
763 }
764 /*************************************************
765 Extraction of Command Line Argument Ends
766 *************************************************/
767
768 if( !Abc_NtkIsStrash( pNtk ) )
769 {
770 printf("The input network was not strashed, strashing....\n");
771 pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
772 pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
773 }
774 else
775 {
776 pAig = Abc_NtkToDar( pNtk, 0, 1 );
777 pNtkTemp = pNtk;
778 }
779
780 /**********************Code for generation of nCk outputs**/
781 //combCount = countCombination(1000, 3);
782 //pAigCombStabil = generateDisjunctiveTester( pNtk, pAig, 7, 2 );
783 printf("Enter parameterizedCombK = " );
784 if( scanf("%d", ¶meterizedCombK) != 1 )
785 {
786 printf("\nFailed to read integer!\n");
787 return 0;
788 }
789 printf("\n");
790
791 pAigCombStabil = generateGeneralDisjunctiveTester( pNtk, pAig, parameterizedCombK );
792 Aig_ManPrintStats(pAigCombStabil);
793 pNtkCombStabil = Abc_NtkFromAigPhase( pAigCombStabil );
794 pNtkCombStabil->pName = Abc_UtilStrsav( pAigCombStabil->pName );
795 if ( !Abc_NtkCheck( pNtkCombStabil ) )
796 fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" );
797 Abc_FrameSetCurrentNetwork( pAbc, pNtkCombStabil );
798
799 Aig_ManStop( pAigCombStabil );
800 Aig_ManStop( pAig );
801
802 return 1;
803 //printf("\ncombCount = %d\n", combCount);
804 //exit(0);
805 /**********************************************************/
806
807 usage:
808 fprintf( stdout, "usage: nck [-cmgCh]\n" );
809 fprintf( stdout, "\tgenerates combinatorial signals for stabilization\n" );
810 fprintf( stdout, "\t-h : print usage\n");
811 return 1;
812
813 }
814
815
816 ABC_NAMESPACE_IMPL_END
817