diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-10-01 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-10-01 08:01:00 -0700 |
commit | 4812c90424dfc40d26725244723887a2d16ddfd9 (patch) | |
tree | b32ace96e7e2d84d586e09ba605463b6f49c3271 /src/misc/mvc/mvcUtils.c | |
parent | e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7 (diff) | |
download | abc-4812c90424dfc40d26725244723887a2d16ddfd9.tar.gz abc-4812c90424dfc40d26725244723887a2d16ddfd9.tar.bz2 abc-4812c90424dfc40d26725244723887a2d16ddfd9.zip |
Version abc71001
Diffstat (limited to 'src/misc/mvc/mvcUtils.c')
-rw-r--r-- | src/misc/mvc/mvcUtils.c | 868 |
1 files changed, 868 insertions, 0 deletions
diff --git a/src/misc/mvc/mvcUtils.c b/src/misc/mvc/mvcUtils.c new file mode 100644 index 00000000..4b13b23d --- /dev/null +++ b/src/misc/mvc/mvcUtils.c @@ -0,0 +1,868 @@ +/**CFile**************************************************************** + + FileName [mvcUtils.c] + + PackageName [MVSIS 2.0: Multi-valued logic synthesis system.] + + Synopsis [Various cover handling utilities.] + + Author [MVSIS Group] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - February 1, 2003.] + + Revision [$Id: mvcUtils.c,v 1.7 2003/04/26 20:41:36 alanmi Exp $] + +***********************************************************************/ + +#include "mvc.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static int bit_count[256] = { + 0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7, + 3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8 +}; + + +static void Mvc_CoverCopyColumn( Mvc_Cover_t * pCoverOld, Mvc_Cover_t * pCoverNew, int iColOld, int iColNew ); + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mvc_CoverSupport( Mvc_Cover_t * pCover, Mvc_Cube_t * pSupp ) +{ + Mvc_Cube_t * pCube; + // clean the support + Mvc_CubeBitClean( pSupp ); + // collect the support + Mvc_CoverForEachCube( pCover, pCube ) + Mvc_CubeBitOr( pSupp, pSupp, pCube ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mvc_CoverSupportAnd( Mvc_Cover_t * pCover, Mvc_Cube_t * pSupp ) +{ + Mvc_Cube_t * pCube; + // clean the support + Mvc_CubeBitFill( pSupp ); + // collect the support + Mvc_CoverForEachCube( pCover, pCube ) + Mvc_CubeBitAnd( pSupp, pSupp, pCube ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Mvc_CoverSupportSizeBinary( Mvc_Cover_t * pCover ) +{ + Mvc_Cube_t * pSupp; + int Counter, i, v0, v1; + // compute the support + pSupp = Mvc_CubeAlloc( pCover ); + Mvc_CoverSupportAnd( pCover, pSupp ); + Counter = pCover->nBits/2; + for ( i = 0; i < pCover->nBits/2; i++ ) + { + v0 = Mvc_CubeBitValue( pSupp, 2*i ); + v1 = Mvc_CubeBitValue( pSupp, 2*i+1 ); + if ( v0 && v1 ) + Counter--; + } + Mvc_CubeFree( pCover, pSupp ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Mvc_CoverSupportVarBelongs( Mvc_Cover_t * pCover, int iVar ) +{ + Mvc_Cube_t * pSupp; + int RetValue, v0, v1; + // compute the support + pSupp = Mvc_CubeAlloc( pCover ); + Mvc_CoverSupportAnd( pCover, pSupp ); + v0 = Mvc_CubeBitValue( pSupp, 2*iVar ); + v1 = Mvc_CubeBitValue( pSupp, 2*iVar+1 ); + RetValue = (int)( !v0 || !v1 ); + Mvc_CubeFree( pCover, pSupp ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mvc_CoverCommonCube( Mvc_Cover_t * pCover, Mvc_Cube_t * pComCube ) +{ + Mvc_Cube_t * pCube; + // clean the support + Mvc_CubeBitFill( pComCube ); + // collect the support + Mvc_CoverForEachCube( pCover, pCube ) + Mvc_CubeBitAnd( pComCube, pComCube, pCube ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Mvc_CoverIsCubeFree( Mvc_Cover_t * pCover ) +{ + int Result; + // get the common cube + Mvc_CoverAllocateMask( pCover ); + Mvc_CoverCommonCube( pCover, pCover->pMask ); + // check whether the common cube is empty + Mvc_CubeBitEmpty( Result, pCover->pMask ); + return Result; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mvc_CoverMakeCubeFree( Mvc_Cover_t * pCover ) +{ + Mvc_Cube_t * pCube; + // get the common cube + Mvc_CoverAllocateMask( pCover ); + Mvc_CoverCommonCube( pCover, pCover->pMask ); + // remove this cube from the cubes in the cover + Mvc_CoverForEachCube( pCover, pCube ) + Mvc_CubeBitSharp( pCube, pCube, pCover->pMask ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Mvc_Cover_t * Mvc_CoverCommonCubeCover( Mvc_Cover_t * pCover ) +{ + Mvc_Cover_t * pRes; + Mvc_Cube_t * pCube; + // create the new cover + pRes = Mvc_CoverClone( pCover ); + // get the new cube + pCube = Mvc_CubeAlloc( pRes ); + // get the common cube + Mvc_CoverCommonCube( pCover, pCube ); + // add the cube to the cover + Mvc_CoverAddCubeTail( pRes, pCube ); + return pRes; +} + + +/**Function************************************************************* + + Synopsis [Returns 1 if the support of cover2 is contained in the support of cover1.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Mvc_CoverCheckSuppContainment( Mvc_Cover_t * pCover1, Mvc_Cover_t * pCover2 ) +{ + int Result; + assert( pCover1->nBits == pCover2->nBits ); + // set the supports + Mvc_CoverAllocateMask( pCover1 ); + Mvc_CoverSupport( pCover1, pCover1->pMask ); + Mvc_CoverAllocateMask( pCover2 ); + Mvc_CoverSupport( pCover2, pCover2->pMask ); + // check the containment + Mvc_CubeBitNotImpl( Result, pCover2->pMask, pCover1->pMask ); + return !Result; +} + +/**Function************************************************************* + + Synopsis [Counts the cube sizes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Mvc_CoverSetCubeSizes( Mvc_Cover_t * pCover ) +{ + Mvc_Cube_t * pCube; + unsigned char * pByte, * pByteStart, * pByteStop; + int nBytes, nOnes; + + // get the number of unsigned chars in the cube's bit strings + nBytes = pCover->nBits / (8 * sizeof(unsigned char)) + (int)(pCover->nBits % (8 * sizeof(unsigned char)) > 0); + // iterate through the cubes + Mvc_CoverForEachCube( pCover, pCube ) + { + // clean the counter of ones + nOnes = 0; + // set the starting and stopping positions + pByteStart = (unsigned char *)pCube->pData; + pByteStop = pByteStart + nBytes; + // iterate through the positions + for ( pByte = pByteStart; pByte < pByteStop; pByte++ ) + nOnes += bit_count[*pByte]; + // set the nOnes + Mvc_CubeSetSize( pCube, nOnes ); + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Counts the cube sizes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Mvc_CoverGetCubeSize( Mvc_Cube_t * pCube ) +{ + unsigned char * pByte, * pByteStart, * pByteStop; + int nOnes, nBytes, nBits; + // get the number of unsigned chars in the cube's bit strings + nBits = (pCube->iLast + 1) * sizeof(Mvc_CubeWord_t) * 8 - pCube->nUnused; + nBytes = nBits / (8 * sizeof(unsigned char)) + (int)(nBits % (8 * sizeof(unsigned char)) > 0); + // clean the counter of ones + nOnes = 0; + // set the starting and stopping positions + pByteStart = (unsigned char *)pCube->pData; + pByteStop = pByteStart + nBytes; + // iterate through the positions + for ( pByte = pByteStart; pByte < pByteStop; pByte++ ) + nOnes += bit_count[*pByte]; + return nOnes; +} + +/**Function************************************************************* + + Synopsis [Counts the differences in each cube pair in the cover.] + + Description [Takes the cover (pCover) and the array where the + diff counters go (pDiffs). The array pDiffs should have as many + entries as there are different pairs of cubes in the cover: n(n-1)/2. + Fills out the array pDiffs with the following info: For each cube + pair, included in the array is the number of literals in both cubes + after they are made cube free.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Mvc_CoverCountCubePairDiffs( Mvc_Cover_t * pCover, unsigned char pDiffs[] ) +{ + Mvc_Cube_t * pCube1; + Mvc_Cube_t * pCube2; + Mvc_Cube_t * pMask; + unsigned char * pByte, * pByteStart, * pByteStop; + int nBytes, nOnes; + int nCubePairs; + + // allocate a temporary mask + pMask = Mvc_CubeAlloc( pCover ); + // get the number of unsigned chars in the cube's bit strings + nBytes = pCover->nBits / (8 * sizeof(unsigned char)) + (int)(pCover->nBits % (8 * sizeof(unsigned char)) > 0); + // iterate through the cubes + nCubePairs = 0; + Mvc_CoverForEachCube( pCover, pCube1 ) + { + Mvc_CoverForEachCubeStart( Mvc_CubeReadNext(pCube1), pCube2 ) + { + // find the bit-wise exor of cubes + Mvc_CubeBitExor( pMask, pCube1, pCube2 ); + // set the starting and stopping positions + pByteStart = (unsigned char *)pMask->pData; + pByteStop = pByteStart + nBytes; + // clean the counter of ones + nOnes = 0; + // iterate through the positions + for ( pByte = pByteStart; pByte < pByteStop; pByte++ ) + nOnes += bit_count[*pByte]; + // set the nOnes + pDiffs[nCubePairs++] = nOnes; + } + } + // deallocate the mask + Mvc_CubeFree( pCover, pMask ); + return 1; +} + + +/**Function************************************************************* + + Synopsis [Creates a new cover containing some literals of the old cover.] + + Description [Creates the new cover containing the given number (nVarsRem) + literals of the old cover. All the bits of the new cover are initialized + to "1". The selected bits from the old cover are copied on top. The numbers + of the selected bits to copy are given in the array pVarsRem. The i-set + entry in this array is the index of the bit in the old cover which goes + to the i-th place in the new cover. If the i-th entry in pVarsRem is -1, + it means that the i-th bit does not change (remains composed of all 1's). + This is a useful feature to speed up remapping covers, which are known + to depend only on a subset of input variables.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Mvc_Cover_t * Mvc_CoverRemap( Mvc_Cover_t * p, int * pVarsRem, int nVarsRem ) +{ + Mvc_Cover_t * pCover; + Mvc_Cube_t * pCube, * pCubeCopy; + int i; + // clone the cover + pCover = Mvc_CoverAlloc( p->pMem, nVarsRem ); + // copy the cube list + Mvc_CoverForEachCube( p, pCube ) + { + pCubeCopy = Mvc_CubeAlloc( pCover ); + //Mvc_CubeBitClean( pCubeCopy ); //changed by wjiang + Mvc_CubeBitFill( pCubeCopy ); //changed by wjiang + Mvc_CoverAddCubeTail( pCover, pCubeCopy ); + } + // copy the corresponding columns + for ( i = 0; i < nVarsRem; i++ ) + { + if (pVarsRem[i] < 0) + continue; //added by wjiang + assert( pVarsRem[i] >= 0 && pVarsRem[i] < p->nBits ); + Mvc_CoverCopyColumn( p, pCover, pVarsRem[i], i ); + } + return pCover; +} + +/**Function************************************************************* + + Synopsis [Copies a column from the old cover to the new cover.] + + Description [Copies the column (iColOld) of the old cover (pCoverOld) + into the column (iColNew) of the new cover (pCoverNew). Assumes that + the number of cubes is the same in both covers. Makes no assuptions + about the current contents of the column in the new cover.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mvc_CoverCopyColumn( Mvc_Cover_t * pCoverOld, Mvc_Cover_t * pCoverNew, + int iColOld, int iColNew ) +{ + Mvc_Cube_t * pCubeOld, * pCubeNew; + int iWordOld, iWordNew, iBitOld, iBitNew; + + assert( Mvc_CoverReadCubeNum(pCoverOld) == Mvc_CoverReadCubeNum(pCoverNew) ); + + // get the place of the old and new columns + iWordOld = Mvc_CubeWhichWord(iColOld); + iBitOld = Mvc_CubeWhichBit(iColOld); + iWordNew = Mvc_CubeWhichWord(iColNew); + iBitNew = Mvc_CubeWhichBit(iColNew); + + // go through the cubes of both covers + pCubeNew = Mvc_CoverReadCubeHead(pCoverNew); + Mvc_CoverForEachCube( pCoverOld, pCubeOld ) + { + if ( pCubeOld->pData[iWordOld] & (1<<iBitOld) ) + pCubeNew->pData[iWordNew] |= (1<<iBitNew); + else + pCubeNew->pData[iWordNew] &= ~(1<<iBitNew); // added by wjiang + pCubeNew = Mvc_CubeReadNext( pCubeNew ); + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mvc_CoverInverse( Mvc_Cover_t * pCover ) +{ + Mvc_Cube_t * pCube; + // complement the cubes + Mvc_CoverForEachCube( pCover, pCube ) + Mvc_CubeBitNot( pCube ); +} + +/**Function************************************************************* + + Synopsis [This function dups the cover and removes DC literals from cubes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Mvc_Cover_t * Mvc_CoverRemoveDontCareLits( Mvc_Cover_t * pCover ) +{ + Mvc_Cover_t * pCoverNew; + Mvc_Cube_t * pCube; + + pCoverNew = Mvc_CoverDup( pCover ); + Mvc_CoverForEachCube( pCoverNew, pCube ) + Mvc_CubeBitRemoveDcs( pCube ); + return pCoverNew; +} + +/**Function************************************************************* + + Synopsis [Returns the cofactor w.r.t. to a binary var.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Mvc_Cover_t * Mvc_CoverCofactor( Mvc_Cover_t * p, int iValue, int iValueOther ) +{ + Mvc_Cover_t * pCover; + Mvc_Cube_t * pCube, * pCubeCopy; + // clone the cover + pCover = Mvc_CoverClone( p ); + // copy the cube list + Mvc_CoverForEachCube( p, pCube ) + if ( Mvc_CubeBitValue( pCube, iValue ) ) + { + pCubeCopy = Mvc_CubeDup( pCover, pCube ); + Mvc_CoverAddCubeTail( pCover, pCubeCopy ); + Mvc_CubeBitInsert( pCubeCopy, iValueOther ); + } + return pCover; +} + +/**Function************************************************************* + + Synopsis [Returns the cover, in which the binary var is complemented.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Mvc_Cover_t * Mvc_CoverFlipVar( Mvc_Cover_t * p, int iValue0, int iValue1 ) +{ + Mvc_Cover_t * pCover; + Mvc_Cube_t * pCube, * pCubeCopy; + int Value0, Value1, Temp; + + assert( iValue0 + 1 == iValue1 ); // should be adjacent + + // clone the cover + pCover = Mvc_CoverClone( p ); + // copy the cube list + Mvc_CoverForEachCube( p, pCube ) + { + pCubeCopy = Mvc_CubeDup( pCover, pCube ); + Mvc_CoverAddCubeTail( pCover, pCubeCopy ); + + // get the bits + Value0 = Mvc_CubeBitValue( pCubeCopy, iValue0 ); + Value1 = Mvc_CubeBitValue( pCubeCopy, iValue1 ); + + // if both bits are one, nothing to swap + if ( Value0 && Value1 ) + continue; + // cannot be both zero because they belong to the same var + assert( Value0 || Value1 ); + + // swap the bits + Temp = Value0; + Value0 = Value1; + Value1 = Temp; + + // set the bits after the swap + if ( Value0 ) + Mvc_CubeBitInsert( pCubeCopy, iValue0 ); + else + Mvc_CubeBitRemove( pCubeCopy, iValue0 ); + + if ( Value1 ) + Mvc_CubeBitInsert( pCubeCopy, iValue1 ); + else + Mvc_CubeBitRemove( pCubeCopy, iValue1 ); + } + return pCover; +} + +/**Function************************************************************* + + Synopsis [Returns the cover derived by universal quantification.] + + Description [Returns the cover computed by universal quantification + as follows: CoverNew = Univ(B) [Cover & (A==B)]. Removes the second + binary var from the support (given by values iValueB0 and iValueB1). + Leaves the first binary variable (given by values iValueA0 and iValueA1) + in the support.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Mvc_Cover_t * Mvc_CoverUnivQuantify( Mvc_Cover_t * p, + int iValueA0, int iValueA1, int iValueB0, int iValueB1 ) +{ + Mvc_Cover_t * pCover; + Mvc_Cube_t * pCube, * pCubeCopy; + int ValueA0, ValueA1, ValueB0, ValueB1; + + // clone the cover + pCover = Mvc_CoverClone( p ); + // copy the cube list + Mvc_CoverForEachCube( p, pCube ) + { + // get the bits + ValueA0 = Mvc_CubeBitValue( pCube, iValueA0 ); + ValueA1 = Mvc_CubeBitValue( pCube, iValueA1 ); + ValueB0 = Mvc_CubeBitValue( pCube, iValueB0 ); + ValueB1 = Mvc_CubeBitValue( pCube, iValueB1 ); + + // cannot be both zero because they belong to the same var + assert( ValueA0 || ValueA1 ); + assert( ValueB0 || ValueB1 ); + + // if the values of this var are different, do not add the cube + if ( ValueA0 != ValueB0 && ValueA1 != ValueB1 ) + continue; + + // create the cube + pCubeCopy = Mvc_CubeDup( pCover, pCube ); + Mvc_CoverAddCubeTail( pCover, pCubeCopy ); + + // insert 1's into for the first var, if both have this value + if ( ValueA0 && ValueB0 ) + Mvc_CubeBitInsert( pCubeCopy, iValueA0 ); + else + Mvc_CubeBitRemove( pCubeCopy, iValueA0 ); + + if ( ValueA1 && ValueB1 ) + Mvc_CubeBitInsert( pCubeCopy, iValueA1 ); + else + Mvc_CubeBitRemove( pCubeCopy, iValueA1 ); + + // insert 1's into for the second var (the cover does not depend on it) + Mvc_CubeBitInsert( pCubeCopy, iValueB0 ); + Mvc_CubeBitInsert( pCubeCopy, iValueB1 ); + } + return pCover; +} + +#if 0 + +/**Function************************************************************* + + Synopsis [Derives the cofactors of the cover.] + + Description [Derives the cofactors w.r.t. a variable and also cubes + that do not depend on this variable.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Mvc_Cover_t ** Mvc_CoverCofactors( Mvc_Data_t * pData, Mvc_Cover_t * pCover, int iVar ) +{ + Mvc_Cover_t ** ppCofs; + Mvc_Cube_t * pCube, * pCubeNew; + int i, nValues, iValueFirst, Res; + + // start the covers for cofactors + iValueFirst = Vm_VarMapReadValuesFirst(pData->pVm, iVar); + nValues = Vm_VarMapReadValues(pData->pVm, iVar); + ppCofs = ALLOC( Mvc_Cover_t *, nValues + 1 ); + for ( i = 0; i <= nValues; i++ ) + ppCofs[i] = Mvc_CoverClone( pCover ); + + // go through the cubes + Mvc_CoverForEachCube( pCover, pCube ) + { + // if the literal if a full literal, add it to last "cofactor" + Mvc_CubeBitEqualUnderMask( Res, pCube, pData->ppMasks[iVar], pData->ppMasks[iVar] ); + if ( Res ) + { + pCubeNew = Mvc_CubeDup(pCover, pCube); + Mvc_CoverAddCubeTail( ppCofs[nValues], pCubeNew ); + continue; + } + + // otherwise, add it to separate values + for ( i = 0; i < nValues; i++ ) + if ( Mvc_CubeBitValue( pCube, iValueFirst + i ) ) + { + pCubeNew = Mvc_CubeDup(pCover, pCube); + Mvc_CubeBitOr( pCubeNew, pCubeNew, pData->ppMasks[iVar] ); + Mvc_CoverAddCubeTail( ppCofs[i], pCubeNew ); + } + } + return ppCofs; +} + +/**Function************************************************************* + + Synopsis [Count the cubes with non-trivial literals with the given value.] + + Description [The data and the cover are given (pData, pCover). Also given + are the variable number and the number of a value of this variable. + This procedure returns the number of cubes having a non-trivial literal + of this variable that have the given value present.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Mvr_CoverCountLitsWithValue( Mvc_Data_t * pData, Mvc_Cover_t * pCover, int iVar, int iValue ) +{ + Mvc_Cube_t * pCube; + int iValueFirst, Res, Counter; + + Counter = 0; + iValueFirst = Vm_VarMapReadValuesFirst( pData->pVm, iVar ); + Mvc_CoverForEachCube( pCover, pCube ) + { + // check if the given literal is the full literal + Mvc_CubeBitEqualUnderMask( Res, pCube, pData->ppMasks[iVar], pData->ppMasks[iVar] ); + if ( Res ) + continue; + // this literal is not a full literal; check if it has this value + Counter += Mvc_CubeBitValue( pCube, iValueFirst + iValue ); + } + return Counter; +} + +/**Function************************************************************* + + Synopsis [Creates the expanded cover.] + + Description [The original cover is expanded by adding some variables. + These variables are the additional variables in pVmNew, compared to + pCvr->pVm. The resulting cover is the same as the original one, except + that it contains the additional variables present as full literals + in every cube.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Mvc_Cover_t * Mvc_CoverCreateExpanded( Mvc_Cover_t * pCover, Vm_VarMap_t * pVmNew ) +{ + Mvc_Cover_t * pCoverNew; + Mvc_Cube_t * pCube, * pCubeNew; + int i, iLast, iLastNew; + + // create the new cover + pCoverNew = Mvc_CoverAlloc( pCover->pMem, Vm_VarMapReadValuesInNum(pVmNew) ); + + // get the cube composed of extra bits + Mvc_CoverAllocateMask( pCoverNew ); + Mvc_CubeBitClean( pCoverNew->pMask ); + for ( i = pCover->nBits; i < pCoverNew->nBits; i++ ) + Mvc_CubeBitInsert( pCoverNew->pMask, i ); + + // get the indexes of the last words in both covers + iLast = pCover->nWords? pCover->nWords - 1: 0; + iLastNew = pCoverNew->nWords? pCoverNew->nWords - 1: 0; + + // create the cubes of the new cover + Mvc_CoverForEachCube( pCover, pCube ) + { + pCubeNew = Mvc_CubeAlloc( pCoverNew ); + Mvc_CubeBitClean( pCubeNew ); + // copy the bits (cannot immediately use Mvc_CubeBitCopy, + // because covers have different numbers of bits) + Mvc_CubeSetLast( pCubeNew, iLast ); + Mvc_CubeBitCopy( pCubeNew, pCube ); + Mvc_CubeSetLast( pCubeNew, iLastNew ); + // add the extra bits + Mvc_CubeBitOr( pCubeNew, pCubeNew, pCoverNew->pMask ); + // add the cube to the new cover + Mvc_CoverAddCubeTail( pCoverNew, pCubeNew ); + } + return pCoverNew; +} + +#endif + +/**Function************************************************************* + + Synopsis [Transposes the cube cover.] + + Description [Returns the cube cover that looks like a transposed + matrix, compared to the matrix derived from the original cover.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Mvc_Cover_t * Mvc_CoverTranspose( Mvc_Cover_t * pCover ) +{ + Mvc_Cover_t * pRes; + Mvc_Cube_t * pCubeRes, * pCube; + int nWord, nBit, i, iCube; + + pRes = Mvc_CoverAlloc( pCover->pMem, Mvc_CoverReadCubeNum(pCover) ); + for ( i = 0; i < pCover->nBits; i++ ) + { + // get the word and bit of this literal + nWord = Mvc_CubeWhichWord(i); + nBit = Mvc_CubeWhichBit(i); + // get the transposed cube + pCubeRes = Mvc_CubeAlloc( pRes ); + Mvc_CubeBitClean( pCubeRes ); + iCube = 0; + Mvc_CoverForEachCube( pCover, pCube ) + { + if ( pCube->pData[nWord] & (1<<nBit) ) + Mvc_CubeBitInsert( pCubeRes, iCube ); + iCube++; + } + Mvc_CoverAddCubeTail( pRes, pCubeRes ); + } + return pRes; +} + +/**Function************************************************************* + + Synopsis [Checks that the cubes of the cover have 0's in unused bits.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Mvc_UtilsCheckUnusedZeros( Mvc_Cover_t * pCover ) +{ + unsigned Unsigned; + Mvc_Cube_t * pCube; + int nCubes; + + nCubes = 0; + Mvc_CoverForEachCube( pCover, pCube ) + { + if ( pCube->nUnused == 0 ) + continue; + + Unsigned = ( pCube->pData[pCube->iLast] & + (BITS_FULL << (32-pCube->nUnused)) ); + if( Unsigned ) + { + printf( "Cube %2d out of %2d contains dirty bits.\n", nCubes, + Mvc_CoverReadCubeNum(pCover) ); + } + nCubes++; + } + return 1; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |