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