From 1b550cb87be41af5e0f2c0ce7805b9ab645d87cc Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 22 Apr 2016 08:36:05 +0300 Subject: Improved algo for edge computation. --- src/aig/gia/gia.h | 2 +- src/aig/gia/giaEdge.c | 8 +- src/aig/gia/giaIf.c | 7 +- src/aig/gia/giaSatEdge.c | 417 +++++++++++++++++++++++++++++++++++++++++++++++ src/aig/gia/giaSpeedup.c | 2 +- src/aig/gia/module.make | 1 + 6 files changed, 430 insertions(+), 7 deletions(-) create mode 100644 src/aig/gia/giaSatEdge.c (limited to 'src/aig/gia') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index af29a72e..16d649cf 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -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 ); diff --git a/src/aig/gia/giaEdge.c b/src/aig/gia/giaEdge.c index b74bbe5c..36a375eb 100644 --- a/src/aig/gia/giaEdge.c +++ b/src/aig/gia/giaEdge.c @@ -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 ) { diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c index 59afb4da..79cfcf6d 100644 --- a/src/aig/gia/giaIf.c +++ b/src/aig/gia/giaIf.c @@ -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; } diff --git a/src/aig/gia/giaSatEdge.c b/src/aig/gia/giaSatEdge.c new file mode 100644 index 00000000..982aaa79 --- /dev/null +++ b/src/aig/gia/giaSatEdge.c @@ -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 + diff --git a/src/aig/gia/giaSpeedup.c b/src/aig/gia/giaSpeedup.c index b23decae..0d593993 100644 --- a/src/aig/gia/giaSpeedup.c +++ b/src/aig/gia/giaSpeedup.c @@ -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 diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index 8c3d5a39..adc21d74 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -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 \ -- cgit v1.2.3