summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaDup.c35
-rw-r--r--src/base/abci/abcDsd.c5
-rw-r--r--src/bdd/dsd/dsd.h1
-rw-r--r--src/bdd/dsd/dsdTree.c114
4 files changed, 154 insertions, 1 deletions
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 45c017bb..b54bdee0 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -3006,6 +3006,41 @@ Gia_Man_t * Gia_ManDupDemiter( Gia_Man_t * p, int fVerbose )
return pNew;
}
+/**Function*************************************************************
+
+ Synopsis [Decomposes the miter outputs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupOuts( Gia_Man_t * p )
+{
+ Gia_Man_t * pNew;
+ Gia_Obj_t * pObj;
+ int i;
+ pNew = Gia_ManStart( Gia_ManObjNum(p) );
+ pNew->pName = Abc_UtilStrsav( p->pName );
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ Gia_ManConst0(p)->Value = 0;
+ Gia_ManForEachCi( p, pObj, i )
+ pObj->Value = Gia_ManAppendCi(pNew);
+ Gia_ManForEachAnd( p, pObj, i )
+ pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ Gia_ManForEachPo( p, pObj, i )
+ Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ Gia_ManForEachAnd( p, pObj, i )
+ Gia_ManAppendCo( pNew, pObj->Value );
+ Gia_ManForEachRi( p, pObj, i )
+ Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+ assert( Gia_ManIsNormalized(pNew) );
+ return pNew;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c
index 481639dd..29982468 100644
--- a/src/base/abci/abcDsd.c
+++ b/src/base/abci/abcDsd.c
@@ -137,7 +137,10 @@ Abc_Ntk_t * Abc_NtkDsdInternal( Abc_Ntk_t * pNtk, int fVerbose, int fPrint, int
{
ppNamesCi = Abc_NtkCollectCioNames( pNtk, 0 );
ppNamesCo = Abc_NtkCollectCioNames( pNtk, 1 );
- Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, fShort, -1 );
+ if ( fVerbose )
+ Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, fShort, -1 );
+ else
+ Dsd_TreePrint2( stdout, pManDsd, ppNamesCi, ppNamesCo, -1 );
ABC_FREE( ppNamesCi );
ABC_FREE( ppNamesCo );
}
diff --git a/src/bdd/dsd/dsd.h b/src/bdd/dsd/dsd.h
index 7bb6111f..49fe4552 100644
--- a/src/bdd/dsd/dsd.h
+++ b/src/bdd/dsd/dsd.h
@@ -116,6 +116,7 @@ extern int Dsd_TreeCollectDecomposableVars( Dsd_Manager_t * dMan, in
extern Dsd_Node_t ** Dsd_TreeCollectNodesDfs( Dsd_Manager_t * dMan, int * pnNodes );
extern Dsd_Node_t ** Dsd_TreeCollectNodesDfsOne( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pNode, int * pnNodes );
extern void Dsd_TreePrint( FILE * pFile, Dsd_Manager_t * dMan, char * pInputNames[], char * pOutputNames[], int fShortNames, int Output );
+extern void Dsd_TreePrint2( FILE * pFile, Dsd_Manager_t * dMan, char * pInputNames[], char * pOutputNames[], int Output );
extern void Dsd_NodePrint( FILE * pFile, Dsd_Node_t * pNode );
/*=== dsdLocal.c =======================================================*/
extern DdNode * Dsd_TreeGetPrimeFunction( DdManager * dd, Dsd_Node_t * pNode );
diff --git a/src/bdd/dsd/dsdTree.c b/src/bdd/dsd/dsdTree.c
index e534e00a..35c69ffe 100644
--- a/src/bdd/dsd/dsdTree.c
+++ b/src/bdd/dsd/dsdTree.c
@@ -17,6 +17,7 @@
***********************************************************************/
#include "dsdInt.h"
+#include "misc/util/utilTruth.h"
ABC_NAMESPACE_IMPL_START
@@ -832,6 +833,119 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp
SeeAlso []
***********************************************************************/
+word Dsd_TreeFunc2Truth_rec( DdManager * dd, DdNode * bFunc )
+{
+ word Cof0, Cof1;
+ int Level;
+ if ( bFunc == b0 )
+ return 0;
+ if ( bFunc == b1 )
+ return ~(word)0;
+ if ( Cudd_IsComplement(bFunc) )
+ return ~Dsd_TreeFunc2Truth_rec( dd, Cudd_Not(bFunc) );
+ Level = dd->perm[bFunc->index];
+ assert( Level >= 0 && Level < 6 );
+ Cof0 = Dsd_TreeFunc2Truth_rec( dd, cuddE(bFunc) );
+ Cof1 = Dsd_TreeFunc2Truth_rec( dd, cuddT(bFunc) );
+ return (s_Truths6[Level] & Cof1) | (~s_Truths6[Level] & Cof0);
+}
+void Dsd_TreePrint2_rec( FILE * pFile, DdManager * dd, Dsd_Node_t * pNode, int fComp, char * pInputNames[] )
+{
+ int i;
+ if ( pNode->Type == DSD_NODE_CONST1 )
+ {
+ fprintf( pFile, "Const%d", !fComp );
+ return;
+ }
+ assert( pNode->Type == DSD_NODE_BUF || pNode->Type == DSD_NODE_PRIME || pNode->Type == DSD_NODE_OR || pNode->Type == DSD_NODE_EXOR );
+// fprintf( pFile, "%s", (fComp ^ (pNode->Type == DSD_NODE_OR))? "!" : "" );
+ if ( pNode->Type == DSD_NODE_BUF )
+ {
+ fprintf( pFile, "%s", fComp? "!" : "" );
+ fprintf( pFile, "%s", pInputNames[pNode->S->index] );
+ }
+ else if ( pNode->Type == DSD_NODE_PRIME )
+ {
+ fprintf( pFile, " " );
+ if ( pNode->nDecs <= 6 )
+ {
+ extern unsigned Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPerm );
+ char pCanonPerm[6]; int uCanonPhase;
+ // compute truth table
+ DdNode * bFunc = Dsd_TreeGetPrimeFunction( dd, pNode );
+ word uTruth = Dsd_TreeFunc2Truth_rec( dd, bFunc );
+ Cudd_Ref( bFunc );
+ Cudd_RecursiveDeref( dd, bFunc );
+ // canonicize truth table
+ uCanonPhase = Abc_TtCanonicize( &uTruth, pNode->nDecs, pCanonPerm );
+ fprintf( pFile, "%s", (fComp ^ ((uCanonPhase >> pNode->nDecs) & 1)) ? "!" : "" );
+ Abc_TtPrintHexRev( pFile, &uTruth, pNode->nDecs );
+ fprintf( pFile, "{" );
+ for ( i = 0; i < pNode->nDecs; i++ )
+ {
+ Dsd_Node_t * pInput = pNode->pDecs[(int)pCanonPerm[i]];
+ Dsd_TreePrint2_rec( pFile, dd, Dsd_Regular(pInput), Dsd_IsComplement(pInput) ^ ((uCanonPhase>>i)&1), pInputNames );
+ }
+ fprintf( pFile, "} " );
+ }
+ else
+ {
+ fprintf( pFile, "|%d|", pNode->nDecs );
+ fprintf( pFile, "{" );
+ for ( i = 0; i < pNode->nDecs; i++ )
+ Dsd_TreePrint2_rec( pFile, dd, Dsd_Regular(pNode->pDecs[i]), Dsd_IsComplement(pNode->pDecs[i]), pInputNames );
+ fprintf( pFile, "} " );
+ }
+ }
+ else if ( pNode->Type == DSD_NODE_OR )
+ {
+ fprintf( pFile, "%s", !fComp? "!" : "" );
+ fprintf( pFile, "(" );
+ for ( i = 0; i < pNode->nDecs; i++ )
+ Dsd_TreePrint2_rec( pFile, dd, Dsd_Regular(pNode->pDecs[i]), !Dsd_IsComplement(pNode->pDecs[i]), pInputNames );
+ fprintf( pFile, ")" );
+ }
+ else if ( pNode->Type == DSD_NODE_EXOR )
+ {
+ fprintf( pFile, "%s", fComp? "!" : "" );
+ fprintf( pFile, "[" );
+ for ( i = 0; i < pNode->nDecs; i++ )
+ Dsd_TreePrint2_rec( pFile, dd, Dsd_Regular(pNode->pDecs[i]), Dsd_IsComplement(pNode->pDecs[i]), pInputNames );
+ fprintf( pFile, "]" );
+ }
+}
+void Dsd_TreePrint2( FILE * pFile, Dsd_Manager_t * pDsdMan, char * pInputNames[], char * pOutputNames[], int Output )
+{
+ if ( Output == -1 )
+ {
+ int i;
+ for ( i = 0; i < pDsdMan->nRoots; i++ )
+ {
+ fprintf( pFile, "%8s = ", pOutputNames[i] );
+ Dsd_TreePrint2_rec( pFile, pDsdMan->dd, Dsd_Regular(pDsdMan->pRoots[i]), Dsd_IsComplement(pDsdMan->pRoots[i]), pInputNames );
+ fprintf( pFile, "\n" );
+ }
+ }
+ else
+ {
+ assert( Output >= 0 && Output < pDsdMan->nRoots );
+ fprintf( pFile, "%8s = ", pOutputNames[Output] );
+ Dsd_TreePrint2_rec( pFile, pDsdMan->dd, Dsd_Regular(pDsdMan->pRoots[Output]), Dsd_IsComplement(pDsdMan->pRoots[Output]), pInputNames );
+ fprintf( pFile, "\n" );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints the decompostion tree into file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
void Dsd_NodePrint( FILE * pFile, Dsd_Node_t * pNode )
{
Dsd_Node_t * pNodeR;
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 20:46:43 +0000