abc/src/base/abc/abcUtil.c
/**Function*************************************************************

  Synopsis    [Derives the AIG representing a property.]

  Description [Given is a sequential logic network (Abc_Ntk_t) and 
  an array of nodes (vector of object IDs) and their values (vector of 0s or 1s).
  This procedure creates a sequential AIG (Abc_Ntk_t), which can be given to a 
  sequential model checker (in particular "pdr") to prove that the given 
  combination of values never appears at the intenal nodes of the network, 
  or produce a counter-example showing that it can appear.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Function
Synopsis    [Derives the AIG representing a property.]

Description [Given is a sequential logic network (Abc_Ntk_t) and
an array of nodes (vector of object IDs) and their values (vector of 0s or 1s).
This procedure creates a sequential AIG (Abc_Ntk_t), which can be given to a
sequential model checker (in particular "pdr") to prove that the given
combination of values never appears at the intenal nodes of the network,
or produce a counter-example showing that it can appear.]




Function Synopsis [ Derives the AIG representing a property . ] Description [ Given is a sequential logic network ( Abc_Ntk_t ) and an array of nodes ( vector of object IDs ) and their values ( vector of 0s or 1s ) . This procedure creates a sequential AIG ( Abc_Ntk_t ) which can be given to a sequential model checker ( in particular " pdr " ) to prove that the given combination of values never appears at the intenal nodes of the network or produce a counter - example showing that it can appear . ]
Abc_Ntk_t * Abc_NtkCreatePropertyMonitor( Abc_Ntk_t * p, Vec_Int_t * vNodeIds, Vec_Int_t * vNodeValues )
{
    Abc_Ntk_t * pMonitor, * pStrashed, * pResult;
    int fLatchConst  =   1;
    int fLatchEqual  =   1;
    int fSaveNames   =   1;
    int fUseMvSweep  =   0;
    int nFramesSymb  =   1;
    int nFramesSatur = 512;
    int fVerbose     =   0;
    int fVeryVerbose =   0;
    assert( Abc_NtkIsLogic(p) );
    assert( Abc_NtkLatchNum(p) > 0 );
    assert( Vec_IntSize(vNodeIds) > 0 );
    assert( Vec_IntSize(vNodeIds) == Vec_IntSize(vNodeValues) );
    pMonitor = Abc_NtkDeriveWithOnePo( p, vNodeIds, vNodeValues );
    pStrashed = Abc_NtkStrash( pMonitor, 0, 1, 0 );
    Abc_NtkDelete( pMonitor );
    pResult = Abc_NtkDarLatchSweep( pStrashed, fLatchConst, fLatchEqual, fSaveNames, fUseMvSweep, nFramesSymb, nFramesSatur, fVerbose, fVeryVerbose );
    Abc_NtkDelete( pStrashed );
    return pResult;
}
Abc_Ntk_t * Abc_NtkCreatePropertyMonitor ( Abc_Ntk_t * p , Vec_Int_t * vNodeIds , Vec_Int_t * vNodeValues ) { Abc_Ntk_t * pMonitor , * pStrashed , * pResult ; int fLatchConst = 1 ; int fLatchEqual = 1 ; int fSaveNames = 1 ; int fUseMvSweep = 0 ; int nFramesSymb = 1 ; int nFramesSatur = 512 ; int fVerbose = 0 ; int fVeryVerbose = 0 ; assert ( Abc_NtkIsLogic ( p ) ) ; assert ( Abc_NtkLatchNum ( p ) > 0 ) ; assert ( Vec_IntSize ( vNodeIds ) > 0 ) ; assert ( Vec_IntSize ( vNodeIds ) == Vec_IntSize ( vNodeValues ) ) ; pMonitor = Abc_NtkDeriveWithOnePo ( p , vNodeIds , vNodeValues ) ; pStrashed = Abc_NtkStrash ( pMonitor , 0 , 1 , 0 ) ; Abc_NtkDelete ( pMonitor ) ; pResult = Abc_NtkDarLatchSweep ( pStrashed , fLatchConst , fLatchEqual , fSaveNames , fUseMvSweep , nFramesSymb , nFramesSatur , fVerbose , fVeryVerbose ) ; Abc_NtkDelete ( pStrashed ) ; return pResult ; }
Function
Synopsis    [Derives the AIG representing a property.]
Function Synopsis [ Derives the AIG representing a property . ]
// sequential cleanup parameters // expecting sequential logic network // derive ABC network whose only output is 1 iff the given nodes have the given values // perform structural hashing // it is a good idea to run sequential cleanup before giving the network to PDR