mirror of https://github.com/YosysHQ/abc.git
Experiments with recent ideas.
This commit is contained in:
Alan Mishchenko
parent
c1fa07db4d
commit
ffa881bce2
156
abclib.dsp
156
abclib.dsp
|
|
@ -729,10 +729,162 @@ SOURCE=.\src\base\test\test.c
|
|||
# Begin Group "abc2"
|
||||
|
||||
# PROP Default_Filter ""
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2_.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2_power.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2Blifi.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2Blifo.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2Core.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2Dup.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2Equiv.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2Extract.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2Flatten.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2Func.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2Fx.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2Gia.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2Hash.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2Insert.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2Logic.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2Map.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2Merge.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2Mfs.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2Multi.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2Ntk.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2Part.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2Print.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2Rec.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2Slack.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2Strash.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2Time.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2Truth.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2Util.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2Veri.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2Verify.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2\abc2Vero.c
|
||||
# End Source File
|
||||
# End Group
|
||||
# Begin Group "abc2d"
|
||||
|
||||
# PROP Default_Filter ""
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2d\abc2d.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2d\ast2.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2d\magic.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2d\magic.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\abc2d\util.c
|
||||
# End Source File
|
||||
# End Group
|
||||
# End Group
|
||||
# Begin Group "bdd"
|
||||
|
|
@ -1447,6 +1599,10 @@ SOURCE=.\src\sat\bmc\bmcICheck.c
|
|||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\sat\bmc\bmcLilac.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\sat\bmc\bmcLoad.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
|
|
|||
|
|
@ -34054,7 +34054,7 @@ 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 nTimeOut, int fVerbose );
|
||||
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,12 +34158,14 @@ 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, 0, fVerbose );
|
||||
Gia_ManTulipTest( pAbc->pGia, nFrames, nWords, 0, fSwitch, fVerbose );
|
||||
|
||||
return 0;
|
||||
usage:
|
||||
Abc_Print( -2, "usage: &test [-F num] [-svh]\n" );
|
||||
Abc_Print( -2, "usage: &test [-FW num] [-svh]\n" );
|
||||
Abc_Print( -2, "\t testing various procedures\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-s : toggle enable (yes) vs. disable (no) [default = %s]\n", fSwitch? "yes": "no" );
|
||||
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
|
||||
Abc_Print( -2, "\t-h : print the command usage\n");
|
||||
|
|
|
|||
|
|
@ -0,0 +1,70 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [bmcLilac.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [SAT-based bounded model checking.]
|
||||
|
||||
Synopsis []
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: bmcLilac.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "bmc.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Bmc_LilacPerform( Gia_Man_t * p, Vec_Int_t * vInitA, Vec_Int_t * vInitB, int nFrames, int fVerbose )
|
||||
{
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Bmc_LilacTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int fVerbose )
|
||||
{
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
|
|
@ -30,6 +30,10 @@ ABC_NAMESPACE_IMPL_START
|
|||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
static inline void Gia_ParTestAlloc( Gia_Man_t * p, int nWords ) { assert( !p->pData ); p->pData = (unsigned *)ABC_ALLOC(word, 2*nWords*Gia_ManObjNum(p)); p->iData = nWords; }
|
||||
static inline void Gia_ParTestFree( Gia_Man_t * p ) { ABC_FREE( p->pData ); p->iData = 0; }
|
||||
static inline word * Gia_ParTestObj( Gia_Man_t * p, int Id ) { return (word *)p->pData + Id*(p->iData << 1); }
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
@ -198,7 +202,7 @@ Vec_Int_t * Gia_ManTulip( Gia_Man_t * p, int nFrames, int nTimeOut, int fVerbose
|
|||
{
|
||||
// if ( fVerbose )
|
||||
// printf( "\n" );
|
||||
printf( "Reached fixed point with %d entries after %d iterations.\n", Vec_IntSize(vLits), Iter+1 );
|
||||
printf( "Reached fixed point with %d entries after %d iterations. ", Vec_IntSize(vLits), Iter+1 );
|
||||
break;
|
||||
}
|
||||
// collect used literals
|
||||
|
|
@ -227,6 +231,7 @@ Vec_Int_t * Gia_ManTulip( Gia_Man_t * p, int nFrames, int nTimeOut, int fVerbose
|
|||
return vLits;
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
|
@ -238,13 +243,259 @@ Vec_Int_t * Gia_ManTulip( Gia_Man_t * p, int nFrames, int nTimeOut, int fVerbose
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Gia_ManTulipTest( Gia_Man_t * p, int nFrames, int nTimeOut, int fVerbose )
|
||||
void Bmc_RoseSimulateInit( Gia_Man_t * p, Vec_Int_t * vInit )
|
||||
{
|
||||
Gia_Obj_t * pObj;
|
||||
word * pData1, * pData0;
|
||||
int i, k;
|
||||
Gia_ManForEachRi( p, pObj, k )
|
||||
{
|
||||
pData0 = Gia_ParTestObj( p, Gia_ObjId(p, pObj) );
|
||||
pData1 = pData0 + p->iData;
|
||||
if ( vInit == NULL ) // both X
|
||||
for ( i = 0; i < p->iData; i++ )
|
||||
pData0[i] = pData1[i] = 0;
|
||||
else if ( Vec_IntEntry(vInit, k) == 0 ) // 0
|
||||
for ( i = 0; i < p->iData; i++ )
|
||||
pData0[i] = ~(word)0, pData1[i] = 0;
|
||||
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 )
|
||||
for ( i = 0; i < p->iData; i++ )
|
||||
pData0[i] = pData1[i] = 0;
|
||||
}
|
||||
}
|
||||
void Bmc_RoseSimulateObj( Gia_Man_t * p, int Id )
|
||||
{
|
||||
Gia_Obj_t * pObj = Gia_ManObj( p, Id );
|
||||
word * pData0, * pDataA0, * pDataB0;
|
||||
word * pData1, * pDataA1, * pDataB1;
|
||||
int i;
|
||||
if ( Gia_ObjIsAnd(pObj) )
|
||||
{
|
||||
pData0 = Gia_ParTestObj( p, Id );
|
||||
pData1 = pData0 + p->iData;
|
||||
if ( Gia_ObjFaninC0(pObj) )
|
||||
{
|
||||
pDataA1 = Gia_ParTestObj( p, Gia_ObjFaninId0(pObj, Id) );
|
||||
pDataA0 = pDataA1 + p->iData;
|
||||
if ( Gia_ObjFaninC1(pObj) )
|
||||
{
|
||||
pDataB1 = Gia_ParTestObj( p, Gia_ObjFaninId1(pObj, Id) );
|
||||
pDataB0 = pDataB1 + p->iData;
|
||||
}
|
||||
else
|
||||
{
|
||||
pDataB0 = Gia_ParTestObj( p, Gia_ObjFaninId1(pObj, Id) );
|
||||
pDataB1 = pDataB0 + p->iData;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
pDataA0 = Gia_ParTestObj( p, Gia_ObjFaninId0(pObj, Id) );
|
||||
pDataA1 = pDataA0 + p->iData;
|
||||
if ( Gia_ObjFaninC1(pObj) )
|
||||
{
|
||||
pDataB1 = Gia_ParTestObj( p, Gia_ObjFaninId1(pObj, Id) );
|
||||
pDataB0 = pDataB1 + p->iData;
|
||||
}
|
||||
else
|
||||
{
|
||||
pDataB0 = Gia_ParTestObj( p, Gia_ObjFaninId1(pObj, Id) );
|
||||
pDataB1 = pDataB0 + p->iData;
|
||||
}
|
||||
}
|
||||
for ( i = 0; i < p->iData; i++ )
|
||||
pData0[i] = pDataA0[i] | pDataB0[i], pData1[i] = pDataA1[i] & pDataB1[i];
|
||||
}
|
||||
else if ( Gia_ObjIsCo(pObj) )
|
||||
{
|
||||
pData0 = Gia_ParTestObj( p, Id );
|
||||
pData1 = pData0 + p->iData;
|
||||
if ( Gia_ObjFaninC0(pObj) )
|
||||
{
|
||||
pDataA1 = Gia_ParTestObj( p, Gia_ObjFaninId0(pObj, Id) );
|
||||
pDataA0 = pDataA1 + p->iData;
|
||||
}
|
||||
else
|
||||
{
|
||||
pDataA0 = Gia_ParTestObj( p, Gia_ObjFaninId0(pObj, Id) );
|
||||
pDataA1 = pDataA0 + p->iData;
|
||||
}
|
||||
for ( i = 0; i < p->iData; i++ )
|
||||
pData0[i] = pDataA0[i], pData1[i] = pDataA1[i];
|
||||
}
|
||||
else if ( Gia_ObjIsCi(pObj) )
|
||||
{
|
||||
if ( Gia_ObjIsPi(p, pObj) )
|
||||
{
|
||||
pData0 = Gia_ParTestObj( p, Id );
|
||||
pData1 = pData0 + p->iData;
|
||||
for ( i = 0; i < p->iData; i++ )
|
||||
pData0[i] = Gia_ManRandomW(0), pData1[i] = ~pData0[i];
|
||||
}
|
||||
else
|
||||
{
|
||||
int Id2 = Gia_ObjId(p, Gia_ObjRoToRi(p, pObj));
|
||||
pData0 = Gia_ParTestObj( p, Id );
|
||||
pData1 = pData0 + p->iData;
|
||||
pDataA0 = Gia_ParTestObj( p, Id2 );
|
||||
pDataA1 = pDataA0 + p->iData;
|
||||
for ( i = 0; i < p->iData; i++ )
|
||||
pData0[i] = pDataA0[i], pData1[i] = pDataA1[i];
|
||||
}
|
||||
}
|
||||
else if ( Gia_ObjIsConst0(pObj) )
|
||||
{
|
||||
pData0 = Gia_ParTestObj( p, Id );
|
||||
pData1 = pData0 + p->iData;
|
||||
for ( i = 0; i < p->iData; i++ )
|
||||
pData0[i] = ~(word)0, pData1[i] = 0;
|
||||
}
|
||||
else assert( 0 );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Bmc_RoseHighestScore( Gia_Man_t * p, int * pCost )
|
||||
{
|
||||
Gia_Obj_t * pObj;
|
||||
word * pData0, * pData1;
|
||||
int * pCounts, CountBest;
|
||||
int i, k, b, nPats, iPat;
|
||||
nPats = 64 * p->iData;
|
||||
pCounts = ABC_CALLOC( int, nPats );
|
||||
Gia_ManForEachRi( p, pObj, k )
|
||||
{
|
||||
pData0 = Gia_ParTestObj( p, Gia_ObjId(p, pObj) );
|
||||
pData1 = pData0 + p->iData;
|
||||
for ( i = 0; i < p->iData; i++ )
|
||||
for ( b = 0; b < 64; b++ )
|
||||
pCounts[64*i+b] += (((pData0[i] >> b) & 1) || ((pData1[i] >> b) & 1)); // binary
|
||||
}
|
||||
iPat = 0;
|
||||
CountBest = pCounts[0];
|
||||
for ( k = 1; k < nPats; k++ )
|
||||
if ( CountBest < pCounts[k] )
|
||||
CountBest = pCounts[k], iPat = k;
|
||||
*pCost = Gia_ManRegNum(p) - CountBest; // ternary
|
||||
ABC_FREE( pCounts );
|
||||
return iPat;
|
||||
}
|
||||
void Bmc_RoseFindStarting( Gia_Man_t * p, Vec_Int_t * vInit, int iPat )
|
||||
{
|
||||
Gia_Obj_t * pObj;
|
||||
word * pData0, * pData1;
|
||||
int i, k;
|
||||
Vec_IntClear( vInit );
|
||||
Gia_ManForEachRi( p, pObj, k )
|
||||
{
|
||||
pData0 = Gia_ParTestObj( p, Gia_ObjId(p, pObj) );
|
||||
pData1 = pData0 + p->iData;
|
||||
for ( i = 0; i < p->iData; i++ )
|
||||
assert( (pData0[i] & pData1[i]) == 0 );
|
||||
if ( Abc_InfoHasBit( (unsigned *)pData0, iPat ) )
|
||||
Vec_IntPush( vInit, 0 );
|
||||
else if ( Abc_InfoHasBit( (unsigned *)pData1, iPat ) )
|
||||
Vec_IntPush( vInit, 1 );
|
||||
else
|
||||
Vec_IntPush( vInit, 2 );
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Int_t * Bmc_RosePerform( 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;
|
||||
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) );
|
||||
Gia_ParTestAlloc( p, nWords );
|
||||
Bmc_RoseSimulateInit( p, vInit0 );
|
||||
if ( fVerbose )
|
||||
printf( "Frame =%6d : Values =%6d (out of %6d)\n", 0, Gia_ManRegNum(p), Gia_ManRegNum(p) );
|
||||
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 );
|
||||
if ( fVerbose )
|
||||
printf( "Frame =%6d : Values =%6d (out of %6d) ", f+1, Cost, Gia_ManRegNum(p) );
|
||||
if ( fVerbose )
|
||||
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
|
||||
}
|
||||
Gia_ParTestFree( p );
|
||||
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 );
|
||||
return vInit;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
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 * vRes;
|
||||
vRes = Gia_ManTulip( p, nFrames, nTimeOut, fVerbose );
|
||||
Vec_IntFree( vRes );
|
||||
if ( fSim )
|
||||
vRes = Bmc_RosePerform( p, NULL, nFrames, nWords, fVerbose );
|
||||
else
|
||||
vRes = Gia_ManTulip( p, nFrames, nTimeOut, fVerbose );
|
||||
Vec_IntFreeP( &vRes );
|
||||
}
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -9,6 +9,7 @@ SRC += src/sat/bmc/bmcBmc.c \
|
|||
src/sat/bmc/bmcCexTools.c \
|
||||
src/sat/bmc/bmcFault.c \
|
||||
src/sat/bmc/bmcICheck.c \
|
||||
src/sat/bmc/bmcLilac.c \
|
||||
src/sat/bmc/bmcLoad.c \
|
||||
src/sat/bmc/bmcMulti.c \
|
||||
src/sat/bmc/bmcTulip.c \
|
||||
|
|
|
|||
Loading…
Reference in New Issue