src/opt/sim/simSupp.c File Reference

#include "abc.h"
#include "fraig.h"
#include "sim.h"
Include dependency graph for simSupp.c:

Go to the source code of this file.

Functions

static int Sim_ComputeSuppRound (Sim_Man_t *p, bool fUseTargets)
static int Sim_ComputeSuppRoundNode (Sim_Man_t *p, int iNumCi, bool 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)
Vec_Ptr_t * Sim_ComputeStrSupp (Abc_Ntk_t *pNtk)
Vec_Ptr_t * Sim_ComputeFunSupp (Abc_Ntk_t *pNtk, int fVerbose)
int Sim_NtkSimTwoPats_rec (Abc_Obj_t *pNode)

Function Documentation

Vec_Ptr_t* Sim_ComputeFunSupp ( Abc_Ntk_t *  pNtk,
int  fVerbose 
)

Function*************************************************************

Synopsis [Compute functional supports.]

Description [Supports are returned as an array of bit strings, one for each CO.]

SideEffects []

SeeAlso []

Definition at line 100 of file simSupp.c.

00101 {
00102     Sim_Man_t * p;
00103     Vec_Ptr_t * vResult;
00104     int nSolved, i, clk = clock();
00105 
00106     srand( 0xABC );
00107 
00108     // start the simulation manager
00109     p = Sim_ManStart( pNtk, 0 );
00110 
00111     // compute functional support using one round of random simulation
00112     Sim_UtilAssignRandom( p );
00113     Sim_ComputeSuppRound( p, 0 );
00114 
00115     // set the support targets 
00116     Sim_ComputeSuppSetTargets( p );
00117 if ( fVerbose )
00118     printf( "Number of support targets after simulation = %5d.\n", Vec_VecSizeSize(p->vSuppTargs) );
00119     if ( Vec_VecSizeSize(p->vSuppTargs) == 0 )
00120         goto exit;
00121 
00122     for ( i = 0; i < 1; i++ )
00123     {
00124         // compute patterns using one round of random simulation
00125         Sim_UtilAssignRandom( p );
00126         nSolved = Sim_ComputeSuppRound( p, 1 );
00127         if ( Vec_VecSizeSize(p->vSuppTargs) == 0 )
00128             goto exit;
00129 
00130 if ( fVerbose )
00131     printf( "Targets = %5d.   Solved = %5d.  Fifo = %5d.\n", 
00132        Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo) );
00133     }
00134 
00135     // try to solve the support targets
00136     while ( Vec_VecSizeSize(p->vSuppTargs) > 0 )
00137     {
00138         // solve targets until the first disproved one (which gives counter-example)
00139         Sim_SolveTargetsUsingSat( p, p->nSimWords/p->nSuppWords );
00140         // compute additional functional support
00141         Sim_UtilAssignFromFifo( p );
00142         nSolved = Sim_ComputeSuppRound( p, 1 );
00143 
00144 if ( fVerbose )
00145     printf( "Targets = %5d.   Solved = %5d.  Fifo = %5d.  SAT runs = %3d.\n", 
00146             Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo), p->nSatRuns );
00147     }
00148 
00149 exit:
00150 p->timeTotal = clock() - clk;
00151     vResult = p->vSuppFun;  
00152     //  p->vSuppFun = NULL;
00153     Sim_ManStop( p );
00154     return vResult;
00155 }

Vec_Ptr_t* Sim_ComputeStrSupp ( Abc_Ntk_t *  pNtk  ) 

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Computes structural supports.]

Description [Supports are returned as an array of bit strings, one for each CO.]

SideEffects []

SeeAlso []

Definition at line 54 of file simSupp.c.

