From 20c2b197984ad6da0f28eb9ef86f95b362d96335 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 7 Oct 2005 08:01:00 -0700 Subject: Version abc51007 --- src/base/abci/abc.c | 22 +- src/base/abci/abcUnreach.c | 2 +- src/base/abci/abcVanEijk.c | 41 +- src/base/abci/abcVanImp.c | 978 +++++++++++++++++++++++++++++++++++++++++++++ src/base/abci/abcVerify.c | 317 ++++++++++++--- 5 files changed, 1290 insertions(+), 70 deletions(-) create mode 100644 src/base/abci/abcVanImp.c (limited to 'src/base/abci') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index cde9c16b..24301ac3 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -2293,7 +2293,7 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv ) } nFrames = atoi(argv[util_optind]); util_optind++; - if ( nFrames < 0 ) + if ( nFrames <= 0 ) goto usage; break; case 'i': @@ -5114,8 +5114,10 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; int nFrames; int fExdc; + int fImp; int fVerbose; extern Abc_Ntk_t * Abc_NtkVanEijk( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkVanImp( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose ); pNtk = Abc_FrameReadNet(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -5124,9 +5126,10 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults nFrames = 1; fExdc = 1; + fImp = 0; fVerbose = 1; util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "Fevh" ) ) != EOF ) + while ( ( c = util_getopt( argc, argv, "Feivh" ) ) != EOF ) { switch ( c ) { @@ -5138,12 +5141,15 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) } nFrames = atoi(argv[util_optind]); util_optind++; - if ( nFrames < 0 ) + if ( nFrames <= 0 ) goto usage; break; case 'e': fExdc ^= 1; break; + case 'i': + fImp ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -5179,7 +5185,10 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get the new network - pNtkRes = Abc_NtkVanEijk( pNtk, nFrames, fExdc, fVerbose ); + if ( fImp ) + pNtkRes = Abc_NtkVanImp( pNtk, nFrames, fExdc, fVerbose ); + else + pNtkRes = Abc_NtkVanEijk( pNtk, nFrames, fExdc, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Sequential FPGA mapping has failed.\n" ); @@ -5190,10 +5199,11 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: seq_sweep [-F num] [-vh]\n" ); + fprintf( pErr, "usage: seq_sweep [-F num] [-eivh]\n" ); fprintf( pErr, "\t performs sequential sweep using van Eijk's method\n" ); fprintf( pErr, "\t-F num : number of time frames in the base case [default = %d]\n", nFrames ); fprintf( pErr, "\t-e : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" ); + fprintf( pErr, "\t-i : toggle computing implications [default = %s]\n", fImp? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -5342,7 +5352,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv ) } nFrames = atoi(argv[util_optind]); util_optind++; - if ( nFrames < 0 ) + if ( nFrames <= 0 ) goto usage; break; case 'T': diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c index e932d076..a8ecef5c 100644 --- a/src/base/abci/abcUnreach.c +++ b/src/base/abci/abcUnreach.c @@ -285,7 +285,7 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn // start the new network pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD ); - pNtkNew->pName = util_strsav("exdc"); + pNtkNew->pName = util_strsav( "exdc" ); pNtkNew->pSpec = NULL; // create PIs corresponding to LOs diff --git a/src/base/abci/abcVanEijk.c b/src/base/abci/abcVanEijk.c index d0179514..d7406ba6 100644 --- a/src/base/abci/abcVanEijk.c +++ b/src/base/abci/abcVanEijk.c @@ -35,10 +35,12 @@ static int Abc_NtkVanEijkClassesRefine( Abc_Ntk_t * pNtk, Vec_Ptr_t * static void Abc_NtkVanEijkClassesOrder( Vec_Ptr_t * vClasses ); static int Abc_NtkVanEijkClassesCountPairs( Vec_Ptr_t * vClasses ); static void Abc_NtkVanEijkClassesTest( Abc_Ntk_t * pNtkSingle, Vec_Ptr_t * vClasses ); -static Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames, int fAddLast, int fShortNames ); -static void Abc_NtkVanEijkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vCorresp, Vec_Ptr_t * vOrder, int fShortNames ); -static Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit ); -static Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtkInit, Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses ); + +extern Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames, int fAddLast, int fShortNames ); +extern void Abc_NtkVanEijkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vCorresp, Vec_Ptr_t * vOrder, int fShortNames ); +extern Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit ); + +static Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses ); //////////////////////////////////////////////////////////////////////// /// INLINED FUNCTIONS /// @@ -99,6 +101,7 @@ Abc_Ntk_t * Abc_NtkVanEijk( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbo Fraig_ParamsSetDefaultFull( &Params ); pNtkSingle = Abc_NtkFraig( pNtk, &Params, 0, 0 ); Abc_AigSetNodePhases( pNtkSingle ); + Abc_NtkCleanNext(pNtkSingle); // get the equivalence classes vClasses = Abc_NtkVanEijkClasses( pNtkSingle, nFrames, fVerbose ); @@ -109,7 +112,7 @@ Abc_Ntk_t * Abc_NtkVanEijk( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbo // pNtkNew = Abc_NtkDup( pNtkSingle ); // derive the EXDC network if asked if ( fExdc ) - pNtkNew->pExdc = Abc_NtkVanEijkDeriveExdc( pNtk, pNtkSingle, vClasses ); + pNtkNew->pExdc = Abc_NtkVanEijkDeriveExdc( pNtkSingle, vClasses ); } else pNtkNew = Abc_NtkDup( pNtkSingle ); @@ -137,23 +140,23 @@ Vec_Ptr_t * Abc_NtkVanEijkClasses( Abc_Ntk_t * pNtkSingle, int nFrames, int fVer Abc_Ntk_t * pNtkMulti; Vec_Ptr_t * vCorresp, * vClasses; int nIter, RetValue; + int nAddFrames = 0; if ( fVerbose ) printf( "The number of ANDs after FRAIGing = %d.\n", Abc_NtkNodeNum(pNtkSingle) ); // get the AIG of the base case vCorresp = Vec_PtrAlloc( 100 ); - Abc_NtkCleanNext(pNtkSingle); - pNtkMulti = Abc_NtkVanEijkFrames( pNtkSingle, vCorresp, nFrames, 0, 0 ); + pNtkMulti = Abc_NtkVanEijkFrames( pNtkSingle, vCorresp, nFrames + nAddFrames, 0, 0 ); if ( fVerbose ) - printf( "The number of ANDs in %d timeframes = %d.\n", nFrames, Abc_NtkNodeNum(pNtkMulti) ); + printf( "The number of ANDs in %d timeframes = %d.\n", nFrames + nAddFrames, Abc_NtkNodeNum(pNtkMulti) ); // FRAIG the initialized frames (labels the nodes of pNtkMulti with FRAIG nodes to be used as hash keys) pFraig = Abc_NtkVanEijkFraig( pNtkMulti, 1 ); Fraig_ManFree( pFraig ); // find initial equivalence classes - vClasses = Abc_NtkVanEijkClassesDeriveBase( pNtkSingle, vCorresp, nFrames ); + vClasses = Abc_NtkVanEijkClassesDeriveBase( pNtkSingle, vCorresp, nFrames + nAddFrames ); if ( fVerbose ) printf( "The number of classes in the base case = %5d. Pairs = %8d.\n", Vec_PtrSize(vClasses), Abc_NtkVanEijkClassesCountPairs(vClasses) ); Abc_NtkDelete( pNtkMulti ); @@ -192,6 +195,12 @@ Vec_Ptr_t * Abc_NtkVanEijkClasses( Abc_Ntk_t * pNtkSingle, int nFrames, int fVer for ( pObj = pClass; pObj; pObj = pObj->pNext ) Counter++; printf( " %d", Counter ); +/* + printf( " = {" ); + for ( pObj = pClass; pObj; pObj = pObj->pNext ) + printf( " %d", pObj->Id ); + printf( " } " ); +*/ } printf( "\n" ); } @@ -541,7 +550,9 @@ Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nF pLatch->pNext = NULL; } // remove dangling nodes - Abc_AigCleanup( pNtkFrames->pManFunc ); +// Abc_AigCleanup( pNtkFrames->pManFunc ); + // otherwise some external nodes may have dandling pointers + // make sure that everything is okay if ( !Abc_NtkCheck( pNtkFrames ) ) printf( "Abc_NtkVanEijkFrames: The network check has failed.\n" ); @@ -699,7 +710,7 @@ Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtkInit, Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses ) +Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses ) { Abc_Ntk_t * pNtkNew; Abc_Obj_t * pClass, * pNode, * pRepr, * pObj; @@ -707,6 +718,8 @@ Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtkInit, Abc_Ntk_t * pNtk, Ve Vec_Ptr_t * vCone; int i, k; + assert( Abc_NtkIsStrash(pNtk) ); + // start the network pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc ); pNtkNew->pName = util_strsav("exdc"); @@ -716,7 +729,7 @@ Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtkInit, Abc_Ntk_t * pNtk, Ve Abc_AigConst1(pNtk->pManFunc)->pCopy = Abc_AigConst1(pNtkNew->pManFunc); // for each CI, create PI Abc_NtkForEachCi( pNtk, pObj, i ) - Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName( Abc_NtkCi(pNtkInit,i) ) ); + Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pObj) ); // cannot add latches here because pLatch->pCopy pointers are used // create the cones for each pair of nodes in an equivalence class @@ -756,9 +769,9 @@ Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtkInit, Abc_Ntk_t * pNtk, Ve // for each CO, create PO (skip POs equal to CIs because of name conflict) Abc_NtkForEachPo( pNtk, pObj, i ) if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) ) - Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName( Abc_NtkPo(pNtkInit,i) ) ); + Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName(pObj) ); Abc_NtkForEachLatch( pNtk, pObj, i ) - Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjNameSuffix( Abc_NtkLatch(pNtkInit,i), "_in") ); + Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjNameSuffix( pObj, "_in") ); // link to the POs of the network Abc_NtkForEachPo( pNtk, pObj, i ) diff --git a/src/base/abci/abcVanImp.c b/src/base/abci/abcVanImp.c new file mode 100644 index 00000000..28320028 --- /dev/null +++ b/src/base/abci/abcVanImp.c @@ -0,0 +1,978 @@ +/**CFile**************************************************************** + + FileName [abcVanImp.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Implementation of van Eijk's method for implications.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - October 2, 2005.] + + Revision [$Id: abcVanImp.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "fraig.h" +#include "sim.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Van_Man_t_ Van_Man_t; +struct Van_Man_t_ +{ + // single frame representation + Abc_Ntk_t * pNtkSingle; // single frame + Vec_Int_t * vCounters; // the counters of 1s in the simulation info + Vec_Ptr_t * vZeros; // the set of constant 0 candidates + Vec_Int_t * vImps; // the set of all implications + Vec_Int_t * vImpsMis; // the minimum independent set of implications + // multiple frame representation + Abc_Ntk_t * pNtkMulti; // multiple frame + Vec_Ptr_t * vCorresp; // the correspondence between single frame and multiple frames + // parameters + int nFrames; // the number of timeframes + int nWords; // the number of simulation words + int nIdMax; // the maximum ID in the single frame + int fVerbose; // the verbosiness flag + // statistics + int nPairsAll; + int nImpsAll; + int nEquals; + int nZeros; + // runtime + int timeAll; + int timeSim; + int timeAdd; + int timeCheck; + int timeInfo; + int timeMis; +}; + +static void Abc_NtkVanImpCompute( Van_Man_t * p ); +static Vec_Ptr_t * Abc_NtkVanImpSortByOnes( Van_Man_t * p ); +static void Abc_NtkVanImpComputeAll( Van_Man_t * p ); +static Vec_Int_t * Abc_NtkVanImpComputeMis( Van_Man_t * p ); +static void Abc_NtkVanImpManFree( Van_Man_t * p ); +static void Abc_NtkVanImpFilter( Van_Man_t * p, Fraig_Man_t * pFraig, Vec_Ptr_t * vZeros, Vec_Int_t * vImps ); +static int Abc_NtkVanImpCountEqual( Van_Man_t * p ); + +static Abc_Ntk_t * Abc_NtkVanImpDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vZeros, Vec_Int_t * vImps ); + +extern Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames, int fAddLast, int fShortNames ); +extern void Abc_NtkVanEijkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vCorresp, Vec_Ptr_t * vOrder, int fShortNames ); +extern Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit ); + +//////////////////////////////////////////////////////////////////////// +/// INLINED FUNCTIONS /// +//////////////////////////////////////////////////////////////////////// + +// returns the correspondence of the node in the frame +static inline Abc_Obj_t * Abc_NodeVanImpReadCorresp( Abc_Obj_t * pNode, Vec_Ptr_t * vCorresp, int iFrame ) +{ + return Vec_PtrEntry( vCorresp, iFrame * Abc_NtkObjNumMax(pNode->pNtk) + pNode->Id ); +} +// returns the left node of the implication +static inline Abc_Obj_t * Abc_NodeVanGetLeft( Abc_Ntk_t * pNtk, unsigned Imp ) +{ + return Abc_NtkObj( pNtk, Imp >> 16 ); +} +// returns the right node of the implication +static inline Abc_Obj_t * Abc_NodeVanGetRight( Abc_Ntk_t * pNtk, unsigned Imp ) +{ + return Abc_NtkObj( pNtk, Imp & 0xFFFF ); +} +// returns the implication +static inline unsigned Abc_NodeVanGetImp( Abc_Obj_t * pLeft, Abc_Obj_t * pRight ) +{ + return (pLeft->Id << 16) | pRight->Id; +} +// returns the right node of the implication +static inline void Abc_NodeVanPrintImp( unsigned Imp ) +{ + printf( "%d -> %d ", Imp >> 16, Imp & 0xFFFF ); +} + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Derives implications that hold sequentially.] + + Description [Adds EXDC network to the current network to record the + set of computed sequentially equivalence implications, representing + a subset of unreachable states.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkVanImp( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose ) +{ + Fraig_Params_t Params; + Abc_Ntk_t * pNtkNew; + Van_Man_t * p; + + assert( Abc_NtkIsStrash(pNtk) ); + + // start the manager + p = ALLOC( Van_Man_t, 1 ); + memset( p, 0, sizeof(Van_Man_t) ); + p->nFrames = nFrames; + p->fVerbose = fVerbose; + p->vCorresp = Vec_PtrAlloc( 100 ); + + // FRAIG the network to get rid of combinational equivalences + Fraig_ParamsSetDefaultFull( &Params ); + p->pNtkSingle = Abc_NtkFraig( pNtk, &Params, 0, 0 ); + p->nIdMax = Abc_NtkObjNumMax( p->pNtkSingle ); + Abc_AigSetNodePhases( p->pNtkSingle ); + Abc_NtkCleanNext( p->pNtkSingle ); +// if ( fVerbose ) +// printf( "The number of ANDs in 1 timeframe = %d.\n", Abc_NtkNodeNum(p->pNtkSingle) ); + + // derive multiple time-frames and node correspondence (to be used in the inductive case) + p->pNtkMulti = Abc_NtkVanEijkFrames( p->pNtkSingle, p->vCorresp, nFrames, 1, 0 ); +// if ( fVerbose ) +// printf( "The number of ANDs in %d timeframes = %d.\n", nFrames + 1, Abc_NtkNodeNum(p->pNtkMulti) ); + + // get the implications + Abc_NtkVanImpCompute( p ); + + // create the new network with EXDC correspondingn to the computed implications + if ( fExdc && (Vec_PtrSize(p->vZeros) > 0 || Vec_IntSize(p->vImpsMis) > 0) ) + { + if ( p->pNtkSingle->pExdc ) + { + printf( "The old EXDC network is thrown away.\n" ); + Abc_NtkDelete( p->pNtkSingle->pExdc ); + p->pNtkSingle->pExdc = NULL; + } + pNtkNew = Abc_NtkDup( p->pNtkSingle ); + pNtkNew->pExdc = Abc_NtkVanImpDeriveExdc( p->pNtkSingle, p->vZeros, p->vImpsMis ); + } + else + pNtkNew = Abc_NtkDup( p->pNtkSingle ); + + // free stuff + Abc_NtkVanImpManFree( p ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Frees the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkVanImpManFree( Van_Man_t * p ) +{ + Abc_NtkDelete( p->pNtkMulti ); + Abc_NtkDelete( p->pNtkSingle ); + Vec_PtrFree( p->vCorresp ); + Vec_PtrFree( p->vZeros ); + Vec_IntFree( p->vCounters ); + Vec_IntFree( p->vImpsMis ); + Vec_IntFree( p->vImps ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Derives the minimum independent set of sequential implications.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkVanImpCompute( Van_Man_t * p ) +{ + Fraig_Man_t * pFraig; + Vec_Ptr_t * vZeros; + Vec_Int_t * vImps, * vImpsTemp; + int nIters, clk; + + // compute all implications and count 1s in the simulation info +clk = clock(); + Abc_NtkVanImpComputeAll( p ); +p->timeAll += clock() - clk; + + // compute the MIS +clk = clock(); + p->vImpsMis = Abc_NtkVanImpComputeMis( p ); +p->timeMis += clock() - clk; + + if ( p->fVerbose ) + { + printf( "Pairs = %8d. Imps = %8d. Seq = %7d. MIS = %7d. Equ = %5d. Const = %5d.\n", + p->nPairsAll, p->nImpsAll, Vec_IntSize(p->vImps), Vec_IntSize(p->vImpsMis), p->nEquals, p->nZeros ); + printf( "Start : Seq = %7d. MIS = %7d. Const = %5d.\n", Vec_IntSize(p->vImps), Vec_IntSize(p->vImpsMis), Vec_PtrSize(p->vZeros) ); + } + + // iterate to perform the iterative filtering of implications + for ( nIters = 1; Vec_PtrSize(p->vZeros) > 0 || Vec_IntSize(p->vImps) > 0; nIters++ ) + { + // FRAIG the ununitialized frames + pFraig = Abc_NtkVanEijkFraig( p->pNtkMulti, 0 ); + + // assuming that zeros and imps hold in the first k-1 frames + // check if they hold in the k-th frame + vZeros = Vec_PtrAlloc( 100 ); + vImps = Vec_IntAlloc( 100 ); + Abc_NtkVanImpFilter( p, pFraig, vZeros, vImps ); + Fraig_ManFree( pFraig ); + +clk = clock(); + vImpsTemp = p->vImps; + p->vImps = vImps; + Vec_IntFree( p->vImpsMis ); + p->vImpsMis = Abc_NtkVanImpComputeMis( p ); + p->vImps = vImpsTemp; +p->timeMis += clock() - clk; + + // report the results + if ( p->fVerbose ) + printf( "Iter = %2d: Seq = %7d. MIS = %7d. Const = %5d.\n", nIters, Vec_IntSize(vImps), Vec_IntSize(p->vImpsMis), Vec_PtrSize(vZeros) ); + + // if the fixed point is reaches, quit the loop + if ( Vec_PtrSize(vZeros) == Vec_PtrSize(p->vZeros) && Vec_IntSize(vImps) == Vec_IntSize(p->vImps) ) + { // no change + Vec_PtrFree(vZeros); + Vec_IntFree(vImps); + break; + } + + // update the sets + Vec_PtrFree( p->vZeros ); p->vZeros = vZeros; + Vec_IntFree( p->vImps ); p->vImps = vImps; + } + + // compute the MIS +clk = clock(); + Vec_IntFree( p->vImpsMis ); + p->vImpsMis = Abc_NtkVanImpComputeMis( p ); +// p->vImpsMis = Vec_IntDup( p->vImps ); +p->timeMis += clock() - clk; + if ( p->fVerbose ) + printf( "Final : Seq = %7d. MIS = %7d. Const = %5d.\n", Vec_IntSize(p->vImps), Vec_IntSize(p->vImpsMis), Vec_PtrSize(p->vZeros) ); + + +/* + if ( p->fVerbose ) + { + PRT( "All ", p->timeAll ); + PRT( "Sim ", p->timeSim ); + PRT( "Add ", p->timeAdd ); + PRT( "Check ", p->timeCheck ); + PRT( "Mis ", p->timeMis ); + } +*/ + +/* + // print the implications in the MIS + if ( p->fVerbose ) + { + Abc_Obj_t * pNode, * pNode1, * pNode2; + unsigned Imp; + int i; + if ( Vec_PtrSize(p->vZeros) ) + { + printf( "The const nodes are: " ); + Vec_PtrForEachEntry( p->vZeros, pNode, i ) + printf( "%d(%d) ", pNode->Id, pNode->fPhase ); + printf( "\n" ); + } + if ( Vec_IntSize(p->vImpsMis) ) + { + printf( "The implications are: " ); + Vec_IntForEachEntry( p->vImpsMis, Imp, i ) + { + pNode1 = Abc_NodeVanGetLeft( p->pNtkSingle, Imp ); + pNode2 = Abc_NodeVanGetRight( p->pNtkSingle, Imp ); + printf( "%d(%d)=>%d(%d) ", pNode1->Id, pNode1->fPhase, pNode2->Id, pNode2->fPhase ); + } + printf( "\n" ); + } + } +*/ +} + +/**Function************************************************************* + + Synopsis [Filters zeros and implications by performing one inductive step.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkVanImpFilter( Van_Man_t * p, Fraig_Man_t * pFraig, Vec_Ptr_t * vZeros, Vec_Int_t * vImps ) +{ + ProgressBar * pProgress; + Abc_Obj_t * pNode, * pNodeM1, * pNodeM2, * pNode1, * pNode2, * pObj; + Fraig_Node_t * pFNode1, * pFNode2; + Fraig_Node_t * ppFNodes[2]; + unsigned Imp; + int i, f, k, clk; + +clk = clock(); + for ( f = 0; f < p->nFrames; f++ ) + { + // add new clauses for zeros + Vec_PtrForEachEntry( p->vZeros, pNode, i ) + { + pNodeM1 = Abc_NodeVanImpReadCorresp( pNode, p->vCorresp, f ); + pFNode1 = Fraig_NotCond( Abc_ObjRegular(pNodeM1)->pCopy, Abc_ObjIsComplement(pNodeM1) ); + pFNode1 = Fraig_NotCond( pFNode1, !pNode->fPhase ); + Fraig_ManAddClause( pFraig, &pFNode1, 1 ); + } + // add new clauses for imps + Vec_IntForEachEntry( p->vImps, Imp, i ) + { + pNode1 = Abc_NodeVanGetLeft( p->pNtkSingle, Imp ); + pNode2 = Abc_NodeVanGetRight( p->pNtkSingle, Imp ); + pNodeM1 = Abc_NodeVanImpReadCorresp( pNode1, p->vCorresp, f ); + pNodeM2 = Abc_NodeVanImpReadCorresp( pNode2, p->vCorresp, f ); + pFNode1 = Fraig_NotCond( Abc_ObjRegular(pNodeM1)->pCopy, Abc_ObjIsComplement(pNodeM1) ); + pFNode2 = Fraig_NotCond( Abc_ObjRegular(pNodeM2)->pCopy, Abc_ObjIsComplement(pNodeM2) ); + ppFNodes[0] = Fraig_NotCond( pFNode1, !pNode1->fPhase ); + ppFNodes[1] = Fraig_NotCond( pFNode2, pNode2->fPhase ); +// assert( Fraig_Regular(ppFNodes[0]) != Fraig_Regular(ppFNodes[1]) ); + Fraig_ManAddClause( pFraig, ppFNodes, 2 ); + } + } +p->timeAdd += clock() - clk; + + // check the zero nodes +clk = clock(); + Vec_PtrClear( vZeros ); + Vec_PtrForEachEntry( p->vZeros, pNode, i ) + { + pNodeM1 = Abc_NodeVanImpReadCorresp( pNode, p->vCorresp, p->nFrames ); + pFNode1 = Fraig_NotCond( Abc_ObjRegular(pNodeM1)->pCopy, Abc_ObjIsComplement(pNodeM1) ); + pFNode1 = Fraig_Regular(pFNode1); + pFNode2 = Fraig_ManReadConst1(pFraig); + if ( pFNode1 == pFNode2 || Fraig_NodeIsEquivalent( pFraig, pFNode1, pFNode2, -1, 100 ) ) + Vec_PtrPush( vZeros, pNode ); + else + { + // since we disproved this zero, we should add all possible implications to p->vImps + // these implications will be checked below and only correct ones will remain + Abc_NtkForEachObj( p->pNtkSingle, pObj, k ) + { + if ( Abc_ObjIsPo(pObj) ) + continue; + if ( Vec_IntEntry( p->vCounters, pObj->Id ) > 0 ) + Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode, pObj) ); + } + } + } + + // check implications + pProgress = Extra_ProgressBarStart( stdout, p->vImps->nSize ); + Vec_IntClear( vImps ); + Vec_IntForEachEntry( p->vImps, Imp, i ) + { + Extra_ProgressBarUpdate( pProgress, i, NULL ); + pNode1 = Abc_NodeVanGetLeft( p->pNtkSingle, Imp ); + pNode2 = Abc_NodeVanGetRight( p->pNtkSingle, Imp ); + pNodeM1 = Abc_NodeVanImpReadCorresp( pNode1, p->vCorresp, p->nFrames ); + pNodeM2 = Abc_NodeVanImpReadCorresp( pNode2, p->vCorresp, p->nFrames ); + pFNode1 = Fraig_NotCond( Abc_ObjRegular(pNodeM1)->pCopy, Abc_ObjIsComplement(pNodeM1) ); + pFNode2 = Fraig_NotCond( Abc_ObjRegular(pNodeM2)->pCopy, Abc_ObjIsComplement(pNodeM2) ); + pFNode1 = Fraig_NotCond( pFNode1, !pNode1->fPhase ); + pFNode2 = Fraig_NotCond( pFNode2, pNode2->fPhase ); + if ( pFNode1 == Fraig_Not(pFNode2) ) + { + Vec_IntPush( vImps, Imp ); + continue; + } + if ( pFNode1 == pFNode2 ) + { + if ( pFNode1 == Fraig_Not( Fraig_ManReadConst1(pFraig) ) ) + continue; + if ( pFNode1 == Fraig_ManReadConst1(pFraig) ) + { + Vec_IntPush( vImps, Imp ); + continue; + } + pFNode1 = Fraig_Regular(pFNode1); + pFNode2 = Fraig_ManReadConst1(pFraig); + if ( Fraig_NodeIsEquivalent( pFraig, pFNode1, pFNode2, -1, 100 ) ) + Vec_IntPush( vImps, Imp ); + continue; + } + + if ( Fraig_ManCheckClauseUsingSat( pFraig, pFNode1, pFNode2, -1 ) ) + Vec_IntPush( vImps, Imp ); + } + Extra_ProgressBarStop( pProgress ); +p->timeCheck += clock() - clk; +} + +/**Function************************************************************* + + Synopsis [Computes all implications.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkVanImpComputeAll( Van_Man_t * p ) +{ + ProgressBar * pProgress; + Fraig_Man_t * pManSingle; + Vec_Ptr_t * vInfo; + Abc_Obj_t * pObj, * pNode1, * pNode2, * pConst1; + Fraig_Node_t * pFNode1, * pFNode2; + unsigned * pPats1, * pPats2; + int nFrames, nUnsigned, RetValue; + int clk, i, k, Count1, Count2; + + // decide how many frames to simulate + nFrames = 32; + nUnsigned = 32; + p->nWords = nFrames * nUnsigned; + + // simulate randomly the initialized frames +clk = clock(); + vInfo = Sim_SimulateSeqRandom( p->pNtkSingle, nFrames, nUnsigned ); + + // complement the info for those nodes whose phase is 1 + Abc_NtkForEachObj( p->pNtkSingle, pObj, i ) + if ( pObj->fPhase ) + Sim_UtilSetCompl( Sim_SimInfoGet(vInfo, pObj), p->nWords ); + + // compute the number of ones for each node + p->vCounters = Sim_UtilCountOnesArray( vInfo, p->nWords ); +p->timeSim += clock() - clk; + + // FRAIG the uninitialized frame + pManSingle = Abc_NtkVanEijkFraig( p->pNtkSingle, 0 ); + // now pNode->pCopy are assigned the pointers to the corresponding FRAIG nodes + +/* +Abc_NtkForEachPi( p->pNtkSingle, pNode1, i ) +printf( "PI = %d\n", pNode1->Id ); +Abc_NtkForEachLatch( p->pNtkSingle, pNode1, i ) +printf( "Latch = %d\n", pNode1->Id ); +Abc_NtkForEachPo( p->pNtkSingle, pNode1, i ) +printf( "PO = %d\n", pNode1->Id ); +*/ + + // go through the pairs of signals in the frames + pProgress = Extra_ProgressBarStart( stdout, p->nIdMax ); + pConst1 = Abc_AigConst1( p->pNtkSingle->pManFunc ); + p->vImps = Vec_IntAlloc( 100 ); + p->vZeros = Vec_PtrAlloc( 100 ); + Abc_NtkForEachObj( p->pNtkSingle, pNode1, i ) + { + if ( Abc_ObjIsPo(pNode1) ) + continue; + if ( pNode1 == pConst1 ) + continue; + Extra_ProgressBarUpdate( pProgress, i, NULL ); + + // get the number of zeros of this node + Count1 = Vec_IntEntry( p->vCounters, pNode1->Id ); + if ( Count1 == 0 ) + { + Vec_PtrPush( p->vZeros, pNode1 ); + p->nZeros++; + continue; + } + pPats1 = Sim_SimInfoGet(vInfo, pNode1); + + Abc_NtkForEachObj( p->pNtkSingle, pNode2, k ) + { + if ( k >= i ) + break; + if ( Abc_ObjIsPo(pNode2) ) + continue; + if ( pNode2 == pConst1 ) + continue; + p->nPairsAll++; + + // here we have a pair of nodes (pNode1 and pNode2) + // such that Id(pNode1) < Id(pNode2) + assert( pNode2->Id < pNode1->Id ); + + // get the number of zeros of this node + Count2 = Vec_IntEntry( p->vCounters, pNode2->Id ); + if ( Count2 == 0 ) + continue; + pPats2 = Sim_SimInfoGet(vInfo, pNode2); + + // check for implications + if ( Count1 < Count2 ) + { +//clk = clock(); + RetValue = Sim_UtilInfoIsImp( pPats1, pPats2, p->nWords ); +//p->timeInfo += clock() - clk; + if ( !RetValue ) + continue; + p->nImpsAll++; + // pPats1 => pPats2 or pPats1' v pPats2 + pFNode1 = Fraig_NotCond( pNode1->pCopy, !pNode1->fPhase ); + pFNode2 = Fraig_NotCond( pNode2->pCopy, pNode2->fPhase ); + // check if this implication is combinational + if ( Fraig_ManCheckClauseUsingSimInfo( pManSingle, pFNode1, pFNode2 ) ) + continue; + // otherwise record it + Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode1, pNode2) ); + } + else if ( Count2 < Count1 ) + { +//clk = clock(); + RetValue = Sim_UtilInfoIsImp( pPats2, pPats1, p->nWords ); +//p->timeInfo += clock() - clk; + if ( !RetValue ) + continue; + p->nImpsAll++; + // pPats2 => pPats2 or pPats2' v pPats1 + pFNode2 = Fraig_NotCond( pNode2->pCopy, !pNode2->fPhase ); + pFNode1 = Fraig_NotCond( pNode1->pCopy, pNode1->fPhase ); + // check if this implication is combinational + if ( Fraig_ManCheckClauseUsingSimInfo( pManSingle, pFNode1, pFNode2 ) ) + continue; + // otherwise record it + Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode2, pNode1) ); + } + else + { +//clk = clock(); + RetValue = Sim_UtilInfoIsEqual(pPats1, pPats2, p->nWords); +//p->timeInfo += clock() - clk; + if ( !RetValue ) + continue; + p->nEquals++; + // get the FRAIG nodes + pFNode1 = Fraig_NotCond( pNode1->pCopy, pNode1->fPhase ); + pFNode2 = Fraig_NotCond( pNode2->pCopy, pNode2->fPhase ); + + // check if this implication is combinational + if ( Fraig_ManCheckClauseUsingSimInfo( pManSingle, Fraig_Not(pFNode1), pFNode2 ) ) + { + if ( !Fraig_ManCheckClauseUsingSimInfo( pManSingle, pFNode1, Fraig_Not(pFNode2) ) ) + Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode2, pNode1) ); + else + assert( 0 ); // impossible for FRAIG + } + else + { + Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode1, pNode2) ); + if ( !Fraig_ManCheckClauseUsingSimInfo( pManSingle, pFNode1, Fraig_Not(pFNode2) ) ) + Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode2, pNode1) ); + } + } +// printf( "Implication %d %d -> %d %d \n", pNode1->Id, pNode1->fPhase, pNode2->Id, pNode2->fPhase ); + } + } + Fraig_ManFree( pManSingle ); + Sim_UtilInfoFree( vInfo ); + Extra_ProgressBarStop( pProgress ); +} + + +/**Function************************************************************* + + Synopsis [Sorts the nodes.] + + Description [Sorts the nodes appearing in the left-hand sides of the + implications by the number of 1s in their simulation info.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abc_NtkVanImpSortByOnes( Van_Man_t * p ) +{ + Abc_Obj_t * pNode, * pList; + Vec_Ptr_t * vSorted; + unsigned Imp; + int i, nOnes; + + // start the sorted array + vSorted = Vec_PtrStart( p->nWords * 32 ); + // go through the implications + Abc_NtkIncrementTravId( p->pNtkSingle ); + Vec_IntForEachEntry( p->vImps, Imp, i ) + { + pNode = Abc_NodeVanGetLeft( p->pNtkSingle, Imp ); + assert( !Abc_ObjIsPo(pNode) ); + // if this node is already visited, skip + if ( Abc_NodeIsTravIdCurrent( pNode ) ) + continue; + // mark the node as visited + Abc_NodeSetTravIdCurrent( pNode ); + + // add the node to the list + nOnes = Vec_IntEntry( p->vCounters, pNode->Id ); + pList = Vec_PtrEntry( vSorted, nOnes ); + pNode->pNext = pList; + Vec_PtrWriteEntry( vSorted, nOnes, pNode ); + } + return vSorted; +} + +/**Function************************************************************* + + Synopsis [Computes the array of beginnings.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Abc_NtkVanImpComputeBegs( Van_Man_t * p ) +{ + Vec_Int_t * vBegins; + unsigned Imp; + int i, ItemLast, ItemCur; + + // sort the implications (by the number of the left-hand-side node) + Vec_IntSort( p->vImps, 0 ); + + // start the array of beginnings + vBegins = Vec_IntStart( p->nIdMax + 1 ); + + // mark the begining of each node's implications + ItemLast = 0; + Vec_IntForEachEntry( p->vImps, Imp, i ) + { + ItemCur = (Imp >> 16); + if ( ItemCur == ItemLast ) + continue; + Vec_IntWriteEntry( vBegins, ItemCur, i ); + ItemLast = ItemCur; + } + // fill in the empty spaces + ItemLast = Vec_IntSize(p->vImps); + Vec_IntWriteEntry( vBegins, p->nIdMax, ItemLast ); + Vec_IntForEachEntryReverse( vBegins, ItemCur, i ) + { + if ( ItemCur == 0 ) + Vec_IntWriteEntry( vBegins, i, ItemLast ); + else + ItemLast = ItemCur; + } + + Imp = Vec_IntEntry( p->vImps, 0 ); + ItemCur = (Imp >> 16); + for ( i = 0; i <= ItemCur; i++ ) + Vec_IntWriteEntry( vBegins, i, 0 ); + return vBegins; +} + +/**Function************************************************************* + + Synopsis [Derives the minimum subset of implications.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkVanImpMark_rec( Abc_Obj_t * pNode, Vec_Vec_t * vImpsMis ) +{ + Vec_Int_t * vNexts; + int i, Next; + // if this node is already visited, skip + if ( Abc_NodeIsTravIdCurrent( pNode ) ) + return; + // mark the node as visited + Abc_NodeSetTravIdCurrent( pNode ); + // mark the children + vNexts = Vec_VecEntry( vImpsMis, pNode->Id ); + Vec_IntForEachEntry( vNexts, Next, i ) + Abc_NtkVanImpMark_rec( Abc_NtkObj(pNode->pNtk, Next), vImpsMis ); +} + +/**Function************************************************************* + + Synopsis [Derives the minimum subset of implications.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Abc_NtkVanImpComputeMis( Van_Man_t * p ) +{ + Abc_Obj_t * pNode, * pNext, * pList; + Vec_Vec_t * vMatrix; + Vec_Ptr_t * vSorted; + Vec_Int_t * vBegins; + Vec_Int_t * vImpsMis; + int i, k, iStart, iStop; + void * pEntry; + unsigned Imp; + + if ( Vec_IntSize(p->vImps) == 0 ) + return Vec_IntAlloc(0); + + // compute the sorted list of nodes by the number of 1s + Abc_NtkCleanNext( p->pNtkSingle ); + vSorted = Abc_NtkVanImpSortByOnes( p ); + + // compute the array of beginnings + vBegins = Abc_NtkVanImpComputeBegs( p ); + +/* +Vec_IntForEachEntry( p->vImps, Imp, i ) +{ + printf( "%d: ", i ); + Abc_NodeVanPrintImp( Imp ); +} +printf( "\n\n" ); +Vec_IntForEachEntry( vBegins, Imp, i ) + printf( "%d=%d ", i, Imp ); +printf( "\n\n" ); +*/ + + // compute the MIS by considering nodes in the reverse order of ones + vMatrix = Vec_VecStart( p->nIdMax ); + Vec_PtrForEachEntryReverse( vSorted, pList, i ) + { + for ( pNode = pList; pNode; pNode = pNode->pNext ) + { + // get the starting and stopping implication of this node + iStart = Vec_IntEntry( vBegins, pNode->Id ); + iStop = Vec_IntEntry( vBegins, pNode->Id + 1 ); + if ( iStart == iStop ) + continue; + assert( iStart < iStop ); + // go through all the implications of this node + Abc_NtkIncrementTravId( p->pNtkSingle ); + Abc_NodeIsTravIdCurrent( pNode ); + Vec_IntForEachEntryStartStop( p->vImps, Imp, k, iStart, iStop ) + { + assert( pNode == Abc_NodeVanGetLeft(p->pNtkSingle, Imp) ); + pNext = Abc_NodeVanGetRight(p->pNtkSingle, Imp); + // if this node is already visited, skip + if ( Abc_NodeIsTravIdCurrent( pNext ) ) + continue; + assert( pNode->Id != pNext->Id ); + // add implication + Vec_VecPush( vMatrix, pNode->Id, (void *)pNext->Id ); + // recursively mark dependent nodes + Abc_NtkVanImpMark_rec( pNext, vMatrix ); + } + } + } + Vec_IntFree( vBegins ); + Vec_PtrFree( vSorted ); + + // transfer the MIS into the normal array + vImpsMis = Vec_IntAlloc( 100 ); + Vec_VecForEachEntry( vMatrix, pEntry, i, k ) + { + assert( (i << 16) != ((int)pEntry) ); + Vec_IntPush( vImpsMis, (i << 16) | ((int)pEntry) ); + } + Vec_VecFree( vMatrix ); + return vImpsMis; +} + + +/**Function************************************************************* + + Synopsis [Count equal pairs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkVanImpCountEqual( Van_Man_t * p ) +{ + Abc_Obj_t * pNode1, * pNode2, * pNode3; + Vec_Int_t * vBegins; + int iStart, iStop; + unsigned Imp, ImpR; + int i, k, Counter; + + // compute the array of beginnings + vBegins = Abc_NtkVanImpComputeBegs( p ); + + // go through each node and out + Counter = 0; + Vec_IntForEachEntry( p->vImps, Imp, i ) + { + pNode1 = Abc_NodeVanGetLeft( p->pNtkSingle, Imp ); + pNode2 = Abc_NodeVanGetRight( p->pNtkSingle, Imp ); + if ( pNode1->Id > pNode2->Id ) + continue; + iStart = Vec_IntEntry( vBegins, pNode2->Id ); + iStop = Vec_IntEntry( vBegins, pNode2->Id + 1 ); + Vec_IntForEachEntryStartStop( p->vImps, ImpR, k, iStart, iStop ) + { + assert( pNode2 == Abc_NodeVanGetLeft(p->pNtkSingle, ImpR) ); + pNode3 = Abc_NodeVanGetRight(p->pNtkSingle, ImpR); + if ( pNode1 == pNode3 ) + { + Counter++; + break; + } + } + } + Vec_IntFree( vBegins ); + return Counter; +} + + +/**Function************************************************************* + + Synopsis [Create EXDC from the equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkVanImpDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vZeros, Vec_Int_t * vImps ) +{ + Abc_Ntk_t * pNtkNew; + Vec_Ptr_t * vCone; + Abc_Obj_t * pObj, * pMiter, * pTotal, * pNode, * pNode1, * pNode2; + unsigned Imp; + int i, k; + + assert( Abc_NtkIsStrash(pNtk) ); + + // start the network + pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc ); + pNtkNew->pName = util_strsav( "exdc" ); + pNtkNew->pSpec = NULL; + + // map the constant nodes + Abc_AigConst1(pNtk->pManFunc)->pCopy = Abc_AigConst1(pNtkNew->pManFunc); + // for each CI, create PI + Abc_NtkForEachCi( pNtk, pObj, i ) + Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pObj) ); + // cannot add latches here because pLatch->pCopy pointers are used + + // build logic cone for zero nodes + pTotal = Abc_ObjNot( Abc_AigConst1(pNtkNew->pManFunc) ); + Vec_PtrForEachEntry( vZeros, pNode, i ) + { + // build the logic cone for the node + if ( Abc_ObjFaninNum(pNode) == 2 ) + { + vCone = Abc_NtkDfsNodes( pNtk, &pNode, 1 ); + Vec_PtrForEachEntry( vCone, pObj, k ) + pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); + Vec_PtrFree( vCone ); + assert( pObj == pNode ); + } + // complement if there is phase difference + pNode->pCopy = Abc_ObjNotCond( pNode->pCopy, pNode->fPhase ); + + // add it to the EXDC + pTotal = Abc_AigOr( pNtkNew->pManFunc, pTotal, pNode->pCopy ); + } + + // create logic cones for the implications + Vec_IntForEachEntry( vImps, Imp, i ) + { + pNode1 = Abc_NtkObj(pNtk, Imp >> 16); + pNode2 = Abc_NtkObj(pNtk, Imp & 0xFFFF); + + // build the logic cone for the first node + if ( Abc_ObjFaninNum(pNode1) == 2 ) + { + vCone = Abc_NtkDfsNodes( pNtk, &pNode1, 1 ); + Vec_PtrForEachEntry( vCone, pObj, k ) + pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); + Vec_PtrFree( vCone ); + assert( pObj == pNode1 ); + } + // complement if there is phase difference + pNode1->pCopy = Abc_ObjNotCond( pNode1->pCopy, pNode1->fPhase ); + + // build the logic cone for the second node + if ( Abc_ObjFaninNum(pNode2) == 2 ) + { + vCone = Abc_NtkDfsNodes( pNtk, &pNode2, 1 ); + Vec_PtrForEachEntry( vCone, pObj, k ) + pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); + Vec_PtrFree( vCone ); + assert( pObj == pNode2 ); + } + // complement if there is phase difference + pNode2->pCopy = Abc_ObjNotCond( pNode2->pCopy, pNode2->fPhase ); + + // build the implication and add it to the EXDC + pMiter = Abc_AigAnd( pNtkNew->pManFunc, pNode1->pCopy, Abc_ObjNot(pNode2->pCopy) ); + pTotal = Abc_AigOr( pNtkNew->pManFunc, pTotal, pMiter ); + } + + // for each CO, create PO (skip POs equal to CIs because of name conflict) + Abc_NtkForEachPo( pNtk, pObj, i ) + if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) ) + Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName(pObj) ); + Abc_NtkForEachLatch( pNtk, pObj, i ) + Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjNameSuffix(pObj, "_in") ); + + // link to the POs of the network + Abc_NtkForEachPo( pNtk, pObj, i ) + if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) ) + Abc_ObjAddFanin( pObj->pCopy, pTotal ); + Abc_NtkForEachLatch( pNtk, pObj, i ) + Abc_ObjAddFanin( pObj->pCopy, pTotal ); + + // remove the extra nodes + Abc_AigCleanup( pNtkNew->pManFunc ); + + // check the result + if ( !Abc_NtkCheck( pNtkNew ) ) + { + printf( "Abc_NtkVanImpDeriveExdc: The network check has failed.\n" ); + Abc_NtkDelete( pNtkNew ); + return NULL; + } + return pNtkNew; +} + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index 08a54e80..4e73d42b 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -20,14 +20,16 @@ #include "abc.h" #include "fraig.h" +#include "sim.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk ); +static int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk, int nFrames ); static int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel ); static void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel ); +static void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// @@ -62,7 +64,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds ) { printf( "Networks are NOT EQUIVALENT after structural hashing.\n" ); // report the error - pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter ); + pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 ); Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel ); FREE( pMiter->pModel ); Abc_NtkDelete( pMiter ); @@ -129,7 +131,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV { printf( "Networks are NOT EQUIVALENT after structural hashing.\n" ); // report the error - pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter ); + pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 ); Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel ); FREE( pMiter->pModel ); Abc_NtkDelete( pMiter ); @@ -278,8 +280,12 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF RetValue = Abc_NtkMiterIsConstant( pMiter ); if ( RetValue == 0 ) { - Abc_NtkDelete( pMiter ); printf( "Networks are NOT EQUIVALENT after structural hashing.\n" ); + // report the error + pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, nFrames ); + Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames ); + FREE( pMiter->pModel ); + Abc_NtkDelete( pMiter ); return; } if ( RetValue == 1 ) @@ -300,8 +306,12 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF RetValue = Abc_NtkMiterIsConstant( pFrames ); if ( RetValue == 0 ) { - Abc_NtkDelete( pFrames ); printf( "Networks are NOT EQUIVALENT after framing.\n" ); + // report the error + pFrames->pModel = Abc_NtkVerifyGetCleanModel( pFrames, 1 ); + Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pFrames->pModel, nFrames ); + FREE( pFrames->pModel ); + Abc_NtkDelete( pFrames ); return; } if ( RetValue == 1 ) @@ -328,7 +338,7 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF else if ( RetValue == 0 ) { printf( "Networks are NOT EQUIVALENT after fraiging.\n" ); -// Abc_NtkVerifyReportError( pNtk1, pNtk2, Fraig_ManReadModel(pMan) ); + Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, Fraig_ManReadModel(pMan), nFrames ); } else assert( 0 ); // delete the fraig manager @@ -337,6 +347,75 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF Abc_NtkDelete( pFrames ); } +/**Function************************************************************* + + Synopsis [Returns a dummy pattern full of zeros.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk, int nFrames ) +{ + int * pModel = ALLOC( int, Abc_NtkCiNum(pNtk) * nFrames ); + memset( pModel, 0, sizeof(int) * Abc_NtkCiNum(pNtk) * nFrames ); + return pModel; +} + +/**Function************************************************************* + + Synopsis [Returns the PO values under the given input pattern.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel ) +{ + Vec_Ptr_t * vNodes; + Abc_Obj_t * pNode; + int * pValues, Value0, Value1, i; + int fStrashed = 0; + if ( !Abc_NtkIsStrash(pNtk) ) + { + pNtk = Abc_NtkStrash(pNtk, 0, 0); + fStrashed = 1; + } + // increment the trav ID + Abc_NtkIncrementTravId( pNtk ); + // set the CI values + Abc_NtkForEachCi( pNtk, pNode, i ) + pNode->pCopy = (void *)pModel[i]; + // simulate in the topological order + vNodes = Abc_NtkDfs( pNtk, 1 ); + Vec_PtrForEachEntry( vNodes, pNode, i ) + { + if ( Abc_NodeIsConst(pNode) ) + pNode->pCopy = NULL; + else + { + Value0 = ((int)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode); + Value1 = ((int)Abc_ObjFanin1(pNode)->pCopy) ^ Abc_ObjFaninC1(pNode); + pNode->pCopy = (void *)(Value0 & Value1); + } + } + Vec_PtrFree( vNodes ); + // fill the output values + pValues = ALLOC( int, Abc_NtkCoNum(pNtk) ); + Abc_NtkForEachCo( pNtk, pNode, i ) + pValues[i] = ((int)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode); + if ( fStrashed ) + Abc_NtkDelete( pNtk ); + return pValues; +} + + /**Function************************************************************* Synopsis [Reports mismatch between the two networks.] @@ -353,7 +432,7 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode Vec_Ptr_t * vNodes; Abc_Obj_t * pNode; int * pValues1, * pValues2; - int nMisses, nPrinted, i, iNode = -1; + int nErrors, nPrinted, i, iNode = -1; assert( Abc_NtkCiNum(pNtk1) == Abc_NtkCiNum(pNtk2) ); assert( Abc_NtkCoNum(pNtk1) == Abc_NtkCoNum(pNtk2) ); @@ -361,10 +440,10 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode pValues1 = Abc_NtkVerifySimulatePattern( pNtk1, pModel ); pValues2 = Abc_NtkVerifySimulatePattern( pNtk2, pModel ); // count the mismatches - nMisses = 0; + nErrors = 0; for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ ) - nMisses += (int)( pValues1[i] != pValues2[i] ); - printf( "Verification failed for %d outputs: ", nMisses ); + nErrors += (int)( pValues1[i] != pValues2[i] ); + printf( "Verification failed for %d outputs: ", nErrors ); // print the first 3 outputs nPrinted = 0; for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ ) @@ -376,7 +455,7 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode if ( ++nPrinted == 3 ) break; } - if ( nPrinted != nMisses ) + if ( nPrinted != nErrors ) printf( " ..." ); printf( "\n" ); // report mismatch for the first output @@ -404,9 +483,10 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode free( pValues2 ); } + /**Function************************************************************* - Synopsis [Returns a dummy pattern full of zeros.] + Synopsis [Computes the COs in the support of the PO in the given frame.] Description [] @@ -415,16 +495,43 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode SeeAlso [] ***********************************************************************/ -int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk ) +void Abc_NtkGetSeqPoSupp( Abc_Ntk_t * pNtk, int iFrame, int iNumPo ) { - int * pModel = ALLOC( int, Abc_NtkCiNum(pNtk) ); - memset( pModel, 0, sizeof(int) * Abc_NtkCiNum(pNtk) ); - return pModel; + Abc_Ntk_t * pFrames; + Abc_Obj_t * pObj, * pNodePo; + Vec_Ptr_t * vSupp; + int i, k; + // get the timeframes of the network + pFrames = Abc_NtkFrames( pNtk, iFrame + 1, 0 ); +//Abc_NtkShowAig( pFrames ); + + // get the PO of the timeframes + pNodePo = Abc_NtkPo( pFrames, iFrame * Abc_NtkPoNum(pNtk) + iNumPo ); + // set the support + vSupp = Abc_NtkNodeSupport( pFrames, &pNodePo, 1 ); + // mark the support of the frames + Abc_NtkForEachCi( pFrames, pObj, i ) + pObj->pCopy = NULL; + Vec_PtrForEachEntry( vSupp, pObj, i ) + pObj->pCopy = (void *)1; + // mark the support of the network if the support of the timeframes is marked + Abc_NtkForEachCi( pNtk, pObj, i ) + pObj->pCopy = NULL; + Abc_NtkForEachLatch( pNtk, pObj, i ) + if ( Abc_NtkLatch(pFrames, i)->pCopy ) + pObj->pCopy = (void *)1; + Abc_NtkForEachPi( pNtk, pObj, i ) + for ( k = 0; k <= iFrame; k++ ) + if ( Abc_NtkPi(pFrames, k*Abc_NtkPiNum(pNtk) + i)->pCopy ) + pObj->pCopy = (void *)1; + // free stuff + Vec_PtrFree( vSupp ); + Abc_NtkDelete( pFrames ); } /**Function************************************************************* - Synopsis [Returns the PO values under the given input pattern.] + Synopsis [Reports mismatch between the two sequential networks.] Description [] @@ -433,45 +540,157 @@ int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel ) +void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames ) { - Vec_Ptr_t * vNodes; - Abc_Obj_t * pNode; - int * pValues, Value0, Value1, i; - int fStrashed = 0; - if ( !Abc_NtkIsStrash(pNtk) ) + Vec_Ptr_t * vInfo1, * vInfo2; + Abc_Obj_t * pObj, * pObjError, * pObj1, * pObj2; + int ValueError1, ValueError2; + unsigned * pPats1, * pPats2; + int i, o, k, nErrors, iFrameError, iNodePo, nPrinted; + int fRemove1 = 0, fRemove2 = 0; + + if ( !Abc_NtkIsStrash(pNtk1) ) + fRemove1 = 1, pNtk1 = Abc_NtkStrash( pNtk1, 0, 0 ); + if ( !Abc_NtkIsStrash(pNtk2) ) + fRemove2 = 1, pNtk2 = Abc_NtkStrash( pNtk2, 0, 0 ); + + // simulate sequential circuits + vInfo1 = Sim_SimulateSeqModel( pNtk1, nFrames, pModel ); + vInfo2 = Sim_SimulateSeqModel( pNtk2, nFrames, pModel ); + + // look for a discrepancy in the PO values + nErrors = 0; + pObjError = NULL; + for ( i = 0; i < nFrames; i++ ) { - pNtk = Abc_NtkStrash(pNtk, 0, 0); - fStrashed = 1; - } - // increment the trav ID - Abc_NtkIncrementTravId( pNtk ); - // set the CI values - Abc_NtkForEachCi( pNtk, pNode, i ) - pNode->pCopy = (void *)pModel[i]; - // simulate in the topological order - vNodes = Abc_NtkDfs( pNtk, 1 ); - Vec_PtrForEachEntry( vNodes, pNode, i ) - { - if ( Abc_NodeIsConst(pNode) ) - pNode->pCopy = NULL; - else + if ( pObjError ) + break; + Abc_NtkForEachPo( pNtk1, pObj1, o ) { - Value0 = ((int)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode); - Value1 = ((int)Abc_ObjFanin1(pNode)->pCopy) ^ Abc_ObjFaninC1(pNode); - pNode->pCopy = (void *)(Value0 & Value1); + pObj2 = Abc_NtkPo( pNtk2, o ); + pPats1 = Sim_SimInfoGet(vInfo1, pObj1); + pPats2 = Sim_SimInfoGet(vInfo2, pObj2); + if ( pPats1[i] == pPats2[i] ) + continue; + nErrors++; + if ( pObjError == NULL ) + { + pObjError = pObj1; + iFrameError = i; + iNodePo = o; + ValueError1 = (pPats1[i] > 0); + ValueError2 = (pPats2[i] > 0); + } } } - Vec_PtrFree( vNodes ); - // fill the output values - pValues = ALLOC( int, Abc_NtkCoNum(pNtk) ); - Abc_NtkForEachCo( pNtk, pNode, i ) - pValues[i] = ((int)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode); - if ( fStrashed ) - Abc_NtkDelete( pNtk ); - return pValues; + + if ( pObjError == NULL ) + { + printf( "No output mismatches detected.\n" ); + Sim_UtilInfoFree( vInfo1 ); + Sim_UtilInfoFree( vInfo2 ); + if ( fRemove1 ) Abc_NtkDelete( pNtk1 ); + if ( fRemove2 ) Abc_NtkDelete( pNtk2 ); + return; + } + + printf( "Verification failed for %d output%s of frame %d: ", nErrors, (nErrors>1? "s":""), iFrameError+1 ); + // print the first 3 outputs + nPrinted = 0; + Abc_NtkForEachPo( pNtk1, pObj1, o ) + { + pObj2 = Abc_NtkPo( pNtk2, o ); + pPats1 = Sim_SimInfoGet(vInfo1, pObj1); + pPats2 = Sim_SimInfoGet(vInfo2, pObj2); + if ( pPats1[iFrameError] == pPats2[iFrameError] ) + continue; + printf( " %s", Abc_ObjName(pObj1) ); + if ( ++nPrinted == 3 ) + break; + } + if ( nPrinted != nErrors ) + printf( " ..." ); + printf( "\n" ); + + // mark CIs of the networks in the cone of influence of this output + Abc_NtkGetSeqPoSupp( pNtk1, iFrameError, iNodePo ); + Abc_NtkGetSeqPoSupp( pNtk2, iFrameError, iNodePo ); + + // report mismatch for the first output + printf( "Output %s: Value in Network1 = %d. Value in Network2 = %d.\n", + Abc_ObjName(pObjError), ValueError1, ValueError2 ); + + printf( "The cone of influence of output %s in Network1:\n", Abc_ObjName(pObjError) ); + printf( "PIs: " ); + Abc_NtkForEachPi( pNtk1, pObj, i ) + if ( pObj->pCopy ) + printf( "%s ", Abc_ObjName(pObj) ); + printf( "\n" ); + printf( "Latches: " ); + Abc_NtkForEachLatch( pNtk1, pObj, i ) + if ( pObj->pCopy ) + printf( "%s ", Abc_ObjName(pObj) ); + printf( "\n" ); + + printf( "The cone of influence of output %s in Network2:\n", Abc_ObjName(pObjError) ); + printf( "PIs: " ); + Abc_NtkForEachPi( pNtk2, pObj, i ) + if ( pObj->pCopy ) + printf( "%s ", Abc_ObjName(pObj) ); + printf( "\n" ); + printf( "Latches: " ); + Abc_NtkForEachLatch( pNtk2, pObj, i ) + if ( pObj->pCopy ) + printf( "%s ", Abc_ObjName(pObj) ); + printf( "\n" ); + + // print the patterns + for ( i = 0; i <= iFrameError; i++ ) + { + printf( "Frame %d: ", i+1 ); + + printf( "PI(1):" ); + Abc_NtkForEachPi( pNtk1, pObj, k ) + if ( pObj->pCopy ) + printf( "%d", Sim_SimInfoGet(vInfo1, pObj)[i] > 0 ); + printf( " " ); + printf( "L(1):" ); + Abc_NtkForEachLatch( pNtk1, pObj, k ) + if ( pObj->pCopy ) + printf( "%d", Sim_SimInfoGet(vInfo1, pObj)[i] > 0 ); + printf( " " ); + printf( "%s(1):", Abc_ObjName(pObjError) ); + printf( "%d", Sim_SimInfoGet(vInfo1, pObjError)[i] > 0 ); + + printf( " " ); + + printf( "PI(2):" ); + Abc_NtkForEachPi( pNtk2, pObj, k ) + if ( pObj->pCopy ) + printf( "%d", Sim_SimInfoGet(vInfo2, pObj)[i] > 0 ); + printf( " " ); + printf( "L(2):" ); + Abc_NtkForEachLatch( pNtk2, pObj, k ) + if ( pObj->pCopy ) + printf( "%d", Sim_SimInfoGet(vInfo2, pObj)[i] > 0 ); + printf( " " ); + printf( "%s(2):", Abc_ObjName(pObjError) ); + printf( "%d", Sim_SimInfoGet(vInfo2, pObjError)[i] > 0 ); + + printf( "\n" ); + } + Abc_NtkForEachCi( pNtk1, pObj, i ) + pObj->pCopy = NULL; + Abc_NtkForEachCi( pNtk2, pObj, i ) + pObj->pCopy = NULL; + + Sim_UtilInfoFree( vInfo1 ); + Sim_UtilInfoFree( vInfo2 ); + if ( fRemove1 ) Abc_NtkDelete( pNtk1 ); + if ( fRemove2 ) Abc_NtkDelete( pNtk2 ); } + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3