/**CFile****************************************************************
FileName [abcIvy.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Network and node package.]
Synopsis [Strashing of the current network.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: abcIvy.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "base/abc/abc.h"
#include "bool/dec/dec.h"
#include "proof/fra/fra.h"
#include "aig/ivy/ivy.h"
#include "proof/fraig/fraig.h"
#include "map/mio/mio.h"
#include "aig/aig/aig.h"
#include "misc/extra/extraBdd.h"
ABC_NAMESPACE_IMPL_START
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
extern void Aig_ManStop( Aig_Man_t * pMan );
//extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
extern Ivy_Obj_t * Dec_GraphToNetworkIvy( Ivy_Man_t * pMan, Dec_Graph_t * pGraph );
extern void Ivy_CutComputeAll( Ivy_Man_t * p, int nInputs );
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static Abc_Ntk_t * Abc_NtkFromIvy( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan );
static Abc_Ntk_t * Abc_NtkFromIvySeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig );
static Ivy_Man_t * Abc_NtkToIvy( Abc_Ntk_t * pNtkOld );
static void Abc_NtkStrashPerformAig( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan );
static Ivy_Obj_t * Abc_NodeStrashAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode );
static Ivy_Obj_t * Abc_NodeStrashAigSopAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode, char * pSop );
static Ivy_Obj_t * Abc_NodeStrashAigExorAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode, char * pSop );
static Ivy_Obj_t * Abc_NodeStrashAigFactorAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode, char * pSop );
typedef int Abc_Edge_t;
static inline Abc_Edge_t Abc_EdgeCreate( int Id, int fCompl ) { return (Id << 1) | fCompl; }
static inline int Abc_EdgeId( Abc_Edge_t Edge ) { return Edge >> 1; }
static inline int Abc_EdgeIsComplement( Abc_Edge_t Edge ) { return Edge & 1; }
static inline Abc_Edge_t Abc_EdgeRegular( Abc_Edge_t Edge ) { return (Edge >> 1) << 1; }
static inline Abc_Edge_t Abc_EdgeNot( Abc_Edge_t Edge ) { return Edge ^ 1; }
static inline Abc_Edge_t Abc_EdgeNotCond( Abc_Edge_t Edge, int fCond ) { return Edge ^ fCond; }
static inline Abc_Edge_t Abc_EdgeFromNode( Abc_Obj_t * pNode ) { return Abc_EdgeCreate( Abc_ObjRegular(pNode)->Id, Abc_ObjIsComplement(pNode) ); }
static inline Abc_Obj_t * Abc_EdgeToNode( Abc_Ntk_t * p, Abc_Edge_t Edge ) { return Abc_ObjNotCond( Abc_NtkObj(p, Abc_EdgeId(Edge)), Abc_EdgeIsComplement(Edge) ); }
static inline Abc_Obj_t * Abc_ObjFanin0Ivy( Abc_Ntk_t * p, Ivy_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_EdgeToNode(p, Ivy_ObjFanin0(pObj)->TravId), Ivy_ObjFaninC0(pObj) ); }
static inline Abc_Obj_t * Abc_ObjFanin1Ivy( Abc_Ntk_t * p, Ivy_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_EdgeToNode(p, Ivy_ObjFanin1(pObj)->TravId), Ivy_ObjFaninC1(pObj) ); }
static Vec_Int_t * Abc_NtkCollectLatchValuesIvy( Abc_Ntk_t * pNtk, int fUseDcs );
extern int timeRetime;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Prepares the IVY package.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )
{
Ivy_Man_t * pMan;
//timeRetime = Abc_Clock();
assert( !Abc_NtkIsNetlist(pNtk) );
if ( Abc_NtkIsBddLogic(pNtk) )
{
if ( !Abc_NtkBddToSop(pNtk, 0) )
{
printf( "Abc_NtkIvyBefore(): Converting to SOPs has failed.\n" );
return NULL;
}
}
if ( fSeq && Abc_NtkCountSelfFeedLatches(pNtk) )
{
printf( "Warning: The network has %d self-feeding latches.\n", Abc_NtkCountSelfFeedLatches(pNtk) );
// return NULL;
}
// print warning about choice nodes
if ( Abc_NtkGetChoiceNum( pNtk ) )
printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" );
// convert to the AIG manager
pMan = Abc_NtkToIvy( pNtk );
if ( !Ivy_ManCheck( pMan ) )
{
printf( "AIG check has failed.\n" );
Ivy_ManStop( pMan );
return NULL;
}
// Ivy_ManPrintStats( pMan );
if ( fSeq )
{
int nLatches = Abc_NtkLatchNum(pNtk);
Vec_Int_t * vInit = Abc_NtkCollectLatchValuesIvy( pNtk, fUseDc );
Ivy_ManMakeSeq( pMan, nLatches, vInit->pArray );
Vec_IntFree( vInit );
// Ivy_ManPrintStats( pMan );
}
//timeRetime = Abc_Clock() - timeRetime;
return pMan;
}
/**Function*************************************************************
Synopsis [Prepares the IVY package.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkIvyAfter( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan, int fSeq, int fHaig )
{
Abc_Ntk_t * pNtkAig;
int nNodes, fCleanup = 1;
// convert from the AIG manager
if ( fSeq )
pNtkAig = Abc_NtkFromIvySeq( pNtk, pMan, fHaig );
else
pNtkAig = Abc_NtkFromIvy( pNtk, pMan );
// report the cleanup results
if ( !fHaig && fCleanup && (nNodes = Abc_AigCleanup((Abc_Aig_t *)pNtkAig->pManFunc)) )
printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes );
// duplicate EXDC
if ( pNtk->pExdc )
pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc );
// make sure everything is okay
if ( !Abc_NtkCheck( pNtkAig ) )
{
printf( "Abc_NtkStrash: The network check has failed.\n" );
Abc_NtkDelete( pNtkAig );
return NULL;
}
return pNtkAig;
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkIvyStrash( Abc_Ntk_t * pNtk )
{
Abc_Ntk_t * pNtkAig;
Ivy_Man_t * pMan;
pMan = Abc_NtkIvyBefore( pNtk, 1, 0 );
if ( pMan == NULL )
return NULL;
pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 );
Ivy_ManStop( pMan );
return pNtkAig;
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int nIters, int fUseZeroCost, int fVerbose )
{
Abc_Ntk_t * pNtkAig;
Ivy_Man_t * pMan;
abctime clk;
// int i;
/*
extern int nMoves;
extern int nMovesS;
extern int nClauses;
extern int timeInv;
nMoves = 0;
nMovesS = 0;
nClauses = 0;
timeInv = 0;
*/
pMan = Abc_NtkIvyBefore( pNtk, 1, 1 );
if ( pMan == NULL )
return NULL;
//timeRetime = Abc_Clock();
clk = Abc_Clock();
Ivy_ManHaigStart( pMan, fVerbose );
// Ivy_ManRewriteSeq( pMan, 0, 0 );
// for ( i = 0; i < nIters; i++ )
// Ivy_ManRewriteSeq( pMan, fUseZeroCost, 0 );
//printf( "%d ", Ivy_ManNodeNum(pMan) );
Ivy_ManRewriteSeq( pMan, 0, 0 );
Ivy_ManRewriteSeq( pMan, 0, 0 );
Ivy_ManRewriteSeq( pMan, 1, 0 );
//printf( "%d ", Ivy_ManNodeNum(pMan) );
//printf( "%d ", Ivy_ManNodeNum(pMan->pHaig) );
//ABC_PRT( " ", Abc_Clock() - clk );
//printf( "\n" );
/*
printf( "Moves = %d. ", nMoves );
printf( "MovesS = %d. ", nMovesS );
printf( "Clauses = %d. ", nClauses );
ABC_PRT( "Time", timeInv );
*/
// Ivy_ManRewriteSeq( pMan, 1, 0 );
//printf( "Haig size = %d.\n", Ivy_ManNodeNum(pMan->pHaig) );
// Ivy_ManHaigPostprocess( pMan, fVerbose );
//timeRetime = Abc_Clock() - timeRetime;
// write working AIG into the current network
// pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 );
// write HAIG into the current network
pNtkAig = Abc_NtkIvyAfter( pNtk, pMan->pHaig, 1, 1 );
Ivy_ManHaigStop( pMan );
Ivy_ManStop( pMan );
return pNtkAig;
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkIvyCuts( Abc_Ntk_t * pNtk, int nInputs )
{
Ivy_Man_t * pMan;
pMan = Abc_NtkIvyBefore( pNtk, 1, 0 );
if ( pMan == NULL )
return;
Ivy_CutComputeAll( pMan, nInputs );
Ivy_ManStop( pMan );
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkIvyRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeroCost, int fVerbose )
{
Abc_Ntk_t * pNtkAig;
Ivy_Man_t * pMan;
pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
if ( pMan == NULL )
return NULL;
//timeRetime = Abc_Clock();
Ivy_ManRewritePre( pMan, fUpdateLevel, fUseZeroCost, fVerbose );
//timeRetime = Abc_Clock() - timeRetime;
pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
Ivy_ManStop( pMan );
return pNtkAig;
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkIvyRewriteSeq( Abc_Ntk_t * pNtk, int fUseZeroCost, int fVerbose )
{
Abc_Ntk_t * pNtkAig;
Ivy_Man_t * pMan;
pMan = Abc_NtkIvyBefore( pNtk, 1, 1 );
if ( pMan == NULL )
return NULL;
//timeRetime = Abc_Clock();
Ivy_ManRewriteSeq( pMan, fUseZeroCost, fVerbose );
//timeRetime = Abc_Clock() - timeRetime;
// Ivy_ManRewriteSeq( pMan, 1, 0 );
// Ivy_ManRewriteSeq( pMan, 1, 0 );
pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 );
Ivy_ManStop( pMan );
return pNtkAig;
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkIvyResyn0( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose )
{
Abc_Ntk_t * pNtkAig;
Ivy_Man_t * pMan, * pTemp;
pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
if ( pMan == NULL )
return NULL;
pMan = Ivy_ManResyn0( pTemp = pMan, fUpdateLevel, fVerbose );
Ivy_ManStop( pTemp );
pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
Ivy_ManStop( pMan );
return pNtkAig;
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkIvyResyn( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose )
{
Abc_Ntk_t * pNtkAig;
Ivy_Man_t * pMan, * pTemp;
pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
if ( pMan == NULL )
return NULL;
pMan = Ivy_ManResyn( pTemp = pMan, fUpdateLevel, fVerbose );
Ivy_ManStop( pTemp );
pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
Ivy_ManStop( pMan );
return pNtkAig;
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkIvySat( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose )
{
Ivy_FraigParams_t Params, * pParams = &Params;
Abc_Ntk_t * pNtkAig;
Ivy_Man_t * pMan, * pTemp;
pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
if ( pMan == NULL )
return NULL;
Ivy_FraigParamsDefault( pParams );
pParams->nBTLimitMiter = nConfLimit;
pParams->fVerbose = fVerbose;
// pMan = Ivy_FraigPerform( pTemp = pMan, pParams );
pMan = Ivy_FraigMiter( pTemp = pMan, pParams );
Ivy_ManStop( pTemp );
pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
Ivy_ManStop( pMan );
return pNtkAig;
}
/**Function*************************************************************
Synopsis [Sets the final nodes to point to the original nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkTransferPointers( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig )
{
Abc_Obj_t * pObj;
Ivy_Obj_t * pObjIvy, * pObjFraig;
int i;
pObj = Abc_AigConst1(pNtk);
pObj->pCopy = Abc_AigConst1(pNtkAig);
Abc_NtkForEachCi( pNtk, pObj, i )
pObj->pCopy = Abc_NtkCi(pNtkAig, i);
Abc_NtkForEachCo( pNtk, pObj, i )
pObj->pCopy = Abc_NtkCo(pNtkAig, i);
Abc_NtkForEachLatch( pNtk, pObj, i )
pObj->pCopy = Abc_NtkBox(pNtkAig, i);
Abc_NtkForEachNode( pNtk, pObj, i )
{
pObjIvy = (Ivy_Obj_t *)pObj->pCopy;
if ( pObjIvy == NULL )
continue;
pObjFraig = Ivy_ObjEquiv( pObjIvy );
if ( pObjFraig == NULL )
continue;
pObj->pCopy = Abc_EdgeToNode( pNtkAig, Ivy_Regular(pObjFraig)->TravId );
pObj->pCopy = Abc_ObjNotCond( pObj->pCopy, Ivy_IsComplement(pObjFraig) );
}
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fVerbose )
{
Ivy_FraigParams_t Params, * pParams = &Params;
Abc_Ntk_t * pNtkAig;
Ivy_Man_t * pMan, * pTemp;
pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
if ( pMan == NULL )
return NULL;
Ivy_FraigParamsDefault( pParams );
pParams->nBTLimitNode = nConfLimit;
pParams->fVerbose = fVerbose;
pParams->fProve = fProve;
pParams->fDoSparse = fDoSparse;
pMan = Ivy_FraigPerform( pTemp = pMan, pParams );
// transfer the pointers
if ( fTransfer == 1 )
{
Vec_Ptr_t * vCopies;
vCopies = Abc_NtkSaveCopy( pNtk );
pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
Abc_NtkLoadCopy( pNtk, vCopies );
Vec_PtrFree( vCopies );
Abc_NtkTransferPointers( pNtk, pNtkAig );
}
else
pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
Ivy_ManStop( pTemp );
Ivy_ManStop( pMan );
return pNtkAig;
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
{
Prove_Params_t * pParams = (Prove_Params_t *)pPars;
Abc_Ntk_t * pNtk = *ppNtk, * pNtkTemp;
Abc_Obj_t * pObj, * pFanin;
Ivy_Man_t * pMan;
Aig_Man_t * pMan2;
int RetValue;
assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsLogic(pNtk) );
// experiment with various parameters settings
// pParams->fUseBdds = 1;
// pParams->fBddReorder = 1;
// pParams->nTotalBacktrackLimit = 10000;
// strash the network if it is not strashed already
if ( !Abc_NtkIsStrash(pNtk) )
{
pNtk = Abc_NtkStrash( pNtkTemp = pNtk, 0, 1, 0 );
Abc_NtkDelete( pNtkTemp );
}
// check the case when the 0000 simulation pattern detect the bug
pObj = Abc_NtkPo(pNtk,0);
pFanin = Abc_ObjFanin0(pObj);
if ( Abc_ObjFanin0(pObj)->fPhase != (unsigned)Abc_ObjFaninC0(pObj) )
{
pNtk->pModel = ABC_CALLOC( int, Abc_NtkCiNum(pNtk) );
return 0;
}
// changed in "src\sat\fraig\fraigMan.c"
// pParams->nMiteringLimitStart = 300; // starting mitering limit
// to be
// pParams->nMiteringLimitStart = 5000; // starting mitering limit
// if SAT only, solve without iteration
// RetValue = Abc_NtkMiterSat( pNtk, 2*(ABC_INT64_T)pParams->nMiteringLimitStart, (ABC_INT64_T)0, 0, NULL, NULL );
pMan2 = Abc_NtkToDar( pNtk, 0, 0 );
RetValue = Fra_FraigSat( pMan2, (ABC_INT64_T)pParams->nMiteringLimitStart, (ABC_INT64_T)0, 0, 0, 0, 1, 0, 0, 0 );
pNtk->pModel = (int *)pMan2->pData, pMan2->pData = NULL;
Aig_ManStop( pMan2 );
// pNtk->pModel = Aig_ManReleaseData( pMan2 );
if ( RetValue >= 0 )
return RetValue;
// apply AIG rewriting
if ( pParams->fUseRewriting && Abc_NtkNodeNum(pNtk) > 500 )
{
// abctime clk = Abc_Clock();
//printf( "Before rwsat = %d. ", Abc_NtkNodeNum(pNtk) );
pParams->fUseRewriting = 0;
pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );
Abc_NtkDelete( pNtkTemp );
Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );
Abc_NtkDelete( pNtkTemp );
Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
//printf( "After rwsat = %d. ", Abc_NtkNodeNum(pNtk) );
//ABC_PRT( "Time", Abc_Clock() - clk );
}
// convert ABC network into IVY network
pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
// solve the CEC problem
RetValue = Ivy_FraigProve( &pMan, pParams );
// RetValue = -1;
// convert IVY network into ABC network
pNtk = Abc_NtkIvyAfter( pNtkTemp = pNtk, pMan, 0, 0 );
Abc_NtkDelete( pNtkTemp );
// transfer model if given
pNtk->pModel = (int *)pMan->pData; pMan->pData = NULL;
Ivy_ManStop( pMan );
// try to prove it using brute force SAT with good CNF encoding
if ( RetValue < 0 )
{
pMan2 = Abc_NtkToDar( pNtk, 0, 0 );
// dump the miter before entering high-effort solving
if ( pParams->fVerbose )
{
char pFileName[100];
sprintf( pFileName, "cecmiter.aig" );
Ioa_WriteAiger( pMan2, pFileName, 0, 0 );
printf( "Intermediate reduced miter is written into file \"%s\".\n", pFileName );
}
RetValue = Fra_FraigSat( pMan2, pParams->nMiteringLimitLast, 0, 0, 0, 0, 0, 0, 0, pParams->fVerbose );
pNtk->pModel = (int *)pMan2->pData, pMan2->pData = NULL;
Aig_ManStop( pMan2 );
}
// try to prove it using brute force BDDs
if ( RetValue < 0 && pParams->fUseBdds )
{
if ( pParams->fVerbose )
{
printf( "Attempting BDDs with node limit %d ...\n", pParams->nBddSizeLimit );
fflush( stdout );
}
pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0 );
if ( pNtk )
{
Abc_NtkDelete( pNtkTemp );
RetValue = ( (Abc_NtkNodeNum(pNtk) == 1) && (Abc_ObjFanin0(Abc_NtkPo(pNtk,0))->pData == Cudd_ReadLogicZero((DdManager *)pNtk->pManFunc)) );
}
else
pNtk = pNtkTemp;
}
// return the result
*ppNtk = pNtk;
return RetValue;
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
{
// Abc_Ntk_t * pNtkAig;
Ivy_Man_t * pMan;//, * pTemp;
// int fCleanup = 1;
// int nNodes;
// int nLatches = Abc_NtkLatchNum(pNtk);
Vec_Int_t * vInit = Abc_NtkCollectLatchValuesIvy( pNtk, 0 );
assert( !Abc_NtkIsNetlist(pNtk) );
if ( Abc_NtkIsBddLogic(pNtk) )
{
if ( !Abc_NtkBddToSop(pNtk, 0) )
{
Vec_IntFree( vInit );
printf( "Abc_NtkIvy(): Converting to SOPs has failed.\n" );
return NULL;
}
}
if ( Abc_NtkCountSelfFeedLatches(pNtk) )
{
printf( "Warning: The network has %d self-feeding latches. Quitting.\n", Abc_NtkCountSelfFeedLatches(pNtk) );
return NULL;
}
// print warning about choice nodes
if ( Abc_NtkGetChoiceNum( pNtk ) )
printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" );
// convert to the AIG manager
pMan = Abc_NtkToIvy( pNtk );
if ( !Ivy_ManCheck( pMan ) )
{
Vec_IntFree( vInit );
printf( "AIG check has failed.\n" );
Ivy_ManStop( pMan );
return NULL;
}
// Ivy_MffcTest( pMan );
// Ivy_ManPrintStats( pMan );
// pMan = Ivy_ManBalance( pTemp = pMan, 1 );
// Ivy_ManStop( pTemp );
// Ivy_ManSeqRewrite( pMan, 0, 0 );
// Ivy_ManTestCutsAlg( pMan );
// Ivy_ManTestCutsBool( pMan );
// Ivy_ManRewriteAlg( pMan, 1, 1 );
// pMan = Ivy_ManResyn( pTemp = pMan, 1, 0 );
// Ivy_ManStop( pTemp );
// Ivy_ManTestCutsAll( pMan );
// Ivy_ManTestCutsTravAll( pMan );
// Ivy_ManPrintStats( pMan );
// Ivy_ManPrintStats( pMan );
// Ivy_ManRewritePre( pMan, 1, 0, 0 );
// Ivy_ManPrintStats( pMan );
// printf( "\n" );
// Ivy_ManPrintStats( pMan );
// Ivy_ManMakeSeq( pMan, nLatches, pInit );
// Ivy_ManPrintStats( pMan );
// Ivy_ManRequiredLevels( pMan );
// Ivy_FastMapPerform( pMan, 8 );
Ivy_ManStop( pMan );
return NULL;
/*
// convert from the AIG manager
pNtkAig = Abc_NtkFromIvy( pNtk, pMan );
// pNtkAig = Abc_NtkFromIvySeq( pNtk, pMan );
Ivy_ManStop( pMan );
// report the cleanup results
if ( fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) )
printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes );
// duplicate EXDC
if ( pNtk->pExdc )
pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc );
// make sure everything is okay
if ( !Abc_NtkCheck( pNtkAig ) )
{
ABC_FREE( pInit );
printf( "Abc_NtkStrash: The network check has failed.\n" );
Abc_NtkDelete( pNtkAig );
return NULL;
}
ABC_FREE( pInit );
return pNtkAig;
*/
}
/**Function*************************************************************
Synopsis [Converts the network from the AIG manager into ABC.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkFromIvy( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
{
Vec_Int_t * vNodes;
Abc_Ntk_t * pNtk;
Abc_Obj_t * pObj, * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1;
Ivy_Obj_t * pNode;
int i;
// perform strashing
pNtk = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
// transfer the pointers to the basic nodes
Ivy_ManConst1(pMan)->TravId = Abc_EdgeFromNode( Abc_AigConst1(pNtk) );
Abc_NtkForEachCi( pNtkOld, pObj, i )
Ivy_ManPi(pMan, i)->TravId = Abc_EdgeFromNode( pObj->pCopy );
// rebuild the AIG
vNodes = Ivy_ManDfs( pMan );
Ivy_ManForEachNodeVec( pMan, vNodes, pNode, i )
{
// add the first fanin
pFaninNew0 = Abc_ObjFanin0Ivy( pNtk, pNode );
if ( Ivy_ObjIsBuf(pNode) )
{
pNode->TravId = Abc_EdgeFromNode( pFaninNew0 );
continue;
}
// add the second fanin
pFaninNew1 = Abc_ObjFanin1Ivy( pNtk, pNode );
// create the new node
if ( Ivy_ObjIsExor(pNode) )
pObjNew = Abc_AigXor( (Abc_Aig_t *)pNtk->pManFunc, pFaninNew0, pFaninNew1 );
else
pObjNew = Abc_AigAnd( (Abc_Aig_t *)pNtk->pManFunc, pFaninNew0, pFaninNew1 );
pNode->TravId = Abc_EdgeFromNode( pObjNew );
}
// connect the PO nodes
Abc_NtkForEachCo( pNtkOld, pObj, i )
{
pFaninNew = Abc_ObjFanin0Ivy( pNtk, Ivy_ManPo(pMan, i) );
Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
}
Vec_IntFree( vNodes );
if ( !Abc_NtkCheck( pNtk ) )
fprintf( stdout, "Abc_NtkFromIvy(): Network check has failed.\n" );
return pNtk;
}
/**Function*************************************************************
Synopsis [Converts the network from the AIG manager into ABC.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkFromIvySeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig )
{
Vec_Int_t * vNodes, * vLatches;
Abc_Ntk_t * pNtk;
Abc_Obj_t * pObj, * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1;
Ivy_Obj_t * pNode, * pTemp;
int i;
// assert( Ivy_ManLatchNum(pMan) > 0 );
// perform strashing
pNtk = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
// transfer the pointers to the basic nodes
Ivy_ManConst1(pMan)->TravId = Abc_EdgeFromNode( Abc_AigConst1(pNtk) );
Abc_NtkForEachPi( pNtkOld, pObj, i )
Ivy_ManPi(pMan, i)->TravId = Abc_EdgeFromNode( pObj->pCopy );
// create latches of the new network
vNodes = Ivy_ManDfsSeq( pMan, &vLatches );
Ivy_ManForEachNodeVec( pMan, vLatches, pNode, i )
{
pObjNew = Abc_NtkCreateLatch( pNtk );
pFaninNew0 = Abc_NtkCreateBi( pNtk );
pFaninNew1 = Abc_NtkCreateBo( pNtk );
Abc_ObjAddFanin( pObjNew, pFaninNew0 );
Abc_ObjAddFanin( pFaninNew1, pObjNew );
if ( fHaig || Ivy_ObjInit(pNode) == IVY_INIT_DC )
Abc_LatchSetInitDc( pObjNew );
else if ( Ivy_ObjInit(pNode) == IVY_INIT_1 )
Abc_LatchSetInit1( pObjNew );
else if ( Ivy_ObjInit(pNode) == IVY_INIT_0 )
Abc_LatchSetInit0( pObjNew );
else assert( 0 );
pNode->TravId = Abc_EdgeFromNode( pFaninNew1 );
}
Abc_NtkAddDummyBoxNames( pNtk );
// rebuild the AIG
Ivy_ManForEachNodeVec( pMan, vNodes, pNode, i )
{
// add the first fanin
pFaninNew0 = Abc_ObjFanin0Ivy( pNtk, pNode );
if ( Ivy_ObjIsBuf(pNode) )
{
pNode->TravId = Abc_EdgeFromNode( pFaninNew0 );
continue;
}
// add the second fanin
pFaninNew1 = Abc_ObjFanin1Ivy( pNtk, pNode );
// create the new node
if ( Ivy_ObjIsExor(pNode) )
pObjNew = Abc_AigXor( (Abc_Aig_t *)pNtk->pManFunc, pFaninNew0, pFaninNew1 );
else
pObjNew = Abc_AigAnd( (Abc_Aig_t *)pNtk->pManFunc, pFaninNew0, pFaninNew1 );
pNode->TravId = Abc_EdgeFromNode( pObjNew );
// process the choice nodes
if ( fHaig && pNode->pEquiv && Ivy_ObjRefs(pNode) > 0 )
{
pFaninNew = Abc_EdgeToNode( pNtk, pNode->TravId );
// pFaninNew->fPhase = 0;
assert( !Ivy_IsComplement(pNode->pEquiv) );
for ( pTemp = pNode->pEquiv; pTemp != pNode; pTemp = Ivy_Regular(pTemp->pEquiv) )
{
pFaninNew1 = Abc_EdgeToNode( pNtk, pTemp->TravId );
// pFaninNew1->fPhase = Ivy_IsComplement( pTemp->pEquiv );
pFaninNew->pData = pFaninNew1;
pFaninNew = pFaninNew1;
}
pFaninNew->pData = NULL;
// printf( "Writing choice node %d.\n", pNode->Id );
}
}
// connect the PO nodes
Abc_NtkForEachPo( pNtkOld, pObj, i )
{
pFaninNew = Abc_ObjFanin0Ivy( pNtk, Ivy_ManPo(pMan, i) );
Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
}
// connect the latches
Ivy_ManForEachNodeVec( pMan, vLatches, pNode, i )
{
pFaninNew = Abc_ObjFanin0Ivy( pNtk, pNode );
Abc_ObjAddFanin( Abc_ObjFanin0(Abc_NtkBox(pNtk, i)), pFaninNew );
}
Vec_IntFree( vLatches );
Vec_IntFree( vNodes );
if ( !Abc_NtkCheck( pNtk ) )
fprintf( stdout, "Abc_NtkFromIvySeq(): Network check has failed.\n" );
return pNtk;
}
/**Function*************************************************************
Synopsis [Converts the network from the AIG manager into ABC.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ivy_Man_t * Abc_NtkToIvy( Abc_Ntk_t * pNtkOld )
{
Ivy_Man_t * pMan;
Abc_Obj_t * pObj;
Ivy_Obj_t * pFanin;
int i;
// create the manager
assert( Abc_NtkHasSop(pNtkOld) || Abc_NtkIsStrash(pNtkOld) );
pMan = Ivy_ManStart();
// create the PIs
if ( Abc_NtkIsStrash(pNtkOld) )
Abc_AigConst1(pNtkOld)->pCopy = (Abc_Obj_t *)Ivy_ManConst1(pMan);
Abc_NtkForEachCi( pNtkOld, pObj, i )
pObj->pCopy = (Abc_Obj_t *)Ivy_ObjCreatePi(pMan);
// perform the conversion of the internal nodes
Abc_NtkStrashPerformAig( pNtkOld, pMan );
// create the POs
Abc_NtkForEachCo( pNtkOld, pObj, i )
{
pFanin = (Ivy_Obj_t *)Abc_ObjFanin0(pObj)->pCopy;
pFanin = Ivy_NotCond( pFanin, Abc_ObjFaninC0(pObj) );
Ivy_ObjCreatePo( pMan, pFanin );
}
Ivy_ManCleanup( pMan );
return pMan;
}
/**Function*************************************************************
Synopsis [Prepares the network for strashing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkStrashPerformAig( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan )
{
// ProgressBar * pProgress;
Vec_Ptr_t * vNodes;
Abc_Obj_t * pNode;
int i;
vNodes = Abc_NtkDfs( pNtk, 0 );
// pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
{
// Extra_ProgressBarUpdate( pProgress, i, NULL );
pNode->pCopy = (Abc_Obj_t *)Abc_NodeStrashAig( pMan, pNode );
}
// Extra_ProgressBarStop( pProgress );
Vec_PtrFree( vNodes );
}
/**Function*************************************************************
Synopsis [Strashes one logic node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ivy_Obj_t * Abc_NodeStrashAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode )
{
int fUseFactor = 1;
char * pSop;
Ivy_Obj_t * pFanin0, * pFanin1;
assert( Abc_ObjIsNode(pNode) );
// consider the case when the graph is an AIG
if ( Abc_NtkIsStrash(pNode->pNtk) )
{
if ( Abc_AigNodeIsConst(pNode) )
return Ivy_ManConst1(pMan);
pFanin0 = (Ivy_Obj_t *)Abc_ObjFanin0(pNode)->pCopy;
pFanin0 = Ivy_NotCond( pFanin0, Abc_ObjFaninC0(pNode) );
pFanin1 = (Ivy_Obj_t *)Abc_ObjFanin1(pNode)->pCopy;
pFanin1 = Ivy_NotCond( pFanin1, Abc_ObjFaninC1(pNode) );
return Ivy_And( pMan, pFanin0, pFanin1 );
}
// get the SOP of the node
if ( Abc_NtkHasMapping(pNode->pNtk) )
pSop = Mio_GateReadSop((Mio_Gate_t *)pNode->pData);
else
pSop = (char *)pNode->pData;
// consider the constant node
if ( Abc_NodeIsConst(pNode) )
return Ivy_NotCond( Ivy_ManConst1(pMan), Abc_SopIsConst0(pSop) );
// decide when to use factoring
if ( fUseFactor && Abc_ObjFaninNum(pNode) > 2 && Abc_SopGetCubeNum(pSop) > 1 && !Abc_SopIsExorType(pSop) )
return Abc_NodeStrashAigFactorAig( pMan, pNode, pSop );
return Abc_NodeStrashAigSopAig( pMan, pNode, pSop );
}
/**Function*************************************************************
Synopsis [Strashes one logic node using its SOP.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ivy_Obj_t * Abc_NodeStrashAigSopAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode, char * pSop )
{
Abc_Obj_t * pFanin;
Ivy_Obj_t * pAnd, * pSum;
char * pCube;
int i, nFanins;
int fExor = Abc_SopIsExorType(pSop);
// get the number of node's fanins
nFanins = Abc_ObjFaninNum( pNode );
assert( nFanins == Abc_SopGetVarNum(pSop) );
// go through the cubes of the node's SOP
pSum = Ivy_Not( Ivy_ManConst1(pMan) );
Abc_SopForEachCube( pSop, nFanins, pCube )
{
// create the AND of literals
pAnd = Ivy_ManConst1(pMan);
Abc_ObjForEachFanin( pNode, pFanin, i ) // pFanin can be a net
{
if ( pCube[i] == '1' )
pAnd = Ivy_And( pMan, pAnd, (Ivy_Obj_t *)pFanin->pCopy );
else if ( pCube[i] == '0' )
pAnd = Ivy_And( pMan, pAnd, Ivy_Not((Ivy_Obj_t *)pFanin->pCopy) );
}
// add to the sum of cubes
if ( fExor )
pSum = Ivy_Exor( pMan, pSum, pAnd );
else
pSum = Ivy_Or( pMan, pSum, pAnd );
}
// decide whether to complement the result
if ( Abc_SopIsComplement(pSop) )
pSum = Ivy_Not(pSum);
return pSum;
}
/**Function*************************************************************
Synopsis [Strashed n-input XOR function.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ivy_Obj_t * Abc_NodeStrashAigExorAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode, char * pSop )
{
Abc_Obj_t * pFanin;
Ivy_Obj_t * pSum;
int i, nFanins;
// get the number of node's fanins
nFanins = Abc_ObjFaninNum( pNode );
assert( nFanins == Abc_SopGetVarNum(pSop) );
// go through the cubes of the node's SOP
pSum = Ivy_Not( Ivy_ManConst1(pMan) );
for ( i = 0; i < nFanins; i++ )
{
pFanin = Abc_ObjFanin( pNode, i );
pSum = Ivy_Exor( pMan, pSum, (Ivy_Obj_t *)pFanin->pCopy );
}
if ( Abc_SopIsComplement(pSop) )
pSum = Ivy_Not(pSum);
return pSum;
}
/**Function*************************************************************
Synopsis [Strashes one logic node using its SOP.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ivy_Obj_t * Abc_NodeStrashAigFactorAig( Ivy_Man_t * pMan, Abc_Obj_t * pRoot, char * pSop )
{
Dec_Graph_t * pFForm;
Dec_Node_t * pNode;
Ivy_Obj_t * pAnd;
int i;
// extern Ivy_Obj_t * Dec_GraphToNetworkAig( Ivy_Man_t * pMan, Dec_Graph_t * pGraph );
// assert( 0 );
// perform factoring
pFForm = Dec_Factor( pSop );
// collect the fanins
Dec_GraphForEachLeaf( pFForm, pNode, i )
pNode->pFunc = Abc_ObjFanin(pRoot,i)->pCopy;
// perform strashing
// pAnd = Dec_GraphToNetworkAig( pMan, pFForm );
pAnd = Dec_GraphToNetworkIvy( pMan, pFForm );
// pAnd = NULL;
Dec_GraphFree( pFForm );
return pAnd;
}
/**Function*************************************************************
Synopsis [Strashes one logic node using its SOP.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Abc_NtkCollectLatchValuesIvy( Abc_Ntk_t * pNtk, int fUseDcs )
{
Abc_Obj_t * pLatch;
Vec_Int_t * vArray;
int i;
vArray = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) );
Abc_NtkForEachLatch( pNtk, pLatch, i )
{
if ( fUseDcs || Abc_LatchIsInitDc(pLatch) )
Vec_IntPush( vArray, IVY_INIT_DC );
else if ( Abc_LatchIsInit1(pLatch) )
Vec_IntPush( vArray, IVY_INIT_1 );
else if ( Abc_LatchIsInit0(pLatch) )
Vec_IntPush( vArray, IVY_INIT_0 );
else assert( 0 );
}
return vArray;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END