00055 {
00056     Vec_Ptr_t * vSuppStr;
00057     Abc_Obj_t * pNode;
00058     unsigned * pSimmNode, * pSimmNode1, * pSimmNode2;
00059     int nSuppWords, i, k;
00060     // allocate room for structural supports
00061     nSuppWords = SIM_NUM_WORDS( Abc_NtkCiNum(pNtk) );
00062     vSuppStr   = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nSuppWords, 1 );
00063     // assign the structural support to the PIs
00064     Abc_NtkForEachCi( pNtk, pNode, i )
00065         Sim_SuppStrSetVar( vSuppStr, pNode, i );
00066     // derive the structural supports of the internal nodes
00067     Abc_NtkForEachNode( pNtk, pNode, i )
00068     {
00069 //        if ( Abc_NodeIsConst(pNode) )
00070 //            continue;
00071         pSimmNode  = vSuppStr->pArray[ pNode->Id ];
00072         pSimmNode1 = vSuppStr->pArray[ Abc_ObjFaninId0(pNode) ];
00073         pSimmNode2 = vSuppStr->pArray[ Abc_ObjFaninId1(pNode) ];
00074         for ( k = 0; k < nSuppWords; k++ )
00075             pSimmNode[k] = pSimmNode1[k] | pSimmNode2[k];
00076     }
00077     // set the structural supports of the PO nodes
00078     Abc_NtkForEachCo( pNtk, pNode, i )
00079     {
00080         pSimmNode  = vSuppStr->pArray[ pNode->Id ];
00081         pSimmNode1 = vSuppStr->pArray[ Abc_ObjFaninId0(pNode) ];
00082         for ( k = 0; k < nSuppWords; k++ )
00083             pSimmNode[k] = pSimmNode1[k];
00084     }
00085     return vSuppStr;
00086 }

int Sim_ComputeSuppRound ( Sim_Man_t *  p,
bool  fUseTargets 
) [static]

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

] DECLARATIONS ///

Function*************************************************************

