1 /**CFile****************************************************************
2
3 FileName [disjunctiveMonotone.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Liveness property checking.]
8
9 Synopsis [Constraint analysis module for the k-Liveness algorithm
10 invented by Koen Classen, Niklas Sorensson.]
11
12 Author [Sayak Ray]
13
14 Affiliation [UC Berkeley]
15
16 Date [Ver. 1.0. Started - October 31, 2012.]
17
18 ***********************************************************************/
19
20 #include <stdio.h>
21 #include "base/main/main.h"
22 #include "aig/aig/aig.h"
23 #include "aig/saig/saig.h"
24 #include <string.h>
25 #include "base/main/mainInt.h"
26 #include "proof/pdr/pdr.h"
27 #include <time.h>
28
29 ABC_NAMESPACE_IMPL_START
30
31 struct aigPoIndices
32 {
33 int attrPendingSignalIndex;
34 int attrHintSingalBeginningMarker;
35 int attrHintSingalEndMarker;
36 int attrSafetyInvarIndex;
37 };
38
39 extern struct aigPoIndices *allocAigPoIndices();
40 extern void deallocAigPoIndices(struct aigPoIndices *toBeDeletedAigPoIndices);
41 extern int collectSafetyInvariantPOIndex(Abc_Ntk_t *pNtk);
42
43 struct antecedentConsequentVectorsStruct
44 {
45 Vec_Int_t *attrAntecedents;
46 Vec_Int_t *attrConsequentCandidates;
47 };
48
allocAntecedentConsequentVectorsStruct()49 struct antecedentConsequentVectorsStruct *allocAntecedentConsequentVectorsStruct()
50 {
51 struct antecedentConsequentVectorsStruct *newStructure;
52
53 newStructure = (struct antecedentConsequentVectorsStruct *)malloc(sizeof (struct antecedentConsequentVectorsStruct));
54
55 newStructure->attrAntecedents = NULL;
56 newStructure->attrConsequentCandidates = NULL;
57
58 assert( newStructure != NULL );
59 return newStructure;
60 }
61
deallocAntecedentConsequentVectorsStruct(struct antecedentConsequentVectorsStruct * toBeDeleted)62 void deallocAntecedentConsequentVectorsStruct(struct antecedentConsequentVectorsStruct *toBeDeleted)
63 {
64 assert( toBeDeleted != NULL );
65 if(toBeDeleted->attrAntecedents)
66 Vec_IntFree( toBeDeleted->attrAntecedents );
67 if(toBeDeleted->attrConsequentCandidates)
68 Vec_IntFree( toBeDeleted->attrConsequentCandidates );
69 free( toBeDeleted );
70 }
71
createDisjunctiveMonotoneTester(Aig_Man_t * pAig,struct aigPoIndices * aigPoIndicesArg,struct antecedentConsequentVectorsStruct * anteConseVectors,int * startMonotonePropPo)72 Aig_Man_t *createDisjunctiveMonotoneTester(Aig_Man_t *pAig, struct aigPoIndices *aigPoIndicesArg,
73 struct antecedentConsequentVectorsStruct *anteConseVectors, int *startMonotonePropPo)
74 {
75 Aig_Man_t *pNewAig;
76 int iElem, i, nRegCount;
77 int piCopied = 0, liCopied = 0, liCreated = 0, loCopied = 0, loCreated = 0;
78 int poCopied = 0, poCreated = 0;
79 Aig_Obj_t *pObj, *pObjPo, *pObjDriver, *pObjDriverNew, *pObjPendingDriverNew, *pObjPendingAndNextPending;
80 Aig_Obj_t *pPendingFlop, *pObjConseCandFlop, *pObjSafetyInvariantPoDriver;
81 //Vec_Ptr_t *vHintMonotoneLocalDriverNew;
82 Vec_Ptr_t *vConseCandFlopOutput;
83 //Vec_Ptr_t *vHintMonotoneLocalProp;
84
85 Aig_Obj_t *pObjAnteDisjunction, *pObjConsecDriver, *pObjConsecDriverNew, *pObjCandMonotone, *pObjPrevCandMonotone, *pObjMonotonePropDriver;
86 Vec_Ptr_t *vCandMonotoneProp;
87 Vec_Ptr_t *vCandMonotoneFlopInput;
88
89 int pendingSignalIndexLocal = aigPoIndicesArg->attrPendingSignalIndex;
90
91 Vec_Int_t *vAntecedentsLocal = anteConseVectors->attrAntecedents;
92 Vec_Int_t *vConsequentCandidatesLocal = anteConseVectors->attrConsequentCandidates;
93
94 if( vConsequentCandidatesLocal == NULL )
95 return NULL; //no candidates for consequent is provided, hence no need to generate a new AIG
96
97
98 //****************************************************************
99 // Step1: create the new manager
100 // Note: The new manager is created with "2 * Aig_ManObjNumMax(p)"
101 // nodes, but this selection is arbitrary - need to be justified
102 //****************************************************************
103 pNewAig = Aig_ManStart( Aig_ManObjNumMax(pAig) );
104 pNewAig->pName = (char *)malloc( strlen( pAig->pName ) + strlen("_monotone") + 2 );
105 sprintf(pNewAig->pName, "%s_%s", pAig->pName, "monotone");
106 pNewAig->pSpec = NULL;
107
108 //****************************************************************
109 // Step 2: map constant nodes
110 //****************************************************************
111 pObj = Aig_ManConst1( pAig );
112 pObj->pData = Aig_ManConst1( pNewAig );
113
114 //****************************************************************
115 // Step 3: create true PIs
116 //****************************************************************
117 Saig_ManForEachPi( pAig, pObj, i )
118 {
119 piCopied++;
120 pObj->pData = Aig_ObjCreateCi(pNewAig);
121 }
122
123 //****************************************************************
124 // Step 5: create register outputs
125 //****************************************************************
126 Saig_ManForEachLo( pAig, pObj, i )
127 {
128 loCopied++;
129 pObj->pData = Aig_ObjCreateCi(pNewAig);
130 }
131
132 //****************************************************************
133 // Step 6: create "D" register output for PENDING flop
134 //****************************************************************
135 loCreated++;
136 pPendingFlop = Aig_ObjCreateCi( pNewAig );
137
138 //****************************************************************
139 // Step 6.a: create "D" register output for HINT_MONOTONE flop
140 //****************************************************************
141 vConseCandFlopOutput = Vec_PtrAlloc(Vec_IntSize(vConsequentCandidatesLocal));
142 Vec_IntForEachEntry( vConsequentCandidatesLocal, iElem, i )
143 {
144 loCreated++;
145 pObjConseCandFlop = Aig_ObjCreateCi( pNewAig );
146 Vec_PtrPush( vConseCandFlopOutput, pObjConseCandFlop );
147 }
148
149 nRegCount = loCreated + loCopied;
150
151 //********************************************************************
152 // Step 7: create internal nodes
153 //********************************************************************
154 Aig_ManForEachNode( pAig, pObj, i )
155 {
156 pObj->pData = Aig_And( pNewAig, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
157 }
158
159 //********************************************************************
160 // Step 8: mapping appropriate new flop drivers
161 //********************************************************************
162
163 if( aigPoIndicesArg->attrSafetyInvarIndex != -1 )
164 {
165 pObjPo = Aig_ManCo( pAig, aigPoIndicesArg->attrSafetyInvarIndex );
166 pObjDriver = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPo), Aig_ObjFaninC0(pObjPo));
167 pObjDriverNew = !Aig_IsComplement(pObjDriver)?
168 (Aig_Obj_t *)(Aig_Regular(pObjDriver)->pData) :
169 Aig_Not((Aig_Obj_t *)(Aig_Regular(pObjDriver)->pData));
170 pObjSafetyInvariantPoDriver = pObjDriverNew;
171 }
172 else
173 pObjSafetyInvariantPoDriver = Aig_ManConst1(pNewAig);
174
175 pObjPo = Aig_ManCo( pAig, pendingSignalIndexLocal );
176 pObjDriver = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPo), Aig_ObjFaninC0(pObjPo));
177 pObjPendingDriverNew = !Aig_IsComplement(pObjDriver)?
178 (Aig_Obj_t *)(Aig_Regular(pObjDriver)->pData) :
179 Aig_Not((Aig_Obj_t *)(Aig_Regular(pObjDriver)->pData));
180
181 pObjPendingAndNextPending = Aig_And( pNewAig, pObjPendingDriverNew, pPendingFlop );
182
183 pObjAnteDisjunction = Aig_Not(Aig_ManConst1( pNewAig ));
184 if( vAntecedentsLocal )
185 {
186 Vec_IntForEachEntry( vAntecedentsLocal, iElem, i )
187 {
188 pObjPo = Aig_ManCo( pAig, iElem );
189 pObjDriver = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPo), Aig_ObjFaninC0(pObjPo));
190 pObjDriverNew = !Aig_IsComplement(pObjDriver)?
191 (Aig_Obj_t *)(Aig_Regular(pObjDriver)->pData) :
192 Aig_Not((Aig_Obj_t *)(Aig_Regular(pObjDriver)->pData));
193
194 pObjAnteDisjunction = Aig_Or( pNewAig, pObjDriverNew, pObjAnteDisjunction );
195 }
196 }
197
198 vCandMonotoneProp = Vec_PtrAlloc( Vec_IntSize(vConsequentCandidatesLocal) );
199 vCandMonotoneFlopInput = Vec_PtrAlloc( Vec_IntSize(vConsequentCandidatesLocal) );
200 Vec_IntForEachEntry( vConsequentCandidatesLocal, iElem, i )
201 {
202 pObjPo = Aig_ManCo( pAig, iElem );
203 pObjConsecDriver = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPo), Aig_ObjFaninC0(pObjPo));
204 pObjConsecDriverNew = !Aig_IsComplement(pObjConsecDriver)?
205 (Aig_Obj_t *)(Aig_Regular(pObjConsecDriver)->pData) :
206 Aig_Not((Aig_Obj_t *)(Aig_Regular(pObjConsecDriver)->pData));
207
208 pObjCandMonotone = Aig_Or( pNewAig, pObjConsecDriverNew, pObjAnteDisjunction );
209 pObjPrevCandMonotone = (Aig_Obj_t *)(Vec_PtrEntry( vConseCandFlopOutput, i ));
210 pObjMonotonePropDriver = Aig_Or( pNewAig, Aig_Not( Aig_And( pNewAig, pObjPendingAndNextPending, pObjPrevCandMonotone ) ),
211 pObjCandMonotone );
212
213 //Conjunting safety invar
214 pObjMonotonePropDriver = Aig_And( pNewAig, pObjMonotonePropDriver, pObjSafetyInvariantPoDriver );
215
216 Vec_PtrPush( vCandMonotoneFlopInput, pObjCandMonotone );
217 Vec_PtrPush( vCandMonotoneProp, pObjMonotonePropDriver );
218 }
219
220 //********************************************************************
221 // Step 9: create primary outputs
222 //********************************************************************
223 Saig_ManForEachPo( pAig, pObj, i )
224 {
225 poCopied++;
226 pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
227 }
228
229 *startMonotonePropPo = i;
230 Vec_PtrForEachEntry( Aig_Obj_t *, vCandMonotoneProp, pObj, i )
231 {
232 poCreated++;
233 pObjPo = Aig_ObjCreateCo( pNewAig, pObj );
234 }
235
236 //********************************************************************
237 // Step 9: create latch inputs
238 //********************************************************************
239
240 Saig_ManForEachLi( pAig, pObj, i )
241 {
242 liCopied++;
243 Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
244 }
245
246 //********************************************************************
247 // Step 9.a: create latch input for PENDING_FLOP
248 //********************************************************************
249
250 liCreated++;
251 Aig_ObjCreateCo( pNewAig, pObjPendingDriverNew );
252
253 //********************************************************************
254 // Step 9.b: create latch input for MONOTONE_FLOP
255 //********************************************************************
256
257 Vec_PtrForEachEntry( Aig_Obj_t *, vCandMonotoneFlopInput, pObj, i )
258 {
259 liCreated++;
260 Aig_ObjCreateCo( pNewAig, pObj );
261 }
262
263 Aig_ManSetRegNum( pNewAig, nRegCount );
264 Aig_ManCleanup( pNewAig );
265
266 assert( Aig_ManCheck( pNewAig ) );
267 assert( loCopied + loCreated == liCopied + liCreated );
268
269 Vec_PtrFree(vConseCandFlopOutput);
270 Vec_PtrFree(vCandMonotoneProp);
271 Vec_PtrFree(vCandMonotoneFlopInput);
272 return pNewAig;
273 }
274
findNewDisjunctiveMonotone(Aig_Man_t * pAig,struct aigPoIndices * aigPoIndicesArg,struct antecedentConsequentVectorsStruct * anteConseVectors)275 Vec_Int_t *findNewDisjunctiveMonotone( Aig_Man_t *pAig, struct aigPoIndices *aigPoIndicesArg, struct antecedentConsequentVectorsStruct *anteConseVectors )
276 {
277 Aig_Man_t *pAigNew;
278 Aig_Obj_t *pObjTargetPo;
279 int poMarker;
280 //int i, RetValue, poSerialNum;
281 int i, poSerialNum;
282 Pdr_Par_t Pars, * pPars = &Pars;
283 //Abc_Cex_t * pCex = NULL;
284 Vec_Int_t *vMonotoneIndex;
285 //char fileName[20];
286 Abc_Cex_t * cexElem;
287
288 int pendingSignalIndexLocal = aigPoIndicesArg->attrPendingSignalIndex;
289
290 pAigNew = createDisjunctiveMonotoneTester(pAig, aigPoIndicesArg, anteConseVectors, &poMarker );
291
292 //printf("enter an integer : ");
293 //waitForInteger = getchar();
294 //putchar(waitForInteger);
295
296 vMonotoneIndex = Vec_IntAlloc(0);
297
298 for( i=0; i<Saig_ManPoNum(pAigNew); i++ )
299 {
300 pObjTargetPo = Aig_ManCo( pAigNew, i );
301 Aig_ObjChild0Flip( pObjTargetPo );
302 }
303
304 Pdr_ManSetDefaultParams( pPars );
305 pPars->fVerbose = 0;
306 pPars->fNotVerbose = 1;
307 pPars->fSolveAll = 1;
308 pAigNew->vSeqModelVec = NULL;
309 Pdr_ManSolve( pAigNew, pPars );
310
311 if( pAigNew->vSeqModelVec )
312 {
313 Vec_PtrForEachEntry( Abc_Cex_t *, pAigNew->vSeqModelVec, cexElem, i )
314 {
315 if( cexElem == NULL && i >= pendingSignalIndexLocal + 1)
316 {
317 poSerialNum = i - (pendingSignalIndexLocal + 1);
318 Vec_IntPush( vMonotoneIndex, Vec_IntEntry( anteConseVectors->attrConsequentCandidates, poSerialNum ));
319 }
320 }
321 }
322 for( i=0; i<Saig_ManPoNum(pAigNew); i++ )
323 {
324 pObjTargetPo = Aig_ManCo( pAigNew, i );
325 Aig_ObjChild0Flip( pObjTargetPo );
326 }
327
328 //if(pAigNew->vSeqModelVec)
329 // Vec_PtrFree(pAigNew->vSeqModelVec);
330
331 Aig_ManStop(pAigNew);
332
333 if( Vec_IntSize( vMonotoneIndex ) > 0 )
334 {
335 return vMonotoneIndex;
336 }
337 else
338 {
339 Vec_IntFree(vMonotoneIndex);
340 return NULL;
341 }
342 }
343
updateAnteConseVectors(struct antecedentConsequentVectorsStruct * anteConse)344 Vec_Int_t *updateAnteConseVectors(struct antecedentConsequentVectorsStruct *anteConse )
345 {
346 Vec_Int_t *vCandMonotone;
347 int iElem, i;
348
349 //if( vKnownMonotone == NULL || Vec_IntSize(vKnownMonotone) <= 0 )
350 // return vHintMonotone;
351 if( anteConse->attrAntecedents == NULL || Vec_IntSize(anteConse->attrAntecedents) <= 0 )
352 return anteConse->attrConsequentCandidates;
353 vCandMonotone = Vec_IntAlloc(0);
354 Vec_IntForEachEntry( anteConse->attrConsequentCandidates, iElem, i )
355 {
356 if( Vec_IntFind( anteConse->attrAntecedents, iElem ) == -1 )
357 Vec_IntPush( vCandMonotone, iElem );
358 }
359
360 return vCandMonotone;
361 }
362
vectorDifference(Vec_Int_t * A,Vec_Int_t * B)363 Vec_Int_t *vectorDifference(Vec_Int_t *A, Vec_Int_t *B)
364 {
365 Vec_Int_t *C;
366 int iElem, i;
367
368 C = Vec_IntAlloc(0);
369 Vec_IntForEachEntry( A, iElem, i )
370 {
371 if( Vec_IntFind( B, iElem ) == -1 )
372 {
373 Vec_IntPush( C, iElem );
374 }
375 }
376
377 return C;
378 }
379
createSingletonIntVector(int iElem)380 Vec_Int_t *createSingletonIntVector( int iElem )
381 {
382 Vec_Int_t *myVec = Vec_IntAlloc(1);
383
384 Vec_IntPush(myVec, iElem);
385 return myVec;
386 }
387
388 #if 0
389 Vec_Ptr_t *generateDisjuntiveMonotone_rec()
390 {
391 nextLevelSignals = ;
392 if level is not exhausted
393 for all x \in nextLevelSignals
394 {
395 append x in currAntecendent
396 recond it as a monotone predicate
397 resurse with level - 1
398 }
399 }
400 #endif
401
402 #if 0
403 Vec_Ptr_t *generateDisjuntiveMonotoneLevels(Aig_Man_t *pAig,
404 struct aigPoIndices *aigPoIndicesInstance,
405 struct antecedentConsequentVectorsStruct *anteConsecInstanceOrig,
406 int level )
407 {
408 Vec_Int_t *firstLevelMonotone;
409 Vec_Int_t *currVecInt;
410 Vec_Ptr_t *hierarchyList;
411 int iElem, i;
412
413 assert( level >= 1 );
414 firstLevelMonotone = findNewDisjunctiveMonotone( pAig, aigPoIndicesInstance, anteConsecInstance );
415 if( firstLevelMonotone == NULL || Vec_IntSize(firstLevelMonotone) <= 0 )
416 return NULL;
417
418 hierarchyList = Vec_PtrAlloc(Vec_IntSize(firstLevelMonotone));
419
420 Vec_IntForEachEntry( firstLevelMonotone, iElem, i )
421 {
422 currVecInt = createSingletonIntVector( iElem );
423 Vec_PtrPush( hierarchyList, currVecInt );
424 }
425
426 if( level > 1 )
427 {
428 Vec_IntForEachEntry( firstLevelMonotone, iElem, i )
429 {
430 currVecInt = (Vec_Int_t *)Vec_PtrEntry( hierarchyList, i );
431
432
433 }
434 }
435
436 return hierarchyList;
437 }
438 #endif
439
Vec_IntPushUniqueLocal(Vec_Int_t * p,int Entry)440 int Vec_IntPushUniqueLocal( Vec_Int_t * p, int Entry )
441 {
442 int i;
443 for ( i = 0; i < p->nSize; i++ )
444 if ( p->pArray[i] == Entry )
445 return 1;
446 Vec_IntPush( p, Entry );
447 return 0;
448 }
449
findNextLevelDisjunctiveMonotone(Aig_Man_t * pAig,struct aigPoIndices * aigPoIndicesInstance,struct antecedentConsequentVectorsStruct * anteConsecInstance,Vec_Ptr_t * previousMonotoneVectors)450 Vec_Ptr_t *findNextLevelDisjunctiveMonotone(
451 Aig_Man_t *pAig,
452 struct aigPoIndices *aigPoIndicesInstance,
453 struct antecedentConsequentVectorsStruct *anteConsecInstance,
454 Vec_Ptr_t *previousMonotoneVectors )
455 {
456 Vec_Ptr_t *newLevelPtrVec;
457 Vec_Int_t *vElem, *vNewDisjunctVector, *newDisjunction;
458 int i, j, iElem;
459 struct antecedentConsequentVectorsStruct *anteConsecInstanceLocal;
460 Vec_Int_t *vUnionPrevMonotoneVector, *vDiffVector;
461
462 newLevelPtrVec = Vec_PtrAlloc(0);
463 vUnionPrevMonotoneVector = Vec_IntAlloc(0);
464 Vec_PtrForEachEntry(Vec_Int_t *, previousMonotoneVectors, vElem, i)
465 Vec_IntForEachEntry( vElem, iElem, j )
466 Vec_IntPushUniqueLocal( vUnionPrevMonotoneVector, iElem );
467
468 Vec_PtrForEachEntry(Vec_Int_t *, previousMonotoneVectors, vElem, i)
469 {
470 anteConsecInstanceLocal = allocAntecedentConsequentVectorsStruct();
471
472 anteConsecInstanceLocal->attrAntecedents = Vec_IntDup(vElem);
473 vDiffVector = vectorDifference( anteConsecInstance->attrConsequentCandidates, vUnionPrevMonotoneVector);
474 anteConsecInstanceLocal->attrConsequentCandidates = vDiffVector;
475 assert( vDiffVector );
476
477 //printf("Calling target function %d\n", i);
478 vNewDisjunctVector = findNewDisjunctiveMonotone( pAig, aigPoIndicesInstance, anteConsecInstanceLocal );
479
480 if( vNewDisjunctVector )
481 {
482 Vec_IntForEachEntry(vNewDisjunctVector, iElem, j)
483 {
484 newDisjunction = Vec_IntDup(vElem);
485 Vec_IntPush( newDisjunction, iElem );
486 Vec_PtrPush( newLevelPtrVec, newDisjunction );
487 }
488 Vec_IntFree(vNewDisjunctVector);
489 }
490 deallocAntecedentConsequentVectorsStruct( anteConsecInstanceLocal );
491 }
492
493 Vec_IntFree(vUnionPrevMonotoneVector);
494
495 return newLevelPtrVec;
496 }
497
printAllIntVectors(Vec_Ptr_t * vDisjunctions,Abc_Ntk_t * pNtk,char * fileName)498 void printAllIntVectors(Vec_Ptr_t *vDisjunctions, Abc_Ntk_t *pNtk, char *fileName)
499 {
500 Vec_Int_t *vElem;
501 int i, j, iElem;
502 char *name, *hintSubStr;
503 FILE *fp;
504
505 fp = fopen( fileName, "a" );
506
507 Vec_PtrForEachEntry(Vec_Int_t *, vDisjunctions, vElem, i)
508 {
509 fprintf(fp, "( ");
510 Vec_IntForEachEntry( vElem, iElem, j )
511 {
512 name = Abc_ObjName( Abc_NtkPo(pNtk, iElem));
513 hintSubStr = strstr( name, "hint");
514 assert( hintSubStr );
515 fprintf(fp, "%s", hintSubStr);
516 if( j < Vec_IntSize(vElem) - 1 )
517 {
518 fprintf(fp, " || ");
519 }
520 else
521 {
522 fprintf(fp, " )\n");
523 }
524 }
525 }
526 fclose(fp);
527 }
528
printAllIntVectorsStabil(Vec_Ptr_t * vDisjunctions,Abc_Ntk_t * pNtk,char * fileName)529 void printAllIntVectorsStabil(Vec_Ptr_t *vDisjunctions, Abc_Ntk_t *pNtk, char *fileName)
530 {
531 Vec_Int_t *vElem;
532 int i, j, iElem;
533 char *name, *hintSubStr;
534 FILE *fp;
535
536 fp = fopen( fileName, "a" );
537
538 Vec_PtrForEachEntry(Vec_Int_t *, vDisjunctions, vElem, i)
539 {
540 printf("INT[%d] : ( ", i);
541 fprintf(fp, "( ");
542 Vec_IntForEachEntry( vElem, iElem, j )
543 {
544 name = Abc_ObjName( Abc_NtkPo(pNtk, iElem));
545 hintSubStr = strstr( name, "csLevel1Stabil");
546 assert( hintSubStr );
547 printf("%s", hintSubStr);
548 fprintf(fp, "%s", hintSubStr);
549 if( j < Vec_IntSize(vElem) - 1 )
550 {
551 printf(" || ");
552 fprintf(fp, " || ");
553 }
554 else
555 {
556 printf(" )\n");
557 fprintf(fp, " )\n");
558 }
559 }
560 //printf(")\n");
561 }
562 fclose(fp);
563 }
564
565
appendVecToMasterVecInt(Vec_Ptr_t * masterVec,Vec_Ptr_t * candVec)566 void appendVecToMasterVecInt(Vec_Ptr_t *masterVec, Vec_Ptr_t *candVec )
567 {
568 int i;
569 Vec_Int_t *vCand;
570 Vec_Int_t *vNewIntVec;
571
572 assert(masterVec != NULL);
573 assert(candVec != NULL);
574 Vec_PtrForEachEntry( Vec_Int_t *, candVec, vCand, i )
575 {
576 vNewIntVec = Vec_IntDup(vCand);
577 Vec_PtrPush(masterVec, vNewIntVec);
578 }
579 }
580
deallocateVecOfIntVec(Vec_Ptr_t * vecOfIntVec)581 void deallocateVecOfIntVec( Vec_Ptr_t *vecOfIntVec )
582 {
583 Vec_Int_t *vInt;
584 int i;
585
586 if( vecOfIntVec )
587 {
588 Vec_PtrForEachEntry( Vec_Int_t *, vecOfIntVec, vInt, i )
589 {
590 Vec_IntFree( vInt );
591 }
592 Vec_PtrFree(vecOfIntVec);
593 }
594 }
595
findDisjunctiveMonotoneSignals(Abc_Ntk_t * pNtk)596 Vec_Ptr_t *findDisjunctiveMonotoneSignals( Abc_Ntk_t *pNtk )
597 {
598 Aig_Man_t *pAig;
599 Vec_Int_t *vCandidateMonotoneSignals;
600 Vec_Int_t *vKnownMonotoneSignals;
601 //Vec_Int_t *vKnownMonotoneSignalsRoundTwo;
602 //Vec_Int_t *vOldConsequentVector;
603 //Vec_Int_t *vRemainingConsecVector;
604 int i;
605 int iElem;
606 int pendingSignalIndex;
607 Abc_Ntk_t *pNtkTemp;
608 int hintSingalBeginningMarker;
609 int hintSingalEndMarker;
610 struct aigPoIndices *aigPoIndicesInstance;
611 //struct monotoneVectorsStruct *monotoneVectorsInstance;
612 struct antecedentConsequentVectorsStruct *anteConsecInstance;
613 //Aig_Obj_t *safetyDriverNew;
614 Vec_Int_t *newIntVec;
615 Vec_Ptr_t *levelOneMonotne, *levelTwoMonotne;
616 //Vec_Ptr_t *levelThreeMonotne;
617
618 Vec_Ptr_t *vMasterDisjunctions;
619
620 extern int findPendingSignal(Abc_Ntk_t *pNtk);
621 extern Vec_Int_t *findHintOutputs(Abc_Ntk_t *pNtk);
622 extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
623
624 //system("rm monotone.dat");
625
626 /*******************************************/
627 //Finding the PO index of the pending signal
628 /*******************************************/
629 pendingSignalIndex = findPendingSignal(pNtk);
630 if( pendingSignalIndex == -1 )
631 {
632 printf("\nNo Pending Signal Found\n");
633 return NULL;
634 }
635 //else
636 //printf("Po[%d] = %s\n", pendingSignalIndex, Abc_ObjName( Abc_NtkPo(pNtk, pendingSignalIndex) ) );
637
638 /*******************************************/
639 //Finding the PO indices of all hint signals
640 /*******************************************/
641 vCandidateMonotoneSignals = findHintOutputs(pNtk);
642 if( vCandidateMonotoneSignals == NULL )
643 return NULL;
644 else
645 {
646 //Vec_IntForEachEntry( vCandidateMonotoneSignals, iElem, i )
647 // printf("Po[%d] = %s\n", iElem, Abc_ObjName( Abc_NtkPo(pNtk, iElem) ) );
648 hintSingalBeginningMarker = Vec_IntEntry( vCandidateMonotoneSignals, 0 );
649 hintSingalEndMarker = Vec_IntEntry( vCandidateMonotoneSignals, Vec_IntSize(vCandidateMonotoneSignals) - 1 );
650 }
651
652 /**********************************************/
653 //Allocating "struct" with necessary parameters
654 /**********************************************/
655 aigPoIndicesInstance = allocAigPoIndices();
656 aigPoIndicesInstance->attrPendingSignalIndex = pendingSignalIndex;
657 aigPoIndicesInstance->attrHintSingalBeginningMarker = hintSingalBeginningMarker;
658 aigPoIndicesInstance->attrHintSingalEndMarker = hintSingalEndMarker;
659 aigPoIndicesInstance->attrSafetyInvarIndex = collectSafetyInvariantPOIndex(pNtk);
660
661 /****************************************************/
662 //Allocating "struct" with necessary monotone vectors
663 /****************************************************/
664 anteConsecInstance = allocAntecedentConsequentVectorsStruct();
665 anteConsecInstance->attrAntecedents = NULL;
666 anteConsecInstance->attrConsequentCandidates = vCandidateMonotoneSignals;
667
668 /*******************************************/
669 //Generate AIG from Ntk
670 /*******************************************/
671 if( !Abc_NtkIsStrash( pNtk ) )
672 {
673 pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
674 pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
675 }
676 else
677 {
678 pAig = Abc_NtkToDar( pNtk, 0, 1 );
679 pNtkTemp = pNtk;
680 }
681
682 /*******************************************/
683 //finding LEVEL 1 monotone signals
684 /*******************************************/
685 //printf("Calling target function outside loop\n");
686 vKnownMonotoneSignals = findNewDisjunctiveMonotone( pAig, aigPoIndicesInstance, anteConsecInstance );
687 levelOneMonotne = Vec_PtrAlloc(0);
688 Vec_IntForEachEntry( vKnownMonotoneSignals, iElem, i )
689 {
690 newIntVec = createSingletonIntVector( iElem );
691 Vec_PtrPush( levelOneMonotne, newIntVec );
692 //printf("Monotone Po[%d] = %s\n", iElem, Abc_ObjName( Abc_NtkPo(pNtk, iElem) ) );
693 }
694 //printAllIntVectors( levelOneMonotne, pNtk, "monotone.dat" );
695
696 vMasterDisjunctions = Vec_PtrAlloc( Vec_PtrSize( levelOneMonotne ));
697 appendVecToMasterVecInt(vMasterDisjunctions, levelOneMonotne );
698
699 /*******************************************/
700 //finding LEVEL >1 monotone signals
701 /*******************************************/
702 #if 0
703 if( vKnownMonotoneSignals )
704 {
705 Vec_IntForEachEntry( vKnownMonotoneSignals, iElem, i )
706 {
707 printf("\n**************************************************************\n");
708 printf("Exploring Second Layer : Reference Po[%d] = %s", iElem, Abc_ObjName( Abc_NtkPo(pNtk, iElem) ));
709 printf("\n**************************************************************\n");
710 anteConsecInstance->attrAntecedents = createSingletonIntVector( iElem );
711 vOldConsequentVector = anteConsecInstance->attrConsequentCandidates;
712 vRemainingConsecVector = updateAnteConseVectors(anteConsecInstance);
713 if( anteConsecInstance->attrConsequentCandidates != vRemainingConsecVector )
714 {
715 anteConsecInstance->attrConsequentCandidates = vRemainingConsecVector;
716 }
717 vKnownMonotoneSignalsRoundTwo = findNewDisjunctiveMonotone( pAig, aigPoIndicesInstance, anteConsecInstance );
718 Vec_IntForEachEntry( vKnownMonotoneSignalsRoundTwo, iElemTwo, iTwo )
719 {
720 printf("Monotone Po[%d] = %s, (%d, %d)\n", iElemTwo, Abc_ObjName( Abc_NtkPo(pNtk, iElemTwo) ), iElem, iElemTwo );
721 }
722 Vec_IntFree(vKnownMonotoneSignalsRoundTwo);
723 Vec_IntFree(anteConsecInstance->attrAntecedents);
724 if(anteConsecInstance->attrConsequentCandidates != vOldConsequentVector)
725 {
726 Vec_IntFree(anteConsecInstance->attrConsequentCandidates);
727 anteConsecInstance->attrConsequentCandidates = vOldConsequentVector;
728 }
729 }
730 }
731 #endif
732
733 #if 1
734 levelTwoMonotne = findNextLevelDisjunctiveMonotone( pAig, aigPoIndicesInstance, anteConsecInstance, levelOneMonotne );
735 //printAllIntVectors( levelTwoMonotne, pNtk, "monotone.dat" );
736 appendVecToMasterVecInt(vMasterDisjunctions, levelTwoMonotne );
737 #endif
738
739 //levelThreeMonotne = findNextLevelDisjunctiveMonotone( pAig, aigPoIndicesInstance, anteConsecInstance, levelTwoMonotne );
740 //printAllIntVectors( levelThreeMonotne );
741 //printAllIntVectors( levelTwoMonotne, pNtk, "monotone.dat" );
742 //appendVecToMasterVecInt(vMasterDisjunctions, levelThreeMonotne );
743
744 deallocAigPoIndices(aigPoIndicesInstance);
745 deallocAntecedentConsequentVectorsStruct(anteConsecInstance);
746 //deallocPointersToMonotoneVectors(monotoneVectorsInstance);
747
748 deallocateVecOfIntVec( levelOneMonotne );
749 deallocateVecOfIntVec( levelTwoMonotne );
750
751 Aig_ManStop(pAig);
752 Vec_IntFree(vKnownMonotoneSignals);
753
754 return vMasterDisjunctions;
755 }
756
757 ABC_NAMESPACE_IMPL_END
758