luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Improved algo for edge computation.

This commit is contained in:
Alan Mishchenko 2016-04-24 20:49:05 +03:00
parent f91f23bed0
commit e37ec2aac5
3 changed files with 90 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
src/aig/gia/giaIf.c
View File

@ -175,8 +175,11 @@ int Gia_ManLutLevel( Gia_Man_t * p, int ** ppLevels )
}
Level = 0;
Gia_ManForEachCo( p, pObj, k )
if ( Level < pLevels[Gia_ObjFaninId0p(p, pObj)] )
Level = pLevels[Gia_ObjFaninId0p(p, pObj)];
{
int LevelFan = pLevels[Gia_ObjFaninId0p(p, pObj)];
Level = Abc_MaxInt( Level, LevelFan );
pLevels[Gia_ObjId(p, pObj)] = LevelFan;
}
if ( ppLevels )
*ppLevels = pLevels;
else

90
src/aig/gia/giaSatEdge.c
View File

@ -98,16 +98,29 @@ Vec_Wec_t * Seg_ManCollectObjEdges( Vec_Int_t * vEdges, int nObjs )
}
int Seg_ManCountIntLevels( Seg_Man_t * p, int iStartVar )
{
Gia_Obj_t * pObj;
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 )
if ( p->pGia->pManTime )
{
p->DelayMax = Gia_ManLutLevelWithBoxes( p->pGia );
p->pLevels = Vec_IntReleaseArray( p->pGia->vLevels );
Vec_IntFreeP( &p->pGia->vLevels );
}
else
p->DelayMax = Gia_ManLutLevel( p->pGia, &p->pLevels );
Gia_ManForEachObj1( p->pGia, pObj, iLut )
{
if ( Gia_ObjIsCo(pObj) )
continue;
if ( Gia_ObjIsAnd(pObj) && !Gia_ObjIsLut(p->pGia, iLut) )
continue;
assert( Gia_ObjIsCi(pObj) || Gia_ObjIsLut(p->pGia, iLut) );
Vec_IntWriteEntry( p->vFirsts, iLut, iStartVar );
assert( p->pLevels[iLut] > 0 );
nVars = p->pLevels[iLut] == 1 ? 0 : p->pLevels[iLut];
//assert( p->pLevels[iLut] > 0 );
nVars = p->pLevels[iLut] < 2 ? 0 : p->pLevels[iLut];
Vec_IntWriteEntry( p->vNvars, iLut, nVars );
iStartVar += nVars;
}
@ -189,6 +202,7 @@ void Seg_ManStop( Seg_Man_t * p )
***********************************************************************/
void Seg_ManCreateCnf( Seg_Man_t * p, int fTwo, int fVerbose )
{
Tim_Man_t * pTim = (Tim_Man_t *)p->pGia->pManTime;
Gia_Obj_t * pObj;
Vec_Wec_t * vObjEdges;
Vec_Int_t * vLevel;
@ -202,10 +216,76 @@ void Seg_ManCreateCnf( Seg_Man_t * p, int fTwo, int fVerbose )
{
int iFirstLut = Vec_IntEntry( p->vFirsts, iLut );
int nVarsLut = Vec_IntEntry( p->vNvars, iLut );
if ( pTim && Gia_ObjIsCi(pObj) )
{
int iBox = Tim_ManBoxForCi( pTim, Gia_ObjCioId(pObj) );
if ( nVarsLut > 0 && iBox >= 0 )
{
int iCiId = Tim_ManBoxOutputFirst( pTim, iBox );
if ( iCiId == Gia_ObjCioId(pObj) ) // first input
{
int nIns = Tim_ManBoxInputNum( pTim, iBox );
int iIn0 = Tim_ManBoxInputFirst( pTim, iBox );
for ( i = 0; i < nIns-1; i++ ) // skip carry-in pin
{
Gia_Obj_t * pOut = Gia_ManCo( p->pGia, iIn0+i );
int iDriverId = Gia_ObjFaninId0p( p->pGia, pOut );
int AddOn;
iFirst = Vec_IntEntry( p->vFirsts, iDriverId );
nVars = Vec_IntEntry( p->vNvars, iDriverId );
assert( nVars < nVarsLut );
AddOn = (int)(nVars < nVarsLut);
for ( k = 0; k < nVars; k++ )
{
pLits[0] = Abc_Var2Lit( iFirst+k, 1 );
pLits[1] = Abc_Var2Lit( iFirstLut+k+AddOn, 0 );
value = sat_solver_addclause( p->pSat, pLits, pLits+2 );
assert( value );
}
}
}
else // intermediate input
{
Gia_Obj_t * pIn = Gia_ManCi( p->pGia, iCiId );
int iObjId = Gia_ObjId( p->pGia, pIn );
iFirst = Vec_IntEntry( p->vFirsts, iObjId );
nVars = Vec_IntEntry( p->vNvars, iObjId );
if ( nVars > 0 )
{
for ( k = 0; k < nVars; k++ )
{
pLits[0] = Abc_Var2Lit( iFirst+k, 1 );
pLits[1] = Abc_Var2Lit( iFirstLut+k, 0 );
value = sat_solver_addclause( p->pSat, pLits, pLits+2 );
assert( value );
}
}
}
}
continue;
}
if ( !Gia_ObjIsLut(p->pGia, iLut) )
continue;
Gia_LutForEachFanin( p->pGia, iLut, iFanin, i )
if ( Gia_ObjIsAnd(Gia_ManObj(p->pGia, iFanin)) )
if ( pTim && Gia_ObjIsCi(Gia_ManObj(p->pGia, iFanin)) )
{
iFirst = Vec_IntEntry( p->vFirsts, iFanin );
nVars = Vec_IntEntry( p->vNvars, iFanin );
assert( nVars <= nVarsLut );
if ( nVars > 0 )
{
for ( k = 0; k < nVars; k++ )
{
pLits[0] = Abc_Var2Lit( iFirst+k, 1 );
pLits[1] = Abc_Var2Lit( iFirstLut+k, 0 );
value = sat_solver_addclause( p->pSat, pLits, pLits+2 );
assert( value );
}
}
}
else if ( Gia_ObjIsAnd(Gia_ManObj(p->pGia, iFanin)) )
{
iFirst = Vec_IntEntry( p->vFirsts, iFanin );
nVars = Vec_IntEntry( p->vNvars, iFanin );

5
src/base/abci/abc.c
View File

@ -34931,11 +34931,6 @@ int Abc_CommandAbc9Edge( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( !fUseOld )
{
if ( pAbc->pGia->pManTime != NULL && Tim_ManBoxNum((Tim_Man_t*)pAbc->pGia->pManTime) )
{
printf( "Currently this version of the algorithm does not work for designs with boxes.\n" );
return 0;
}
//Edg_ManAssignEdgeNew( pAbc->pGia, nEdges, fVerbose );
Seg_ManComputeDelay( pAbc->pGia, DelayMax, nEdges==2, fVerbose );
return 0;