Synopsis [Computes functional support using one round of simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 168 of file simSupp.c.

00169 {
00170     Vec_Int_t * vTargets;
00171     int i, Counter = 0;
00172     int clk;
00173     // perform one round of random simulation
00174 clk = clock();
00175     Sim_UtilSimulate( p, 0 );
00176 p->timeSim += clock() - clk;
00177     // iterate through the CIs and detect COs that depend on them
00178     for ( i = p->iInput; i < p->nInputs; i++ )
00179     {
00180         vTargets = p->vSuppTargs->pArray[i];
00181         if ( fUseTargets && vTargets->nSize == 0 )
00182             continue;
00183         Counter += Sim_ComputeSuppRoundNode( p, i, fUseTargets );
00184     }
00185     return Counter;
00186 }

int Sim_ComputeSuppRoundNode ( Sim_Man_t *  p,
int  iNumCi,
bool  fUseTargets 
) [static]

Function*************************************************************

Synopsis [Computes functional support for one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 199 of file simSupp.c.

00200 {
00201     int fVerbose = 0;
00202     Sim_Pat_t * pPat;
00203     Vec_Int_t * vTargets;
00204     Vec_Vec_t * vNodesByLevel;
00205     Abc_Obj_t * pNodeCi, * pNode;
00206     int i, k, v, Output, LuckyPat, fType0, fType1;
00207     int Counter = 0;
00208     int fFirst = 1;
00209     int clk;
00210     // collect nodes by level in the TFO of the CI 
00211     // this proceduredoes not collect the CIs and COs
00212     // but it increments TravId of the collected nodes and CIs/COs
00213 clk = clock();
00214     pNodeCi       = Abc_NtkCi( p->pNtk, iNumCi );
00215     vNodesByLevel = Abc_DfsLevelized( pNodeCi, 0 );
00216 p->timeTrav += clock() - clk;
00217     // complement the simulation info of the selected CI
00218     Sim_UtilInfoFlip( p, pNodeCi );
00219     // simulate the levelized structure of nodes
00220     Vec_VecForEachEntry( vNodesByLevel, pNode, i, k )
00221     {
00222         fType0 = Abc_NodeIsTravIdCurrent( Abc_ObjFanin0(pNode) );
00223         fType1 = Abc_NodeIsTravIdCurrent( Abc_ObjFanin1(pNode) );
00224 clk = clock();
00225         Sim_UtilSimulateNode( p, pNode, 1, fType0, fType1 );
00226 p->timeSim += clock() - clk;
00227     }
00228     // set the simulation info of the affected COs
00229     if ( fUseTargets )
00230     {
00231         vTargets = p->vSuppTargs->pArray[iNumCi];
00232         for ( i = vTargets->nSize - 1; i >= 0; i-- )
00233         {
00234             // get the target output
00235             Output = vTargets->pArray[i];
00236             // get the target node
00237             pNode  = Abc_ObjFanin0( Abc_NtkCo(p->pNtk, Output) );
00238             // the output should be in the cone
00239             assert( Abc_NodeIsTravIdCurrent(pNode) );
00240 
00241             // skip if the simulation info is equal
00242             if ( Sim_UtilInfoCompare( p, pNode ) )
00243                 continue;
00244 
00245             // otherwise, we solved a new target
00246             Vec_IntRemove( vTargets, Output );
00247 if ( fVerbose )
00248     printf( "(%d,%d) ", iNumCi, Output );
00249             Counter++;
00250             // make sure this variable is not yet detected
00251             assert( !Sim_SuppFunHasVar(p->vSuppFun, Output, iNumCi) );
00252             // set this variable
00253             Sim_SuppFunSetVar( p->vSuppFun, Output, iNumCi );
00254             
00255             // detect the differences in the simulation info
00256             Sim_UtilInfoDetectDiffs( p->vSim0->pArray[pNode->Id], p->vSim1->pArray[pNode->Id], p->nSimWords, p->vDiffs );
00257             // create new patterns
00258             if ( !fFirst && p->vFifo->nSize > 1000 )
00259                 continue;
00260 
00261             Vec_IntForEachEntry( p->vDiffs, LuckyPat, k )
00262             {
00263                 // set the new pattern
00264                 pPat = Sim_ManPatAlloc( p );
00265                 pPat->Input  = iNumCi;
00266                 pPat->Output = Output;
00267                 Abc_NtkForEachCi( p->pNtk, pNodeCi, v )
00268                     if ( Sim_SimInfoHasVar( p->vSim0, pNodeCi, LuckyPat ) )
00269                         Sim_SetBit( pPat->pData, v );
00270                 Vec_PtrPush( p->vFifo, pPat );
00271 
00272                 fFirst = 0;
00273                 break;
00274             }
00275         }
00276 if ( fVerbose && Counter )
00277 printf( "\n" );
00278     }
00279     else
00280     {
00281         Abc_NtkForEachCo( p->pNtk, pNode, Output )
00282         {
00283             if ( !Abc_NodeIsTravIdCurrent( pNode ) )
00284                 continue;
00285             if ( !Sim_UtilInfoCompare( p, Abc_ObjFanin0(pNode) ) )
00286             {
00287                 if ( !Sim_SuppFunHasVar(p->vSuppFun, Output, iNumCi) )
00288                 {
00289                     Counter++;
00290                     Sim_SuppFunSetVar( p->vSuppFun, Output, iNumCi );
00291                 }
00292             }
00293         }
00294     }
00295     Vec_VecFree( vNodesByLevel );
00296     return Counter;
00297 }

void Sim_ComputeSuppSetTargets ( Sim_Man_t *  p  )  [static]

Function*************************************************************

Synopsis [Sets the simulation targets.]

Description []

SideEffects []

SeeAlso []

Definition at line 310 of file simSupp.c.

00311 {
00312     Abc_Obj_t * pNode;
00313     unsigned * pSuppStr, * pSuppFun;
00314     int i, k, Num;
00315     Abc_NtkForEachCo( p->pNtk, pNode, i )
00316     {
00317         pSuppStr = p->vSuppStr->pArray[pNode->Id];
00318         pSuppFun = p->vSuppFun->pArray[i];
00319         // find vars in the structural support that are not in the functional support
00320         Sim_UtilInfoDetectNews( pSuppFun, pSuppStr, p->nSuppWords, p->vDiffs );
00321         Vec_IntForEachEntry( p->vDiffs, Num, k )
00322             Vec_VecPush( p->vSuppTargs, Num, (void *)i );
00323     }
00324 }

int Sim_NtkSimTwoPats_rec ( Abc_Obj_t *  pNode  ) 

Function*************************************************************

Synopsis [Saves the counter example.]

Description []

SideEffects []

SeeAlso []

Definition at line 544 of file simSupp.c.

00545 {
00546     int Value0, Value1;
00547     if ( Abc_NodeIsTravIdCurrent( pNode ) )
00548         return (int)pNode->pCopy;
00549     Abc_NodeSetTravIdCurrent( pNode );
00550     Value0 = Sim_NtkSimTwoPats_rec( Abc_ObjFanin0(pNode) );
00551     Value1 = Sim_NtkSimTwoPats_rec( Abc_ObjFanin1(pNode) );
00552     if ( Abc_ObjFaninC0(pNode) )
00553         Value0 = ~Value0;
00554     if ( Abc_ObjFaninC1(pNode) )
00555         Value1 = ~Value1;
00556     pNode->pCopy = (Abc_Obj_t *)(Value0 & Value1);
00557     return Value0 & Value1;
00558 }

int Sim_SolveSuppModelVerify ( Abc_Ntk_t *  pNtk,
int *  pModel,
int  Input,
int  Output 
) [static]

Function*************************************************************

Synopsis [Verifies that pModel proves the presence of Input in the support of Output.]

Description []

SideEffects []

SeeAlso []

Definition at line 571 of file simSupp.c.

00572 {
00573     Abc_Obj_t * pNode;
00574     int RetValue, i;
00575     // set the PI values
00576     Abc_NtkIncrementTravId( pNtk );
00577     Abc_NtkForEachCi( pNtk, pNode, i )
00578     {
00579         Abc_NodeSetTravIdCurrent( pNode );
00580         if ( pNode == Abc_NtkCi(pNtk,Input) )
00581             pNode->pCopy = (Abc_Obj_t *)1;
00582         else if ( pModel[i] == 1 )
00583             pNode->pCopy = (Abc_Obj_t *)3;
00584         else
00585             pNode->pCopy = NULL;
00586     }
00587     // perform the traversal
00588     RetValue = 3 & Sim_NtkSimTwoPats_rec( Abc_ObjFanin0( Abc_NtkCo(pNtk,Output) ) );
00589 //    assert( RetValue == 1 || RetValue == 2 ); 
00590     return RetValue == 1 || RetValue == 2;
00591 }

void Sim_SolveTargetsUsingSat ( Sim_Man_t *  p,
int  Limit 
) [static]

Function*************************************************************

Synopsis [Get the given number of counter-examples using SAT.]

Description []

SideEffects []

SeeAlso []

Definition at line 445 of file simSupp.c.

00446 {
00447     Fraig_Params_t Params;
00448     Fraig_Man_t * pMan;
00449     Abc_Obj_t * pNodeCi;
00450     Abc_Ntk_t * pMiter;
00451     Sim_Pat_t * pPat;
00452     void * pEntry;
00453     int * pModel;
00454     int RetValue, Output, Input, k, v;
00455     int Counter = 0;
00456     int clk;
00457 
00458     p->nSatRuns = 0;
00459     // put targets into one array
00460     Vec_VecForEachEntryReverse( p->vSuppTargs, pEntry, Input, k )
00461     {
00462         p->nSatRuns++;
00463         Output = (int)pEntry;
00464 
00465         // set up the miter for the two cofactors of this output w.r.t. this input
00466         pMiter = Abc_NtkMiterForCofactors( p->pNtk, Output, Input, -1 );
00467 
00468         // transform the miter into a fraig
00469         Fraig_ParamsSetDefault( &Params );
00470         Params.nSeconds = ABC_INFINITY;
00471         Params.fInternal = 1;
00472 clk = clock();
00473         pMan = Abc_NtkToFraig( pMiter, &Params, 0, 0 ); 
00474 p->timeFraig += clock() - clk;
00475 clk = clock();
00476         Fraig_ManProveMiter( pMan );
00477 p->timeSat += clock() - clk;
00478 
00479         // analyze the result
00480         RetValue = Fraig_ManCheckMiter( pMan );
00481         assert( RetValue >= 0 );
00482         if ( RetValue == 1 ) // unsat
00483         {
00484             p->nSatRunsUnsat++;
00485             pModel = NULL;
00486             Vec_PtrRemove( p->vSuppTargs->pArray[Input], pEntry );
00487         }
00488         else // sat
00489         {
00490             p->nSatRunsSat++;
00491             pModel = Fraig_ManReadModel( pMan );
00492             assert( pModel != NULL );
00493             assert( Sim_SolveSuppModelVerify( p->pNtk, pModel, Input, Output ) );
00494 
00495 //printf( "Solved by SAT (%d,%d).\n", Input, Output );
00496             // set the new pattern
00497             pPat = Sim_ManPatAlloc( p );
00498             pPat->Input  = Input;
00499             pPat->Output = Output;
00500             Abc_NtkForEachCi( p->pNtk, pNodeCi, v )
00501                 if ( pModel[v] )
00502                     Sim_SetBit( pPat->pData, v );
00503             Vec_PtrPush( p->vFifo, pPat );
00504 /*
00505             // set the new pattern
00506             pPat = Sim_ManPatAlloc( p );
00507             pPat->Input  = Input;
00508             pPat->Output = Output;
00509             Abc_NtkForEachCi( p->pNtk, pNodeCi, v )
00510                 if ( pModel[v] )
00511                     Sim_SetBit( pPat->pData, v );
00512             Sim_XorBit( pPat->pData, Input );  // add this bit in the opposite polarity
00513             Vec_PtrPush( p->vFifo, pPat );
00514 */
00515             Counter++;
00516         }
00517         // delete the fraig manager
00518         Fraig_ManFree( pMan );
00519         // delete the miter
00520         Abc_NtkDelete( pMiter );
00521 
00522         // makr the input, which we are processing
00523         p->iInput = Input;
00524 
00525         // stop when we found enough patterns
00526 //        if ( Counter == Limit )
00527         if ( Counter == 1 )
00528             return;
00529     }
00530 }

void Sim_UtilAssignFromFifo ( Sim_Man_t *  p  )  [static]

Function*************************************************************

Synopsis [Sets the new patterns from fifo.]

Description []

SideEffects []

SeeAlso []

Definition at line 362 of file simSupp.c.

00363 {
00364     int fUseOneWord = 0;
00365     Abc_Obj_t * pNode;
00366     Sim_Pat_t * pPat;
00367     unsigned * pSimInfo;
00368     int nWordsNew, iWord, iWordLim, i, w;
00369     int iBeg, iEnd;
00370     int Counter = 0;
00371     // go through the patterns and fill in the dist-1 minterms for each
00372     for ( iWord = 0; p->vFifo->nSize > 0; iWord = iWordLim )
00373     {
00374         ++Counter;
00375         // get the pattern
00376         pPat = Vec_PtrPop( p->vFifo );
00377         if ( fUseOneWord )
00378         {
00379             // get the first word of the next series
00380             iWordLim = iWord + 1; 
00381             // set the pattern for all PIs from iBit to iWord + p->nInputs
00382             iBeg = p->iInput;
00383             iEnd = ABC_MIN( iBeg + 32, p->nInputs );
00384 //            for ( i = iBeg; i < iEnd; i++ )
00385             Abc_NtkForEachCi( p->pNtk, pNode, i )
00386             {
00387                 pNode = Abc_NtkCi(p->pNtk,i);
00388                 pSimInfo = p->vSim0->pArray[pNode->Id];
00389                 if ( Sim_HasBit(pPat->pData, i) )
00390                     pSimInfo[iWord] = SIM_MASK_FULL;
00391                 else
00392                     pSimInfo[iWord] = 0;
00393                 // flip one bit
00394                 if ( i >= iBeg && i < iEnd )
00395                     Sim_XorBit( pSimInfo + iWord, i-iBeg );
00396             }
00397         }
00398         else
00399         {
00400             // get the number of words for the remaining inputs
00401             nWordsNew = p->nSuppWords;
00402 //            nWordsNew = SIM_NUM_WORDS( p->nInputs - p->iInput );
00403             // get the first word of the next series
00404             iWordLim = (iWord + nWordsNew < p->nSimWords)? iWord + nWordsNew : p->nSimWords; 
00405             // set the pattern for all CIs from iWord to iWord + nWordsNew
00406             Abc_NtkForEachCi( p->pNtk, pNode, i )
00407             {
00408                 pSimInfo = p->vSim0->pArray[pNode->Id];
00409                 if ( Sim_HasBit(pPat->pData, i) )
00410                 {
00411                     for ( w = iWord; w < iWordLim; w++ )
00412                         pSimInfo[w] = SIM_MASK_FULL;
00413                 }
00414                 else
00415                 {
00416                     for ( w = iWord; w < iWordLim; w++ )
00417                         pSimInfo[w] = 0;
00418                 }
00419                 Sim_XorBit( pSimInfo + iWord, i );
00420                 // flip one bit
00421 //                if ( i >= p->iInput )
00422 //                    Sim_XorBit( pSimInfo + iWord, i-p->iInput );
00423             }
00424         }
00425         Sim_ManPatFree( p, pPat );
00426         // stop if we ran out of room for patterns
00427         if ( iWordLim == p->nSimWords )
00428             break;
00429 //        if ( Counter == 1 )
00430 //            break;
00431     }
00432 }

void Sim_UtilAssignRandom ( Sim_Man_t *  p  )  [static]

Function*************************************************************

Synopsis [Assigns random simulation info to the PIs.]

Description []

SideEffects []

SeeAlso []

Definition at line 337 of file simSupp.c.

00338 {
00339     Abc_Obj_t * pNode;
00340     unsigned * pSimInfo;
00341     int i, k;
00342     // assign the random/systematic simulation info to the PIs
00343     Abc_NtkForEachCi( p->pNtk, pNode, i )
00344     {
00345         pSimInfo = p->vSim0->pArray[pNode->Id];
00346         for ( k = 0; k < p->nSimWords; k++ )
00347             pSimInfo[k] = SIM_RANDOM_UNSIGNED;
00348     }
00349 }

Generated on Tue Jan 5 12:19:35 2010 for abc70930 by  doxygen 1.6.1