summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/gia.h1
-rw-r--r--src/aig/gia/giaMan.c1
-rw-r--r--src/base/abci/abc.c97
-rw-r--r--src/sat/bmc/bmcTulip.c104
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 );
@@ -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:
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;
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-17 23:45:48 +0000