ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
abcAuto.c
Go to the documentation of this file.
1
20
21#include "base/abc/abc.h"
22
23#ifdef ABC_USE_CUDD
24#include "bdd/extrab/extraBdd.h"
25#endif
26
28
29
33
34#ifdef ABC_USE_CUDD
35
36static void Abc_NtkAutoPrintAll( DdManager * dd, int nInputs, DdNode * pbOutputs[], int nOutputs, char * pInputNames[], char * pOutputNames[], int fNaive );
37static void Abc_NtkAutoPrintOne( DdManager * dd, int nInputs, DdNode * pbOutputs[], int Output, char * pInputNames[], char * pOutputNames[], int fNaive );
38
42
54void Abc_NtkAutoPrint( Abc_Ntk_t * pNtk, int Output, int fNaive, int fVerbose )
55{
56 DdManager * dd; // the BDD manager used to hold shared BDDs
57 DdNode ** pbGlobal; // temporary storage for global BDDs
58 char ** pInputNames; // pointers to the CI names
59 char ** pOutputNames; // pointers to the CO names
60 int nOutputs, nInputs, i;
61 Vec_Ptr_t * vFuncsGlob;
62 Abc_Obj_t * pObj;
63
64 // compute the global BDDs
65 if ( Abc_NtkBuildGlobalBdds(pNtk, 10000000, 1, 1, 0, fVerbose) == NULL )
66 return;
67
68 // get information about the network
69 nInputs = Abc_NtkCiNum(pNtk);
70 nOutputs = Abc_NtkCoNum(pNtk);
71// dd = pNtk->pManGlob;
72 dd = (DdManager *)Abc_NtkGlobalBddMan( pNtk );
73
74 // complement the global functions
75 vFuncsGlob = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
76 Abc_NtkForEachCo( pNtk, pObj, i )
77 Vec_PtrPush( vFuncsGlob, Abc_ObjGlobalBdd(pObj) );
78 pbGlobal = (DdNode **)Vec_PtrArray( vFuncsGlob );
79
80 // get the network names
81 pInputNames = Abc_NtkCollectCioNames( pNtk, 0 );
82 pOutputNames = Abc_NtkCollectCioNames( pNtk, 1 );
83
84 // print the size of the BDDs
85 if ( fVerbose )
86 printf( "Shared BDD size = %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
87
88 // allocate additional variables
89 for ( i = 0; i < nInputs; i++ )
90 Cudd_bddNewVar( dd );
91 assert( Cudd_ReadSize(dd) == 2 * nInputs );
92
93 // create ZDD variables in the manager
94 Cudd_zddVarsFromBddVars( dd, 2 );
95
96 // perform the analysis of the primary output functions for auto-symmetry
97 if ( Output == -1 )
98 Abc_NtkAutoPrintAll( dd, nInputs, pbGlobal, nOutputs, pInputNames, pOutputNames, fNaive );
99 else
100 Abc_NtkAutoPrintOne( dd, nInputs, pbGlobal, Output, pInputNames, pOutputNames, fNaive );
101
102 // deref the PO functions
103// Abc_NtkFreeGlobalBdds( pNtk );
104 // stop the global BDD manager
105// Extra_StopManager( pNtk->pManGlob );
106// pNtk->pManGlob = NULL;
107 Abc_NtkFreeGlobalBdds( pNtk, 1 );
108 ABC_FREE( pInputNames );
109 ABC_FREE( pOutputNames );
110 Vec_PtrFree( vFuncsGlob );
111}
112
124void Abc_NtkAutoPrintAll( DdManager * dd, int nInputs, DdNode * pbOutputs[], int nOutputs, char * pInputNames[], char * pOutputNames[], int fNaive )
125{
126 DdNode * bSpace1, * bSpace2, * bCanVars, * bReduced, * zEquations;
127 double nMints;
128 int nSupp, SigCounter, o;
129
130 int nAutos;
131 int nAutoSyms;
132 int nAutoSymsMax;
133 int nAutoSymsMaxSupp;
134 int nAutoSymOuts;
135 int nSuppSizeMax;
136 abctime clk;
137
138 nAutoSymOuts = 0;
139 nAutoSyms = 0;
140 nAutoSymsMax = 0;
141 nAutoSymsMaxSupp = 0;
142 nSuppSizeMax = 0;
143 clk = Abc_Clock();
144
145 SigCounter = 0;
146 for ( o = 0; o < nOutputs; o++ )
147 {
148// bSpace1 = Extra_bddSpaceFromFunctionFast( dd, pbOutputs[o] ); Cudd_Ref( bSpace1 );
149 bSpace1 = Extra_bddSpaceFromFunction( dd, pbOutputs[o], pbOutputs[o] ); Cudd_Ref( bSpace1 );
150 bCanVars = Extra_bddSpaceCanonVars( dd, bSpace1 ); Cudd_Ref( bCanVars );
151 bReduced = Extra_bddSpaceReduce( dd, pbOutputs[o], bCanVars ); Cudd_Ref( bReduced );
152 zEquations = Extra_bddSpaceEquations( dd, bSpace1 ); Cudd_Ref( zEquations );
153
154 nSupp = Cudd_SupportSize( dd, bSpace1 );
155 nMints = Cudd_CountMinterm( dd, bSpace1, nSupp );
156 nAutos = Extra_Base2LogDouble(nMints);
157 printf( "Output #%3d: Inputs = %2d. AutoK = %2d.\n", o, nSupp, nAutos );
158
159 if ( nAutos > 0 )
160 {
161 nAutoSymOuts++;
162 nAutoSyms += nAutos;
163 if ( nAutoSymsMax < nAutos )
164 {
165 nAutoSymsMax = nAutos;
166 nAutoSymsMaxSupp = nSupp;
167 }
168 }
169 if ( nSuppSizeMax < nSupp )
170 nSuppSizeMax = nSupp;
171
172
173//ABC_PRB( dd, bCanVars );
174//ABC_PRB( dd, bReduced );
175//Cudd_PrintMinterm( dd, bReduced );
176//printf( "The equations are:\n" );
177//Cudd_zddPrintCover( dd, zEquations );
178//printf( "\n" );
179//fflush( stdout );
180
181 bSpace2 = Extra_bddSpaceFromMatrixPos( dd, zEquations ); Cudd_Ref( bSpace2 );
182//ABC_PRB( dd, bSpace1 );
183//ABC_PRB( dd, bSpace2 );
184 if ( bSpace1 != bSpace2 )
185 printf( "Spaces are NOT EQUAL!\n" );
186// else
187// printf( "Spaces are equal.\n" );
188
189 Cudd_RecursiveDeref( dd, bSpace1 );
190 Cudd_RecursiveDeref( dd, bSpace2 );
191 Cudd_RecursiveDeref( dd, bCanVars );
192 Cudd_RecursiveDeref( dd, bReduced );
193 Cudd_RecursiveDerefZdd( dd, zEquations );
194 }
195
196 printf( "The cumulative statistics for all outputs:\n" );
197 printf( "Ins=%3d ", nInputs );
198 printf( "InMax=%3d ", nSuppSizeMax );
199 printf( "Outs=%3d ", nOutputs );
200 printf( "Auto=%3d ", nAutoSymOuts );
201 printf( "SumK=%3d ", nAutoSyms );
202 printf( "KMax=%2d ", nAutoSymsMax );
203 printf( "Supp=%3d ", nAutoSymsMaxSupp );
204 printf( "Time=%4.2f ", (float)(Abc_Clock() - clk)/(float)(CLOCKS_PER_SEC) );
205 printf( "\n" );
206}
207
219void Abc_NtkAutoPrintOne( DdManager * dd, int nInputs, DdNode * pbOutputs[], int Output, char * pInputNames[], char * pOutputNames[], int fNaive )
220{
221 DdNode * bSpace1, * bCanVars, * bReduced, * zEquations;
222 double nMints;
223 int nSupp, SigCounter;
224 int nAutos;
225
226 SigCounter = 0;
227 bSpace1 = Extra_bddSpaceFromFunctionFast( dd, pbOutputs[Output] ); Cudd_Ref( bSpace1 );
228// bSpace1 = Extra_bddSpaceFromFunction( dd, pbOutputs[Output], pbOutputs[Output] ); Cudd_Ref( bSpace1 );
229 bCanVars = Extra_bddSpaceCanonVars( dd, bSpace1 ); Cudd_Ref( bCanVars );
230 bReduced = Extra_bddSpaceReduce( dd, pbOutputs[Output], bCanVars ); Cudd_Ref( bReduced );
231 zEquations = Extra_bddSpaceEquations( dd, bSpace1 ); Cudd_Ref( zEquations );
232
233 nSupp = Cudd_SupportSize( dd, bSpace1 );
234 nMints = Cudd_CountMinterm( dd, bSpace1, nSupp );
235 nAutos = Extra_Base2LogDouble(nMints);
236 printf( "Output #%3d: Inputs = %2d. AutoK = %2d.\n", Output, nSupp, nAutos );
237
238 Cudd_RecursiveDeref( dd, bSpace1 );
239 Cudd_RecursiveDeref( dd, bCanVars );
240 Cudd_RecursiveDeref( dd, bReduced );
241 Cudd_RecursiveDerefZdd( dd, zEquations );
242}
243
244#else
245
246void Abc_NtkAutoPrint( Abc_Ntk_t * pNtk, int Output, int fNaive, int fVerbose ) {}
247
248#endif
249
253
254
256
ABC_NAMESPACE_IMPL_START void Abc_NtkAutoPrint(Abc_Ntk_t *pNtk, int Output, int fNaive, int fVerbose)
DECLARATIONS ///.
Definition abcAuto.c:246
struct Abc_Obj_t_ Abc_Obj_t
Definition abc.h:116
#define Abc_NtkForEachCo(pNtk, pCo, i)
Definition abc.h:522
struct Abc_Ntk_t_ Abc_Ntk_t
Definition abc.h:115
ABC_DLL void * Abc_NtkFreeGlobalBdds(Abc_Ntk_t *pNtk, int fFreeMan)
ABC_DLL void * Abc_NtkBuildGlobalBdds(Abc_Ntk_t *pNtk, int fBddSizeMax, int fDropInternal, int fReorder, int fReverse, int fVerbose)
ABC_DLL char ** Abc_NtkCollectCioNames(Abc_Ntk_t *pNtk, int fCollectCos)
Definition abcNames.c:285
ABC_INT64_T abctime
Definition abc_global.h:332
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
DdNode * Extra_bddSpaceFromFunction(DdManager *dd, DdNode *bF, DdNode *bG)
DdNode * Extra_bddSpaceFromMatrixPos(DdManager *dd, DdNode *zA)
DdNode * Extra_bddSpaceCanonVars(DdManager *dd, DdNode *bSpace)
DdNode * Extra_bddSpaceEquations(DdManager *dd, DdNode *bSpace)
DdNode * Extra_bddSpaceReduce(DdManager *dd, DdNode *bFunc, DdNode *bCanonVars)
DdNode * Extra_bddSpaceFromFunctionFast(DdManager *dd, DdNode *bFunc)
int Extra_Base2LogDouble(double Num)
#define assert(ex)
Definition util_old.h:213
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42