diff options
Diffstat (limited to 'src/sop/ft')
| -rw-r--r-- | src/sop/ft/ft.h | 105 | ||||
| -rw-r--r-- | src/sop/ft/ftFactor.c | 842 | ||||
| -rw-r--r-- | src/sop/ft/ftPrint.c | 255 | ||||
| -rw-r--r-- | src/sop/ft/module.make | 2 |
4 files changed, 1204 insertions, 0 deletions
diff --git a/src/sop/ft/ft.h b/src/sop/ft/ft.h new file mode 100644 index 00000000..81e1a2dc --- /dev/null +++ b/src/sop/ft/ft.h @@ -0,0 +1,105 @@ +/**CFile**************************************************************** + + FileName [ft.h] + + PackageName [MVSIS 2.0: Multi-valued logic synthesis system.] + + Synopsis [Data structure for algebraic factoring.] + + Author [MVSIS Group] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - February 1, 2003.] + + Revision [$Id: ft.h,v 1.1 2003/05/22 19:20:04 alanmi Exp $] + +***********************************************************************/ + +#ifndef __FT_H__ +#define __FT_H__ + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// STRUCTURE DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Ft_Node_t_ Ft_Node_t; +struct Ft_Node_t_ +{ + // the first child + unsigned fCompl0 : 1; // complemented attribute + unsigned iFanin0 : 11; // fanin number + // the second child + unsigned fCompl1 : 1; // complemented attribute + unsigned iFanin1 : 11; // fanin number (1-based) + // other info + unsigned fIntern : 1; // marks any node that is not an elementary var + unsigned fConst : 1; // marks the constant 1 function + unsigned fCompl : 1; // marks the complement of topmost node + // printing info + unsigned fNodeOr : 1; // marks the original OR node + unsigned fEdge0 : 1; // marks the original complemented edge + unsigned fEdge1 : 1; // marks the original complemented edge + // some bits are unused +}; + +/* + The factored form of a SOP is an array (Vec_Int_t) of entries Ft_Node_t. + If the SOP has n input variables (some of them may not be in the true support) + the first n entries of the factored form array have 0s. This representation + makes it each to translate the factored form into an AIG. + + The node structure contains fanins of the node and their complemented attributes + (using AIG semantics). The elementary variable (buffer or interver) are + represented as a node with the same fanins. For example: x' = AND( x', x' ). + The constant node cannot be represented. Constant functions should be detected + before calling the factoring procedure. +*/ + +// working with complemented attributes of objects +static inline bool Ptr_IsComplement( void * p ) { return (bool)(((unsigned)p) & 01); } +static inline void * Ptr_Regular( void * p ) { return (void *)((unsigned)(p) & ~01); } +static inline void * Ptr_Not( void * p ) { return (void *)((unsigned)(p) ^ 01); } +static inline void * Ptr_NotCond( void * p, int c ) { return (void *)((unsigned)(p) ^ (c)); } + +static inline Ft_Node_t * Ft_NodeRead( Vec_Int_t * vForm, int i ) { return (Ft_Node_t *)vForm->pArray + i; } +static inline Ft_Node_t * Ft_NodeReadLast( Vec_Int_t * vForm ) { return (Ft_Node_t *)vForm->pArray + vForm->nSize - 1; } +static inline Ft_Node_t * Ft_NodeFanin0( Vec_Int_t * vForm, Ft_Node_t * pNode ) { assert( pNode->fIntern ); return (Ft_Node_t *)vForm->pArray + pNode->iFanin0; } +static inline Ft_Node_t * Ft_NodeFanin1( Vec_Int_t * vForm, Ft_Node_t * pNode ) { assert( pNode->fIntern ); return (Ft_Node_t *)vForm->pArray + pNode->iFanin1; } + +static inline Ft_Node_t Ft_Int2Node( int Num ) { return *((Ft_Node_t *)&Num); } +static inline int Ft_Node2Int( Ft_Node_t Node ) { return *((int *)&Node); } +static inline void Ft_NodeClean( Ft_Node_t * pNode ) { *((int *)pNode) = 0; } + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== ftFactor.c =====================================================*/ +extern void Ft_FactorStartMan(); +extern void Ft_FactorStopMan(); +extern Vec_Int_t * Ft_Factor( char * pSop ); +extern int Ft_FactorGetNumNodes( Vec_Int_t * vForm ); +extern int Ft_FactorGetNumVars( Vec_Int_t * vForm ); +/*=== ftPrint.c =====================================================*/ +extern void Ft_FactorPrint( FILE * pFile, Vec_Int_t * vForm, char * pNamesIn[], char * pNameOut ); + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + +#endif + diff --git a/src/sop/ft/ftFactor.c b/src/sop/ft/ftFactor.c new file mode 100644 index 00000000..04779fe0 --- /dev/null +++ b/src/sop/ft/ftFactor.c @@ -0,0 +1,842 @@ +/**CFile**************************************************************** + + FileName [ftFactor.c] + + PackageName [MVSIS 2.0: Multi-valued logic synthesis system.] + + Synopsis [Procedures for algebraic factoring.] + + Author [MVSIS Group] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - February 1, 2003.] + + Revision [$Id: ftFactor.c,v 1.3 2003/09/01 04:56:43 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "mvc.h" +#include "ft.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// the types of nodes in FFs +enum { FT_NODE_NONE, FT_NODE_AND, FT_NODE_OR, FT_NODE_INV, FT_NODE_LEAF, FT_NODE_0, FT_NODE_1 }; + +static Ft_Node_t * Ft_Factor_rec( Vec_Int_t * vForm, Mvc_Cover_t * pCover ); +static Ft_Node_t * Ft_FactorLF_rec( Vec_Int_t * vForm, Mvc_Cover_t * pCover, Mvc_Cover_t * pSimple ); + +static Ft_Node_t * Ft_FactorTrivial( Vec_Int_t * vForm, Mvc_Cover_t * pCover ); +static Ft_Node_t * Ft_FactorTrivialCube( Vec_Int_t * vForm, Mvc_Cover_t * pCover, Mvc_Cube_t * pCube ); +static Ft_Node_t * Ft_FactorTrivialTree_rec( Vec_Int_t * vForm, Ft_Node_t ** ppNodes, int nNodes, int fAnd ); +static Ft_Node_t * Ft_FactorTrivialCascade( Vec_Int_t * vForm, Mvc_Cover_t * pCover ); +static Ft_Node_t * Ft_FactorTrivialCubeCascade( Vec_Int_t * vForm, Mvc_Cover_t * pCover, Mvc_Cube_t * pCube ); + +static Ft_Node_t * Ft_FactorNodeCreate( Vec_Int_t * vForm, int Type, Ft_Node_t * pNode1, Ft_Node_t * pNode2 ); +static Ft_Node_t * Ft_FactorLeafCreate( Vec_Int_t * vForm, int iLit ); +static void Ft_FactorFinalize( Vec_Int_t * vForm, Ft_Node_t * pNode, int nVars ); +static void Ft_FactorComplement( Vec_Int_t * vForm ); +static Vec_Int_t * Ft_FactorConst( int fConst1 ); + +// temporary procedures that work with the covers +static Mvc_Cover_t * Ft_ConvertSopToMvc( char * pSop ); +static int Ft_FactorVerify( char * pSop, Vec_Int_t * vForm ); + +// temporary managers +static Mvc_Manager_t * pMem = NULL; +static DdManager * dd = NULL; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Factors the cover.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Ft_Factor( char * pSop ) +{ + Vec_Int_t * vForm; + Ft_Node_t * pNode; + Mvc_Cover_t * pCover; + int nVars = Abc_SopGetVarNum( pSop ); + + // derive the cover from the SOP representation + pCover = Ft_ConvertSopToMvc( pSop ); + + // make sure the cover is CCS free (should be done before CST) + Mvc_CoverContain( pCover ); + // check for trivial functions + if ( Mvc_CoverIsEmpty(pCover) ) + { + Mvc_CoverFree( pCover ); + return Ft_FactorConst( 0 ); + } + if ( Mvc_CoverIsTautology(pCover) ) + { + Mvc_CoverFree( pCover ); + return Ft_FactorConst( 1 ); + } + + // perform CST + Mvc_CoverInverse( pCover ); // CST + + // start the factored form + vForm = Vec_IntAlloc( 1000 ); + Vec_IntFill( vForm, nVars, 0 ); + // factor the cover + pNode = Ft_Factor_rec( vForm, pCover ); + // finalize the factored form + Ft_FactorFinalize( vForm, pNode, nVars ); + // check if the cover was originally complented + if ( Abc_SopGetPhase(pSop) == 0 ) + Ft_FactorComplement( vForm ); + + // verify the factored form +// if ( !Ft_FactorVerify( pSop, vForm ) ) +// printf( "Verification has failed.\n" ); + +// Mvc_CoverInverse( pCover ); // undo CST + Mvc_CoverFree( pCover ); + return vForm; +} + +/**Function************************************************************* + + Synopsis [Internal recursive factoring procedure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ft_Node_t * Ft_Factor_rec( Vec_Int_t * vForm, Mvc_Cover_t * pCover ) +{ + Mvc_Cover_t * pDiv, * pQuo, * pRem, * pCom; + Ft_Node_t * pNodeDiv, * pNodeQuo, * pNodeRem; + Ft_Node_t * pNodeAnd, * pNode; + + // make sure the cover contains some cubes + assert( Mvc_CoverReadCubeNum(pCover) ); + + // get the divisor + pDiv = Mvc_CoverDivisor( pCover ); + if ( pDiv == NULL ) + return Ft_FactorTrivial( vForm, pCover ); + + // divide the cover by the divisor + Mvc_CoverDivideInternal( pCover, pDiv, &pQuo, &pRem ); + assert( Mvc_CoverReadCubeNum(pQuo) ); + + Mvc_CoverFree( pDiv ); + Mvc_CoverFree( pRem ); + + // check the trivial case + if ( Mvc_CoverReadCubeNum(pQuo) == 1 ) + { + pNode = Ft_FactorLF_rec( vForm, pCover, pQuo ); + Mvc_CoverFree( pQuo ); + return pNode; + } + + // make the quotient cube free + Mvc_CoverMakeCubeFree( pQuo ); + + // divide the cover by the quotient + Mvc_CoverDivideInternal( pCover, pQuo, &pDiv, &pRem ); + + // check the trivial case + if ( Mvc_CoverIsCubeFree( pDiv ) ) + { + pNodeDiv = Ft_Factor_rec( vForm, pDiv ); + pNodeQuo = Ft_Factor_rec( vForm, pQuo ); + Mvc_CoverFree( pDiv ); + Mvc_CoverFree( pQuo ); + pNodeAnd = Ft_FactorNodeCreate( vForm, FT_NODE_AND, pNodeDiv, pNodeQuo ); + if ( Mvc_CoverReadCubeNum(pRem) == 0 ) + { + Mvc_CoverFree( pRem ); + return pNodeAnd; + } + else + { + pNodeRem = Ft_Factor_rec( vForm, pRem ); + Mvc_CoverFree( pRem ); + return Ft_FactorNodeCreate( vForm, FT_NODE_OR, pNodeAnd, pNodeRem ); + } + } + + // get the common cube + pCom = Mvc_CoverCommonCubeCover( pDiv ); + Mvc_CoverFree( pDiv ); + Mvc_CoverFree( pQuo ); + Mvc_CoverFree( pRem ); + + // solve the simple problem + pNode = Ft_FactorLF_rec( vForm, pCover, pCom ); + Mvc_CoverFree( pCom ); + return pNode; +} + + +/**Function************************************************************* + + Synopsis [Internal recursive factoring procedure for the leaf case.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ft_Node_t * Ft_FactorLF_rec( Vec_Int_t * vForm, Mvc_Cover_t * pCover, Mvc_Cover_t * pSimple ) +{ + Mvc_Cover_t * pDiv, * pQuo, * pRem; + Ft_Node_t * pNodeDiv, * pNodeQuo, * pNodeRem; + Ft_Node_t * pNodeAnd; + + // get the most often occurring literal + pDiv = Mvc_CoverBestLiteralCover( pCover, pSimple ); + // divide the cover by the literal + Mvc_CoverDivideByLiteral( pCover, pDiv, &pQuo, &pRem ); + // get the node pointer for the literal + pNodeDiv = Ft_FactorTrivialCube( vForm, pDiv, Mvc_CoverReadCubeHead(pDiv) ); + Mvc_CoverFree( pDiv ); + // factor the quotient and remainder + pNodeQuo = Ft_Factor_rec( vForm, pQuo ); + Mvc_CoverFree( pQuo ); + pNodeAnd = Ft_FactorNodeCreate( vForm, FT_NODE_AND, pNodeDiv, pNodeQuo ); + if ( Mvc_CoverReadCubeNum(pRem) == 0 ) + { + Mvc_CoverFree( pRem ); + return pNodeAnd; + } + else + { + pNodeRem = Ft_Factor_rec( vForm, pRem ); + Mvc_CoverFree( pRem ); + return Ft_FactorNodeCreate( vForm, FT_NODE_OR, pNodeAnd, pNodeRem ); + } +} + + + +/**Function************************************************************* + + Synopsis [Factoring the cover, which has no algebraic divisors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ft_Node_t * Ft_FactorTrivial( Vec_Int_t * vForm, Mvc_Cover_t * pCover ) +{ + Ft_Node_t ** ppNodes; + Ft_Node_t * pNode; + Mvc_Cube_t * pCube; + int i, nNodes; + + // create space to put the cubes + nNodes = Mvc_CoverReadCubeNum(pCover); + assert( nNodes > 0 ); + ppNodes = ALLOC( Ft_Node_t *, nNodes ); + // create the factored form for each cube + i = 0; + Mvc_CoverForEachCube( pCover, pCube ) + ppNodes[i++] = Ft_FactorTrivialCube( vForm, pCover, pCube ); + assert( i == nNodes ); + // balance the factored forms + pNode = Ft_FactorTrivialTree_rec( vForm, ppNodes, nNodes, 0 ); + free( ppNodes ); + return pNode; +} + +/**Function************************************************************* + + Synopsis [Factoring the cube.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ft_Node_t * Ft_FactorTrivialCube( Vec_Int_t * vForm, Mvc_Cover_t * pCover, Mvc_Cube_t * pCube ) +{ + Ft_Node_t ** ppNodes; + Ft_Node_t * pNode; + int iBit, Value, i; + + // create space to put each literal + ppNodes = ALLOC( Ft_Node_t *, pCover->nBits ); + // create the factored form for each literal + i = 0; + Mvc_CubeForEachBit( pCover, pCube, iBit, Value ) + { + if ( Value ) + ppNodes[i++] = Ft_FactorLeafCreate( vForm, iBit ); + } + assert( i > 0 && i < pCover->nBits ); + // balance the factored forms + pNode = Ft_FactorTrivialTree_rec( vForm, ppNodes, i, 1 ); + free( ppNodes ); + return pNode; +} + +/**Function************************************************************* + + Synopsis [Create the well-balanced tree of nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ft_Node_t * Ft_FactorTrivialTree_rec( Vec_Int_t * vForm, Ft_Node_t ** ppNodes, int nNodes, int fAnd ) +{ + Ft_Node_t * pNode1, * pNode2; + int nNodes1, nNodes2; + + if ( nNodes == 1 ) + return ppNodes[0]; + + // split the nodes into two parts + nNodes1 = nNodes/2; + nNodes2 = nNodes - nNodes1; + + // recursively construct the tree for the parts + pNode1 = Ft_FactorTrivialTree_rec( vForm, ppNodes, nNodes1, fAnd ); + pNode2 = Ft_FactorTrivialTree_rec( vForm, ppNodes + nNodes1, nNodes2, fAnd ); + + return Ft_FactorNodeCreate( vForm, fAnd? FT_NODE_AND : FT_NODE_OR, pNode1, pNode2 ); +} + + + +/**Function************************************************************* + + Synopsis [Factoring the cover, which has no algebraic divisors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ft_Node_t * Ft_FactorTrivialCascade( Vec_Int_t * vForm, Mvc_Cover_t * pCover ) +{ + Ft_Node_t * pNode; + Mvc_Cube_t * pCube; + + // iterate through the cubes + pNode = NULL; + Mvc_CoverForEachCube( pCover, pCube ) + { + if ( pNode == NULL ) + pNode = Ft_FactorTrivialCube( vForm, pCover, pCube ); + else + pNode = Ft_FactorNodeCreate( vForm, FT_NODE_OR, pNode, Ft_FactorTrivialCubeCascade( vForm, pCover, pCube ) ); + } + assert( pNode ); // if this assertion fails, the input cover is not SCC-free + return pNode; +} + +/**Function************************************************************* + + Synopsis [Factoring the cube.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ft_Node_t * Ft_FactorTrivialCubeCascade( Vec_Int_t * vForm, Mvc_Cover_t * pCover, Mvc_Cube_t * pCube ) +{ + Ft_Node_t * pNode; + int iBit, Value; + + // iterate through the literals + pNode = NULL; + Mvc_CubeForEachBit( pCover, pCube, iBit, Value ) + { + if ( Value ) + { + if ( pNode == NULL ) + pNode = Ft_FactorLeafCreate( vForm, iBit ); + else + pNode = Ft_FactorNodeCreate( vForm, FT_NODE_AND, pNode, Ft_FactorLeafCreate( vForm, iBit ) ); + } + } + assert( pNode ); // if this assertion fails, the input cover is not SCC-free + return pNode; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ft_Node_t * Ft_FactorNodeCreate( Vec_Int_t * vForm, int Type, Ft_Node_t * pNode1, Ft_Node_t * pNode2 ) +{ + Ft_Node_t * pNode; + // get the new node + Vec_IntPush( vForm, 0 ); + pNode = Ft_NodeReadLast( vForm ); + // set the inputs and other info + pNode->iFanin0 = (Ft_Node_t *)Ptr_Regular(pNode1) - (Ft_Node_t *)vForm->pArray; + pNode->iFanin1 = (Ft_Node_t *)Ptr_Regular(pNode2) - (Ft_Node_t *)vForm->pArray; + assert( pNode->iFanin0 < (unsigned)vForm->nSize ); + assert( pNode->iFanin1 < (unsigned)vForm->nSize ); + pNode->fIntern = 1; + pNode->fCompl = 0; + pNode->fConst = 0; + pNode->fEdge0 = Ptr_IsComplement(pNode1); + pNode->fEdge1 = Ptr_IsComplement(pNode2); + // consider specific gates + if ( Type == FT_NODE_OR ) + { + pNode->fCompl0 = !Ptr_IsComplement(pNode1); + pNode->fCompl1 = !Ptr_IsComplement(pNode2); + pNode->fNodeOr = 1; + return Ptr_Not( pNode ); + } + if ( Type == FT_NODE_AND ) + { + pNode->fCompl0 = Ptr_IsComplement(pNode1); + pNode->fCompl1 = Ptr_IsComplement(pNode2); + pNode->fNodeOr = 0; + return pNode; + } + assert( 0 ); + return NULL; + +/* + Vec_Int_t * vForm; + assert( pNode1 && pNode2 ); + pNode = MEM_ALLOC( vForm->pMem, void, 1 ); + memset( pNode, 0, sizeof(void) ); + pNode->Type = Type; + pNode->pOne = pNode1; + pNode->pTwo = pNode2; + // update FF statistics + if ( pNode->Type == FT_NODE_LEAF ) + vForm->nNodes++; + return pNode; +*/ +} + +/**Function************************************************************* + + Synopsis [Factoring the cube.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ft_Node_t * Ft_FactorLeafCreate( Vec_Int_t * vForm, int iLit ) +{ + return Ptr_NotCond( Ft_NodeRead(vForm, iLit/2), iLit%2 ); // using CST + +/* + Vm_VarMap_t * pVm; + int * pValuesFirst, * pValues; + int nValuesIn, nVarsIn; + Vec_Int_t * vForm; + int iVar; + pVm = vForm->pVm; + pValues = Vm_VarMapReadValuesArray(pVm); + pValuesFirst = Vm_VarMapReadValuesFirstArray(pVm); + nValuesIn = Vm_VarMapReadValuesInNum(pVm); + nVarsIn = Vm_VarMapReadVarsInNum(pVm); + assert( iLit < nValuesIn ); + for ( iVar = 0; iVar < nVarsIn; iVar++ ) + if ( iLit < pValuesFirst[iVar] + pValues[iVar] ) + break; + assert( iVar < nVarsIn ); + pNode = Ft_FactorNodeCreate( vForm, FT_NODE_LEAF, NULL, NULL ); + pNode->VarNum = iVar; + pNode->nValues = pValues[iVar]; + pNode->uData = FT_MV_MASK(pNode->nValues) ^ (1 << (iLit - pValuesFirst[iVar])); + return pNode; +*/ +} + + +/**Function************************************************************* + + Synopsis [Adds a single-variable literal if necessary.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ft_FactorFinalize( Vec_Int_t * vForm, Ft_Node_t * pRoot, int nVars ) +{ + Ft_Node_t * pRootR = Ptr_Regular(pRoot); + int iNode = pRootR - (Ft_Node_t *)vForm->pArray; + Ft_Node_t * pNode; + if ( iNode >= nVars ) + { + // set the complemented attribute + pRootR->fCompl = Ptr_IsComplement(pRoot); + return; + } + // create a new node + Vec_IntPush( vForm, 0 ); + pNode = Ft_NodeReadLast( vForm ); + pNode->iFanin0 = iNode; + pNode->iFanin1 = iNode; + pNode->fIntern = 1; + pNode->fCompl = Ptr_IsComplement(pRoot); +} + +/**Function************************************************************* + + Synopsis [Computes the number of variables in the factored form.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ft_FactorGetNumVars( Vec_Int_t * vForm ) +{ + int i; + for ( i = 0; i < vForm->nSize; i++ ) + if ( vForm->pArray[i] ) + break; + return i; +} + +/**Function************************************************************* + + Synopsis [Computes the number of variables in the factored form.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ft_FactorGetNumNodes( Vec_Int_t * vForm ) +{ + Ft_Node_t * pNode; + int i; + pNode = Ft_NodeReadLast(vForm); + if ( pNode->fConst ) + return 0; + if ( !pNode->fConst && pNode->iFanin0 == pNode->iFanin1 ) // literal + return 1; + for ( i = 0; i < vForm->nSize; i++ ) + if ( vForm->pArray[i] ) + break; + return vForm->nSize - i + 1; +} + +/**Function************************************************************* + + Synopsis [Complements the factored form.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ft_FactorComplement( Vec_Int_t * vForm ) +{ + Ft_Node_t * pNode; + int nVars = Ft_FactorGetNumVars( vForm ); + assert( nVars >= 0 ); + pNode = Ft_NodeReadLast(vForm); + pNode->fCompl ^= 1; +} + +/**Function************************************************************* + + Synopsis [Creates a constant 0 or 1 factored form.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Ft_FactorConst( int fConst1 ) +{ + Vec_Int_t * vForm; + Ft_Node_t * pNode; + // create the constant node + vForm = Vec_IntAlloc( 1 ); + Vec_IntPush( vForm, 0 ); + pNode = Ft_NodeReadLast( vForm ); + pNode->fIntern = 1; + pNode->fConst = 1; + pNode->fCompl = !fConst1; + return vForm; +} + + + + + + +/**Function************************************************************* + + Synopsis [Start the MVC manager used in the factoring package.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ft_FactorStartMan() +{ + assert( pMem == NULL ); + pMem = Mvc_ManagerStart(); + dd = Cudd_Init( 0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); +} + +/**Function************************************************************* + + Synopsis [Stops the MVC maanager used in the factoring package.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ft_FactorStopMan() +{ + assert( pMem ); + Mvc_ManagerFree( pMem ); + Cudd_Quit( dd ); + pMem = NULL; + dd = NULL; +} + + + + + +/**Function************************************************************* + + Synopsis [Converts SOP into MVC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Mvc_Cover_t * Ft_ConvertSopToMvc( char * pSop ) +{ + Mvc_Cover_t * pMvc; + Mvc_Cube_t * pMvcCube; + char * pCube; + int nVars, Value, v; + + // start the cover + nVars = Abc_SopGetVarNum(pSop); + pMvc = Mvc_CoverAlloc( pMem, nVars * 2 ); + // check the logic function of the node + Abc_SopForEachCube( pSop, nVars, pCube ) + { + // create and add the cube + pMvcCube = Mvc_CubeAlloc( pMvc ); + Mvc_CoverAddCubeTail( pMvc, pMvcCube ); + // fill in the literals + Mvc_CubeBitFill( pMvcCube ); + Abc_CubeForEachVar( pCube, Value, v ) + { + if ( Value == '0' ) + Mvc_CubeBitRemove( pMvcCube, v * 2 + 1 ); + else if ( Value == '1' ) + Mvc_CubeBitRemove( pMvcCube, v * 2 ); + } + } +//Mvc_CoverPrint( pMvc ); + return pMvc; +} + + + +/**Function************************************************************* + + Synopsis [Converts SOP into BDD.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Ft_ConvertSopToBdd( DdManager * dd, char * pSop ) +{ + DdNode * bSum, * bCube, * bTemp, * bVar; + char * pCube; + int nVars, Value, v; + // start the cover + nVars = Abc_SopGetVarNum(pSop); + // check the logic function of the node + bSum = Cudd_ReadLogicZero(dd); Cudd_Ref( bSum ); + Abc_SopForEachCube( pSop, nVars, pCube ) + { + bCube = Cudd_ReadOne(dd); Cudd_Ref( bCube ); + Abc_CubeForEachVar( pCube, Value, v ) + { + if ( Value == '0' ) + bVar = Cudd_Not( Cudd_bddIthVar( dd, v ) ); + else if ( Value == '1' ) + bVar = Cudd_bddIthVar( dd, v ); + else + continue; + bCube = Cudd_bddAnd( dd, bTemp = bCube, bVar ); Cudd_Ref( bCube ); + Cudd_RecursiveDeref( dd, bTemp ); + } + bSum = Cudd_bddOr( dd, bTemp = bSum, bCube ); Cudd_Ref( bSum ); + Cudd_RecursiveDeref( dd, bTemp ); + Cudd_RecursiveDeref( dd, bCube ); + } + // complement the result if necessary + bSum = Cudd_NotCond( bSum, !Abc_SopGetPhase(pSop) ); + Cudd_Deref( bSum ); + return bSum; +} + +/**Function************************************************************* + + Synopsis [Converts SOP into BDD.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Ft_ConvertFormToBdd( DdManager * dd, Vec_Int_t * vForm ) +{ + Vec_Ptr_t * vFuncs; + DdNode * bFunc, * bFunc0, * bFunc1; + Ft_Node_t * pNode; + int i, nVars; + + // sanity checks + nVars = Ft_FactorGetNumVars( vForm ); + assert( nVars >= 0 ); + assert( vForm->nSize > nVars ); + + // check for constant function + pNode = Ft_NodeRead( vForm, 0 ); + if ( pNode->fConst ) + return Cudd_NotCond( dd->one, pNode->fCompl ); + + // start the array of elementary variables + vFuncs = Vec_PtrAlloc( 20 ); + for ( i = 0; i < nVars; i++ ) + Vec_PtrPush( vFuncs, Cudd_bddIthVar(dd, i) ); + + // compute the functions of other nodes + for ( i = nVars; i < vForm->nSize; i++ ) + { + pNode = Ft_NodeRead( vForm, i ); + bFunc0 = Cudd_NotCond( vFuncs->pArray[pNode->iFanin0], pNode->fCompl0 ); + bFunc1 = Cudd_NotCond( vFuncs->pArray[pNode->iFanin1], pNode->fCompl1 ); + bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( bFunc ); + Vec_PtrPush( vFuncs, bFunc ); + } + assert( vForm->nSize = vFuncs->nSize ); + + // deref the intermediate results + for ( i = nVars; i < vForm->nSize-1; i++ ) + Cudd_RecursiveDeref( dd, (DdNode *)vFuncs->pArray[i] ); + Vec_PtrFree( vFuncs ); + + // complement the result if necessary + pNode = Ft_NodeReadLast( vForm ); + bFunc = Cudd_NotCond( bFunc, pNode->fCompl ); + + // return the result + Cudd_Deref( bFunc ); + return bFunc; +} + + +/**Function************************************************************* + + Synopsis [Verifies that the factoring is correct.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ft_FactorVerify( char * pSop, Vec_Int_t * vForm ) +{ + DdNode * bFunc1, * bFunc2; + int RetValue; + bFunc1 = Ft_ConvertSopToBdd( dd, pSop ); Cudd_Ref( bFunc1 ); + bFunc2 = Ft_ConvertFormToBdd( dd, vForm ); Cudd_Ref( bFunc2 ); +//Extra_bddPrint( dd, bFunc1 ); printf("\n"); +//Extra_bddPrint( dd, bFunc2 ); printf("\n"); + RetValue = (bFunc1 == bFunc2); + Cudd_RecursiveDeref( dd, bFunc1 ); + Cudd_RecursiveDeref( dd, bFunc2 ); + return RetValue; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sop/ft/ftPrint.c b/src/sop/ft/ftPrint.c new file mode 100644 index 00000000..e08ceaae --- /dev/null +++ b/src/sop/ft/ftPrint.c @@ -0,0 +1,255 @@ +/**CFile**************************************************************** + + FileName [ftPrint.c] + + PackageName [MVSIS 2.0: Multi-valued logic synthesis system.] + + Synopsis [Procedures to print the factored tree.] + + Author [MVSIS Group] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - February 1, 2003.] + + Revision [$Id: ftPrint.c,v 1.1 2003/05/22 19:20:05 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "ft.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Ft_FactorPrint_rec( FILE * pFile, Vec_Int_t * vForm, Ft_Node_t * pNode, int fCompl, char * pNamesIn[], int * pPos, int LitSizeMax ); +static int Ft_FactorPrintGetLeafName( FILE * pFile, Vec_Int_t * vForm, Ft_Node_t * pNode, int fCompl, char * pNamesIn[] ); +static void Ft_FactorPrintUpdatePos( FILE * pFile, int * pPos, int LitSizeMax ); +static int Ft_FactorPrintOutputName( FILE * pFile, char * pNameOut, int fCompl ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ft_FactorPrint( FILE * pFile, Vec_Int_t * vForm, char * pNamesIn[], char * pNameOut ) +{ + Ft_Node_t * pNode; + char Buffer[5]; + int Pos, i, LitSizeMax, LitSizeCur, nVars; + int fMadeupNames; + + // sanity checks + nVars = Ft_FactorGetNumVars( vForm ); + assert( nVars >= 0 ); + assert( vForm->nSize > nVars ); + + // create the names if not given by the user + fMadeupNames = 0; + if ( pNamesIn == NULL ) + { + fMadeupNames = 1; + pNamesIn = ALLOC( char *, nVars ); + for ( i = 0; i < nVars; i++ ) + { + if ( nVars < 26 ) + { + Buffer[0] = 'a' + i; + Buffer[1] = 0; + } + else + { + Buffer[0] = 'a' + i%26; + Buffer[1] = '0' + i/26; + Buffer[2] = 0; + } + pNamesIn[i] = util_strsav( Buffer ); + } + } + + // get the size of the longest literal + LitSizeMax = 0; + for ( i = 0; i < nVars; i++ ) + { + LitSizeCur = strlen(pNamesIn[i]); + if ( LitSizeMax < LitSizeCur ) + LitSizeMax = LitSizeCur; + } + if ( LitSizeMax > 50 ) + LitSizeMax = 20; + + // print the output name + pNode = Ft_NodeReadLast(vForm); + if ( !pNode->fConst && pNode->iFanin0 == pNode->iFanin1 ) // literal + { + Pos = Ft_FactorPrintOutputName( pFile, pNameOut, 0 ); + Ft_FactorPrintGetLeafName( pFile, vForm, Ft_NodeFanin0(vForm,pNode), pNode->fCompl, pNamesIn ); + } + else // constant or non-trivial form + { + Pos = Ft_FactorPrintOutputName( pFile, pNameOut, pNode->fCompl ); + Ft_FactorPrint_rec( pFile, vForm, pNode, 0, pNamesIn, &Pos, LitSizeMax ); + } + fprintf( pFile, "\n" ); + + if ( fMadeupNames ) + { + for ( i = 0; i < nVars; i++ ) + free( pNamesIn[i] ); + free( pNamesIn ); + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ft_FactorPrint_rec( FILE * pFile, Vec_Int_t * vForm, Ft_Node_t * pNode, int fCompl, char * pNamesIn[], int * pPos, int LitSizeMax ) +{ + Ft_Node_t * pNode0, * pNode1; + + if ( pNode->fConst ) // FT_NODE_0 ) + { + if ( fCompl ) + fprintf( pFile, "Constant 0" ); + else + fprintf( pFile, "Constant 1" ); + return; + } + if ( !pNode->fIntern ) // FT_NODE_LEAF ) + { + (*pPos) += Ft_FactorPrintGetLeafName( pFile, vForm, pNode, fCompl, pNamesIn ); + return; + } + + pNode0 = Ft_NodeFanin0( vForm, pNode ); + pNode1 = Ft_NodeFanin1( vForm, pNode ); + if ( !pNode->fNodeOr ) // FT_NODE_AND ) + { + if ( !pNode0->fNodeOr ) // != FT_NODE_OR ) + Ft_FactorPrint_rec( pFile, vForm, pNode0, pNode->fEdge0, pNamesIn, pPos, LitSizeMax ); + else + { + fprintf( pFile, "(" ); + (*pPos)++; + Ft_FactorPrint_rec( pFile, vForm, pNode0, pNode->fEdge0, pNamesIn, pPos, LitSizeMax ); + fprintf( pFile, ")" ); + (*pPos)++; + } + fprintf( pFile, " " ); + (*pPos)++; + + Ft_FactorPrintUpdatePos( pFile, pPos, LitSizeMax ); + + if ( !pNode1->fNodeOr ) // != FT_NODE_OR ) + Ft_FactorPrint_rec( pFile, vForm, pNode1, pNode->fEdge1, pNamesIn, pPos, LitSizeMax ); + else + { + fprintf( pFile, "(" ); + (*pPos)++; + Ft_FactorPrint_rec( pFile, vForm, pNode1, pNode->fEdge1, pNamesIn, pPos, LitSizeMax ); + fprintf( pFile, ")" ); + (*pPos)++; + } + return; + } + if ( pNode->fNodeOr ) // FT_NODE_OR ) + { + Ft_FactorPrint_rec( pFile, vForm, pNode0, pNode->fEdge0, pNamesIn, pPos, LitSizeMax ); + fprintf( pFile, " + " ); + (*pPos) += 3; + + Ft_FactorPrintUpdatePos( pFile, pPos, LitSizeMax ); + + Ft_FactorPrint_rec( pFile, vForm, pNode1, pNode->fEdge1, pNamesIn, pPos, LitSizeMax ); + return; + } + assert( 0 ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ft_FactorPrintGetLeafName( FILE * pFile, Vec_Int_t * vForm, Ft_Node_t * pNode, int fCompl, char * pNamesIn[] ) +{ + static char Buffer[100]; + int iVar; + assert( !Ptr_IsComplement(pNode) ); + iVar = (Ft_Node_t *)pNode - (Ft_Node_t *)vForm->pArray; + sprintf( Buffer, "%s%s", pNamesIn[iVar], fCompl? "\'" : "" ); + fprintf( pFile, "%s", Buffer ); + return strlen( Buffer ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ft_FactorPrintUpdatePos( FILE * pFile, int * pPos, int LitSizeMax ) +{ + int i; + if ( *pPos + LitSizeMax < 77 ) + return; + fprintf( pFile, "\n" ); + for ( i = 0; i < 10; i++ ) + fprintf( pFile, " " ); + *pPos = 10; +} + +/**Function************************************************************* + + Synopsis [Starts the printout for a factored form or cover.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ft_FactorPrintOutputName( FILE * pFile, char * pNameOut, int fCompl ) +{ + if ( pNameOut == NULL ) + return 0; + fprintf( pFile, "%6s%s = ", pNameOut, fCompl? "\'" : " " ); + return 10; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sop/ft/module.make b/src/sop/ft/module.make new file mode 100644 index 00000000..37e78ce6 --- /dev/null +++ b/src/sop/ft/module.make @@ -0,0 +1,2 @@ +SRC += src/sop/ft/ftFactor.c \ + src/sop/ft/ftPrint.c |