mirror of https://github.com/YosysHQ/abc.git
Improved algo for edge computation.
This commit is contained in:
Alan Mishchenko
parent
813b0e5851
commit
1b550cb87b
|
|
@ -4363,6 +4363,10 @@ SOURCE=.\src\aig\gia\giaRex.c
|
|||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\gia\giaSatEdge.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\gia\giaSatLut.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
|
|
|||
|
|
@ -1299,7 +1299,7 @@ extern void Gia_ManPrintLutStats( Gia_Man_t * p );
|
|||
extern int Gia_ManLutFaninCount( Gia_Man_t * p );
|
||||
extern int Gia_ManLutSizeMax( Gia_Man_t * p );
|
||||
extern int Gia_ManLutNum( Gia_Man_t * p );
|
||||
extern int Gia_ManLutLevel( Gia_Man_t * p );
|
||||
extern int Gia_ManLutLevel( Gia_Man_t * p, int ** ppLevels );
|
||||
extern void Gia_ManLutParams( Gia_Man_t * p, int * pnCurLuts, int * pnCurEdges, int * pnCurLevels );
|
||||
extern void Gia_ManSetRefsMapped( Gia_Man_t * p );
|
||||
extern void Gia_ManSetLutRefs( Gia_Man_t * p );
|
||||
|
|
|
|||
|
|
@ -71,7 +71,7 @@ static inline void Gia_ObjEdgeClean( int iObj, Vec_Int_t * vEdge1, Vec_Int_t * v
|
|||
***********************************************************************/
|
||||
void Gia_ManEdgeFromArray( Gia_Man_t * p, Vec_Int_t * vArray )
|
||||
{
|
||||
int i, iObj1, iObj2;
|
||||
int i, iObj1, iObj2, Count = 0;
|
||||
Vec_IntFreeP( &p->vEdge1 );
|
||||
Vec_IntFreeP( &p->vEdge2 );
|
||||
p->vEdge1 = Vec_IntStart( Gia_ManObjNum(p) );
|
||||
|
|
@ -79,9 +79,11 @@ void Gia_ManEdgeFromArray( Gia_Man_t * p, Vec_Int_t * vArray )
|
|||
Vec_IntForEachEntryDouble( vArray, iObj1, iObj2, i )
|
||||
{
|
||||
assert( iObj1 < iObj2 );
|
||||
Gia_ObjEdgeAdd( iObj1, iObj2, p->vEdge1, p->vEdge2 );
|
||||
Gia_ObjEdgeAdd( iObj2, iObj1, p->vEdge1, p->vEdge2 );
|
||||
Count += Gia_ObjEdgeAdd( iObj1, iObj2, p->vEdge1, p->vEdge2 );
|
||||
Count += Gia_ObjEdgeAdd( iObj2, iObj1, p->vEdge1, p->vEdge2 );
|
||||
}
|
||||
if ( Count )
|
||||
printf( "Found %d violations during edge conversion.\n", Count );
|
||||
}
|
||||
Vec_Int_t * Gia_ManEdgeToArray( Gia_Man_t * p )
|
||||
{
|
||||
|
|
|
|||
|
|
@ -160,7 +160,7 @@ int Gia_ManLutNum( Gia_Man_t * p )
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Gia_ManLutLevel( Gia_Man_t * p )
|
||||
int Gia_ManLutLevel( Gia_Man_t * p, int ** ppLevels )
|
||||
{
|
||||
Gia_Obj_t * pObj;
|
||||
int i, k, iFan, Level;
|
||||
|
|
@ -177,7 +177,10 @@ int Gia_ManLutLevel( Gia_Man_t * p )
|
|||
Gia_ManForEachCo( p, pObj, k )
|
||||
if ( Level < pLevels[Gia_ObjFaninId0p(p, pObj)] )
|
||||
Level = pLevels[Gia_ObjFaninId0p(p, pObj)];
|
||||
ABC_FREE( pLevels );
|
||||
if ( ppLevels )
|
||||
*ppLevels = pLevels;
|
||||
else
|
||||
ABC_FREE( pLevels );
|
||||
return Level;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -0,0 +1,417 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [giaSatEdge.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Scalable AIG package.]
|
||||
|
||||
Synopsis []
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: giaSatEdge.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "gia.h"
|
||||
#include "misc/tim/tim.h"
|
||||
#include "sat/bsat/satStore.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
typedef struct Seg_Man_t_ Seg_Man_t;
|
||||
struct Seg_Man_t_
|
||||
{
|
||||
sat_solver * pSat; // SAT solver
|
||||
Vec_Int_t * vCardVars; // candinality variables
|
||||
int nVars; // max vars (edge num)
|
||||
int LogN; // base-2 log of max vars
|
||||
int Power2; // power-2 of LogN
|
||||
int FirstVar; // first variable to be used
|
||||
// parameters
|
||||
int nBTLimit; // conflicts
|
||||
int DelayMax; // external delay
|
||||
int nEdges; // the number of edges
|
||||
int fDelay; // delay mode
|
||||
int fReverse; // reverse windowing
|
||||
int fVerbose; // verbose
|
||||
// window
|
||||
Gia_Man_t * pGia;
|
||||
Vec_Int_t * vEdges; // edges as fanin/fanout pairs
|
||||
Vec_Int_t * vFirsts; // first SAT variable
|
||||
Vec_Int_t * vNvars; // number of SAT variables
|
||||
Vec_Int_t * vLits; // literals
|
||||
int * pLevels; // levels
|
||||
|
||||
// statistics
|
||||
abctime timeStart;
|
||||
};
|
||||
|
||||
extern sat_solver * Sbm_AddCardinSolver( int LogN, Vec_Int_t ** pvVars );
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Count the number of edges between internal nodes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Int_t * Seg_ManCountIntEdges( Gia_Man_t * p )
|
||||
{
|
||||
int i, iLut, iFanin;
|
||||
Vec_Int_t * vEdges = Vec_IntAlloc( 1000 );
|
||||
assert( Gia_ManHasMapping(p) );
|
||||
Gia_ManForEachLut( p, iLut )
|
||||
Gia_LutForEachFanin( p, iLut, iFanin, i )
|
||||
if ( Gia_ObjIsAnd(Gia_ManObj(p, iFanin)) )
|
||||
{
|
||||
//printf( "Var %d: %d -> %d\n", Vec_IntSize(vEdges)/2, iFanin, iLut );
|
||||
|
||||
Vec_IntPushTwo( vEdges, iFanin, iLut );
|
||||
}
|
||||
return vEdges;
|
||||
}
|
||||
Vec_Wec_t * Seg_ManCollectObjEdges( Vec_Int_t * vEdges, int nObjs )
|
||||
{
|
||||
int iFanin, iObj, i;
|
||||
Vec_Wec_t * vRes = Vec_WecStart( nObjs );
|
||||
Vec_IntForEachEntryDouble( vEdges, iFanin, iObj, i )
|
||||
{
|
||||
Vec_WecPush( vRes, iFanin, i/2 );
|
||||
Vec_WecPush( vRes, iObj, i/2 );
|
||||
}
|
||||
return vRes;
|
||||
}
|
||||
int Seg_ManCountIntLevels( Seg_Man_t * p, int iStartVar )
|
||||
{
|
||||
int iLut, nVars;
|
||||
Vec_IntFill( p->vFirsts, Gia_ManObjNum(p->pGia), -1 );
|
||||
Vec_IntFill( p->vNvars, Gia_ManObjNum(p->pGia), 0 );
|
||||
ABC_FREE( p->pLevels );
|
||||
p->DelayMax = Gia_ManLutLevel( p->pGia, &p->pLevels );
|
||||
Gia_ManForEachLut( p->pGia, iLut )
|
||||
{
|
||||
Vec_IntWriteEntry( p->vFirsts, iLut, iStartVar );
|
||||
assert( p->pLevels[iLut] > 0 );
|
||||
nVars = p->pLevels[iLut] == 1 ? 0 : p->pLevels[iLut];
|
||||
Vec_IntWriteEntry( p->vNvars, iLut, nVars );
|
||||
iStartVar += nVars;
|
||||
}
|
||||
return iStartVar;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Seg_Man_t * Seg_ManAlloc( Gia_Man_t * pGia )
|
||||
{
|
||||
int nVarsAll;
|
||||
Seg_Man_t * p = ABC_CALLOC( Seg_Man_t, 1 );
|
||||
p->vEdges = Seg_ManCountIntEdges( pGia );
|
||||
p->nVars = Vec_IntSize(p->vEdges)/2;
|
||||
p->LogN = Abc_Base2Log(p->nVars);
|
||||
p->Power2 = 1 << p->LogN;
|
||||
//p->pSat = Sbm_AddCardinSolver( p->LogN, &p->vCardVars );
|
||||
p->pSat = sat_solver_new();
|
||||
sat_solver_setnvars( p->pSat, p->nVars );
|
||||
p->FirstVar = sat_solver_nvars( p->pSat );
|
||||
sat_solver_bookmark( p->pSat );
|
||||
p->pGia = pGia;
|
||||
// internal
|
||||
p->vFirsts = Vec_IntAlloc( 0 );
|
||||
p->vNvars = Vec_IntAlloc( 0 );
|
||||
p->vLits = Vec_IntAlloc( 0 );
|
||||
nVarsAll = Seg_ManCountIntLevels( p, p->FirstVar );
|
||||
sat_solver_setnvars( p->pSat, nVarsAll );
|
||||
printf( "Edges = %d. Total = %d.\n", p->FirstVar, nVarsAll );
|
||||
// other
|
||||
Gia_ManFillValue( pGia );
|
||||
return p;
|
||||
}
|
||||
void Seg_ManClean( Seg_Man_t * p )
|
||||
{
|
||||
p->timeStart = Abc_Clock();
|
||||
sat_solver_rollback( p->pSat );
|
||||
sat_solver_bookmark( p->pSat );
|
||||
// internal
|
||||
Vec_IntClear( p->vEdges );
|
||||
Vec_IntClear( p->vFirsts );
|
||||
Vec_IntClear( p->vNvars );
|
||||
Vec_IntClear( p->vLits );
|
||||
// other
|
||||
Gia_ManFillValue( p->pGia );
|
||||
}
|
||||
void Seg_ManStop( Seg_Man_t * p )
|
||||
{
|
||||
sat_solver_delete( p->pSat );
|
||||
//Vec_IntFree( p->vCardVars );
|
||||
// internal
|
||||
Vec_IntFree( p->vEdges );
|
||||
Vec_IntFree( p->vFirsts );
|
||||
Vec_IntFree( p->vNvars );
|
||||
Vec_IntFree( p->vLits );
|
||||
ABC_FREE( p->pLevels );
|
||||
// other
|
||||
ABC_FREE( p );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Seg_ManCreateCnf( Seg_Man_t * p, int fTwo )
|
||||
{
|
||||
Gia_Obj_t * pObj;
|
||||
Vec_Wec_t * vObjEdges;
|
||||
Vec_Int_t * vLevel;
|
||||
int iLut, iFanin, iFirst;
|
||||
int pLits[3], Count = 0;
|
||||
int i, k, nVars, value;
|
||||
abctime clk = Abc_Clock();
|
||||
// edge delay constraints
|
||||
int nConstr = sat_solver_nclauses(p->pSat);
|
||||
Gia_ManForEachObj( p->pGia, pObj, iLut )
|
||||
{
|
||||
int iFirstLut = Vec_IntEntry( p->vFirsts, iLut );
|
||||
int nVarsLut = Vec_IntEntry( p->vNvars, iLut );
|
||||
if ( !Gia_ObjIsLut(p->pGia, iLut) )
|
||||
continue;
|
||||
Gia_LutForEachFanin( p->pGia, iLut, iFanin, i )
|
||||
if ( Gia_ObjIsAnd(Gia_ManObj(p->pGia, iFanin)) )
|
||||
{
|
||||
iFirst = Vec_IntEntry( p->vFirsts, iFanin );
|
||||
nVars = Vec_IntEntry( p->vNvars, iFanin );
|
||||
assert( nVars != 1 && nVars < nVarsLut );
|
||||
// add initial
|
||||
if ( nVars == 0 )
|
||||
{
|
||||
pLits[0] = Abc_Var2Lit( Count, 1 );
|
||||
pLits[1] = Abc_Var2Lit( iFirstLut, 0 );
|
||||
value = sat_solver_addclause( p->pSat, pLits, pLits+2 );
|
||||
assert( value );
|
||||
|
||||
pLits[0] = Abc_Var2Lit( Count, 0 );
|
||||
pLits[1] = Abc_Var2Lit( iFirstLut+1, 0 );
|
||||
value = sat_solver_addclause( p->pSat, pLits, pLits+2 );
|
||||
assert( value );
|
||||
}
|
||||
// add others
|
||||
for ( k = 0; k < nVars; k++ )
|
||||
{
|
||||
pLits[0] = Abc_Var2Lit( iFirst+k, 1 );
|
||||
pLits[1] = Abc_Var2Lit( Count, 1 );
|
||||
pLits[2] = Abc_Var2Lit( iFirstLut+k, 0 );
|
||||
value = sat_solver_addclause( p->pSat, pLits, pLits+3 );
|
||||
assert( value );
|
||||
|
||||
pLits[0] = Abc_Var2Lit( iFirst+k, 1 );
|
||||
pLits[1] = Abc_Var2Lit( Count, 0 );
|
||||
pLits[2] = Abc_Var2Lit( iFirstLut+k+1, 0 );
|
||||
value = sat_solver_addclause( p->pSat, pLits, pLits+3 );
|
||||
assert( value );
|
||||
}
|
||||
Count++;
|
||||
}
|
||||
}
|
||||
assert( Count == p->nVars );
|
||||
printf( "Delay constraints = %d. ", sat_solver_nclauses(p->pSat) - nConstr );
|
||||
nConstr = sat_solver_nclauses(p->pSat);
|
||||
/*
|
||||
// delay relationship constraints
|
||||
Vec_IntForEachEntryTwo( p->vFirsts, p->vNvars, iFirst, nVars, iLut )
|
||||
{
|
||||
if ( nVars < 2 )
|
||||
continue;
|
||||
for ( i = 1; i < nVars; i++ )
|
||||
{
|
||||
pLits[0] = Abc_Var2Lit( iFirst + i - 1, 1 );
|
||||
pLits[1] = Abc_Var2Lit( iFirst + i, 0 );
|
||||
value = sat_solver_addclause( p->pSat, pLits, pLits+2 );
|
||||
assert( value );
|
||||
}
|
||||
}
|
||||
*/
|
||||
// edge compatibility constraint
|
||||
vObjEdges = Seg_ManCollectObjEdges( p->vEdges, Gia_ManObjNum(p->pGia) );
|
||||
Vec_WecForEachLevel( vObjEdges, vLevel, i )
|
||||
{
|
||||
int v1, v2, v3, Var1, Var2, Var3;
|
||||
if ( !fTwo && Vec_IntSize(vLevel) >= 2 )
|
||||
{
|
||||
Vec_IntForEachEntry( vLevel, Var1, v1 )
|
||||
Vec_IntForEachEntryStart( vLevel, Var2, v2, v1 + 1 )
|
||||
{
|
||||
pLits[0] = Abc_Var2Lit( Var1, 1 );
|
||||
pLits[1] = Abc_Var2Lit( Var2, 1 );
|
||||
value = sat_solver_addclause( p->pSat, pLits, pLits+2 );
|
||||
assert( value );
|
||||
}
|
||||
}
|
||||
else if ( fTwo && Vec_IntSize(vLevel) >= 3 )
|
||||
{
|
||||
Vec_IntForEachEntry( vLevel, Var1, v1 )
|
||||
Vec_IntForEachEntryStart( vLevel, Var2, v2, v1 + 1 )
|
||||
Vec_IntForEachEntryStart( vLevel, Var3, v3, v2 + 1 )
|
||||
{
|
||||
pLits[0] = Abc_Var2Lit( Var1, 1 );
|
||||
pLits[1] = Abc_Var2Lit( Var2, 1 );
|
||||
pLits[2] = Abc_Var2Lit( Var3, 1 );
|
||||
value = sat_solver_addclause( p->pSat, pLits, pLits+3 );
|
||||
assert( value );
|
||||
}
|
||||
}
|
||||
}
|
||||
Vec_WecFree( vObjEdges );
|
||||
printf( "Edge constraints = %d. ", sat_solver_nclauses(p->pSat) - nConstr );
|
||||
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Seg_ManConvertResult( Seg_Man_t * p )
|
||||
{
|
||||
int iFanin, iObj, i;
|
||||
Vec_Int_t * vEdges2 = Vec_IntAlloc( 1000 );
|
||||
Vec_IntForEachEntryDouble( p->vEdges, iFanin, iObj, i )
|
||||
if ( sat_solver_var_value(p->pSat, i/2) )
|
||||
Vec_IntPushTwo( vEdges2, iFanin, iObj );
|
||||
Gia_ManEdgeFromArray( p->pGia, vEdges2 );
|
||||
Vec_IntFree( vEdges2 );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Seg_ManComputeDelay( Gia_Man_t * pGia, int Delay, int fTwo, int fVerbose )
|
||||
{
|
||||
Gia_Obj_t * pObj;
|
||||
abctime clk = Abc_Clock();
|
||||
int i, d, iLut, iFirst, nVars, status, Limit;//, value;
|
||||
Seg_Man_t * p = Seg_ManAlloc( pGia );
|
||||
|
||||
//if ( fVerbose )
|
||||
printf( "Running SatEdge with delay %d and edge %d\n", Delay, fTwo+1 );
|
||||
|
||||
Seg_ManCreateCnf( p, fTwo );
|
||||
//Sat_SolverWriteDimacs( p->pSat, "test_edge.cnf", NULL, NULL, 0 );
|
||||
|
||||
// for ( Delay = p->DelayMax; Delay >= 2; Delay-- )
|
||||
{
|
||||
// collect assumptions
|
||||
Vec_IntClear( p->vLits );
|
||||
Gia_ManForEachCoDriver( p->pGia, pObj, i )
|
||||
{
|
||||
if ( !Gia_ObjIsAnd(pObj) )
|
||||
continue;
|
||||
iLut = Gia_ObjId( p->pGia, pObj );
|
||||
iFirst = Vec_IntEntry( p->vFirsts, iLut );
|
||||
nVars = Vec_IntEntry( p->vNvars, iLut );
|
||||
Limit = Abc_MinInt( nVars, Delay );
|
||||
|
||||
// for ( d = 0; d < Limit; d++ )
|
||||
// Vec_IntPush( p->vLits, Abc_Var2Lit(iFirst + d, 0) );
|
||||
// value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits) );
|
||||
// assert( value );
|
||||
|
||||
for ( d = Delay; d < nVars; d++ )
|
||||
Vec_IntPush( p->vLits, Abc_Var2Lit(iFirst + d, 1) );
|
||||
|
||||
}
|
||||
// solve with assumptions
|
||||
status = sat_solver_solve( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits), 0, 0, 0, 0 );
|
||||
|
||||
//if ( status != l_True )
|
||||
// break;
|
||||
|
||||
if ( status == l_True )
|
||||
{
|
||||
int Count = 0;
|
||||
for ( i = 0; i < p->nVars; i++ )
|
||||
Count += sat_solver_var_value(p->pSat, i);
|
||||
|
||||
//printf( "\n" );
|
||||
//Vec_IntPrint( p->vLits );
|
||||
printf( "Solution with delay %d exists. Edges = %d. ", Delay, Count );
|
||||
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
|
||||
|
||||
if ( fVerbose )
|
||||
{
|
||||
for ( i = 0; i < p->nVars; i++ )
|
||||
printf( "%d=%d ", i, sat_solver_var_value(p->pSat, i) );
|
||||
printf( " " );
|
||||
|
||||
for ( i = p->nVars; i < sat_solver_nvars(p->pSat); i++ )
|
||||
printf( "%d=%d ", i, sat_solver_var_value(p->pSat, i) );
|
||||
printf( "\n" );
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
printf( "Proved UNSAT for delay %d. ", Delay );
|
||||
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
|
||||
}
|
||||
}
|
||||
// convert and quit
|
||||
if ( status == l_True )
|
||||
Seg_ManConvertResult( p );
|
||||
Seg_ManStop( p );
|
||||
}
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
|
|
@ -453,7 +453,7 @@ float Gia_ManDelayTraceLutPrint( Gia_Man_t * p, int fVerbose )
|
|||
return -ABC_INFINITY;
|
||||
}
|
||||
// decide how many steps
|
||||
nSteps = pLutLib ? 20 : Gia_ManLutLevel(p);
|
||||
nSteps = pLutLib ? 20 : Gia_ManLutLevel(p, NULL);
|
||||
pCounters = ABC_ALLOC( int, nSteps + 1 );
|
||||
memset( pCounters, 0, sizeof(int)*(nSteps + 1) );
|
||||
// perform delay trace
|
||||
|
|
|
|||
|
|
@ -56,6 +56,7 @@ SRC += src/aig/gia/giaAig.c \
|
|||
src/aig/gia/giaResub.c \
|
||||
src/aig/gia/giaRetime.c \
|
||||
src/aig/gia/giaRex.c \
|
||||
src/aig/gia/giaSatEdge.c \
|
||||
src/aig/gia/giaSatLut.c \
|
||||
src/aig/gia/giaSatMap.c \
|
||||
src/aig/gia/giaScl.c \
|
||||
|
|
|
|||
|
|
@ -34850,12 +34850,23 @@ usage:
|
|||
int Abc_CommandAbc9Edge( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||
{
|
||||
extern int Edg_ManAssignEdgeNew( Gia_Man_t * p, int nEdges, int fVerbose );
|
||||
extern void Seg_ManComputeDelay( Gia_Man_t * pGia, int Delay, int fTwo, int fVerbose );
|
||||
|
||||
int c, DelayMax = 0, nEdges = 1, fReverse = 0, fUsePack = 0, fUseOld = 0, fVerbose = 0;
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "Erpovh" ) ) != EOF )
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "DErpovh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
case 'D':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-D\" should be followed by a positive integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
DelayMax = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
break;
|
||||
case 'E':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
|
|
@ -34912,6 +34923,11 @@ int Abc_CommandAbc9Edge( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
Gia_ManConvertPackingToEdges( pAbc->pGia );
|
||||
return 0;
|
||||
}
|
||||
if ( DelayMax )
|
||||
{
|
||||
Seg_ManComputeDelay( pAbc->pGia, DelayMax, nEdges==2, fVerbose );
|
||||
return 0;
|
||||
}
|
||||
if ( !fUseOld )
|
||||
{
|
||||
if ( pAbc->pGia->pManTime != NULL && Tim_ManBoxNum((Tim_Man_t*)pAbc->pGia->pManTime) )
|
||||
|
|
@ -34935,8 +34951,9 @@ int Abc_CommandAbc9Edge( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
return 0;
|
||||
|
||||
usage:
|
||||
Abc_Print( -2, "usage: &edge [-E num] [-rpovh]\n" );
|
||||
Abc_Print( -2, "usage: &edge [-DE num] [-rpovh]\n" );
|
||||
Abc_Print( -2, "\t find edge assignment of the LUT-mapped network\n" );
|
||||
Abc_Print( -2, "\t-D num : the upper bound on delay [default = %d]\n", DelayMax );
|
||||
Abc_Print( -2, "\t-E num : the limit on the number of edges (1 <= num <= 2) [default = %d]\n", nEdges );
|
||||
Abc_Print( -2, "\t-r : toggles using reverse order [default = %s]\n", fReverse? "yes": "no" );
|
||||
Abc_Print( -2, "\t-p : toggles deriving edges from packing [default = %s]\n", fUsePack? "yes": "no" );
|
||||
|
|
@ -40922,6 +40939,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
// Gia_ManCheckFalseTest( pAbc->pGia, nFrames );
|
||||
// Gia_ParTest( pAbc->pGia, nWords, nProcs );
|
||||
Gia_Iso3Test( pAbc->pGia );
|
||||
|
||||
// printf( "\nThis command is currently disabled.\n\n" );
|
||||
return 0;
|
||||
usage:
|
||||
|
|
|
|||
Loading…
Reference in New Issue