From d6804597a397379f826810a736ccbe99bf56c497 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 24 Jun 2007 08:01:00 -0700 Subject: Version abc70624 --- src/base/abci/abc.c | 24 ++++++++++++---- src/base/abci/abcDar.c | 76 +++++++++++++++++++++++++++++++++++++++++++++++--- 2 files changed, 90 insertions(+), 10 deletions(-) (limited to 'src/base/abci') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index d5321e6d..36311596 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -26,6 +26,7 @@ #include "fpga.h" #include "if.h" #include "res.h" +//#include "dar.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -330,7 +331,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) // Kit_TruthCountMintermsPrecomp(); // Kit_DsdPrecompute4Vars(); -// Dar_LibStart(); + Dar_LibStart(); } /**Function************************************************************* @@ -346,7 +347,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) ***********************************************************************/ void Abc_End() { -// Dar_LibStop(); + Dar_LibStop(); Abc_NtkFraigStoreClean(); // Rwt_Man4ExplorePrint(); @@ -6048,7 +6049,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) } */ // Abc_Ntk4VarTable( pNtk ); -// Dat_NtkGenerateArrays( pNtk ); +// Dar_NtkGenerateArrays( pNtk ); +// Dar_ManDeriveCnfTest2(); if ( !Abc_NtkIsStrash(pNtk) ) { @@ -7301,6 +7303,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) int fExdc; int c; int fPartition = 0; + extern void Abc_NtkFraigPartitionedTime( Abc_Ntk_t * pNtk, void * pParams ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -10535,6 +10538,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv ) char ** pArgvNew; int nArgcNew; int c; + int fRetime; int fSat; int fVerbose; int nFrames; @@ -10544,6 +10548,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv ) extern void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit, int nFrames ); extern int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose ); + extern void Abc_NtkSecRetime( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ); pNtk = Abc_FrameReadNtk(pAbc); @@ -10551,6 +10556,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults + fRetime = 0; // verification after retiming fSat = 0; fVerbose = 0; nFrames = 5; @@ -10558,7 +10564,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv ) nConfLimit = 10000; nInsLimit = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FTCIsvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FTCIsrvh" ) ) != EOF ) { switch ( c ) { @@ -10606,6 +10612,9 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nInsLimit < 0 ) goto usage; break; + case 'r': + fRetime ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -10629,7 +10638,9 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; // perform equivalence checking - if ( fSat ) + if ( fRetime ) + Abc_NtkSecRetime( pNtk1, pNtk2 ); + else if ( fSat ) Abc_NtkSecSat( pNtk1, pNtk2, nConfLimit, nInsLimit, nFrames ); else Abc_NtkSecFraig( pNtk1, pNtk2, nSeconds, nFrames, fVerbose ); @@ -10639,9 +10650,10 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: sec [-F num] [-T num] [-C num] [-I num] [-svh] \n" ); + fprintf( pErr, "usage: sec [-F num] [-T num] [-C num] [-I num] [-srvh] \n" ); fprintf( pErr, "\t performs bounded sequential equivalence checking\n" ); fprintf( pErr, "\t-s : toggle \"SAT only\" and \"FRAIG + SAT\" [default = %s]\n", fSat? "SAT only": "FRAIG + SAT" ); + fprintf( pErr, "\t-r : toggles retiming verification [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames ); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 81278515..a936f9bf 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -53,7 +53,10 @@ Dar_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk ) pObj->pCopy = (Abc_Obj_t *)Dar_ObjCreatePi(pMan); // perform the conversion of the internal nodes (assumes DFS ordering) Abc_NtkForEachNode( pNtk, pObj, i ) + { pObj->pCopy = (Abc_Obj_t *)Dar_And( pMan, (Dar_Obj_t *)Abc_ObjChild0Copy(pObj), (Dar_Obj_t *)Abc_ObjChild1Copy(pObj) ); +// printf( "%d->%d ", pObj->Id, ((Dar_Obj_t *)pObj->pCopy)->Id ); + } // create the POs Abc_NtkForEachCo( pNtk, pObj, i ) Dar_ObjCreatePo( pMan, (Dar_Obj_t *)Abc_ObjChild0Copy(pObj) ); @@ -87,7 +90,10 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Dar_Man_t * pMan ) // rebuild the AIG vNodes = Dar_ManDfs( pMan ); Vec_PtrForEachEntry( vNodes, pObj, i ) - pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Dar_ObjChild0Copy(pObj), (Abc_Obj_t *)Dar_ObjChild1Copy(pObj) ); + if ( Dar_ObjIsBuf(pObj) ) + pObj->pData = (Abc_Obj_t *)Dar_ObjChild0Copy(pObj); + else + pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Dar_ObjChild0Copy(pObj), (Abc_Obj_t *)Dar_ObjChild1Copy(pObj) ); Vec_PtrFree( vNodes ); // connect the PO nodes Dar_ManForEachPo( pMan, pObj, i ) @@ -193,6 +199,52 @@ int * Abc_NtkGetLatchValues( Abc_Ntk_t * pNtk ) return pArray; } +/**Function************************************************************* + + Synopsis [Performs verification after retiming.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkSecRetime( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ) +{ + int fRemove1, fRemove2; + Dar_Man_t * pMan1, * pMan2; + int * pArray; + + fRemove1 = (!Abc_NtkIsStrash(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0, 0, 0)); + fRemove2 = (!Abc_NtkIsStrash(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0, 0, 0)); + + + pMan1 = Abc_NtkToDar( pNtk1 ); + pMan2 = Abc_NtkToDar( pNtk2 ); + + Dar_ManPrintStats( pMan1 ); + Dar_ManPrintStats( pMan2 ); + + pArray = Abc_NtkGetLatchValues(pNtk1); + Dar_ManSeqStrash( pMan1, Abc_NtkLatchNum(pNtk1), pArray ); + free( pArray ); + + pArray = Abc_NtkGetLatchValues(pNtk2); + Dar_ManSeqStrash( pMan2, Abc_NtkLatchNum(pNtk2), pArray ); + free( pArray ); + + Dar_ManPrintStats( pMan1 ); + Dar_ManPrintStats( pMan2 ); + + Dar_ManStop( pMan1 ); + Dar_ManStop( pMan2 ); + + + if ( fRemove1 ) Abc_NtkDelete( pNtk1 ); + if ( fRemove2 ) Abc_NtkDelete( pNtk2 ); +} + /**Function************************************************************* Synopsis [Gives the current ABC network to AIG manager for processing.] @@ -208,7 +260,7 @@ Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk ) { Abc_Ntk_t * pNtkAig; Dar_Man_t * pMan;//, * pTemp; - int * pArray; +// int * pArray; assert( Abc_NtkIsStrash(pNtk) ); // convert to the AIG manager @@ -223,15 +275,29 @@ Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk ) } // perform balance Dar_ManPrintStats( pMan ); - +/* pArray = Abc_NtkGetLatchValues(pNtk); Dar_ManSeqStrash( pMan, Abc_NtkLatchNum(pNtk), pArray ); free( pArray ); +*/ // Dar_ManDumpBlif( pMan, "aig_temp.blif" ); // pMan->pPars = Dar_ManDefaultParams(); -// Dar_ManRewrite( pMan ); + Dar_ManRewrite( pMan ); Dar_ManPrintStats( pMan ); + Dar_ManPrintRuntime( pMan ); +// Dar_ManComputeCuts( pMan ); + +/* +{ +extern Dar_Cnf_t * Dar_ManDeriveCnf( Dar_Man_t * p ); +extern void Dar_CnfFree( Dar_Cnf_t * pCnf ); +Dar_Cnf_t * pCnf; +pCnf = Dar_ManDeriveCnf( pMan ); +Dar_CnfFree( pCnf ); +} +*/ + // convert from the AIG manager if ( Dar_ManLatchNum(pMan) ) pNtkAig = Abc_NtkFromDarSeq( pNtk, pMan ); @@ -250,6 +316,8 @@ Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk ) return pNtkAig; } + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3