summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/giaSatEdge.c44
-rw-r--r--src/base/abci/abc.c20
2 files changed, 48 insertions, 16 deletions
diff --git a/src/aig/gia/giaSatEdge.c b/src/aig/gia/giaSatEdge.c
index 02b442f7..13446414 100644
--- a/src/aig/gia/giaSatEdge.c
+++ b/src/aig/gia/giaSatEdge.c
@@ -48,6 +48,7 @@ struct Seg_Man_t_
// window
Gia_Man_t * pGia;
Vec_Int_t * vPolars; // polarity
+ Vec_Int_t * vToSkip; // edges to skip
Vec_Int_t * vEdges; // edges as fanin/fanout pairs
Vec_Int_t * vFirsts; // first SAT variable
Vec_Int_t * vNvars; // number of SAT variables
@@ -75,20 +76,27 @@ extern sat_solver * Sbm_AddCardinSolver( int LogN, Vec_Int_t ** pvVars );
SeeAlso []
***********************************************************************/
-Vec_Int_t * Seg_ManCountIntEdges( Gia_Man_t * p, Vec_Int_t * vPolars )
+Vec_Int_t * Seg_ManCountIntEdges( Gia_Man_t * p, Vec_Int_t * vPolars, Vec_Int_t * vToSkip, int nFanouts )
{
int i, iLut, iFanin;
Vec_Int_t * vEdges = Vec_IntAlloc( 1000 );
assert( Gia_ManHasMapping(p) );
Vec_IntClear( vPolars );
+ Vec_IntClear( vToSkip );
+ if ( nFanouts )
+ Gia_ManSetLutRefs( p );
Gia_ManForEachLut( p, iLut )
Gia_LutForEachFanin( p, iLut, iFanin, i )
if ( Gia_ObjIsAnd(Gia_ManObj(p, iFanin)) )
{
if ( p->vEdge1 && Gia_ObjCheckEdge(p, iFanin, iLut) )
Vec_IntPush( vPolars, Vec_IntSize(vEdges)/2 );
+ if ( nFanouts && Gia_ObjLutRefNumId(p, iFanin) >= nFanouts )
+ Vec_IntPush( vToSkip, Vec_IntSize(vEdges)/2 );
Vec_IntPushTwo( vEdges, iFanin, iLut );
}
+ if ( nFanouts )
+ ABC_FREE( p->pLutRefs );
return vEdges;
}
Vec_Wec_t * Seg_ManCollectObjEdges( Vec_Int_t * vEdges, int nObjs )
@@ -144,12 +152,13 @@ int Seg_ManCountIntLevels( Seg_Man_t * p, int iStartVar )
SeeAlso []
***********************************************************************/
-Seg_Man_t * Seg_ManAlloc( Gia_Man_t * pGia )
+Seg_Man_t * Seg_ManAlloc( Gia_Man_t * pGia, int nFanouts )
{
int nVarsAll;
Seg_Man_t * p = ABC_CALLOC( Seg_Man_t, 1 );
p->vPolars = Vec_IntAlloc( 1000 );
- p->vEdges = Seg_ManCountIntEdges( pGia, p->vPolars );
+ p->vToSkip = Vec_IntAlloc( 1000 );
+ p->vEdges = Seg_ManCountIntEdges( pGia, p->vPolars, p->vToSkip, nFanouts );
p->nVars = Vec_IntSize(p->vEdges)/2;
p->LogN = Abc_Base2Log(p->nVars);
p->Power2 = 1 << p->LogN;
@@ -180,6 +189,7 @@ void Seg_ManClean( Seg_Man_t * p )
Vec_IntClear( p->vNvars );
Vec_IntClear( p->vLits );
Vec_IntClear( p->vPolars );
+ Vec_IntClear( p->vToSkip );
// other
Gia_ManFillValue( p->pGia );
}
@@ -193,6 +203,7 @@ void Seg_ManStop( Seg_Man_t * p )
Vec_IntFree( p->vNvars );
Vec_IntFree( p->vLits );
Vec_IntFree( p->vPolars );
+ Vec_IntFree( p->vToSkip );
ABC_FREE( p->pLevels );
// other
ABC_FREE( p );
@@ -217,7 +228,7 @@ void Seg_ManCreateCnf( Seg_Man_t * p, int fTwo, int fVerbose )
Vec_Int_t * vLevel;
int iLut, iFanin, iFirst;
int pLits[3], Count = 0;
- int i, k, nVars, value;
+ int i, k, nVars, Edge, value;
abctime clk = Abc_Clock();
// edge delay constraints
int nConstr = sat_solver_nclauses(p->pSat);
@@ -380,6 +391,13 @@ void Seg_ManCreateCnf( Seg_Man_t * p, int fTwo, int fVerbose )
}
}
Vec_WecFree( vObjEdges );
+ // block forbidden edges
+ Vec_IntForEachEntry( p->vToSkip, Edge, i )
+ {
+ pLits[0] = Abc_Var2Lit( Edge, 1 );
+ value = sat_solver_addclause( p->pSat, pLits, pLits+1 );
+ assert( value );
+ }
if ( fVerbose )
printf( "Edge constraints = %d. ", sat_solver_nclauses(p->pSat) - nConstr );
if ( fVerbose )
@@ -418,7 +436,7 @@ Vec_Int_t * Seg_ManConvertResult( Seg_Man_t * p )
SeeAlso []
***********************************************************************/
-void Seg_ManComputeDelay( Gia_Man_t * pGia, int DelayInit, int fTwo, int fVerbose )
+void Seg_ManComputeDelay( Gia_Man_t * pGia, int DelayInit, int nFanouts, int fTwo, int fVerbose )
{
int nBTLimit = 0;
int nTimeOut = 0;
@@ -428,7 +446,7 @@ void Seg_ManComputeDelay( Gia_Man_t * pGia, int DelayInit, int fTwo, int fVerbos
abctime clk = Abc_Clock();
Vec_Int_t * vEdges2 = NULL;
int i, iLut, iFirst, nVars, status, Delay, nConfs;
- Seg_Man_t * p = Seg_ManAlloc( pGia );
+ Seg_Man_t * p = Seg_ManAlloc( pGia, nFanouts );
Vec_Int_t * vVars = Vec_IntStartNatural( p->nVars );
int DelayStart = DelayInit ? DelayInit : p->DelayMax;
@@ -447,16 +465,20 @@ void Seg_ManComputeDelay( Gia_Man_t * pGia, int DelayInit, int fTwo, int fVerbos
// increment delay gradually
for ( Delay = p->DelayMax; Delay >= 0; Delay-- )
{
+ // we constrain COs, although it would be fine to constrain only POs
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 );
- if ( Delay < nVars )
- sat_solver_push( p->pSat, Abc_Var2Lit(iFirst + Delay, 1) );
-
+ if ( Delay < nVars && !sat_solver_push(p->pSat, Abc_Var2Lit(iFirst + Delay, 1)) )
+ break;
+ }
+ if ( i < Gia_ManCoNum(p->pGia) )
+ {
+ printf( "Proved UNSAT for delay %d. ", Delay );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ break;
}
if ( Delay > DelayStart )
continue;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c0052a74..f8935902 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -34858,11 +34858,11 @@ 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 );
+ extern void Seg_ManComputeDelay( Gia_Man_t * pGia, int Delay, int nFanouts, int fTwo, int fVerbose );
- int c, DelayMax = 0, nEdges = 1, fReverse = 0, fUsePack = 0, fUseOld = 0, fVerbose = 0;
+ int c, DelayMax = 0, nFanouts = 0, nEdges = 1, fReverse = 0, fUsePack = 0, fUseOld = 0, fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "DErpovh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "DFErpovh" ) ) != EOF )
{
switch ( c )
{
@@ -34875,6 +34875,15 @@ int Abc_CommandAbc9Edge( Abc_Frame_t * pAbc, int argc, char ** argv )
DelayMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
break;
+ case 'F':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-F\" should be followed by a positive integer.\n" );
+ goto usage;
+ }
+ nFanouts = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ break;
case 'E':
if ( globalUtilOptind >= argc )
{
@@ -34934,7 +34943,7 @@ int Abc_CommandAbc9Edge( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( !fUseOld )
{
//Edg_ManAssignEdgeNew( pAbc->pGia, nEdges, fVerbose );
- Seg_ManComputeDelay( pAbc->pGia, DelayMax, nEdges==2, fVerbose );
+ Seg_ManComputeDelay( pAbc->pGia, DelayMax, nFanouts, nEdges==2, fVerbose );
return 0;
}
if ( pAbc->pGia->pManTime && fReverse )
@@ -34950,9 +34959,10 @@ int Abc_CommandAbc9Edge( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: &edge [-DE num] [-rpovh]\n" );
+ Abc_Print( -2, "usage: &edge [-DFE 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-F num : skip using edge if fanout higher than this [default = %d]\n", nFanouts );
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" );
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-05 01:10:37 +0000