From c0ef1f469a3204adbd26edec0b9d3af56532d794 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 18 Jan 2006 08:01:00 -0800 Subject: Version abc60118 --- src/base/abci/abc.c | 13 +- src/base/abci/abcNewAig.c | 376 ++++++++++++++++++++++++++++++++++++++++++++++ src/base/abci/abcSat.c | 6 +- 3 files changed, 385 insertions(+), 10 deletions(-) create mode 100644 src/base/abci/abcNewAig.c (limited to 'src/base/abci') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 259187bf..5f5c4b49 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -3782,8 +3782,9 @@ usage: int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; - Abc_Ntk_t * pNtk;//, * pNtkRes; + Abc_Ntk_t * pNtk, * pNtkRes; int c; + extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk ); pNtk = Abc_FrameReadNet(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -3807,19 +3808,18 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - if ( !Abc_NtkIsStrash(pNtk) ) + if ( Abc_NtkIsSeq(pNtk) ) { - fprintf( pErr, "Only works for strashed networks.\n" ); + fprintf( pErr, "Only works for non-sequential networks.\n" ); return 1; } // Abc_NtkTestEsop( pNtk ); // Abc_NtkTestSop( pNtk ); // printf( "This command is currently not used.\n" ); - -/* // run the command - pNtkRes = Abc_NtkMiterForCofactors( pNtk, 0, 0, -1 ); +// pNtkRes = Abc_NtkMiterForCofactors( pNtk, 0, 0, -1 ); + pNtkRes = Abc_NtkNewAig( pNtk ); if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); @@ -3827,7 +3827,6 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) } // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); -*/ return 0; usage: diff --git a/src/base/abci/abcNewAig.c b/src/base/abci/abcNewAig.c new file mode 100644 index 00000000..33f58135 --- /dev/null +++ b/src/base/abci/abcNewAig.c @@ -0,0 +1,376 @@ +/**CFile**************************************************************** + + FileName [aigNewAig.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: aigNewAig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "extra.h" +#include "dec.h" +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ); +static Aig_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtkOld ); + +static void Abc_NtkStrashPerformAig( Abc_Ntk_t * pNtk, Aig_Man_t * pMan ); +static Aig_Node_t * Abc_NodeStrashAig( Aig_Man_t * pMan, Abc_Obj_t * pNode ); +static Aig_Node_t * Abc_NodeStrashAigSopAig( Aig_Man_t * pMan, Abc_Obj_t * pNode, char * pSop ); +static Aig_Node_t * Abc_NodeStrashAigExorAig( Aig_Man_t * pMan, Abc_Obj_t * pNode, char * pSop ); +static Aig_Node_t * Abc_NodeStrashAigFactorAig( Aig_Man_t * pMan, Abc_Obj_t * pNode, char * pSop ); +extern char * Mio_GateReadSop( void * pGate ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk ) +{ + Aig_Man_t * pMan; + Abc_Ntk_t * pNtkAig; + Aig_ProofType_t RetValue; + int fCleanup = 1; + int nNodes; + + assert( !Abc_NtkIsNetlist(pNtk) ); + assert( !Abc_NtkIsSeq(pNtk) ); + if ( Abc_NtkIsBddLogic(pNtk) ) + Abc_NtkBddToSop(pNtk); + // 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_NtkToAig( pNtk ); + // execute a command in the AIG manager + RetValue = Aig_FraigProve( pMan ); + if ( RetValue == AIG_PROOF_SAT ) + printf( "Satisfiable.\n" ); + else if ( RetValue == AIG_PROOF_UNSAT ) + printf( "Unsatisfiable.\n" ); + else if ( RetValue == AIG_PROOF_TIMEOUT ) + printf( "Undecided.\n" ); + else + assert( 0 ); + + // convert from the AIG manager + pNtkAig = Abc_NtkFromAig( pNtk, pMan ); + Aig_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 ) ) + { + printf( "Abc_NtkStrash: The network check has failed.\n" ); + Abc_NtkDelete( pNtkAig ); + return NULL; + } + return pNtkAig; +} + +/**Function************************************************************* + + Synopsis [Converts the network from the AIG manager into ABC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) +{ + Abc_Ntk_t * pNtk; + Abc_Obj_t * pObj, * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1; + Aig_Node_t * pAnd; + int i; + // perform strashing + pNtk = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG ); + // transfer the pointers to the basic nodes + Aig_ManConst1(pMan)->Data = Abc_NtkConst1(pNtk)->Id; + Abc_NtkForEachCi( pNtkOld, pObj, i ) + Aig_ManPi(pMan, i)->Data = pObj->pCopy->Id; + // rebuild the AIG + Aig_ManForEachAnd( pMan, pAnd, i ) + { + // add the first fanins + pFaninNew0 = Abc_NtkObj( pNtk, Aig_NodeFanin0(pAnd)->Data ); + pFaninNew0 = Abc_ObjNotCond( pFaninNew0, Aig_NodeFaninC0(pAnd) ); + // add the first second + pFaninNew1 = Abc_NtkObj( pNtk, Aig_NodeFanin1(pAnd)->Data ); + pFaninNew1 = Abc_ObjNotCond( pFaninNew1, Aig_NodeFaninC1(pAnd) ); + // create the new node + pObjNew = Abc_AigAnd( pNtk->pManFunc, pFaninNew0, pFaninNew1 ); + pAnd->Data = pObjNew->Id; + } + // connect the PO nodes + Abc_NtkForEachCo( pNtkOld, pObj, i ) + { + pAnd = Aig_ManPo( pMan, i ); + pFaninNew = Abc_NtkObj( pNtk, Aig_NodeFanin0(pAnd)->Data ); + pFaninNew = Abc_ObjNotCond( pFaninNew, Aig_NodeFaninC0(pAnd) ); + Abc_ObjAddFanin( pObj->pCopy, pFaninNew ); + } + return pNtk; +} + +/**Function************************************************************* + + Synopsis [Converts the network from the AIG manager into ABC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtkOld ) +{ + Aig_Param_t Params; + Aig_Man_t * pMan; + Abc_Obj_t * pObj; + Aig_Node_t * pFanin; + int i; + // create the manager + Aig_ManSetDefaultParams( &Params ); + pMan = Aig_ManStart( &Params ); + // create the PIs + Abc_NtkConst1(pNtkOld)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan); + Abc_NtkForEachCi( pNtkOld, pObj, i ) + pObj->pCopy = (Abc_Obj_t *)Aig_NodeCreatePi(pMan); + // perform the conversion of the internal nodes + Abc_NtkStrashPerformAig( pNtkOld, pMan ); + // create the POs + Abc_NtkForEachCo( pNtkOld, pObj, i ) + { + pFanin = (Aig_Node_t *)Abc_ObjFanin0(pObj)->pCopy; + pFanin = Aig_NotCond( pFanin, Abc_ObjFaninC0(pObj) ); + pObj->pCopy = (Abc_Obj_t *)Aig_NodeCreatePo( pMan, pFanin ); + } + return pMan; +} + +/**Function************************************************************* + + Synopsis [Prepares the network for strashing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkStrashPerformAig( Abc_Ntk_t * pNtk, Aig_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( 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 [] + +***********************************************************************/ +Aig_Node_t * Abc_NodeStrashAig( Aig_Man_t * pMan, Abc_Obj_t * pNode ) +{ + int fUseFactor = 1; + char * pSop; + Aig_Node_t * pFanin0, * pFanin1; + extern int Abc_SopIsExorType( char * pSop ); + + assert( Abc_ObjIsNode(pNode) ); + + // consider the case when the graph is an AIG + if ( Abc_NtkIsStrash(pNode->pNtk) ) + { + if ( Abc_NodeIsConst(pNode) ) + return Aig_ManConst1(pMan); + pFanin0 = (Aig_Node_t *)Abc_ObjFanin0(pNode)->pCopy; + pFanin0 = Aig_NotCond( pFanin0, Abc_ObjFaninC0(pNode) ); + pFanin1 = (Aig_Node_t *)Abc_ObjFanin1(pNode)->pCopy; + pFanin1 = Aig_NotCond( pFanin1, Abc_ObjFaninC1(pNode) ); + return Aig_And( pMan, pFanin0, pFanin1 ); + } + + // get the SOP of the node + if ( Abc_NtkHasMapping(pNode->pNtk) ) + pSop = Mio_GateReadSop(pNode->pData); + else + pSop = pNode->pData; + + // consider the constant node + if ( Abc_NodeIsConst(pNode) ) + return Aig_NotCond( Aig_ManConst1(pMan), Abc_SopIsConst0(pSop) ); + + // consider the special case of EXOR function + if ( Abc_SopIsExorType(pSop) ) + return Abc_NodeStrashAigExorAig( pMan, pNode, pSop ); + + // decide when to use factoring + if ( fUseFactor && Abc_ObjFaninNum(pNode) > 2 && Abc_SopGetCubeNum(pSop) > 1 ) + return Abc_NodeStrashAigFactorAig( pMan, pNode, pSop ); + return Abc_NodeStrashAigSopAig( pMan, pNode, pSop ); +} + +/**Function************************************************************* + + Synopsis [Strashes one logic node using its SOP.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Node_t * Abc_NodeStrashAigSopAig( Aig_Man_t * pMan, Abc_Obj_t * pNode, char * pSop ) +{ + Abc_Obj_t * pFanin; + Aig_Node_t * pAnd, * pSum; + char * pCube; + 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 = Aig_Not( Aig_ManConst1(pMan) ); + Abc_SopForEachCube( pSop, nFanins, pCube ) + { + // create the AND of literals + pAnd = Aig_ManConst1(pMan); + Abc_ObjForEachFanin( pNode, pFanin, i ) // pFanin can be a net + { + if ( pCube[i] == '1' ) + pAnd = Aig_And( pMan, pAnd, (Aig_Node_t *)pFanin->pCopy ); + else if ( pCube[i] == '0' ) + pAnd = Aig_And( pMan, pAnd, Aig_Not((Aig_Node_t *)pFanin->pCopy) ); + } + // add to the sum of cubes + pSum = Aig_Or( pMan, pSum, pAnd ); + } + // decide whether to complement the result + if ( Abc_SopIsComplement(pSop) ) + pSum = Aig_Not(pSum); + return pSum; +} + +/**Function************************************************************* + + Synopsis [Strashed n-input XOR function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Node_t * Abc_NodeStrashAigExorAig( Aig_Man_t * pMan, Abc_Obj_t * pNode, char * pSop ) +{ + Abc_Obj_t * pFanin; + Aig_Node_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 = Aig_Not( Aig_ManConst1(pMan) ); + for ( i = 0; i < nFanins; i++ ) + { + pFanin = Abc_ObjFanin( pNode, i ); + pSum = Aig_Xor( pMan, pSum, (Aig_Node_t *)pFanin->pCopy ); + } + if ( Abc_SopIsComplement(pSop) ) + pSum = Aig_Not(pSum); + return pSum; +} + +/**Function************************************************************* + + Synopsis [Strashes one logic node using its SOP.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Node_t * Abc_NodeStrashAigFactorAig( Aig_Man_t * pMan, Abc_Obj_t * pRoot, char * pSop ) +{ + Dec_Graph_t * pFForm; + Dec_Node_t * pNode; + Aig_Node_t * pAnd; + int i; + extern Aig_Node_t * Dec_GraphToNetworkAig( Aig_Man_t * pMan, Dec_Graph_t * pGraph ); + + // 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 ); + Dec_GraphFree( pFForm ); + return pAnd; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c index 8c8636c5..f7b9892e 100644 --- a/src/base/abci/abcSat.c +++ b/src/base/abci/abcSat.c @@ -534,10 +534,10 @@ int Abc_NtkClauseMux( solver * pSat, Abc_Obj_t * pNode, Abc_Obj_t * pNodeC, Abc_ Vec_IntPush( vVars, toLitCond(VarF, 1) ); if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) return 0; - + if ( VarT == VarE ) { - assert( fCompT == !fCompE ); +// assert( fCompT == !fCompE ); return 1; } @@ -774,7 +774,7 @@ solver * Abc_NtkMiterSatCreate2( Abc_Ntk_t * pNtk ) RetValue = Abc_NtkMiterSatCreate2Int( pSat, pNtk ); Abc_NtkForEachObj( pNtk, pNode, i ) pNode->fMarkA = 0; - Asat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 ); +// Asat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 ); if ( RetValue == 0 ) { solver_delete(pSat); -- cgit v1.2.3