ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
liveness.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#include "base/main/mainInt.h"
27
28ABC_NAMESPACE_IMPL_START
29
30#define PROPAGATE_NAMES
31#define MULTIPLE_LTL_FORMULA
32#define ALLOW_SAFETY_PROPERTIES
33
34#define FULL_BIERE_MODE 0
35#define IGNORE_LIVENESS_KEEP_SAFETY_MODE 1
36#define IGNORE_SAFETY_KEEP_LIVENESS_MODE 2
37#define IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE 3
38#define FULL_BIERE_ONE_LOOP_MODE 4
39//#define DUPLICATE_CKT_DEBUG
40
41extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
42extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
43//char *strdup(const char *string);
44
45//******************************************
46//external functions defined in ltl_parser.c
47//******************************************
48typedef struct ltlNode_t ltlNode;
49extern ltlNode *readLtlFormula( char *formula );
50extern void traverseAbstractSyntaxTree( ltlNode *node );
51extern ltlNode *parseFormulaCreateAST( char *inputFormula );
52extern int isWellFormed( ltlNode *topNode );
53extern int checkSignalNameExistence( Abc_Ntk_t *pNtk, ltlNode *topASTNode );
54extern void populateBoolWithAigNodePtr( Abc_Ntk_t *pNtk, Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, ltlNode *topASTNode );
55extern int checkAllBoolHaveAIGPointer( ltlNode *topASTNode );
56extern void populateAigPointerUnitGF( Aig_Man_t *pAigNew, ltlNode *topASTNode, Vec_Ptr_t *vSignal, Vec_Vec_t *vAigGFMap );
57extern void setAIGNodePtrOfGloballyNode( ltlNode *astNode, Aig_Obj_t *pObjLo );
58extern Aig_Obj_t *buildLogicFromLTLNode( Aig_Man_t *pAig, ltlNode *pLtlNode );
59extern Aig_Obj_t *retriveAIGPointerFromLTLNode( ltlNode *astNode );
60extern void traverseAbstractSyntaxTree_postFix( ltlNode *node );
61//**********************************
62//external function declaration ends
63//**********************************
64
65
66/*******************************************************************
67LAYOUT OF PI VECTOR:
68
69+------------------------------------------------------------------------------------------------------------------------------------+
70| TRUE ORIGINAL PI (n) | SAVE(PI) (1) | ORIGINAL LO (k) | SAVED(LO) (1) | SHADOW_ORIGINAL LO (k) | LIVENESS LO (l) | FAIRNESS LO (f) |
71+------------------------------------------------------------------------------------------------------------------------------------+
72<------------True PI----------------->|<----------------------------LO--------------------------------------------------------------->
73
74LAYOUT OF PO VECTOR:
75
76+-----------------------------------------------------------------------------------------------------------+
77| SOLE PO (1) | ORIGINAL LI (k) | SAVED LI (1) | SHADOW_ORIGINAL LI (k) | LIVENESS LI (l) | FAIRNESS LI (f) |
78+-----------------------------------------------------------------------------------------------------------+
79<--True PO--->|<--------------------------------------LI---------------------------------------------------->
80
81********************************************************************/
82
83
84static int nodeName_starts_with( Abc_Obj_t *pNode, const char *prefix )
85{
86 if( strstr( Abc_ObjName( pNode ), prefix ) == Abc_ObjName( pNode ) )
87 return 1;
88 else
89 return 0;
90}
91
92void printVecPtrOfString( Vec_Ptr_t *vec )
93{
94 int i;
95
96 for( i=0; i< Vec_PtrSize( vec ); i++ )
97 {
98 printf("vec[%d] = %s\n", i, (char *)Vec_PtrEntry(vec, i) );
99 }
100}
101
102int getPoIndex( Aig_Man_t *pAig, Aig_Obj_t *pPivot )
103{
104 int i;
105 Aig_Obj_t *pObj;
106
107 Saig_ManForEachPo( pAig, pObj, i )
108 {
109 if( pObj == pPivot )
110 return i;
111 }
112 return -1;
113}
114
115char * retrieveTruePiName( Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, Aig_Obj_t *pObjPivot )
116{
117 Aig_Obj_t *pObjOld, *pObj;
118 Abc_Obj_t *pNode;
119 int index;
120
121 assert( Saig_ObjIsPi( pAigNew, pObjPivot ) );
122 Aig_ManForEachCi( pAigNew, pObj, index )
123 if( pObj == pObjPivot )
124 break;
125 assert( index < Aig_ManCiNum( pAigNew ) - Aig_ManRegNum( pAigNew ) );
126 if( index == Saig_ManPiNum( pAigNew ) - 1 )
127 return "SAVE_BIERE";
128 else
129 {
130 pObjOld = Aig_ManCi( pAigOld, index );
131 pNode = Abc_NtkPi( pNtkOld, index );
132 assert( pObjOld->pData == pObjPivot );
133 return Abc_ObjName( pNode );
134 }
135}
136
137char * 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 )
138{
139 Aig_Obj_t *pObjOld, *pObj;
140 Abc_Obj_t *pNode;
141 int index, oldIndex, originalLatchNum = Saig_ManRegNum(pAigOld), strMatch, i;
142 char *dummyStr = (char *)malloc( sizeof(char) * 50 );
143
144 assert( Saig_ObjIsLo( pAigNew, pObjPivot ) );
145 Saig_ManForEachLo( pAigNew, pObj, index )
146 if( pObj == pObjPivot )
147 break;
148 if( index < originalLatchNum )
149 {
150 oldIndex = Saig_ManPiNum( pAigOld ) + index;
151 pObjOld = Aig_ManCi( pAigOld, oldIndex );
152 pNode = Abc_NtkCi( pNtkOld, oldIndex );
153 assert( pObjOld->pData == pObjPivot );
154 return Abc_ObjName( pNode );
155 }
156 else if( index == originalLatchNum )
157 return "SAVED_LO";
158 else if( index > originalLatchNum && index < 2 * originalLatchNum + 1 )
159 {
160 oldIndex = Saig_ManPiNum( pAigOld ) + index - originalLatchNum - 1;
161 pObjOld = Aig_ManCi( pAigOld, oldIndex );
162 pNode = Abc_NtkCi( pNtkOld, oldIndex );
163 sprintf( dummyStr, "%s__%s", Abc_ObjName( pNode ), "SHADOW");
164 return dummyStr;
165 }
166 else if( index >= 2 * originalLatchNum + 1 && index < 2 * originalLatchNum + 1 + Vec_PtrSize( vLive ) )
167 {
168 oldIndex = index - 2 * originalLatchNum - 1;
169 strMatch = 0;
170 dummyStr[0] = '\0';
171 Saig_ManForEachPo( pAigOld, pObj, i )
172 {
173 pNode = Abc_NtkPo( pNtkOld, i );
174 //if( strstr( Abc_ObjName( pNode ), "assert_fair" ) != NULL )
175 if( nodeName_starts_with( pNode, "assert_fair" ) )
176 {
177 if( strMatch == oldIndex )
178 {
179 sprintf( dummyStr, "%s__%s", Abc_ObjName( pNode ), "LIVENESS");
180 //return dummyStr;
181 break;
182 }
183 else
184 strMatch++;
185 }
186 }
187 assert( dummyStr[0] != '\0' );
188 return dummyStr;
189 }
190 else if( index >= 2 * originalLatchNum + 1 + Vec_PtrSize( vLive ) && index < 2 * originalLatchNum + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) )
191 {
192 oldIndex = index - 2 * originalLatchNum - 1 - Vec_PtrSize( vLive );
193 strMatch = 0;
194 dummyStr[0] = '\0';
195 Saig_ManForEachPo( pAigOld, pObj, i )
196 {
197 pNode = Abc_NtkPo( pNtkOld, i );
198 //if( strstr( Abc_ObjName( pNode ), "assume_fair" ) != NULL )
199 if( nodeName_starts_with( pNode, "assume_fair" ) )
200 {
201 if( strMatch == oldIndex )
202 {
203 sprintf( dummyStr, "%s__%s", Abc_ObjName( pNode ), "FAIRNESS");
204 //return dummyStr;
205 break;
206 }
207 else
208 strMatch++;
209 }
210 }
211 assert( dummyStr[0] != '\0' );
212 return dummyStr;
213 }
214 else
215 return "UNKNOWN";
216}
217
218Vec_Ptr_t *vecPis, *vecPiNames;
219Vec_Ptr_t *vecLos, *vecLoNames;
220
221
222int Aig_ManCiCleanupBiere( Aig_Man_t * p )
223{
224 int nPisOld = Aig_ManCiNum(p);
225
226 p->nObjs[AIG_OBJ_CI] = Vec_PtrSize( p->vCis );
227 if ( Aig_ManRegNum(p) )
228 p->nTruePis = Aig_ManCiNum(p) - Aig_ManRegNum(p);
229
230 return nPisOld - Aig_ManCiNum(p);
231}
232
233
234int Aig_ManCoCleanupBiere( Aig_Man_t * p )
235{
236 int nPosOld = Aig_ManCoNum(p);
237
238 p->nObjs[AIG_OBJ_CO] = Vec_PtrSize( p->vCos );
239 if ( Aig_ManRegNum(p) )
240 p->nTruePos = Aig_ManCoNum(p) - Aig_ManRegNum(p);
241 return nPosOld - Aig_ManCoNum(p);
242}
243
244Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_t * p,
245 Vec_Ptr_t *vLive, Vec_Ptr_t *vFair, Vec_Ptr_t *vAssertSafety, Vec_Ptr_t *vAssumeSafety )
246{
247 Aig_Man_t * pNew;
248 int i, nRegCount;
249 Aig_Obj_t * pObjSavePi = NULL;
250 Aig_Obj_t *pObjSavedLo = NULL, *pObjSavedLi = NULL;
251 Aig_Obj_t *pObj, *pMatch;
252 Aig_Obj_t *pObjSaveOrSaved = NULL, *pObjSaveAndNotSaved = NULL, *pObjSavedLoAndEquality;
253 Aig_Obj_t *pObjShadowLo, *pObjShadowLi, *pObjShadowLiDriver;
254 Aig_Obj_t *pObjXor, *pObjXnor, *pObjAndAcc;
255 Aig_Obj_t *pObjLive, *pObjFair, *pObjSafetyGate;
256 Aig_Obj_t *pObjSafetyPropertyOutput = NULL;
257 Aig_Obj_t *pObjOriginalSafetyPropertyOutput;
258 Aig_Obj_t *pDriverImage, *pArgument, *collectiveAssertSafety, *collectiveAssumeSafety;
259 char *nodeName;
260 int piCopied = 0, liCopied = 0, loCopied = 0, liCreated = 0, loCreated = 0, liveLatch = 0, fairLatch = 0;
261
262 vecPis = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
263 vecPiNames = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
264
265 vecLos = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
266 vecLoNames = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
267
268 //****************************************************************
269 // Step1: create the new manager
270 // Note: The new manager is created with "2 * Aig_ManObjNumMax(p)"
271 // nodes, but this selection is arbitrary - need to be justified
272 //****************************************************************
273 pNew = Aig_ManStart( 2 * Aig_ManObjNumMax(p) );
274 pNew->pName = (char *)malloc( strlen( pNtk->pName ) + strlen("_l2s") + 1 );
275 sprintf(pNew->pName, "%s_%s", pNtk->pName, "l2s");
276 pNew->pSpec = NULL;
277
278 //****************************************************************
279 // Step 2: map constant nodes
280 //****************************************************************
281 pObj = Aig_ManConst1( p );
282 pObj->pData = Aig_ManConst1( pNew );
283
284 //****************************************************************
285 // Step 3: create true PIs
286 //****************************************************************
287 Saig_ManForEachPi( p, pObj, i )
288 {
289 piCopied++;
290 pObj->pData = Aig_ObjCreateCi(pNew);
291 Vec_PtrPush( vecPis, pObj->pData );
292 nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) ));
293 Vec_PtrPush( vecPiNames, nodeName );
294 }
295
296 //****************************************************************
297 // Step 4: create the special Pi corresponding to SAVE
298 //****************************************************************
299 if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
300 {
301 pObjSavePi = Aig_ObjCreateCi( pNew );
302 nodeName = "SAVE_BIERE",
303 Vec_PtrPush( vecPiNames, nodeName );
304 }
305
306 //****************************************************************
307 // Step 5: create register outputs
308 //****************************************************************
309 Saig_ManForEachLo( p, pObj, i )
310 {
311 loCopied++;
312 pObj->pData = Aig_ObjCreateCi(pNew);
313 Vec_PtrPush( vecLos, pObj->pData );
314 nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ));
315 Vec_PtrPush( vecLoNames, nodeName );
316 }
317
318 //****************************************************************
319 // Step 6: create "saved" register output
320 //****************************************************************
321 if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
322 {
323 loCreated++;
324 pObjSavedLo = Aig_ObjCreateCi( pNew );
325 Vec_PtrPush( vecLos, pObjSavedLo );
326 nodeName = "SAVED_LO";
327 Vec_PtrPush( vecLoNames, nodeName );
328 }
329
330 //****************************************************************
331 // Step 7: create the OR gate and the AND gate directly fed by "SAVE" Pi
332 //****************************************************************
333 if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
334 {
335 pObjSaveOrSaved = Aig_Or( pNew, pObjSavePi, pObjSavedLo );
336 pObjSaveAndNotSaved = Aig_And( pNew, pObjSavePi, Aig_Not(pObjSavedLo) );
337 }
338
339 //********************************************************************
340 // Step 8: create internal nodes
341 //********************************************************************
342 Aig_ManForEachNode( p, pObj, i )
343 {
344 pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
345 }
346
347
348 //********************************************************************
349 // Step 8.x : create PO for each safety assertions
350 // NOTE : Here the output is purposely inverted as it will be thrown to
351 // dprove
352 //********************************************************************
353 if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
354 {
355 if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) == 0 )
356 {
357 pObjAndAcc = Aig_ManConst1( pNew );
358 Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
359 {
360 pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
361 pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
362 }
363 pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_Not(pObjAndAcc) );
364 }
365 else if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) != 0 )
366 {
367 pObjAndAcc = Aig_ManConst1( pNew );
368 Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
369 {
370 pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
371 pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
372 }
373 collectiveAssertSafety = pObjAndAcc;
374
375 pObjAndAcc = Aig_ManConst1( pNew );
376 Vec_PtrForEachEntry( Aig_Obj_t *, vAssumeSafety, pObj, i )
377 {
378 pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
379 pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
380 }
381 collectiveAssumeSafety = pObjAndAcc;
382 pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) );
383 }
384 else
385 {
386 printf("WARNING!! No safety property is found, a new (negated) constant 1 output is created\n");
387 pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_Not( Aig_ManConst1(pNew) ) );
388 }
389 }
390
391 //********************************************************************
392 // Step 9: create the safety property output gate for the liveness properties
393 // discuss with Sat/Alan for an alternative implementation
394 //********************************************************************
395 if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
396 {
397 pObjSafetyPropertyOutput = Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
398 }
399
400 // create register inputs for the original registers
401 nRegCount = 0;
402
403 Saig_ManForEachLo( p, pObj, i )
404 {
405 pMatch = Saig_ObjLoToLi( p, pObj );
406 Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
407 nRegCount++;
408 liCopied++;
409 }
410
411 // create register input corresponding to the register "saved"
412 if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
413 {
414 #ifndef DUPLICATE_CKT_DEBUG
415 pObjSavedLi = Aig_ObjCreateCo( pNew, pObjSaveOrSaved );
416 nRegCount++;
417 liCreated++;
418
419 //Changed on October 13, 2009
420 //pObjAndAcc = NULL;
421 pObjAndAcc = Aig_ManConst1( pNew );
422
423 // create the family of shadow registers, then create the cascade of Xnor and And gates for the comparator
424 Saig_ManForEachLo( p, pObj, i )
425 {
426 pObjShadowLo = Aig_ObjCreateCi( pNew );
427
428 #ifdef PROPAGATE_NAMES
429 Vec_PtrPush( vecLos, pObjShadowLo );
430 nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ) ) + 10 );
431 sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "SHADOW" );
432
433 Vec_PtrPush( vecLoNames, nodeName );
434 #endif
435
436 pObjShadowLiDriver = Aig_Mux( pNew, pObjSaveAndNotSaved, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
437 pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
438 nRegCount++;
439 loCreated++; liCreated++;
440
441 pObjXor = Aig_Exor( pNew, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
442 pObjXnor = Aig_Not( pObjXor );
443
444 pObjAndAcc = Aig_And( pNew, pObjXnor, pObjAndAcc );
445 }
446
447 // create the AND gate whose output will be the signal "looped"
448 pObjSavedLoAndEquality = Aig_And( pNew, pObjSavedLo, pObjAndAcc );
449
450 // create the master AND gate and corresponding AND and OR logic for the liveness properties
451 pObjAndAcc = Aig_ManConst1( pNew );
452 if( vLive == NULL || Vec_PtrSize( vLive ) == 0 )
453 {
454 printf("Circuit without any liveness property\n");
455 }
456 else
457 {
458 Vec_PtrForEachEntry( Aig_Obj_t *, vLive, pObj, i )
459 {
460 liveLatch++;
461 pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
462 pObjShadowLo = Aig_ObjCreateCi( pNew );
463
464 #ifdef PROPAGATE_NAMES
465 Vec_PtrPush( vecLos, pObjShadowLo );
466 nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 );
467 sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "LIVENESS" );
468 Vec_PtrPush( vecLoNames, nodeName );
469 #endif
470
471 pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
472 pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
473 nRegCount++;
474 loCreated++; liCreated++;
475
476 pObjAndAcc = Aig_And( pNew, pObjShadowLo, pObjAndAcc );
477 }
478 }
479
480 pObjLive = pObjAndAcc;
481
482 pObjAndAcc = Aig_ManConst1( pNew );
483 if( vFair == NULL || Vec_PtrSize( vFair ) == 0 )
484 printf("Circuit without any fairness property\n");
485 else
486 {
487 Vec_PtrForEachEntry( Aig_Obj_t *, vFair, pObj, i )
488 {
489 fairLatch++;
490 pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
491 pObjShadowLo = Aig_ObjCreateCi( pNew );
492
493 #ifdef PROPAGATE_NAMES
494 Vec_PtrPush( vecLos, pObjShadowLo );
495 nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 );
496 sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "FAIRNESS" );
497 Vec_PtrPush( vecLoNames, nodeName );
498 #endif
499
500 pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
501 pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
502 nRegCount++;
503 loCreated++; liCreated++;
504
505 pObjAndAcc = Aig_And( pNew, pObjShadowLo, pObjAndAcc );
506 }
507 }
508
509 pObjFair = pObjAndAcc;
510
511 //pObjSafetyGate = Aig_Exor( pNew, Aig_Not(Aig_ManConst1( pNew )), Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) ) );
512 //Following is the actual Biere translation
513 pObjSafetyGate = Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) );
514
515 Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyGate );
516 #endif
517 }
518
519 Aig_ManSetRegNum( pNew, nRegCount );
520
521 Aig_ManCiCleanupBiere( pNew );
522 Aig_ManCoCleanupBiere( pNew );
523
524 Aig_ManCleanup( pNew );
525
526 assert( Aig_ManCheck( pNew ) );
527
528 if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
529 {
530 assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjCioId(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
531 assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) );
532 assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch );
533 }
534
535 return pNew;
536}
537
538
539
540
541
542Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_Man_t * p, Vec_Int_t *vFlops,
543 Vec_Ptr_t *vLive, Vec_Ptr_t *vFair, Vec_Ptr_t *vAssertSafety, Vec_Ptr_t *vAssumeSafety )
544{
545 Aig_Man_t * pNew;
546 int i, nRegCount, iEntry;
547 Aig_Obj_t * pObjSavePi = NULL;
548 Aig_Obj_t *pObjSavedLi = NULL, *pObjSavedLo = NULL;
549 Aig_Obj_t *pObj, *pMatch;
550 Aig_Obj_t *pObjSavedLoAndEquality, *pObjSaveOrSaved = NULL, *pObjSaveAndNotSaved = NULL;
551 Aig_Obj_t *pObjShadowLo, *pObjShadowLi, *pObjShadowLiDriver;
552 Aig_Obj_t *pObjXor, *pObjXnor, *pObjAndAcc;
553 Aig_Obj_t *pObjLive, *pObjFair, *pObjSafetyGate;
554 Aig_Obj_t *pObjSafetyPropertyOutput = NULL;
555 Aig_Obj_t *pDriverImage, *pArgument, *collectiveAssertSafety, *collectiveAssumeSafety;
556 char *nodeName;
557 int piCopied = 0, liCopied = 0, loCopied = 0, liCreated = 0, loCreated = 0, liveLatch = 0, fairLatch = 0;//, piVecIndex = 0;
558
559 vecPis = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
560 vecPiNames = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
561
562 vecLos = Vec_PtrAlloc( Saig_ManRegNum( p ) + Vec_IntSize( vFlops ) + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
563 vecLoNames = Vec_PtrAlloc( Saig_ManRegNum( p ) + Vec_IntSize( vFlops ) + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
564
565 //****************************************************************
566 // Step1: create the new manager
567 // Note: The new manager is created with "2 * Aig_ManObjNumMax(p)"
568 // nodes, but this selection is arbitrary - need to be justified
569 //****************************************************************
570 pNew = Aig_ManStart( 2 * Aig_ManObjNumMax(p) );
571 pNew->pName = (char *)malloc( strlen( pNtk->pName ) + strlen("_l2s") + 1 );
572 sprintf(pNew->pName, "%s_%s", pNtk->pName, "l2s");
573 pNew->pSpec = NULL;
574
575 //****************************************************************
576 // Step 2: map constant nodes
577 //****************************************************************
578 pObj = Aig_ManConst1( p );
579 pObj->pData = Aig_ManConst1( pNew );
580
581 //****************************************************************
582 // Step 3: create true PIs
583 //****************************************************************
584 Saig_ManForEachPi( p, pObj, i )
585 {
586 piCopied++;
587 pObj->pData = Aig_ObjCreateCi(pNew);
588 Vec_PtrPush( vecPis, pObj->pData );
589 nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) ));
590 Vec_PtrPush( vecPiNames, nodeName );
591 }
592
593 //****************************************************************
594 // Step 4: create the special Pi corresponding to SAVE
595 //****************************************************************
596 if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
597 {
598 pObjSavePi = Aig_ObjCreateCi( pNew );
599 nodeName = "SAVE_BIERE",
600 Vec_PtrPush( vecPiNames, nodeName );
601 }
602
603 //****************************************************************
604 // Step 5: create register outputs
605 //****************************************************************
606 Saig_ManForEachLo( p, pObj, i )
607 {
608 loCopied++;
609 pObj->pData = Aig_ObjCreateCi(pNew);
610 Vec_PtrPush( vecLos, pObj->pData );
611 nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ));
612 Vec_PtrPush( vecLoNames, nodeName );
613 }
614
615 //****************************************************************
616 // Step 6: create "saved" register output
617 //****************************************************************
618 if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
619 {
620 loCreated++;
621 pObjSavedLo = Aig_ObjCreateCi( pNew );
622 Vec_PtrPush( vecLos, pObjSavedLo );
623 nodeName = "SAVED_LO";
624 Vec_PtrPush( vecLoNames, nodeName );
625 }
626
627 //****************************************************************
628 // Step 7: create the OR gate and the AND gate directly fed by "SAVE" Pi
629 //****************************************************************
630 if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
631 {
632 pObjSaveOrSaved = Aig_Or( pNew, pObjSavePi, pObjSavedLo );
633 pObjSaveAndNotSaved = Aig_And( pNew, pObjSavePi, Aig_Not(pObjSavedLo) );
634 }
635
636 //********************************************************************
637 // Step 8: create internal nodes
638 //********************************************************************
639 Aig_ManForEachNode( p, pObj, i )
640 {
641 pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
642 }
643
644
645 //********************************************************************
646 // Step 8.x : create PO for each safety assertions
647 // NOTE : Here the output is purposely inverted as it will be thrown to
648 // dprove
649 //********************************************************************
650 if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
651 {
652 if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) == 0 )
653 {
654 pObjAndAcc = Aig_ManConst1( pNew );
655 Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
656 {
657 pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
658 pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
659 }
660 Aig_ObjCreateCo( pNew, Aig_Not(pObjAndAcc) );
661 }
662 else if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) != 0 )
663 {
664 pObjAndAcc = Aig_ManConst1( pNew );
665 Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
666 {
667 pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
668 pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
669 }
670 collectiveAssertSafety = pObjAndAcc;
671
672 pObjAndAcc = Aig_ManConst1( pNew );
673 Vec_PtrForEachEntry( Aig_Obj_t *, vAssumeSafety, pObj, i )
674 {
675 pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
676 pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
677 }
678 collectiveAssumeSafety = pObjAndAcc;
679 Aig_ObjCreateCo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) );
680 }
681 else
682 {
683 printf("WARNING!! No safety property is found, a new (negated) constant 1 output is created\n");
684 Aig_ObjCreateCo( pNew, Aig_Not( Aig_ManConst1(pNew) ) );
685 }
686 }
687
688 //********************************************************************
689 // Step 9: create the safety property output gate for the liveness properties
690 // discuss with Sat/Alan for an alternative implementation
691 //********************************************************************
692 if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
693 {
694 pObjSafetyPropertyOutput = Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
695 }
696
697 // create register inputs for the original registers
698 nRegCount = 0;
699
700 Saig_ManForEachLo( p, pObj, i )
701 {
702 pMatch = Saig_ObjLoToLi( p, pObj );
703 Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
704 nRegCount++;
705 liCopied++;
706 }
707
708 // create register input corresponding to the register "saved"
709 if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
710 {
711 #ifndef DUPLICATE_CKT_DEBUG
712 pObjSavedLi = Aig_ObjCreateCo( pNew, pObjSaveOrSaved );
713 nRegCount++;
714 liCreated++;
715
716 //Changed on October 13, 2009
717 //pObjAndAcc = NULL;
718 pObjAndAcc = Aig_ManConst1( pNew );
719
720 // create the family of shadow registers, then create the cascade of Xnor and And gates for the comparator
721 //Saig_ManForEachLo( p, pObj, i )
722 Saig_ManForEachLo( p, pObj, i )
723 {
724 printf("Flop[%d] = %s\n", i, Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ) );
725 }
726 Vec_IntForEachEntry( vFlops, iEntry, i )
727 {
728 pObjShadowLo = Aig_ObjCreateCi( pNew );
729 pObj = Aig_ManLo( p, iEntry );
730
731 #ifdef PROPAGATE_NAMES
732 Vec_PtrPush( vecLos, pObjShadowLo );
733 nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + iEntry ) ) ) + 10 );
734 sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + iEntry ) ), "SHADOW" );
735 printf("Flop copied [%d] = %s\n", iEntry, nodeName );
736 Vec_PtrPush( vecLoNames, nodeName );
737 #endif
738
739 pObjShadowLiDriver = Aig_Mux( pNew, pObjSaveAndNotSaved, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
740 pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
741 nRegCount++;
742 loCreated++; liCreated++;
743
744 pObjXor = Aig_Exor( pNew, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
745 pObjXnor = Aig_Not( pObjXor );
746
747 pObjAndAcc = Aig_And( pNew, pObjXnor, pObjAndAcc );
748 }
749
750 // create the AND gate whose output will be the signal "looped"
751 pObjSavedLoAndEquality = Aig_And( pNew, pObjSavedLo, pObjAndAcc );
752
753 // create the master AND gate and corresponding AND and OR logic for the liveness properties
754 pObjAndAcc = Aig_ManConst1( pNew );
755 if( vLive == NULL || Vec_PtrSize( vLive ) == 0 )
756 {
757 printf("Circuit without any liveness property\n");
758 }
759 else
760 {
761 Vec_PtrForEachEntry( Aig_Obj_t *, vLive, pObj, i )
762 {
763 liveLatch++;
764 pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
765 pObjShadowLo = Aig_ObjCreateCi( pNew );
766
767 #ifdef PROPAGATE_NAMES
768 Vec_PtrPush( vecLos, pObjShadowLo );
769 nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 );
770 sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "LIVENESS" );
771 Vec_PtrPush( vecLoNames, nodeName );
772 #endif
773
774 pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
775 pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
776 nRegCount++;
777 loCreated++; liCreated++;
778
779 pObjAndAcc = Aig_And( pNew, pObjShadowLo, pObjAndAcc );
780 }
781 }
782
783 pObjLive = pObjAndAcc;
784
785 pObjAndAcc = Aig_ManConst1( pNew );
786 if( vFair == NULL || Vec_PtrSize( vFair ) == 0 )
787 printf("Circuit without any fairness property\n");
788 else
789 {
790 Vec_PtrForEachEntry( Aig_Obj_t *, vFair, pObj, i )
791 {
792 fairLatch++;
793 pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
794 pObjShadowLo = Aig_ObjCreateCi( pNew );
795
796 #ifdef PROPAGATE_NAMES
797 Vec_PtrPush( vecLos, pObjShadowLo );
798 nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 );
799 sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "FAIRNESS" );
800 Vec_PtrPush( vecLoNames, nodeName );
801 #endif
802
803 pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
804 pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
805 nRegCount++;
806 loCreated++; liCreated++;
807
808 pObjAndAcc = Aig_And( pNew, pObjShadowLo, pObjAndAcc );
809 }
810 }
811
812 pObjFair = pObjAndAcc;
813
814 //pObjSafetyGate = Aig_Exor( pNew, Aig_Not(Aig_ManConst1( pNew )), Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) ) );
815 //Following is the actual Biere translation
816 pObjSafetyGate = Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) );
817
818 Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyGate );
819 #endif
820 }
821
822 Aig_ManSetRegNum( pNew, nRegCount );
823
824 Aig_ManCiCleanupBiere( pNew );
825 Aig_ManCoCleanupBiere( pNew );
826
827 Aig_ManCleanup( pNew );
828
829 assert( Aig_ManCheck( pNew ) );
830
831 if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
832 {
833 assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjCioId(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
834 assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) );
835 assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) + Vec_IntSize( vFlops ) + 1 + liveLatch + fairLatch );
836 }
837
838 return pNew;
839}
840
841
842
843Aig_Man_t * LivenessToSafetyTransformationOneStepLoop( int mode, Abc_Ntk_t * pNtk, Aig_Man_t * p,
844 Vec_Ptr_t *vLive, Vec_Ptr_t *vFair, Vec_Ptr_t *vAssertSafety, Vec_Ptr_t *vAssumeSafety )
845{
846 Aig_Man_t * pNew;
847 int i, nRegCount;
848 Aig_Obj_t * pObjSavePi = NULL;
849 Aig_Obj_t *pObj, *pMatch;
850 Aig_Obj_t *pObjSavedLoAndEquality;
851 Aig_Obj_t *pObjXor, *pObjXnor, *pObjAndAcc, *pObjAndAccDummy;
852 Aig_Obj_t *pObjLive, *pObjFair, *pObjSafetyGate;
853 Aig_Obj_t *pObjSafetyPropertyOutput = NULL;
854 Aig_Obj_t *pDriverImage;
855 Aig_Obj_t *pObjCorrespondingLi;
856 Aig_Obj_t *pArgument;
857 Aig_Obj_t *collectiveAssertSafety, *collectiveAssumeSafety;
858
859 char *nodeName;
860 int piCopied = 0, liCopied = 0, loCopied = 0;//, liCreated = 0, loCreated = 0, piVecIndex = 0;
861
862 if( Aig_ManRegNum( p ) == 0 )
863 {
864 printf("The input AIG contains no register, returning the original AIG as it is\n");
865 return p;
866 }
867
868 vecPis = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
869 vecPiNames = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
870
871 vecLos = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
872 vecLoNames = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
873
874 //****************************************************************
875 // Step1: create the new manager
876 // Note: The new manager is created with "2 * Aig_ManObjNumMax(p)"
877 // nodes, but this selection is arbitrary - need to be justified
878 //****************************************************************
879 pNew = Aig_ManStart( 2 * Aig_ManObjNumMax(p) );
880 pNew->pName = Abc_UtilStrsav( "live2safe" );
881 pNew->pSpec = NULL;
882
883 //****************************************************************
884 // Step 2: map constant nodes
885 //****************************************************************
886 pObj = Aig_ManConst1( p );
887 pObj->pData = Aig_ManConst1( pNew );
888
889 //****************************************************************
890 // Step 3: create true PIs
891 //****************************************************************
892 Saig_ManForEachPi( p, pObj, i )
893 {
894 piCopied++;
895 pObj->pData = Aig_ObjCreateCi(pNew);
896 Vec_PtrPush( vecPis, pObj->pData );
897 nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) ));
898 Vec_PtrPush( vecPiNames, nodeName );
899 }
900
901 //****************************************************************
902 // Step 4: create the special Pi corresponding to SAVE
903 //****************************************************************
904 if( mode == FULL_BIERE_ONE_LOOP_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE )
905 {
906 pObjSavePi = Aig_ObjCreateCi( pNew );
907 nodeName = "SAVE_BIERE",
908 Vec_PtrPush( vecPiNames, nodeName );
909 }
910
911 //****************************************************************
912 // Step 5: create register outputs
913 //****************************************************************
914 Saig_ManForEachLo( p, pObj, i )
915 {
916 loCopied++;
917 pObj->pData = Aig_ObjCreateCi(pNew);
918 Vec_PtrPush( vecLos, pObj->pData );
919 nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ));
920 Vec_PtrPush( vecLoNames, nodeName );
921 }
922
923 //****************************************************************
924 // Step 6: create "saved" register output
925 //****************************************************************
926
927#if 0
928 loCreated++;
929 pObjSavedLo = Aig_ObjCreateCi( pNew );
930 Vec_PtrPush( vecLos, pObjSavedLo );
931 nodeName = "SAVED_LO";
932 Vec_PtrPush( vecLoNames, nodeName );
933#endif
934
935 //****************************************************************
936 // Step 7: create the OR gate and the AND gate directly fed by "SAVE" Pi
937 //****************************************************************
938#if 0
939 pObjSaveOrSaved = Aig_Or( pNew, pObjSavePi, pObjSavedLo );
940 pObjSaveAndNotSaved = Aig_And( pNew, pObjSavePi, Aig_Not(pObjSavedLo) );
941#endif
942
943 //********************************************************************
944 // Step 8: create internal nodes
945 //********************************************************************
946 Aig_ManForEachNode( p, pObj, i )
947 {
948 pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
949 }
950
951#if 0
952 //********************************************************************
953 // Step 8.x : create PO for each safety assertions
954 //********************************************************************
955 Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
956 {
957 pObj->pData = Aig_ObjCreateCo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) );
958 }
959#endif
960
961 if( mode == FULL_BIERE_ONE_LOOP_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
962 {
963 if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) == 0 )
964 {
965 pObjAndAcc = NULL;
966 Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
967 {
968 //pObj->pData = Aig_ObjCreateCo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) );
969 pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
970 if( pObjAndAcc == NULL )
971 pObjAndAcc = pArgument;
972 else
973 {
974 pObjAndAccDummy = pObjAndAcc;
975 pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAccDummy );
976 }
977 }
978 Aig_ObjCreateCo( pNew, Aig_Not(pObjAndAcc) );
979 }
980 else if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) != 0 )
981 {
982 pObjAndAcc = NULL;
983 Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
984 {
985 //pObj->pData = Aig_ObjCreateCo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) );
986 pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
987 if( pObjAndAcc == NULL )
988 pObjAndAcc = pArgument;
989 else
990 {
991 pObjAndAccDummy = pObjAndAcc;
992 pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAccDummy );
993 }
994 }
995 collectiveAssertSafety = pObjAndAcc;
996 pObjAndAcc = NULL;
997 Vec_PtrForEachEntry( Aig_Obj_t *, vAssumeSafety, pObj, i )
998 {
999 //pObj->pData = Aig_ObjCreateCo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) );
1000 pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
1001 if( pObjAndAcc == NULL )
1002 pObjAndAcc = pArgument;
1003 else
1004 {
1005 pObjAndAccDummy = pObjAndAcc;
1006 pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAccDummy );
1007 }
1008 }
1009 collectiveAssumeSafety = pObjAndAcc;
1010 Aig_ObjCreateCo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) );
1011 }
1012 else
1013 printf("No safety property is specified, hence no safety gate is created\n");
1014 }
1015
1016 //********************************************************************
1017 // Step 9: create the safety property output gate
1018 // create the safety property output gate, this will be the sole true PO
1019 // of the whole circuit, discuss with Sat/Alan for an alternative implementation
1020 //********************************************************************
1021
1022 if( mode == FULL_BIERE_ONE_LOOP_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE )
1023 {
1024 pObjSafetyPropertyOutput = Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
1025 }
1026
1027 // create register inputs for the original registers
1028 nRegCount = 0;
1029
1030 Saig_ManForEachLo( p, pObj, i )
1031 {
1032 pMatch = Saig_ObjLoToLi( p, pObj );
1033 //Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pMatch) );
1034 Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
1035 nRegCount++;
1036 liCopied++;
1037 }
1038
1039#if 0
1040 // create register input corresponding to the register "saved"
1041 pObjSavedLi = Aig_ObjCreateCo( pNew, pObjSaveOrSaved );
1042 nRegCount++;
1043 liCreated++;7
1044#endif
1045
1046 pObjAndAcc = NULL;
1047
1048 //****************************************************************************************************
1049 //For detection of loop of length 1 we do not need any shadow register, we only need equality detector
1050 //between Lo_j and Li_j and then a cascade of AND gates
1051 //****************************************************************************************************
1052
1053 if( mode == FULL_BIERE_ONE_LOOP_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE )
1054 {
1055 Saig_ManForEachLo( p, pObj, i )
1056 {
1057 pObjCorrespondingLi = Saig_ObjLoToLi( p, pObj );
1058
1059 pObjXor = Aig_Exor( pNew, (Aig_Obj_t *)pObj->pData, Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0( pObjCorrespondingLi )->pData, Aig_ObjFaninC0( pObjCorrespondingLi ) ) );
1060 pObjXnor = Aig_Not( pObjXor );
1061
1062 if( pObjAndAcc == NULL )
1063 pObjAndAcc = pObjXnor;
1064 else
1065 {
1066 pObjAndAccDummy = pObjAndAcc;
1067 pObjAndAcc = Aig_And( pNew, pObjXnor, pObjAndAccDummy );
1068 }
1069 }
1070
1071 // create the AND gate whose output will be the signal "looped"
1072 pObjSavedLoAndEquality = Aig_And( pNew, pObjSavePi, pObjAndAcc );
1073
1074 // create the master AND gate and corresponding AND and OR logic for the liveness properties
1075 pObjAndAcc = NULL;
1076 if( vLive == NULL || Vec_PtrSize( vLive ) == 0 )
1077 printf("Circuit without any liveness property\n");
1078 else
1079 {
1080 Vec_PtrForEachEntry( Aig_Obj_t *, vLive, pObj, i )
1081 {
1082 pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
1083 if( pObjAndAcc == NULL )
1084 pObjAndAcc = pDriverImage;
1085 else
1086 {
1087 pObjAndAccDummy = pObjAndAcc;
1088 pObjAndAcc = Aig_And( pNew, pDriverImage, pObjAndAccDummy );
1089 }
1090 }
1091 }
1092
1093 if( pObjAndAcc != NULL )
1094 pObjLive = pObjAndAcc;
1095 else
1096 pObjLive = Aig_ManConst1( pNew );
1097
1098 // create the master AND gate and corresponding AND and OR logic for the fairness properties
1099 pObjAndAcc = NULL;
1100 if( vFair == NULL || Vec_PtrSize( vFair ) == 0 )
1101 printf("Circuit without any fairness property\n");
1102 else
1103 {
1104 Vec_PtrForEachEntry( Aig_Obj_t *, vFair, pObj, i )
1105 {
1106 pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
1107 if( pObjAndAcc == NULL )
1108 pObjAndAcc = pDriverImage;
1109 else
1110 {
1111 pObjAndAccDummy = pObjAndAcc;
1112 pObjAndAcc = Aig_And( pNew, pDriverImage, pObjAndAccDummy );
1113 }
1114 }
1115 }
1116
1117 if( pObjAndAcc != NULL )
1118 pObjFair = pObjAndAcc;
1119 else
1120 pObjFair = Aig_ManConst1( pNew );
1121
1122 pObjSafetyGate = Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) );
1123
1124 Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyGate );
1125 }
1126
1127 Aig_ManSetRegNum( pNew, nRegCount );
1128
1129 //printf("\nSaig_ManPiNum = %d, Reg Num = %d, before everything, before Pi cleanup\n", Vec_PtrSize( pNew->vPis ), pNew->nRegs );
1130
1131 Aig_ManCiCleanupBiere( pNew );
1132 Aig_ManCoCleanupBiere( pNew );
1133
1134 Aig_ManCleanup( pNew );
1135
1136 assert( Aig_ManCheck( pNew ) );
1137
1138 return pNew;
1139}
1140
1141
1142
1143Vec_Ptr_t * populateLivenessVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
1144{
1145 Abc_Obj_t * pNode;
1146 int i, liveCounter = 0;
1147 Vec_Ptr_t * vLive;
1148
1149 vLive = Vec_PtrAlloc( 100 );
1150 Abc_NtkForEachPo( pNtk, pNode, i )
1151 //if( strstr( Abc_ObjName( pNode ), "assert_fair") != NULL )
1152 if( nodeName_starts_with( pNode, "assert_fair" ) )
1153 {
1154 Vec_PtrPush( vLive, Aig_ManCo( pAig, i ) );
1155 liveCounter++;
1156 }
1157 printf("Number of liveness property found = %d\n", liveCounter);
1158 return vLive;
1159}
1160
1161Vec_Ptr_t * populateFairnessVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
1162{
1163 Abc_Obj_t * pNode;
1164 int i, fairCounter = 0;
1165 Vec_Ptr_t * vFair;
1166
1167 vFair = Vec_PtrAlloc( 100 );
1168 Abc_NtkForEachPo( pNtk, pNode, i )
1169 //if( strstr( Abc_ObjName( pNode ), "assume_fair") != NULL )
1170 if( nodeName_starts_with( pNode, "assume_fair" ) )
1171 {
1172 Vec_PtrPush( vFair, Aig_ManCo( pAig, i ) );
1173 fairCounter++;
1174 }
1175 printf("Number of fairness property found = %d\n", fairCounter);
1176 return vFair;
1177}
1178
1179Vec_Ptr_t * populateSafetyAssertionVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
1180{
1181 Abc_Obj_t * pNode;
1182 int i, assertSafetyCounter = 0;
1183 Vec_Ptr_t * vAssertSafety;
1184
1185 vAssertSafety = Vec_PtrAlloc( 100 );
1186 Abc_NtkForEachPo( pNtk, pNode, i )
1187 //if( strstr( Abc_ObjName( pNode ), "Assert") != NULL )
1188 if( nodeName_starts_with( pNode, "assert_safety" ) || nodeName_starts_with( pNode, "Assert" ))
1189 {
1190 Vec_PtrPush( vAssertSafety, Aig_ManCo( pAig, i ) );
1191 assertSafetyCounter++;
1192 }
1193 printf("Number of safety property found = %d\n", assertSafetyCounter);
1194 return vAssertSafety;
1195}
1196
1197Vec_Ptr_t * populateSafetyAssumptionVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
1198{
1199 Abc_Obj_t * pNode;
1200 int i, assumeSafetyCounter = 0;
1201 Vec_Ptr_t * vAssumeSafety;
1202
1203 vAssumeSafety = Vec_PtrAlloc( 100 );
1204 Abc_NtkForEachPo( pNtk, pNode, i )
1205 //if( strstr( Abc_ObjName( pNode ), "Assert") != NULL )
1206 if( nodeName_starts_with( pNode, "assume_safety" ) || nodeName_starts_with( pNode, "Assume" ))
1207 {
1208 Vec_PtrPush( vAssumeSafety, Aig_ManCo( pAig, i ) );
1209 assumeSafetyCounter++;
1210 }
1211 printf("Number of assume_safety property found = %d\n", assumeSafetyCounter);
1212 return vAssumeSafety;
1213}
1214
1215void updateNewNetworkNameManager( Abc_Ntk_t *pNtk, Aig_Man_t *pAig, Vec_Ptr_t *vPiNames, Vec_Ptr_t *vLoNames )
1216{
1217 Aig_Obj_t *pObj;
1218 Abc_Obj_t *pNode;
1219 int i, ntkObjId;
1220
1221 pNtk->pManName = Nm_ManCreate( Abc_NtkCiNum( pNtk ) );
1222
1223 if( vPiNames )
1224 {
1225 Saig_ManForEachPi( pAig, pObj, i )
1226 {
1227 ntkObjId = Abc_NtkCi( pNtk, i )->Id;
1228 //printf("Pi %d, Saved Name = %s, id = %d\n", i, Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), Vec_PtrEntry(vPiNames, i), NULL ), ntkObjId);
1229 Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), (char *)Vec_PtrEntry(vPiNames, i), NULL );
1230 }
1231 }
1232 if( vLoNames )
1233 {
1234 Saig_ManForEachLo( pAig, pObj, i )
1235 {
1236 ntkObjId = Abc_NtkCi( pNtk, Saig_ManPiNum( pAig ) + i )->Id;
1237 //printf("Lo %d, Saved name = %s, id = %d\n", i, Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), Vec_PtrEntry(vLoNames, i), NULL ), ntkObjId);
1238 Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), (char *)Vec_PtrEntry(vLoNames, i), NULL );
1239 }
1240 }
1241
1242 Abc_NtkForEachPo(pNtk, pNode, i)
1243 {
1244 Abc_ObjAssignName(pNode, "assert_safety_", Abc_ObjName(pNode) );
1245 }
1246
1247 // assign latch input names
1248 Abc_NtkForEachLatch(pNtk, pNode, i)
1249 if ( Nm_ManFindNameById(pNtk->pManName, Abc_ObjFanin0(pNode)->Id) == NULL )
1250 Abc_ObjAssignName( Abc_ObjFanin0(pNode), Abc_ObjName(Abc_ObjFanin0(pNode)), NULL );
1251}
1252
1253
1254int Abc_CommandAbcLivenessToSafety( Abc_Frame_t * pAbc, int argc, char ** argv )
1255{
1256 FILE * pOut, * pErr;
1257 Abc_Ntk_t * pNtk, * pNtkTemp, *pNtkNew, *pNtkOld;
1258 Aig_Man_t * pAig, *pAigNew = NULL;
1259 int c;
1260 Vec_Ptr_t * vLive, * vFair, *vAssertSafety, *vAssumeSafety;
1261 int directive = -1;
1262
1263 pNtk = Abc_FrameReadNtk(pAbc);
1264 pOut = Abc_FrameReadOut(pAbc);
1265 pErr = Abc_FrameReadErr(pAbc);
1266
1267 if( argc == 1 )
1268 {
1269 assert( directive == -1 );
1270 directive = FULL_BIERE_MODE;
1271 }
1272 else
1273 {
1274 Extra_UtilGetoptReset();
1275 while ( ( c = Extra_UtilGetopt( argc, argv, "1slh" ) ) != EOF )
1276 {
1277 switch( c )
1278 {
1279 case '1':
1280 if( directive == -1 )
1281 directive = FULL_BIERE_ONE_LOOP_MODE;
1282 else
1283 {
1284 assert( directive == IGNORE_LIVENESS_KEEP_SAFETY_MODE || directive == IGNORE_SAFETY_KEEP_LIVENESS_MODE );
1285 if( directive == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
1286 directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE;
1287 else
1288 directive = IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE;
1289 }
1290 break;
1291 case 's':
1292 if( directive == -1 )
1293 directive = IGNORE_SAFETY_KEEP_LIVENESS_MODE;
1294 else
1295 {
1296 if( directive != FULL_BIERE_ONE_LOOP_MODE )
1297 goto usage;
1298 assert(directive == FULL_BIERE_ONE_LOOP_MODE);
1299 directive = IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE;
1300 }
1301 break;
1302 case 'l':
1303 if( directive == -1 )
1304 directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE;
1305 else
1306 {
1307 if( directive != FULL_BIERE_ONE_LOOP_MODE )
1308 goto usage;
1309 assert(directive == FULL_BIERE_ONE_LOOP_MODE);
1310 directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE;
1311 }
1312 break;
1313 case 'h':
1314 goto usage;
1315 default:
1316 goto usage;
1317 }
1318 }
1319 }
1320
1321 if ( pNtk == NULL )
1322 {
1323 fprintf( pErr, "Empty network.\n" );
1324 return 1;
1325 }
1326 if( !Abc_NtkIsStrash( pNtk ) )
1327 {
1328 printf("The input network was not strashed, strashing....\n");
1329 pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
1330 pNtkOld = pNtkTemp;
1331 pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
1332 vLive = populateLivenessVector( pNtk, pAig );
1333 vFair = populateFairnessVector( pNtk, pAig );
1334 vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
1335 vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
1336 }
1337 else
1338 {
1339 pAig = Abc_NtkToDar( pNtk, 0, 1 );
1340 pNtkOld = pNtk;
1341 vLive = populateLivenessVector( pNtk, pAig );
1342 vFair = populateFairnessVector( pNtk, pAig );
1343 vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
1344 vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
1345 }
1346
1347 switch( directive )
1348 {
1349 case FULL_BIERE_MODE:
1350 //if( Vec_PtrSize(vLive) == 0 && Vec_PtrSize(vAssertSafety) == 0 )
1351 //{
1352 // printf("Input circuit has NO safety and NO liveness property, original network is not disturbed\n");
1353 // return 1;
1354 //}
1355 //else
1356 //{
1357 pAigNew = LivenessToSafetyTransformation( FULL_BIERE_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
1358 if( Aig_ManRegNum(pAigNew) != 0 )
1359 printf("A new circuit is produced with\n\t2 POs - one for safety and one for liveness.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created if the original circuit is combinational\n\tnon-property POs are suppressed\n");
1360 break;
1361 //}
1362 case FULL_BIERE_ONE_LOOP_MODE:
1363 //if( Vec_PtrSize(vLive) == 0 && Vec_PtrSize(vAssertSafety) == 0 )
1364 //{
1365 // printf("Input circuit has NO safety and NO liveness property, original network is not disturbed\n");
1366 // return 1;
1367 //}
1368 //else
1369 //{
1370 pAigNew = LivenessToSafetyTransformationOneStepLoop( FULL_BIERE_ONE_LOOP_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
1371 if( Aig_ManRegNum(pAigNew) != 0 )
1372 printf("A new circuit is produced with\n\t2 POs - one for safety and one for liveness.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created\n\tnon-property POs are suppressed\n");
1373 break;
1374 //}
1375 case IGNORE_LIVENESS_KEEP_SAFETY_MODE:
1376 //if( Vec_PtrSize(vAssertSafety) == 0 )
1377 //{
1378 // printf("Input circuit has NO safety property, original network is not disturbed\n");
1379 // return 1;
1380 //}
1381 //else
1382 //{
1383 pAigNew = LivenessToSafetyTransformation( IGNORE_LIVENESS_KEEP_SAFETY_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
1384 if( Aig_ManRegNum(pAigNew) != 0 )
1385 printf("A new circuit is produced with\n\t1 PO - only for safety property; liveness properties are ignored, if any.\n\tno additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created\n\tnon-property POs are suppressed\n");
1386 break;
1387 //}
1388 case IGNORE_SAFETY_KEEP_LIVENESS_MODE:
1389 //if( Vec_PtrSize(vLive) == 0 )
1390 //{
1391 // printf("Input circuit has NO liveness property, original network is not disturbed\n");
1392 // return 1;
1393 //}
1394 //else
1395 //{
1396 pAigNew = LivenessToSafetyTransformation( IGNORE_SAFETY_KEEP_LIVENESS_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
1397 if( Aig_ManRegNum(pAigNew) != 0 )
1398 printf("A new circuit is produced with\n\t1 PO - only for liveness property; safety properties are ignored, if any.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created if the original circuit is combinational\n\tnon-property POs are suppressed\n");
1399 break;
1400 //}
1401 case IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE:
1402 //if( Vec_PtrSize(vLive) == 0 )
1403 //{
1404 // printf("Input circuit has NO liveness property, original network is not disturbed\n");
1405 // return 1;
1406 //}
1407 //else
1408 //{
1409 pAigNew = LivenessToSafetyTransformationOneStepLoop( IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
1410 if( Aig_ManRegNum(pAigNew) != 0 )
1411 printf("New circuit is produced ignoring safety outputs!\nOnly liveness and fairness outputs are considered.\nShadow registers are not created\n");
1412 break;
1413 //}
1414 }
1415
1416#if 0
1417 if( argc == 1 )
1418 {
1419 pAigNew = LivenessToSafetyTransformation( FULL_BIERE_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
1420 if( Aig_ManRegNum(pAigNew) != 0 )
1421 printf("New circuit is produced considering all safety, liveness and fairness outputs.\nBiere's logic is created\n");
1422 }
1423 else
1424 {
1425 Extra_UtilGetoptReset();
1426 c = Extra_UtilGetopt( argc, argv, "1lsh" );
1427 if( c == '1' )
1428 {
1429 if ( pNtk == NULL )
1430 {
1431 fprintf( pErr, "Empty network.\n" );
1432 return 1;
1433 }
1434 if( !Abc_NtkIsStrash( pNtk ) )
1435 {
1436 printf("The input network was not strashed, strashing....\n");
1437 pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
1438 pNtkOld = pNtkTemp;
1439 pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
1440 vLive = populateLivenessVector( pNtk, pAig );
1441 vFair = populateFairnessVector( pNtk, pAig );
1442 vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
1443 vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
1444 }
1445 else
1446 {
1447 pAig = Abc_NtkToDar( pNtk, 0, 1 );
1448 pNtkOld = pNtk;
1449 vLive = populateLivenessVector( pNtk, pAig );
1450 vFair = populateFairnessVector( pNtk, pAig );
1451 vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
1452 vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
1453 }
1454 pAigNew = LivenessToSafetyTransformationOneStepLoop( pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
1455 }
1456 else if( c == 'l' )
1457 {
1458 if ( pNtk == NULL )
1459 {
1460 fprintf( pErr, "Empty network.\n" );
1461 return 1;
1462 }
1463 if( !Abc_NtkIsStrash( pNtk ) )
1464 {
1465 printf("The input network was not strashed, strashing....\n");
1466 pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
1467 pNtkOld = pNtkTemp;
1468 pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
1469 vLive = populateLivenessVector( pNtk, pAig );
1470 vFair = populateFairnessVector( pNtk, pAig );
1471 vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
1472 vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
1473 }
1474 else
1475 {
1476 pAig = Abc_NtkToDar( pNtk, 0, 1 );
1477 pNtkOld = pNtk;
1478 vLive = populateLivenessVector( pNtk, pAig );
1479 vFair = populateFairnessVector( pNtk, pAig );
1480 vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
1481 vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
1482 }
1483 pAigNew = LivenessToSafetyTransformation( IGNORE_LIVENESS_KEEP_SAFETY_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
1484 if( Aig_ManRegNum(pAigNew) != 0 )
1485 printf("New circuit is produced ignoring liveness outputs!\nOnly safety outputs are kept.\nBiere's logic is not created\n");
1486 }
1487 else if( c == 's' )
1488 {
1489 if ( pNtk == NULL )
1490 {
1491 fprintf( pErr, "Empty network.\n" );
1492 return 1;
1493 }
1494
1495 if( !Abc_NtkIsStrash( pNtk ) )
1496 {
1497 printf("The input network was not strashed, strashing....\n");
1498 pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
1499 pNtkOld = pNtkTemp;
1500 pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
1501 vLive = populateLivenessVector( pNtk, pAig );
1502 vFair = populateFairnessVector( pNtk, pAig );
1503 vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
1504 vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
1505 }
1506 else
1507 {
1508 pAig = Abc_NtkToDar( pNtk, 0, 1 );
1509 pNtkOld = pNtk;
1510 vLive = populateLivenessVector( pNtk, pAig );
1511 vFair = populateFairnessVector( pNtk, pAig );
1512 vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
1513 vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
1514 }
1515 pAigNew = LivenessToSafetyTransformation( IGNORE_SAFETY_KEEP_LIVENESS_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
1516 if( Aig_ManRegNum(pAigNew) != 0 )
1517 printf("New circuit is produced ignoring safety outputs!\nOnly liveness and fairness outputs are considered.\nBiere's logic is created\n");
1518 }
1519 else if( c == 'h' )
1520 goto usage;
1521 else
1522 goto usage;
1523 }
1524#endif
1525
1526#if 0
1527 Aig_ManPrintStats( pAigNew );
1528 printf("\nDetail statistics*************************************\n");
1529 printf("Number of true primary inputs = %d\n", Saig_ManPiNum( pAigNew ));
1530 printf("Number of true primary outputs = %d\n", Saig_ManPoNum( pAigNew ));
1531 printf("Number of true latch outputs = %d\n", Saig_ManCiNum( pAigNew ) - Saig_ManPiNum( pAigNew ));
1532 printf("Number of true latch inputs = %d\n", Saig_ManCoNum( pAigNew ) - Saig_ManPoNum( pAigNew ));
1533 printf("Numer of registers = %d\n", Saig_ManRegNum( pAigNew ) );
1534 printf("\n*******************************************************\n");
1535#endif
1536
1537 pNtkNew = Abc_NtkFromAigPhase( pAigNew );
1538 pNtkNew->pName = Abc_UtilStrsav( pAigNew->pName );
1539
1540 if ( !Abc_NtkCheck( pNtkNew ) )
1541 fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" );
1542
1543 updateNewNetworkNameManager( pNtkNew, pAigNew, vecPiNames, vecLoNames );
1544 Abc_FrameSetCurrentNetwork( pAbc, pNtkNew );
1545
1546#if 0
1547#ifndef DUPLICATE_CKT_DEBUG
1548 Saig_ManForEachPi( pAigNew, pObj, i )
1549 assert( strcmp( (char *)Vec_PtrEntry(vecPiNames, i), retrieveTruePiName( pNtk, pAig, pAigNew, pObj ) ) == 0 );
1550 //printf("Name of %d-th Pi = %s, %s\n", i, retrieveTruePiName( pNtk, pAig, pAigNew, pObj ), (char *)Vec_PtrEntry(vecPiNames, i) );
1551
1552 Saig_ManForEachLo( pAigNew, pObj, i )
1553 assert( strcmp( (char *)Vec_PtrEntry(vecLoNames, i), retrieveLOName( pNtk, pAig, pAigNew, pObj, vLive, vFair ) ) == 0 );
1554#endif
1555#endif
1556
1557 return 0;
1558
1559usage:
1560 fprintf( stdout, "usage: l2s [-1lsh]\n" );
1561 fprintf( stdout, "\t performs Armin Biere's live-to-safe transformation\n" );
1562 fprintf( stdout, "\t-1 : no shadow logic, presume all loops are self loops\n");
1563 fprintf( stdout, "\t-l : ignore liveness and fairness outputs\n");
1564 fprintf( stdout, "\t-s : ignore safety assertions and assumptions\n");
1565 fprintf( stdout, "\t-h : print command usage\n");
1566 return 1;
1567}
1568
1569Vec_Int_t * prepareFlopVector( Aig_Man_t * pAig, int vectorLength )
1570{
1571 Vec_Int_t *vFlops;
1572 int i;
1573
1574 vFlops = Vec_IntAlloc( vectorLength );
1575
1576 for( i=0; i<vectorLength; i++ )
1577 Vec_IntPush( vFlops, i );
1578
1579#if 0
1580 Vec_IntPush( vFlops, 19 );
1581 Vec_IntPush( vFlops, 20 );
1582 Vec_IntPush( vFlops, 23 );
1583 Vec_IntPush( vFlops, 24 );
1584 //Vec_IntPush( vFlops, 2 );
1585 //Vec_IntPush( vFlops, 3 );
1586 //Vec_IntPush( vFlops, 4 );
1587 //Vec_IntPush( vFlops, 5 );
1588 //Vec_IntPush( vFlops, 8 );
1589 //Vec_IntPush( vFlops, 9 );
1590 //Vec_IntPush( vFlops, 10 );
1591 //Vec_IntPush( vFlops, 11 );
1592 //Vec_IntPush( vFlops, 0 );
1593 //Vec_IntPush( vFlops, 0 );
1594#endif
1595
1596 return vFlops;
1597}
1598
1599int Abc_CommandAbcLivenessToSafetyAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
1600{
1601 FILE * pOut, * pErr;
1602 Abc_Ntk_t * pNtk, * pNtkTemp, *pNtkNew, *pNtkOld;
1603 Aig_Man_t * pAig, *pAigNew = NULL;
1604 int c;
1605 Vec_Ptr_t * vLive, * vFair, *vAssertSafety, *vAssumeSafety;
1606 int directive = -1;
1607 Vec_Int_t * vFlops;
1608
1609 pNtk = Abc_FrameReadNtk(pAbc);
1610 pOut = Abc_FrameReadOut(pAbc);
1611 pErr = Abc_FrameReadErr(pAbc);
1612
1613 if( argc == 1 )
1614 {
1615 assert( directive == -1 );
1616 directive = FULL_BIERE_MODE;
1617 }
1618 else
1619 {
1620 Extra_UtilGetoptReset();
1621 while ( ( c = Extra_UtilGetopt( argc, argv, "1slh" ) ) != EOF )
1622 {
1623 switch( c )
1624 {
1625 case '1':
1626 if( directive == -1 )
1627 directive = FULL_BIERE_ONE_LOOP_MODE;
1628 else
1629 {
1630 assert( directive == IGNORE_LIVENESS_KEEP_SAFETY_MODE || directive == IGNORE_SAFETY_KEEP_LIVENESS_MODE );
1631 if( directive == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
1632 directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE;
1633 else
1634 directive = IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE;
1635 }
1636 break;
1637 case 's':
1638 if( directive == -1 )
1639 directive = IGNORE_SAFETY_KEEP_LIVENESS_MODE;
1640 else
1641 {
1642 if( directive != FULL_BIERE_ONE_LOOP_MODE )
1643 goto usage;
1644 assert(directive == FULL_BIERE_ONE_LOOP_MODE);
1645 directive = IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE;
1646 }
1647 break;
1648 case 'l':
1649 if( directive == -1 )
1650 directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE;
1651 else
1652 {
1653 if( directive != FULL_BIERE_ONE_LOOP_MODE )
1654 goto usage;
1655 assert(directive == FULL_BIERE_ONE_LOOP_MODE);
1656 directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE;
1657 }
1658 break;
1659 case 'h':
1660 goto usage;
1661 default:
1662 goto usage;
1663 }
1664 }
1665 }
1666
1667 if ( pNtk == NULL )
1668 {
1669 fprintf( pErr, "Empty network.\n" );
1670 return 1;
1671 }
1672 if( !Abc_NtkIsStrash( pNtk ) )
1673 {
1674 printf("The input network was not strashed, strashing....\n");
1675 pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
1676 pNtkOld = pNtkTemp;
1677 pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
1678 vLive = populateLivenessVector( pNtk, pAig );
1679 vFair = populateFairnessVector( pNtk, pAig );
1680 vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
1681 vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
1682 }
1683 else
1684 {
1685 pAig = Abc_NtkToDar( pNtk, 0, 1 );
1686 pNtkOld = pNtk;
1687 vLive = populateLivenessVector( pNtk, pAig );
1688 vFair = populateFairnessVector( pNtk, pAig );
1689 vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
1690 vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
1691 }
1692
1693 vFlops = prepareFlopVector( pAig, Aig_ManRegNum(pAig)%2 == 0? Aig_ManRegNum(pAig)/2 : (Aig_ManRegNum(pAig)-1)/2);
1694
1695 //vFlops = prepareFlopVector( pAig, 100 );
1696
1697 switch( directive )
1698 {
1699 case FULL_BIERE_MODE:
1700 //if( Vec_PtrSize(vLive) == 0 && Vec_PtrSize(vAssertSafety) == 0 )
1701 //{
1702 // printf("Input circuit has NO safety and NO liveness property, original network is not disturbed\n");
1703 // return 1;
1704 //}
1705 //else
1706 //{
1707 pAigNew = LivenessToSafetyTransformationAbs( FULL_BIERE_MODE, pNtk, pAig, vFlops, vLive, vFair, vAssertSafety, vAssumeSafety );
1708 if( Aig_ManRegNum(pAigNew) != 0 )
1709 printf("A new circuit is produced with\n\t2 POs - one for safety and one for liveness.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created if the original circuit is combinational\n\tnon-property POs are suppressed\n");
1710 break;
1711 //}
1712 case FULL_BIERE_ONE_LOOP_MODE:
1713 //if( Vec_PtrSize(vLive) == 0 && Vec_PtrSize(vAssertSafety) == 0 )
1714 //{
1715 // printf("Input circuit has NO safety and NO liveness property, original network is not disturbed\n");
1716 // return 1;
1717 //}
1718 //else
1719 //{
1720 pAigNew = LivenessToSafetyTransformationOneStepLoop( FULL_BIERE_ONE_LOOP_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
1721 if( Aig_ManRegNum(pAigNew) != 0 )
1722 printf("A new circuit is produced with\n\t2 POs - one for safety and one for liveness.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created\n\tnon-property POs are suppressed\n");
1723 break;
1724 //}
1725 case IGNORE_LIVENESS_KEEP_SAFETY_MODE:
1726 //if( Vec_PtrSize(vAssertSafety) == 0 )
1727 //{
1728 // printf("Input circuit has NO safety property, original network is not disturbed\n");
1729 // return 1;
1730 //}
1731 //else
1732 //{
1733 pAigNew = LivenessToSafetyTransformationAbs( IGNORE_LIVENESS_KEEP_SAFETY_MODE, pNtk, pAig, vFlops, vLive, vFair, vAssertSafety, vAssumeSafety );
1734 if( Aig_ManRegNum(pAigNew) != 0 )
1735 printf("A new circuit is produced with\n\t1 PO - only for safety property; liveness properties are ignored, if any.\n\tno additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created\n\tnon-property POs are suppressed\n");
1736 break;
1737 //}
1738 case IGNORE_SAFETY_KEEP_LIVENESS_MODE:
1739 //if( Vec_PtrSize(vLive) == 0 )
1740 //{
1741 // printf("Input circuit has NO liveness property, original network is not disturbed\n");
1742 // return 1;
1743 //}
1744 //else
1745 //{
1746 pAigNew = LivenessToSafetyTransformationAbs( IGNORE_SAFETY_KEEP_LIVENESS_MODE, pNtk, pAig, vFlops, vLive, vFair, vAssertSafety, vAssumeSafety );
1747 if( Aig_ManRegNum(pAigNew) != 0 )
1748 printf("A new circuit is produced with\n\t1 PO - only for liveness property; safety properties are ignored, if any.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created if the original circuit is combinational\n\tnon-property POs are suppressed\n");
1749 break;
1750 //}
1751 case IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE:
1752 //if( Vec_PtrSize(vLive) == 0 )
1753 //{
1754 // printf("Input circuit has NO liveness property, original network is not disturbed\n");
1755 // return 1;
1756 //}
1757 //else
1758 //{
1759 pAigNew = LivenessToSafetyTransformationOneStepLoop( IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
1760 if( Aig_ManRegNum(pAigNew) != 0 )
1761 printf("New circuit is produced ignoring safety outputs!\nOnly liveness and fairness outputs are considered.\nShadow registers are not created\n");
1762 break;
1763 //}
1764 }
1765
1766 pNtkNew = Abc_NtkFromAigPhase( pAigNew );
1767 pNtkNew->pName = Abc_UtilStrsav( pAigNew->pName );
1768
1769 if ( !Abc_NtkCheck( pNtkNew ) )
1770 fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" );
1771
1772 updateNewNetworkNameManager( pNtkNew, pAigNew, vecPiNames,vecLoNames );
1773 Abc_FrameSetCurrentNetwork( pAbc, pNtkNew );
1774
1775#if 0
1776#ifndef DUPLICATE_CKT_DEBUG
1777 Saig_ManForEachPi( pAigNew, pObj, i )
1778 assert( strcmp( (char *)Vec_PtrEntry(vecPiNames, i), retrieveTruePiName( pNtk, pAig, pAigNew, pObj ) ) == 0 );
1779 //printf("Name of %d-th Pi = %s, %s\n", i, retrieveTruePiName( pNtk, pAig, pAigNew, pObj ), (char *)Vec_PtrEntry(vecPiNames, i) );
1780
1781 Saig_ManForEachLo( pAigNew, pObj, i )
1782 assert( strcmp( (char *)Vec_PtrEntry(vecLoNames, i), retrieveLOName( pNtk, pAig, pAigNew, pObj, vLive, vFair ) ) == 0 );
1783#endif
1784#endif
1785
1786 return 0;
1787
1788usage:
1789 fprintf( stdout, "usage: l2s [-1lsh]\n" );
1790 fprintf( stdout, "\t performs Armin Biere's live-to-safe transformation\n" );
1791 fprintf( stdout, "\t-1 : no shadow logic, presume all loops are self loops\n");
1792 fprintf( stdout, "\t-l : ignore liveness and fairness outputs\n");
1793 fprintf( stdout, "\t-s : ignore safety assertions and assumptions\n");
1794 fprintf( stdout, "\t-h : print command usage\n");
1795 return 1;
1796}
1797
1798Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, Aig_Man_t * p,
1799 Vec_Ptr_t *vLive, Vec_Ptr_t *vFair, Vec_Ptr_t *vAssertSafety, Vec_Ptr_t *vAssumeSafety,
1800 int *numLtlProcessed, Vec_Ptr_t *ltlBuffer )
1801{
1802 Aig_Man_t * pNew;
1803 int i, ii, iii, nRegCount;
1804 Aig_Obj_t * pObjSavePi = NULL;
1805 Aig_Obj_t *pObjSavedLo = NULL, *pObjSavedLi = NULL;
1806 Aig_Obj_t *pObj, *pMatch;
1807 Aig_Obj_t *pObjSaveOrSaved = NULL, *pObjSaveAndNotSaved = NULL, *pObjSavedLoAndEquality;
1808 Aig_Obj_t *pObjShadowLo, *pObjShadowLi, *pObjShadowLiDriver;
1809 Aig_Obj_t *pObjXor, *pObjXnor, *pObjAndAcc;
1810 Aig_Obj_t *pObjLive, *pObjSafetyGate;
1811 Aig_Obj_t *pObjSafetyPropertyOutput;
1812 Aig_Obj_t *pObjOriginalSafetyPropertyOutput;
1813 Aig_Obj_t *pDriverImage, *pArgument, *collectiveAssertSafety, *collectiveAssumeSafety;
1814 Aig_Obj_t *pNegatedSafetyConjunction = NULL;
1815 Aig_Obj_t *pObjSafetyAndLiveToSafety;
1816 char *nodeName, *pFormula;
1817 int piCopied = 0, liCopied = 0, loCopied = 0, liCreated = 0, loCreated = 0, liveLatch = 0;//, piVecIndex = 0, fairLatch = 0;
1818 Vec_Ptr_t *vSignal, *vTopASTNodeArray = NULL;
1819 ltlNode *pEnrtyGLOBALLY;
1820 ltlNode *topNodeOfAST, *tempTopASTNode;
1821 Vec_Vec_t *vAigGFMap;
1822 Vec_Ptr_t *vSignalMemory, *vGFFlopMemory, *vPoForLtlProps = NULL;
1823 Vec_Ptr_t *vecInputLtlFormulae;
1824
1825 vecPis = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
1826 vecPiNames = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
1827
1828 vecLos = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
1829 vecLoNames = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
1830
1831 //****************************************************************
1832 //step0: Parsing the LTL formula
1833 //****************************************************************
1834 //Vec_PtrForEachEntry( char *, pNtk->vLtlProperties, pFormula, i )
1835 // printf("\ninput LTL formula [%d] = %s\n", i, pFormula );
1836
1837
1838#ifdef MULTIPLE_LTL_FORMULA
1839
1840
1841 //***************************************************************************
1842 //Reading input LTL formulae from Ntk data-structure and creating
1843 //AST for them, Steps involved:
1844 // parsing -> AST creation -> well-formedness check -> signal name check
1845 //***************************************************************************
1846
1847 //resetting numLtlProcessed
1848 *numLtlProcessed = 0;
1849
1850 if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
1851 {
1852 //if( ltlBuffer )
1853 vecInputLtlFormulae = ltlBuffer;
1854 //vecInputLtlFormulae = pNtk->vLtlProperties;
1855 if( vecInputLtlFormulae )
1856 {
1857 vTopASTNodeArray = Vec_PtrAlloc( Vec_PtrSize( vecInputLtlFormulae ) );
1858 printf("\n");
1859 Vec_PtrForEachEntry( char *, vecInputLtlFormulae, pFormula, i )
1860 {
1861 tempTopASTNode = parseFormulaCreateAST( pFormula );
1862 //traverseAbstractSyntaxTree_postFix( tempTopASTNode );
1863 if( tempTopASTNode )
1864 {
1865 printf("Formula %d: AST is created, ", i+1);
1866 if( isWellFormed( tempTopASTNode ) )
1867 printf("Well-formedness check PASSED, ");
1868 else
1869 {
1870 printf("Well-formedness check FAILED!!\n");
1871 printf("AST will be ignored for formula %d, no extra logic will be added for this formula\n", i+1 );
1872 //do memory management to free the created AST
1873 continue;
1874 }
1875 if( checkSignalNameExistence( pNtk, tempTopASTNode ) )
1876 printf("Signal check PASSED\n");
1877 else
1878 {
1879 printf("Signal check FAILED!!");
1880 printf("AST will be ignored for formula %d, no extra logic will be added for this formula\n", i+1 );
1881 //do memory management to free the created AST
1882 continue;
1883 }
1884 Vec_PtrPush( vTopASTNodeArray, tempTopASTNode );
1885 (*numLtlProcessed)++;
1886 }
1887 else
1888 printf("\nNo AST has been created for formula %d, no extra logic will be added\n", i+1 );
1889 }
1890 }
1891 printf("\n");
1892 if( Vec_PtrSize( vTopASTNodeArray ) == 0 )
1893 {
1894 //printf("\nNo AST has been created for any formula; hence the circuit is left untouched\n");
1895 printf("\nCurrently aborting, need to take care when Vec_PtrSize( vTopASTNodeArray ) == 0\n");
1896 exit(0);
1897 }
1898 }
1899
1900 //****************************************************************
1901 // Step1: create the new manager
1902 // Note: The new manager is created with "2 * Aig_ManObjNumMax(p)"
1903 // nodes, but this selection is arbitrary - need to be justified
1904 //****************************************************************
1905 pNew = Aig_ManStart( 2 * Aig_ManObjNumMax(p) );
1906 pNew->pName = (char *)malloc( strlen( pNtk->pName ) + strlen("_l3s") + 1 );
1907 sprintf(pNew->pName, "%s_%s", pNtk->pName, "l3s");
1908 pNew->pSpec = NULL;
1909
1910 //****************************************************************
1911 // Step 2: map constant nodes
1912 //****************************************************************
1913 pObj = Aig_ManConst1( p );
1914 pObj->pData = Aig_ManConst1( pNew );
1915
1916 //****************************************************************
1917 // Step 3: create true PIs
1918 //****************************************************************
1919 Saig_ManForEachPi( p, pObj, i )
1920 {
1921 piCopied++;
1922 pObj->pData = Aig_ObjCreateCi(pNew);
1923 Vec_PtrPush( vecPis, pObj->pData );
1924 nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) ));
1925 Vec_PtrPush( vecPiNames, nodeName );
1926 }
1927
1928 //****************************************************************
1929 // Step 4: create the special Pi corresponding to SAVE
1930 //****************************************************************
1931 if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
1932 {
1933 pObjSavePi = Aig_ObjCreateCi( pNew );
1934 nodeName = "SAVE_BIERE",
1935 Vec_PtrPush( vecPiNames, nodeName );
1936 }
1937
1938 //****************************************************************
1939 // Step 5: create register outputs
1940 //****************************************************************
1941 Saig_ManForEachLo( p, pObj, i )
1942 {
1943 loCopied++;
1944 pObj->pData = Aig_ObjCreateCi(pNew);
1945 Vec_PtrPush( vecLos, pObj->pData );
1946 nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ));
1947 Vec_PtrPush( vecLoNames, nodeName );
1948 }
1949
1950 //****************************************************************
1951 // Step 6: create "saved" register output
1952 //****************************************************************
1953 if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
1954 {
1955 loCreated++;
1956 pObjSavedLo = Aig_ObjCreateCi( pNew );
1957 Vec_PtrPush( vecLos, pObjSavedLo );
1958 nodeName = "SAVED_LO";
1959 Vec_PtrPush( vecLoNames, nodeName );
1960 }
1961
1962 //****************************************************************
1963 // Step 7: create the OR gate and the AND gate directly fed by "SAVE" Pi
1964 //****************************************************************
1965 if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
1966 {
1967 pObjSaveOrSaved = Aig_Or( pNew, pObjSavePi, pObjSavedLo );
1968 pObjSaveAndNotSaved = Aig_And( pNew, pObjSavePi, Aig_Not(pObjSavedLo) );
1969 }
1970
1971 //********************************************************************
1972 // Step 8: create internal nodes
1973 //********************************************************************
1974 Aig_ManForEachNode( p, pObj, i )
1975 {
1976 pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
1977 }
1978
1979
1980 //********************************************************************
1981 // Step 8.x : create PO for each safety assertions
1982 // NOTE : Here the output is purposely inverted as it will be thrown to
1983 // dprove
1984 //********************************************************************
1985 assert( pNegatedSafetyConjunction == NULL );
1986 if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE)
1987 {
1988 if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) == 0 )
1989 {
1990 pObjAndAcc = Aig_ManConst1( pNew );
1991 Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
1992 {
1993 pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
1994 pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
1995 }
1996 pNegatedSafetyConjunction = Aig_Not(pObjAndAcc);
1997 if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
1998 pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_Not(pObjAndAcc) );
1999 }
2000 else if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) != 0 )
2001 {
2002 pObjAndAcc = Aig_ManConst1( pNew );
2003 Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
2004 {
2005 pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
2006 pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
2007 }
2008 collectiveAssertSafety = pObjAndAcc;
2009
2010 pObjAndAcc = Aig_ManConst1( pNew );
2011 Vec_PtrForEachEntry( Aig_Obj_t *, vAssumeSafety, pObj, i )
2012 {
2013 pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
2014 pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
2015 }
2016 collectiveAssumeSafety = pObjAndAcc;
2017 pNegatedSafetyConjunction = Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety );
2018 if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
2019 pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) );
2020 }
2021 else
2022 {
2023 printf("WARNING!! No safety property is found, a new (negated) constant 1 output is created\n");
2024 pNegatedSafetyConjunction = Aig_Not( Aig_ManConst1(pNew) );
2025 if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
2026 pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_Not( Aig_ManConst1(pNew) ) );
2027 }
2028 }
2029 assert( pNegatedSafetyConjunction != NULL );
2030
2031 //********************************************************************
2032 // Step 9: create the safety property output gate for the liveness properties
2033 // discuss with Sat/Alan for an alternative implementation
2034 //********************************************************************
2035 if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
2036 {
2037 vPoForLtlProps = Vec_PtrAlloc( Vec_PtrSize( vTopASTNodeArray ) );
2038 if( Vec_PtrSize( vTopASTNodeArray ) )
2039 {
2040 //no effective AST for any input LTL property
2041 //must do something graceful
2042 }
2043 for( i=0; i<Vec_PtrSize( vTopASTNodeArray ); i++ )
2044 {
2045 pObjSafetyPropertyOutput = Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
2046 Vec_PtrPush( vPoForLtlProps, pObjSafetyPropertyOutput );
2047 }
2048 }
2049
2050 //*************************************************************************************
2051 // Step 10: Placeholder PO's were created for Liveness property outputs in the
2052 // last step. FYI, # of new liveness property outputs = # of LTL properties in the circuit
2053 // It is time for creation of loop LI's and other stuff
2054 // Now creating register inputs for the original flops
2055 //*************************************************************************************
2056 nRegCount = 0;
2057
2058 Saig_ManForEachLo( p, pObj, i )
2059 {
2060 pMatch = Saig_ObjLoToLi( p, pObj );
2061 Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
2062 nRegCount++;
2063 liCopied++;
2064 }
2065
2066 //*************************************************************************************
2067 // Step 11: create register input corresponding to the register "saved"
2068 //*************************************************************************************
2069 if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
2070 {
2071 #ifndef DUPLICATE_CKT_DEBUG
2072 pObjSavedLi = Aig_ObjCreateCo( pNew, pObjSaveOrSaved );
2073 nRegCount++;
2074 liCreated++;
2075
2076 pObjAndAcc = Aig_ManConst1( pNew );
2077
2078 //*************************************************************************************
2079 // Step 11: create the family of shadow registers, then create the cascade of Xnor
2080 // and And gates for the comparator
2081 //*************************************************************************************
2082 Saig_ManForEachLo( p, pObj, i )
2083 {
2084 //printf("\nKEMON RENDY = %s", Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i )) );
2085 //top|route0_target0_queue_with_credit0_queue0
2086 //top|route0_master0_queue2
2087 // if( strcmp( Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "top|route0_queue1_num[0]" ) == 0
2088 // || strcmp( Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "top|route0_queue1_num[1]" ) == 0 || strcmp( Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "top|route0_queue1_num[2]" ) == 0 )
2089 {
2090 pObjShadowLo = Aig_ObjCreateCi( pNew );
2091
2092 #ifdef PROPAGATE_NAMES
2093 Vec_PtrPush( vecLos, pObjShadowLo );
2094 nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ) ) + 10 );
2095 sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "SHADOW" );
2096
2097 Vec_PtrPush( vecLoNames, nodeName );
2098 #endif
2099
2100 pObjShadowLiDriver = Aig_Mux( pNew, pObjSaveAndNotSaved, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
2101 pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
2102 nRegCount++;
2103 loCreated++; liCreated++;
2104
2105 pObjXor = Aig_Exor( pNew, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
2106 pObjXnor = Aig_Not( pObjXor );
2107
2108 pObjAndAcc = Aig_And( pNew, pObjXnor, pObjAndAcc );
2109 }
2110 }
2111
2112 // create the AND gate whose output will be the signal "looped"
2113 pObjSavedLoAndEquality = Aig_And( pNew, pObjSavedLo, pObjAndAcc );
2114
2115 // create the master AND gate and corresponding AND and OR logic for the liveness properties
2116
2117 //*************************************************************************************
2118 // Step 11: logic for LTL properties:- (looped & ~theta) where theta is the input ltl
2119 // property
2120 // Description of some data-structure:
2121 //-------------------------------------------------------------------------------------
2122 // Name | Type | Purpose
2123 //-------------------------------------------------------------------------------------
2124 // vSignalMemory | Vec_Ptr_t * | A vector across all ASTs of the LTL properties
2125 // | | It remembers if OR+Latch for GF node has already been
2126 // | | created for a particular signal.
2127 // | |
2128 // vGFFlopMemory | Vec_Ptr_t * | A vector across all ASTs of the LTL properties
2129 // | | remembers if OR+Latch of a GF node has already been created
2130 // | |
2131 // vSignal | Vec_Ptr_t * | vector for each AST; contains pointers from GF nodes
2132 // | | to AIG signals
2133 // | |
2134 // vAigGFMap | Vec_Vec_t * | vAigGFMap[ index ] = vector of GF nodes pointing to
2135 // | | the same AIG node; "index" is the index of that
2136 // | | AIG node in the vector vSignal
2137 //*************************************************************************************
2138
2139 vSignalMemory = Vec_PtrAlloc(10);
2140 vGFFlopMemory = Vec_PtrAlloc(10);
2141
2142 Vec_PtrForEachEntry( ltlNode *, vTopASTNodeArray, topNodeOfAST, iii )
2143 {
2144 vSignal = Vec_PtrAlloc( 10 );
2145 vAigGFMap = Vec_VecAlloc( 10 );
2146
2147 //*************************************************************************************
2148 //Step 11a: for the current AST, find out the leaf level Boolean signal pointers from
2149 // the NEW aig.
2150 //*************************************************************************************
2151 populateBoolWithAigNodePtr( pNtk, p, pNew, topNodeOfAST );
2152 assert( checkAllBoolHaveAIGPointer( topNodeOfAST ) );
2153
2154 //*************************************************************************************
2155 //Step 11b: for each GF node, compute the pointer in AIG that it should point to
2156 // In particular, if the subtree below GF is some Boolean crown (including the case
2157 // of simple negation, create new logic and populate the AIG pointer in GF node
2158 // accordingly
2159 //*************************************************************************************
2160 populateAigPointerUnitGF( pNew, topNodeOfAST, vSignal, vAigGFMap );
2161
2162 //*************************************************************************************
2163 //Step 11c: everything below GF are computed. Now, it is time to create logic for individual
2164 // GF nodes (i.e. the OR gate and the latch and the Boolean crown of the AST
2165 //*************************************************************************************
2166 Vec_PtrForEachEntry( Aig_Obj_t *, vSignal, pObj, i )
2167 {
2168 //*********************************************************
2169 // Step 11c.1: if the OR+Latch of the particular signal is
2170 // not already created, create it. It may have already been
2171 // created from another property, so check it before creation
2172 //*********************************************************
2173 if( Vec_PtrFind( vSignalMemory, pObj ) == -1 )
2174 {
2175 liveLatch++;
2176
2177 pDriverImage = pObj;
2178 pObjShadowLo = Aig_ObjCreateCi( pNew );
2179 pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
2180 pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
2181
2182 nRegCount++;
2183 loCreated++; liCreated++;
2184
2185 Vec_PtrPush( vSignalMemory, pObj );
2186 Vec_PtrPush( vGFFlopMemory, pObjShadowLo );
2187
2188 #if 1
2189 #ifdef PROPAGATE_NAMES
2190 Vec_PtrPush( vecLos, pObjShadowLo );
2191 //nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 );
2192 //sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "LIVENESS" );
2193 nodeName = (char *)malloc( 20 );
2194 sprintf( nodeName, "n%d__%s", Aig_ObjId(pObjShadowLo), "GF_flop" );
2195 Vec_PtrPush( vecLoNames, nodeName );
2196 #endif
2197 #endif
2198 }
2199 else
2200 pObjShadowLo = (Aig_Obj_t *)Vec_PtrEntry( vGFFlopMemory, Vec_PtrFind( vSignalMemory, pObj ) );
2201
2202 Vec_VecForEachEntryLevel( ltlNode *, vAigGFMap, pEnrtyGLOBALLY, ii, i )
2203 setAIGNodePtrOfGloballyNode( pEnrtyGLOBALLY, pObjShadowLo);
2204
2205
2206 //#ifdef PROPAGATE_NAMES
2207 // Vec_PtrPush( vecLos, pObjShadowLo );
2208 // nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 );
2209 // sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "LIVENESS" );
2210 // Vec_PtrPush( vecLoNames, nodeName );
2211 //#endif
2212
2213 }
2214
2215 //*********************************************************
2216 //Step 11c.2: creating the Boolean crown
2217 //*********************************************************
2218 buildLogicFromLTLNode( pNew, topNodeOfAST );
2219
2220 //*********************************************************
2221 //Step 11c.3: creating logic for (looped & ~theta) and patching
2222 // it with the proper PO
2223 //Note: if ALLOW_SAFETY_PROPERTIES is defined then the final AND
2224 //gate is a conjunction of safety & liveness, i.e. SAFETY & (looped => theta)
2225 //since ABC convention demands a NOT gate at the end, the property logic
2226 //becomes !( SAFETY & (looped => theta) ) = !SAFETY + (looped & !theta)
2227 //*********************************************************
2228 pObjLive = retriveAIGPointerFromLTLNode( topNodeOfAST );
2229 pObjSafetyGate = Aig_And( pNew, pObjSavedLoAndEquality, Aig_Not(pObjLive) );
2230 #ifdef ALLOW_SAFETY_PROPERTIES
2231 printf("liveness output is conjoined with safety assertions\n");
2232 pObjSafetyAndLiveToSafety = Aig_Or( pNew, pObjSafetyGate, pNegatedSafetyConjunction );
2233 pObjSafetyPropertyOutput = (Aig_Obj_t *)Vec_PtrEntry( vPoForLtlProps, iii );
2234 Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyAndLiveToSafety );
2235 #else
2236 pObjSafetyPropertyOutput = Vec_PtrEntry( vPoForLtlProps, iii );
2237 Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyGate );
2238 #endif
2239 //refreshing vSignal and vAigGFMap arrays
2240 Vec_PtrFree( vSignal );
2241 Vec_VecFree( vAigGFMap );
2242 }
2243
2244 #endif
2245 }
2246#endif
2247
2248 Aig_ManSetRegNum( pNew, nRegCount );
2249
2250 Aig_ManCiCleanupBiere( pNew );
2251 Aig_ManCoCleanupBiere( pNew );
2252
2253 Aig_ManCleanup( pNew );
2254
2255 assert( Aig_ManCheck( pNew ) );
2256
2257 if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
2258 {
2259 assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjCioId(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
2260 assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) );
2261 //assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch );
2262 }
2263
2264
2265 return pNew;
2266}
2267
2268int Abc_CommandAbcLivenessToSafetyWithLTL( Abc_Frame_t * pAbc, int argc, char ** argv )
2269{
2270 FILE * pOut, * pErr;
2271 Abc_Ntk_t * pNtk, * pNtkTemp, *pNtkNew, *pNtkOld;
2272 Aig_Man_t * pAig, *pAigNew = NULL;
2273 int c;
2274 Vec_Ptr_t * vLive, * vFair, *vAssertSafety, *vAssumeSafety;
2275 int directive = -1;
2276// char *ltfFormulaString = NULL;
2277 int numOfLtlPropOutput;//, LTL_FLAG = 0;
2278 Vec_Ptr_t *ltlBuffer;
2279
2280 pNtk = Abc_FrameReadNtk(pAbc);
2281 pOut = Abc_FrameReadOut(pAbc);
2282 pErr = Abc_FrameReadErr(pAbc);
2283
2284 if( argc == 1 )
2285 {
2286 assert( directive == -1 );
2287 directive = FULL_BIERE_MODE;
2288 }
2289 else
2290 {
2291 Extra_UtilGetoptReset();
2292 while ( ( c = Extra_UtilGetopt( argc, argv, "1slhf" ) ) != EOF )
2293 {
2294 switch( c )
2295 {
2296 case '1':
2297 if( directive == -1 )
2298 directive = FULL_BIERE_ONE_LOOP_MODE;
2299 else
2300 {
2301 assert( directive == IGNORE_LIVENESS_KEEP_SAFETY_MODE || directive == IGNORE_SAFETY_KEEP_LIVENESS_MODE );
2302 if( directive == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
2303 directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE;
2304 else
2305 directive = IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE;
2306 }
2307 break;
2308 case 's':
2309 if( directive == -1 )
2310 directive = IGNORE_SAFETY_KEEP_LIVENESS_MODE;
2311 else
2312 {
2313 if( directive != FULL_BIERE_ONE_LOOP_MODE )
2314 goto usage;
2315 assert(directive == FULL_BIERE_ONE_LOOP_MODE);
2316 directive = IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE;
2317 }
2318 break;
2319 case 'l':
2320 if( directive == -1 )
2321 directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE;
2322 else
2323 {
2324 if( directive != FULL_BIERE_ONE_LOOP_MODE )
2325 goto usage;
2326 assert(directive == FULL_BIERE_ONE_LOOP_MODE);
2327 directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE;
2328 }
2329 break;
2330 case 'f':
2331 //assert( argc >= 3 );
2332 //vecLtlFormula = Vec_PtrAlloc( argc - 2 );
2333 //if( argc >= 3 )
2334 //{
2335 // for( t=3; t<=argc; t++ )
2336 // {
2337 // printf("argv[%d] = %s\n", t-1, argv[t-1]);
2338 // Vec_PtrPush( vecLtlFormula, argv[t-1] );
2339 // }
2340 //}
2341 //printf("argv[argc] = %s\n", argv[argc-1]);
2342 //ltfFormulaString = argv[2];
2343
2344 //LTL_FLAG = 1;
2345 printf("\nILLEGAL FLAG: aborting....\n");
2346 exit(0);
2347 break;
2348 case 'h':
2349 goto usage;
2350 default:
2351 goto usage;
2352 }
2353 }
2354 }
2355
2356 if ( pNtk == NULL )
2357 {
2358 fprintf( pErr, "Empty network.\n" );
2359 return 1;
2360 }
2361 if( !Abc_NtkIsStrash( pNtk ) )
2362 {
2363 printf("The input network was not strashed, strashing....\n");
2364 pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
2365 pNtkOld = pNtkTemp;
2366 pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
2367 vLive = populateLivenessVector( pNtk, pAig );
2368 vFair = populateFairnessVector( pNtk, pAig );
2369 vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
2370 vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
2371 }
2372 else
2373 {
2374 pAig = Abc_NtkToDar( pNtk, 0, 1 );
2375 pNtkOld = pNtk;
2376 vLive = populateLivenessVector( pNtk, pAig );
2377 vFair = populateFairnessVector( pNtk, pAig );
2378 vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
2379 vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
2380 }
2381
2382 if( pAbc->vLTLProperties_global != NULL )
2383 ltlBuffer = pAbc->vLTLProperties_global;
2384 else
2385 ltlBuffer = NULL;
2386
2387 switch( directive )
2388 {
2389 case FULL_BIERE_MODE:
2390 pAigNew = LivenessToSafetyTransformationWithLTL( FULL_BIERE_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety, &numOfLtlPropOutput, ltlBuffer );
2391 if( Aig_ManRegNum(pAigNew) != 0 )
2392 printf("A new circuit is produced with\n\t%d POs - one for safety and %d for liveness.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created if the original circuit is combinational\n\tnon-property POs are suppressed\n", numOfLtlPropOutput+1, numOfLtlPropOutput);
2393 break;
2394
2395 case FULL_BIERE_ONE_LOOP_MODE:
2396 pAigNew = LivenessToSafetyTransformationOneStepLoop( FULL_BIERE_ONE_LOOP_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
2397 if( Aig_ManRegNum(pAigNew) != 0 )
2398 printf("A new circuit is produced with\n\t2 POs - one for safety and one for liveness.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created\n\tnon-property POs are suppressed\n");
2399 break;
2400
2401 case IGNORE_LIVENESS_KEEP_SAFETY_MODE:
2402 pAigNew = LivenessToSafetyTransformationWithLTL( IGNORE_LIVENESS_KEEP_SAFETY_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety, &numOfLtlPropOutput, ltlBuffer );
2403 assert( numOfLtlPropOutput == 0 );
2404 if( Aig_ManRegNum(pAigNew) != 0 )
2405 printf("A new circuit is produced with\n\t1 PO - only for safety property; liveness properties are ignored, if any.\n\tno additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created\n\tnon-property POs are suppressed\n");
2406 break;
2407
2408 case IGNORE_SAFETY_KEEP_LIVENESS_MODE:
2409 pAigNew = LivenessToSafetyTransformationWithLTL( IGNORE_SAFETY_KEEP_LIVENESS_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety, &numOfLtlPropOutput, ltlBuffer );
2410 if( Aig_ManRegNum(pAigNew) != 0 )
2411 printf("A new circuit is produced with\n\t%d PO - only for liveness property; safety properties are ignored, if any.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created if the original circuit is combinational\n\tnon-property POs are suppressed\n", numOfLtlPropOutput);
2412 break;
2413
2414 case IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE:
2415 pAigNew = LivenessToSafetyTransformationOneStepLoop( IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
2416 if( Aig_ManRegNum(pAigNew) != 0 )
2417 printf("New circuit is produced ignoring safety outputs!\nOnly liveness and fairness outputs are considered.\nShadow registers are not created\n");
2418 break;
2419 }
2420
2421#if 0
2422 if( argc == 1 )
2423 {
2424 pAigNew = LivenessToSafetyTransformation( FULL_BIERE_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
2425 if( Aig_ManRegNum(pAigNew) != 0 )
2426 printf("New circuit is produced considering all safety, liveness and fairness outputs.\nBiere's logic is created\n");
2427 }
2428 else
2429 {
2430 Extra_UtilGetoptReset();
2431 c = Extra_UtilGetopt( argc, argv, "1lsh" );
2432 if( c == '1' )
2433 {
2434 if ( pNtk == NULL )
2435 {
2436 fprintf( pErr, "Empty network.\n" );
2437 return 1;
2438 }
2439 if( !Abc_NtkIsStrash( pNtk ) )
2440 {
2441 printf("The input network was not strashed, strashing....\n");
2442 pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
2443 pNtkOld = pNtkTemp;
2444 pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
2445 vLive = populateLivenessVector( pNtk, pAig );
2446 vFair = populateFairnessVector( pNtk, pAig );
2447 vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
2448 vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
2449 }
2450 else
2451 {
2452 pAig = Abc_NtkToDar( pNtk, 0, 1 );
2453 pNtkOld = pNtk;
2454 vLive = populateLivenessVector( pNtk, pAig );
2455 vFair = populateFairnessVector( pNtk, pAig );
2456 vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
2457 vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
2458 }
2459 pAigNew = LivenessToSafetyTransformationOneStepLoop( pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
2460 }
2461 else if( c == 'l' )
2462 {
2463 if ( pNtk == NULL )
2464 {
2465 fprintf( pErr, "Empty network.\n" );
2466 return 1;
2467 }
2468 if( !Abc_NtkIsStrash( pNtk ) )
2469 {
2470 printf("The input network was not strashed, strashing....\n");
2471 pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
2472 pNtkOld = pNtkTemp;
2473 pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
2474 vLive = populateLivenessVector( pNtk, pAig );
2475 vFair = populateFairnessVector( pNtk, pAig );
2476 vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
2477 vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
2478 }
2479 else
2480 {
2481 pAig = Abc_NtkToDar( pNtk, 0, 1 );
2482 pNtkOld = pNtk;
2483 vLive = populateLivenessVector( pNtk, pAig );
2484 vFair = populateFairnessVector( pNtk, pAig );
2485 vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
2486 vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
2487 }
2488 pAigNew = LivenessToSafetyTransformation( IGNORE_LIVENESS_KEEP_SAFETY_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
2489 if( Aig_ManRegNum(pAigNew) != 0 )
2490 printf("New circuit is produced ignoring liveness outputs!\nOnly safety outputs are kept.\nBiere's logic is not created\n");
2491 }
2492 else if( c == 's' )
2493 {
2494 if ( pNtk == NULL )
2495 {
2496 fprintf( pErr, "Empty network.\n" );
2497 return 1;
2498 }
2499
2500 if( !Abc_NtkIsStrash( pNtk ) )
2501 {
2502 printf("The input network was not strashed, strashing....\n");
2503 pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
2504 pNtkOld = pNtkTemp;
2505 pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
2506 vLive = populateLivenessVector( pNtk, pAig );
2507 vFair = populateFairnessVector( pNtk, pAig );
2508 vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
2509 vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
2510 }
2511 else
2512 {
2513 pAig = Abc_NtkToDar( pNtk, 0, 1 );
2514 pNtkOld = pNtk;
2515 vLive = populateLivenessVector( pNtk, pAig );
2516 vFair = populateFairnessVector( pNtk, pAig );
2517 vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
2518 vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
2519 }
2520 pAigNew = LivenessToSafetyTransformation( IGNORE_SAFETY_KEEP_LIVENESS_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
2521 if( Aig_ManRegNum(pAigNew) != 0 )
2522 printf("New circuit is produced ignoring safety outputs!\nOnly liveness and fairness outputs are considered.\nBiere's logic is created\n");
2523 }
2524 else if( c == 'h' )
2525 goto usage;
2526 else
2527 goto usage;
2528 }
2529#endif
2530
2531#if 0
2532 Aig_ManPrintStats( pAigNew );
2533 printf("\nDetail statistics*************************************\n");
2534 printf("Number of true primary inputs = %d\n", Saig_ManPiNum( pAigNew ));
2535 printf("Number of true primary outputs = %d\n", Saig_ManPoNum( pAigNew ));
2536 printf("Number of true latch outputs = %d\n", Saig_ManCiNum( pAigNew ) - Saig_ManPiNum( pAigNew ));
2537 printf("Number of true latch inputs = %d\n", Saig_ManCoNum( pAigNew ) - Saig_ManPoNum( pAigNew ));
2538 printf("Numer of registers = %d\n", Saig_ManRegNum( pAigNew ) );
2539 printf("\n*******************************************************\n");
2540#endif
2541
2542 pNtkNew = Abc_NtkFromAigPhase( pAigNew );
2543 pNtkNew->pName = Abc_UtilStrsav( pAigNew->pName );
2544
2545 if ( !Abc_NtkCheck( pNtkNew ) )
2546 fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" );
2547
2548 updateNewNetworkNameManager( pNtkNew, pAigNew, vecPiNames, vecLoNames );
2549 Abc_FrameSetCurrentNetwork( pAbc, pNtkNew );
2550
2551#if 0
2552#ifndef DUPLICATE_CKT_DEBUG
2553 Saig_ManForEachPi( pAigNew, pObj, i )
2554 assert( strcmp( (char *)Vec_PtrEntry(vecPiNames, i), retrieveTruePiName( pNtk, pAig, pAigNew, pObj ) ) == 0 );
2555 //printf("Name of %d-th Pi = %s, %s\n", i, retrieveTruePiName( pNtk, pAig, pAigNew, pObj ), (char *)Vec_PtrEntry(vecPiNames, i) );
2556
2557 Saig_ManForEachLo( pAigNew, pObj, i )
2558 assert( strcmp( (char *)Vec_PtrEntry(vecLoNames, i), retrieveLOName( pNtk, pAig, pAigNew, pObj, vLive, vFair ) ) == 0 );
2559#endif
2560#endif
2561
2562 return 0;
2563
2564usage:
2565 fprintf( stdout, "usage: l3s [-1lsh]\n" );
2566 fprintf( stdout, "\t performs Armin Biere's live-to-safe transformation\n" );
2567 fprintf( stdout, "\t-1 : no shadow logic, presume all loops are self loops\n");
2568 fprintf( stdout, "\t-l : ignore liveness and fairness outputs\n");
2569 fprintf( stdout, "\t-s : ignore safety assertions and assumptions\n");
2570 fprintf( stdout, "\t-h : print command usage\n");
2571 return 1;
2572}
2573
2574
2575ABC_NAMESPACE_IMPL_END
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_NtkForEachLatch
#define Abc_NtkForEachLatch(pNtk, pObj, i)
Definition abc.h:500
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_ObjAssignName
ABC_DLL char * Abc_ObjAssignName(Abc_Obj_t *pObj, char *pName, char *pSuffix)
Definition abcNames.c:69
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
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
p
Cube * p
Definition exorList.c:222
Extra_UtilGetopt
int Extra_UtilGetopt(int argc, char *argv[], const char *optstring)
Definition extraUtilUtil.c:98
Extra_UtilGetoptReset
ABC_DLL void Extra_UtilGetoptReset()
Definition extraUtilUtil.c:80
buildLogicFromLTLNode
Aig_Obj_t * buildLogicFromLTLNode(Aig_Man_t *pAig, ltlNode *pLtlNode)
Definition ltl_parser.c:601
printVecPtrOfString
void printVecPtrOfString(Vec_Ptr_t *vec)
Definition liveness.c:92
vecLoNames
Vec_Ptr_t * vecLoNames
Definition liveness.c:219
ltlNode
struct ltlNode_t ltlNode
Definition liveness.c:48
checkAllBoolHaveAIGPointer
int checkAllBoolHaveAIGPointer(ltlNode *topASTNode)
Definition ltl_parser.c:795
vecLos
Vec_Ptr_t * vecLos
Definition liveness.c:219
IGNORE_LIVENESS_KEEP_SAFETY_MODE
#define IGNORE_LIVENESS_KEEP_SAFETY_MODE
Definition liveness.c:35
vecPiNames
Vec_Ptr_t * vecPiNames
Definition liveness.c:218
Abc_CommandAbcLivenessToSafety
int Abc_CommandAbcLivenessToSafety(Abc_Frame_t *pAbc, int argc, char **argv)
Definition liveness.c:1254
FULL_BIERE_ONE_LOOP_MODE
#define FULL_BIERE_ONE_LOOP_MODE
Definition liveness.c:38
LivenessToSafetyTransformation
Aig_Man_t * LivenessToSafetyTransformation(int mode, Abc_Ntk_t *pNtk, Aig_Man_t *p, Vec_Ptr_t *vLive, Vec_Ptr_t *vFair, Vec_Ptr_t *vAssertSafety, Vec_Ptr_t *vAssumeSafety)
Definition liveness.c:244
populateFairnessVector
Vec_Ptr_t * populateFairnessVector(Abc_Ntk_t *pNtk, Aig_Man_t *pAig)
Definition liveness.c:1161
traverseAbstractSyntaxTree
void traverseAbstractSyntaxTree(ltlNode *node)
Definition ltl_parser.c:377
Aig_ManCoCleanupBiere
int Aig_ManCoCleanupBiere(Aig_Man_t *p)
Definition liveness.c:234
populateSafetyAssertionVector
Vec_Ptr_t * populateSafetyAssertionVector(Abc_Ntk_t *pNtk, Aig_Man_t *pAig)
Definition liveness.c:1179
vecPis
Vec_Ptr_t * vecPis
Definition liveness.c:218
Abc_CommandAbcLivenessToSafetyAbstraction
int Abc_CommandAbcLivenessToSafetyAbstraction(Abc_Frame_t *pAbc, int argc, char **argv)
Definition liveness.c:1599
retrieveTruePiName
char * retrieveTruePiName(Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, Aig_Obj_t *pObjPivot)
Definition liveness.c:115
LivenessToSafetyTransformationWithLTL
Aig_Man_t * LivenessToSafetyTransformationWithLTL(int mode, Abc_Ntk_t *pNtk, Aig_Man_t *p, Vec_Ptr_t *vLive, Vec_Ptr_t *vFair, Vec_Ptr_t *vAssertSafety, Vec_Ptr_t *vAssumeSafety, int *numLtlProcessed, Vec_Ptr_t *ltlBuffer)
Definition liveness.c:1798
traverseAbstractSyntaxTree_postFix
void traverseAbstractSyntaxTree_postFix(ltlNode *node)
Definition ltl_parser.c:436
isWellFormed
int isWellFormed(ltlNode *topNode)
Definition ltl_parser.c:661
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
Abc_NtkToDar
Aig_Man_t * Abc_NtkToDar(Abc_Ntk_t *pNtk, int fExors, int fRegisters)
DECLARATIONS ///.
Definition abcDar.c:237
retriveAIGPointerFromLTLNode
Aig_Obj_t * retriveAIGPointerFromLTLNode(ltlNode *astNode)
Definition ltl_parser.c:833
Abc_CommandAbcLivenessToSafetyWithLTL
int Abc_CommandAbcLivenessToSafetyWithLTL(Abc_Frame_t *pAbc, int argc, char **argv)
Definition liveness.c:2268
populateAigPointerUnitGF
void populateAigPointerUnitGF(Aig_Man_t *pAigNew, ltlNode *topASTNode, Vec_Ptr_t *vSignal, Vec_Vec_t *vAigGFMap)
Definition ltl_parser.c:505
LivenessToSafetyTransformationOneStepLoop
Aig_Man_t * LivenessToSafetyTransformationOneStepLoop(int mode, Abc_Ntk_t *pNtk, Aig_Man_t *p, Vec_Ptr_t *vLive, Vec_Ptr_t *vFair, Vec_Ptr_t *vAssertSafety, Vec_Ptr_t *vAssumeSafety)
Definition liveness.c:843
checkSignalNameExistence
int checkSignalNameExistence(Abc_Ntk_t *pNtk, ltlNode *topASTNode)
Definition ltl_parser.c:699
prepareFlopVector
Vec_Int_t * prepareFlopVector(Aig_Man_t *pAig, int vectorLength)
Definition liveness.c:1569
IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE
#define IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE
Definition liveness.c:37
updateNewNetworkNameManager
void updateNewNetworkNameManager(Abc_Ntk_t *pNtk, Aig_Man_t *pAig, Vec_Ptr_t *vPiNames, Vec_Ptr_t *vLoNames)
Definition liveness.c:1215
LivenessToSafetyTransformationAbs
Aig_Man_t * LivenessToSafetyTransformationAbs(int mode, Abc_Ntk_t *pNtk, Aig_Man_t *p, Vec_Int_t *vFlops, Vec_Ptr_t *vLive, Vec_Ptr_t *vFair, Vec_Ptr_t *vAssertSafety, Vec_Ptr_t *vAssumeSafety)
Definition liveness.c:542
FULL_BIERE_MODE
#define FULL_BIERE_MODE
Definition liveness.c:34
readLtlFormula
ltlNode * readLtlFormula(char *formula)
Definition ltl_parser.c:137
Abc_NtkFromAigPhase
Abc_Ntk_t * Abc_NtkFromAigPhase(Aig_Man_t *pMan)
DECLARATIONS ///.
Definition abcDar.c:595
IGNORE_SAFETY_KEEP_LIVENESS_MODE
#define IGNORE_SAFETY_KEEP_LIVENESS_MODE
Definition liveness.c:36
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
parseFormulaCreateAST
ltlNode * parseFormulaCreateAST(char *inputFormula)
Definition ltl_parser.c:366
populateLivenessVector
Vec_Ptr_t * populateLivenessVector(Abc_Ntk_t *pNtk, Aig_Man_t *pAig)
Definition liveness.c:1143
populateBoolWithAigNodePtr
void populateBoolWithAigNodePtr(Abc_Ntk_t *pNtk, Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, ltlNode *topASTNode)
Definition ltl_parser.c:742
setAIGNodePtrOfGloballyNode
void setAIGNodePtrOfGloballyNode(ltlNode *astNode, Aig_Obj_t *pObjLo)
Definition ltl_parser.c:828
populateSafetyAssumptionVector
Vec_Ptr_t * populateSafetyAssumptionVector(Abc_Ntk_t *pNtk, Aig_Man_t *pAig)
Definition liveness.c:1197
usage
usage()
Definition main.c:626
Nm_ManFindNameById
char * Nm_ManFindNameById(Nm_Man_t *p, int ObjId)
Definition nmApi.c:199
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_::pName
char * pName
Definition abc.h:158
Abc_Ntk_t_::pManName
Nm_Man_t * pManName
Definition abc.h:160
Aig_Obj_t_::pData
void * pData
Definition aig.h:87
ltlNode_t
Definition ltl_parser.c:38
ltlNode_t::pObj
Aig_Obj_t * pObj
Definition ltl_parser.c:41
mode
Definition mode.h:11
assert
#define assert(ex)
Definition util_old.h:213
strlen
int strlen()
strcmp
int strcmp()
sprintf
char * sprintf()
strstr
char * strstr()
exit
VOID_HACK exit()
malloc
char * malloc()
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
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
Vec_VecForEachEntryLevel
#define Vec_VecForEachEntryLevel(Type, vGlob, pEntry, i, Level)
Definition vecVec.h:90
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition vecVec.h:42