Skip to content

A
abc
Commit e34d41b3 by Alan Mishchenko
Options

Experiments with recent ideas.

parent ffa881bc
Showing with 155 additions and 46 deletions
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
......
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 );
......
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 );
......@@ -32747,6 +32749,98 @@ usage:
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 []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9CexCut( Abc_Frame_t * pAbc, int argc, char ** argv )
{
return -1;
......@@ -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:
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 )
{
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;
}
......
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