ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
liveness_sim.c
Go to the documentation of this file.
1
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
27ABC_NAMESPACE_IMPL_START
28
29
30#define PROPAGATE_NAMES
31//#define DUPLICATE_CKT_DEBUG
32
33extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
34extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
35//char *strdup(const char *string);
36
37
38/*******************************************************************
39LAYOUT 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
46LAYOUT 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
55static 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
65static 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
78static 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
100static 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
172extern Vec_Ptr_t *vecPis, *vecPiNames;
173extern Vec_Ptr_t *vecLos, *vecLoNames;
174
175
176static 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
188static 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
198static 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
480static 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
698static 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
715static 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
732static 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
754int 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}
848ABC_NAMESPACE_IMPL_END
849
Abc_Obj_t
struct Abc_Obj_t_ Abc_Obj_t
Definition abc.h:116
Abc_NtkForEachPo
#define Abc_NtkForEachPo(pNtk, pPo, i)
Definition abc.h:520
Abc_NtkCheck
ABC_DLL int Abc_NtkCheck(Abc_Ntk_t *pNtk)
FUNCTION DEFINITIONS ///.
Definition abcCheck.c:64
Abc_ObjName
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
Definition abcNames.c:49
Abc_Ntk_t
struct Abc_Ntk_t_ Abc_Ntk_t
Definition abc.h:115
Abc_NtkStrash
ABC_DLL Abc_Ntk_t * Abc_NtkStrash(Abc_Ntk_t *pNtk, int fAllNodes, int fCleanup, int fRecord)
Definition abcStrash.c:265
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Abc_Frame_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Frame_t_ Abc_Frame_t
INCLUDES ///.
Definition abcapis.h:38
Aig_ManSetRegNum
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition aigMan.c:438
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition aig.h:393
Aig_And
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition aigOper.c:104
Aig_ObjCreateCo
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition aigObj.c:66
Aig_Mux
Aig_Obj_t * Aig_Mux(Aig_Man_t *p, Aig_Obj_t *pC, Aig_Obj_t *p1, Aig_Obj_t *p0)
Definition aigOper.c:317
Aig_Obj_t
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
Aig_Exor
Aig_Obj_t * Aig_Exor(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition aigOper.c:220
Aig_ManStart
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition aigMan.c:47
Aig_ManPrintStats
void Aig_ManPrintStats(Aig_Man_t *p)
Definition aigMan.c:379
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition aig.h:413
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
Aig_ManCleanup
int Aig_ManCleanup(Aig_Man_t *p)
Definition aigMan.c:265
Aig_ObjPatchFanin0
void Aig_ObjPatchFanin0(Aig_Man_t *p, Aig_Obj_t *pObj, Aig_Obj_t *pFaninNew)
Definition aigObj.c:282
Aig_ObjCreateCi
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition aigObj.c:45
AIG_OBJ_CO
@ AIG_OBJ_CO
Definition aig.h:61
AIG_OBJ_CI
@ AIG_OBJ_CI
Definition aig.h:60
Aig_Or
Aig_Obj_t * Aig_Or(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition aigOper.c:259
Aig_ManCheck
ABC_DLL int Aig_ManCheck(Aig_Man_t *p)
FUNCTION DECLARATIONS ///.
Definition aigCheck.c:45
Abc_FrameReadNtk
ABC_DLL Abc_Ntk_t * Abc_FrameReadNtk(Abc_Frame_t *p)
Definition mainFrame.c:327
Abc_FrameReadErr
ABC_DLL FILE * Abc_FrameReadErr(Abc_Frame_t *p)
Definition mainFrame.c:375
Abc_FrameReadOut
ABC_DLL FILE * Abc_FrameReadOut(Abc_Frame_t *p)
Definition mainFrame.c:359
Abc_FrameSetCurrentNetwork
ABC_DLL void Abc_FrameSetCurrentNetwork(Abc_Frame_t *p, Abc_Ntk_t *pNet)
Definition mainFrame.c:441
p
Cube * p
Definition exorList.c:222
Extra_UtilGetopt
int Extra_UtilGetopt(int argc, char *argv[], const char *optstring)
Definition extraUtilUtil.c:98
printVecPtrOfString
void printVecPtrOfString(Vec_Ptr_t *vec)
Definition liveness.c:92
vecLoNames
Vec_Ptr_t * vecLoNames
Definition liveness.c:219
vecLos
Vec_Ptr_t * vecLos
Definition liveness.c:219
vecPiNames
Vec_Ptr_t * vecPiNames
Definition liveness.c:218
populateFairnessVector
Vec_Ptr_t * populateFairnessVector(Abc_Ntk_t *pNtk, Aig_Man_t *pAig)
Definition liveness.c:1161
Aig_ManCoCleanupBiere
int Aig_ManCoCleanupBiere(Aig_Man_t *p)
Definition liveness.c:234
vecPis
Vec_Ptr_t * vecPis
Definition liveness.c:218
retrieveTruePiName
char * retrieveTruePiName(Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, Aig_Obj_t *pObjPivot)
Definition liveness.c:115
retrieveLOName
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)
Definition liveness.c:137
updateNewNetworkNameManager
void updateNewNetworkNameManager(Abc_Ntk_t *pNtk, Aig_Man_t *pAig, Vec_Ptr_t *vPiNames, Vec_Ptr_t *vLoNames)
Definition liveness.c:1215
Aig_ManCiCleanupBiere
int Aig_ManCiCleanupBiere(Aig_Man_t *p)
Definition liveness.c:222
getPoIndex
int getPoIndex(Aig_Man_t *pAig, Aig_Obj_t *pPivot)
Definition liveness.c:102
populateLivenessVector
Vec_Ptr_t * populateLivenessVector(Abc_Ntk_t *pNtk, Aig_Man_t *pAig)
Definition liveness.c:1143
Abc_CommandAbcLivenessToSafetySim
int Abc_CommandAbcLivenessToSafetySim(Abc_Frame_t *pAbc, int argc, char **argv)
Definition liveness_sim.c:754
Abc_NtkToDar
Aig_Man_t * Abc_NtkToDar(Abc_Ntk_t *pNtk, int fExors, int fRegisters)
DECLARATIONS ///.
Definition abcDar.c:237
Abc_NtkFromAigPhase
Abc_Ntk_t * Abc_NtkFromAigPhase(Aig_Man_t *pMan)
DECLARATIONS ///.
Definition abcDar.c:595
Nm_ManCreate
Nm_Man_t * Nm_ManCreate(int nSize)
MACRO DEFINITIONS ///.
Definition nmApi.c:45
Nm_ManStoreIdName
char * Nm_ManStoreIdName(Nm_Man_t *p, int ObjId, int Type, char *pName, char *pSuffix)
Definition nmApi.c:112
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition saig.h:93
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition saig.h:96
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition saig.h:91
Abc_Ntk_t_::pManName
Nm_Man_t * pManName
Definition abc.h:160
Aig_Obj_t_::pData
void * pData
Definition aig.h:87
assert
#define assert(ex)
Definition util_old.h:213
strlen
int strlen()
strcmp
int strcmp()
sprintf
char * sprintf()
strstr
char * strstr()
malloc
char * malloc()
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55