From e34d41b374c5be1f5c80ac9ade8bd40a00519c19 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 19 Mar 2014 17:57:34 -0700 Subject: Experiments with recent ideas. --- src/aig/gia/gia.h | 1 + src/aig/gia/giaMan.c | 1 + src/base/abci/abc.c | 97 ++++++++++++++++++++++++++++++++++++++++++++- src/sat/bmc/bmcTulip.c | 104 ++++++++++++++++++++++++++++--------------------- 4 files changed, 156 insertions(+), 47 deletions(-) diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index a5858ca6..79578113 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -139,6 +139,7 @@ struct Gia_Man_t_ Vec_Int_t * vFlopClasses; // classes of flops for retiming/merging/etc Vec_Int_t * vGateClasses; // classes of gates for abstraction Vec_Int_t * vObjClasses; // classes of objects for abstraction + Vec_Int_t * vInitClasses; // classes of flops for retiming/merging/etc Vec_Int_t * vDoms; // dominators unsigned char* pSwitching; // switching activity for each object Gia_Plc_t * pPlacement; // placement of the objects diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 805ab4f9..e78cb849 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -95,6 +95,7 @@ void Gia_ManStop( Gia_Man_t * p ) Vec_IntFreeP( &p->vFlopClasses ); Vec_IntFreeP( &p->vGateClasses ); Vec_IntFreeP( &p->vObjClasses ); + Vec_IntFreeP( &p->vInitClasses ); Vec_IntFreeP( &p->vDoms ); Vec_IntFreeP( &p->vLevels ); Vec_IntFreeP( &p->vTruths ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 76412726..8b8fab5e 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -399,6 +399,7 @@ static int Abc_CommandAbc9Bmc ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9ICheck ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SatTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9FunFaTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Tulip ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9PoPart2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9CexCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9CexMerge ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -962,6 +963,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&icheck", Abc_CommandAbc9ICheck, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&sattest", Abc_CommandAbc9SatTest, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&funfatest", Abc_CommandAbc9FunFaTest, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&tulip", Abc_CommandAbc9Tulip, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&popart2", Abc_CommandAbc9PoPart2, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&cexcut", Abc_CommandAbc9CexCut, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&cexmerge", Abc_CommandAbc9CexMerge, 0 ); @@ -32736,6 +32738,98 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9Tulip( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Vec_Int_t * Gia_ManTulipTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose ); + Vec_Int_t * vTemp; + int c, nFrames = 5, nWords = 1000, nTimeOut = 0, fSim = 0, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "FWTsvh" ) ) != EOF ) + { + switch ( c ) + { + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + nFrames = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nFrames < 0 ) + goto usage; + break; + case 'W': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" ); + goto usage; + } + nWords = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nWords < 0 ) + goto usage; + break; + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + nTimeOut = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nTimeOut < 0 ) + goto usage; + break; + case 's': + fSim ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9Tulip(): There is no AIG.\n" ); + return 0; + } + if ( Gia_ManRegNum(pAbc->pGia) == 0 ) + { + Abc_Print( -1, "Abc_CommandAbc9Tulip(): AIG is combinational.\n" ); + return 0; + } + pAbc->pGia->vInitClasses = Gia_ManTulipTest( pAbc->pGia, vTemp = pAbc->pGia->vInitClasses, nFrames, nWords, nTimeOut, fSim, fVerbose ); + Vec_IntFreeP( &vTemp ); + return 0; + +usage: + Abc_Print( -2, "usage: &tulip [-FWT num] [-scdvh]\n" ); + Abc_Print( -2, "\t experimental prcedure for testing new ideas\n" ); + Abc_Print( -2, "\t-F num : the number of timeframes [default = %d]\n", nFrames ); + Abc_Print( -2, "\t-W num : the number of machine words [default = %d]\n", nWords ); + Abc_Print( -2, "\t-T num : approximate global runtime limit in seconds [default = %d]\n", nTimeOut ); + Abc_Print( -2, "\t-s : toggles using ternary simulation [default = %s]\n", fSim? "yes": "no" ); + Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] @@ -34054,7 +34148,6 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // extern void Agi_ManTest( Gia_Man_t * pGia ); // extern void Gia_ManCheckFalseTest( Gia_Man_t * p, int nSlackMax ); // extern void Gia_ParTest( Gia_Man_t * p, int nWords, int nProcs ); - extern void Gia_ManTulipTest( Gia_Man_t * p, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose ); Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "WPFsvh" ) ) != EOF ) @@ -34158,7 +34251,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // Jf_ManTestCnf( pAbc->pGia ); // Gia_ManCheckFalseTest( pAbc->pGia, nFrames ); // Gia_ParTest( pAbc->pGia, nWords, nProcs ); - Gia_ManTulipTest( pAbc->pGia, nFrames, nWords, 0, fSwitch, fVerbose ); + printf( "\nThis command is currently disabled.\n\n" ); return 0; usage: diff --git a/src/sat/bmc/bmcTulip.c b/src/sat/bmc/bmcTulip.c index 1d790522..29e8781f 100644 --- a/src/sat/bmc/bmcTulip.c +++ b/src/sat/bmc/bmcTulip.c @@ -70,7 +70,7 @@ static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManTulipUnfold( Gia_Man_t * p, int nFrames, int fUseVars ) +Gia_Man_t * Gia_ManTulipUnfold( Gia_Man_t * p, int nFrames, int fUseVars, Vec_Int_t * vInit ) { Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj; @@ -85,8 +85,21 @@ Gia_Man_t * Gia_ManTulipUnfold( Gia_Man_t * p, int nFrames, int fUseVars ) Gia_ManForEachRo( p, pObj, i ) Gia_ManAppendCi( pNew ); // build timeframes + assert( !vInit || Vec_IntSize(vInit) == Gia_ManRegNum(p) ); Gia_ManForEachRo( p, pObj, i ) - pObj->Value = fUseVars ? Gia_ManHashAnd(pNew, Gia_ManCiLit(pNew, i), Gia_ManCiLit(pNew, Gia_ManRegNum(p)+i)) : 0; + { + if ( vInit == NULL ) // assume 2 + pObj->Value = fUseVars ? Gia_ManHashAnd(pNew, Gia_ManCiLit(pNew, i), Gia_ManCiLit(pNew, Gia_ManRegNum(p)+i)) : 0; + else if ( Vec_IntEntry(vInit, i) == 0 ) + pObj->Value = 0; + else if ( Vec_IntEntry(vInit, i) == 1 ) + pObj->Value = 1; + else if ( Vec_IntEntry(vInit, i) == 2 ) + pObj->Value = fUseVars ? Gia_ManHashAnd(pNew, Gia_ManCiLit(pNew, i), Gia_ManCiLit(pNew, Gia_ManRegNum(p)+i)) : 0; + else if ( Vec_IntEntry(vInit, i) == 3 ) + pObj->Value = fUseVars ? Gia_ManHashAnd(pNew, Gia_ManCiLit(pNew, i), Gia_ManCiLit(pNew, Gia_ManRegNum(p)+i)) : 1; + else assert( 0 ); + } for ( f = 0; f < nFrames; f++ ) { Gia_ManForEachPi( p, pObj, i ) @@ -118,7 +131,7 @@ Gia_Man_t * Gia_ManTulipUnfold( Gia_Man_t * p, int nFrames, int fUseVars ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Gia_ManTulip( Gia_Man_t * p, int nFrames, int nTimeOut, int fVerbose ) +Vec_Int_t * Gia_ManTulipPerform( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nTimeOut, int fVerbose ) { int nIterMax = 1000000; int i, iLit, Iter, status; @@ -128,13 +141,15 @@ Vec_Int_t * Gia_ManTulip( Gia_Man_t * p, int nFrames, int nTimeOut, int fVerbose Vec_Int_t * vLits, * vMap; sat_solver * pSat; Gia_Obj_t * pObj; - Gia_Man_t * p0 = Gia_ManTulipUnfold( p, nFrames, 0 ); - Gia_Man_t * p1 = Gia_ManTulipUnfold( p, nFrames, 1 ); + Gia_Man_t * p0 = Gia_ManTulipUnfold( p, nFrames, 0, vInit ); + Gia_Man_t * p1 = Gia_ManTulipUnfold( p, nFrames, 1, vInit ); Gia_Man_t * pM = Gia_ManMiter( p0, p1, 0, 0, 0, 0, 0 ); Cnf_Dat_t * pCnf = Cnf_DeriveGiaRemapped( pM ); Gia_ManStop( p0 ); Gia_ManStop( p1 ); assert( Gia_ManRegNum(p) > 0 ); + if ( fVerbose ) + printf( "Running with %d frames and %sgiven init state.\n", nFrames, vInit ? "":"no " ); pSat = sat_solver_new(); sat_solver_setnvars( pSat, pCnf->nVars ); @@ -154,7 +169,7 @@ Vec_Int_t * Gia_ManTulip( Gia_Man_t * p, int nFrames, int nTimeOut, int fVerbose Gia_ManForEachPi( pM, pObj, i ) if ( i == Gia_ManRegNum(p) ) break; - else + else if ( vInit == NULL || (Vec_IntEntry(vInit, i) & 2) ) Vec_IntPush( vLits, Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pM, pObj)], 1) ); if ( fVerbose ) @@ -163,7 +178,7 @@ Vec_Int_t * Gia_ManTulip( Gia_Man_t * p, int nFrames, int nTimeOut, int fVerbose printf( "Var =%10d ", sat_solver_nvars(pSat) ); printf( "Clause =%10d ", sat_solver_nclauses(pSat) ); printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) ); - printf( "Subset =%6d ", Gia_ManRegNum(p) ); + printf( "Subset =%6d ", Vec_IntSize(vLits) ); Abc_PrintTime( 1, "Time", clkSat ); // ABC_PRTr( "Solver time", clkSat ); } @@ -214,13 +229,18 @@ Vec_Int_t * Gia_ManTulip( Gia_Man_t * p, int nFrames, int nTimeOut, int fVerbose vMap = Vec_IntStart( pCnf->nVars ); Vec_IntForEachEntry( vLits, iLit, i ) Vec_IntWriteEntry( vMap, Abc_Lit2Var(iLit), 1 ); + // create output - Vec_IntClear( vLits ); + Vec_IntFree( vLits ); + if ( vInit ) + vLits = Vec_IntDup(vInit); + else + vLits = Vec_IntAlloc(Gia_ManRegNum(p)), Vec_IntFill(vLits, Gia_ManRegNum(p), 2); Gia_ManForEachPi( pM, pObj, i ) if ( i == Gia_ManRegNum(p) ) break; - else if ( Vec_IntEntry( vMap, pCnf->pVarNums[Gia_ObjId(pM, pObj)] ) ) - Vec_IntPush( vLits, i ); + else if ( (Vec_IntEntry(vLits, i) & 2) && !Vec_IntEntry( vMap, pCnf->pVarNums[Gia_ObjId(pM, pObj)] ) ) + Vec_IntWriteEntry( vLits, i, (Vec_IntEntry(vLits, i) & 1) ); Vec_IntFree( vMap ); // cleanup @@ -243,7 +263,7 @@ Vec_Int_t * Gia_ManTulip( Gia_Man_t * p, int nFrames, int nTimeOut, int fVerbose SeeAlso [] ***********************************************************************/ -void Bmc_RoseSimulateInit( Gia_Man_t * p, Vec_Int_t * vInit ) +void Gia_ManRoseInit( Gia_Man_t * p, Vec_Int_t * vInit ) { Gia_Obj_t * pObj; word * pData1, * pData0; @@ -252,7 +272,7 @@ void Bmc_RoseSimulateInit( Gia_Man_t * p, Vec_Int_t * vInit ) { pData0 = Gia_ParTestObj( p, Gia_ObjId(p, pObj) ); pData1 = pData0 + p->iData; - if ( vInit == NULL ) // both X + if ( vInit == NULL ) // X for ( i = 0; i < p->iData; i++ ) pData0[i] = pData1[i] = 0; else if ( Vec_IntEntry(vInit, k) == 0 ) // 0 @@ -261,12 +281,12 @@ void Bmc_RoseSimulateInit( Gia_Man_t * p, Vec_Int_t * vInit ) else if ( Vec_IntEntry(vInit, k) == 1 ) // 1 for ( i = 0; i < p->iData; i++ ) pData0[i] = 0, pData1[i] = ~(word)0; - else // if ( Vec_IntEntry(vInit, k) == 2 ) + else // if ( Vec_IntEntry(vInit, k) > 1 ) // X for ( i = 0; i < p->iData; i++ ) pData0[i] = pData1[i] = 0; } } -void Bmc_RoseSimulateObj( Gia_Man_t * p, int Id ) +void Gia_ManRoseSimulateObj( Gia_Man_t * p, int Id ) { Gia_Obj_t * pObj = Gia_ManObj( p, Id ); word * pData0, * pDataA0, * pDataB0; @@ -367,7 +387,7 @@ void Bmc_RoseSimulateObj( Gia_Man_t * p, int Id ) SeeAlso [] ***********************************************************************/ -int Bmc_RoseHighestScore( Gia_Man_t * p, int * pCost ) +int Gia_ManRoseHighestScore( Gia_Man_t * p, int * pCost ) { Gia_Obj_t * pObj; word * pData0, * pData1; @@ -392,7 +412,7 @@ int Bmc_RoseHighestScore( Gia_Man_t * p, int * pCost ) ABC_FREE( pCounts ); return iPat; } -void Bmc_RoseFindStarting( Gia_Man_t * p, Vec_Int_t * vInit, int iPat ) +void Gia_ManRoseFindStarting( Gia_Man_t * p, Vec_Int_t * vInit, int iPat ) { Gia_Obj_t * pObj; word * pData0, * pData1; @@ -424,30 +444,37 @@ void Bmc_RoseFindStarting( Gia_Man_t * p, Vec_Int_t * vInit, int iPat ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Bmc_RosePerform( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, int nWords, int fVerbose ) +Vec_Int_t * Gia_ManRosePerform( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, int nWords, int fVerbose ) { Vec_Int_t * vInit; Gia_Obj_t * pObj; - int i, f, iPat, Cost; + int i, f, iPat, Cost, Cost0; abctime clk, clkTotal = Abc_Clock(); Gia_ManRandomW( 1 ); if ( fVerbose ) printf( "Running with %d frames, %d words, and %sgiven init state.\n", nFrames, nWords, vInit0 ? "":"no " ); - vInit = Vec_IntAlloc( Gia_ManRegNum(p) ); + if ( vInit0 ) + vInit = Vec_IntDup(vInit0); + else + vInit = Vec_IntAlloc(Gia_ManRegNum(p)), Vec_IntFill(vInit, Gia_ManRegNum(p), 2); + assert( Vec_IntSize(vInit) == Gia_ManRegNum(p) ); Gia_ParTestAlloc( p, nWords ); - Bmc_RoseSimulateInit( p, vInit0 ); + Gia_ManRoseInit( p, vInit ); + Cost0 = 0; + Vec_IntForEachEntry( vInit, iPat, i ) + Cost0 += ((iPat >> 1) & 1); if ( fVerbose ) - printf( "Frame =%6d : Values =%6d (out of %6d)\n", 0, Gia_ManRegNum(p), Gia_ManRegNum(p) ); + printf( "Frame =%6d : Values =%6d (out of %6d)\n", 0, Cost0, Cost0 ); for ( f = 0; f < nFrames; f++ ) { clk = Abc_Clock(); Gia_ManForEachObj( p, pObj, i ) - Bmc_RoseSimulateObj( p, i ); - iPat = Bmc_RoseHighestScore( p, &Cost ); - Bmc_RoseFindStarting( p, vInit, iPat ); - Bmc_RoseSimulateInit( p, vInit ); + Gia_ManRoseSimulateObj( p, i ); + iPat = Gia_ManRoseHighestScore( p, &Cost ); + Gia_ManRoseFindStarting( p, vInit, iPat ); + Gia_ManRoseInit( p, vInit ); if ( fVerbose ) - printf( "Frame =%6d : Values =%6d (out of %6d) ", f+1, Cost, Gia_ManRegNum(p) ); + printf( "Frame =%6d : Values =%6d (out of %6d) ", f+1, Cost, Cost0 ); if ( fVerbose ) Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } @@ -455,6 +482,8 @@ Vec_Int_t * Bmc_RosePerform( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, int printf( "After %d frames, found a sequence to produce %d x-values (out of %d). ", f, Cost, Gia_ManRegNum(p) ); Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); // Vec_IntFreeP( &vInit ); + Vec_IntFill(vInit, Vec_IntSize(vInit), 2); +// printf( "The resulting init state is invalid.\n" ); return vInit; } @@ -469,30 +498,15 @@ Vec_Int_t * Bmc_RosePerform( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, int SeeAlso [] ***********************************************************************/ -void Bmc_RoseTest( Gia_Man_t * p, int nFrames, int nWords, int fVerbose ) -{ - Bmc_RosePerform( p, NULL, nFrames, nWords, fVerbose ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManTulipTest( Gia_Man_t * p, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose ) +Vec_Int_t * Gia_ManTulipTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose ) { Vec_Int_t * vRes; if ( fSim ) - vRes = Bmc_RosePerform( p, NULL, nFrames, nWords, fVerbose ); + vRes = Gia_ManRosePerform( p, vInit, nFrames, nWords, fVerbose ); else - vRes = Gia_ManTulip( p, nFrames, nTimeOut, fVerbose ); + vRes = Gia_ManTulipPerform( p, vInit, nFrames, nTimeOut, fVerbose ); Vec_IntFreeP( &vRes ); + return vRes; } -- cgit v1.2.3