abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
kLiveConstraints.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.

Functions

ABC_NAMESPACE_IMPL_START
Aig_Obj_t
createConstrained0LiveCone (Aig_Man_t *pNewAig, Vec_Ptr_t *signalList)
 
Vec_Ptr_tcollectCSSignals (Abc_Ntk_t *pNtk, Aig_Man_t *pAig)
 
Aig_Man_tcreateNewAigWith0LivePo (Aig_Man_t *pAig, Vec_Ptr_t *signalList, int *index0Live)
 
Vec_Ptr_tcheckMonotoneSignal ()
 
Vec_Ptr_tgatherMonotoneSignals (Aig_Man_t *pAig)
 
Aig_Man_tgenerateWorkingAig (Aig_Man_t *pAig, Abc_Ntk_t *pNtk, int *pIndex0Live)
 

Function Documentation

Vec_Ptr_t* checkMonotoneSignal ( )

Definition at line 144 of file kLiveConstraints.c.

145 {
146  return NULL;
147 }
Vec_Ptr_t* collectCSSignals ( Abc_Ntk_t pNtk,
Aig_Man_t pAig 
)

Definition at line 55 of file kLiveConstraints.c.

56 {
57  int i;
58  Aig_Obj_t *pObj, *pConsequent = NULL;
59  Vec_Ptr_t *vNodeArray;
60 
61  vNodeArray = Vec_PtrAlloc(1);
62 
63  Saig_ManForEachPo( pAig, pObj, i )
64  {
65  if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "csLiveConst_" ) != NULL )
66  Vec_PtrPush( vNodeArray, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj)) );
67  else if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "csLiveTarget_" ) != NULL )
68  pConsequent = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj));
69  }
70  assert( pConsequent );
71  Vec_PtrPush( vNodeArray, pConsequent );
72  return vNodeArray;
73 }
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
ABC_NAMESPACE_IMPL_START Aig_Obj_t* createConstrained0LiveCone ( Aig_Man_t pNewAig,
Vec_Ptr_t signalList 
)

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

FileName [kLiveConstraints.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Liveness property checking.]

Synopsis [Constraint analysis module for the k-Liveness algorithm invented by Koen Classen, Niklas Sorensson.]

Author [Sayak Ray]

Affiliation [UC Berkeley]

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

Revision [

Id:
liveness.c,v 1.00 2009/01/01 00:00:00 alanmi Exp

]

Definition at line 32 of file kLiveConstraints.c.

33 {
34  Aig_Obj_t *pConsequent, *pConsequentCopy, *pAntecedent, *p0LiveCone, *pObj;
35  int i, numSigAntecedent;
36 
37  numSigAntecedent = Vec_PtrSize( signalList ) - 1;
38 
39  pAntecedent = Aig_ManConst1( pNewAig );
40  pConsequent = (Aig_Obj_t *)Vec_PtrEntry( signalList, numSigAntecedent );
41  pConsequentCopy = Aig_NotCond( (Aig_Obj_t *)(Aig_Regular(pConsequent)->pData), Aig_IsComplement( pConsequent ) );
42 
43  for(i=0; i<numSigAntecedent; i++ )
44  {
45  pObj = (Aig_Obj_t *)Vec_PtrEntry( signalList, i );
46  assert( Aig_Regular(pObj)->pData );
47  pAntecedent = Aig_And( pNewAig, pAntecedent, Aig_NotCond((Aig_Obj_t *)(Aig_Regular(pObj)->pData), Aig_IsComplement(pObj)) );
48  }
49 
50  p0LiveCone = Aig_Or( pNewAig, Aig_Not(pAntecedent), pConsequentCopy );
51 
52  return p0LiveCone;
53 }
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
Aig_Man_t* createNewAigWith0LivePo ( Aig_Man_t pAig,
Vec_Ptr_t signalList,
int *  index0Live 
)

Definition at line 75 of file kLiveConstraints.c.

