1 /**CFile****************************************************************
2
3 FileName [liveness_sim.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Liveness property checking.]
8
9 Synopsis [Main implementation module.]
10
11 Author [Sayak Ray]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - January 1, 2009.]
16
17 Revision [$Id: liveness_sim.c,v 1.00 2009/01/01 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include <stdio.h>
22 #include "base/main/main.h"
23 #include "aig/aig/aig.h"
24 #include "aig/saig/saig.h"
25 #include <string.h>
26
27 ABC_NAMESPACE_IMPL_START
28
29
30 #define PROPAGATE_NAMES
31 //#define DUPLICATE_CKT_DEBUG
32
33 extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
34 extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
35 //char *strdup(const char *string);
36
37
38 /*******************************************************************
39 LAYOUT OF PI VECTOR:
40
41 +------------------------------------------------------------------------------------------------------------------------------------+
42 | TRUE ORIGINAL PI (n) | SAVE(PI) (1) | ORIGINAL LO (k) | SAVED(LO) (1) | SHADOW_ORIGINAL LO (k) | LIVENESS LO (l) | FAIRNESS LO (f) |
43 +------------------------------------------------------------------------------------------------------------------------------------+
44 <------------True PI----------------->|<----------------------------LO--------------------------------------------------------------->
45
46 LAYOUT OF PO VECTOR:
47
48 +-----------------------------------------------------------------------------------------------------------+
49 | SOLE PO (1) | ORIGINAL LI (k) | SAVED LI (1) | SHADOW_ORIGINAL LI (k) | LIVENESS LI (l) | FAIRNESS LI (f) |
50 +-----------------------------------------------------------------------------------------------------------+
51 <--True PO--->|<--------------------------------------LI---------------------------------------------------->
52
53 ********************************************************************/
54
printVecPtrOfString(Vec_Ptr_t * vec)55 static void printVecPtrOfString( Vec_Ptr_t *vec )
56 {
57 int i;
58
59 for( i=0; i< Vec_PtrSize( vec ); i++ )
60 {
61 printf("vec[%d] = %s\n", i, (char *)Vec_PtrEntry(vec, i) );
62 }
63 }
64
getPoIndex(Aig_Man_t * pAig,Aig_Obj_t * pPivot)65 static int getPoIndex( Aig_Man_t *pAig, Aig_Obj_t *pPivot )
66 {
67 int i;
68 Aig_Obj_t *pObj;
69
70 Saig_ManForEachPo( pAig, pObj, i )
71 {
72 if( pObj == pPivot )
73 return i;
74 }
75 return -1;
76 }
77
retrieveTruePiName(Abc_Ntk_t * pNtkOld,Aig_Man_t * pAigOld,Aig_Man_t * pAigNew,Aig_Obj_t * pObjPivot)78 static char * retrieveTruePiName( Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, Aig_Obj_t *pObjPivot )
79 {
80 Aig_Obj_t *pObjOld, *pObj;
81 Abc_Obj_t *pNode;
82 int index;
83
84 assert( Saig_ObjIsPi( pAigNew, pObjPivot ) );
85 Aig_ManForEachCi( pAigNew, pObj, index )
86 if( pObj == pObjPivot )
87 break;
88 assert( index < Aig_ManCiNum( pAigNew ) - Aig_ManRegNum( pAigNew ) );
89 if( index == Saig_ManPiNum( pAigNew ) - 1 )
90 return "SAVE_BIERE";
91 else
92 {
93 pObjOld = Aig_ManCi( pAigOld, index );
94 pNode = Abc_NtkPi( pNtkOld, index );
95 assert( pObjOld->pData == pObjPivot );
96 return Abc_ObjName( pNode );
97 }
98 }
99
retrieveLOName(Abc_Ntk_t * pNtkOld,Aig_Man_t * pAigOld,Aig_Man_t * pAigNew,Aig_Obj_t * pObjPivot,Vec_Ptr_t * vLive,Vec_Ptr_t * vFair)100 static char * retrieveLOName( Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, Aig_Obj_t *pObjPivot, Vec_Ptr_t *vLive, Vec_Ptr_t * vFair )
101 {
102 Aig_Obj_t *pObjOld, *pObj;
103 Abc_Obj_t *pNode;
104 int index, oldIndex, originalLatchNum = Saig_ManRegNum(pAigOld), strMatch, i;
105 char *dummyStr = (char *)malloc( sizeof(char) * 50 );
106
107 assert( Saig_ObjIsLo( pAigNew, pObjPivot ) );
108 Saig_ManForEachLo( pAigNew, pObj, index )
109 if( pObj == pObjPivot )
110 break;
111 if( index < originalLatchNum )
112 {
113 oldIndex = Saig_ManPiNum( pAigOld ) + index;
114 pObjOld = Aig_ManCi( pAigOld, oldIndex );
115 pNode = Abc_NtkCi( pNtkOld, oldIndex );
116 assert( pObjOld->pData == pObjPivot );
117 return Abc_ObjName( pNode );
118 }
119 else if( index == originalLatchNum )
120 return "SAVED_LO";
121 else if( index > originalLatchNum && index < 2 * originalLatchNum + 1 )
122 {
123 oldIndex = Saig_ManPiNum( pAigOld ) + index - originalLatchNum - 1;
124 pObjOld = Aig_ManCi( pAigOld, oldIndex );
125 pNode = Abc_NtkCi( pNtkOld, oldIndex );
126 sprintf( dummyStr, "%s__%s", Abc_ObjName( pNode ), "SHADOW");
127 return dummyStr;
128 }
129 else if( index >= 2 * originalLatchNum + 1 && index < 2 * originalLatchNum + 1 + Vec_PtrSize( vLive ) )
130 {
131 oldIndex = index - 2 * originalLatchNum - 1;
132 strMatch = 0;
133 Saig_ManForEachPo( pAigOld, pObj, i )
134 {
135 pNode = Abc_NtkPo( pNtkOld, i );
136 if( strstr( Abc_ObjName( pNode ), "assert_fair" ) != NULL )
137 {
138 if( strMatch == oldIndex )
139 {
140 sprintf( dummyStr, "%s__%s", Abc_ObjName( pNode ), "LIVENESS");
141 return dummyStr;
142 }
143 else
144 strMatch++;
145 }
146 }
147 }
148 else if( index >= 2 * originalLatchNum + 1 + Vec_PtrSize( vLive ) && index < 2 * originalLatchNum + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) )
149 {
150 oldIndex = index - 2 * originalLatchNum - 1 - Vec_PtrSize( vLive );
151 strMatch = 0;
152 Saig_ManForEachPo( pAigOld, pObj, i )
153 {
154 pNode = Abc_NtkPo( pNtkOld, i );
155 if( strstr( Abc_ObjName( pNode ), "assume_fair" ) != NULL )
156 {
157 if( strMatch == oldIndex )
158 {
159 sprintf( dummyStr, "%s__%s", Abc_ObjName( pNode ), "FAIRNESS");
160 return dummyStr;
161 }
162 else
163 strMatch++;
164 }
165 }
166 }
167 else
168 return "UNKNOWN";
169 return NULL;
170 }
171
172 extern Vec_Ptr_t *vecPis, *vecPiNames;
173 extern Vec_Ptr_t *vecLos, *vecLoNames;
174
175
Aig_ManCiCleanupBiere(Aig_Man_t * p)176 static int Aig_ManCiCleanupBiere( Aig_Man_t * p )
177 {
178 int nPisOld = Aig_ManCiNum(p);
179
180 p->nObjs[AIG_OBJ_CI] = Vec_PtrSize( p->vCis );
181 if ( Aig_ManRegNum(p) )
182 p->nTruePis = Aig_ManCiNum(p) - Aig_ManRegNum(p);
183
184 return nPisOld - Aig_ManCiNum(p);
185 }
186
187
Aig_ManCoCleanupBiere(Aig_Man_t * p)188 static int Aig_ManCoCleanupBiere( Aig_Man_t * p )
189 {
190 int nPosOld = Aig_ManCoNum(p);
191
192 p->nObjs[AIG_OBJ_CO] = Vec_PtrSize( p->vCos );
193 if ( Aig_ManRegNum(p) )
194 p->nTruePos = Aig_ManCoNum(p) - Aig_ManRegNum(p);
195 return nPosOld - Aig_ManCoNum(p);
196 }
197
LivenessToSafetyTransformationSim(Abc_Ntk_t * pNtk,Aig_Man_t * p,Vec_Ptr_t * vLive,Vec_Ptr_t * vFair)198 static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_t * p, Vec_Ptr_t *vLive, Vec_Ptr_t *vFair )
199 {
200 Aig_Man_t * pNew;
201 int i, nRegCount;
202 Aig_Obj_t * pObjSavePi;
203 Aig_Obj_t *pObjSavedLo, *pObjSavedLi;
204 Aig_Obj_t *pObj, *pMatch;
205 Aig_Obj_t *pObjSaveOrSaved, *pObjSavedLoAndEquality;
206 Aig_Obj_t *pObjShadowLo, *pObjShadowLi, *pObjShadowLiDriver;
207 Aig_Obj_t *pObjXor, *pObjXnor, *pObjAndAcc, *pObjAndAccDummy;
208 Aig_Obj_t *pObjLive, *pObjFair, *pObjSafetyGate;
209 Aig_Obj_t *pObjSafetyPropertyOutput;
210 Aig_Obj_t *pDriverImage;
211 char *nodeName;
212 int piCopied = 0, liCopied = 0, loCopied = 0, liCreated = 0, loCreated = 0, liveLatch = 0, fairLatch = 0;
213
214 vecPis = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
215 vecPiNames = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
216
217 vecLos = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
218 vecLoNames = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
219
220 #ifdef DUPLICATE_CKT_DEBUG
221 printf("\nCode is compiled in DEBUG mode, the input-output behavior will be the same as the original circuit\n");
222 printf("Press any key to continue...");
223 scanf("%c", &c);
224 #endif
225
226 //****************************************************************
227 // Step1: create the new manager
228 // Note: The new manager is created with "2 * Aig_ManObjNumMax(p)"
229 // nodes, but this selection is arbitrary - need to be justified
230 //****************************************************************
231 pNew = Aig_ManStart( 2 * Aig_ManObjNumMax(p) );
232 pNew->pName = Abc_UtilStrsav( "live2safe" );
233 pNew->pSpec = NULL;
234
235 //****************************************************************
236 // Step 2: map constant nodes
237 //****************************************************************
238 pObj = Aig_ManConst1( p );
239 pObj->pData = Aig_ManConst1( pNew );
240
241 //****************************************************************
242 // Step 3: create true PIs
243 //****************************************************************
244 Saig_ManForEachPi( p, pObj, i )
245 {
246 piCopied++;
247 pObj->pData = Aig_ObjCreateCi(pNew);
248 Vec_PtrPush( vecPis, pObj->pData );
249 nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) ));
250 Vec_PtrPush( vecPiNames, nodeName );
251 }
252
253 //****************************************************************
254 // Step 4: create the special Pi corresponding to SAVE
255 //****************************************************************
256 #ifndef DUPLICATE_CKT_DEBUG
257 pObjSavePi = Aig_ObjCreateCi( pNew );
258 nodeName = Abc_UtilStrsav("SAVE_BIERE"),
259 Vec_PtrPush( vecPiNames, nodeName );
260 #endif
261
262 //****************************************************************
263 // Step 5: create register outputs
264 //****************************************************************
265 Saig_ManForEachLo( p, pObj, i )
266 {
267 loCopied++;
268 pObj->pData = Aig_ObjCreateCi(pNew);
269 Vec_PtrPush( vecLos, pObj->pData );
270 nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ));
271 Vec_PtrPush( vecLoNames, nodeName );
272 }
273
274 //****************************************************************
275 // Step 6: create "saved" register output
276 //****************************************************************
277 #ifndef DUPLICATE_CKT_DEBUG
278 loCreated++;
279 pObjSavedLo = Aig_ObjCreateCi( pNew );
280 Vec_PtrPush( vecLos, pObjSavedLo );
281 nodeName = Abc_UtilStrsav("SAVED_LO");
282 Vec_PtrPush( vecLoNames, nodeName );
283 #endif
284
285 //****************************************************************
286 // Step 7: create the OR gate and the AND gate directly fed by "SAVE" Pi
287 //****************************************************************
288 #ifndef DUPLICATE_CKT_DEBUG
289 pObjSaveOrSaved = Aig_Or( pNew, pObjSavePi, pObjSavedLo );
290 //pObjSaveAndNotSaved = Aig_And( pNew, pObjSavePi, Aig_Not(pObjSavedLo) );
291 #endif
292
293 //********************************************************************
294 // Step 8: create internal nodes
295 //********************************************************************
296 Aig_ManForEachNode( p, pObj, i )
297 {
298 pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
299 }
300
301 //********************************************************************
302 // Step 9: create the safety property output gate
303 // create the safety property output gate, this will be the sole true PO
304 // of the whole circuit, discuss with Sat/Alan for an alternative implementation
305 //********************************************************************
306 #ifndef DUPLICATE_CKT_DEBUG
307 pObjSafetyPropertyOutput = Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
308 #endif
309
310 //********************************************************************
311 // DEBUG: To recreate the same circuit, at least from the input and output
312 // behavior, we need to copy the original PO
313 //********************************************************************
314 #ifdef DUPLICATE_CKT_DEBUG
315 Saig_ManForEachPo( p, pObj, i )
316 {
317 Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
318 }
319 #endif
320
321 // create register inputs for the original registers
322 nRegCount = 0;
323
324 Saig_ManForEachLo( p, pObj, i )
325 {
326 pMatch = Saig_ObjLoToLi( p, pObj );
327 //Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pMatch) );
328 Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
329 nRegCount++;
330 liCopied++;
331 }
332
333 // create register input corresponding to the register "saved"
334 #ifndef DUPLICATE_CKT_DEBUG
335 pObjSavedLi = Aig_ObjCreateCo( pNew, pObjSaveOrSaved );
336 nRegCount++;
337 liCreated++;
338
339 pObjAndAcc = NULL;
340
341 // create the family of shadow registers, then create the cascade of Xnor and And gates for the comparator
342 Saig_ManForEachLo( p, pObj, i )
343 {
344 pObjShadowLo = Aig_ObjCreateCi( pNew );
345
346 #ifdef PROPAGATE_NAMES
347 Vec_PtrPush( vecLos, pObjShadowLo );
348 nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ) ) + 10 );
349 sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "SHADOW" );
350 Vec_PtrPush( vecLoNames, nodeName );
351 #endif
352
353 pObjShadowLiDriver = Aig_Mux( pNew, pObjSavePi, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
354 pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
355 nRegCount++;
356 loCreated++; liCreated++;
357
358 pObjXor = Aig_Exor( pNew, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
359 pObjXnor = Aig_Not( pObjXor );
360 if( pObjAndAcc == NULL )
361 pObjAndAcc = pObjXnor;
362 else
363 {
364 pObjAndAccDummy = pObjAndAcc;
365 pObjAndAcc = Aig_And( pNew, pObjXnor, pObjAndAccDummy );
366 }
367 }
368
369 // create the AND gate whose output will be the signal "looped"
370 pObjSavedLoAndEquality = Aig_And( pNew, pObjSavedLo, pObjAndAcc );
371
372 // create the master AND gate and corresponding AND and OR logic for the liveness properties
373 pObjAndAcc = NULL;
374 if( vLive == NULL || Vec_PtrSize( vLive ) == 0 )
375 printf("\nCircuit without any liveness property\n");
376 else
377 {
378 Vec_PtrForEachEntry( Aig_Obj_t *, vLive, pObj, i )
379 {
380 //assert( Aig_ObjIsNode( Aig_ObjChild0( pObj ) ) );
381 //Aig_ObjPrint( pNew, pObj );
382 liveLatch++;
383 pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
384 pObjShadowLo = Aig_ObjCreateCi( pNew );
385
386 #ifdef PROPAGATE_NAMES
387 Vec_PtrPush( vecLos, pObjShadowLo );
388 nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 );
389 sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "LIVENESS" );
390 Vec_PtrPush( vecLoNames, nodeName );
391 #endif
392
393 pObjShadowLiDriver = Aig_Or( pNew, Aig_Mux(pNew, pObjSavePi, Aig_Not(Aig_ManConst1(pNew)), pObjShadowLo),
394 Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
395 pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
396 nRegCount++;
397 loCreated++; liCreated++;
398
399 if( pObjAndAcc == NULL )
400 pObjAndAcc = pObjShadowLo;
401 else
402 {
403 pObjAndAccDummy = pObjAndAcc;
404 pObjAndAcc = Aig_And( pNew, pObjShadowLo, pObjAndAccDummy );
405 }
406 }
407 }
408
409 if( pObjAndAcc != NULL )
410 pObjLive = pObjAndAcc;
411 else
412 pObjLive = Aig_ManConst1( pNew );
413
414 // create the master AND gate and corresponding AND and OR logic for the fairness properties
415 pObjAndAcc = NULL;
416 if( vFair == NULL || Vec_PtrSize( vFair ) == 0 )
417 printf("\nCircuit without any fairness property\n");
418 else
419 {
420 Vec_PtrForEachEntry( Aig_Obj_t *, vFair, pObj, i )
421 {
422 fairLatch++;
423 //assert( Aig_ObjIsNode( Aig_ObjChild0( pObj ) ) );
424 pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
425 pObjShadowLo = Aig_ObjCreateCi( pNew );
426
427 #ifdef PROPAGATE_NAMES
428 Vec_PtrPush( vecLos, pObjShadowLo );
429 nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 );
430 sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "FAIRNESS" );
431 Vec_PtrPush( vecLoNames, nodeName );
432 #endif
433
434 pObjShadowLiDriver = Aig_Or( pNew, Aig_Mux(pNew, pObjSavePi, Aig_Not(Aig_ManConst1(pNew)), pObjShadowLo),
435 Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
436 pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
437 nRegCount++;
438 loCreated++; liCreated++;
439
440 if( pObjAndAcc == NULL )
441 pObjAndAcc = pObjShadowLo;
442 else
443 {
444 pObjAndAccDummy = pObjAndAcc;
445 pObjAndAcc = Aig_And( pNew, pObjShadowLo, pObjAndAccDummy );
446 }
447 }
448 }
449
450 if( pObjAndAcc != NULL )
451 pObjFair = pObjAndAcc;
452 else
453 pObjFair = Aig_ManConst1( pNew );
454
455 //pObjSafetyGate = Aig_Exor( pNew, Aig_Not(Aig_ManConst1( pNew )), Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) ) );
456 pObjSafetyGate = Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) );
457
458 Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyGate );
459 #endif
460
461 Aig_ManSetRegNum( pNew, nRegCount );
462
463 Aig_ManCiCleanupBiere( pNew );
464 Aig_ManCoCleanupBiere( pNew );
465
466 Aig_ManCleanup( pNew );
467 assert( Aig_ManCheck( pNew ) );
468
469 #ifndef DUPLICATE_CKT_DEBUG
470 assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjCioId(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
471 assert( Saig_ManPoNum( pNew ) == 1 );
472 assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) );
473 assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch );
474 #endif
475
476 return pNew;
477 }
478
479
LivenessToSafetyTransformationOneStepLoopSim(Abc_Ntk_t * pNtk,Aig_Man_t * p,Vec_Ptr_t * vLive,Vec_Ptr_t * vFair)480 static Aig_Man_t * LivenessToSafetyTransformationOneStepLoopSim( Abc_Ntk_t * pNtk, Aig_Man_t * p, Vec_Ptr_t *vLive, Vec_Ptr_t *vFair )
481 {
482 Aig_Man_t * pNew;
483 int i, nRegCount;
484 Aig_Obj_t * pObjSavePi;
485 Aig_Obj_t *pObj, *pMatch;
486 Aig_Obj_t *pObjSavedLoAndEquality;
487 Aig_Obj_t *pObjXor, *pObjXnor, *pObjAndAcc, *pObjAndAccDummy;
488 Aig_Obj_t *pObjLive, *pObjFair, *pObjSafetyGate;
489 Aig_Obj_t *pObjSafetyPropertyOutput;
490 Aig_Obj_t *pDriverImage;
491 Aig_Obj_t *pObjCorrespondingLi;
492
493
494 char *nodeName;
495 int piCopied = 0, liCopied = 0, loCopied = 0;//, liCreated = 0, loCreated = 0, piVecIndex = 0;
496
497 vecPis = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
498 vecPiNames = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
499
500 vecLos = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
501 vecLoNames = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
502
503 //****************************************************************
504 // Step1: create the new manager
505 // Note: The new manager is created with "2 * Aig_ManObjNumMax(p)"
506 // nodes, but this selection is arbitrary - need to be justified
507 //****************************************************************
508 pNew = Aig_ManStart( 2 * Aig_ManObjNumMax(p) );
509 pNew->pName = Abc_UtilStrsav( "live2safe" );
510 pNew->pSpec = NULL;
511
512 //****************************************************************
513 // Step 2: map constant nodes
514 //****************************************************************
515 pObj = Aig_ManConst1( p );
516 pObj->pData = Aig_ManConst1( pNew );
517
518 //****************************************************************
519 // Step 3: create true PIs
520 //****************************************************************
521 Saig_ManForEachPi( p, pObj, i )
522 {
523 piCopied++;
524 pObj->pData = Aig_ObjCreateCi(pNew);
525 Vec_PtrPush( vecPis, pObj->pData );
526 nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) ));
527 Vec_PtrPush( vecPiNames, nodeName );
528 }
529
530 //****************************************************************
531 // Step 4: create the special Pi corresponding to SAVE
532 //****************************************************************
533 pObjSavePi = Aig_ObjCreateCi( pNew );
534 nodeName = "SAVE_BIERE",
535 Vec_PtrPush( vecPiNames, nodeName );
536
537 //****************************************************************
538 // Step 5: create register outputs
539 //****************************************************************
540 Saig_ManForEachLo( p, pObj, i )
541 {
542 loCopied++;
543 pObj->pData = Aig_ObjCreateCi(pNew);
544 Vec_PtrPush( vecLos, pObj->pData );
545 nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ));
546 Vec_PtrPush( vecLoNames, nodeName );
547 }
548
549 //****************************************************************
550 // Step 6: create "saved" register output
551 //****************************************************************
552
553 #if 0
554 loCreated++;
555 pObjSavedLo = Aig_ObjCreateCi( pNew );
556 Vec_PtrPush( vecLos, pObjSavedLo );
557 nodeName = "SAVED_LO";
558 Vec_PtrPush( vecLoNames, nodeName );
559 #endif
560
561 //****************************************************************
562 // Step 7: create the OR gate and the AND gate directly fed by "SAVE" Pi
563 //****************************************************************
564 #if 0
565 pObjSaveOrSaved = Aig_Or( pNew, pObjSavePi, pObjSavedLo );
566 pObjSaveAndNotSaved = Aig_And( pNew, pObjSavePi, Aig_Not(pObjSavedLo) );
567 #endif
568
569 //********************************************************************
570 // Step 8: create internal nodes
571 //********************************************************************
572 Aig_ManForEachNode( p, pObj, i )
573 {
574 pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
575 }
576
577 //********************************************************************
578 // Step 9: create the safety property output gate
579 // create the safety property output gate, this will be the sole true PO
580 // of the whole circuit, discuss with Sat/Alan for an alternative implementation
581 //********************************************************************
582
583 pObjSafetyPropertyOutput = Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
584
585 // create register inputs for the original registers
586 nRegCount = 0;
587
588 Saig_ManForEachLo( p, pObj, i )
589 {
590 pMatch = Saig_ObjLoToLi( p, pObj );
591 //Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pMatch) );
592 Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
593 nRegCount++;
594 liCopied++;
595 }
596
597 #if 0
598 // create register input corresponding to the register "saved"
599 pObjSavedLi = Aig_ObjCreateCo( pNew, pObjSaveOrSaved );
600 nRegCount++;
601 liCreated++;
602 #endif
603
604 pObjAndAcc = NULL;
605
606 //****************************************************************************************************
607 //For detection of loop of length 1 we do not need any shadow register, we only need equality detector
608 //between Lo_j and Li_j and then a cascade of AND gates
609 //****************************************************************************************************
610
611 Saig_ManForEachLo( p, pObj, i )
612 {
613 pObjCorrespondingLi = Saig_ObjLoToLi( p, pObj );
614
615 pObjXor = Aig_Exor( pNew, (Aig_Obj_t *)pObj->pData, Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0( pObjCorrespondingLi )->pData, Aig_ObjFaninC0( pObjCorrespondingLi ) ) );
616 pObjXnor = Aig_Not( pObjXor );
617
618 if( pObjAndAcc == NULL )
619 pObjAndAcc = pObjXnor;
620 else
621 {
622 pObjAndAccDummy = pObjAndAcc;
623 pObjAndAcc = Aig_And( pNew, pObjXnor, pObjAndAccDummy );
624 }
625 }
626
627 // create the AND gate whose output will be the signal "looped"
628 pObjSavedLoAndEquality = Aig_And( pNew, pObjSavePi, pObjAndAcc );
629
630 // create the master AND gate and corresponding AND and OR logic for the liveness properties
631 pObjAndAcc = NULL;
632 if( vLive == NULL || Vec_PtrSize( vLive ) == 0 )
633 printf("\nCircuit without any liveness property\n");
634 else
635 {
636 Vec_PtrForEachEntry( Aig_Obj_t *, vLive, pObj, i )
637 {
638 pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
639 if( pObjAndAcc == NULL )
640 pObjAndAcc = pDriverImage;
641 else
642 {
643 pObjAndAccDummy = pObjAndAcc;
644 pObjAndAcc = Aig_And( pNew, pDriverImage, pObjAndAccDummy );
645 }
646 }
647 }
648
649 if( pObjAndAcc != NULL )
650 pObjLive = pObjAndAcc;
651 else
652 pObjLive = Aig_ManConst1( pNew );
653
654 // create the master AND gate and corresponding AND and OR logic for the fairness properties
655 pObjAndAcc = NULL;
656 if( vFair == NULL || Vec_PtrSize( vFair ) == 0 )
657 printf("\nCircuit without any fairness property\n");
658 else
659 {
660 Vec_PtrForEachEntry( Aig_Obj_t *, vFair, pObj, i )
661 {
662 pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
663 if( pObjAndAcc == NULL )
664 pObjAndAcc = pDriverImage;
665 else
666 {
667 pObjAndAccDummy = pObjAndAcc;
668 pObjAndAcc = Aig_And( pNew, pDriverImage, pObjAndAccDummy );
669 }
670 }
671 }
672
673 if( pObjAndAcc != NULL )
674 pObjFair = pObjAndAcc;
675 else
676 pObjFair = Aig_ManConst1( pNew );
677
678 pObjSafetyGate = Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) );
679
680 Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyGate );
681
682 Aig_ManSetRegNum( pNew, nRegCount );
683
684 printf("\nSaig_ManPiNum = %d, Reg Num = %d, before everything, before Pi cleanup\n", Vec_PtrSize( pNew->vCis ), pNew->nRegs );
685
686 Aig_ManCiCleanupBiere( pNew );
687 Aig_ManCoCleanupBiere( pNew );
688
689 Aig_ManCleanup( pNew );
690
691 assert( Aig_ManCheck( pNew ) );
692
693 return pNew;
694 }
695
696
697
populateLivenessVector(Abc_Ntk_t * pNtk,Aig_Man_t * pAig)698 static Vec_Ptr_t * populateLivenessVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
699 {
700 Abc_Obj_t * pNode;
701 int i, liveCounter = 0;
702 Vec_Ptr_t * vLive;
703
704 vLive = Vec_PtrAlloc( 100 );
705 Abc_NtkForEachPo( pNtk, pNode, i )
706 if( strstr( Abc_ObjName( pNode ), "assert_fair") != NULL )
707 {
708 Vec_PtrPush( vLive, Aig_ManCo( pAig, i ) );
709 liveCounter++;
710 }
711 printf("\nNumber of liveness property found = %d\n", liveCounter);
712 return vLive;
713 }
714
populateFairnessVector(Abc_Ntk_t * pNtk,Aig_Man_t * pAig)715 static Vec_Ptr_t * populateFairnessVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
716 {
717 Abc_Obj_t * pNode;
718 int i, fairCounter = 0;
719 Vec_Ptr_t * vFair;
720
721 vFair = Vec_PtrAlloc( 100 );
722 Abc_NtkForEachPo( pNtk, pNode, i )
723 if( strstr( Abc_ObjName( pNode ), "assume_fair") != NULL )
724 {
725 Vec_PtrPush( vFair, Aig_ManCo( pAig, i ) );
726 fairCounter++;
727 }
728 printf("\nNumber of fairness property found = %d\n", fairCounter);
729 return vFair;
730 }
731
updateNewNetworkNameManager(Abc_Ntk_t * pNtk,Aig_Man_t * pAig,Vec_Ptr_t * vPiNames,Vec_Ptr_t * vLoNames)732 static void updateNewNetworkNameManager( Abc_Ntk_t *pNtk, Aig_Man_t *pAig, Vec_Ptr_t *vPiNames, Vec_Ptr_t *vLoNames )
733 {
734 Aig_Obj_t *pObj;
735 int i, ntkObjId;
736
737 pNtk->pManName = Nm_ManCreate( Abc_NtkCiNum( pNtk ) );
738
739 Saig_ManForEachPi( pAig, pObj, i )
740 {
741 ntkObjId = Abc_NtkCi( pNtk, i )->Id;
742 //printf("Pi %d, Saved Name = %s, id = %d\n", i, Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), Vec_PtrEntry(vPiNames, i), NULL ), ntkObjId);
743 Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), (char *)Vec_PtrEntry(vPiNames, i), NULL );
744 }
745 Saig_ManForEachLo( pAig, pObj, i )
746 {
747 ntkObjId = Abc_NtkCi( pNtk, Saig_ManPiNum( pAig ) + i )->Id;
748 //printf("Lo %d, Saved name = %s, id = %d\n", i, Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), Vec_PtrEntry(vLoNames, i), NULL ), ntkObjId);
749 Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), (char *)Vec_PtrEntry(vLoNames, i), NULL );
750 }
751 }
752
753
Abc_CommandAbcLivenessToSafetySim(Abc_Frame_t * pAbc,int argc,char ** argv)754 int Abc_CommandAbcLivenessToSafetySim( Abc_Frame_t * pAbc, int argc, char ** argv )
755 {
756 FILE * pOut, * pErr;
757 Abc_Ntk_t * pNtk, * pNtkTemp, *pNtkNew, *pNtkOld;
758 Aig_Man_t * pAig, *pAigNew;
759 int c;
760 Vec_Ptr_t * vLive, * vFair;
761
762 pNtk = Abc_FrameReadNtk(pAbc);
763 pOut = Abc_FrameReadOut(pAbc);
764 pErr = Abc_FrameReadErr(pAbc);
765
766 if ( pNtk == NULL )
767 {
768 fprintf( pErr, "Empty network.\n" );
769 return 1;
770 }
771
772 if( !Abc_NtkIsStrash( pNtk ) )
773 {
774 printf("\nThe input network was not strashed, strashing....\n");
775 pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
776 pNtkOld = pNtkTemp;
777 pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
778 vLive = populateLivenessVector( pNtk, pAig );
779 vFair = populateFairnessVector( pNtk, pAig );
780 }
781 else
782 {
783 pAig = Abc_NtkToDar( pNtk, 0, 1 );
784 pNtkOld = pNtk;
785 vLive = populateLivenessVector( pNtk, pAig );
786 vFair = populateFairnessVector( pNtk, pAig );
787 }
788
789 #if 0
790 Aig_ManPrintStats( pAig );
791 printf("\nDetail statistics*************************************\n");
792 printf("Number of true primary inputs = %d\n", Saig_ManPiNum( pAig ));
793 printf("Number of true primary outputs = %d\n", Saig_ManPoNum( pAig ));
794 printf("Number of true latch outputs = %d\n", Saig_ManCiNum( pAig ) - Saig_ManPiNum( pAig ));
795 printf("Number of true latch inputs = %d\n", Saig_ManCoNum( pAig ) - Saig_ManPoNum( pAig ));
796 printf("Numer of registers = %d\n", Saig_ManRegNum( pAig ) );
797 printf("\n*******************************************************\n");
798 #endif
799
800 c = Extra_UtilGetopt( argc, argv, "1" );
801 if( c == '1' )
802 pAigNew = LivenessToSafetyTransformationOneStepLoopSim( pNtk, pAig, vLive, vFair );
803 else
804 pAigNew = LivenessToSafetyTransformationSim( pNtk, pAig, vLive, vFair );
805
806 #if 0
807 Aig_ManPrintStats( pAigNew );
808 printf("\nDetail statistics*************************************\n");
809 printf("Number of true primary inputs = %d\n", Saig_ManPiNum( pAigNew ));
810 printf("Number of true primary outputs = %d\n", Saig_ManPoNum( pAigNew ));
811 printf("Number of true latch outputs = %d\n", Saig_ManCiNum( pAigNew ) - Saig_ManPiNum( pAigNew ));
812 printf("Number of true latch inputs = %d\n", Saig_ManCoNum( pAigNew ) - Saig_ManPoNum( pAigNew ));
813 printf("Numer of registers = %d\n", Saig_ManRegNum( pAigNew ) );
814 printf("\n*******************************************************\n");
815 #endif
816
817 pNtkNew = Abc_NtkFromAigPhase( pAigNew );
818
819 if ( !Abc_NtkCheck( pNtkNew ) )
820 fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" );
821
822 updateNewNetworkNameManager( pNtkNew, pAigNew, vecPiNames,vecLoNames );
823 Abc_FrameSetCurrentNetwork( pAbc, pNtkNew );
824
825 //Saig_ManForEachPi( pAigNew, pObj, i )
826 // printf("Name of %d-th Pi = %s\n", i, retrieveTruePiName( pNtk, pAig, pAigNew, pObj ) );
827
828 //Saig_ManForEachLo( pAigNew, pObj, i )
829 // printf("Name of %d-th Lo = %s\n", i, retrieveLOName( pNtk, pAig, pAigNew, pObj, vLive, vFair ) );
830
831 //printVecPtrOfString( vecPiNames );
832 //printVecPtrOfString( vecLoNames );
833
834 #if 0
835 #ifndef DUPLICATE_CKT_DEBUG
836 Saig_ManForEachPi( pAigNew, pObj, i )
837 assert( strcmp( (char *)Vec_PtrEntry(vecPiNames, i), retrieveTruePiName( pNtk, pAig, pAigNew, pObj ) ) == 0 );
838 //printf("Name of %d-th Pi = %s, %s\n", i, retrieveTruePiName( pNtk, pAig, pAigNew, pObj ), (char *)Vec_PtrEntry(vecPiNames, i) );
839
840 Saig_ManForEachLo( pAigNew, pObj, i )
841 assert( strcmp( (char *)Vec_PtrEntry(vecLoNames, i), retrieveLOName( pNtk, pAig, pAigNew, pObj, vLive, vFair ) ) == 0 );
842 #endif
843 #endif
844
845 return 0;
846
847 }
848 ABC_NAMESPACE_IMPL_END
849
850