mirror of https://github.com/YosysHQ/abc.git
1614 lines
63 KiB
C
1614 lines
63 KiB
C
/**CFile****************************************************************
|
|
|
|
FileName [dsdProc.c]
|
|
|
|
PackageName [DSD: Disjoint-support decomposition package.]
|
|
|
|
Synopsis [The core procedures of the package.]
|
|
|
|
Author [Alan Mishchenko]
|
|
|
|
Affiliation [UC Berkeley]
|
|
|
|
Date [Ver. 8.0. Started - September 22, 2003.]
|
|
|
|
Revision [$Id: dsdProc.c,v 1.0 2002/22/09 00:00:00 alanmi Exp $]
|
|
|
|
***********************************************************************/
|
|
|
|
#include "dsdInt.h"
|
|
|
|
ABC_NAMESPACE_IMPL_START
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// FUNCTION DECLARATIONS ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
// the most important procedures
|
|
void dsdKernelDecompose( Dsd_Manager_t * pDsdMan, DdNode ** pbFuncs, int nFuncs );
|
|
static Dsd_Node_t * dsdKernelDecompose_rec( Dsd_Manager_t * pDsdMan, DdNode * F );
|
|
|
|
// additional procedures
|
|
static Dsd_Node_t * dsdKernelFindContainingComponent( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pWhere, DdNode * Var, int * fPolarity );
|
|
static int dsdKernelFindCommonComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd_Node_t * pH, Dsd_Node_t *** pCommon, Dsd_Node_t ** pLastDiffL, Dsd_Node_t ** pLastDiffH );
|
|
static void dsdKernelComputeSumOfComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t ** pCommon, int nCommon, DdNode ** pCompF, DdNode ** pCompS, int fExor );
|
|
static int dsdKernelCheckContainment( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd_Node_t * pH, Dsd_Node_t ** pLarge, Dsd_Node_t ** pSmall );
|
|
|
|
// list copying
|
|
static void dsdKernelCopyListPlusOne( Dsd_Node_t * p, Dsd_Node_t * First, Dsd_Node_t ** ppList, int nListSize );
|
|
static void dsdKernelCopyListPlusOneMinusOne( Dsd_Node_t * p, Dsd_Node_t * First, Dsd_Node_t ** ppList, int nListSize, int Skipped );
|
|
|
|
// debugging procedures
|
|
static int dsdKernelVerifyDecomposition( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pDE );
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// STATIC VARIABLES ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
// the counter of marks
|
|
static int s_Mark;
|
|
|
|
// debugging flag
|
|
//static int s_Show = 0;
|
|
// temporary var used for debugging
|
|
static int Depth = 0;
|
|
|
|
static int s_Loops1;
|
|
static int s_Loops2;
|
|
static int s_Loops3;
|
|
static int s_Common;
|
|
static int s_CommonNo;
|
|
|
|
static int s_Case4Calls;
|
|
static int s_Case4CallsSpecial;
|
|
|
|
//static int s_Case5;
|
|
//static int s_Loops2Useless;
|
|
|
|
// statistical variables
|
|
static int s_nDecBlocks;
|
|
static int s_nLiterals;
|
|
static int s_nExorGates;
|
|
static int s_nReusedBlocks;
|
|
static int s_nCascades;
|
|
static int s_nPrimeBlocks;
|
|
|
|
static int HashSuccess = 0;
|
|
static int HashFailure = 0;
|
|
|
|
static int s_CacheEntries;
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// DECOMPOSITION FUNCTIONS ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Performs DSD for the array of functions represented by BDDs.]
|
|
|
|
Description [This function takes the DSD manager, which should be
|
|
previously allocated by the call to Dsd_ManagerStart(). The resulting
|
|
DSD tree is stored in the DSD manager (pDsdMan->pRoots, pDsdMan->nRoots).
|
|
Access to the tree is through the APIs of the manager. The resulting
|
|
tree is a shared DSD DAG for the functions given in the array. For one
|
|
function the resulting DAG is always a tree. The root node pointers can
|
|
be complemented, as discussed in the literature referred to in "dsd.h".
|
|
This procedure can be called repeatedly for different functions. There is
|
|
no need to remove the decomposition tree after it is returned, because
|
|
the next call to the DSD manager will "recycle" the tree. The user should
|
|
not modify or dereference any data associated with the nodes of the
|
|
DSD trees (the user can only change the contents of a temporary
|
|
mark associated with each node by the calling to Dsd_NodeSetMark()).
|
|
All the decomposition trees and intermediate nodes will be removed when
|
|
the DSD manager is deallocated at the end by calling Dsd_ManagerStop().]
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
void Dsd_Decompose( Dsd_Manager_t * pDsdMan, DdNode ** pbFuncs, int nFuncs )
|
|
{
|
|
DdManager * dd = pDsdMan->dd;
|
|
int i;
|
|
abctime clk;
|
|
Dsd_Node_t * pTemp;
|
|
int SumMaxGateSize = 0;
|
|
int nDecOutputs = 0;
|
|
int nCBFOutputs = 0;
|
|
/*
|
|
s_Loops1 = 0;
|
|
s_Loops2 = 0;
|
|
s_Loops3 = 0;
|
|
s_Case4Calls = 0;
|
|
s_Case4CallsSpecial = 0;
|
|
s_Case5 = 0;
|
|
s_Loops2Useless = 0;
|
|
*/
|
|
// resize the number of roots in the manager
|
|
if ( pDsdMan->nRootsAlloc < nFuncs )
|
|
{
|
|
if ( pDsdMan->nRootsAlloc > 0 )
|
|
ABC_FREE( pDsdMan->pRoots );
|
|
pDsdMan->nRootsAlloc = nFuncs;
|
|
pDsdMan->pRoots = (Dsd_Node_t **) ABC_ALLOC( char, pDsdMan->nRootsAlloc * sizeof(Dsd_Node_t *) );
|
|
}
|
|
|
|
if ( pDsdMan->fVerbose )
|
|
printf( "\nDecomposability statistics for individual outputs:\n" );
|
|
|
|
// set the counter of decomposition nodes
|
|
s_nDecBlocks = 0;
|
|
|
|
// perform decomposition for all outputs
|
|
clk = Abc_Clock();
|
|
pDsdMan->nRoots = 0;
|
|
s_nCascades = 0;
|
|
for ( i = 0; i < nFuncs; i++ )
|
|
{
|
|
int nLiteralsPrev;
|
|
int nDecBlocksPrev;
|
|
int nExorGatesPrev;
|
|
int nReusedBlocksPres;
|
|
int nCascades;
|
|
int MaxBlock;
|
|
int nPrimeBlocks;
|
|
abctime clk;
|
|
|
|
clk = Abc_Clock();
|
|
nLiteralsPrev = s_nLiterals;
|
|
nDecBlocksPrev = s_nDecBlocks;
|
|
nExorGatesPrev = s_nExorGates;
|
|
nReusedBlocksPres = s_nReusedBlocks;
|
|
nPrimeBlocks = s_nPrimeBlocks;
|
|
|
|
pDsdMan->pRoots[ pDsdMan->nRoots++ ] = dsdKernelDecompose_rec( pDsdMan, pbFuncs[i] );
|
|
|
|
Dsd_TreeNodeGetInfoOne( pDsdMan->pRoots[i], &nCascades, &MaxBlock );
|
|
s_nCascades = ddMax( s_nCascades, nCascades );
|
|
pTemp = Dsd_Regular(pDsdMan->pRoots[i]);
|
|
if ( pTemp->Type != DSD_NODE_PRIME || pTemp->nDecs != Extra_bddSuppSize(dd,pTemp->S) )
|
|
nDecOutputs++;
|
|
if ( MaxBlock < 3 )
|
|
nCBFOutputs++;
|
|
SumMaxGateSize += MaxBlock;
|
|
|
|
if ( pDsdMan->fVerbose )
|
|
{
|
|
printf("#%02d: ", i );
|
|
printf("Ins=%2d. ", Cudd_SupportSize(dd,pbFuncs[i]) );
|
|
printf("Gts=%3d. ", Dsd_TreeCountNonTerminalNodesOne( pDsdMan->pRoots[i] ) );
|
|
printf("Pri=%3d. ", Dsd_TreeCountPrimeNodesOne( pDsdMan->pRoots[i] ) );
|
|
printf("Max=%3d. ", MaxBlock );
|
|
printf("Reuse=%2d. ", s_nReusedBlocks-nReusedBlocksPres );
|
|
printf("Csc=%2d. ", nCascades );
|
|
printf("T= %.2f s. ", (float)(Abc_Clock()-clk)/(float)(CLOCKS_PER_SEC) ) ;
|
|
printf("Bdd=%2d. ", Cudd_DagSize(pbFuncs[i]) );
|
|
printf("\n");
|
|
fflush( stdout );
|
|
}
|
|
}
|
|
assert( pDsdMan->nRoots == nFuncs );
|
|
|
|
if ( pDsdMan->fVerbose )
|
|
{
|
|
printf( "\n" );
|
|
printf( "The cumulative decomposability statistics:\n" );
|
|
printf( " Total outputs = %5d\n", nFuncs );
|
|
printf( " Decomposable outputs = %5d\n", nDecOutputs );
|
|
printf( " Completely decomposable outputs = %5d\n", nCBFOutputs );
|
|
printf( " The sum of max gate sizes = %5d\n", SumMaxGateSize );
|
|
printf( " Shared BDD size = %5d\n", Cudd_SharingSize( pbFuncs, nFuncs ) );
|
|
printf( " Decomposition entries = %5d\n", st__count( pDsdMan->Table ) );
|
|
printf( " Pure decomposition time = %.2f sec\n", (float)(Abc_Clock() - clk)/(float)(CLOCKS_PER_SEC) );
|
|
}
|
|
/*
|
|
printf( "s_Loops1 = %d.\n", s_Loops1 );
|
|
printf( "s_Loops2 = %d.\n", s_Loops2 );
|
|
printf( "s_Loops3 = %d.\n", s_Loops3 );
|
|
printf( "s_Case4Calls = %d.\n", s_Case4Calls );
|
|
printf( "s_Case4CallsSpecial = %d.\n", s_Case4CallsSpecial );
|
|
printf( "s_Case5 = %d.\n", s_Case5 );
|
|
printf( "s_Loops2Useless = %d.\n", s_Loops2Useless );
|
|
*/
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Performs decomposition for one function.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
Dsd_Node_t * Dsd_DecomposeOne( Dsd_Manager_t * pDsdMan, DdNode * bFunc )
|
|
{
|
|
return dsdKernelDecompose_rec( pDsdMan, bFunc );
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [The main function of this module. Recursive implementation of DSD.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
Dsd_Node_t * dsdKernelDecompose_rec( Dsd_Manager_t * pDsdMan, DdNode * bFunc0 )
|
|
{
|
|
DdManager * dd = pDsdMan->dd;
|
|
DdNode * bLow;
|
|
DdNode * bLowR;
|
|
DdNode * bHigh;
|
|
|
|
int VarInt;
|
|
DdNode * bVarCur;
|
|
Dsd_Node_t * pVarCurDE;
|
|
// works only if var indices start from 0!!!
|
|
DdNode * bSuppNew = NULL, * bTemp;
|
|
|
|
int fContained;
|
|
int nSuppLH;
|
|
int nSuppL;
|
|
int nSuppH;
|
|
|
|
|
|
|
|
// various decomposition nodes
|
|
Dsd_Node_t * pThis, * pL, * pH, * pLR, * pHR;
|
|
|
|
Dsd_Node_t * pSmallR, * pLargeR;
|
|
Dsd_Node_t * pTableEntry;
|
|
|
|
|
|
// treat the complemented case
|
|
DdNode * bF = Cudd_Regular(bFunc0);
|
|
int fCompF = (int)(bF != bFunc0);
|
|
|
|
// check cache
|
|
if ( st__lookup( pDsdMan->Table, (char*)bF, (char**)&pTableEntry ) )
|
|
{ // the entry is present
|
|
HashSuccess++;
|
|
return Dsd_NotCond( pTableEntry, fCompF );
|
|
}
|
|
HashFailure++;
|
|
Depth++;
|
|
|
|
// proceed to consider "four cases"
|
|
//////////////////////////////////////////////////////////////////////
|
|
// TERMINAL CASES - CASES 1 and 2
|
|
//////////////////////////////////////////////////////////////////////
|
|
bLow = cuddE(bF);
|
|
bLowR = Cudd_Regular(bLow);
|
|
bHigh = cuddT(bF);
|
|
VarInt = bF->index;
|
|
bVarCur = dd->vars[VarInt];
|
|
pVarCurDE = pDsdMan->pInputs[VarInt];
|
|
// works only if var indices start from 0!!!
|
|
bSuppNew = NULL;
|
|
|
|
if ( bLowR->index == CUDD_CONST_INDEX || bHigh->index == CUDD_CONST_INDEX )
|
|
{ // one of the cofactors in the constant
|
|
if ( bHigh == b1 ) // bHigh cannot be equal to b0, because then it will be complemented
|
|
if ( bLow == b0 ) // bLow cannot be equal to b1, because then the node will have bLow == bHigh
|
|
/////////////////////////////////////////////////////////////////
|
|
// bLow == 0, bHigh == 1, F = x'&0 + x&1 = x
|
|
/////////////////////////////////////////////////////////////////
|
|
{ // create the elementary variable node
|
|
assert(0); // should be already in the hash table
|
|
pThis = Dsd_TreeNodeCreate( DSD_NODE_BUF, 1, s_nDecBlocks++ );
|
|
pThis->pDecs[0] = NULL;
|
|
}
|
|
else // if ( bLow != constant )
|
|
/////////////////////////////////////////////////////////////////
|
|
// bLow != const, bHigh == 1, F = x'&bLow + x&1 = bLow + x --- DSD_NODE_OR(x,bLow)
|
|
/////////////////////////////////////////////////////////////////
|
|
{
|
|
pL = dsdKernelDecompose_rec( pDsdMan, bLow );
|
|
pLR = Dsd_Regular( pL );
|
|
bSuppNew = Cudd_bddAnd( dd, bVarCur, pLR->S ); Cudd_Ref(bSuppNew);
|
|
if ( pLR->Type == DSD_NODE_OR && pL == pLR ) // OR and no complement
|
|
{ // add to the components
|
|
pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, pL->nDecs+1, s_nDecBlocks++ );
|
|
dsdKernelCopyListPlusOne( pThis, pVarCurDE, pL->pDecs, pL->nDecs );
|
|
}
|
|
else // all other cases
|
|
{ // create a new 2-input OR-gate
|
|
pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, 2, s_nDecBlocks++ );
|
|
dsdKernelCopyListPlusOne( pThis, pVarCurDE, &pL, 1 );
|
|
}
|
|
}
|
|
else // if ( bHigh != const ) // meaning that bLow should be a constant
|
|
{
|
|
pH = dsdKernelDecompose_rec( pDsdMan, bHigh );
|
|
pHR = Dsd_Regular( pH );
|
|
bSuppNew = Cudd_bddAnd( dd, bVarCur, pHR->S ); Cudd_Ref(bSuppNew);
|
|
if ( bLow == b0 )
|
|
/////////////////////////////////////////////////////////////////
|
|
// Low == 0, High != 1, F = x'&0+x&High = (x'+High')'--- NOR(x',High')
|
|
/////////////////////////////////////////////////////////////////
|
|
if ( pHR->Type == DSD_NODE_OR && pH != pHR ) // DSD_NODE_OR and complement
|
|
{ // add to the components
|
|
pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, pHR->nDecs+1, s_nDecBlocks++ );
|
|
dsdKernelCopyListPlusOne( pThis, Dsd_Not(pVarCurDE), pHR->pDecs, pHR->nDecs );
|
|
pThis = Dsd_Not(pThis);
|
|
}
|
|
else // all other cases
|
|
{ // create a new 2-input NOR gate
|
|
pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, 2, s_nDecBlocks++ );
|
|
pH = Dsd_Not(pH);
|
|
dsdKernelCopyListPlusOne( pThis, Dsd_Not(pVarCurDE), &pH, 1 );
|
|
pThis = Dsd_Not(pThis);
|
|
}
|
|
else // if ( bLow == b1 )
|
|
/////////////////////////////////////////////////////////////////
|
|
// Low == 1, High != 1, F = x'&1 + x&High = x' + High --- DSD_NODE_OR(x',High)
|
|
/////////////////////////////////////////////////////////////////
|
|
if ( pHR->Type == DSD_NODE_OR && pH == pHR ) // OR and no complement
|
|
{ // add to the components
|
|
pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, pH->nDecs+1, s_nDecBlocks++ );
|
|
dsdKernelCopyListPlusOne( pThis, Dsd_Not(pVarCurDE), pH->pDecs, pH->nDecs );
|
|
}
|
|
else // all other cases
|
|
{ // create a new 2-input OR-gate
|
|
pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, 2, s_nDecBlocks++ );
|
|
dsdKernelCopyListPlusOne( pThis, Dsd_Not(pVarCurDE), &pH, 1 );
|
|
}
|
|
}
|
|
goto EXIT;
|
|
}
|
|
// else if ( bLow != const && bHigh != const )
|
|
|
|
// the case of equal cofactors (up to complementation)
|
|
if ( bLowR == bHigh )
|
|
/////////////////////////////////////////////////////////////////
|
|
// Low == G, High == G', F = x'&G + x&G' = (x(+)G) --- EXOR(x,Low)
|
|
/////////////////////////////////////////////////////////////////
|
|
{
|
|
pL = dsdKernelDecompose_rec( pDsdMan, bLow );
|
|
pLR = Dsd_Regular( pL );
|
|
bSuppNew = Cudd_bddAnd( dd, bVarCur, pLR->S ); Cudd_Ref(bSuppNew);
|
|
if ( pLR->Type == DSD_NODE_EXOR ) // complemented or not - does not matter!
|
|
{ // add to the components
|
|
pThis = Dsd_TreeNodeCreate( DSD_NODE_EXOR, pLR->nDecs+1, s_nDecBlocks++ );
|
|
dsdKernelCopyListPlusOne( pThis, pVarCurDE, pLR->pDecs, pLR->nDecs );
|
|
if ( pL != pLR )
|
|
pThis = Dsd_Not( pThis );
|
|
}
|
|
else // all other cases
|
|
{ // create a new 2-input EXOR-gate
|
|
pThis = Dsd_TreeNodeCreate( DSD_NODE_EXOR, 2, s_nDecBlocks++ );
|
|
if ( pL != pLR ) // complemented
|
|
{
|
|
dsdKernelCopyListPlusOne( pThis, pVarCurDE, &pLR, 1 );
|
|
pThis = Dsd_Not( pThis );
|
|
}
|
|
else // non-complemented
|
|
dsdKernelCopyListPlusOne( pThis, pVarCurDE, &pL, 1 );
|
|
}
|
|
goto EXIT;
|
|
}
|
|
|
|
//////////////////////////////////////////////////////////////////////
|
|
// solve subproblems
|
|
//////////////////////////////////////////////////////////////////////
|
|
pL = dsdKernelDecompose_rec( pDsdMan, bLow );
|
|
pH = dsdKernelDecompose_rec( pDsdMan, bHigh );
|
|
pLR = Dsd_Regular( pL );
|
|
pHR = Dsd_Regular( pH );
|
|
|
|
assert( pLR->Type == DSD_NODE_BUF || pLR->Type == DSD_NODE_OR || pLR->Type == DSD_NODE_EXOR || pLR->Type == DSD_NODE_PRIME );
|
|
assert( pHR->Type == DSD_NODE_BUF || pHR->Type == DSD_NODE_OR || pHR->Type == DSD_NODE_EXOR || pHR->Type == DSD_NODE_PRIME );
|
|
|
|
/*
|
|
if ( Depth == 1 )
|
|
{
|
|
// PRK(bLow,pDecTreeTotal->nInputs);
|
|
// PRK(bHigh,pDecTreeTotal->nInputs);
|
|
if ( s_Show )
|
|
{
|
|
PRD( pL );
|
|
PRD( pH );
|
|
}
|
|
}
|
|
*/
|
|
// compute the new support
|
|
bTemp = Cudd_bddAnd( dd, pLR->S, pHR->S ); Cudd_Ref( bTemp );
|
|
nSuppL = Extra_bddSuppSize( dd, pLR->S );
|
|
nSuppH = Extra_bddSuppSize( dd, pHR->S );
|
|
nSuppLH = Extra_bddSuppSize( dd, bTemp );
|
|
bSuppNew = Cudd_bddAnd( dd, bTemp, bVarCur ); Cudd_Ref( bSuppNew );
|
|
Cudd_RecursiveDeref( dd, bTemp );
|
|
|
|
|
|
// several possibilities are possible
|
|
// (1) support of one component contains another
|
|
// (2) none of the supports is contained in another
|
|
fContained = dsdKernelCheckContainment( pDsdMan, pLR, pHR, &pLargeR, &pSmallR );
|
|
|
|
//////////////////////////////////////////////////////////////////////
|
|
// CASE 3.b One of the cofactors in a constant (OR and EXOR)
|
|
//////////////////////////////////////////////////////////////////////
|
|
// the support of the larger component should contain the support of the smaller
|
|
// it is possible to have PRIME function in this role
|
|
// for example: F = ITE( a+b, c(+)d, e+f ), F0 = ITE( b, c(+)d, e+f ), F1 = c(+)d
|
|
if ( fContained )
|
|
{
|
|
Dsd_Node_t * pSmall, * pLarge;
|
|
int c, iCompLarge = -1; // the number of the component is Large is equal to the whole of Small; suppress "might be used uninitialized"
|
|
int fLowIsLarge;
|
|
|
|
DdNode * bFTemp; // the changed input function
|
|
Dsd_Node_t * pDETemp, * pDENew;
|
|
|
|
Dsd_Node_t * pComp = NULL;
|
|
int nComp = -1; // Suppress "might be used uninitialized"
|
|
|
|
if ( pSmallR == pLR )
|
|
{ // Low is Small => High is Large
|
|
pSmall = pL;
|
|
pLarge = pH;
|
|
fLowIsLarge = 0;
|
|
}
|
|
else
|
|
{ // vice versa
|
|
pSmall = pH;
|
|
pLarge = pL;
|
|
fLowIsLarge = 1;
|
|
}
|
|
|
|
// treat the situation when the larger is PRIME
|
|
if ( pLargeR->Type == DSD_NODE_PRIME ) //&& pLargeR->nDecs != pSmallR->nDecs )
|
|
{
|
|
// QUESTION: Is it possible for pLargeR->nDecs > 3
|
|
// and pSmall contained as one of input in pLarge?
|
|
// Yes, for example F = a'c + a & MUX(b,c',d) = a'c + abc' + ab'd is non-decomposable
|
|
// Consider the function H(a->xy) = F( xy, b, c, d )
|
|
// H0 = H(x=0) = F(0,b,c,d) = c
|
|
// H1 = F(x=1) = F(y,b,c,d) - non-decomposable
|
|
//
|
|
// QUESTION: Is it possible that pLarge is PRIME(3) and pSmall is OR(2),
|
|
// which is not contained in PRIME as one input?
|
|
// Yes, for example F = abcd + b'c'd' + a'c'd' = PRIME(ab, c, d)
|
|
// F(a=0) = c'd' = NOT(OR(a,d)) F(a=1) = bcd + b'c'd' = PRIME(b,c,d)
|
|
// To find decomposition, we have to prove that F(a=1)|b=0 = F(a=0)
|
|
|
|
// Is it possible that (pLargeR->nDecs == pSmallR->nDecs) and yet this case holds?
|
|
// Yes, consider the function such that F(a=0) = PRIME(a,b+c,d,e) and F(a=1) = OR(b,c,d,e)
|
|
// They have the same number of inputs and it is possible that they will be the cofactors
|
|
// as discribed in the previous example.
|
|
|
|
// find the component, which when substituted for 0 or 1, produces the desired result
|
|
int g, fFoundComp = -1; // {0,1} depending on whether setting cofactor to 0 or 1 worked out; suppress "might be used uninitialized"
|
|
|
|
DdNode * bLarge, * bSmall;
|
|
if ( fLowIsLarge )
|
|
{
|
|
bLarge = bLow;
|
|
bSmall = bHigh;
|
|
}
|
|
else
|
|
{
|
|
bLarge = bHigh;
|
|
bSmall = bLow;
|
|
}
|
|
|
|
for ( g = 0; g < pLargeR->nDecs; g++ )
|
|
// if ( g != c )
|
|
{
|
|
pDETemp = pLargeR->pDecs[g]; // cannot be complemented
|
|
if ( Dsd_CheckRootFunctionIdentity( dd, bLarge, bSmall, pDETemp->G, b1 ) )
|
|
{
|
|
fFoundComp = 1;
|
|
break;
|
|
}
|
|
|
|
s_Loops1++;
|
|
|
|
if ( Dsd_CheckRootFunctionIdentity( dd, bLarge, bSmall, Cudd_Not(pDETemp->G), b1 ) )
|
|
{
|
|
fFoundComp = 0;
|
|
break;
|
|
}
|
|
|
|
s_Loops1++;
|
|
}
|
|
|
|
if ( g != pLargeR->nDecs )
|
|
{ // decomposition is found
|
|
if ( fFoundComp )
|
|
if ( fLowIsLarge )
|
|
bFTemp = Cudd_bddOr( dd, bVarCur, pLargeR->pDecs[g]->G );
|
|
else
|
|
bFTemp = Cudd_bddOr( dd, Cudd_Not(bVarCur), pLargeR->pDecs[g]->G );
|
|
else
|
|
if ( fLowIsLarge )
|
|
bFTemp = Cudd_bddAnd( dd, Cudd_Not(bVarCur), pLargeR->pDecs[g]->G );
|
|
else
|
|
bFTemp = Cudd_bddAnd( dd, bVarCur, pLargeR->pDecs[g]->G );
|
|
Cudd_Ref( bFTemp );
|
|
|
|
pDENew = dsdKernelDecompose_rec( pDsdMan, bFTemp );
|
|
pDENew = Dsd_Regular( pDENew );
|
|
Cudd_RecursiveDeref( dd, bFTemp );
|
|
|
|
// get the new gate
|
|
pThis = Dsd_TreeNodeCreate( DSD_NODE_PRIME, pLargeR->nDecs, s_nDecBlocks++ );
|
|
dsdKernelCopyListPlusOneMinusOne( pThis, pDENew, pLargeR->pDecs, pLargeR->nDecs, g );
|
|
goto EXIT;
|
|
}
|
|
}
|
|
|
|
// try to find one component in the pLarger that is equal to the whole of pSmaller
|
|
for ( c = 0; c < pLargeR->nDecs; c++ )
|
|
if ( pLargeR->pDecs[c] == pSmall || pLargeR->pDecs[c] == Dsd_Not(pSmall) )
|
|
{
|
|
iCompLarge = c;
|
|
break;
|
|
}
|
|
|
|
// assign the equal component
|
|
if ( c != pLargeR->nDecs ) // the decomposition is possible!
|
|
{
|
|
pComp = pLargeR->pDecs[iCompLarge];
|
|
nComp = 1;
|
|
}
|
|
else // the decomposition is still possible
|
|
{ // for example F = OR(ab,c,d), F(a=0) = OR(c,d), F(a=1) = OR(b,c,d)
|
|
// supp(F0) is contained in supp(F1), Polarity(F(a=0)) == Polarity(F(a=1))
|
|
|
|
// try to find a group of common components
|
|
if ( pLargeR->Type == pSmallR->Type &&
|
|
(pLargeR->Type == DSD_NODE_EXOR || (pSmallR->Type == DSD_NODE_OR && ((pLarge==pLargeR) == (pSmall==pSmallR)))) )
|
|
{
|
|
Dsd_Node_t ** pCommon, * pLastDiffL = NULL, * pLastDiffH = NULL;
|
|
int nCommon = dsdKernelFindCommonComponents( pDsdMan, pLargeR, pSmallR, &pCommon, &pLastDiffL, &pLastDiffH );
|
|
// if all the components of pSmall are contained in pLarge,
|
|
// then the decomposition exists
|
|
if ( nCommon == pSmallR->nDecs )
|
|
{
|
|
pComp = pSmallR;
|
|
nComp = pSmallR->nDecs;
|
|
}
|
|
}
|
|
}
|
|
|
|
if ( pComp ) // the decomposition is possible!
|
|
{
|
|
// Dsd_Node_t * pComp = pLargeR->pDecs[iCompLarge];
|
|
Dsd_Node_t * pCompR = Dsd_Regular( pComp );
|
|
int fComp1 = (int)( pLarge != pLargeR );
|
|
int fComp2 = (int)( pComp != pCompR );
|
|
int fComp3 = (int)( pSmall != pSmallR );
|
|
|
|
DdNode * bFuncComp; // the function of the given component
|
|
DdNode * bFuncNew; // the function of the input component
|
|
|
|
if ( pLargeR->Type == DSD_NODE_OR ) // Figure 4 of Matsunaga's paper
|
|
{
|
|
// the decomposition exists only if the polarity assignment
|
|
// along the paths is the same
|
|
if ( (fComp1 ^ fComp2) == fComp3 )
|
|
{ // decomposition exists = consider 4 cases
|
|
// consideration of cases leads to the following conclusion
|
|
// fComp1 gives the polarity of the resulting DSD_NODE_OR gate
|
|
// fComp2 gives the polarity of the common component feeding into the DSD_NODE_OR gate
|
|
//
|
|
// | fComp1 pL/ |pS
|
|
// <> .........<=>....... <> |
|
|
// | / |
|
|
// [OR] [OR] | fComp3
|
|
// / \ fComp2 / | \ |
|
|
// <> <> .......<=>... /..|..<> |
|
|
// / \ / | \|
|
|
// [OR] [C] S1 S2 C
|
|
// / \ .
|
|
// <> \ .
|
|
// / \ .
|
|
// [OR] [x] .
|
|
// / \ .
|
|
// S1 S2 .
|
|
//
|
|
|
|
|
|
// at this point we have the function F (bFTemp) and the common component C (bFuncComp)
|
|
// to get the remainder, R, in the relationship F = R + C, supp(R) & supp(C) = 0
|
|
// we compute the following R = Exist( F - C, supp(C) )
|
|
bFTemp = (fComp1)? Cudd_Not( bF ): bF;
|
|
bFuncComp = (fComp2)? Cudd_Not( pCompR->G ): pCompR->G;
|
|
bFuncNew = Cudd_bddAndAbstract( dd, bFTemp, Cudd_Not(bFuncComp), pCompR->S ); Cudd_Ref( bFuncNew );
|
|
|
|
// there is no need to copy the dec entry list first, because pComp is a component
|
|
// which will not be destroyed by the recursive call to decomposition
|
|
pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew );
|
|
assert( Dsd_IsComplement(pDENew) ); // follows from the consideration of cases
|
|
Cudd_RecursiveDeref( dd, bFuncNew );
|
|
|
|
// get the new gate
|
|
if ( nComp == 1 )
|
|
{
|
|
pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, 2, s_nDecBlocks++ );
|
|
pThis->pDecs[0] = pDENew;
|
|
pThis->pDecs[1] = pComp; // takes the complement
|
|
}
|
|
else
|
|
{ // pComp is not complemented
|
|
pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, nComp+1, s_nDecBlocks++ );
|
|
dsdKernelCopyListPlusOne( pThis, pDENew, pComp->pDecs, nComp );
|
|
}
|
|
|
|
if ( fComp1 )
|
|
pThis = Dsd_Not( pThis );
|
|
goto EXIT;
|
|
}
|
|
}
|
|
else if ( pLargeR->Type == DSD_NODE_EXOR ) // Figure 5 of Matsunaga's paper (with correction)
|
|
{ // decomposition always exists = consider 4 cases
|
|
|
|
// consideration of cases leads to the following conclusion
|
|
// fComp3 gives the COMPLEMENT of the polarity of the resulting EXOR gate
|
|
// (if fComp3 is 0, the EXOR gate is complemented, and vice versa)
|
|
//
|
|
// | fComp1 pL/ |pS
|
|
// <> .........<=>....... /....| fComp3
|
|
// | / |
|
|
// [XOR] [XOR] |
|
|
// / \ fComp2==0 / | \ |
|
|
// / \ / | \ |
|
|
// / \ / | \|
|
|
// [OR] [C] S1 S2 C
|
|
// / \ .
|
|
// <> \ .
|
|
// / \ .
|
|
// [XOR] [x] .
|
|
// / \ .
|
|
// S1 S2 .
|
|
//
|
|
|
|
assert( fComp2 == 0 );
|
|
// find the functionality of the lower gates
|
|
bFTemp = (fComp3)? bF: Cudd_Not( bF );
|
|
bFuncNew = Cudd_bddXor( dd, bFTemp, pComp->G ); Cudd_Ref( bFuncNew );
|
|
|
|
pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew );
|
|
assert( !Dsd_IsComplement(pDENew) ); // follows from the consideration of cases
|
|
Cudd_RecursiveDeref( dd, bFuncNew );
|
|
|
|
// get the new gate
|
|
if ( nComp == 1 )
|
|
{
|
|
pThis = Dsd_TreeNodeCreate( DSD_NODE_EXOR, 2, s_nDecBlocks++ );
|
|
pThis->pDecs[0] = pDENew;
|
|
pThis->pDecs[1] = pComp;
|
|
}
|
|
else
|
|
{ // pComp is not complemented
|
|
pThis = Dsd_TreeNodeCreate( DSD_NODE_EXOR, nComp+1, s_nDecBlocks++ );
|
|
dsdKernelCopyListPlusOne( pThis, pDENew, pComp->pDecs, nComp );
|
|
}
|
|
|
|
if ( !fComp3 )
|
|
pThis = Dsd_Not( pThis );
|
|
goto EXIT;
|
|
}
|
|
}
|
|
}
|
|
|
|
// this case was added to fix the trivial bug found November 4, 2002 in Japan
|
|
// by running the example provided by T. Sasao
|
|
if ( nSuppLH == nSuppL + nSuppH ) // the supports of the components are disjoint
|
|
{
|
|
// create a new component of the type ITE( a, pH, pL )
|
|
pThis = Dsd_TreeNodeCreate( DSD_NODE_PRIME, 3, s_nDecBlocks++ );
|
|
if ( dd->perm[pLR->S->index] < dd->perm[pHR->S->index] ) // pLR is higher in the varible order
|
|
{
|
|
pThis->pDecs[1] = pLR;
|
|
pThis->pDecs[2] = pHR;
|
|
}
|
|
else // pHR is higher in the varible order
|
|
{
|
|
pThis->pDecs[1] = pHR;
|
|
pThis->pDecs[2] = pLR;
|
|
}
|
|
// add the first component
|
|
pThis->pDecs[0] = pVarCurDE;
|
|
goto EXIT;
|
|
}
|
|
|
|
|
|
//////////////////////////////////////////////////////////////////////
|
|
// CASE 3.a Neither of the cofactors is a constant (OR, EXOR, PRIME)
|
|
//////////////////////////////////////////////////////////////////////
|
|
// the component types are identical
|
|
// and if they are OR, they are either both complemented or both not complemented
|
|
// and if they are PRIME, their dec numbers should be the same
|
|
if ( pLR->Type == pHR->Type &&
|
|
pLR->Type != DSD_NODE_BUF &&
|
|
(pLR->Type != DSD_NODE_OR || ( (pL == pLR && pH == pHR) || (pL != pLR && pH != pHR) ) ) &&
|
|
(pLR->Type != DSD_NODE_PRIME || pLR->nDecs == pHR->nDecs) )
|
|
{
|
|
// array to store common comps in pL and pH
|
|
Dsd_Node_t ** pCommon, * pLastDiffL = NULL, * pLastDiffH = NULL;
|
|
int nCommon = dsdKernelFindCommonComponents( pDsdMan, pLR, pHR, &pCommon, &pLastDiffL, &pLastDiffH );
|
|
if ( nCommon )
|
|
{
|
|
if ( pLR->Type == DSD_NODE_OR ) // Figure 2 of Matsunaga's paper
|
|
{ // at this point we have the function F and the group of common components C
|
|
// to get the remainder, R, in the relationship F = R + C, supp(R) & supp(C) = 0
|
|
// we compute the following R = Exist( F - C, supp(C) )
|
|
|
|
// compute the sum total of the common components and the union of their supports
|
|
DdNode * bCommF, * bCommS, * bFTemp, * bFuncNew;
|
|
Dsd_Node_t * pDENew;
|
|
|
|
dsdKernelComputeSumOfComponents( pDsdMan, pCommon, nCommon, &bCommF, &bCommS, 0 );
|
|
Cudd_Ref( bCommF );
|
|
Cudd_Ref( bCommS );
|
|
bFTemp = ( pL != pLR )? Cudd_Not(bF): bF;
|
|
|
|
bFuncNew = Cudd_bddAndAbstract( dd, bFTemp, Cudd_Not(bCommF), bCommS ); Cudd_Ref( bFuncNew );
|
|
Cudd_RecursiveDeref( dd, bCommF );
|
|
Cudd_RecursiveDeref( dd, bCommS );
|
|
|
|
// get the new gate
|
|
|
|
// copy the components first, then call the decomposition
|
|
// because decomposition will distroy the list used for copying
|
|
pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, nCommon + 1, s_nDecBlocks++ );
|
|
dsdKernelCopyListPlusOne( pThis, NULL, pCommon, nCommon );
|
|
|
|
// call the decomposition recursively
|
|
pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew );
|
|
// assert( !Dsd_IsComplement(pDENew) ); // follows from the consideration of cases
|
|
Cudd_RecursiveDeref( dd, bFuncNew );
|
|
|
|
// add the first component
|
|
pThis->pDecs[0] = pDENew;
|
|
|
|
if ( pL != pLR )
|
|
pThis = Dsd_Not( pThis );
|
|
goto EXIT;
|
|
}
|
|
else
|
|
if ( pLR->Type == DSD_NODE_EXOR ) // Figure 3 of Matsunaga's paper
|
|
{
|
|
// compute the sum total of the common components and the union of their supports
|
|
DdNode * bCommF, * bFuncNew;
|
|
Dsd_Node_t * pDENew;
|
|
int fCompExor;
|
|
|
|
dsdKernelComputeSumOfComponents( pDsdMan, pCommon, nCommon, &bCommF, NULL, 1 );
|
|
Cudd_Ref( bCommF );
|
|
|
|
bFuncNew = Cudd_bddXor( dd, bF, bCommF ); Cudd_Ref( bFuncNew );
|
|
Cudd_RecursiveDeref( dd, bCommF );
|
|
|
|
// get the new gate
|
|
|
|
// copy the components first, then call the decomposition
|
|
// because decomposition will distroy the list used for copying
|
|
pThis = Dsd_TreeNodeCreate( DSD_NODE_EXOR, nCommon + 1, s_nDecBlocks++ );
|
|
dsdKernelCopyListPlusOne( pThis, NULL, pCommon, nCommon );
|
|
|
|
// call the decomposition recursively
|
|
pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew );
|
|
Cudd_RecursiveDeref( dd, bFuncNew );
|
|
|
|
// remember the fact that it was complemented
|
|
fCompExor = Dsd_IsComplement(pDENew);
|
|
pDENew = Dsd_Regular(pDENew);
|
|
|
|
// add the first component
|
|
pThis->pDecs[0] = pDENew;
|
|
|
|
|
|
if ( fCompExor )
|
|
pThis = Dsd_Not( pThis );
|
|
goto EXIT;
|
|
}
|
|
else
|
|
if ( pLR->Type == DSD_NODE_PRIME && (nCommon == pLR->nDecs-1 || nCommon == pLR->nDecs) )
|
|
{
|
|
// for example the function F(a,b,c,d) = ITE(b,c,a(+)d) produces
|
|
// two cofactors F(a=0) = PRIME(b,c,d) and F(a=1) = PRIME(b,c,d)
|
|
// with exactly the same list of common components
|
|
|
|
Dsd_Node_t * pDENew;
|
|
DdNode * bFuncNew;
|
|
int fCompComp = 0; // this flag can be {0,1,2}
|
|
// if it is 0 there is no identity
|
|
// if it is 1/2, the cofactored functions are equal in the direct/complemented polarity
|
|
|
|
if ( nCommon == pLR->nDecs )
|
|
{ // all the components are the same
|
|
// find the formal input, in which pLow and pHigh differ (if such input exists)
|
|
int m;
|
|
Dsd_Node_t * pTempL, * pTempH;
|
|
|
|
s_Common++;
|
|
for ( m = 0; m < pLR->nDecs; m++ )
|
|
{
|
|
pTempL = pLR->pDecs[m]; // cannot be complemented
|
|
pTempH = pHR->pDecs[m]; // cannot be complemented
|
|
|
|
if ( Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh, pTempL->G, Cudd_Not(pTempH->G) ) &&
|
|
Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh, Cudd_Not(pTempL->G), pTempH->G ) )
|
|
{
|
|
pLastDiffL = pTempL;
|
|
pLastDiffH = pTempH;
|
|
assert( pLastDiffL == pLastDiffH );
|
|
fCompComp = 2;
|
|
break;
|
|
}
|
|
|
|
s_Loops2++;
|
|
s_Loops2++;
|
|
/*
|
|
if ( s_Loops2 % 10000 == 0 )
|
|
{
|
|
int i;
|
|
for ( i = 0; i < pLR->nDecs; i++ )
|
|
printf( " %d(s=%d)", pLR->pDecs[i]->Type,
|
|
Extra_bddSuppSize(dd, pLR->pDecs[i]->S) );
|
|
printf( "\n" );
|
|
}
|
|
*/
|
|
|
|
}
|
|
// if ( pLR->nDecs == Extra_bddSuppSize(dd, pLR->S) )
|
|
// s_Loops2Useless += pLR->nDecs * 2;
|
|
|
|
if ( fCompComp )
|
|
{ // put the equal components into pCommon, so that they could be copied into the new dec entry
|
|
nCommon = 0;
|
|
for ( m = 0; m < pLR->nDecs; m++ )
|
|
if ( pLR->pDecs[m] != pLastDiffL )
|
|
pCommon[nCommon++] = pLR->pDecs[m];
|
|
assert( nCommon = pLR->nDecs-1 );
|
|
}
|
|
}
|
|
else
|
|
{ // the differing components are known - check that they have compatible PRIME function
|
|
|
|
s_CommonNo++;
|
|
|
|
// find the numbers of different components
|
|
assert( pLastDiffL );
|
|
assert( pLastDiffH );
|
|
// also, they cannot be complemented, because the decomposition type is PRIME
|
|
|
|
if ( Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh, Cudd_Not(pLastDiffL->G), Cudd_Not(pLastDiffH->G) ) &&
|
|
Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh, pLastDiffL->G, pLastDiffH->G ) )
|
|
fCompComp = 1;
|
|
else if ( Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh, pLastDiffL->G, Cudd_Not(pLastDiffH->G) ) &&
|
|
Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh, Cudd_Not(pLastDiffL->G), pLastDiffH->G ) )
|
|
fCompComp = 2;
|
|
|
|
s_Loops3 += 4;
|
|
}
|
|
|
|
if ( fCompComp )
|
|
{
|
|
if ( fCompComp == 1 ) // it is true that bLow(G=0) == bHigh(H=0) && bLow(G=1) == bHigh(H=1)
|
|
bFuncNew = Cudd_bddIte( dd, bVarCur, pLastDiffH->G, pLastDiffL->G );
|
|
else // it is true that bLow(G=0) == bHigh(H=1) && bLow(G=1) == bHigh(H=0)
|
|
bFuncNew = Cudd_bddIte( dd, bVarCur, Cudd_Not(pLastDiffH->G), pLastDiffL->G );
|
|
Cudd_Ref( bFuncNew );
|
|
|
|
// get the new gate
|
|
|
|
// copy the components first, then call the decomposition
|
|
// because decomposition will distroy the list used for copying
|
|
pThis = Dsd_TreeNodeCreate( DSD_NODE_PRIME, pLR->nDecs, s_nDecBlocks++ );
|
|
dsdKernelCopyListPlusOne( pThis, NULL, pCommon, nCommon );
|
|
|
|
// create a new component
|
|
pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew );
|
|
Cudd_RecursiveDeref( dd, bFuncNew );
|
|
// the BDD of the argument function in PRIME decomposition, should be regular
|
|
pDENew = Dsd_Regular(pDENew);
|
|
|
|
// add the first component
|
|
pThis->pDecs[0] = pDENew;
|
|
goto EXIT;
|
|
}
|
|
} // end of PRIME type
|
|
} // end of existing common components
|
|
} // end of CASE 3.a
|
|
|
|
// if ( Depth != 1)
|
|
// {
|
|
|
|
//CASE4:
|
|
//////////////////////////////////////////////////////////////////////
|
|
// CASE 4
|
|
//////////////////////////////////////////////////////////////////////
|
|
{
|
|
// estimate the number of entries in the list
|
|
int nEntriesMax = pDsdMan->nInputs - dd->perm[VarInt];
|
|
|
|
// create the new decomposition entry
|
|
int nEntries = 0;
|
|
|
|
DdNode * SuppL, * SuppH, * SuppL_init, * SuppH_init;
|
|
Dsd_Node_t *pHigher = NULL; // Suppress "might be used uninitialized"
|
|
Dsd_Node_t *pLower, * pTemp, * pDENew;
|
|
|
|
|
|
int levTopSuppL;
|
|
int levTopSuppH;
|
|
int levTop;
|
|
|
|
pThis = Dsd_TreeNodeCreate( DSD_NODE_PRIME, nEntriesMax, s_nDecBlocks++ );
|
|
pThis->pDecs[ nEntries++ ] = pVarCurDE;
|
|
// other entries will be added to this list one-by-one during analysis
|
|
|
|
// count how many times does it happen that the decomposition entries are
|
|
s_Case4Calls++;
|
|
|
|
// consider the simplest case: when the supports are equal
|
|
// and at least one of the components
|
|
// is the PRIME without decompositions, or
|
|
// when both of them are without decomposition
|
|
if ( (((pLR->Type == DSD_NODE_PRIME && nSuppL == pLR->nDecs) || (pHR->Type == DSD_NODE_PRIME && nSuppH == pHR->nDecs)) && pLR->S == pHR->S) ||
|
|
((pLR->Type == DSD_NODE_PRIME && nSuppL == pLR->nDecs) && (pHR->Type == DSD_NODE_PRIME && nSuppH == pHR->nDecs)) )
|
|
{
|
|
|
|
s_Case4CallsSpecial++;
|
|
// walk through both supports and create the decomposition list composed of simple entries
|
|
SuppL = pLR->S;
|
|
SuppH = pHR->S;
|
|
do
|
|
{
|
|
// determine levels
|
|
levTopSuppL = cuddI(dd,SuppL->index);
|
|
levTopSuppH = cuddI(dd,SuppH->index);
|
|
|
|
// skip the topmost variable in both supports
|
|
if ( levTopSuppL <= levTopSuppH )
|
|
{
|
|
levTop = levTopSuppL;
|
|
SuppL = cuddT(SuppL);
|
|
}
|
|
else
|
|
levTop = levTopSuppH;
|
|
|
|
if ( levTopSuppH <= levTopSuppL )
|
|
SuppH = cuddT(SuppH);
|
|
|
|
// set the new decomposition entry
|
|
pThis->pDecs[ nEntries++ ] = pDsdMan->pInputs[ dd->invperm[levTop] ];
|
|
}
|
|
while ( SuppL != b1 || SuppH != b1 );
|
|
}
|
|
else
|
|
{
|
|
|
|
// compare two different decomposition lists
|
|
SuppL_init = pLR->S;
|
|
SuppH_init = pHR->S;
|
|
// start references (because these supports will change)
|
|
SuppL = pLR->S; Cudd_Ref( SuppL );
|
|
SuppH = pHR->S; Cudd_Ref( SuppH );
|
|
while ( SuppL != b1 || SuppH != b1 )
|
|
{
|
|
// determine the top level in cofactors and
|
|
// whether they have the same top level
|
|
int TopLevL = cuddI(dd,SuppL->index);
|
|
int TopLevH = cuddI(dd,SuppH->index);
|
|
int TopLevel = TopLevH;
|
|
int fEqualLevel = 0;
|
|
|
|
DdNode * bVarTop;
|
|
DdNode * bSuppSubract;
|
|
|
|
|
|
if ( TopLevL < TopLevH )
|
|
{
|
|
pHigher = pLR;
|
|
pLower = pHR;
|
|
TopLevel = TopLevL;
|
|
}
|
|
else if ( TopLevL > TopLevH )
|
|
{
|
|
pHigher = pHR;
|
|
pLower = pLR;
|
|
}
|
|
else
|
|
fEqualLevel = 1;
|
|
assert( TopLevel != CUDD_CONST_INDEX );
|
|
|
|
|
|
// find the currently top variable in the decomposition lists
|
|
bVarTop = dd->vars[dd->invperm[TopLevel]];
|
|
|
|
if ( !fEqualLevel )
|
|
{
|
|
// find the lower support
|
|
DdNode * bSuppLower = (TopLevL < TopLevH)? SuppH_init: SuppL_init;
|
|
|
|
// find the first component in pHigher
|
|
// whose support does not overlap with supp(Lower)
|
|
// and remember the previous component
|
|
int fPolarity;
|
|
Dsd_Node_t * pPrev = NULL; // the pointer to the component proceeding pCur
|
|
Dsd_Node_t * pCur = pHigher; // the first component not contained in supp(Lower)
|
|
while ( Extra_bddSuppOverlapping( dd, pCur->S, bSuppLower ) )
|
|
{ // get the next component
|
|
pPrev = pCur;
|
|
pCur = dsdKernelFindContainingComponent( pDsdMan, pCur, bVarTop, &fPolarity );
|
|
};
|
|
|
|
// look for the possibility to subtract more than one component
|
|
if ( pPrev == NULL || pPrev->Type == DSD_NODE_PRIME )
|
|
{ // if there is no previous component, or if the previous component is PRIME
|
|
// there is no way to subtract more than one component
|
|
|
|
// add the new decomposition entry (it is already regular)
|
|
pThis->pDecs[ nEntries++ ] = pCur;
|
|
// assign the support to be subtracted from both components
|
|
bSuppSubract = pCur->S;
|
|
}
|
|
else // all other types
|
|
{
|
|
// go through the decomposition list of pPrev and find components
|
|
// whose support does not overlap with supp(Lower)
|
|
|
|
static Dsd_Node_t * pNonOverlap[MAXINPUTS];
|
|
int i, nNonOverlap = 0;
|
|
for ( i = 0; i < pPrev->nDecs; i++ )
|
|
{
|
|
pTemp = Dsd_Regular( pPrev->pDecs[i] );
|
|
if ( !Extra_bddSuppOverlapping( dd, pTemp->S, bSuppLower ) )
|
|
pNonOverlap[ nNonOverlap++ ] = pPrev->pDecs[i];
|
|
}
|
|
assert( nNonOverlap > 0 );
|
|
|
|
if ( nNonOverlap == 1 )
|
|
{ // one one component was found, which is the original one
|
|
assert( Dsd_Regular(pNonOverlap[0]) == pCur);
|
|
// add the new decomposition entry
|
|
pThis->pDecs[ nEntries++ ] = pCur;
|
|
// assign the support to be subtracted from both components
|
|
bSuppSubract = pCur->S;
|
|
}
|
|
else // more than one components was found
|
|
{
|
|
// find the OR (EXOR) of the non-overlapping components
|
|
DdNode * bCommF;
|
|
dsdKernelComputeSumOfComponents( pDsdMan, pNonOverlap, nNonOverlap, &bCommF, NULL, (int)(pPrev->Type==DSD_NODE_EXOR) );
|
|
Cudd_Ref( bCommF );
|
|
|
|
// create a new gated
|
|
pDENew = dsdKernelDecompose_rec( pDsdMan, bCommF );
|
|
Cudd_RecursiveDeref(dd, bCommF);
|
|
// make it regular... it must be regular already
|
|
assert( !Dsd_IsComplement(pDENew) );
|
|
|
|
// add the new decomposition entry
|
|
pThis->pDecs[ nEntries++ ] = pDENew;
|
|
// assign the support to be subtracted from both components
|
|
bSuppSubract = pDENew->S;
|
|
}
|
|
}
|
|
|
|
// subtract its support from the support of upper component
|
|
if ( TopLevL < TopLevH )
|
|
{
|
|
SuppL = Cudd_bddExistAbstract( dd, bTemp = SuppL, bSuppSubract ); Cudd_Ref( SuppL );
|
|
Cudd_RecursiveDeref(dd, bTemp);
|
|
}
|
|
else
|
|
{
|
|
SuppH = Cudd_bddExistAbstract( dd, bTemp = SuppH, bSuppSubract ); Cudd_Ref( SuppH );
|
|
Cudd_RecursiveDeref(dd, bTemp);
|
|
}
|
|
} // end of if ( !fEqualLevel )
|
|
else // if ( fEqualLevel ) -- they have the same top level var
|
|
{
|
|
static Dsd_Node_t * pMarkedLeft[MAXINPUTS]; // the pointers to the marked blocks
|
|
static char pMarkedPols[MAXINPUTS]; // polarities of the marked blocks
|
|
int nMarkedLeft = 0;
|
|
|
|
int fPolarity = 0;
|
|
Dsd_Node_t * pTempL = pLR;
|
|
|
|
int fPolarityCurH = 0;
|
|
Dsd_Node_t * pPrevH = NULL, * pCurH = pHR;
|
|
|
|
int fPolarityCurL = 0;
|
|
Dsd_Node_t * pPrevL = NULL, * pCurL = pLR; // = pMarkedLeft[0];
|
|
int index = 1;
|
|
|
|
// set the new mark
|
|
s_Mark++;
|
|
|
|
// go over the dec list of pL, mark all components that contain the given variable
|
|
assert( Extra_bddSuppContainVar( dd, pLR->S, bVarTop ) );
|
|
assert( Extra_bddSuppContainVar( dd, pHR->S, bVarTop ) );
|
|
do {
|
|
pTempL->Mark = s_Mark;
|
|
pMarkedLeft[ nMarkedLeft ] = pTempL;
|
|
pMarkedPols[ nMarkedLeft ] = fPolarity;
|
|
nMarkedLeft++;
|
|
} while ( (pTempL = dsdKernelFindContainingComponent( pDsdMan, pTempL, bVarTop, &fPolarity )) );
|
|
|
|
// go over the dec list of pH, and find the component that is marked and the previos one
|
|
// (such component always exists, because they have common variables)
|
|
while ( pCurH->Mark != s_Mark )
|
|
{
|
|
pPrevH = pCurH;
|
|
pCurH = dsdKernelFindContainingComponent( pDsdMan, pCurH, bVarTop, &fPolarityCurH );
|
|
assert( pCurH );
|
|
}
|
|
|
|
// go through the first list once again and find
|
|
// the component proceeding the one marked found in the second list
|
|
while ( pCurL != pCurH )
|
|
{
|
|
pPrevL = pCurL;
|
|
pCurL = pMarkedLeft[index];
|
|
fPolarityCurL = pMarkedPols[index];
|
|
index++;
|
|
}
|
|
|
|
// look for the possibility to subtract more than one component
|
|
if ( !pPrevL || !pPrevH || pPrevL->Type != pPrevH->Type || pPrevL->Type == DSD_NODE_PRIME || fPolarityCurL != fPolarityCurH )
|
|
{ // there is no way to extract more than one
|
|
pThis->pDecs[ nEntries++ ] = pCurH;
|
|
// assign the support to be subtracted from both components
|
|
bSuppSubract = pCurH->S;
|
|
}
|
|
else
|
|
{
|
|
// find the equal components in two decomposition lists
|
|
Dsd_Node_t ** pCommon, * pLastDiffL = NULL, * pLastDiffH = NULL;
|
|
int nCommon = dsdKernelFindCommonComponents( pDsdMan, pPrevL, pPrevH, &pCommon, &pLastDiffL, &pLastDiffH );
|
|
|
|
if ( nCommon == 0 || nCommon == 1 )
|
|
{ // one one component was found, which is the original one
|
|
// assert( Dsd_Regular(pCommon[0]) == pCurL);
|
|
// add the new decomposition entry
|
|
pThis->pDecs[ nEntries++ ] = pCurL;
|
|
// assign the support to be subtracted from both components
|
|
bSuppSubract = pCurL->S;
|
|
}
|
|
else // more than one components was found
|
|
{
|
|
// find the OR (EXOR) of the non-overlapping components
|
|
DdNode * bCommF;
|
|
dsdKernelComputeSumOfComponents( pDsdMan, pCommon, nCommon, &bCommF, NULL, (int)(pPrevL->Type==DSD_NODE_EXOR) );
|
|
Cudd_Ref( bCommF );
|
|
|
|
pDENew = dsdKernelDecompose_rec( pDsdMan, bCommF );
|
|
assert( !Dsd_IsComplement(pDENew) ); // cannot be complemented because of construction
|
|
Cudd_RecursiveDeref( dd, bCommF );
|
|
|
|
// add the new decomposition entry
|
|
pThis->pDecs[ nEntries++ ] = pDENew;
|
|
|
|
// assign the support to be subtracted from both components
|
|
bSuppSubract = pDENew->S;
|
|
}
|
|
}
|
|
|
|
SuppL = Cudd_bddExistAbstract( dd, bTemp = SuppL, bSuppSubract ), Cudd_Ref( SuppL );
|
|
Cudd_RecursiveDeref(dd, bTemp);
|
|
|
|
SuppH = Cudd_bddExistAbstract( dd, bTemp = SuppH, bSuppSubract ), Cudd_Ref( SuppH );
|
|
Cudd_RecursiveDeref(dd, bTemp);
|
|
|
|
} // end of if ( fEqualLevel )
|
|
|
|
} // end of decomposition list comparison
|
|
Cudd_RecursiveDeref( dd, SuppL );
|
|
Cudd_RecursiveDeref( dd, SuppH );
|
|
|
|
}
|
|
|
|
// check that the estimation of the number of entries was okay
|
|
assert( nEntries <= nEntriesMax );
|
|
|
|
// if ( nEntries != Extra_bddSuppSize(dd, bSuppNew) )
|
|
// s_Case5++;
|
|
|
|
// update the number of entries in the new decomposition list
|
|
pThis->nDecs = nEntries;
|
|
}
|
|
//}
|
|
EXIT:
|
|
|
|
{
|
|
// if the component created is complemented, it represents a function without complement
|
|
// therefore, as it is, without complement, it should recieve the complemented function
|
|
Dsd_Node_t * pThisR = Dsd_Regular( pThis );
|
|
assert( pThisR->G == NULL );
|
|
assert( pThisR->S == NULL );
|
|
|
|
if ( pThisR == pThis ) // set regular function
|
|
pThisR->G = bF;
|
|
else // set complemented function
|
|
pThisR->G = Cudd_Not(bF);
|
|
Cudd_Ref(bF); // reference the function in the component
|
|
|
|
assert( bSuppNew );
|
|
pThisR->S = bSuppNew; // takes the reference from the new support
|
|
if ( st__insert( pDsdMan->Table, (char*)bF, (char*)pThis ) )
|
|
{
|
|
assert( 0 );
|
|
}
|
|
s_CacheEntries++;
|
|
|
|
|
|
/*
|
|
if ( dsdKernelVerifyDecomposition(dd, pThis) == 0 )
|
|
{
|
|
// write the function, for which verification does not work
|
|
cout << endl << "Internal verification failed!"" );
|
|
|
|
// create the variable mask
|
|
static int s_pVarMask[MAXINPUTS];
|
|
int nInputCounter = 0;
|
|
|
|
Cudd_SupportArray( dd, bF, s_pVarMask );
|
|
int k;
|
|
for ( k = 0; k < dd->size; k++ )
|
|
if ( s_pVarMask[k] )
|
|
nInputCounter++;
|
|
|
|
cout << endl << "The problem function is "" );
|
|
|
|
DdNode * zNewFunc = Cudd_zddIsopCover( dd, bF, bF ); Cudd_Ref( zNewFunc );
|
|
cuddWriteFunctionSop( stdout, dd, zNewFunc, -1, dd->size, "1", s_pVarMask );
|
|
Cudd_RecursiveDerefZdd( dd, zNewFunc );
|
|
}
|
|
*/
|
|
|
|
}
|
|
|
|
Depth--;
|
|
return Dsd_NotCond( pThis, fCompF );
|
|
}
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// OTHER FUNCTIONS ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Finds the corresponding decomposition entry.]
|
|
|
|
Description [This function returns the non-complemented pointer to the
|
|
DecEntry of that component which contains the given variable in its
|
|
support, or NULL if no such component exists]
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
Dsd_Node_t * dsdKernelFindContainingComponent( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pWhere, DdNode * Var, int * fPolarity )
|
|
|
|
{
|
|
Dsd_Node_t * pTemp;
|
|
int i;
|
|
|
|
// assert( !Dsd_IsComplement( pWhere ) );
|
|
// assert( Extra_bddSuppContainVar( pDsdMan->dd, pWhere->S, Var ) );
|
|
|
|
if ( pWhere->nDecs == 1 )
|
|
return NULL;
|
|
|
|
for( i = 0; i < pWhere->nDecs; i++ )
|
|
{
|
|
pTemp = Dsd_Regular( pWhere->pDecs[i] );
|
|
if ( Extra_bddSuppContainVar( pDsdMan->dd, pTemp->S, Var ) )
|
|
{
|
|
*fPolarity = (int)( pTemp != pWhere->pDecs[i] );
|
|
return pTemp;
|
|
}
|
|
}
|
|
assert( 0 );
|
|
return NULL;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Find the common decomposition components.]
|
|
|
|
Description [This function determines the common components. It counts
|
|
the number of common components in the decomposition lists of pL and pH
|
|
and returns their number and the lists of common components. It assumes
|
|
that pL and pH are regular pointers. It retuns also the pointers to the
|
|
last different components encountered in pL and pH.]
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
int dsdKernelFindCommonComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd_Node_t * pH, Dsd_Node_t *** pCommon, Dsd_Node_t ** pLastDiffL, Dsd_Node_t ** pLastDiffH )
|
|
{
|
|
static Dsd_Node_t * Common[MAXINPUTS];
|
|
int nCommon = 0;
|
|
|
|
// pointers to the current decomposition entries
|
|
Dsd_Node_t * pLcur;
|
|
Dsd_Node_t * pHcur;
|
|
|
|
// the pointers to their supports
|
|
DdNode * bSLcur;
|
|
DdNode * bSHcur;
|
|
|
|
// the top variable in the supports
|
|
int TopVar;
|
|
|
|
// the indices running through the components
|
|
int iCurL = 0;
|
|
int iCurH = 0;
|
|
while ( iCurL < pL->nDecs && iCurH < pH->nDecs )
|
|
{ // both did not run out
|
|
|
|
pLcur = Dsd_Regular(pL->pDecs[iCurL]);
|
|
pHcur = Dsd_Regular(pH->pDecs[iCurH]);
|
|
|
|
bSLcur = pLcur->S;
|
|
bSHcur = pHcur->S;
|
|
|
|
// find out what component is higher in the BDD
|
|
if ( pDsdMan->dd->perm[bSLcur->index] < pDsdMan->dd->perm[bSHcur->index] )
|
|
TopVar = bSLcur->index;
|
|
else
|
|
TopVar = bSHcur->index;
|
|
|
|
if ( TopVar == bSLcur->index && TopVar == bSHcur->index )
|
|
{
|
|
// the components may be equal - should match exactly!
|
|
if ( pL->pDecs[iCurL] == pH->pDecs[iCurH] )
|
|
Common[nCommon++] = pL->pDecs[iCurL];
|
|
else
|
|
{
|
|
*pLastDiffL = pL->pDecs[iCurL];
|
|
*pLastDiffH = pH->pDecs[iCurH];
|
|
}
|
|
|
|
// skip both
|
|
iCurL++;
|
|
iCurH++;
|
|
}
|
|
else if ( TopVar == bSLcur->index )
|
|
{ // the components cannot be equal
|
|
// skip the top-most one
|
|
*pLastDiffL = pL->pDecs[iCurL++];
|
|
}
|
|
else // if ( TopVar == bSHcur->index )
|
|
{ // the components cannot be equal
|
|
// skip the top-most one
|
|
*pLastDiffH = pH->pDecs[iCurH++];
|
|
}
|
|
}
|
|
|
|
// if one of the lists still has components, write the first one down
|
|
if ( iCurL < pL->nDecs )
|
|
*pLastDiffL = pL->pDecs[iCurL];
|
|
|
|
if ( iCurH < pH->nDecs )
|
|
*pLastDiffH = pH->pDecs[iCurH];
|
|
|
|
// return the pointer to the array
|
|
*pCommon = Common;
|
|
// return the number of common components
|
|
return nCommon;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Computes the sum (OR or EXOR) of the functions of the components.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
void dsdKernelComputeSumOfComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t ** pCommon, int nCommon, DdNode ** pCompF, DdNode ** pCompS, int fExor )
|
|
{
|
|
DdManager * dd = pDsdMan->dd;
|
|
DdNode * bF, * bFadd, * bTemp;
|
|
DdNode * bS = NULL; // Suppress "might be used uninitialized"
|
|
Dsd_Node_t * pDE, * pDER;
|
|
int i;
|
|
|
|
// start the function
|
|
bF = b0; Cudd_Ref( bF );
|
|
// start the support
|
|
if ( pCompS )
|
|
bS = b1, Cudd_Ref( bS );
|
|
|
|
assert( nCommon > 0 );
|
|
for ( i = 0; i < nCommon; i++ )
|
|
{
|
|
pDE = pCommon[i];
|
|
pDER = Dsd_Regular( pDE );
|
|
bFadd = (pDE != pDER)? Cudd_Not(pDER->G): pDER->G;
|
|
// add to the function
|
|
if ( fExor )
|
|
bF = Cudd_bddXor( dd, bTemp = bF, bFadd );
|
|
else
|
|
bF = Cudd_bddOr( dd, bTemp = bF, bFadd );
|
|
Cudd_Ref( bF );
|
|
Cudd_RecursiveDeref( dd, bTemp );
|
|
if ( pCompS )
|
|
{
|
|
// add to the support
|
|
bS = Cudd_bddAnd( dd, bTemp = bS, pDER->S ); Cudd_Ref( bS );
|
|
Cudd_RecursiveDeref( dd, bTemp );
|
|
}
|
|
}
|
|
// return the function
|
|
Cudd_Deref( bF );
|
|
*pCompF = bF;
|
|
|
|
// return the support
|
|
if ( pCompS )
|
|
Cudd_Deref( bS ), *pCompS = bS;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Checks support containment of the decomposition components.]
|
|
|
|
Description [This function returns 1 if support of one component is contained
|
|
in that of another. In this case, pLarge (pSmall) is assigned to point to the
|
|
larger (smaller) support. If the supports are identical return 0, and does not
|
|
assign the components.]
|
|
]
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
int dsdKernelCheckContainment( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd_Node_t * pH, Dsd_Node_t ** pLarge, Dsd_Node_t ** pSmall )
|
|
{
|
|
DdManager * dd = pDsdMan->dd;
|
|
DdNode * bSuppLarge, * bSuppSmall;
|
|
int RetValue;
|
|
|
|
RetValue = Extra_bddSuppCheckContainment( dd, pL->S, pH->S, &bSuppLarge, &bSuppSmall );
|
|
|
|
if ( RetValue == 0 )
|
|
return 0;
|
|
|
|
if ( pH->S == bSuppLarge )
|
|
{
|
|
*pLarge = pH;
|
|
*pSmall = pL;
|
|
}
|
|
else // if ( pL->S == bSuppLarge )
|
|
{
|
|
*pLarge = pL;
|
|
*pSmall = pH;
|
|
}
|
|
return 1;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Copies the list of components plus one.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
void dsdKernelCopyListPlusOne( Dsd_Node_t * p, Dsd_Node_t * First, Dsd_Node_t ** ppList, int nListSize )
|
|
{
|
|
int i;
|
|
assert( nListSize+1 == p->nDecs );
|
|
p->pDecs[0] = First;
|
|
for( i = 0; i < nListSize; i++ )
|
|
p->pDecs[i+1] = ppList[i];
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Copies the list of components plus one, and skips one.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
void dsdKernelCopyListPlusOneMinusOne( Dsd_Node_t * p, Dsd_Node_t * First, Dsd_Node_t ** ppList, int nListSize, int iSkipped )
|
|
{
|
|
int i, Counter;
|
|
assert( nListSize == p->nDecs );
|
|
p->pDecs[0] = First;
|
|
for( i = 0, Counter = 1; i < nListSize; i++ )
|
|
if ( i != iSkipped )
|
|
p->pDecs[Counter++] = ppList[i];
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Debugging procedure to compute the functionality of the decomposed structure.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
int dsdKernelVerifyDecomposition( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pDE )
|
|
{
|
|
DdManager * dd = pDsdMan->dd;
|
|
Dsd_Node_t * pR = Dsd_Regular(pDE);
|
|
int RetValue;
|
|
|
|
DdNode * bRes;
|
|
if ( pR->Type == DSD_NODE_CONST1 )
|
|
bRes = b1;
|
|
else if ( pR->Type == DSD_NODE_BUF )
|
|
bRes = pR->G;
|
|
else if ( pR->Type == DSD_NODE_OR || pR->Type == DSD_NODE_EXOR )
|
|
dsdKernelComputeSumOfComponents( pDsdMan, pR->pDecs, pR->nDecs, &bRes, NULL, (int)(pR->Type == DSD_NODE_EXOR) );
|
|
else if ( pR->Type == DSD_NODE_PRIME )
|
|
{
|
|
int i;
|
|
static DdNode * bGVars[MAXINPUTS];
|
|
// transform the function of this block, so that it depended on inputs
|
|
// corresponding to the formal inputs
|
|
DdNode * bNewFunc = Dsd_TreeGetPrimeFunctionOld( dd, pR, 1 ); Cudd_Ref( bNewFunc );
|
|
|
|
// compose this function with the inputs
|
|
// create the elementary permutation
|
|
for ( i = 0; i < dd->size; i++ )
|
|
bGVars[i] = dd->vars[i];
|
|
|
|
// assign functions to be composed
|
|
for ( i = 0; i < pR->nDecs; i++ )
|
|
bGVars[dd->invperm[i]] = pR->pDecs[i]->G;
|
|
|
|
// perform the composition
|
|
bRes = Cudd_bddVectorCompose( dd, bNewFunc, bGVars ); Cudd_Ref( bRes );
|
|
Cudd_RecursiveDeref( dd, bNewFunc );
|
|
|
|
/////////////////////////////////////////////////////////
|
|
RetValue = (int)( bRes == pR->G );//|| bRes == Cudd_Not(pR->G) );
|
|
/////////////////////////////////////////////////////////
|
|
Cudd_Deref( bRes );
|
|
}
|
|
else
|
|
{
|
|
assert(0);
|
|
}
|
|
|
|
Cudd_Ref( bRes );
|
|
RetValue = (int)( bRes == pR->G );//|| bRes == Cudd_Not(pR->G) );
|
|
Cudd_RecursiveDeref( dd, bRes );
|
|
return RetValue;
|
|
}
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// END OF FILE ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
ABC_NAMESPACE_IMPL_END
|
|
|