openwrt/upstream - upstream openwrt

	Commit message (Expand)	Author	Age	Files	Lines
*	get rid of $Id$ - it has never helped us and it has broken too many patches ;)	Felix Fietkau	2009-04-17	1	-1/+0
*	Use the openwrt.org mirror, others are offline	Florian Fainelli	2008-11-15	1	-1/+1
*	major target cleanup. it is now possible to have subtargets that can override...	Felix Fietkau	2007-09-08	1	-1/+1
*	strip the kernel version suffix from target directories, except for brcm-2.4 ...	Felix Fietkau	2007-09-06	1	-1/+1
*	add file type autodetection for the unpack command and nuke PKG_CAT:= in lots...	Felix Fietkau	2007-03-16	1	-1/+0
*	same propset here as changeset:6500	Tim Yardley	2007-03-04	1	-1/+1
*	move another DEFAULT:=y and fix a dependency bug	Felix Fietkau	2007-01-14	1	-2/+1
*	Was not selected by default actually :/	Florian Fainelli	2007-01-02	1	-1/+1
*	Include yamonenv by default in au1000 images	Florian Fainelli	2006-12-31	1	-0/+1
*	replace lots of manual install commands with INSTALL_* variables	Felix Fietkau	2006-11-23	1	-1/+1
*	finally move buildroot-ng to trunk	Felix Fietkau	2016-03-20	1	-0/+40

