abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
liveness.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [liveness.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Liveness property checking.]
8 
9  Synopsis [Main implementation module.]
10 
11  Author [Sayak Ray]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - January 1, 2009.]
16 
17  Revision [$Id: liveness.c,v 1.00 2009/01/01 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include <stdio.h>
22 #include "base/main/main.h"
23 #include "aig/aig/aig.h"
24 #include "aig/saig/saig.h"
25 #include <string.h>
26 #include "base/main/mainInt.h"
27 
28 ABC_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 
41 extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
42 extern 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 //******************************************
48 typedef struct ltlNode_t ltlNode;
49 extern ltlNode *readLtlFormula( char *formula );
50 extern void traverseAbstractSyntaxTree( ltlNode *node );
51 extern ltlNode *parseFormulaCreateAST( char *inputFormula );
52 extern int isWellFormed( ltlNode *topNode );
53 extern int checkSignalNameExistence( Abc_Ntk_t *pNtk, ltlNode *topASTNode );
54 extern void populateBoolWithAigNodePtr( Abc_Ntk_t *pNtk, Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, ltlNode *topASTNode );
55 extern int checkAllBoolHaveAIGPointer( ltlNode *topASTNode );
56 extern void populateAigPointerUnitGF( Aig_Man_t *pAigNew, ltlNode *topASTNode, Vec_Ptr_t *vSignal, Vec_Vec_t *vAigGFMap );
57 extern void setAIGNodePtrOfGloballyNode( ltlNode *astNode, Aig_Obj_t *pObjLo );
58 extern Aig_Obj_t *buildLogicFromLTLNode( Aig_Man_t *pAig, ltlNode *pLtlNode );
59 extern Aig_Obj_t *retriveAIGPointerFromLTLNode( ltlNode *astNode );
60 extern void traverseAbstractSyntaxTree_postFix( ltlNode *node );
61 //**********************************
62 //external function declaration ends
63 //**********************************
64 
65 
66 /*******************************************************************
67 LAYOUT 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 
74 LAYOUT 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 
84 static 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 
92 void 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 
102 int 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 
115 char * 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 
137 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 )
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 
218 Vec_Ptr_t *vecPis, *vecPiNames;
219 Vec_Ptr_t *vecLos, *vecLoNames;
220 
221 
222 int 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 
234 int 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 
244 Aig_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 
542 Aig_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 
843 Aig_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 
1143 Vec_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 
1161 Vec_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 
1179 Vec_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 
1197 Vec_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 
1215 void 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 
1254 int 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 
1559 usage:
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 
1569 Vec_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 
1599 int 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 
1788 usage:
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 
1798 Aig_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 
2268 int 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 
2564 usage:
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 
2575 ABC_NAMESPACE_IMPL_END
Aig_ObjCreateCo
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE
#define IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE
Definition: liveness.c:37
malloc
char * malloc()
exit
VOID_HACK exit()
Abc_NtkIsStrash
static int Abc_NtkIsStrash(Abc_Ntk_t *pNtk)
Definition: abc.h:251
vecLoNames
Vec_Ptr_t * vecLoNames
Definition: liveness.c:219
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Aig_ManCheck
ABC_DLL int Aig_ManCheck(Aig_Man_t *p)
FUNCTION DECLARATIONS ///.
Definition: aigCheck.c:45
nodeName_starts_with
static int nodeName_starts_with(Abc_Obj_t *pNode, const char *prefix)
Definition: liveness.c:84
populateSafetyAssertionVector
Vec_Ptr_t * populateSafetyAssertionVector(Abc_Ntk_t *pNtk, Aig_Man_t *pAig)
Definition: liveness.c:1179
Vec_VecAlloc
static Vec_Vec_t * Vec_VecAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecVec.h:145
Aig_ObjType
static Aig_Type_t Aig_ObjType(Aig_Obj_t *pObj)
Definition: aig.h:272
Abc_Ntk_t_::pManName
Nm_Man_t * pManName
Definition: abc.h:160
checkSignalNameExistence
int checkSignalNameExistence(Abc_Ntk_t *pNtk, ltlNode *topASTNode)
Definition: ltl_parser.c:699
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
Saig_ManPoNum
static int Saig_ManPoNum(Aig_Man_t *p)
Definition: saig.h:74
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
Saig_ObjIsLo
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:84
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
printVecPtrOfString
void printVecPtrOfString(Vec_Ptr_t *vec)
Definition: liveness.c:92
Aig_ObjChild0
static Aig_Obj_t * Aig_ObjChild0(Aig_Obj_t *pObj)
Definition: aig.h:310
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
retriveAIGPointerFromLTLNode
Aig_Obj_t * retriveAIGPointerFromLTLNode(ltlNode *astNode)
Definition: ltl_parser.c:833
AIG_OBJ_CO
Definition: aig.h:61
Saig_ObjLoToLi
static Aig_Obj_t * Saig_ObjLoToLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:86
Abc_NtkToDar
Aig_Man_t * Abc_NtkToDar(Abc_Ntk_t *pNtk, int fExors, int fRegisters)
DECLARATIONS ///.
Definition: abcDar.c:233
Abc_Ntk_t_
Definition: abc.h:153
Abc_FrameSetCurrentNetwork
ABC_DLL void Abc_FrameSetCurrentNetwork(Abc_Frame_t *p, Abc_Ntk_t *pNet)
Definition: mainFrame.c:396
Aig_Obj_t_::pData
void * pData
Definition: aig.h:87
Aig_Exor
Aig_Obj_t * Aig_Exor(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:220
Abc_NtkStrash
ABC_DLL Abc_Ntk_t * Abc_NtkStrash(Abc_Ntk_t *pNtk, int fAllNodes, int fCleanup, int fRecord)
Definition: abcStrash.c:265
vecPiNames
Vec_Ptr_t * vecPiNames
Definition: liveness.c:218
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
populateSafetyAssumptionVector
Vec_Ptr_t * populateSafetyAssumptionVector(Abc_Ntk_t *pNtk, Aig_Man_t *pAig)
Definition: liveness.c:1197
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_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Aig_Regular
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
Aig_ObjCreateCi
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
IGNORE_SAFETY_KEEP_LIVENESS_MODE
#define IGNORE_SAFETY_KEEP_LIVENESS_MODE
Definition: liveness.c:36
Abc_NtkCiNum
static int Abc_NtkCiNum(Abc_Ntk_t *pNtk)
Definition: abc.h:287
FULL_BIERE_MODE
#define FULL_BIERE_MODE
Definition: liveness.c:34
Abc_CommandAbcLivenessToSafetyWithLTL
int Abc_CommandAbcLivenessToSafetyWithLTL(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: liveness.c:2268
populateBoolWithAigNodePtr
void populateBoolWithAigNodePtr(Abc_Ntk_t *pNtk, Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, ltlNode *topASTNode)
Definition: ltl_parser.c:742
Abc_NtkCi
static Abc_Obj_t * Abc_NtkCi(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:317
Aig_Not
static Aig_Obj_t * Aig_Not(Aig_Obj_t *p)
Definition: aig.h:247
populateFairnessVector
Vec_Ptr_t * populateFairnessVector(Abc_Ntk_t *pNtk, Aig_Man_t *pAig)
Definition: liveness.c:1161
Abc_NtkCheck
ABC_DLL int Abc_NtkCheck(Abc_Ntk_t *pNtk)
FUNCTION DEFINITIONS ///.
Definition: abcCheck.c:61
Abc_ObjAssignName
ABC_DLL char * Abc_ObjAssignName(Abc_Obj_t *pObj, char *pName, char *pSuffix)
Definition: abcNames.c:68
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_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
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Vec_VecFree
static void Vec_VecFree(Vec_Vec_t *p)
Definition: vecVec.h:347
Abc_ObjFanin0
static Abc_Obj_t * Abc_ObjFanin0(Abc_Obj_t *pObj)
Definition: abc.h:373
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
ltlNode_t
Definition: ltl_parser.c:37
Vec_PtrFind
static int Vec_PtrFind(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:694
Aig_And
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
strcmp
int strcmp()
checkAllBoolHaveAIGPointer
int checkAllBoolHaveAIGPointer(ltlNode *topASTNode)
Definition: ltl_parser.c:795
Abc_Obj_t_
Definition: abc.h:128
isWellFormed
int isWellFormed(ltlNode *topNode)
Definition: ltl_parser.c:661
Nm_ManStoreIdName
char * Nm_ManStoreIdName(Nm_Man_t *p, int ObjId, int Type, char *pName, char *pSuffix)
Definition: nmApi.c:112
Aig_ManCoNum
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
Vec_VecForEachEntryLevel
#define Vec_VecForEachEntryLevel(Type, vGlob, pEntry, i, Level)
Definition: vecVec.h:90
Abc_Frame_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Frame_t_ Abc_Frame_t
INCLUDES ///.
Definition: base/main/main.h:39
Extra_UtilGetoptReset
ABC_DLL void Extra_UtilGetoptReset()
Definition: extraUtilUtil.c:80
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
Aig_ManLo
static Aig_Obj_t * Aig_ManLo(Aig_Man_t *p, int i)
Definition: aig.h:268
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Aig_ObjPatchFanin0
void Aig_ObjPatchFanin0(Aig_Man_t *p, Aig_Obj_t *pObj, Aig_Obj_t *pFaninNew)
Definition: aigObj.c:282
strstr
char * strstr()
Aig_ManSetRegNum
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition: aigMan.c:438
Aig_ManCi
static Aig_Obj_t * Aig_ManCi(Aig_Man_t *p, int i)
Definition: aig.h:266
populateAigPointerUnitGF
void populateAigPointerUnitGF(Aig_Man_t *pAigNew, ltlNode *topASTNode, Vec_Ptr_t *vSignal, Vec_Vec_t *vAigGFMap)
Definition: ltl_parser.c:505
Aig_ManCiNum
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
prepareFlopVector
Vec_Int_t * prepareFlopVector(Aig_Man_t *pAig, int vectorLength)
Definition: liveness.c:1569
Nm_ManFindNameById
char * Nm_ManFindNameById(Nm_Man_t *p, int ObjId)
Definition: nmApi.c:199
updateNewNetworkNameManager
void updateNewNetworkNameManager(Abc_Ntk_t *pNtk, Aig_Man_t *pAig, Vec_Ptr_t *vPiNames, Vec_Ptr_t *vLoNames)
Definition: liveness.c:1215
Aig_ObjChild1Copy
static Aig_Obj_t * Aig_ObjChild1Copy(Aig_Obj_t *pObj)
Definition: aig.h:313
Aig_Or
Aig_Obj_t * Aig_Or(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:259
Aig_ManCoCleanupBiere
int Aig_ManCoCleanupBiere(Aig_Man_t *p)
Definition: liveness.c:234
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
sprintf
char * sprintf()
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
buildLogicFromLTLNode
Aig_Obj_t * buildLogicFromLTLNode(Aig_Man_t *pAig, ltlNode *pLtlNode)
Definition: ltl_parser.c:601
Aig_ObjChild0Copy
static Aig_Obj_t * Aig_ObjChild0Copy(Aig_Obj_t *pObj)
Definition: aig.h:312
Abc_NtkForEachLatch
#define Abc_NtkForEachLatch(pNtk, pObj, i)
Definition: abc.h:497
Saig_ManCiNum
static int Saig_ManCiNum(Aig_Man_t *p)
Definition: saig.h:75
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Saig_ManRegNum
static int Saig_ManRegNum(Aig_Man_t *p)
Definition: saig.h:77
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Aig_ManCo
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
Abc_FrameReadNtk
ABC_DLL Abc_Ntk_t * Abc_FrameReadNtk(Abc_Frame_t *p)
Definition: mainFrame.c:282
Abc_CommandAbcLivenessToSafetyAbstraction
int Abc_CommandAbcLivenessToSafetyAbstraction(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: liveness.c:1599
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
IGNORE_LIVENESS_KEEP_SAFETY_MODE
#define IGNORE_LIVENESS_KEEP_SAFETY_MODE
Definition: liveness.c:35
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
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
Abc_NtkPo
static Abc_Obj_t * Abc_NtkPo(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:316
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Saig_ManPiNum
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
Abc_Obj_t_::Id
int Id
Definition: abc.h:132
Abc_NtkPiNum
static int Abc_NtkPiNum(Abc_Ntk_t *pNtk)
Definition: abc.h:285
Abc_ObjName
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
Definition: abcNames.c:48
Extra_UtilGetopt
int Extra_UtilGetopt(int argc, char *argv[], const char *optstring)
Definition: extraUtilUtil.c:98
readLtlFormula
ltlNode * readLtlFormula(char *formula)
Definition: ltl_parser.c:137
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
Nm_ManCreate
Nm_Man_t * Nm_ManCreate(int nSize)
MACRO DEFINITIONS ///.
Definition: nmApi.c:45
vecPis
Vec_Ptr_t * vecPis
Definition: liveness.c:218
traverseAbstractSyntaxTree_postFix
void traverseAbstractSyntaxTree_postFix(ltlNode *node)
Definition: ltl_parser.c:436
ltlNode_t::pObj
Aig_Obj_t * pObj
Definition: ltl_parser.c:41
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
Aig_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
populateLivenessVector
Vec_Ptr_t * populateLivenessVector(Abc_Ntk_t *pNtk, Aig_Man_t *pAig)
Definition: liveness.c:1143
AIG_OBJ_CI
Definition: aig.h:60
Abc_FrameReadErr
ABC_DLL FILE * Abc_FrameReadErr(Abc_Frame_t *p)
Definition: mainFrame.c:330
assert
#define assert(ex)
Definition: util_old.h:213
strlen
int strlen()
Saig_ManCoNum
static int Saig_ManCoNum(Aig_Man_t *p)
Definition: saig.h:76
parseFormulaCreateAST
ltlNode * parseFormulaCreateAST(char *inputFormula)
Definition: ltl_parser.c:366
Aig_ManCiCleanupBiere
int Aig_ManCiCleanupBiere(Aig_Man_t *p)
Definition: liveness.c:222
Abc_NtkPi
static Abc_Obj_t * Abc_NtkPi(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:315
vecLos
Vec_Ptr_t * vecLos
Definition: liveness.c:219
Abc_FrameReadOut
ABC_DLL FILE * Abc_FrameReadOut(Abc_Frame_t *p)
Definition: mainFrame.c:314
Abc_NtkForEachPo
#define Abc_NtkForEachPo(pNtk, pPo, i)
Definition: abc.h:517
Aig_NotCond
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Abc_NtkFromAigPhase
Abc_Ntk_t * Abc_NtkFromAigPhase(Aig_Man_t *pMan)
Definition: abcDar.c:590
setAIGNodePtrOfGloballyNode
void setAIGNodePtrOfGloballyNode(ltlNode *astNode, Aig_Obj_t *pObjLo)
Definition: ltl_parser.c:828
getPoIndex
int getPoIndex(Aig_Man_t *pAig, Aig_Obj_t *pPivot)
Definition: liveness.c:102
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Saig_ObjIsPi
static int Saig_ObjIsPi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:82
traverseAbstractSyntaxTree
void traverseAbstractSyntaxTree(ltlNode *node)
Definition: ltl_parser.c:377
Aig_ManCleanup
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
Abc_Ntk_t_::pName
char * pName
Definition: abc.h:158
Aig_ObjCioId
static int Aig_ObjCioId(Aig_Obj_t *pObj)
Definition: aig.h:285
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91
retrieveTruePiName
char * retrieveTruePiName(Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, Aig_Obj_t *pObjPivot)
Definition: liveness.c:115