summaryrefslogtreecommitdiffstats
path: root/src/base/abci/abcAuto.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/abci/abcAuto.c')
-rw-r--r--src/base/abci/abcAuto.c239
1 files changed, 239 insertions, 0 deletions
diff --git a/src/base/abci/abcAuto.c b/src/base/abci/abcAuto.c
new file mode 100644
index 00000000..40212c17
--- /dev/null
+++ b/src/base/abci/abcAuto.c
@@ -0,0 +1,239 @@
+/**CFile****************************************************************
+
+ FileName [abcAuto.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Computation of autosymmetries.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abcAuto.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static void Abc_NtkAutoPrintAll( DdManager * dd, int nInputs, DdNode * pbOutputs[], int nOutputs, char * pInputNames[], char * pOutputNames[], int fNaive );
+static void Abc_NtkAutoPrintOne( DdManager * dd, int nInputs, DdNode * pbOutputs[], int Output, char * pInputNames[], char * pOutputNames[], int fNaive );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkAutoPrint( Abc_Ntk_t * pNtk, int Output, int fNaive, int fVerbose )
+{
+ DdManager * dd; // the BDD manager used to hold shared BDDs
+ DdNode ** pbGlobal; // temporary storage for global BDDs
+ char ** pInputNames; // pointers to the CI names
+ char ** pOutputNames; // pointers to the CO names
+ int nOutputs, nInputs, i;
+ Vec_Ptr_t * vFuncsGlob;
+ Abc_Obj_t * pObj;
+
+ // compute the global BDDs
+ if ( Abc_NtkBuildGlobalBdds(pNtk, 10000000, 1, 1, fVerbose) == NULL )
+ return;
+
+ // get information about the network
+ nInputs = Abc_NtkCiNum(pNtk);
+ nOutputs = Abc_NtkCoNum(pNtk);
+// dd = pNtk->pManGlob;
+ dd = Abc_NtkGlobalBddMan( pNtk );
+
+ // complement the global functions
+ vFuncsGlob = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
+ Abc_NtkForEachCo( pNtk, pObj, i )
+ Vec_PtrPush( vFuncsGlob, Abc_ObjGlobalBdd(pObj) );
+ pbGlobal = (DdNode **)Vec_PtrArray( vFuncsGlob );
+
+ // get the network names
+ pInputNames = Abc_NtkCollectCioNames( pNtk, 0 );
+ pOutputNames = Abc_NtkCollectCioNames( pNtk, 1 );
+
+ // print the size of the BDDs
+ if ( fVerbose )
+ printf( "Shared BDD size = %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+
+ // allocate additional variables
+ for ( i = 0; i < nInputs; i++ )
+ Cudd_bddNewVar( dd );
+ assert( Cudd_ReadSize(dd) == 2 * nInputs );
+
+ // create ZDD variables in the manager
+ Cudd_zddVarsFromBddVars( dd, 2 );
+
+ // perform the analysis of the primary output functions for auto-symmetry
+ if ( Output == -1 )
+ Abc_NtkAutoPrintAll( dd, nInputs, pbGlobal, nOutputs, pInputNames, pOutputNames, fNaive );
+ else
+ Abc_NtkAutoPrintOne( dd, nInputs, pbGlobal, Output, pInputNames, pOutputNames, fNaive );
+
+ // deref the PO functions
+// Abc_NtkFreeGlobalBdds( pNtk );
+ // stop the global BDD manager
+// Extra_StopManager( pNtk->pManGlob );
+// pNtk->pManGlob = NULL;
+ Abc_NtkFreeGlobalBdds( pNtk, 1 );
+ free( pInputNames );
+ free( pOutputNames );
+ Vec_PtrFree( vFuncsGlob );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkAutoPrintAll( DdManager * dd, int nInputs, DdNode * pbOutputs[], int nOutputs, char * pInputNames[], char * pOutputNames[], int fNaive )
+{
+ DdNode * bSpace1, * bSpace2, * bCanVars, * bReduced, * zEquations;
+ double nMints;
+ int nSupp, SigCounter, o;
+
+ int nAutos;
+ int nAutoSyms;
+ int nAutoSymsMax;
+ int nAutoSymsMaxSupp;
+ int nAutoSymOuts;
+ int nSuppSizeMax;
+ int clk;
+
+ nAutoSymOuts = 0;
+ nAutoSyms = 0;
+ nAutoSymsMax = 0;
+ nAutoSymsMaxSupp = 0;
+ nSuppSizeMax = 0;
+ clk = clock();
+
+ SigCounter = 0;
+ for ( o = 0; o < nOutputs; o++ )
+ {
+// bSpace1 = Extra_bddSpaceFromFunctionFast( dd, pbOutputs[o] ); Cudd_Ref( bSpace1 );
+ bSpace1 = Extra_bddSpaceFromFunction( dd, pbOutputs[o], pbOutputs[o] ); Cudd_Ref( bSpace1 );
+ bCanVars = Extra_bddSpaceCanonVars( dd, bSpace1 ); Cudd_Ref( bCanVars );
+ bReduced = Extra_bddSpaceReduce( dd, pbOutputs[o], bCanVars ); Cudd_Ref( bReduced );
+ zEquations = Extra_bddSpaceEquations( dd, bSpace1 ); Cudd_Ref( zEquations );
+
+ nSupp = Cudd_SupportSize( dd, bSpace1 );
+ nMints = Cudd_CountMinterm( dd, bSpace1, nSupp );
+ nAutos = Extra_Base2LogDouble(nMints);
+ printf( "Output #%3d: Inputs = %2d. AutoK = %2d.\n", o, nSupp, nAutos );
+
+ if ( nAutos > 0 )
+ {
+ nAutoSymOuts++;
+ nAutoSyms += nAutos;
+ if ( nAutoSymsMax < nAutos )
+ {
+ nAutoSymsMax = nAutos;
+ nAutoSymsMaxSupp = nSupp;
+ }
+ }
+ if ( nSuppSizeMax < nSupp )
+ nSuppSizeMax = nSupp;
+
+
+//PRB( dd, bCanVars );
+//PRB( dd, bReduced );
+//Cudd_PrintMinterm( dd, bReduced );
+//printf( "The equations are:\n" );
+//Cudd_zddPrintCover( dd, zEquations );
+//printf( "\n" );
+//fflush( stdout );
+
+ bSpace2 = Extra_bddSpaceFromMatrixPos( dd, zEquations ); Cudd_Ref( bSpace2 );
+//PRB( dd, bSpace1 );
+//PRB( dd, bSpace2 );
+ if ( bSpace1 != bSpace2 )
+ printf( "Spaces are NOT EQUAL!\n" );
+// else
+// printf( "Spaces are equal.\n" );
+
+ Cudd_RecursiveDeref( dd, bSpace1 );
+ Cudd_RecursiveDeref( dd, bSpace2 );
+ Cudd_RecursiveDeref( dd, bCanVars );
+ Cudd_RecursiveDeref( dd, bReduced );
+ Cudd_RecursiveDerefZdd( dd, zEquations );
+ }
+
+ printf( "The cumulative statistics for all outputs:\n" );
+ printf( "Ins=%3d ", nInputs );
+ printf( "InMax=%3d ", nSuppSizeMax );
+ printf( "Outs=%3d ", nOutputs );
+ printf( "Auto=%3d ", nAutoSymOuts );
+ printf( "SumK=%3d ", nAutoSyms );
+ printf( "KMax=%2d ", nAutoSymsMax );
+ printf( "Supp=%3d ", nAutoSymsMaxSupp );
+ printf( "Time=%4.2f ", (float)(clock() - clk)/(float)(CLOCKS_PER_SEC) );
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkAutoPrintOne( DdManager * dd, int nInputs, DdNode * pbOutputs[], int Output, char * pInputNames[], char * pOutputNames[], int fNaive )
+{
+ DdNode * bSpace1, * bCanVars, * bReduced, * zEquations;
+ double nMints;
+ int nSupp, SigCounter;
+ int nAutos;
+
+ SigCounter = 0;
+ bSpace1 = Extra_bddSpaceFromFunctionFast( dd, pbOutputs[Output] ); Cudd_Ref( bSpace1 );
+// bSpace1 = Extra_bddSpaceFromFunction( dd, pbOutputs[Output], pbOutputs[Output] ); Cudd_Ref( bSpace1 );
+ bCanVars = Extra_bddSpaceCanonVars( dd, bSpace1 ); Cudd_Ref( bCanVars );
+ bReduced = Extra_bddSpaceReduce( dd, pbOutputs[Output], bCanVars ); Cudd_Ref( bReduced );
+ zEquations = Extra_bddSpaceEquations( dd, bSpace1 ); Cudd_Ref( zEquations );
+
+ nSupp = Cudd_SupportSize( dd, bSpace1 );
+ nMints = Cudd_CountMinterm( dd, bSpace1, nSupp );
+ nAutos = Extra_Base2LogDouble(nMints);
+ printf( "Output #%3d: Inputs = %2d. AutoK = %2d.\n", Output, nSupp, nAutos );
+
+ Cudd_RecursiveDeref( dd, bSpace1 );
+ Cudd_RecursiveDeref( dd, bCanVars );
+ Cudd_RecursiveDeref( dd, bReduced );
+ Cudd_RecursiveDerefZdd( dd, zEquations );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+