mirror of https://github.com/YosysHQ/abc.git
584 lines
19 KiB
C
584 lines
19 KiB
C
/**CFile****************************************************************
|
|
|
|
FileName [abcFraig.c]
|
|
|
|
SystemName [ABC: Logic synthesis and verification system.]
|
|
|
|
PackageName [Network and node package.]
|
|
|
|
Synopsis [Procedures interfacing with the FRAIG package.]
|
|
|
|
Author [Alan Mishchenko]
|
|
|
|
Affiliation [UC Berkeley]
|
|
|
|
Date [Ver. 1.0. Started - June 20, 2005.]
|
|
|
|
Revision [$Id: abcFraig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
|
|
|
***********************************************************************/
|
|
|
|
#include "abc.h"
|
|
#include "fraig.h"
|
|
#include "main.h"
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// DECLARATIONS ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes );
|
|
static Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
|
|
static Abc_Obj_t * Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFraig );
|
|
|
|
static int Abc_NtkFraigTrustCheck( Abc_Ntk_t * pNtk );
|
|
static void Abc_NtkFraigTrustOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
|
|
static Abc_Obj_t * Abc_NodeFraigTrust( Abc_Aig_t * pMan, Abc_Obj_t * pNode );
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// FUNCTION DEFITIONS ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Interfaces the network with the FRAIG package.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes )
|
|
{
|
|
int fCheck = 1;
|
|
Abc_Ntk_t * pNtkNew;
|
|
Fraig_Man_t * pMan;
|
|
// perform fraiging
|
|
pMan = Abc_NtkToFraig( pNtk, pParams, fAllNodes );
|
|
// prove the miter if asked to
|
|
if ( ((Fraig_Params_t *)pParams)->fTryProve )
|
|
Fraig_ManProveMiter( pMan );
|
|
// reconstruct FRAIG in the new network
|
|
pNtkNew = Abc_NtkFromFraig( pMan, pNtk );
|
|
Fraig_ManFree( pMan );
|
|
// make sure that everything is okay
|
|
if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
|
|
{
|
|
printf( "Abc_NtkFraig: The network check has failed.\n" );
|
|
Abc_NtkDelete( pNtkNew );
|
|
return NULL;
|
|
}
|
|
return pNtkNew;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Transforms the strashed network into FRAIG.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes )
|
|
{
|
|
Fraig_Man_t * pMan;
|
|
ProgressBar * pProgress;
|
|
Fraig_Node_t * pNodeFraig;
|
|
Vec_Ptr_t * vNodes;
|
|
Abc_Obj_t * pNode, * pConst1, * pReset;
|
|
int i;
|
|
|
|
assert( Abc_NtkIsStrash(pNtk) );
|
|
|
|
// create the FRAIG manager
|
|
pMan = Fraig_ManCreate( pParams );
|
|
|
|
// create PIs and remember them in the old nodes
|
|
Abc_NtkCleanCopy( pNtk );
|
|
Abc_NtkForEachCi( pNtk, pNode, i )
|
|
pNode->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, i);
|
|
pConst1 = Abc_AigConst1( pNtk->pManFunc );
|
|
pReset = Abc_AigReset( pNtk->pManFunc );
|
|
|
|
// perform strashing
|
|
vNodes = Abc_AigDfs( pNtk, fAllNodes, 0 );
|
|
pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
|
|
Vec_PtrForEachEntry( vNodes, pNode, i )
|
|
{
|
|
Extra_ProgressBarUpdate( pProgress, i, NULL );
|
|
if ( pNode == pConst1 )
|
|
pNodeFraig = Fraig_ManReadConst1(pMan);
|
|
else if ( pNode == pReset )
|
|
continue;
|
|
else
|
|
pNodeFraig = Fraig_NodeAnd( pMan,
|
|
Fraig_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ),
|
|
Fraig_NotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) ) );
|
|
assert( pNode->pCopy == NULL );
|
|
pNode->pCopy = (Abc_Obj_t *)pNodeFraig;
|
|
}
|
|
Extra_ProgressBarStop( pProgress );
|
|
Vec_PtrFree( vNodes );
|
|
|
|
// set the primary outputs
|
|
Abc_NtkForEachCo( pNtk, pNode, i )
|
|
Fraig_ManSetPo( pMan, (Fraig_Node_t *)Abc_ObjFanin0(pNode)->pCopy );
|
|
return pMan;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Transforms FRAIG into what looks like a strashed network.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
|
|
{
|
|
ProgressBar * pProgress;
|
|
Abc_Ntk_t * pNtkNew;
|
|
Abc_Obj_t * pNode;//, * pNodeNew;
|
|
int i;
|
|
// create the new network
|
|
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_STRASH, ABC_FUNC_AIG );
|
|
// make the mapper point to the new network
|
|
Abc_NtkForEachCi( pNtk, pNode, i )
|
|
Fraig_NodeSetData1( Fraig_ManReadIthVar(pMan, i), (Fraig_Node_t *)pNode->pCopy );
|
|
// set the constant node
|
|
Fraig_NodeSetData1( Fraig_ManReadConst1(pMan), (Fraig_Node_t *)Abc_AigConst1(pNtkNew->pManFunc) );
|
|
// process the nodes in topological order
|
|
pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
|
|
Abc_NtkForEachCo( pNtk, pNode, i )
|
|
{
|
|
Extra_ProgressBarUpdate( pProgress, i, NULL );
|
|
Abc_ObjFanin0(pNode)->pCopy = Abc_NodeFromFraig_rec( pNtkNew, Fraig_ManReadOutputs(pMan)[i] );
|
|
}
|
|
Extra_ProgressBarStop( pProgress );
|
|
// finalize the new network
|
|
Abc_NtkFinalize( pNtk, pNtkNew );
|
|
return pNtkNew;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Transforms into AIG one node.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
Abc_Obj_t * Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFraig )
|
|
{
|
|
Abc_Obj_t * pRes, * pRes0, * pRes1, * pResMin, * pResCur;
|
|
Fraig_Node_t * pNodeTemp, * pNodeFraigR = Fraig_Regular(pNodeFraig);
|
|
void ** ppTail;
|
|
// check if the node was already considered
|
|
if ( pRes = (Abc_Obj_t *)Fraig_NodeReadData1(pNodeFraigR) )
|
|
return Abc_ObjNotCond( pRes, Fraig_IsComplement(pNodeFraig) );
|
|
// solve the children
|
|
pRes0 = Abc_NodeFromFraig_rec( pNtkNew, Fraig_NodeReadOne(pNodeFraigR) );
|
|
pRes1 = Abc_NodeFromFraig_rec( pNtkNew, Fraig_NodeReadTwo(pNodeFraigR) );
|
|
// derive the new node
|
|
pRes = Abc_AigAnd( pNtkNew->pManFunc, pRes0, pRes1 );
|
|
pRes->fPhase = Fraig_NodeReadSimInv( pNodeFraigR );
|
|
// if the node has an equivalence class, find its representative
|
|
if ( Fraig_NodeReadRepr(pNodeFraigR) == NULL && Fraig_NodeReadNextE(pNodeFraigR) != NULL )
|
|
{
|
|
// go through the FRAIG nodes belonging to this equivalence class
|
|
// and find the representative node (the node with the smallest level)
|
|
pResMin = pRes;
|
|
for ( pNodeTemp = Fraig_NodeReadNextE(pNodeFraigR); pNodeTemp; pNodeTemp = Fraig_NodeReadNextE(pNodeTemp) )
|
|
{
|
|
assert( Fraig_NodeReadData1(pNodeTemp) == NULL );
|
|
pResCur = Abc_NodeFromFraig_rec( pNtkNew, pNodeTemp );
|
|
if ( pResMin->Level > pResCur->Level )
|
|
pResMin = pResCur;
|
|
}
|
|
// link the nodes in such a way that representative goes first
|
|
ppTail = &pResMin->pData;
|
|
if ( pRes != pResMin )
|
|
{
|
|
*ppTail = pRes;
|
|
ppTail = &pRes->pData;
|
|
}
|
|
for ( pNodeTemp = Fraig_NodeReadNextE(pNodeFraigR); pNodeTemp; pNodeTemp = Fraig_NodeReadNextE(pNodeTemp) )
|
|
{
|
|
pResCur = (Abc_Obj_t *)Fraig_NodeReadData1(pNodeTemp);
|
|
assert( pResCur );
|
|
if ( pResMin == pResCur )
|
|
continue;
|
|
*ppTail = pResCur;
|
|
ppTail = &pResCur->pData;
|
|
}
|
|
assert( *ppTail == NULL );
|
|
|
|
// update the phase of the node
|
|
pRes = Abc_ObjNotCond( pResMin, (pRes->fPhase ^ pResMin->fPhase) );
|
|
}
|
|
Fraig_NodeSetData1( pNodeFraigR, (Fraig_Node_t *)pRes );
|
|
return Abc_ObjNotCond( pRes, Fraig_IsComplement(pNodeFraig) );
|
|
}
|
|
|
|
|
|
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Interfaces the network with the FRAIG package.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
Abc_Ntk_t * Abc_NtkFraigTrust( Abc_Ntk_t * pNtk )
|
|
{
|
|
int fCheck = 1;
|
|
Abc_Ntk_t * pNtkNew;
|
|
|
|
if ( !Abc_NtkIsSopLogic(pNtk) )
|
|
{
|
|
printf( "Abc_NtkFraigTrust: Trust mode works for netlists and logic SOP networks.\n" );
|
|
return NULL;
|
|
}
|
|
|
|
if ( !Abc_NtkFraigTrustCheck(pNtk) )
|
|
{
|
|
printf( "Abc_NtkFraigTrust: The network does not look like an AIG with choice nodes.\n" );
|
|
return NULL;
|
|
}
|
|
|
|
// perform strashing
|
|
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_STRASH, ABC_FUNC_AIG );
|
|
Abc_NtkFraigTrustOne( pNtk, pNtkNew );
|
|
Abc_NtkFinalize( pNtk, pNtkNew );
|
|
|
|
// print a warning about choice nodes
|
|
printf( "Warning: The resulting AIG contains %d choice nodes.\n", Abc_NtkGetChoiceNum( pNtkNew ) );
|
|
|
|
// make sure that everything is okay
|
|
if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
|
|
{
|
|
printf( "Abc_NtkFraigTrust: The network check has failed.\n" );
|
|
Abc_NtkDelete( pNtkNew );
|
|
return NULL;
|
|
}
|
|
return pNtkNew;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Checks whether the node can be processed in the trust mode.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
int Abc_NtkFraigTrustCheck( Abc_Ntk_t * pNtk )
|
|
{
|
|
Abc_Obj_t * pNode;
|
|
int i, nFanins;
|
|
Abc_NtkForEachNode( pNtk, pNode, i )
|
|
{
|
|
nFanins = Abc_ObjFaninNum(pNode);
|
|
if ( nFanins < 2 )
|
|
continue;
|
|
if ( nFanins == 2 && Abc_SopIsAndType(pNode->pData) )
|
|
continue;
|
|
if ( !Abc_SopIsOrType(pNode->pData) )
|
|
return 0;
|
|
}
|
|
return 1;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Interfaces the network with the FRAIG package.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
void Abc_NtkFraigTrustOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
|
|
{
|
|
ProgressBar * pProgress;
|
|
Abc_Aig_t * pMan = pNtkNew->pManFunc;
|
|
Vec_Ptr_t * vNodes;
|
|
Abc_Obj_t * pNode, * pNodeNew, * pObj;
|
|
int i;
|
|
|
|
// perform strashing
|
|
vNodes = Abc_NtkDfs( pNtk, 0 );
|
|
pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
|
|
Vec_PtrForEachEntry( vNodes, pNode, i )
|
|
{
|
|
Extra_ProgressBarUpdate( pProgress, i, NULL );
|
|
// get the node
|
|
assert( Abc_ObjIsNode(pNode) );
|
|
// strash the node
|
|
pNodeNew = Abc_NodeFraigTrust( pMan, pNode );
|
|
// get the old object
|
|
if ( Abc_NtkIsNetlist(pNtk) )
|
|
pObj = Abc_ObjFanout0( pNode ); // the fanout net
|
|
else
|
|
pObj = pNode; // the node itself
|
|
// make sure the node is not yet strashed
|
|
assert( pObj->pCopy == NULL );
|
|
// mark the old object with the new AIG node
|
|
pObj->pCopy = pNodeNew;
|
|
}
|
|
Vec_PtrFree( vNodes );
|
|
Extra_ProgressBarStop( pProgress );
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Transforms one node into a FRAIG in the trust mode.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
Abc_Obj_t * Abc_NodeFraigTrust( Abc_Aig_t * pMan, Abc_Obj_t * pNode )
|
|
{
|
|
Abc_Obj_t * pSum, * pFanin;
|
|
Abc_Obj_t * pConst1 = Abc_AigConst1(pMan);
|
|
void ** ppTail;
|
|
int i, nFanins, fCompl;
|
|
|
|
assert( Abc_ObjIsNode(pNode) );
|
|
// get the number of node's fanins
|
|
nFanins = Abc_ObjFaninNum( pNode );
|
|
assert( nFanins == Abc_SopGetVarNum(pNode->pData) );
|
|
// check if it is a constant
|
|
if ( nFanins == 0 )
|
|
return Abc_ObjNotCond( pConst1, Abc_SopIsConst0(pNode->pData) );
|
|
if ( nFanins == 1 )
|
|
return Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_SopIsInv(pNode->pData) );
|
|
if ( nFanins == 2 && Abc_SopIsAndType(pNode->pData) )
|
|
return Abc_AigAnd( pMan,
|
|
Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, !Abc_SopGetIthCareLit(pNode->pData,0) ),
|
|
Abc_ObjNotCond( Abc_ObjFanin1(pNode)->pCopy, !Abc_SopGetIthCareLit(pNode->pData,1) ) );
|
|
assert( Abc_SopIsOrType(pNode->pData) );
|
|
fCompl = Abc_SopGetIthCareLit(pNode->pData,0);
|
|
// get the root of the choice node (the first fanin)
|
|
pSum = Abc_ObjFanin0(pNode)->pCopy;
|
|
// connect other fanins
|
|
ppTail = &pSum->pData;
|
|
Abc_ObjForEachFanin( pNode, pFanin, i )
|
|
{
|
|
if ( i == 0 )
|
|
continue;
|
|
*ppTail = pFanin->pCopy;
|
|
ppTail = &pFanin->pCopy->pData;
|
|
// set the complemented bit of this cut
|
|
if ( fCompl ^ Abc_SopGetIthCareLit(pNode->pData, i) )
|
|
pFanin->pCopy->fPhase = 1;
|
|
}
|
|
assert( *ppTail == NULL );
|
|
return pSum;
|
|
}
|
|
|
|
|
|
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Interfaces the network with the FRAIG package.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
|
|
{
|
|
Abc_Frame_t * p;
|
|
Abc_Ntk_t * pStore;
|
|
int nAndsOld;
|
|
|
|
if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) )
|
|
{
|
|
printf( "The netlist need to be converted into a logic network before adding it to storage.\n" );
|
|
return 0;
|
|
}
|
|
|
|
// get the network currently stored
|
|
p = Abc_FrameGetGlobalFrame();
|
|
pStore = Abc_FrameReadNtkStore(p);
|
|
if ( pStore == NULL )
|
|
{
|
|
// start the stored network
|
|
pStore = Abc_NtkStrash( pNtk, 0, 0 );
|
|
if ( pStore == NULL )
|
|
{
|
|
printf( "Abc_NtkFraigStore: Initial strashing has failed.\n" );
|
|
return 0;
|
|
}
|
|
// save the parameters
|
|
Abc_FrameSetNtkStore( p, pStore );
|
|
Abc_FrameSetNtkStoreSize( p, 1 );
|
|
nAndsOld = 0;
|
|
}
|
|
else
|
|
{
|
|
// add the new network to storage
|
|
nAndsOld = Abc_NtkNodeNum( pStore );
|
|
if ( !Abc_NtkAppend( pStore, pNtk ) )
|
|
{
|
|
printf( "The current network cannot be appended to the stored network.\n" );
|
|
return 0;
|
|
}
|
|
// set the number of networks stored
|
|
Abc_FrameSetNtkStoreSize( p, Abc_FrameReadNtkStoreSize(p) + 1 );
|
|
}
|
|
printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pStore) - nAndsOld );
|
|
return 1;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Interfaces the network with the FRAIG package.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
Abc_Ntk_t * Abc_NtkFraigRestore()
|
|
{
|
|
Abc_Frame_t * p;
|
|
Fraig_Params_t Params;
|
|
Abc_Ntk_t * pStore, * pFraig;
|
|
int nWords1, nWords2, nWordsMin;
|
|
|
|
// get the stored network
|
|
p = Abc_FrameGetGlobalFrame();
|
|
pStore = Abc_FrameReadNtkStore(p);
|
|
Abc_FrameSetNtkStore( p, NULL );
|
|
if ( pStore == NULL )
|
|
{
|
|
printf( "There are no network currently in storage.\n" );
|
|
return NULL;
|
|
}
|
|
printf( "Currently stored %d networks with %d nodes will be fraiged.\n",
|
|
Abc_FrameReadNtkStoreSize(p), Abc_NtkNodeNum(pStore) );
|
|
|
|
// to determine the number of simulation patterns
|
|
// use the following strategy
|
|
// at least 64 words (32 words random and 32 words dynamic)
|
|
// no more than 256M for one circuit (128M + 128M)
|
|
nWords1 = 32;
|
|
nWords2 = (1<<27) / (Abc_NtkNodeNum(pStore) + Abc_NtkCiNum(pStore));
|
|
nWordsMin = ABC_MIN( nWords1, nWords2 );
|
|
|
|
// set parameters for fraiging
|
|
Fraig_ParamsSetDefault( &Params );
|
|
Params.nPatsRand = nWordsMin * 32; // the number of words of random simulation info
|
|
Params.nPatsDyna = nWordsMin * 32; // the number of words of dynamic simulation info
|
|
Params.nBTLimit = 99; // the max number of backtracks to perform
|
|
Params.fFuncRed = 1; // performs only one level hashing
|
|
Params.fFeedBack = 1; // enables solver feedback
|
|
Params.fDist1Pats = 1; // enables distance-1 patterns
|
|
Params.fDoSparse = 1; // performs equiv tests for sparse functions
|
|
Params.fChoicing = 1; // enables recording structural choices
|
|
Params.fTryProve = 0; // tries to solve the final miter
|
|
Params.fVerbose = 0; // the verbosiness flag
|
|
|
|
// Fraig_ManReportChoices( p );
|
|
// transform it into FRAIG
|
|
pFraig = Abc_NtkFraig( pStore, &Params, 1 );
|
|
if ( pFraig == NULL )
|
|
return NULL;
|
|
Abc_NtkDelete( pStore );
|
|
return pFraig;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Interfaces the network with the FRAIG package.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
void Abc_NtkFraigStoreClean()
|
|
{
|
|
Abc_Frame_t * p;
|
|
Abc_Ntk_t * pStore;
|
|
// get the stored network
|
|
p = Abc_FrameGetGlobalFrame();
|
|
pStore = Abc_FrameReadNtkStore(p);
|
|
if ( pStore )
|
|
Abc_NtkDelete( pStore );
|
|
Abc_FrameSetNtkStore( p, NULL );
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Checks the correctness of stored networks.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
void Abc_NtkFraigStoreCheck( Abc_Ntk_t * pFraig )
|
|
{
|
|
Abc_Obj_t * pNode0, * pNode1;
|
|
int nPoOrig, nPoFinal, nStored;
|
|
int i, k;
|
|
// check that the PO functions are correct
|
|
nPoFinal = Abc_NtkPoNum(pFraig);
|
|
nStored = Abc_FrameReadNtkStoreSize(Abc_FrameGetGlobalFrame());
|
|
assert( nPoFinal % nStored == 0 );
|
|
nPoOrig = nPoFinal / nStored;
|
|
for ( i = 0; i < nPoOrig; i++ )
|
|
{
|
|
pNode0 = Abc_ObjFanin0( Abc_NtkPo(pFraig, i) );
|
|
for ( k = 1; k < nStored; k++ )
|
|
{
|
|
pNode1 = Abc_ObjFanin0( Abc_NtkPo(pFraig, k*nPoOrig+i) );
|
|
if ( pNode0 != pNode1 )
|
|
printf( "Verification for PO #%d of network #%d has failed. The PO function is not used.\n", i+1, k+1 );
|
|
}
|
|
}
|
|
}
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// END OF FILE ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
|