diff options
| -rw-r--r-- | abclib.dsp | 4 | ||||
| -rw-r--r-- | src/aig/gia/giaAbsVta.c | 516 | ||||
| -rw-r--r-- | src/aig/gia/module.make | 1 | ||||
| -rw-r--r-- | src/base/abc/abcHieCec.c | 99 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 14 |
5 files changed, 560 insertions, 74 deletions
@@ -4003,6 +4003,10 @@ SOURCE=.\src\aig\gia\giaAbs.c # End Source File # Begin Source File +SOURCE=.\src\aig\gia\giaAbsVta.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\gia\giaAig.c # End Source File # Begin Source File diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c new file mode 100644 index 00000000..c407510c --- /dev/null +++ b/src/aig/gia/giaAbsVta.c @@ -0,0 +1,516 @@ +/**CFile**************************************************************** + + FileName [giaAbsVta.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [Variable time-frame abstraction.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaAbsVta.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" +#include "satSolver2.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Vta_Man_t_ Vta_Man_t; // manager +struct Vta_Man_t_ +{ + // user data + Gia_Man_t * pGia; + int nFramesMax; // maximum number of frames + int nConfMax; + int nTimeMax; + int fVerbose; + // internal data + int nSatVars; // the number of SAT variables + int nObjUsed; // the number objects used + int Shift; // bit count for obj number + int Mask; // bit mask for obj number + Vec_Int_t * vOrder; // map Num to Id + Vec_Int_t * vId2Num; // map Id to Num + Vec_Int_t * vFraLims; // frame limits + Vec_Int_t * vOne2Sat; // map (Frame; Num) to Sat + Vec_Int_t * vCla2One; // map clause to (Frame; Num) + Vec_Int_t * vNumAbs; // abstraction for each timeframe + sat_solver2 * pSat; +}; + +static inline int Vta_FraNum2One( Vta_Man_t * p, int f, int n ) { return (f << p->Shift) | n; } +static inline int Vta_One2Fra( Vta_Man_t * p, int i ) { return i >> p->Shift; } +static inline int Vta_One2Num( Vta_Man_t * p, int i ) { return i & p->Mask; } + +static inline void Vta_SetSatVar( Vta_Man_t * p, int f, int n ) +{ + int One = Vta_FraNum2One( p, f, n ); + int * pPlace = Vec_IntEntryP( p->vOne2Sat, One ); + assert( *pPlace == 0 ); + *pPlace = p->nSatVars++; + // create additional var for ROs of frame 0 +} +static inline int Vta_GetSatVar( Vta_Man_t * p, int f, int n ) +{ + int One = Vta_FraNum2One( p, f, n ); + int * pPlace = Vec_IntEntryP( p->vOne2Sat, One ); + assert( *pPlace == 0 ); + return *pPlace; +} +static inline int Vta_GetSatVarObj( Vta_Man_t * p, int f, Gia_Obj_t * pObj ) +{ + return Vta_GetSatVar( p, f, Vec_IntEntry(p->vId2Num, Gia_ObjId(p->pGia, pObj)) ); +} + +extern Vec_Int_t * Gia_VtaCollect( Gia_Man_t * p, Vec_Int_t ** pvFraLims, Vec_Int_t ** pvRoots ); + +// check the first value of vOrder!!! + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline int sat_solver2_add_const( sat_solver2 * pSat, int iVar, int fCompl, int fMark ) +{ + lit Lits[1]; + int Cid; + assert( iVar >= 0 ); + + Lits[0] = toLitCond( iVar, fCompl ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 1 ); + if ( fMark ) + clause_set_partA( pSat, Cid, 1 ); + return 1; +} +static inline int sat_solver2_add_buffer( sat_solver2 * pSat, int iVarA, int iVarB, int fCompl, int fMark ) +{ + lit Lits[2]; + int Cid; + assert( iVarA >= 0 && iVarB >= 0 ); + + Lits[0] = toLitCond( iVarA, 0 ); + Lits[1] = toLitCond( iVarB, !fCompl ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 ); + if ( fMark ) + clause_set_partA( pSat, Cid, 1 ); + + Lits[0] = toLitCond( iVarA, 1 ); + Lits[1] = toLitCond( iVarB, fCompl ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 ); + if ( fMark ) + clause_set_partA( pSat, Cid, 1 ); + return 2; +} +static inline int sat_solver2_add_and( sat_solver2 * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fMark ) +{ + lit Lits[3]; + int Cid; + + Lits[0] = toLitCond( iVar, 1 ); + Lits[1] = toLitCond( iVar0, fCompl0 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 ); + if ( fMark ) + clause_set_partA( pSat, Cid, 1 ); + + Lits[0] = toLitCond( iVar, 1 ); + Lits[1] = toLitCond( iVar1, fCompl1 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 ); + if ( fMark ) + clause_set_partA( pSat, Cid, 1 ); + + Lits[0] = toLitCond( iVar, 0 ); + Lits[1] = toLitCond( iVar0, !fCompl0 ); + Lits[2] = toLitCond( iVar1, !fCompl1 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 ); + if ( fMark ) + clause_set_partA( pSat, Cid, 1 ); + return 3; +} +static inline int sat_solver2_add_xor( sat_solver2 * pSat, int iVarA, int iVarB, int iVarC, int fCompl, int fMark ) +{ + lit Lits[3]; + int Cid; + assert( iVarA >= 0 && iVarB >= 0 && iVarC >= 0 ); + + Lits[0] = toLitCond( iVarA, !fCompl ); + Lits[1] = toLitCond( iVarB, 1 ); + Lits[2] = toLitCond( iVarC, 1 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 ); + if ( fMark ) + clause_set_partA( pSat, Cid, 1 ); + + Lits[0] = toLitCond( iVarA, !fCompl ); + Lits[1] = toLitCond( iVarB, 0 ); + Lits[2] = toLitCond( iVarC, 0 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 ); + if ( fMark ) + clause_set_partA( pSat, Cid, 1 ); + + Lits[0] = toLitCond( iVarA, fCompl ); + Lits[1] = toLitCond( iVarB, 1 ); + Lits[2] = toLitCond( iVarC, 0 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 ); + if ( fMark ) + clause_set_partA( pSat, Cid, 1 ); + + Lits[0] = toLitCond( iVarA, fCompl ); + Lits[1] = toLitCond( iVarB, 0 ); + Lits[2] = toLitCond( iVarC, 1 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 ); + if ( fMark ) + clause_set_partA( pSat, Cid, 1 ); + return 4; +} +static inline int sat_solver2_add_constraint( sat_solver2 * pSat, int iVar, int fCompl, int fMark ) +{ + lit Lits[2]; + int Cid; + assert( iVar >= 0 ); + + Lits[0] = toLitCond( iVar, fCompl ); + Lits[1] = toLitCond( iVar+1, 0 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 ); + if ( fMark ) + clause_set_partA( pSat, Cid, 1 ); + + Lits[0] = toLitCond( iVar, fCompl ); + Lits[1] = toLitCond( iVar+1, 1 ); + Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 ); + if ( fMark ) + clause_set_partA( pSat, Cid, 1 ); + return 2; +} + + + +/**Function************************************************************* + + Synopsis [Adds one time-frame to the solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Vga_ManGrow( Vta_Man_t * p, int fThis ) +{ + static int PrevF = -1; + Gia_Obj_t * pObj, * pObj2; + int Beg, End, One, i, c, f, iOutVar, nClauses; + assert( ++PrevF == f ); + assert( fThis >= 0 && fThis < p->nFramesMax ); + + // create variable for the output + iOutVar = p->nSatVars++; + + // add variables for this frame + for ( f = fThis; f >= 0; f-- ) + { + Beg = Vec_IntEntry( p->vFraLims, fThis-f ); + End = Vec_IntEntry( p->vFraLims, fThis-f+1 ); + for ( i = End-1; i >= Beg; i-- ) + Vta_SetSatVar( p, f, i ); + } + + // create clauses for the output + pObj = Gia_ManPo( p->pGia, 0 ); + nClauses = sat_solver2_add_buffer( p->pSat, + iOutVar, + Vta_GetSatVarObj( p, f, Gia_ObjFanin0(pObj) ), + Gia_ObjFaninC0(pObj), 0 ); + + // add clauses for this frame + for ( f = fThis; f >= 0; f-- ) + { + Beg = Vec_IntEntry( p->vFraLims, fThis-f ); + End = Vec_IntEntry( p->vFraLims, fThis-f+1 ); + for ( i = End-1; i >= Beg; i-- ) + { + nClauses = 0; + pObj = Gia_ManObj( p->pGia, Vec_IntEntry(p->vOrder, i) ); + if ( Gia_ObjIsAnd(pObj) ) + nClauses = sat_solver2_add_and( p->pSat, + Vta_GetSatVarObj( p, f, pObj ), + Vta_GetSatVarObj( p, f, Gia_ObjFanin0(pObj) ), + Vta_GetSatVarObj( p, f, Gia_ObjFanin1(pObj) ), + Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); + else if ( Gia_ObjIsRo(p->pGia, pObj) ) + { + if ( f == 0 ) + { + nClauses = sat_solver2_add_constraint( p->pSat, + Vta_GetSatVarObj( p, f, pObj ), + 1, 0 ); + } + else + { + pObj2 = Gia_ObjRoToRi(p->pGia, pObj); + nClauses = sat_solver2_add_buffer( p->pSat, + Vta_GetSatVarObj( p, f, pObj ), + Vta_GetSatVarObj( p, f-1, Gia_ObjFanin0(pObj2) ), + Gia_ObjFaninC0(pObj2), 0 ); + } + } + else if ( Gia_ObjIsConst0(pObj) ) + { + nClauses = sat_solver2_add_const( p->pSat, + Vta_GetSatVarObj( p, f, pObj ), + 1, 0 ); + } + One = Vta_FraNum2One( p, f, i ); + for ( c = 0; c < nClauses; c++ ) + Vec_IntPush( p->vCla2One, One ); + } + } +} + +/**Function************************************************************* + + Synopsis [Create manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, int nFramesMax, int nConfMax, int nTimeMax, int fVerbose ) +{ + Vta_Man_t * p; + assert( nFramesMax > 0 && nFramesMax < 32 ); + p = ABC_CALLOC( Vta_Man_t, 1 ); + p->pGia = pGia; + p->nFramesMax = nFramesMax; + p->nConfMax = nConfMax; + p->nTimeMax = nTimeMax; + p->fVerbose = fVerbose; + // internal data + p->vOrder = Gia_VtaCollect( pGia, &p->vFraLims, NULL ); + Vec_IntWriteEntry( p->vOrder, 0, 0 ); + p->vId2Num = Vec_IntInvert( p->vOrder, 0 ); + Vec_IntWriteEntry( p->vOrder, 0, -1 ); + Vec_IntWriteEntry( p->vId2Num, 0, -1 ); + // internal data + p->nObjUsed = Vec_IntEntry( p->vFraLims, nFramesMax ); + p->Shift = Gia_Base2Log( p->nObjUsed ); + p->Mask = (1 << p->Shift) - 1; + // internal data + p->vOne2Sat = Vec_IntStart( (1 << p->Shift) * nFramesMax ); + p->vCla2One = Vec_IntAlloc( 100000 ); Vec_IntPush( p->vCla2One, -1 ); + p->vNumAbs = Vec_IntAlloc( p->nObjUsed ); + p->pSat = sat_solver2_new(); + sat_solver2_setnvars( p->pSat, 10000 ); + p->nSatVars = 1; + return p; +} + +/**Function************************************************************* + + Synopsis [Delete manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Vga_ManStop( Vta_Man_t * p ) +{ + Vec_IntFreeP( &p->vOrder ); + Vec_IntFreeP( &p->vId2Num ); + Vec_IntFreeP( &p->vFraLims ); + Vec_IntFreeP( &p->vOne2Sat ); + Vec_IntFreeP( &p->vCla2One ); + sat_solver2_delete( p->pSat ); + ABC_FREE( p ); +} + + + +/**Function************************************************************* + + Synopsis [Duplicate AIG with the given ordering of nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_VtaDup( Gia_Man_t * p, Vec_Int_t * vOrder ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i, nFlops = 0; + Gia_ManFillValue( p ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Gia_UtilStrsav( p->pName ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachPi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + Gia_ManForEachObjVec( vOrder, p, pObj, i ) + if ( i && Gia_ObjIsRo(p, pObj) ) + pObj->Value = Gia_ManAppendCi(pNew), nFlops++; + Gia_ManForEachObjVec( vOrder, p, pObj, i ) + if ( i && Gia_ObjIsAnd(pObj) ) + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachPo( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManForEachObjVec( vOrder, p, pObj, i ) + if ( i && Gia_ObjIsRo(p, pObj) && (pObj = Gia_ObjRoToRi(p, pObj)) ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManSetRegNum( pNew, nFlops ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Collect nodes/flops involved in different timeframes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_VtaCollect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vOrder, Vec_Int_t * vRoots ) +{ + if ( pObj->fMark0 ) + return; + pObj->fMark0 = 1; + if ( Gia_ObjIsConst0(pObj) ) + return; + if ( Gia_ObjIsAnd(pObj) ) + { + Gia_VtaCollect_rec( p, Gia_ObjFanin0(pObj), vOrder, vRoots ); + Gia_VtaCollect_rec( p, Gia_ObjFanin1(pObj), vOrder, vRoots ); + } + else if ( Gia_ObjIsRo(p, pObj) ) + Vec_IntPush( vRoots, Gia_ObjId(p, Gia_ObjRoToRi(p, pObj)) ); + Vec_IntPush( vOrder, Gia_ObjId(p, pObj) ); +} + +/**Function************************************************************* + + Synopsis [Collect nodes/flops involved in different timeframes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_VtaCollect( Gia_Man_t * p, Vec_Int_t ** pvFraLims, Vec_Int_t ** pvRoots ) +{ + Vec_Int_t * vOrder; // resulting ordering of PI/RO/And + Vec_Int_t * vFraLims; // frame limits + Vec_Int_t * vRoots; // CO roots + Gia_Obj_t * pObj; + int i, StopPoint; + + Gia_ManCheckMark0( p ); + + // create roots + vRoots = Vec_IntAlloc( 1000 ); + Gia_ManForEachPo( p, pObj, i ) + Vec_IntPush( vRoots, Gia_ObjId(p, pObj) ); + + // collects nodes/flops + vFraLims = Vec_IntAlloc( 1000 ); + vOrder = Vec_IntAlloc( Gia_ManObjNum(p) ); + Vec_IntPush( vOrder, -1 ); + StopPoint = Vec_IntSize(vRoots); + Gia_ManForEachObjVec( vRoots, p, pObj, i ) + { + if ( i == StopPoint ) + { + Vec_IntPush( vFraLims, Vec_IntSize(vOrder) ); + StopPoint = Vec_IntSize(vRoots); + } + Gia_VtaCollect_rec( p, Gia_ObjFanin0(pObj), vOrder, vRoots ); + } + assert( i == StopPoint ); + Vec_IntPush( vFraLims, Vec_IntSize(vOrder) ); + +/* + // add unmarked PIs + Gia_ManForEachPi( p, pObj, i ) + if ( !pObj->fMark0 ) + Vec_IntPush( vOrder, Gia_ObjId(p, pObj) ); +*/ + + // clean/return + Gia_ManCleanMark0( p ); + if ( pvFraLims ) + *pvFraLims = vFraLims; + else + Vec_IntFree( vFraLims ); + if ( pvRoots ) + *pvRoots = vRoots; + else + Vec_IntFree( vRoots ); + return vOrder; +} + +/**Function************************************************************* + + Synopsis [Collect nodes/flops involved in different timeframes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_VtaTest( Gia_Man_t * p ) +{ + Vec_Int_t * vOrder, * vFraLims, * vRoots; + Gia_Man_t * pCopy; + // the new AIG orders flops and PIs in the "natural" order + vOrder = Gia_VtaCollect( p, &vFraLims, &vRoots ); + + // print results +// Gia_ManPrintStats( p, 0 ); + printf( "Obj =%8d. Unused =%8d. Frames =%6d.\n", + Gia_ManObjNum(p), + Gia_ManObjNum(p) - Gia_ManCoNum(p) - Vec_IntSize(vOrder), + Vec_IntSize(vFraLims) - 1 ); + + pCopy = Gia_VtaDup( p, vOrder ); +// Gia_ManStopP( &pCopy ); + + // cleanup + Vec_IntFree( vOrder ); + Vec_IntFree( vFraLims ); + Vec_IntFree( vRoots ); + return pCopy; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index fd0e0a5e..85356fd7 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -1,5 +1,6 @@ SRC += src/aig/gia/gia.c \ src/aig/gia/giaAbs.c \ + src/aig/gia/giaAbsVta.c \ src/aig/gia/giaAig.c \ src/aig/gia/giaAiger.c \ src/aig/gia/giaBidec.c \ diff --git a/src/base/abc/abcHieCec.c b/src/base/abc/abcHieCec.c index 4e49aea2..ee2500ce 100644 --- a/src/base/abc/abcHieCec.c +++ b/src/base/abc/abcHieCec.c @@ -553,40 +553,6 @@ void Abc_NtkCountInst( Abc_Ntk_t * pNtk ) /**Function************************************************************* - Synopsis [Count the number of instances and I/O pins in the hierarchy.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkCountInstances_rec( Abc_Ntk_t * pNtk, int * pCountInst, int * pCountPins ) -{ - Vec_Ptr_t * vOrder = (Vec_Ptr_t *)pNtk->pData; - Abc_Obj_t * pObj; - int i; - *pCountInst += 1; - *pCountPins += Abc_NtkPiNum(pNtk) + Abc_NtkPoNum(pNtk); - Vec_PtrForEachEntry( Abc_Obj_t *, vOrder, pObj, i ) - if ( Abc_ObjIsBox(pObj) ) - Abc_NtkCountInstances_rec( (Abc_Ntk_t *)pObj->pData, pCountInst, pCountPins ); -} - -void Abc_NtkCountInstances( Abc_Ntk_t * pNtk ) -{ - int CountInst = 0, CountPins = 0; - assert( Abc_NtkIsNetlist(pNtk) ); - assert( !Abc_NtkLatchNum(pNtk) ); - // recursively flatten hierarchy - Abc_NtkCountInstances_rec( pNtk, &CountInst, &CountPins ); - printf( "Instances = %10d. I/O pins = %10d.\n", CountInst, CountPins ); -} - - -/**Function************************************************************* - Synopsis [Performs hierarchical equivalence checking.] Description [] @@ -598,6 +564,7 @@ void Abc_NtkCountInstances( Abc_Ntk_t * pNtk ) ***********************************************************************/ Gia_Man_t * Abc_NtkHieCecTest( char * pFileName, int fVerbose ) { + int fUseNew = 0; int fCheck = 1; Vec_Ptr_t * vMods, * vOrder; Abc_Ntk_t * pNtk, * pModel; @@ -626,39 +593,39 @@ Gia_Man_t * Abc_NtkHieCecTest( char * pFileName, int fVerbose ) if ( fVerbose ) Abc_NtkPrintBoxInfo( pNtk ); - clk = clock(); - vOrder = Abc_NtkCollectHie( pNtk ); - Abc_PrintTime( 1, "Collect DFS ", clock() - clk ); - - // derive GIA - clk = clock(); - pGia = Abc_NtkDeriveFlatGia2( pNtk, vOrder ); - Abc_PrintTime( 1, "Deriving GIA", clock() - clk ); - Gia_ManPrintStats( pGia, 0 ); -// Gia_ManStop( pGia ); - - Vec_PtrFree( vOrder ); - -/* - // order nodes/boxes of all models - vMods = pNtk->pDesign->vModules; - Vec_PtrForEachEntry( Abc_Ntk_t *, vMods, pModel, i ) - pModel->pData = Abc_NtkDfsBoxes( pModel ); - - // derive GIA - clk = clock(); - pGia = Abc_NtkDeriveFlatGia( pNtk ); - Abc_PrintTime( 1, "Deriving GIA", clock() - clk ); - Gia_ManPrintStats( pGia, 0 ); - - clk = clock(); - Abc_NtkCountInstances( pNtk ); - Abc_PrintTime( 1, "Gather stats", clock() - clk ); + if ( fUseNew ) + { + clk = clock(); + vOrder = Abc_NtkCollectHie( pNtk ); + Abc_PrintTime( 1, "Collect DFS ", clock() - clk ); + + // derive GIA + clk = clock(); + pGia = Abc_NtkDeriveFlatGia2( pNtk, vOrder ); + Abc_PrintTime( 1, "Deriving GIA", clock() - clk ); + Gia_ManPrintStats( pGia, 0 ); + // Gia_ManStop( pGia ); + + Vec_PtrFree( vOrder ); + } + else + { + // order nodes/boxes of all models + vMods = pNtk->pDesign->vModules; + Vec_PtrForEachEntry( Abc_Ntk_t *, vMods, pModel, i ) + pModel->pData = Abc_NtkDfsBoxes( pModel ); + + // derive GIA + clk = clock(); + pGia = Abc_NtkDeriveFlatGia( pNtk ); + Abc_PrintTime( 1, "Deriving GIA", clock() - clk ); + Gia_ManPrintStats( pGia, 0 ); + + // clean nodes/boxes of all nodes + Vec_PtrForEachEntry( Abc_Ntk_t *, vMods, pModel, i ) + Vec_PtrFree( (Vec_Ptr_t *)pModel->pData ); + } - // clean nodes/boxes of all nodes - Vec_PtrForEachEntry( Abc_Ntk_t *, vMods, pModel, i ) - Vec_PtrFree( (Vec_Ptr_t *)pModel->pData ); -*/ clk = clock(); Abc_NtkCountInst( pNtk ); Abc_PrintTime( 1, "Gather stats", clock() - clk ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index b127eacd..22ff9411 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -30097,8 +30097,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) Gia_Man_t * pTemp = NULL; int c, fVerbose = 0; int fSwitch = 0; - extern void Gia_SatSolveTest( Gia_Man_t * p ); - extern void Cbs_ManSolveTest( Gia_Man_t * pGia ); + extern Gia_Man_t * Gia_VtaTest( Gia_Man_t * p ); Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF ) @@ -30129,13 +30128,12 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // Gia_SatSolveTest( pAbc->pGia ); // For_ManExperiment( pAbc->pGia, 20, 1, 1 ); // Gia_ManUnrollSpecial( pAbc->pGia, 5, 100, 1 ); - - if ( fSwitch ) - pAbc->pGia = Gia_ManDupSelf( pTemp = pAbc->pGia ); - else - pAbc->pGia = Gia_ManRemoveEnables( pTemp = pAbc->pGia ); - Gia_ManStop( pTemp ); +// pAbc->pGia = Gia_ManDupSelf( pTemp = pAbc->pGia ); +// pAbc->pGia = Gia_ManRemoveEnables( pTemp = pAbc->pGia ); // Cbs_ManSolveTest( pAbc->pGia ); + + pAbc->pGia = Gia_VtaTest( pTemp = pAbc->pGia ); + Gia_ManStopP( &pTemp ); return 0; usage: |