abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
abcUnreach.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [abcUnreach.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Network and node package.]
8 
9  Synopsis [Computes unreachable states for small benchmarks.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: abcUnreach.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "base/abc/abc.h"
22 #include "misc/extra/extraBdd.h"
23 
25 
26 
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30 
31 static DdNode * Abc_NtkTransitionRelation( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose );
32 static DdNode * Abc_NtkInitStateAndVarMap( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose );
33 static DdNode * Abc_NtkComputeUnreachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bRelation, DdNode * bInitial, int fVerbose );
34 static Abc_Ntk_t * Abc_NtkConstructExdc ( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUnreach );
35 
36 ////////////////////////////////////////////////////////////////////////
37 /// FUNCTION DEFINITIONS ///
38 ////////////////////////////////////////////////////////////////////////
39 
40 /**Function*************************************************************
41 
42  Synopsis [Extracts sequential DCs of the network.]
43 
44  Description []
45 
46  SideEffects []
47 
48  SeeAlso []
49 
50 ***********************************************************************/
51 int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, int fVerbose )
52 {
53  int fReorder = 1;
54  DdManager * dd;
55  DdNode * bRelation, * bInitial, * bUnreach;
56 
57  // remove EXDC network if present
58  if ( pNtk->pExdc )
59  {
60  Abc_NtkDelete( pNtk->pExdc );
61  pNtk->pExdc = NULL;
62  }
63 
64  // compute the global BDDs of the latches
65  dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, 1, fVerbose );
66  if ( dd == NULL )
67  return 0;
68  if ( fVerbose )
69  printf( "Shared BDD size = %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
70 
71  // create the transition relation (dereferenced global BDDs)
72  bRelation = Abc_NtkTransitionRelation( dd, pNtk, fVerbose ); Cudd_Ref( bRelation );
73  // create the initial state and the variable map
74  bInitial = Abc_NtkInitStateAndVarMap( dd, pNtk, fVerbose ); Cudd_Ref( bInitial );
75  // compute the unreachable states
76  bUnreach = Abc_NtkComputeUnreachable( dd, pNtk, bRelation, bInitial, fVerbose ); Cudd_Ref( bUnreach );
77  Cudd_RecursiveDeref( dd, bRelation );
78  Cudd_RecursiveDeref( dd, bInitial );
79 
80  // reorder and disable reordering
81  if ( fReorder )
82  {
83  if ( fVerbose )
84  fprintf( stdout, "BDD nodes in the unreachable states before reordering %d.\n", Cudd_DagSize(bUnreach) );
86  Cudd_AutodynDisable( dd );
87  if ( fVerbose )
88  fprintf( stdout, "BDD nodes in the unreachable states after reordering %d.\n", Cudd_DagSize(bUnreach) );
89  }
90 
91  // allocate ZDD variables
92  Cudd_zddVarsFromBddVars( dd, 2 );
93  // create the EXDC network representing the unreachable states
94  if ( pNtk->pExdc )
95  Abc_NtkDelete( pNtk->pExdc );
96  pNtk->pExdc = Abc_NtkConstructExdc( dd, pNtk, bUnreach );
97  Cudd_RecursiveDeref( dd, bUnreach );
98  Extra_StopManager( dd );
99 // pNtk->pManGlob = NULL;
100 
101  // make sure that everything is okay
102  if ( pNtk->pExdc && !Abc_NtkCheck( pNtk->pExdc ) )
103  {
104  printf( "Abc_NtkExtractSequentialDcs: The network check has failed.\n" );
105  Abc_NtkDelete( pNtk->pExdc );
106  return 0;
107  }
108  return 1;
109 }
110 
111 /**Function*************************************************************
112 
113  Synopsis [Computes the transition relation of the network.]
114 
115  Description [Assumes that the global BDDs are computed.]
116 
117  SideEffects []
118 
119  SeeAlso []
120 
121 ***********************************************************************/
122 DdNode * Abc_NtkTransitionRelation( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose )
123 {
124  DdNode * bRel, * bTemp, * bProd, * bVar, * bInputs;
125  Abc_Obj_t * pNode;
126  int fReorder = 1;
127  int i;
128 
129  // extand the BDD manager to represent NS variables
130  assert( dd->size == Abc_NtkCiNum(pNtk) );
131  Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + Abc_NtkLatchNum(pNtk) - 1 );
132 
133  // enable reordering
134  if ( fReorder )
136  else
137  Cudd_AutodynDisable( dd );
138 
139  // compute the transition relation
140  bRel = b1; Cudd_Ref( bRel );
141  Abc_NtkForEachLatch( pNtk, pNode, i )
142  {
143  bVar = Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + i );
144 // bProd = Cudd_bddXnor( dd, bVar, pNtk->vFuncsGlob->pArray[i] ); Cudd_Ref( bProd );
145  bProd = Cudd_bddXnor( dd, bVar, (DdNode *)Abc_ObjGlobalBdd(Abc_ObjFanin0(pNode)) ); Cudd_Ref( bProd );
146  bRel = Cudd_bddAnd( dd, bTemp = bRel, bProd ); Cudd_Ref( bRel );
147  Cudd_RecursiveDeref( dd, bTemp );
148  Cudd_RecursiveDeref( dd, bProd );
149  }
150  // free the global BDDs
151 // Abc_NtkFreeGlobalBdds( pNtk );
152  Abc_NtkFreeGlobalBdds( pNtk, 0 );
153 
154  // quantify the PI variables
155  bInputs = Extra_bddComputeRangeCube( dd, 0, Abc_NtkPiNum(pNtk) ); Cudd_Ref( bInputs );
156  bRel = Cudd_bddExistAbstract( dd, bTemp = bRel, bInputs ); Cudd_Ref( bRel );
157  Cudd_RecursiveDeref( dd, bTemp );
158  Cudd_RecursiveDeref( dd, bInputs );
159 
160  // reorder and disable reordering
161  if ( fReorder )
162  {
163  if ( fVerbose )
164  fprintf( stdout, "BDD nodes in the transition relation before reordering %d.\n", Cudd_DagSize(bRel) );
166  Cudd_AutodynDisable( dd );
167  if ( fVerbose )
168  fprintf( stdout, "BDD nodes in the transition relation after reordering %d.\n", Cudd_DagSize(bRel) );
169  }
170  Cudd_Deref( bRel );
171  return bRel;
172 }
173 
174 /**Function*************************************************************
175 
176  Synopsis [Computes the initial state and sets up the variable map.]
177 
178  Description []
179 
180  SideEffects []
181 
182  SeeAlso []
183 
184 ***********************************************************************/
185 DdNode * Abc_NtkInitStateAndVarMap( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose )
186 {
187  DdNode ** pbVarsX, ** pbVarsY;
188  DdNode * bTemp, * bProd, * bVar;
189  Abc_Obj_t * pLatch;
190  int i;
191 
192  // set the variable mapping for Cudd_bddVarMap()
193  pbVarsX = ABC_ALLOC( DdNode *, dd->size );
194  pbVarsY = ABC_ALLOC( DdNode *, dd->size );
195  bProd = b1; Cudd_Ref( bProd );
196  Abc_NtkForEachLatch( pNtk, pLatch, i )
197  {
198  pbVarsX[i] = dd->vars[ Abc_NtkPiNum(pNtk) + i ];
199  pbVarsY[i] = dd->vars[ Abc_NtkCiNum(pNtk) + i ];
200  // get the initial value of the latch
201  bVar = Cudd_NotCond( pbVarsX[i], !Abc_LatchIsInit1(pLatch) );
202  bProd = Cudd_bddAnd( dd, bTemp = bProd, bVar ); Cudd_Ref( bProd );
203  Cudd_RecursiveDeref( dd, bTemp );
204  }
205  Cudd_SetVarMap( dd, pbVarsX, pbVarsY, Abc_NtkLatchNum(pNtk) );
206  ABC_FREE( pbVarsX );
207  ABC_FREE( pbVarsY );
208 
209  Cudd_Deref( bProd );
210  return bProd;
211 }
212 
213 /**Function*************************************************************
214 
215  Synopsis [Computes the set of unreachable states.]
216 
217  Description []
218 
219  SideEffects []
220 
221  SeeAlso []
222 
223 ***********************************************************************/
224 DdNode * Abc_NtkComputeUnreachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bTrans, DdNode * bInitial, int fVerbose )
225 {
226  DdNode * bRelation, * bReached, * bCubeCs;
227  DdNode * bCurrent, * bNext, * bTemp;
228  int nIters, nMints;
229 
230  // perform reachability analisys
231  bCurrent = bInitial; Cudd_Ref( bCurrent );
232  bReached = bInitial; Cudd_Ref( bReached );
233  bRelation = bTrans; Cudd_Ref( bRelation );
234  bCubeCs = Extra_bddComputeRangeCube( dd, Abc_NtkPiNum(pNtk), Abc_NtkCiNum(pNtk) ); Cudd_Ref( bCubeCs );
235  for ( nIters = 1; ; nIters++ )
236  {
237  // compute the next states
238  bNext = Cudd_bddAndAbstract( dd, bRelation, bCurrent, bCubeCs ); Cudd_Ref( bNext );
239  Cudd_RecursiveDeref( dd, bCurrent );
240  // remap these states into the current state vars
241  bNext = Cudd_bddVarMap( dd, bTemp = bNext ); Cudd_Ref( bNext );
242  Cudd_RecursiveDeref( dd, bTemp );
243  // check if there are any new states
244  if ( Cudd_bddLeq( dd, bNext, bReached ) )
245  break;
246  // get the new states
247  bCurrent = Cudd_bddAnd( dd, bNext, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
248  // minimize the new states with the reached states
249 // bCurrent = Cudd_bddConstrain( dd, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
250 // Cudd_RecursiveDeref( dd, bTemp );
251  // add to the reached states
252  bReached = Cudd_bddOr( dd, bTemp = bReached, bNext ); Cudd_Ref( bReached );
253  Cudd_RecursiveDeref( dd, bTemp );
254  Cudd_RecursiveDeref( dd, bNext );
255  // minimize the transition relation
256 // bRelation = Cudd_bddConstrain( dd, bTemp = bRelation, Cudd_Not(bReached) ); Cudd_Ref( bRelation );
257 // Cudd_RecursiveDeref( dd, bTemp );
258  }
259  Cudd_RecursiveDeref( dd, bRelation );
260  Cudd_RecursiveDeref( dd, bCubeCs );
261  Cudd_RecursiveDeref( dd, bNext );
262  // report the stats
263  if ( fVerbose )
264  {
265  nMints = (int)Cudd_CountMinterm(dd, bReached, Abc_NtkLatchNum(pNtk) );
266  fprintf( stdout, "Reachability analysis completed in %d iterations.\n", nIters );
267  fprintf( stdout, "The number of minterms in the reachable state set = %d. (%6.2f %%)\n", nMints, 100.0*nMints/(1<<Abc_NtkLatchNum(pNtk)) );
268  }
269 //ABC_PRB( dd, bReached );
270  Cudd_Deref( bReached );
271  return Cudd_Not( bReached );
272 }
273 
274 /**Function*************************************************************
275 
276  Synopsis [Creates the EXDC network.]
277 
278  Description [The set of unreachable states depends on CS variables.]
279 
280  SideEffects []
281 
282  SeeAlso []
283 
284 ***********************************************************************/
286 {
287  Abc_Ntk_t * pNtkNew;
288  Abc_Obj_t * pNode, * pNodeNew;
289  int * pPermute;
290  int i;
291 
292  // start the new network
293  pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD, 1 );
294  pNtkNew->pName = Extra_UtilStrsav( "exdc" );
295  pNtkNew->pSpec = NULL;
296 
297  // create PIs corresponding to LOs
298  Abc_NtkForEachLatchOutput( pNtk, pNode, i )
299  Abc_ObjAssignName( pNode->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pNode), NULL );
300  // cannot ADD POs here because pLatch->pCopy point to the PIs
301 
302  // create a new node
303  pNodeNew = Abc_NtkCreateNode(pNtkNew);
304  // add the fanins corresponding to latch outputs
305  Abc_NtkForEachLatchOutput( pNtk, pNode, i )
306  Abc_ObjAddFanin( pNodeNew, pNode->pCopy );
307 
308  // create the logic function
309  pPermute = ABC_ALLOC( int, dd->size );
310  for ( i = 0; i < dd->size; i++ )
311  pPermute[i] = -1;
312  Abc_NtkForEachLatch( pNtk, pNode, i )
313  pPermute[Abc_NtkPiNum(pNtk) + i] = i;
314  // remap the functions
315  pNodeNew->pData = Extra_TransferPermute( dd, (DdManager *)pNtkNew->pManFunc, bUnreach, pPermute ); Cudd_Ref( (DdNode *)pNodeNew->pData );
316  ABC_FREE( pPermute );
317  Abc_NodeMinimumBase( pNodeNew );
318 
319  // for each CO, create PO (skip POs equal to CIs because of name conflict)
320  Abc_NtkForEachPo( pNtk, pNode, i )
321  if ( !Abc_ObjIsCi(Abc_ObjFanin0(pNode)) )
322  Abc_ObjAssignName( pNode->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName(pNode), NULL );
323  Abc_NtkForEachLatchInput( pNtk, pNode, i )
324  Abc_ObjAssignName( pNode->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName(pNode), NULL );
325 
326  // link to the POs of the network
327  Abc_NtkForEachPo( pNtk, pNode, i )
328  if ( !Abc_ObjIsCi(Abc_ObjFanin0(pNode)) )
329  Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
330  Abc_NtkForEachLatchInput( pNtk, pNode, i )
331  Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
332 
333  // remove the extra nodes
334  Abc_AigCleanup( (Abc_Aig_t *)pNtkNew->pManFunc );
335 
336  // fix the problem with complemented and duplicated CO edges
337  Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
338 
339  // transform the network to the SOP representation
340  if ( !Abc_NtkBddToSop( pNtkNew, 0 ) )
341  {
342  printf( "Abc_NtkConstructExdc(): Converting to SOPs has failed.\n" );
343  return NULL;
344  }
345  return pNtkNew;
346 // return NULL;
347 }
348 
349 ////////////////////////////////////////////////////////////////////////
350 /// END OF FILE ///
351 ////////////////////////////////////////////////////////////////////////
352 
353 
355 
static int Abc_ObjIsCi(Abc_Obj_t *pObj)
Definition: abc.h:351
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
double Cudd_CountMinterm(DdManager *manager, DdNode *node, int nvars)
Definition: cuddUtil.c:578
Definition: cudd.h:278
#define Cudd_Not(node)
Definition: cudd.h:367
Abc_Ntk_t * pExdc
Definition: abc.h:201
static DdNode * Abc_NtkComputeUnreachable(DdManager *dd, Abc_Ntk_t *pNtk, DdNode *bRelation, DdNode *bInitial, int fVerbose)
Definition: abcUnreach.c:224
void Cudd_Deref(DdNode *node)
Definition: cuddRef.c:438
int size
Definition: cuddInt.h:361
#define Abc_NtkForEachLatchOutput(pNtk, pObj, i)
Definition: abc.h:503
#define b1
Definition: extraBdd.h:76
DdNode * Cudd_bddExistAbstract(DdManager *manager, DdNode *f, DdNode *cube)
Definition: cuddBddAbs.c:130
DdNode * Extra_TransferPermute(DdManager *ddSource, DdManager *ddDestination, DdNode *f, int *Permute)
Definition: extraBddMisc.c:87
int Cudd_SetVarMap(DdManager *manager, DdNode **x, DdNode **y, int n)
Definition: cuddCompose.c:416
static int Abc_NtkLatchNum(Abc_Ntk_t *pNtk)
Definition: abc.h:294
static ABC_NAMESPACE_IMPL_START DdNode * Abc_NtkTransitionRelation(DdManager *dd, Abc_Ntk_t *pNtk, int fVerbose)
DECLARATIONS ///.
Definition: abcUnreach.c:122
static int Abc_NtkCiNum(Abc_Ntk_t *pNtk)
Definition: abc.h:287
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
ABC_DLL int Abc_NtkCheck(Abc_Ntk_t *pNtk)
FUNCTION DEFINITIONS ///.
Definition: abcCheck.c:61
ABC_DLL char * Abc_ObjAssignName(Abc_Obj_t *pObj, char *pName, char *pSuffix)
Definition: abcNames.c:68
void Extra_StopManager(DdManager *dd)
Definition: extraBddMisc.c:223
static DdNode * Abc_NtkInitStateAndVarMap(DdManager *dd, Abc_Ntk_t *pNtk, int fVerbose)
Definition: abcUnreach.c:185
static Abc_Obj_t * Abc_ObjFanin0(Abc_Obj_t *pObj)
Definition: abc.h:373
DECLARATIONS ///.
Definition: abcAig.c:52
int Abc_NtkExtractSequentialDcs(Abc_Ntk_t *pNtk, int fVerbose)
FUNCTION DEFINITIONS ///.
Definition: abcUnreach.c:51
ABC_DLL void Abc_NtkDelete(Abc_Ntk_t *pNtk)
Definition: abcNtk.c:1233
char * Extra_UtilStrsav(const char *s)
static void * Abc_ObjGlobalBdd(Abc_Obj_t *pObj)
Definition: abc.h:431
ABC_DLL void Abc_ObjAddFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
Definition: abcFanio.c:84
ABC_DLL Abc_Ntk_t * Abc_NtkAlloc(Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan)
DECLARATIONS ///.
Definition: abcNtk.c:50
ABC_DLL void * Abc_NtkFreeGlobalBdds(Abc_Ntk_t *pNtk, int fFreeMan)
Definition: abcNtbdd.c:476
void * pManFunc
Definition: abc.h:191
DdNode * Cudd_bddVarMap(DdManager *manager, DdNode *f)
Definition: cuddCompose.c:373
Abc_Obj_t * pCopy
Definition: abc.h:148
DdNode * Extra_bddComputeRangeCube(DdManager *dd, int iStart, int iStop)
Definition: extraBddMisc.c:699
ABC_DLL int Abc_AigCleanup(Abc_Aig_t *pMan)
Definition: abcAig.c:194
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
DdNode * Cudd_bddAndAbstract(DdManager *manager, DdNode *f, DdNode *g, DdNode *cube)
Definition: cuddAndAbs.c:124
#define Abc_NtkForEachLatch(pNtk, pObj, i)
Definition: abc.h:497
static int Abc_LatchIsInit1(Abc_Obj_t *pLatch)
Definition: abc.h:423
static Abc_Obj_t * Abc_NtkCreatePi(Abc_Ntk_t *pNtk)
Definition: abc.h:303
DdNode * Cudd_bddXnor(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:507
DdNode * Cudd_bddOr(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:381
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
void Cudd_AutodynDisable(DdManager *unique)
Definition: cuddAPI.c:708
char * pSpec
Definition: abc.h:159
ABC_DLL int Abc_NtkLogicMakeSimpleCos(Abc_Ntk_t *pNtk, int fDuplicate)
Definition: abcUtil.c:1047
int Cudd_bddLeq(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:536
ABC_DLL int Abc_NtkBddToSop(Abc_Ntk_t *pNtk, int fDirect)
Definition: abcFunc.c:359
#define ABC_FREE(obj)
Definition: abc_global.h:232
static int Abc_NtkPiNum(Abc_Ntk_t *pNtk)
Definition: abc.h:285
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
Definition: abcNames.c:48
DdNode ** vars
Definition: cuddInt.h:390
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:416
#define Abc_NtkForEachLatchInput(pNtk, pObj, i)
Definition: abc.h:500
static Abc_Obj_t * Abc_NtkCreateNode(Abc_Ntk_t *pNtk)
Definition: abc.h:308
unsigned int Cudd_ReadKeys(DdManager *dd)
Definition: cuddAPI.c:1626
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
int Cudd_zddVarsFromBddVars(DdManager *dd, int multiplicity)
Definition: cuddAPI.c:519
static Abc_Ntk_t * Abc_NtkConstructExdc(DdManager *dd, Abc_Ntk_t *pNtk, DdNode *bUnreach)
Definition: abcUnreach.c:285
#define assert(ex)
Definition: util_old.h:213
int Cudd_ReduceHeap(DdManager *table, Cudd_ReorderingType heuristic, int minsize)
Definition: cuddReorder.c:176
void Cudd_AutodynEnable(DdManager *unique, Cudd_ReorderingType method)
Definition: cuddAPI.c:669
void * pData
Definition: abc.h:145
ABC_DLL void * Abc_NtkBuildGlobalBdds(Abc_Ntk_t *pNtk, int fBddSizeMax, int fDropInternal, int fReorder, int fVerbose)
Definition: abcNtbdd.c:251
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
#define Abc_NtkForEachPo(pNtk, pPo, i)
Definition: abc.h:517
unsigned int Cudd_ReadDead(DdManager *dd)
Definition: cuddAPI.c:1646
static Abc_Obj_t * Abc_NtkCreatePo(Abc_Ntk_t *pNtk)
Definition: abc.h:304
char * pName
Definition: abc.h:158
ABC_DLL int Abc_NodeMinimumBase(Abc_Obj_t *pNode)
Definition: abcMinBase.c:70
int Cudd_DagSize(DdNode *node)
Definition: cuddUtil.c:442