From 0c6505a26a537dc911b6566f82d759521e527c08 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 30 Jan 2008 20:01:00 -0800 Subject: Version abc80130_2 --- src/opt/sim/module.make | 1 + src/opt/sim/sim.h | 38 ++++++--- src/opt/sim/simMan.c | 43 +++++----- src/opt/sim/simSat.c | 2 +- src/opt/sim/simSeq.c | 171 +++++++++++++++++++++++++++++++++++++++ src/opt/sim/simSupp.c | 17 ++-- src/opt/sim/simSwitch.c | 6 +- src/opt/sim/simSym.c | 5 +- src/opt/sim/simSymSat.c | 8 +- src/opt/sim/simSymSim.c | 12 +-- src/opt/sim/simSymStr.c | 12 +-- src/opt/sim/simUtils.c | 210 +++++++++++++++++++++++++++++++++++++++++++++--- 12 files changed, 454 insertions(+), 71 deletions(-) create mode 100644 src/opt/sim/simSeq.c (limited to 'src/opt/sim') diff --git a/src/opt/sim/module.make b/src/opt/sim/module.make index 43d0a125..54058402 100644 --- a/src/opt/sim/module.make +++ b/src/opt/sim/module.make @@ -1,5 +1,6 @@ SRC += src/opt/sim/simMan.c \ src/opt/sim/simSat.c \ + src/opt/sim/simSeq.c \ src/opt/sim/simSupp.c \ src/opt/sim/simSwitch.c \ src/opt/sim/simSym.c \ diff --git a/src/opt/sim/sim.h b/src/opt/sim/sim.h index afed7190..7fcf5ae6 100644 --- a/src/opt/sim/sim.h +++ b/src/opt/sim/sim.h @@ -17,10 +17,14 @@ Revision [$Id: sim.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ - + #ifndef __SIM_H__ #define __SIM_H__ +#ifdef __cplusplus +extern "C" { +#endif + /* The ideas realized in this package are described in the paper: "Detecting Symmetries in Boolean Functions using Circuit Representation, @@ -98,6 +102,7 @@ struct Sim_Man_t_ Abc_Ntk_t * pNtk; int nInputs; int nOutputs; + int fLightweight; // internal simulation information int nSimBits; // the number of bits in simulation info int nSimWords; // the number of words in simulation info @@ -135,11 +140,11 @@ struct Sim_Pat_t_ }; //////////////////////////////////////////////////////////////////////// -/// MACRO DEFITIONS /// +/// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -#define SIM_NUM_WORDS(n) ((n)/32 + (((n)%32) > 0)) -#define SIM_LAST_BITS(n) ((((n)%32) > 0)? (n)%32 : 32) +#define SIM_NUM_WORDS(n) (((n)>>5) + (((n)&31) > 0)) +#define SIM_LAST_BITS(n) ((((n)&31) > 0)? (n)&31 : 32) #define SIM_MASK_FULL (0xFFFFFFFF) #define SIM_MASK_BEG(n) (SIM_MASK_FULL >> (32-n)) @@ -162,6 +167,7 @@ struct Sim_Pat_t_ #define Sim_SuppFunHasVar(vSupps,Output,v) Sim_HasBit((unsigned*)(vSupps)->pArray[Output],(v)) #define Sim_SimInfoSetVar(vSupps,pNode,v) Sim_SetBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v)) #define Sim_SimInfoHasVar(vSupps,pNode,v) Sim_HasBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v)) +#define Sim_SimInfoGet(vInfo,pNode) ((unsigned *)((vInfo)->pArray[(pNode)->Id])) //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// @@ -171,11 +177,14 @@ struct Sim_Pat_t_ extern Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk, int fVerbose ); extern void Sym_ManStop( Sym_Man_t * p ); extern void Sym_ManPrintStats( Sym_Man_t * p ); -extern Sim_Man_t * Sim_ManStart( Abc_Ntk_t * pNtk ); +extern Sim_Man_t * Sim_ManStart( Abc_Ntk_t * pNtk, int fLightweight ); extern void Sim_ManStop( Sim_Man_t * p ); extern void Sim_ManPrintStats( Sim_Man_t * p ); extern Sim_Pat_t * Sim_ManPatAlloc( Sim_Man_t * p ); extern void Sim_ManPatFree( Sim_Man_t * p, Sim_Pat_t * pPat ); +/*=== simSeq.c ==========================================================*/ +extern Vec_Ptr_t * Sim_SimulateSeqRandom( Abc_Ntk_t * pNtk, int nFrames, int nWords ); +extern Vec_Ptr_t * Sim_SimulateSeqModel( Abc_Ntk_t * pNtk, int nFrames, int * pModel ); /*=== simSupp.c ==========================================================*/ extern Vec_Ptr_t * Sim_ComputeStrSupp( Abc_Ntk_t * pNtk ); extern Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose ); @@ -197,17 +206,28 @@ extern void Sim_UtilInfoFlip( Sim_Man_t * p, Abc_Obj_t * pNode ); extern bool Sim_UtilInfoCompare( Sim_Man_t * p, Abc_Obj_t * pNode ); extern void Sim_UtilSimulate( Sim_Man_t * p, bool fFirst ); extern void Sim_UtilSimulateNode( Sim_Man_t * p, Abc_Obj_t * pNode, bool fType, bool fType1, bool fType2 ); -extern void Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords ); +extern void Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords, int nOffset ); +extern void Sim_UtilTransferNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords, int nOffset, int fShift ); extern int Sim_UtilCountSuppSizes( Sim_Man_t * p, int fStruct ); extern int Sim_UtilCountOnes( unsigned * pSimInfo, int nSimWords ); -extern void Sim_UtilGetRandom( unsigned * pPatRand, int nSimWords ); +extern Vec_Int_t * Sim_UtilCountOnesArray( Vec_Ptr_t * vInfo, int nSimWords ); +extern void Sim_UtilSetRandom( unsigned * pPatRand, int nSimWords ); +extern void Sim_UtilSetCompl( unsigned * pPatRand, int nSimWords ); +extern void Sim_UtilSetConst( unsigned * pPatRand, int nSimWords, int fConst1 ); +extern int Sim_UtilInfoIsEqual( unsigned * pPats1, unsigned * pPats2, int nSimWords ); +extern int Sim_UtilInfoIsImp( unsigned * pPats1, unsigned * pPats2, int nSimWords ); +extern int Sim_UtilInfoIsClause( unsigned * pPats1, unsigned * pPats2, int nSimWords ); extern int Sim_UtilCountAllPairs( Vec_Ptr_t * vSuppFun, int nSimWords, Vec_Int_t * vCounters ); extern void Sim_UtilCountPairsAll( Sym_Man_t * p ); extern int Sim_UtilMatrsAreDisjoint( Sym_Man_t * p ); +#ifdef __cplusplus +} +#endif + +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif - diff --git a/src/opt/sim/simMan.c b/src/opt/sim/simMan.c index 780ecfd8..3b50ad84 100644 --- a/src/opt/sim/simMan.c +++ b/src/opt/sim/simMan.c @@ -26,12 +26,12 @@ //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFITIONS /// +/// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* - Synopsis [Starts the simulatin manager.] + Synopsis [Starts the simulation manager.] Description [] @@ -83,7 +83,7 @@ Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk, int fVerbose ) /**Function************************************************************* - Synopsis [Stops the simulatin manager.] + Synopsis [Stops the simulation manager.] Description [] @@ -149,11 +149,9 @@ void Sym_ManPrintStats( Sym_Man_t * p ) } - - /**Function************************************************************* - Synopsis [Starts the simulatin manager.] + Synopsis [Starts the simulation manager.] Description [] @@ -162,7 +160,7 @@ void Sym_ManPrintStats( Sym_Man_t * p ) SeeAlso [] ***********************************************************************/ -Sim_Man_t * Sim_ManStart( Abc_Ntk_t * pNtk ) +Sim_Man_t * Sim_ManStart( Abc_Ntk_t * pNtk, int fLightweight ) { Sim_Man_t * p; // start the manager @@ -175,24 +173,27 @@ Sim_Man_t * Sim_ManStart( Abc_Ntk_t * pNtk ) p->nSimBits = 2048; p->nSimWords = SIM_NUM_WORDS(p->nSimBits); p->vSim0 = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), p->nSimWords, 0 ); - p->vSim1 = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), p->nSimWords, 0 ); - // support information - p->nSuppBits = Abc_NtkCiNum(pNtk); - p->nSuppWords = SIM_NUM_WORDS(p->nSuppBits); - p->vSuppStr = Sim_ComputeStrSupp( pNtk ); - p->vSuppFun = Sim_UtilInfoAlloc( Abc_NtkCoNum(p->pNtk), p->nSuppWords, 1 ); - // other data - p->pMmPat = Extra_MmFixedStart( sizeof(Sim_Pat_t) + p->nSuppWords * sizeof(unsigned) ); - p->vFifo = Vec_PtrAlloc( 100 ); - p->vDiffs = Vec_IntAlloc( 100 ); - // allocate support targets (array of unresolved outputs for each input) - p->vSuppTargs = Vec_VecStart( p->nInputs ); + p->fLightweight = fLightweight; + if (!p->fLightweight) { + p->vSim1 = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), p->nSimWords, 0 ); + // support information + p->nSuppBits = Abc_NtkCiNum(pNtk); + p->nSuppWords = SIM_NUM_WORDS(p->nSuppBits); + p->vSuppStr = Sim_ComputeStrSupp( pNtk ); + p->vSuppFun = Sim_UtilInfoAlloc( Abc_NtkCoNum(p->pNtk), p->nSuppWords, 1 ); + // other data + p->pMmPat = Extra_MmFixedStart( sizeof(Sim_Pat_t) + p->nSuppWords * sizeof(unsigned) ); + p->vFifo = Vec_PtrAlloc( 100 ); + p->vDiffs = Vec_IntAlloc( 100 ); + // allocate support targets (array of unresolved outputs for each input) + p->vSuppTargs = Vec_VecStart( p->nInputs ); + } return p; } /**Function************************************************************* - Synopsis [Stops the simulatin manager.] + Synopsis [Stops the simulation manager.] Description [] @@ -209,7 +210,7 @@ void Sim_ManStop( Sim_Man_t * p ) if ( p->vSuppStr ) Sim_UtilInfoFree( p->vSuppStr ); // if ( p->vSuppFun ) Sim_UtilInfoFree( p->vSuppFun ); if ( p->vSuppTargs ) Vec_VecFree( p->vSuppTargs ); - if ( p->pMmPat ) Extra_MmFixedStop( p->pMmPat, 0 ); + if ( p->pMmPat ) Extra_MmFixedStop( p->pMmPat ); if ( p->vFifo ) Vec_PtrFree( p->vFifo ); if ( p->vDiffs ) Vec_IntFree( p->vDiffs ); free( p ); diff --git a/src/opt/sim/simSat.c b/src/opt/sim/simSat.c index b4e080fe..d514f7f2 100644 --- a/src/opt/sim/simSat.c +++ b/src/opt/sim/simSat.c @@ -26,7 +26,7 @@ //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFITIONS /// +/// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* diff --git a/src/opt/sim/simSeq.c b/src/opt/sim/simSeq.c new file mode 100644 index 00000000..49fb939f --- /dev/null +++ b/src/opt/sim/simSeq.c @@ -0,0 +1,171 @@ +/**CFile**************************************************************** + + FileName [simSeq.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Simulation for sequential circuits.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: simUtils.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "sim.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Sim_SimulateSeqFrame( Vec_Ptr_t * vInfo, Abc_Ntk_t * pNtk, int iFrames, int nWords, int fTransfer ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Simulates sequential circuit.] + + Description [Takes sequential circuit (pNtk). Simulates the given number + (nFrames) of the circuit with the given number of machine words (nWords) + of random simulation data, starting from the initial state. If the initial + state of some latches is a don't-care, uses random input for that latch.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Sim_SimulateSeqRandom( Abc_Ntk_t * pNtk, int nFrames, int nWords ) +{ + Vec_Ptr_t * vInfo; + Abc_Obj_t * pNode; + int i; + assert( Abc_NtkIsStrash(pNtk) ); + vInfo = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nWords * nFrames, 0 ); + // set the constant data + pNode = Abc_AigConst1(pNtk); + Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nWords * nFrames, 1 ); + // set the random PI data + Abc_NtkForEachPi( pNtk, pNode, i ) + Sim_UtilSetRandom( Sim_SimInfoGet(vInfo,pNode), nWords * nFrames ); + // set the initial state data + Abc_NtkForEachLatch( pNtk, pNode, i ) + if ( Abc_LatchIsInit0(pNode) ) + Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nWords, 0 ); + else if ( Abc_LatchIsInit1(pNode) ) + Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nWords, 1 ); + else + Sim_UtilSetRandom( Sim_SimInfoGet(vInfo,pNode), nWords ); + // simulate the nodes for the given number of timeframes + for ( i = 0; i < nFrames; i++ ) + Sim_SimulateSeqFrame( vInfo, pNtk, i, nWords, (int)(i < nFrames-1) ); + return vInfo; +} + +/**Function************************************************************* + + Synopsis [Simulates sequential circuit.] + + Description [Takes sequential circuit (pNtk). Simulates the given number + (nFrames) of the circuit with the given model. The model is assumed to + contain values of PIs for each frame. The latches are initialized to + the initial state. One word of data is simulated.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Sim_SimulateSeqModel( Abc_Ntk_t * pNtk, int nFrames, int * pModel ) +{ + Vec_Ptr_t * vInfo; + Abc_Obj_t * pNode; + unsigned * pUnsigned; + int i, k; + vInfo = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nFrames, 0 ); + // set the constant data + pNode = Abc_AigConst1(pNtk); + Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nFrames, 1 ); + // set the random PI data + Abc_NtkForEachPi( pNtk, pNode, i ) + { + pUnsigned = Sim_SimInfoGet(vInfo,pNode); + for ( k = 0; k < nFrames; k++ ) + pUnsigned[k] = pModel[k * Abc_NtkPiNum(pNtk) + i] ? ~((unsigned)0) : 0; + } + // set the initial state data + Abc_NtkForEachLatch( pNtk, pNode, i ) + { + pUnsigned = Sim_SimInfoGet(vInfo,pNode); + if ( Abc_LatchIsInit0(pNode) ) + pUnsigned[0] = 0; + else if ( Abc_LatchIsInit1(pNode) ) + pUnsigned[0] = ~((unsigned)0); + else + pUnsigned[0] = SIM_RANDOM_UNSIGNED; + } + // simulate the nodes for the given number of timeframes + for ( i = 0; i < nFrames; i++ ) + Sim_SimulateSeqFrame( vInfo, pNtk, i, 1, (int)(i < nFrames-1) ); +/* + // print the simulated values + for ( i = 0; i < nFrames; i++ ) + { + printf( "Frame %d : ", i+1 ); + Abc_NtkForEachPi( pNtk, pNode, k ) + printf( "%d", Sim_SimInfoGet(vInfo,pNode)[i] > 0 ); + printf( " " ); + Abc_NtkForEachLatch( pNtk, pNode, k ) + printf( "%d", Sim_SimInfoGet(vInfo,pNode)[i] > 0 ); + printf( " " ); + Abc_NtkForEachPo( pNtk, pNode, k ) + printf( "%d", Sim_SimInfoGet(vInfo,pNode)[i] > 0 ); + printf( "\n" ); + } + printf( "\n" ); +*/ + return vInfo; +} + +/**Function************************************************************* + + Synopsis [Simulates one frame of sequential circuit.] + + Description [Assumes that the latches and POs are already initialized. + In the end transfers the data to the latches of the next frame.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_SimulateSeqFrame( Vec_Ptr_t * vInfo, Abc_Ntk_t * pNtk, int iFrames, int nWords, int fTransfer ) +{ + Abc_Obj_t * pNode; + int i; + Abc_NtkForEachNode( pNtk, pNode, i ) + Sim_UtilSimulateNodeOne( pNode, vInfo, nWords, iFrames * nWords ); + Abc_NtkForEachPo( pNtk, pNode, i ) + Sim_UtilTransferNodeOne( pNode, vInfo, nWords, iFrames * nWords, 0 ); + if ( !fTransfer ) + return; + Abc_NtkForEachLatch( pNtk, pNode, i ) + Sim_UtilTransferNodeOne( pNode, vInfo, nWords, iFrames * nWords, 1 ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/sim/simSupp.c b/src/opt/sim/simSupp.c index 576e19cc..f7048f4a 100644 --- a/src/opt/sim/simSupp.c +++ b/src/opt/sim/simSupp.c @@ -35,10 +35,8 @@ static void Sim_UtilAssignFromFifo( Sim_Man_t * p ); static void Sim_SolveTargetsUsingSat( Sim_Man_t * p, int nCounters ); static int Sim_SolveSuppModelVerify( Abc_Ntk_t * pNtk, int * pModel, int Input, int Output ); -extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes ); - //////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFITIONS /// +/// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* @@ -68,8 +66,8 @@ Vec_Ptr_t * Sim_ComputeStrSupp( Abc_Ntk_t * pNtk ) // derive the structural supports of the internal nodes Abc_NtkForEachNode( pNtk, pNode, i ) { - if ( Abc_NodeIsConst(pNode) ) - continue; +// if ( Abc_NodeIsConst(pNode) ) +// continue; pSimmNode = vSuppStr->pArray[ pNode->Id ]; pSimmNode1 = vSuppStr->pArray[ Abc_ObjFaninId0(pNode) ]; pSimmNode2 = vSuppStr->pArray[ Abc_ObjFaninId1(pNode) ]; @@ -108,7 +106,7 @@ Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose ) srand( 0xABC ); // start the simulation manager - p = Sim_ManStart( pNtk ); + p = Sim_ManStart( pNtk, 0 ); // compute functional support using one round of random simulation Sim_UtilAssignRandom( p ); @@ -469,9 +467,10 @@ void Sim_SolveTargetsUsingSat( Sim_Man_t * p, int Limit ) // transform the miter into a fraig Fraig_ParamsSetDefault( &Params ); + Params.nSeconds = ABC_INFINITY; Params.fInternal = 1; clk = clock(); - pMan = Abc_NtkToFraig( pMiter, &Params, 0 ); + pMan = Abc_NtkToFraig( pMiter, &Params, 0, 0 ); p->timeFraig += clock() - clk; clk = clock(); Fraig_ManProveMiter( pMan ); @@ -587,10 +586,6 @@ int Sim_SolveSuppModelVerify( Abc_Ntk_t * pNtk, int * pModel, int Input, int Out } // perform the traversal RetValue = 3 & Sim_NtkSimTwoPats_rec( Abc_ObjFanin0( Abc_NtkCo(pNtk,Output) ) ); - if ( RetValue == 0 || RetValue == 3 ) - { - int x = 0; - } // assert( RetValue == 1 || RetValue == 2 ); return RetValue == 1 || RetValue == 2; } diff --git a/src/opt/sim/simSwitch.c b/src/opt/sim/simSwitch.c index b43597f3..218d4d59 100644 --- a/src/opt/sim/simSwitch.c +++ b/src/opt/sim/simSwitch.c @@ -29,7 +29,7 @@ static void Sim_NodeSimulate( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimW static float Sim_ComputeSwitching( unsigned * pSimInfo, int nSimWords ); //////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFITIONS /// +/// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* @@ -65,7 +65,7 @@ Vec_Int_t * Sim_NtkComputeSwitching( Abc_Ntk_t * pNtk, int nPatterns ) Abc_NtkForEachCi( pNtk, pNode, i ) { pSimInfo = Vec_PtrEntry(vSimInfo, pNode->Id); - Sim_UtilGetRandom( pSimInfo, nSimWords ); + Sim_UtilSetRandom( pSimInfo, nSimWords ); pSwitching[pNode->Id] = Sim_ComputeSwitching( pSimInfo, nSimWords ); } // simulate the internal nodes @@ -73,7 +73,7 @@ Vec_Int_t * Sim_NtkComputeSwitching( Abc_Ntk_t * pNtk, int nPatterns ) Vec_PtrForEachEntry( vNodes, pNode, i ) { pSimInfo = Vec_PtrEntry(vSimInfo, pNode->Id); - Sim_UtilSimulateNodeOne( pNode, vSimInfo, nSimWords ); + Sim_UtilSimulateNodeOne( pNode, vSimInfo, nSimWords, 0 ); pSwitching[pNode->Id] = Sim_ComputeSwitching( pSimInfo, nSimWords ); } Vec_PtrFree( vNodes ); diff --git a/src/opt/sim/simSym.c b/src/opt/sim/simSym.c index c452bb1b..71de5b05 100644 --- a/src/opt/sim/simSym.c +++ b/src/opt/sim/simSym.c @@ -26,7 +26,7 @@ //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFITIONS /// +/// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* @@ -71,7 +71,7 @@ p->timeStruct = clock() - clk; for ( i = 1; i <= 1000; i++ ) { // simulate this pattern - Sim_UtilGetRandom( p->uPatRand, p->nSimWords ); + Sim_UtilSetRandom( p->uPatRand, p->nSimWords ); Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms ); if ( i % 50 != 0 ) continue; @@ -125,6 +125,7 @@ p->timeStruct = clock() - clk; if ( fVerbose ) printf( "Total = %8d. Sym = %8d. NonSym = %8d. Remaining = %8d.\n", p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem ); +// Sim_UtilCountPairsAllPrint( p ); Result = p->nPairsSymm; vResult = p->vMatrSymms; diff --git a/src/opt/sim/simSymSat.c b/src/opt/sim/simSymSat.c index db9917b3..7690a891 100644 --- a/src/opt/sim/simSymSat.c +++ b/src/opt/sim/simSymSat.c @@ -26,11 +26,10 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -extern int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned * pPattern ); -extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes ); +static int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned * pPattern ); //////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFITIONS /// +/// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* @@ -145,9 +144,10 @@ int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned * Params.fInternal = 1; Params.nPatsRand = 512; Params.nPatsDyna = 512; + Params.nSeconds = ABC_INFINITY; clk = clock(); - pMan = Abc_NtkToFraig( pMiter, &Params, 0 ); + pMan = Abc_NtkToFraig( pMiter, &Params, 0, 0 ); p->timeFraig += clock() - clk; clk = clock(); Fraig_ManProveMiter( pMan ); diff --git a/src/opt/sim/simSymSim.c b/src/opt/sim/simSymSim.c index 94028c47..2282825b 100644 --- a/src/opt/sim/simSymSim.c +++ b/src/opt/sim/simSymSim.c @@ -29,7 +29,7 @@ static void Sim_SymmsCreateSquare( Sym_Man_t * p, unsigned * pPat ); static void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNode, Vec_Ptr_t * vMatrsNonSym, int Output ); //////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFITIONS /// +/// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* @@ -55,9 +55,9 @@ void Sim_SymmsSimulate( Sym_Man_t * p, unsigned * pPat, Vec_Ptr_t * vMatrsNonSym clk = clock(); Vec_PtrForEachEntry( p->vNodes, pNode, i ) { - if ( Abc_NodeIsConst(pNode) ) - continue; - Sim_UtilSimulateNodeOne( pNode, p->vSim, p->nSimWords ); +// if ( Abc_NodeIsConst(pNode) ) +// continue; + Sim_UtilSimulateNodeOne( pNode, p->vSim, p->nSimWords, 0 ); } p->timeSim += clock() - clk; // collect info into the CO matrices @@ -65,8 +65,8 @@ clk = clock(); Abc_NtkForEachCo( p->pNtk, pNode, i ) { pNode = Abc_ObjFanin0(pNode); - if ( Abc_ObjIsCi(pNode) || Abc_NodeIsConst(pNode) ) - continue; +// if ( Abc_ObjIsCi(pNode) || Abc_AigNodeIsConst(pNode) ) +// continue; nPairsTotal = Vec_IntEntry(p->vPairsTotal, i); nPairsSym = Vec_IntEntry(p->vPairsSym, i); nPairsNonSym = Vec_IntEntry(p->vPairsNonSym,i); diff --git a/src/opt/sim/simSymStr.c b/src/opt/sim/simSymStr.c index ed7e93bf..d52c4328 100644 --- a/src/opt/sim/simSymStr.c +++ b/src/opt/sim/simSymStr.c @@ -41,7 +41,7 @@ static void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * v static int * Sim_SymmsCreateMap( Abc_Ntk_t * pNtk ); //////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFITIONS /// +/// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* @@ -74,15 +74,16 @@ void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs, Vec_Ptr_t * v vNodes = Abc_NtkDfs( pNtk, 0 ); Vec_PtrForEachEntry( vNodes, pTemp, i ) { - if ( Abc_NodeIsConst(pTemp) ) - continue; +// if ( Abc_NodeIsConst(pTemp) ) +// continue; Sim_SymmsStructComputeOne( pNtk, pTemp, pMap ); } // collect the results for the COs; Abc_NtkForEachCo( pNtk, pTemp, i ) { +//printf( "Output %d:\n", i ); pTemp = Abc_ObjFanin0(pTemp); - if ( Abc_ObjIsCi(pTemp) || Abc_NodeIsConst(pTemp) ) + if ( Abc_ObjIsCi(pTemp) || Abc_AigNodeIsConst(pTemp) ) continue; Sim_SymmsTransferToMatrix( Vec_PtrEntry(vMatrs, i), SIM_READ_SYMMS(pTemp), Vec_PtrEntry(vSuppFun, i) ); } @@ -92,7 +93,7 @@ void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs, Vec_Ptr_t * v Abc_NtkForEachCi( pNtk, pTemp, i ) Vec_IntFree( SIM_READ_SYMMS(pTemp) ); Vec_PtrForEachEntry( vNodes, pTemp, i ) - if ( !Abc_NodeIsConst(pTemp) ) +// if ( !Abc_NodeIsConst(pTemp) ) Vec_IntFree( SIM_READ_SYMMS(pTemp) ); Vec_PtrFree( vNodes ); free( pMap ); @@ -444,6 +445,7 @@ void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms, u uSymm = (unsigned)vSymms->pArray[i]; Ind1 = (uSymm & 0xffff); Ind2 = (uSymm >> 16); +//printf( "%d,%d ", Ind1, Ind2 ); // skip variables that are not in the true support assert( Sim_HasBit(pSupport, Ind1) == Sim_HasBit(pSupport, Ind2) ); if ( !Sim_HasBit(pSupport, Ind1) || !Sim_HasBit(pSupport, Ind2) ) diff --git a/src/opt/sim/simUtils.c b/src/opt/sim/simUtils.c index 4b89c650..b0660001 100644 --- a/src/opt/sim/simUtils.c +++ b/src/opt/sim/simUtils.c @@ -37,7 +37,7 @@ static int bit_count[256] = { }; //////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFITIONS /// +/// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* @@ -232,9 +232,6 @@ void Sim_UtilSimulateNode( Sim_Man_t * p, Abc_Obj_t * pNode, bool fType, bool fT // simulate the internal nodes if ( Abc_ObjIsNode(pNode) ) { - if ( Abc_NodeIsConst(pNode) ) - return; - if ( fType ) pSimmNode = p->vSim1->pArray[ pNode->Id ]; else @@ -299,17 +296,18 @@ void Sim_UtilSimulateNode( Sim_Man_t * p, Abc_Obj_t * pNode, bool fType, bool fT SeeAlso [] ***********************************************************************/ -void Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords ) +void Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords, int nOffset ) { unsigned * pSimmNode, * pSimmNode1, * pSimmNode2; int k, fComp1, fComp2; // simulate the internal nodes assert( Abc_ObjIsNode(pNode) ); - if ( Abc_NodeIsConst(pNode) ) - return; pSimmNode = Vec_PtrEntry(vSimInfo, pNode->Id); pSimmNode1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode)); pSimmNode2 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId1(pNode)); + pSimmNode += nOffset; + pSimmNode1 += nOffset; + pSimmNode2 += nOffset; fComp1 = Abc_ObjFaninC0(pNode); fComp2 = Abc_ObjFaninC1(pNode); if ( fComp1 && fComp2 ) @@ -326,6 +324,36 @@ void Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimW pSimmNode[k] = pSimmNode1[k] & pSimmNode2[k]; } +/**Function************************************************************* + + Synopsis [Simulates one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_UtilTransferNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords, int nOffset, int fShift ) +{ + unsigned * pSimmNode, * pSimmNode1; + int k, fComp1; + // simulate the internal nodes + assert( Abc_ObjIsCo(pNode) ); + pSimmNode = Vec_PtrEntry(vSimInfo, pNode->Id); + pSimmNode1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode)); + pSimmNode += nOffset + (fShift > 0)*nSimWords; + pSimmNode1 += nOffset; + fComp1 = Abc_ObjFaninC0(pNode); + if ( fComp1 ) + for ( k = 0; k < nSimWords; k++ ) + pSimmNode[k] = ~pSimmNode1[k]; + else + for ( k = 0; k < nSimWords; k++ ) + pSimmNode[k] = pSimmNode1[k]; +} + /**Function************************************************************* Synopsis [Returns 1 if the simulation infos are equal.] @@ -380,10 +408,31 @@ int Sim_UtilCountOnes( unsigned * pSimInfo, int nSimWords ) return nOnes; } +/**Function************************************************************* + + Synopsis [Counts the number of 1's in the bitstring.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Sim_UtilCountOnesArray( Vec_Ptr_t * vInfo, int nSimWords ) +{ + Vec_Int_t * vCounters; + unsigned * pSimInfo; + int i; + vCounters = Vec_IntStart( Vec_PtrSize(vInfo) ); + Vec_PtrForEachEntry( vInfo, pSimInfo, i ) + Vec_IntWriteEntry( vCounters, i, Sim_UtilCountOnes(pSimInfo, nSimWords) ); + return vCounters; +} /**Function************************************************************* - Synopsis [Returns the random pattern.] + Synopsis [Returns random patterns.] Description [] @@ -392,13 +441,111 @@ int Sim_UtilCountOnes( unsigned * pSimInfo, int nSimWords ) SeeAlso [] ***********************************************************************/ -void Sim_UtilGetRandom( unsigned * pPatRand, int nSimWords ) +void Sim_UtilSetRandom( unsigned * pPatRand, int nSimWords ) { int k; for ( k = 0; k < nSimWords; k++ ) pPatRand[k] = SIM_RANDOM_UNSIGNED; } +/**Function************************************************************* + + Synopsis [Returns complemented patterns.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_UtilSetCompl( unsigned * pPatRand, int nSimWords ) +{ + int k; + for ( k = 0; k < nSimWords; k++ ) + pPatRand[k] = ~pPatRand[k]; +} + +/**Function************************************************************* + + Synopsis [Returns constant patterns.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_UtilSetConst( unsigned * pPatRand, int nSimWords, int fConst1 ) +{ + int k; + for ( k = 0; k < nSimWords; k++ ) + pPatRand[k] = 0; + if ( fConst1 ) + Sim_UtilSetCompl( pPatRand, nSimWords ); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if equal.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sim_UtilInfoIsEqual( unsigned * pPats1, unsigned * pPats2, int nSimWords ) +{ + int k; + for ( k = 0; k < nSimWords; k++ ) + if ( pPats1[k] != pPats2[k] ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if Node1 implies Node2.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sim_UtilInfoIsImp( unsigned * pPats1, unsigned * pPats2, int nSimWords ) +{ + int k; + for ( k = 0; k < nSimWords; k++ ) + if ( pPats1[k] & ~pPats2[k] ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if Node1 v Node2 is always true.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sim_UtilInfoIsClause( unsigned * pPats1, unsigned * pPats2, int nSimWords ) +{ + int k; + for ( k = 0; k < nSimWords; k++ ) + if ( ~pPats1[k] & ~pPats2[k] ) + return 0; + return 1; +} + /**Function************************************************************* Synopsis [Counts the total number of pairs.] @@ -449,6 +596,51 @@ int Sim_UtilCountPairsOne( Extra_BitMat_t * pMat, Vec_Int_t * vSupport ) return Counter; } +/**Function************************************************************* + + Synopsis [Counts the number of entries in the array of matrices.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sim_UtilCountPairsOnePrint( Extra_BitMat_t * pMat, Vec_Int_t * vSupport ) +{ + int i, k, Index1, Index2; + Vec_IntForEachEntry( vSupport, i, Index1 ) + Vec_IntForEachEntryStart( vSupport, k, Index2, Index1+1 ) + if ( Extra_BitMatrixLookup1( pMat, i, k ) ) + printf( "(%d,%d) ", i, k ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Counts the number of entries in the array of matrices.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sim_UtilCountPairsAllPrint( Sym_Man_t * p ) +{ + int i, clk; +clk = clock(); + for ( i = 0; i < p->nOutputs; i++ ) + { + printf( "Output %2d :", i ); + Sim_UtilCountPairsOnePrint( Vec_PtrEntry(p->vMatrSymms, i), Vec_VecEntry(p->vSupports, i) ); + printf( "\n" ); + } +p->timeCount += clock() - clk; +} + /**Function************************************************************* Synopsis [Counts the number of entries in the array of matrices.] -- cgit v1.2.3