Skip to content

A
abc
Commit 385cb73d by Alan Mishchenko
Options

Updates to delay optimization project.

parent 4b20003e
Showing with 40 additions and 1 deletions
abclib.dsp
......@@ -2763,6 +2763,10 @@ SOURCE=.\src\opt\sbd\sbdCut.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\sbd\sbdCut2.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\sbd\sbdInt.h
# End Source File
# Begin Source File
......
src/opt/sbd/module.make
......@@ -2,6 +2,7 @@ SRC += src/opt/sbd/sbd.c \
src/opt/sbd/sbdCnf.c \
src/opt/sbd/sbdCore.c \
src/opt/sbd/sbdCut.c \
src/opt/sbd/sbdCut2.c \
src/opt/sbd/sbdLut.c \
src/opt/sbd/sbdSat.c \
src/opt/sbd/sbdWin.c
src/opt/sbd/sbdCore.c
......@@ -56,6 +56,7 @@ struct Sbd_Man_t_
abctime timeOther;
abctime timeTotal;
Sbd_Sto_t * pSto;
Sbd_Srv_t * pSrv;
// target node
int Pivot; // target node
int DivCutoff; // the place where D-2 divisors begin
......@@ -230,7 +231,8 @@ Sbd_Man_t * Sbd_ManStart( Gia_Man_t * pGia, Sbd_Par_t * pPars )
for ( w = 0; w < p->pPars->nWords; w++ )
Sbd_ObjSim0(p, Id)[w] = Gia_ManRandomW( 0 );
// cut enumeration
p->pSto = Sbd_StoAlloc( pGia, p->vMirrors, pPars->nLutSize, pPars->nCutSize, pPars->nCutNum, 1, 1 );
p->pSto = Sbd_StoAlloc( pGia, p->vMirrors, pPars->nLutSize, pPars->nLutSize, pPars->nCutNum, 1, 1 );
p->pSrv = Sbd_ManCutServerStart( pGia, p->vMirrors, p->vLutLevs, NULL, NULL, pPars->nLutSize, pPars->nCutSize, pPars->nCutNum, 0 );
return p;
}
void Sbd_ManStop( Sbd_Man_t * p )
......@@ -257,6 +259,7 @@ void Sbd_ManStop( Sbd_Man_t * p )
Vec_WrdFree( p->vMatrix );
sat_solver_delete_p( &p->pSat );
Sbd_StoFree( p->pSto );
Sbd_ManCutServerStop( p->pSrv );
ABC_FREE( p );
}
......@@ -1320,6 +1323,11 @@ int Sbd_ManExploreCut( Sbd_Man_t * p, int Pivot, int nLeaves, int * pLeaves, int
clk = Abc_Clock();
Truth = Sbd_ManSolve( p->pSat, PivotVar, (*pFreeVar)++, p->vDivSet, p->vDivVars, p->vDivValues, p->vLits );
p->timeSat += Abc_Clock() - clk;
if ( Truth == SBD_SAT_SAT )
{
printf( "The cut at node %d is not topological.\n", p->Pivot );
return 0;
}
assert( Truth != SBD_SAT_UNDEC && Truth != SBD_SAT_SAT );
// create structure
Strs->fLut = 1;
......@@ -1552,6 +1560,17 @@ int Sbd_ManExplore3( Sbd_Man_t * p, int Pivot, int * pnStrs, Sbd_Str_t * Strs )
p->pSat = Sbd_ManSatSolver( p->pSat, p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots, 0 );
p->timeCnf += Abc_Clock() - clk;
// extract one cut
if ( p->pSrv )
{
nLeaves = Sbd_ManCutServerFirst( p->pSrv, Pivot, pLeaves );
if ( nLeaves == -1 )
return 0;
assert( nLeaves <= p->pPars->nCutSize );
if ( Sbd_ManExploreCut( p, Pivot, nLeaves, pLeaves, pnStrs, Strs, &FreeVar ) )
return 1;
return 0;
}
// extract one cut
for ( nSize = p->pPars->nLutSize + 1; nSize <= p->pPars->nCutSize; nSize++ )
{
nLeaves = Sbd_StoObjBestCut( p->pSto, Pivot, nSize, pLeaves );
......@@ -1679,6 +1698,7 @@ int Sbd_ManMergeCuts( Sbd_Man_t * p, int Node )
assert( iFan0 != iFan1 );
assert( Vec_IntEntry(p->vLutLevs, Node) == 0 );
Vec_IntWriteEntry( p->vLutLevs, Node, LevCur );
//Vec_IntWriteEntry( p->vLevs, Node, 1+Abc_MaxInt(Vec_IntEntry(p->vLevs, iFan0), Vec_IntEntry(p->vLevs, iFan1)) );
assert( pCutRes[0] <= p->pPars->nLutSize );
memcpy( Sbd_ObjCut(p, Node), pCutRes, sizeof(int) * (pCutRes[0] + 1) );
//printf( "Setting node %d with delay %d.\n", Node, LevCur );
......@@ -1742,6 +1762,7 @@ void Sbd_ManFindCut( Sbd_Man_t * p, int Node, Vec_Int_t * vCutLits )
// create cut
assert( Vec_IntEntry(p->vLutLevs, Node) == 0 );
Vec_IntWriteEntry( p->vLutLevs, Node, LevelMax+1 );
//Vec_IntWriteEntry( p->vLevs, Node, 1+Abc_MaxInt(Vec_IntEntry(p->vLevs, Gia_ObjFaninId0(pObj, Node)), Vec_IntEntry(p->vLevs, Gia_ObjFaninId1(pObj, Node))) );
memcpy( Sbd_ObjCut(p, Node), pCut, sizeof(int) * (pCut[0] + 1) );
}
......@@ -1803,11 +1824,13 @@ int Sbd_ManImplement( Sbd_Man_t * p, int Pivot, word Truth )
// update delay of the initial node
assert( Vec_IntEntry(p->vLutLevs, Pivot) == iCurLev );
Vec_IntWriteEntry( p->vLutLevs, Pivot, iNewLev );
//Vec_IntWriteEntry( p->vLevs, Pivot, 1+Abc_MaxInt(Vec_IntEntry(p->vLevs, Gia_ObjFaninId0(pObj, Pivot)), Vec_IntEntry(p->vLevs, Gia_ObjFaninId1(pObj, Pivot))) );
return 0;
}
int Sbd_ManImplement2( Sbd_Man_t * p, int Pivot, int nStrs, Sbd_Str_t * pStrs )
{
Gia_Obj_t * pObj = NULL;
int i, k, w, iLit, Node;
int iObjLast = Gia_ManObjNum(p->pGia);
int iCurLev = Vec_IntEntry(p->vLutLevs, Pivot);
......@@ -1871,11 +1894,13 @@ int Sbd_ManImplement2( Sbd_Man_t * p, int Pivot, int nStrs, Sbd_Str_t * pStrs )
Sbd_StoDerefObj( p->pSto, Pivot );
for ( i = iObjLast; i < Gia_ManObjNum(p->pGia); i++ )
{
Gia_Obj_t * pObjI = Gia_ManObj( p->pGia, i );
abctime clk = Abc_Clock();
int Delay = Sbd_StoComputeCutsNode( p->pSto, i );
p->timeCut += Abc_Clock() - clk;
assert( i == Vec_IntSize(p->vLutLevs) );
Vec_IntPush( p->vLutLevs, Delay );
//Vec_IntPush( p->vLevs, 1+Abc_MaxInt(Vec_IntEntry(p->vLevs, Gia_ObjFaninId0(pObjI, i)), Vec_IntEntry(p->vLevs, Gia_ObjFaninId1(pObjI, i))) );
Vec_IntPush( p->vObj2Var, 0 );
Vec_IntFillExtra( p->vLutCuts, Vec_IntSize(p->vLutCuts) + p->pPars->nLutSize + 1, 0 );
//Sbd_ManFindCut( p, i, p->vLits );
......@@ -1887,8 +1912,10 @@ int Sbd_ManImplement2( Sbd_Man_t * p, int Pivot, int nStrs, Sbd_Str_t * pStrs )
iNewLev = Vec_IntEntry( p->vLutLevs, Abc_Lit2Var(iLit) );
assert( !iNewLev || iNewLev < iCurLev );
// update delay of the initial node
pObj = Gia_ManObj( p->pGia, Pivot );
assert( Vec_IntEntry(p->vLutLevs, Pivot) == iCurLev );
Vec_IntWriteEntry( p->vLutLevs, Pivot, iNewLev );
//Vec_IntWriteEntry( p->vLevs, Pivot, Pivot ? 1+Abc_MaxInt(Vec_IntEntry(p->vLevs, Gia_ObjFaninId0(pObj, Pivot)), Vec_IntEntry(p->vLevs, Gia_ObjFaninId1(pObj, Pivot))) : 0 );
return 0;
}
......
src/opt/sbd/sbdInt.h
......@@ -62,6 +62,7 @@ ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
typedef struct Sbd_Sto_t_ Sbd_Sto_t;
typedef struct Sbd_Srv_t_ Sbd_Srv_t;
typedef struct Sbd_Str_t_ Sbd_Str_t;
struct Sbd_Str_t_
......@@ -92,6 +93,12 @@ extern void Sbd_StoComputeCutsObj( Sbd_Sto_t * p, int iObj, int Delay, i
extern void Sbd_StoComputeCutsCi( Sbd_Sto_t * p, int iObj, int Delay, int Level );
extern int Sbd_StoComputeCutsNode( Sbd_Sto_t * p, int iObj );
extern int Sbd_StoObjBestCut( Sbd_Sto_t * p, int iObj, int nSize, int * pLeaves );
/*=== sbdCut2.c ==========================================================*/
extern Sbd_Srv_t * Sbd_ManCutServerStart( Gia_Man_t * pGia, Vec_Int_t * vMirrors,
Vec_Int_t * vLutLevs, Vec_Int_t * vLevs, Vec_Int_t * vRefs,
int nLutSize, int nCutSize, int nCutNum, int fVerbose );
extern void Sbd_ManCutServerStop( Sbd_Srv_t * p );
extern int Sbd_ManCutServerFirst( Sbd_Srv_t * p, int iObj, int * pLeaves );
/*=== sbdWin.c ==========================================================*/
extern word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivSet, Vec_Int_t * vDivVars, Vec_Int_t * vDivValues, Vec_Int_t * vTemp );
extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment