abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
arenaViolation.c File Reference
#include <stdio.h>
#include "base/main/main.h"
#include "aig/aig/aig.h"
#include "aig/saig/saig.h"
#include <string.h>
#include "base/main/mainInt.h"
#include "proof/pdr/pdr.h"

Go to the source code of this file.

Macros

#define BARRIER_MONOTONE_TEST
 

Functions

ABC_NAMESPACE_IMPL_START
Vec_Ptr_t
createArenaLO (Aig_Man_t *pAigNew, Vec_Ptr_t *vBarriers)
 
Vec_Ptr_tcreateArenaLi (Aig_Man_t *pAigNew, Vec_Ptr_t *vBarriers, Vec_Ptr_t *vArenaSignal)
 
Vec_Ptr_tcreateMonotoneBarrierLO (Aig_Man_t *pAigNew, Vec_Ptr_t *vBarriers)
 
Aig_Obj_tdriverToPoNew (Aig_Man_t *pAig, Aig_Obj_t *pObjPo)
 
Vec_Ptr_tcollectBarrierDisjunctions (Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, Vec_Ptr_t *vBarriers)
 
Aig_Obj_tAig_Xor (Aig_Man_t *pAig, Aig_Obj_t *pObj1, Aig_Obj_t *pObj2)
 
Aig_Obj_tcreateArenaViolation (Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, Aig_Obj_t *pWindowBegins, Aig_Obj_t *pWithinWindow, Vec_Ptr_t *vMasterBarriers, Vec_Ptr_t *vBarrierLo, Vec_Ptr_t *vBarrierLiDriver, Vec_Ptr_t *vMonotoneDisjunctionNodes)
 
Aig_Obj_tcreateConstrained0LiveConeWithDSC (Aig_Man_t *pNewAig, Vec_Ptr_t *signalList)
 
Vec_Ptr_tcollectCSSignalsWithDSC (Abc_Ntk_t *pNtk, Aig_Man_t *pAig)
 
int collectWindowBeginSignalWithDSC (Abc_Ntk_t *pNtk, Aig_Man_t *pAig)
 
int collectWithinWindowSignalWithDSC (Abc_Ntk_t *pNtk, Aig_Man_t *pAig)
 
int collectPendingSignalWithDSC (Abc_Ntk_t *pNtk, Aig_Man_t *pAig)
 
Aig_Obj_tcreateAndGateForMonotonicityVerification (Aig_Man_t *pNewAig, Vec_Ptr_t *vDisjunctionSignals, Vec_Ptr_t *vDisjunctionLo, Aig_Obj_t *pendingLo, Aig_Obj_t *pendingSignal)
 
Aig_Man_tcreateNewAigWith0LivePoWithDSC (Aig_Man_t *pAig, Vec_Ptr_t *signalList, int *index0Live, int windowBeginIndex, int withinWindowIndex, int pendingSignalIndex, Vec_Ptr_t *vBarriers)
 
Aig_Man_tgenerateWorkingAigWithDSC (Aig_Man_t *pAig, Abc_Ntk_t *pNtk, int *pIndex0Live, Vec_Ptr_t *vMasterBarriers)
 

Macro Definition Documentation

#define BARRIER_MONOTONE_TEST

CFile****************************************************************

FileName [arenaViolation.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Liveness property checking.]

Synopsis [module for addition of arena violator detector induced by stabilizing constraints]

Author [Sayak Ray]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - October 31, 2012.]

Definition at line 29 of file arenaViolation.c.

Function Documentation

Aig_Obj_t* Aig_Xor ( Aig_Man_t pAig,
Aig_Obj_t pObj1,
Aig_Obj_t pObj2 
)

Definition at line 160 of file arenaViolation.c.

161 {
162  return Aig_Or( pAig, Aig_And( pAig, pObj1, Aig_Not(pObj2) ), Aig_And( pAig, Aig_Not(pObj1), pObj2 ) );
163 }
static Aig_Obj_t * Aig_Not(Aig_Obj_t *p)
Definition: aig.h:247
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
Aig_Obj_t * Aig_Or(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:259
Vec_Ptr_t* collectBarrierDisjunctions ( Aig_Man_t pAigOld,
Aig_Man_t pAigNew,
Vec_Ptr_t vBarriers 
)

Definition at line 124 of file arenaViolation.c.

125 {
126  int barrierCount, i, j, jElem;
127  Vec_Int_t *vIthBarrier;
128  Aig_Obj_t *pObjBarrier, *pObjCurr, *pObjTargetPoOld;
129  Vec_Ptr_t *vNewBarrierSignals;
130 
131  if( vBarriers == NULL )
132  return NULL;
133  barrierCount = Vec_PtrSize( vBarriers );
134  if( barrierCount <= 0 )
135  return NULL;
136 
137  vNewBarrierSignals = Vec_PtrAlloc( barrierCount );
138 
139  for( i=0; i<barrierCount; i++ )
140  {
141  vIthBarrier = (Vec_Int_t *)Vec_PtrEntry( vBarriers, i );
142  assert( Vec_IntSize( vIthBarrier ) >= 1 );
143  pObjBarrier = Aig_Not(Aig_ManConst1(pAigNew));
144  Vec_IntForEachEntry( vIthBarrier, jElem, j )
145  {
146  pObjTargetPoOld = Aig_ManCo( pAigOld, jElem );
147  //Aig_ObjPrint( pAigOld, pObjTargetPoOld );
148  //printf("\n");
149  pObjCurr = driverToPoNew( pAigOld, pObjTargetPoOld );
150  pObjBarrier = Aig_Or( pAigNew, pObjCurr, pObjBarrier );
151  }
152  assert( pObjBarrier );
153  Vec_PtrPush(vNewBarrierSignals, pObjBarrier);
154  }
155  assert( Vec_PtrSize( vNewBarrierSignals ) == barrierCount );
156 
157  return vNewBarrierSignals;
158 }
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
static Aig_Obj_t * Aig_Not(Aig_Obj_t *p)
Definition: aig.h:247
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Aig_Obj_t * driverToPoNew(Aig_Man_t *pAig, Aig_Obj_t *pObjPo)
Aig_Obj_t * Aig_Or(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:259
Definition: aig.h:69
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
#define assert(ex)
Definition: util_old.h:213
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Vec_Ptr_t* collectCSSignalsWithDSC ( Abc_Ntk_t pNtk,
Aig_Man_t pAig 
)

Definition at line 235 of file arenaViolation.c.

236 {
237  int i;
238  Aig_Obj_t *pObj, *pConsequent = NULL;
239  Vec_Ptr_t *vNodeArray;
240 
241  vNodeArray = Vec_PtrAlloc(1);
242 
243  Saig_ManForEachPo( pAig, pObj, i )
244  {
245  if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "csLiveConst_" ) != NULL )
246  Vec_PtrPush( vNodeArray, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj)) );
247  else if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "csLiveTarget_" ) != NULL )
248  pConsequent = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj));
249  }
250  assert( pConsequent );
251  Vec_PtrPush( vNodeArray, pConsequent );
252  return vNodeArray;
253 }
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
char * strstr()
Definition: aig.h:69
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
static Abc_Obj_t * Abc_NtkPo(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:316
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
Definition: abcNames.c:48
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
#define assert(ex)
Definition: util_old.h:213
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
int collectPendingSignalWithDSC ( Abc_Ntk_t pNtk,
Aig_Man_t pAig 
)

Definition at line 285 of file arenaViolation.c.

286 {
287  int i;
288  Aig_Obj_t *pObj;
289 
290  Saig_ManForEachPo( pAig, pObj, i )
291  {
292  if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "pendingSignal" ) != NULL )
293  return i;
294  }
295 
296  return -1;
297 }
char * strstr()
Definition: aig.h:69
static Abc_Obj_t * Abc_NtkPo(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:316
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
Definition: abcNames.c:48
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
int collectWindowBeginSignalWithDSC ( Abc_Ntk_t pNtk,
Aig_Man_t pAig 
)

Definition at line 255 of file arenaViolation.c.

256 {
257  int i;
258  Aig_Obj_t *pObj;
259 
260  Saig_ManForEachPo( pAig, pObj, i )
261  {
262  if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "windowBegins_" ) != NULL )
263  {
264  return i;
265  }
266  }
267 
268  return -1;
269 }
char * strstr()
Definition: aig.h:69
static Abc_Obj_t * Abc_NtkPo(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:316
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
Definition: abcNames.c:48
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
int collectWithinWindowSignalWithDSC ( Abc_Ntk_t pNtk,
Aig_Man_t pAig 
)

Definition at line 271 of file arenaViolation.c.

272 {
273  int i;
274  Aig_Obj_t *pObj;
275 
276  Saig_ManForEachPo( pAig, pObj, i )
277  {
278  if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "withinWindow_" ) != NULL )
279  return i;
280  }
281 
282  return -1;
283 }
char * strstr()
Definition: aig.h:69
static Abc_Obj_t * Abc_NtkPo(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:316
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
Definition: abcNames.c:48
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
Aig_Obj_t* createAndGateForMonotonicityVerification ( Aig_Man_t pNewAig,
Vec_Ptr_t vDisjunctionSignals,
Vec_Ptr_t vDisjunctionLo,
Aig_Obj_t pendingLo,
Aig_Obj_t pendingSignal 
)

Definition at line 299 of file arenaViolation.c.

306 {
307  Aig_Obj_t *pObjBigAnd, *pObj, *pObjLo, *pObjImply;
308  Aig_Obj_t *pObjPendingAndPendingLo;
309  int i;
310 
311  pObjBigAnd = Aig_ManConst1( pNewAig );
312  pObjPendingAndPendingLo = Aig_And( pNewAig, pendingLo, pendingSignal );
313  Vec_PtrForEachEntry( Aig_Obj_t *, vDisjunctionSignals, pObj, i )
314  {
315  pObjLo = (Aig_Obj_t *)Vec_PtrEntry( vDisjunctionLo, i );
316  pObjImply = Aig_Or( pNewAig, Aig_Not(Aig_And( pNewAig, pObjPendingAndPendingLo, pObjLo)),
317  pObj );
318  pObjBigAnd = Aig_And( pNewAig, pObjBigAnd, pObjImply );
319  }
320  return pObjBigAnd;
321 }
static Aig_Obj_t * Aig_Not(Aig_Obj_t *p)
Definition: aig.h:247
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
Aig_Obj_t * Aig_Or(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:259
Definition: aig.h:69
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Vec_Ptr_t* createArenaLi ( Aig_Man_t pAigNew,
Vec_Ptr_t vBarriers,
Vec_Ptr_t vArenaSignal 
)

Definition at line 57 of file arenaViolation.c.

58 {
59  Vec_Ptr_t *vArenaLi;
60  int barrierCount;
61  int i;
62  Aig_Obj_t *pObj, *pObjDriver;
63 
64  if( vBarriers == NULL )
65  return NULL;
66 
67  barrierCount = Vec_PtrSize(vBarriers);
68  if( barrierCount <= 0 )
69  return NULL;
70 
71  vArenaLi = Vec_PtrAlloc(barrierCount);
72  for( i=0; i<barrierCount; i++ )
73  {
74  pObjDriver = (Aig_Obj_t *)Vec_PtrEntry( vArenaSignal, i );
75  pObj = Aig_ObjCreateCo( pAigNew, pObjDriver );
76  Vec_PtrPush( vArenaLi, pObj );
77  }
78 
79  return vArenaLi;
80 }
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Definition: aig.h:69
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
ABC_NAMESPACE_IMPL_START Vec_Ptr_t* createArenaLO ( Aig_Man_t pAigNew,
Vec_Ptr_t vBarriers 
)

Definition at line 33 of file arenaViolation.c.

34 {
35  Vec_Ptr_t *vArenaLO;
36  int barrierCount;
37  Aig_Obj_t *pObj;
38  int i;
39 
40  if( vBarriers == NULL )
41  return NULL;
42 
43  barrierCount = Vec_PtrSize(vBarriers);
44  if( barrierCount <= 0 )
45  return NULL;
46 
47  vArenaLO = Vec_PtrAlloc(barrierCount);
48  for( i=0; i<barrierCount; i++ )
49  {
50  pObj = Aig_ObjCreateCi( pAigNew );
51  Vec_PtrPush( vArenaLO, pObj );
52  }
53 
54  return vArenaLO;
55 }
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Definition: aig.h:69
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Aig_Obj_t* createArenaViolation ( Aig_Man_t pAigOld,
Aig_Man_t pAigNew,
Aig_Obj_t pWindowBegins,
Aig_Obj_t pWithinWindow,
Vec_Ptr_t vMasterBarriers,
Vec_Ptr_t vBarrierLo,
Vec_Ptr_t vBarrierLiDriver,
Vec_Ptr_t vMonotoneDisjunctionNodes 
)

Definition at line 165 of file arenaViolation.c.

175 {
176  Aig_Obj_t *pWindowBeginsLocal = pWindowBegins;
177  Aig_Obj_t *pWithinWindowLocal = pWithinWindow;
178  int i;
179  Aig_Obj_t *pObj, *pObjAnd1, *pObjOr1, *pObjAnd2, *pObjBarrierLo, *pObjBarrierSwitch, *pObjArenaViolation;
180  Vec_Ptr_t *vBarrierSignals;
181 
182  assert( vBarrierLiDriver != NULL );
183  assert( vMonotoneDisjunctionNodes != NULL );
184 
185  pObjArenaViolation = Aig_Not(Aig_ManConst1( pAigNew ));
186 
187  vBarrierSignals = collectBarrierDisjunctions(pAigOld, pAigNew, vMasterBarriers);
188  assert( vBarrierSignals != NULL );
189 
190  assert( Vec_PtrSize( vMonotoneDisjunctionNodes ) == 0 );
191  Vec_PtrForEachEntry( Aig_Obj_t *, vBarrierSignals, pObj, i )
192  Vec_PtrPush( vMonotoneDisjunctionNodes, pObj );
193  assert( Vec_PtrSize( vMonotoneDisjunctionNodes ) == Vec_PtrSize( vMasterBarriers ) );
194 
195  Vec_PtrForEachEntry( Aig_Obj_t *, vBarrierSignals, pObj, i )
196  {
197  //pObjNew = driverToPoNew( pAigOld, pObj );
198  pObjAnd1 = Aig_And(pAigNew, pObj, pWindowBeginsLocal);
199  pObjBarrierLo = (Aig_Obj_t *)Vec_PtrEntry( vBarrierLo, i );
200  pObjOr1 = Aig_Or(pAigNew, pObjAnd1, pObjBarrierLo);
201  Vec_PtrPush( vBarrierLiDriver, pObjOr1 );
202 
203  pObjBarrierSwitch = Aig_Xor( pAigNew, pObj, pObjBarrierLo );
204  pObjAnd2 = Aig_And( pAigNew, pObjBarrierSwitch, pWithinWindowLocal );
205  pObjArenaViolation = Aig_Or( pAigNew, pObjAnd2, pObjArenaViolation );
206  }
207 
208  Vec_PtrFree(vBarrierSignals);
209  return pObjArenaViolation;
210 }
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Aig_Obj_t * Aig_Xor(Aig_Man_t *pAig, Aig_Obj_t *pObj1, Aig_Obj_t *pObj2)
static Aig_Obj_t * Aig_Not(Aig_Obj_t *p)
Definition: aig.h:247
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
Aig_Obj_t * Aig_Or(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:259
Definition: aig.h:69
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Vec_Ptr_t * collectBarrierDisjunctions(Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, Vec_Ptr_t *vBarriers)
#define assert(ex)
Definition: util_old.h:213
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Aig_Obj_t* createConstrained0LiveConeWithDSC ( Aig_Man_t pNewAig,
Vec_Ptr_t signalList 
)

Definition at line 212 of file arenaViolation.c.

213 {
214  Aig_Obj_t *pConsequent, *pConsequentCopy, *pAntecedent, *p0LiveCone, *pObj;
215  int i, numSigAntecedent;
216 
217  numSigAntecedent = Vec_PtrSize( signalList ) - 1;
218 
219  pAntecedent = Aig_ManConst1( pNewAig );
220  pConsequent = (Aig_Obj_t *)Vec_PtrEntry( signalList, numSigAntecedent );
221  pConsequentCopy = Aig_NotCond( (Aig_Obj_t *)(Aig_Regular(pConsequent)->pData), Aig_IsComplement( pConsequent ) );
222 
223  for(i=0; i<numSigAntecedent; i++ )
224  {
225  pObj = (Aig_Obj_t *)Vec_PtrEntry( signalList, i );
226  assert( Aig_Regular(pObj)->pData );
227  pAntecedent = Aig_And( pNewAig, pAntecedent, Aig_NotCond((Aig_Obj_t *)(Aig_Regular(pObj)->pData), Aig_IsComplement(pObj)) );
228  }
229 
230  p0LiveCone = Aig_Or( pNewAig, Aig_Not(pAntecedent), pConsequentCopy );
231 
232  return p0LiveCone;
233 }
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
static Aig_Obj_t * Aig_Not(Aig_Obj_t *p)
Definition: aig.h:247
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
Aig_Obj_t * Aig_Or(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:259
Definition: aig.h:69
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
#define assert(ex)
Definition: util_old.h:213
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
Vec_Ptr_t* createMonotoneBarrierLO ( Aig_Man_t pAigNew,
Vec_Ptr_t vBarriers 
)

Definition at line 82 of file arenaViolation.c.

83 {
84  Vec_Ptr_t *vMonotoneLO;
85  int barrierCount;
86  Aig_Obj_t *pObj;
87  int i;
88 
89  if( vBarriers == NULL )
90  return NULL;
91 
92  barrierCount = Vec_PtrSize(vBarriers);
93  if( barrierCount <= 0 )
94  return NULL;
95 
96  vMonotoneLO = Vec_PtrAlloc(barrierCount);
97  for( i=0; i<barrierCount; i++ )
98  {
99  pObj = Aig_ObjCreateCi( pAigNew );
100  Vec_PtrPush( vMonotoneLO, pObj );
101  }
102 
103  return vMonotoneLO;
104 }
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Definition: aig.h:69
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Aig_Man_t* createNewAigWith0LivePoWithDSC ( Aig_Man_t pAig,
Vec_Ptr_t signalList,
int *  index0Live,
int  windowBeginIndex,
int  withinWindowIndex,
int  pendingSignalIndex,
Vec_Ptr_t vBarriers 
)

Definition at line 323 of file arenaViolation.c.

324 {
325  Aig_Man_t *pNewAig;
326  Aig_Obj_t *pObj, *pObjNewPoDriver;
327  int i;
328  int loCopied = 0, loCreated = 0, liCopied = 0, liCreated = 0;
329  Aig_Obj_t *pObjWindowBeginsNew, *pObjWithinWindowNew, *pObjArenaViolation, *pObjTarget, *pObjArenaViolationLiDriver;
330  Aig_Obj_t *pObjNewPoDriverArenaViolated, *pObjArenaViolationLo;
331  Vec_Ptr_t *vBarrierLo, *vBarrierLiDriver, *vBarrierLi;
332  Vec_Ptr_t *vMonotoneNodes;
333 
334 #ifdef BARRIER_MONOTONE_TEST
335  Aig_Obj_t *pObjPendingSignal;
336  Aig_Obj_t *pObjPendingFlopLo;
337  Vec_Ptr_t *vMonotoneBarrierLo;
338  Aig_Obj_t *pObjPendingAndPendingSignal, *pObjMonotoneAnd, *pObjCurrMonotoneLo;
339 #endif
340 
341  //assert( Vec_PtrSize( signalList ) > 1 );
342 
343  //****************************************************************
344  // Step1: create the new manager
345  // Note: The new manager is created with "2 * Aig_ManObjNumMax(p)"
346  // nodes, but this selection is arbitrary - need to be justified
347  //****************************************************************
348  pNewAig = Aig_ManStart( Aig_ManObjNumMax(pAig) );
349  pNewAig->pName = (char *)malloc( strlen( pAig->pName ) + strlen("_0Live") + 1 );
350  sprintf(pNewAig->pName, "%s_%s", pAig->pName, "0Live");
351  pNewAig->pSpec = NULL;
352 
353  //****************************************************************
354  // Step 2: map constant nodes
355  //****************************************************************
356  pObj = Aig_ManConst1( pAig );
357  pObj->pData = Aig_ManConst1( pNewAig );
358 
359  //****************************************************************
360  // Step 3: create true PIs
361  //****************************************************************
362  Saig_ManForEachPi( pAig, pObj, i )
363  {
364  pObj->pData = Aig_ObjCreateCi( pNewAig );
365  }
366 
367  //****************************************************************
368  // Step 4: create register outputs
369  //****************************************************************
370  Saig_ManForEachLo( pAig, pObj, i )
371  {
372  loCopied++;
373  pObj->pData = Aig_ObjCreateCi( pNewAig );
374  }
375 
376  //****************************************************************
377  // Step 4.a: create register outputs for the barrier flops
378  //****************************************************************
379  vBarrierLo = createArenaLO( pNewAig, vBarriers );
380  loCreated = Vec_PtrSize(vBarrierLo);
381 
382  //****************************************************************
383  // Step 4.b: create register output for arenaViolationFlop
384  //****************************************************************
385  pObjArenaViolationLo = Aig_ObjCreateCi( pNewAig );
386  loCreated++;
387 
388 #ifdef BARRIER_MONOTONE_TEST
389  //****************************************************************
390  // Step 4.c: create register output for pendingFlop
391  //****************************************************************
392  pObjPendingFlopLo = Aig_ObjCreateCi( pNewAig );
393  loCreated++;
394 
395  //****************************************************************
396  // Step 4.d: create register outputs for the barrier flops
397  // for asserting monotonicity
398  //****************************************************************
399  vMonotoneBarrierLo = createMonotoneBarrierLO( pNewAig, vBarriers );
400  loCreated = loCreated + Vec_PtrSize(vMonotoneBarrierLo);
401 #endif
402 
403  //********************************************************************
404  // Step 5: create internal nodes
405  //********************************************************************
406  Aig_ManForEachNode( pAig, pObj, i )
407  {
408  pObj->pData = Aig_And( pNewAig, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
409  }
410 
411  //********************************************************************
412  // Step 5.a: create internal nodes corresponding to arenaViolation
413  //********************************************************************
414  pObjTarget = Aig_ManCo( pAig, windowBeginIndex );
415  pObjWindowBeginsNew = driverToPoNew( pAig, pObjTarget );
416 
417  pObjTarget = Aig_ManCo( pAig, withinWindowIndex );
418  pObjWithinWindowNew = driverToPoNew( pAig, pObjTarget );
419 
420  vBarrierLiDriver = Vec_PtrAlloc( Vec_PtrSize(vBarriers) );
421  vMonotoneNodes = Vec_PtrAlloc( Vec_PtrSize(vBarriers) );
422 
423  pObjArenaViolation = createArenaViolation( pAig, pNewAig,
424  pObjWindowBeginsNew, pObjWithinWindowNew,
425  vBarriers, vBarrierLo, vBarrierLiDriver, vMonotoneNodes );
426  assert( Vec_PtrSize(vMonotoneNodes) == Vec_PtrSize(vBarriers) );
427 
428 #ifdef ARENA_VIOLATION_CONSTRAINT
429 
430 #endif
431 
432  pObjArenaViolationLiDriver = Aig_Or( pNewAig, pObjArenaViolation, pObjArenaViolationLo );
433 
434 #ifdef BARRIER_MONOTONE_TEST
435  //********************************************************************
436  // Step 5.b: Create internal nodes for monotone testing
437  //********************************************************************
438 
439  pObjTarget = Aig_ManCo( pAig, pendingSignalIndex );
440  pObjPendingSignal = driverToPoNew( pAig, pObjTarget );
441 
442  pObjPendingAndPendingSignal = Aig_And( pNewAig, pObjPendingSignal, pObjPendingFlopLo );
443  pObjMonotoneAnd = Aig_ManConst1( pNewAig );
444  Vec_PtrForEachEntry( Aig_Obj_t *, vMonotoneNodes, pObj, i )
445  {
446  pObjCurrMonotoneLo = (Aig_Obj_t *)Vec_PtrEntry(vMonotoneBarrierLo, i);
447  pObjMonotoneAnd = Aig_And( pNewAig, pObjMonotoneAnd,
448  Aig_Or( pNewAig,
449  Aig_Not(Aig_And(pNewAig, pObjPendingAndPendingSignal, pObjCurrMonotoneLo)),
450  pObj ) );
451  }
452 #endif
453 
454  //********************************************************************
455  // Step 6: create primary outputs
456  //********************************************************************
457 
458  Saig_ManForEachPo( pAig, pObj, i )
459  {
460  pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
461  }
462 
463  pObjNewPoDriver = createConstrained0LiveConeWithDSC( pNewAig, signalList );
464  pObjNewPoDriverArenaViolated = Aig_Or( pNewAig, pObjNewPoDriver, pObjArenaViolationLo );
465 #ifdef BARRIER_MONOTONE_TEST
466  pObjNewPoDriverArenaViolated = Aig_And( pNewAig, pObjNewPoDriverArenaViolated, pObjMonotoneAnd );
467 #endif
468  Aig_ObjCreateCo( pNewAig, pObjNewPoDriverArenaViolated );
469 
470  *index0Live = i;
471 
472  //********************************************************************
473  // Step 7: create register inputs
474  //********************************************************************
475 
476  Saig_ManForEachLi( pAig, pObj, i )
477  {
478  liCopied++;
479  pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
480  }
481 
482  //********************************************************************
483  // Step 7.a: create register inputs for barrier flops
484  //********************************************************************
485  assert( Vec_PtrSize(vBarrierLiDriver) == Vec_PtrSize(vBarriers) );
486  vBarrierLi = createArenaLi( pNewAig, vBarriers, vBarrierLiDriver );
487  liCreated = Vec_PtrSize( vBarrierLi );
488 
489  //********************************************************************
490  // Step 7.b: create register inputs for arenaViolation flop
491  //********************************************************************
492  Aig_ObjCreateCo( pNewAig, pObjArenaViolationLiDriver );
493  liCreated++;
494 
495 #ifdef BARRIER_MONOTONE_TEST
496  //****************************************************************
497  // Step 7.c: create register input for pendingFlop
498  //****************************************************************
499  Aig_ObjCreateCo( pNewAig, pObjPendingSignal);
500  liCreated++;
501 
502  //********************************************************************
503  // Step 7.d: create register inputs for the barrier flops
504  // for asserting monotonicity
505  //********************************************************************
506  Vec_PtrForEachEntry( Aig_Obj_t *, vMonotoneNodes, pObj, i )
507  {
508  Aig_ObjCreateCo( pNewAig, pObj );
509  liCreated++;
510  }
511 #endif
512 
513  assert(loCopied + loCreated == liCopied + liCreated);
514  //next step should be changed
515  Aig_ManSetRegNum( pNewAig, loCopied + loCreated );
516  Aig_ManCleanup( pNewAig );
517 
518  assert( Aig_ManCheck( pNewAig ) );
519 
520  Vec_PtrFree(vBarrierLo);
521  Vec_PtrFree(vMonotoneBarrierLo);
522  Vec_PtrFree(vBarrierLiDriver);
523  Vec_PtrFree(vBarrierLi);
524  Vec_PtrFree(vMonotoneNodes);
525 
526  return pNewAig;
527 }
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
char * malloc()
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
ABC_DLL int Aig_ManCheck(Aig_Man_t *p)
FUNCTION DECLARATIONS ///.
Definition: aigCheck.c:45
Vec_Ptr_t * createMonotoneBarrierLO(Aig_Man_t *pAigNew, Vec_Ptr_t *vBarriers)
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
void * pData
Definition: aig.h:87
Aig_Obj_t * createArenaViolation(Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, Aig_Obj_t *pWindowBegins, Aig_Obj_t *pWithinWindow, Vec_Ptr_t *vMasterBarriers, Vec_Ptr_t *vBarrierLo, Vec_Ptr_t *vBarrierLiDriver, Vec_Ptr_t *vMonotoneDisjunctionNodes)
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
Vec_Ptr_t * createArenaLi(Aig_Man_t *pAigNew, Vec_Ptr_t *vBarriers, Vec_Ptr_t *vArenaSignal)
static Aig_Obj_t * Aig_Not(Aig_Obj_t *p)
Definition: aig.h:247
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
ABC_NAMESPACE_IMPL_START Vec_Ptr_t * createArenaLO(Aig_Man_t *pAigNew, Vec_Ptr_t *vBarriers)
Aig_Obj_t * createConstrained0LiveConeWithDSC(Aig_Man_t *pNewAig, Vec_Ptr_t *signalList)
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition: aigMan.c:438
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
Aig_Obj_t * driverToPoNew(Aig_Man_t *pAig, Aig_Obj_t *pObjPo)
static Aig_Obj_t * Aig_ObjChild1Copy(Aig_Obj_t *pObj)
Definition: aig.h:313
Aig_Obj_t * Aig_Or(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:259
Definition: aig.h:69
char * sprintf()
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
static Aig_Obj_t * Aig_ObjChild0Copy(Aig_Obj_t *pObj)
Definition: aig.h:312
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
#define assert(ex)
Definition: util_old.h:213
int strlen()
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91
Aig_Obj_t* driverToPoNew ( Aig_Man_t pAig,
Aig_Obj_t pObjPo 
)

Definition at line 106 of file arenaViolation.c.

107 {
108  Aig_Obj_t *poDriverOld;
109  Aig_Obj_t *poDriverNew;
110 
111  //Aig_ObjPrint( pAig, pObjPo );
112  //printf("\n");
113 
114  assert( Aig_ObjIsCo(pObjPo) );
115  poDriverOld = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPo), Aig_ObjFaninC0(pObjPo));
116  assert( !Aig_ObjIsCo(poDriverOld) );
117  poDriverNew = !Aig_IsComplement(poDriverOld)?
118  (Aig_Obj_t *)(Aig_Regular(poDriverOld)->pData) :
119  Aig_Not((Aig_Obj_t *)(Aig_Regular(poDriverOld)->pData));
120  //assert( !Aig_ObjIsCo(poDriverNew) );
121  return poDriverNew;
122 }
void * pData
Definition: aig.h:87
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
static Aig_Obj_t * Aig_Not(Aig_Obj_t *p)
Definition: aig.h:247
Definition: aig.h:69
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
#define assert(ex)
Definition: util_old.h:213
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
Aig_Man_t* generateWorkingAigWithDSC ( Aig_Man_t pAig,
Abc_Ntk_t pNtk,
int *  pIndex0Live,
Vec_Ptr_t vMasterBarriers 
)

Definition at line 529 of file arenaViolation.c.

530 {
531  Vec_Ptr_t *vSignalVector;
532  Aig_Man_t *pAigNew;
533  int pObjWithinWindow;
534  int pObjWindowBegin;
535  int pObjPendingSignal;
536 
537  vSignalVector = collectCSSignalsWithDSC( pNtk, pAig );
538 
539  pObjWindowBegin = collectWindowBeginSignalWithDSC( pNtk, pAig );
540  pObjWithinWindow = collectWithinWindowSignalWithDSC( pNtk, pAig );
541  pObjPendingSignal = collectPendingSignalWithDSC( pNtk, pAig );
542 
543  pAigNew = createNewAigWith0LivePoWithDSC( pAig, vSignalVector, pIndex0Live, pObjWindowBegin, pObjWithinWindow, pObjPendingSignal, vMasterBarriers );
544  Vec_PtrFree(vSignalVector);
545 
546  return pAigNew;
547 }
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Vec_Ptr_t * collectCSSignalsWithDSC(Abc_Ntk_t *pNtk, Aig_Man_t *pAig)
int collectPendingSignalWithDSC(Abc_Ntk_t *pNtk, Aig_Man_t *pAig)
int collectWithinWindowSignalWithDSC(Abc_Ntk_t *pNtk, Aig_Man_t *pAig)
int collectWindowBeginSignalWithDSC(Abc_Ntk_t *pNtk, Aig_Man_t *pAig)
Aig_Man_t * createNewAigWith0LivePoWithDSC(Aig_Man_t *pAig, Vec_Ptr_t *signalList, int *index0Live, int windowBeginIndex, int withinWindowIndex, int pendingSignalIndex, Vec_Ptr_t *vBarriers)
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223