76 {
77  Aig_Man_t *pNewAig;
78  Aig_Obj_t *pObj, *pObjNewPoDriver;
79  int i;
80 
81  //assert( Vec_PtrSize( signalList ) > 1 );
82 
83  //****************************************************************
84  // Step1: create the new manager
85  // Note: The new manager is created with "2 * Aig_ManObjNumMax(p)"
86  // nodes, but this selection is arbitrary - need to be justified
87  //****************************************************************
88  pNewAig = Aig_ManStart( Aig_ManObjNumMax(pAig) );
89  pNewAig->pName = (char *)malloc( strlen( pAig->pName ) + strlen("_0Live") + 1 );
90  sprintf(pNewAig->pName, "%s_%s", pAig->pName, "0Live");
91  pNewAig->pSpec = NULL;
92 
93  //****************************************************************
94  // Step 2: map constant nodes
95  //****************************************************************
96  pObj = Aig_ManConst1( pAig );
97  pObj->pData = Aig_ManConst1( pNewAig );
98 
99  //****************************************************************
100  // Step 3: create true PIs
101  //****************************************************************
102  Saig_ManForEachPi( pAig, pObj, i )
103  {
104  pObj->pData = Aig_ObjCreateCi( pNewAig );
105  }
106 
107  //****************************************************************
108  // Step 5: create register outputs
109  //****************************************************************
110  Saig_ManForEachLo( pAig, pObj, i )
111  {
112  pObj->pData = Aig_ObjCreateCi( pNewAig );
113  }
114 
115  //********************************************************************
116  // Step 7: create internal nodes
117  //********************************************************************
118  Aig_ManForEachNode( pAig, pObj, i )
119  {
120  pObj->pData = Aig_And( pNewAig, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
121  }
122 
123  Saig_ManForEachPo( pAig, pObj, i )
124  {
125  pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
126  }
127 
128  pObjNewPoDriver = createConstrained0LiveCone( pNewAig, signalList );
129  Aig_ObjCreateCo( pNewAig, pObjNewPoDriver );
130  *index0Live = i;
131 
132  Saig_ManForEachLi( pAig, pObj, i )
133  {
134  pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
135  }
136 
137  Aig_ManSetRegNum( pNewAig, Aig_ManRegNum(pAig) );
138  Aig_ManCleanup( pNewAig );
139 
140  assert( Aig_ManCheck( pNewAig ) );
141  return pNewAig;
142 }
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
char * malloc()
ABC_DLL int Aig_ManCheck(Aig_Man_t *p)
FUNCTION DECLARATIONS ///.
Definition: aigCheck.c:45
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
void * pData
Definition: aig.h:87
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
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
#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
ABC_NAMESPACE_IMPL_START Aig_Obj_t * createConstrained0LiveCone(Aig_Man_t *pNewAig, Vec_Ptr_t *signalList)
static Aig_Obj_t * Aig_ObjChild1Copy(Aig_Obj_t *pObj)
Definition: aig.h:313
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 int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
#define assert(ex)
Definition: util_old.h:213
int strlen()
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91
Vec_Ptr_t* gatherMonotoneSignals ( Aig_Man_t pAig)

Definition at line 149 of file kLiveConstraints.c.

150 {
151  int i;
152  Aig_Obj_t *pObj;
153 
154  Aig_ManForEachNode( pAig, pObj, i )
155  {
156  Aig_ObjPrint( pAig, pObj );
157  printf("\n");
158  }
159 
160  return NULL;
161 }
void Aig_ObjPrint(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aigObj.c:316
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Definition: aig.h:69
Aig_Man_t* generateWorkingAig ( Aig_Man_t pAig,
Abc_Ntk_t pNtk,
int *  pIndex0Live 
)

Definition at line 163 of file kLiveConstraints.c.

164 {
165  Vec_Ptr_t *vSignalVector;
166  Aig_Man_t *pAigNew;
167 
168  vSignalVector = collectCSSignals( pNtk, pAig );
169  assert(vSignalVector);
170  pAigNew = createNewAigWith0LivePo( pAig, vSignalVector, pIndex0Live );
171  Vec_PtrFree(vSignalVector);
172 
173  return pAigNew;
174 }
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
Aig_Man_t * createNewAigWith0LivePo(Aig_Man_t *pAig, Vec_Ptr_t *signalList, int *index0Live)
Vec_Ptr_t * collectCSSignals(Abc_Ntk_t *pNtk, Aig_Man_t *pAig)
#define assert(ex)
Definition: util_old.h:213
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223