| /**CFile**************************************************************** |
| |
| FileName [simSupp.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Network and node package.] |
| |
| Synopsis [Simulation to determine functional support.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: simSupp.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "base/abc/abc.h" |
| #include "proof/fraig/fraig.h" |
| #include "sim.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| static int Sim_ComputeSuppRound( Sim_Man_t * p, int fUseTargets ); |
| static int Sim_ComputeSuppRoundNode( Sim_Man_t * p, int iNumCi, int fUseTargets ); |
| static void Sim_ComputeSuppSetTargets( Sim_Man_t * p ); |
| |
| static void Sim_UtilAssignRandom( Sim_Man_t * p ); |
| 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 ); |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Computes structural supports.] |
| |
| Description [Supports are returned as an array of bit strings, one |
| for each CO.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Ptr_t * Sim_ComputeStrSupp( Abc_Ntk_t * pNtk ) |
| { |
| Vec_Ptr_t * vSuppStr; |
| Abc_Obj_t * pNode; |
| unsigned * pSimmNode, * pSimmNode1, * pSimmNode2; |
| int nSuppWords, i, k; |
| // allocate room for structural supports |
| nSuppWords = SIM_NUM_WORDS( Abc_NtkCiNum(pNtk) ); |
| vSuppStr = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nSuppWords, 1 ); |
| // assign the structural support to the PIs |
| Abc_NtkForEachCi( pNtk, pNode, i ) |
| Sim_SuppStrSetVar( vSuppStr, pNode, i ); |
| // derive the structural supports of the internal nodes |
| Abc_NtkForEachNode( pNtk, pNode, i ) |
| { |
| // if ( Abc_NodeIsConst(pNode) ) |
| // continue; |
| pSimmNode = (unsigned *)vSuppStr->pArray[ pNode->Id ]; |
| pSimmNode1 = (unsigned *)vSuppStr->pArray[ Abc_ObjFaninId0(pNode) ]; |
| pSimmNode2 = (unsigned *)vSuppStr->pArray[ Abc_ObjFaninId1(pNode) ]; |
| for ( k = 0; k < nSuppWords; k++ ) |
| pSimmNode[k] = pSimmNode1[k] | pSimmNode2[k]; |
| } |
| // set the structural supports of the PO nodes |
| Abc_NtkForEachCo( pNtk, pNode, i ) |
| { |
| pSimmNode = (unsigned *)vSuppStr->pArray[ pNode->Id ]; |
| pSimmNode1 = (unsigned *)vSuppStr->pArray[ Abc_ObjFaninId0(pNode) ]; |
| for ( k = 0; k < nSuppWords; k++ ) |
| pSimmNode[k] = pSimmNode1[k]; |
| } |
| return vSuppStr; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Compute functional supports.] |
| |
| Description [Supports are returned as an array of bit strings, one |
| for each CO.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose ) |
| { |
| Sim_Man_t * p; |
| Vec_Ptr_t * vResult; |
| int nSolved, i; |
| abctime clk = Abc_Clock(); |
| |
| srand( 0xABC ); |
| |
| // start the simulation manager |
| p = Sim_ManStart( pNtk, 0 ); |
| |
| // compute functional support using one round of random simulation |
| Sim_UtilAssignRandom( p ); |
| Sim_ComputeSuppRound( p, 0 ); |
| |
| // set the support targets |
| Sim_ComputeSuppSetTargets( p ); |
| if ( fVerbose ) |
| printf( "Number of support targets after simulation = %5d.\n", Vec_VecSizeSize(p->vSuppTargs) ); |
| if ( Vec_VecSizeSize(p->vSuppTargs) == 0 ) |
| goto exit; |
| |
| for ( i = 0; i < 1; i++ ) |
| { |
| // compute patterns using one round of random simulation |
| Sim_UtilAssignRandom( p ); |
| nSolved = Sim_ComputeSuppRound( p, 1 ); |
| if ( Vec_VecSizeSize(p->vSuppTargs) == 0 ) |
| goto exit; |
| |
| if ( fVerbose ) |
| printf( "Targets = %5d. Solved = %5d. Fifo = %5d.\n", |
| Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo) ); |
| } |
| |
| // try to solve the support targets |
| while ( Vec_VecSizeSize(p->vSuppTargs) > 0 ) |
| { |
| // solve targets until the first disproved one (which gives counter-example) |
| Sim_SolveTargetsUsingSat( p, p->nSimWords/p->nSuppWords ); |
| // compute additional functional support |
| Sim_UtilAssignFromFifo( p ); |
| nSolved = Sim_ComputeSuppRound( p, 1 ); |
| |
| if ( fVerbose ) |
| printf( "Targets = %5d. Solved = %5d. Fifo = %5d. SAT runs = %3d.\n", |
| Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo), p->nSatRuns ); |
| } |
| |
| exit: |
| p->timeTotal = Abc_Clock() - clk; |
| vResult = p->vSuppFun; |
| // p->vSuppFun = NULL; |
| Sim_ManStop( p ); |
| return vResult; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Computes functional support using one round of simulation.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Sim_ComputeSuppRound( Sim_Man_t * p, int fUseTargets ) |
| { |
| Vec_Ptr_t * vTargets; |
| int i, Counter = 0; |
| abctime clk; |
| // perform one round of random simulation |
| clk = Abc_Clock(); |
| Sim_UtilSimulate( p, 0 ); |
| p->timeSim += Abc_Clock() - clk; |
| // iterate through the CIs and detect COs that depend on them |
| for ( i = p->iInput; i < p->nInputs; i++ ) |
| { |
| vTargets = (Vec_Ptr_t *)p->vSuppTargs->pArray[i]; |
| if ( fUseTargets && vTargets->nSize == 0 ) |
| continue; |
| Counter += Sim_ComputeSuppRoundNode( p, i, fUseTargets ); |
| } |
| return Counter; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Computes functional support for one node.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Sim_ComputeSuppRoundNode( Sim_Man_t * p, int iNumCi, int fUseTargets ) |
| { |
| int fVerbose = 0; |
| Sim_Pat_t * pPat; |
| Vec_Ptr_t * vTargets; |
| Vec_Vec_t * vNodesByLevel; |
| Abc_Obj_t * pNodeCi, * pNode; |
| int i, k, v, Output, LuckyPat, fType0, fType1; |
| int Counter = 0; |
| int fFirst = 1; |
| abctime clk; |
| // collect nodes by level in the TFO of the CI |
| // this procedure does not collect the CIs and COs |
| // but it increments TravId of the collected nodes and CIs/COs |
| clk = Abc_Clock(); |
| pNodeCi = Abc_NtkCi( p->pNtk, iNumCi ); |
| vNodesByLevel = Abc_DfsLevelized( pNodeCi, 0 ); |
| p->timeTrav += Abc_Clock() - clk; |
| // complement the simulation info of the selected CI |
| Sim_UtilInfoFlip( p, pNodeCi ); |
| // simulate the levelized structure of nodes |
| Vec_VecForEachEntry( Abc_Obj_t *, vNodesByLevel, pNode, i, k ) |
| { |
| fType0 = Abc_NodeIsTravIdCurrent( Abc_ObjFanin0(pNode) ); |
| fType1 = Abc_NodeIsTravIdCurrent( Abc_ObjFanin1(pNode) ); |
| clk = Abc_Clock(); |
| Sim_UtilSimulateNode( p, pNode, 1, fType0, fType1 ); |
| p->timeSim += Abc_Clock() - clk; |
| } |
| // set the simulation info of the affected COs |
| if ( fUseTargets ) |
| { |
| vTargets = (Vec_Ptr_t *)p->vSuppTargs->pArray[iNumCi]; |
| for ( i = vTargets->nSize - 1; i >= 0; i-- ) |
| { |
| // get the target output |
| Output = (int)(ABC_PTRUINT_T)vTargets->pArray[i]; |
| // get the target node |
| pNode = Abc_ObjFanin0( Abc_NtkCo(p->pNtk, Output) ); |
| // the output should be in the cone |
| assert( Abc_NodeIsTravIdCurrent(pNode) ); |
| |
| // skip if the simulation info is equal |
| if ( Sim_UtilInfoCompare( p, pNode ) ) |
| continue; |
| |
| // otherwise, we solved a new target |
| Vec_PtrRemove( vTargets, vTargets->pArray[i] ); |
| if ( fVerbose ) |
| printf( "(%d,%d) ", iNumCi, Output ); |
| Counter++; |
| // make sure this variable is not yet detected |
| assert( !Sim_SuppFunHasVar(p->vSuppFun, Output, iNumCi) ); |
| // set this variable |
| Sim_SuppFunSetVar( p->vSuppFun, Output, iNumCi ); |
| |
| // detect the differences in the simulation info |
| Sim_UtilInfoDetectDiffs( (unsigned *)p->vSim0->pArray[pNode->Id], (unsigned *)p->vSim1->pArray[pNode->Id], p->nSimWords, p->vDiffs ); |
| // create new patterns |
| if ( !fFirst && p->vFifo->nSize > 1000 ) |
| continue; |
| |
| Vec_IntForEachEntry( p->vDiffs, LuckyPat, k ) |
| { |
| // set the new pattern |
| pPat = Sim_ManPatAlloc( p ); |
| pPat->Input = iNumCi; |
| pPat->Output = Output; |
| Abc_NtkForEachCi( p->pNtk, pNodeCi, v ) |
| if ( Sim_SimInfoHasVar( p->vSim0, pNodeCi, LuckyPat ) ) |
| Sim_SetBit( pPat->pData, v ); |
| Vec_PtrPush( p->vFifo, pPat ); |
| |
| fFirst = 0; |
| break; |
| } |
| } |
| if ( fVerbose && Counter ) |
| printf( "\n" ); |
| } |
| else |
| { |
| Abc_NtkForEachCo( p->pNtk, pNode, Output ) |
| { |
| if ( !Abc_NodeIsTravIdCurrent( pNode ) ) |
| continue; |
| if ( !Sim_UtilInfoCompare( p, Abc_ObjFanin0(pNode) ) ) |
| { |
| if ( !Sim_SuppFunHasVar(p->vSuppFun, Output, iNumCi) ) |
| { |
| Counter++; |
| Sim_SuppFunSetVar( p->vSuppFun, Output, iNumCi ); |
| } |
| } |
| } |
| } |
| Vec_VecFree( vNodesByLevel ); |
| return Counter; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Sets the simulation targets.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Sim_ComputeSuppSetTargets( Sim_Man_t * p ) |
| { |
| Abc_Obj_t * pNode; |
| unsigned * pSuppStr, * pSuppFun; |
| int i, k, Num; |
| Abc_NtkForEachCo( p->pNtk, pNode, i ) |
| { |
| pSuppStr = (unsigned *)p->vSuppStr->pArray[pNode->Id]; |
| pSuppFun = (unsigned *)p->vSuppFun->pArray[i]; |
| // find vars in the structural support that are not in the functional support |
| Sim_UtilInfoDetectNews( pSuppFun, pSuppStr, p->nSuppWords, p->vDiffs ); |
| Vec_IntForEachEntry( p->vDiffs, Num, k ) |
| Vec_VecPush( p->vSuppTargs, Num, (void *)(ABC_PTRUINT_T)i ); |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Assigns random simulation info to the PIs.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Sim_UtilAssignRandom( Sim_Man_t * p ) |
| { |
| Abc_Obj_t * pNode; |
| unsigned * pSimInfo; |
| int i, k; |
| // assign the random/systematic simulation info to the PIs |
| Abc_NtkForEachCi( p->pNtk, pNode, i ) |
| { |
| pSimInfo = (unsigned *)p->vSim0->pArray[pNode->Id]; |
| for ( k = 0; k < p->nSimWords; k++ ) |
| pSimInfo[k] = SIM_RANDOM_UNSIGNED; |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Sets the new patterns from fifo.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Sim_UtilAssignFromFifo( Sim_Man_t * p ) |
| { |
| int fUseOneWord = 0; |
| Abc_Obj_t * pNode; |
| Sim_Pat_t * pPat; |
| unsigned * pSimInfo; |
| int nWordsNew, iWord, iWordLim, i, w; |
| int iBeg, iEnd; |
| int Counter = 0; |
| // go through the patterns and fill in the dist-1 minterms for each |
| for ( iWord = 0; p->vFifo->nSize > 0; iWord = iWordLim ) |
| { |
| ++Counter; |
| // get the pattern |
| pPat = (Sim_Pat_t *)Vec_PtrPop( p->vFifo ); |
| if ( fUseOneWord ) |
| { |
| // get the first word of the next series |
| iWordLim = iWord + 1; |
| // set the pattern for all PIs from iBit to iWord + p->nInputs |
| iBeg = p->iInput; |
| iEnd = Abc_MinInt( iBeg + 32, p->nInputs ); |
| // for ( i = iBeg; i < iEnd; i++ ) |
| Abc_NtkForEachCi( p->pNtk, pNode, i ) |
| { |
| pNode = Abc_NtkCi(p->pNtk,i); |
| pSimInfo = (unsigned *)p->vSim0->pArray[pNode->Id]; |
| if ( Sim_HasBit(pPat->pData, i) ) |
| pSimInfo[iWord] = SIM_MASK_FULL; |
| else |
| pSimInfo[iWord] = 0; |
| // flip one bit |
| if ( i >= iBeg && i < iEnd ) |
| Sim_XorBit( pSimInfo + iWord, i-iBeg ); |
| } |
| } |
| else |
| { |
| // get the number of words for the remaining inputs |
| nWordsNew = p->nSuppWords; |
| // nWordsNew = SIM_NUM_WORDS( p->nInputs - p->iInput ); |
| // get the first word of the next series |
| iWordLim = (iWord + nWordsNew < p->nSimWords)? iWord + nWordsNew : p->nSimWords; |
| // set the pattern for all CIs from iWord to iWord + nWordsNew |
| Abc_NtkForEachCi( p->pNtk, pNode, i ) |
| { |
| pSimInfo = (unsigned *)p->vSim0->pArray[pNode->Id]; |
| if ( Sim_HasBit(pPat->pData, i) ) |
| { |
| for ( w = iWord; w < iWordLim; w++ ) |
| pSimInfo[w] = SIM_MASK_FULL; |
| } |
| else |
| { |
| for ( w = iWord; w < iWordLim; w++ ) |
| pSimInfo[w] = 0; |
| } |
| Sim_XorBit( pSimInfo + iWord, i ); |
| // flip one bit |
| // if ( i >= p->iInput ) |
| // Sim_XorBit( pSimInfo + iWord, i-p->iInput ); |
| } |
| } |
| Sim_ManPatFree( p, pPat ); |
| // stop if we ran out of room for patterns |
| if ( iWordLim == p->nSimWords ) |
| break; |
| // if ( Counter == 1 ) |
| // break; |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Get the given number of counter-examples using SAT.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Sim_SolveTargetsUsingSat( Sim_Man_t * p, int Limit ) |
| { |
| Fraig_Params_t Params; |
| Fraig_Man_t * pMan; |
| Abc_Obj_t * pNodeCi; |
| Abc_Ntk_t * pMiter; |
| Sim_Pat_t * pPat; |
| void * pEntry; |
| int * pModel; |
| int RetValue, Output, Input, k, v; |
| int Counter = 0; |
| abctime clk; |
| |
| p->nSatRuns = 0; |
| // put targets into one array |
| Vec_VecForEachEntryReverse( void *, p->vSuppTargs, pEntry, Input, k ) |
| { |
| p->nSatRuns++; |
| Output = (int)(ABC_PTRUINT_T)pEntry; |
| |
| // set up the miter for the two cofactors of this output w.r.t. this input |
| pMiter = Abc_NtkMiterForCofactors( p->pNtk, Output, Input, -1 ); |
| |
| // transform the miter into a fraig |
| Fraig_ParamsSetDefault( &Params ); |
| Params.nSeconds = ABC_INFINITY; |
| Params.fInternal = 1; |
| clk = Abc_Clock(); |
| pMan = (Fraig_Man_t *)Abc_NtkToFraig( pMiter, &Params, 0, 0 ); |
| p->timeFraig += Abc_Clock() - clk; |
| clk = Abc_Clock(); |
| Fraig_ManProveMiter( pMan ); |
| p->timeSat += Abc_Clock() - clk; |
| |
| // analyze the result |
| RetValue = Fraig_ManCheckMiter( pMan ); |
| assert( RetValue >= 0 ); |
| if ( RetValue == 1 ) // unsat |
| { |
| p->nSatRunsUnsat++; |
| pModel = NULL; |
| Vec_PtrRemove( (Vec_Ptr_t *)p->vSuppTargs->pArray[Input], pEntry ); |
| } |
| else // sat |
| { |
| p->nSatRunsSat++; |
| pModel = Fraig_ManReadModel( pMan ); |
| assert( pModel != NULL ); |
| assert( Sim_SolveSuppModelVerify( p->pNtk, pModel, Input, Output ) ); |
| |
| //printf( "Solved by SAT (%d,%d).\n", Input, Output ); |
| // set the new pattern |
| pPat = Sim_ManPatAlloc( p ); |
| pPat->Input = Input; |
| pPat->Output = Output; |
| Abc_NtkForEachCi( p->pNtk, pNodeCi, v ) |
| if ( pModel[v] ) |
| Sim_SetBit( pPat->pData, v ); |
| Vec_PtrPush( p->vFifo, pPat ); |
| /* |
| // set the new pattern |
| pPat = Sim_ManPatAlloc( p ); |
| pPat->Input = Input; |
| pPat->Output = Output; |
| Abc_NtkForEachCi( p->pNtk, pNodeCi, v ) |
| if ( pModel[v] ) |
| Sim_SetBit( pPat->pData, v ); |
| Sim_XorBit( pPat->pData, Input ); // add this bit in the opposite polarity |
| Vec_PtrPush( p->vFifo, pPat ); |
| */ |
| Counter++; |
| } |
| // delete the fraig manager |
| Fraig_ManFree( pMan ); |
| // delete the miter |
| Abc_NtkDelete( pMiter ); |
| |
| // makr the input, which we are processing |
| p->iInput = Input; |
| |
| // stop when we found enough patterns |
| // if ( Counter == Limit ) |
| if ( Counter == 1 ) |
| return; |
| } |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Saves the counter example.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Sim_NtkSimTwoPats_rec( Abc_Obj_t * pNode ) |
| { |
| int Value0, Value1; |
| if ( Abc_NodeIsTravIdCurrent( pNode ) ) |
| return (int)(ABC_PTRUINT_T)pNode->pCopy; |
| Abc_NodeSetTravIdCurrent( pNode ); |
| Value0 = Sim_NtkSimTwoPats_rec( Abc_ObjFanin0(pNode) ); |
| Value1 = Sim_NtkSimTwoPats_rec( Abc_ObjFanin1(pNode) ); |
| if ( Abc_ObjFaninC0(pNode) ) |
| Value0 = ~Value0; |
| if ( Abc_ObjFaninC1(pNode) ) |
| Value1 = ~Value1; |
| pNode->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)(Value0 & Value1); |
| return Value0 & Value1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Verifies that pModel proves the presence of Input in the support of Output.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Sim_SolveSuppModelVerify( Abc_Ntk_t * pNtk, int * pModel, int Input, int Output ) |
| { |
| Abc_Obj_t * pNode; |
| int RetValue, i; |
| // set the PI values |
| Abc_NtkIncrementTravId( pNtk ); |
| Abc_NtkForEachCi( pNtk, pNode, i ) |
| { |
| Abc_NodeSetTravIdCurrent( pNode ); |
| if ( pNode == Abc_NtkCi(pNtk,Input) ) |
| pNode->pCopy = (Abc_Obj_t *)1; |
| else if ( pModel[i] == 1 ) |
| pNode->pCopy = (Abc_Obj_t *)3; |
| else |
| pNode->pCopy = NULL; |
| } |
| // perform the traversal |
| RetValue = 3 & Sim_NtkSimTwoPats_rec( Abc_ObjFanin0( Abc_NtkCo(pNtk,Output) ) ); |
| // assert( RetValue == 1 || RetValue == 2 ); |
| return RetValue == 1 || RetValue == 2; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