/**CFile**************************************************************** FileName [utilCex.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Handling counter-examples.] Synopsis [Handling counter-examples.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - Feburary 13, 2011.] Revision [$Id: utilCex.c,v 1.00 2011/02/11 00:00:00 alanmi Exp $] ***********************************************************************/ #include <stdio.h> #include <string.h> #include <stdlib.h> #include <assert.h> #include "misc/vec/vec.h" #include "utilCex.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [Allocates a counter-example.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Abc_Cex_t * Abc_CexAlloc( int nRegs, int nRealPis, int nFrames ) { Abc_Cex_t * pCex; int nWords = Abc_BitWordNum( nRegs + nRealPis * nFrames ); pCex = (Abc_Cex_t *)ABC_ALLOC( char, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords ); memset( pCex, 0, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords ); pCex->nRegs = nRegs; pCex->nPis = nRealPis; pCex->nBits = nRegs + nRealPis * nFrames; return pCex; } Abc_Cex_t * Abc_CexAllocFull( int nRegs, int nRealPis, int nFrames ) { Abc_Cex_t * pCex; int nWords = Abc_BitWordNum( nRegs + nRealPis * nFrames ); pCex = (Abc_Cex_t *)ABC_ALLOC( char, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords ); memset( pCex, 0xFF, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords ); pCex->nRegs = nRegs; pCex->nPis = nRealPis; pCex->nBits = nRegs + nRealPis * nFrames; return pCex; } /**Function************************************************************* Synopsis [Make the trivial counter-example for the trivially asserted output.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Abc_Cex_t * Abc_CexMakeTriv( int nRegs, int nTruePis, int nTruePos, int iFrameOut ) { Abc_Cex_t * pCex; int iPo, iFrame; assert( nRegs > 0 ); iPo = iFrameOut % nTruePos; iFrame = iFrameOut / nTruePos; // allocate the counter example pCex = Abc_CexAlloc( nRegs, nTruePis, iFrame + 1 ); pCex->iPo = iPo; pCex->iFrame = iFrame; return pCex; } /**Function************************************************************* Synopsis [Derives the counter-example.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Abc_Cex_t * Abc_CexCreate( int nRegs, int nPis, int * pArray, int iFrame, int iPo, int fSkipRegs ) { Abc_Cex_t * pCex; int i; pCex = Abc_CexAlloc( nRegs, nPis, iFrame+1 ); pCex->iPo = iPo; pCex->iFrame = iFrame; if ( pArray == NULL ) return pCex; if ( fSkipRegs ) { for ( i = nRegs; i < pCex->nBits; i++ ) if ( pArray[i-nRegs] ) Abc_InfoSetBit( pCex->pData, i ); } else { for ( i = 0; i < pCex->nBits; i++ ) if ( pArray[i] ) Abc_InfoSetBit( pCex->pData, i ); } return pCex; } /**Function************************************************************* Synopsis [Make the trivial counter-example for the trivially asserted output.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Abc_Cex_t * Abc_CexDup( Abc_Cex_t * p, int nRegsNew ) { Abc_Cex_t * pCex; int i; if ( p == (Abc_Cex_t *)(ABC_PTRINT_T)1 ) return p; if ( nRegsNew == -1 ) nRegsNew = p->nRegs; pCex = Abc_CexAlloc( nRegsNew, p->nPis, p->iFrame+1 ); pCex->iPo = p->iPo; pCex->iFrame = p->iFrame; for ( i = p->nRegs; i < p->nBits; i++ ) if ( Abc_InfoHasBit(p->pData, i) ) Abc_InfoSetBit( pCex->pData, pCex->nRegs + i - p->nRegs ); return pCex; } /**Function************************************************************* Synopsis [Derives CEX from comb model.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Abc_Cex_t * Abc_CexDeriveFromCombModel( int * pModel, int nPis, int nRegs, int iPo ) { Abc_Cex_t * pCex; int i; pCex = Abc_CexAlloc( nRegs, nPis, 1 ); pCex->iPo = iPo; pCex->iFrame = 0; for ( i = 0; i < nPis; i++ ) if ( pModel[i] ) pCex->pData[i>>5] |= (1<<(i & 31)); return pCex; } /**Function************************************************************* Synopsis [Derives CEX from comb model.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Abc_Cex_t * Abc_CexMerge( Abc_Cex_t * pCex, Abc_Cex_t * pPart, int iFrBeg, int iFrEnd ) { Abc_Cex_t * pNew; int nFramesGain; int i, f, iBit; if ( iFrBeg < 0 ) { printf( "Starting frame is less than 0.\n" ); return NULL; } if ( iFrEnd < 0 ) { printf( "Stopping frame is less than 0.\n" ); return NULL; } if ( iFrBeg > pCex->iFrame ) { printf( "Starting frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; } if ( iFrEnd > pCex->iFrame ) { printf( "Stopping frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; } if ( iFrBeg > iFrEnd ) { printf( "Starting frame (%d) should be less than stopping frame (%d).\n", iFrBeg, iFrEnd ); return NULL; } assert( iFrBeg >= 0 && iFrBeg <= pCex->iFrame ); assert( iFrEnd >= 0 && iFrEnd <= pCex->iFrame ); assert( iFrBeg <= iFrEnd ); assert( pCex->nPis == pPart->nPis ); assert( iFrEnd - iFrBeg + pPart->iPo >= pPart->iFrame ); nFramesGain = iFrEnd - iFrBeg + pPart->iPo - pPart->iFrame; pNew = Abc_CexAlloc( pCex->nRegs, pCex->nPis, pCex->iFrame + 1 - nFramesGain ); pNew->iPo = pCex->iPo; pNew->iFrame = pCex->iFrame - nFramesGain; for ( iBit = 0; iBit < pCex->nRegs; iBit++ ) if ( Abc_InfoHasBit(pCex->pData, iBit) ) Abc_InfoSetBit( pNew->pData, iBit ); for ( f = 0; f < iFrBeg; f++ ) for ( i = 0; i < pCex->nPis; i++, iBit++ ) if ( Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) ) Abc_InfoSetBit( pNew->pData, iBit ); for ( f = 0; f < pPart->iFrame; f++ ) for ( i = 0; i < pCex->nPis; i++, iBit++ ) if ( Abc_InfoHasBit(pPart->pData, pPart->nRegs + pCex->nPis * f + i) ) Abc_InfoSetBit( pNew->pData, iBit ); for ( f = iFrEnd; f <= pCex->iFrame; f++ ) for ( i = 0; i < pCex->nPis; i++, iBit++ ) if ( Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) ) Abc_InfoSetBit( pNew->pData, iBit ); assert( iBit == pNew->nBits ); return pNew; } /**Function************************************************************* Synopsis [Prints out the counter-example.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Abc_CexPrintStats( Abc_Cex_t * p ) { int k, Counter = 0; if ( p == NULL ) { printf( "The counter example is NULL.\n" ); return; } if ( p == (Abc_Cex_t *)(ABC_PTRINT_T)1 ) { printf( "The counter example is present but not available (pointer has value \"1\").\n" ); return; } for ( k = 0; k < p->nBits; k++ ) Counter += Abc_InfoHasBit(p->pData, k); printf( "CEX: Po =%4d Frame =%4d FF = %d PI = %d Bit =%8d 1s =%8d (%5.2f %%)\n", p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits, Counter, 100.0 * Counter / (p->nBits - p->nRegs) ); } void Abc_CexPrintStatsInputs( Abc_Cex_t * p, int nInputs ) { int k, Counter = 0, Counter2 = 0; if ( p == NULL ) { printf( "The counter example is NULL.\n" ); return; } if ( p == (Abc_Cex_t *)(ABC_PTRINT_T)1 ) { printf( "The counter example is present but not available (pointer has value \"1\").\n" ); return; } for ( k = 0; k < p->nBits; k++ ) { Counter += Abc_InfoHasBit(p->pData, k); if ( (k - p->nRegs) % p->nPis < nInputs ) Counter2 += Abc_InfoHasBit(p->pData, k); } printf( "CEX: Po =%4d Frame =%4d FF = %d PI = %d Bit =%8d 1s =%8d (%5.2f %%) 1sIn =%8d (%5.2f %%)\n", p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits, Counter, 100.0 * Counter / (p->nBits - p->nRegs), Counter2, 100.0 * Counter2 / (p->nBits - p->nRegs - (p->iFrame + 1) * (p->nPis - nInputs)) ); } /**Function************************************************************* Synopsis [Prints out the counter-example.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Abc_CexPrint( Abc_Cex_t * p ) { int i, f, k; if ( p == NULL ) { printf( "The counter example is NULL.\n" ); return; } if ( p == (Abc_Cex_t *)(ABC_PTRINT_T)1 ) { printf( "The counter example is present but not available (pointer has value \"1\").\n" ); return; } Abc_CexPrintStats( p ); printf( "State : " ); for ( k = 0; k < p->nRegs; k++ ) printf( "%d", Abc_InfoHasBit(p->pData, k) ); printf( "\n" ); for ( f = 0; f <= p->iFrame; f++ ) { printf( "Frame %3d : ", f ); for ( i = 0; i < p->nPis; i++ ) printf( "%d", Abc_InfoHasBit(p->pData, k++) ); printf( "\n" ); } assert( k == p->nBits ); } /**Function************************************************************* Synopsis [Frees the counter-example.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Abc_CexFreeP( Abc_Cex_t ** p ) { if ( *p == NULL ) return; if ( *p == (Abc_Cex_t *)(ABC_PTRINT_T)1 ) *p = NULL; else ABC_FREE( *p ); } /**Function************************************************************* Synopsis [Frees the counter-example.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Abc_CexFree( Abc_Cex_t * p ) { if ( p == (Abc_Cex_t *)(ABC_PTRINT_T)1 ) return; ABC_FREE( p ); } /**Function************************************************************* Synopsis [Transform CEX after phase abstraction with nFrames frames.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Abc_Cex_t * Abc_CexTransformPhase( Abc_Cex_t * p, int nPisOld, int nPosOld, int nRegsOld ) { Abc_Cex_t * pCex; int nFrames = p->nPis / nPisOld; int nPosNew = nPosOld * nFrames; assert( p->nPis % nPisOld == 0 ); assert( p->iPo < nPosNew ); pCex = Abc_CexDup( p, nRegsOld ); pCex->nPis = nPisOld; pCex->iPo = -1; pCex->iFrame = (p->iFrame + 1) * nFrames - 1; pCex->nBits = p->nBits; return pCex; } /**Function************************************************************* Synopsis [Transform CEX after phase temporal decomposition with nFrames frames.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Abc_Cex_t * Abc_CexTransformTempor( Abc_Cex_t * p, int nPisOld, int nPosOld, int nRegsOld ) { Abc_Cex_t * pCex; int i, k, iBit = nRegsOld, nFrames = p->nPis / nPisOld - 1; assert( p->iFrame > 0 ); // otherwise tempor did not properly check for failures in the prefix assert( p->nPis % nPisOld == 0 ); pCex = Abc_CexAlloc( nRegsOld, nPisOld, nFrames + p->iFrame + 1 ); pCex->iPo = p->iPo; pCex->iFrame = nFrames + p->iFrame; for ( i = 0; i < nFrames; i++ ) for ( k = 0; k < nPisOld; k++, iBit++ ) if ( Abc_InfoHasBit(p->pData, p->nRegs + (i+1)*nPisOld + k) ) Abc_InfoSetBit( pCex->pData, iBit ); for ( i = 0; i <= p->iFrame; i++ ) for ( k = 0; k < nPisOld; k++, iBit++ ) if ( Abc_InfoHasBit(p->pData, p->nRegs + i*p->nPis + k) ) Abc_InfoSetBit( pCex->pData, iBit ); assert( iBit == pCex->nBits ); return pCex; } /**Function************************************************************* Synopsis [Transform CEX after "logic; undc; st; zero".] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Abc_Cex_t * Abc_CexTransformUndc( Abc_Cex_t * p, char * pInit ) { Abc_Cex_t * pCex; int nFlops = strlen(pInit); int i, f, iBit, iAddPi = 0, nAddPis = 0; // count how many flops got a new PI for ( i = 0; i < nFlops; i++ ) nAddPis += (int)(pInit[i] == 'x'); // create new CEX pCex = Abc_CexAlloc( nFlops, p->nPis - nAddPis, p->iFrame + 1 ); pCex->iPo = p->iPo; pCex->iFrame = p->iFrame; for ( iBit = 0; iBit < nFlops; iBit++ ) { if ( pInit[iBit] == '1' || (pInit[iBit] == 'x' && Abc_InfoHasBit(p->pData, p->nRegs + p->nPis - nAddPis + iAddPi)) ) Abc_InfoSetBit( pCex->pData, iBit ); iAddPi += (int)(pInit[iBit] == 'x'); } assert( iAddPi == nAddPis ); // add timeframes for ( f = 0; f <= p->iFrame; f++ ) for ( i = 0; i < pCex->nPis; i++, iBit++ ) if ( Abc_InfoHasBit(p->pData, p->nRegs + p->nPis * f + i) ) Abc_InfoSetBit( pCex->pData, iBit ); assert( iBit == pCex->nBits ); return pCex; } /**Function************************************************************* Synopsis [Derives permuted CEX using permutation of its inputs.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Abc_Cex_t * Abc_CexPermute( Abc_Cex_t * p, Vec_Int_t * vMapOld2New ) { Abc_Cex_t * pCex; int i, iNew; assert( Vec_IntSize(vMapOld2New) == p->nPis ); pCex = Abc_CexAlloc( p->nRegs, p->nPis, p->iFrame+1 ); pCex->iPo = p->iPo; pCex->iFrame = p->iFrame; for ( i = p->nRegs; i < p->nBits; i++ ) if ( Abc_InfoHasBit(p->pData, i) ) { iNew = p->nRegs + p->nPis * ((i - p->nRegs) / p->nPis) + Vec_IntEntry( vMapOld2New, (i - p->nRegs) % p->nPis ); Abc_InfoSetBit( pCex->pData, iNew ); } return pCex; } /**Function************************************************************* Synopsis [Derives permuted CEX using two canonical permutations.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Abc_Cex_t * Abc_CexPermuteTwo( Abc_Cex_t * p, Vec_Int_t * vPermOld, Vec_Int_t * vPermNew ) { Abc_Cex_t * pCex; Vec_Int_t * vPerm; int i, eOld, eNew; assert( Vec_IntSize(vPermOld) == p->nPis ); assert( Vec_IntSize(vPermNew) == p->nPis ); vPerm = Vec_IntStartFull( p->nPis ); Vec_IntForEachEntryTwo( vPermOld, vPermNew, eOld, eNew, i ) Vec_IntWriteEntry( vPerm, eOld, eNew ); pCex = Abc_CexPermute( p, vPerm ); Vec_IntFree( vPerm ); return pCex; } /**Function************************************************************* Synopsis [Count the number of 1s in the CEX.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline int Abc_CexOnes32( unsigned i ) { i = i - ((i >> 1) & 0x55555555); i = (i & 0x33333333) + ((i >> 2) & 0x33333333); i = ((i + (i >> 4)) & 0x0F0F0F0F); return (i*(0x01010101))>>24; } int Abc_CexCountOnes( Abc_Cex_t * p ) { int nWords = Abc_BitWordNum( p->nBits ); int i, Count = 0; for ( i = 0; i < nWords; i++ ) Count += Abc_CexOnes32( p->pData[i] ); return Count; } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END