From c86a13f0b56b061fd0841efd080758fc3b77c53e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 20 Mar 2014 20:18:25 -0700 Subject: Experiments with recent ideas. --- src/aig/gia/giaMan.c | 20 +- src/base/abci/abc.c | 131 ++++++++++-- src/sat/bmc/bmcBmci.c | 344 ++++++++++++++++++++++++++++++++ src/sat/bmc/bmcInse.c | 345 ++++++++++++++++++++++++++++++++ src/sat/bmc/bmcLilac.c | 344 -------------------------------- src/sat/bmc/bmcMaxi.c | 282 ++++++++++++++++++++++++++ src/sat/bmc/bmcTulip.c | 514 ------------------------------------------------ src/sat/bmc/module.make | 5 +- 8 files changed, 1102 insertions(+), 883 deletions(-) create mode 100644 src/sat/bmc/bmcBmci.c create mode 100644 src/sat/bmc/bmcInse.c delete mode 100644 src/sat/bmc/bmcLilac.c create mode 100644 src/sat/bmc/bmcMaxi.c delete mode 100644 src/sat/bmc/bmcTulip.c (limited to 'src') diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index d3ee3f48..36be9e49 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -305,12 +305,16 @@ void Gia_ManPrintTents( Gia_Man_t * p ) void Gia_ManPrintInitClasses( Vec_Int_t * vInits ) { int i, Value; - int Counts[4] = {0}; + int Counts[6] = {0}; Vec_IntForEachEntry( vInits, Value, i ) Counts[Value]++; - for ( i = 0; i < 4; i++ ) - printf( "%d = %d ", i, Counts[i] ); - printf( "X = %d\n", Counts[2] + Counts[3] ); + for ( i = 0; i < 6; i++ ) + if ( Counts[i] ) + printf( "%d = %d ", i, Counts[i] ); + printf( " " ); + printf( "B = %d ", Counts[0] + Counts[1] ); + printf( "X = %d ", Counts[2] + Counts[3] ); + printf( "Q = %d\n", Counts[4] + Counts[5] ); Vec_IntForEachEntry( vInits, Value, i ) { Counts[Value]++; @@ -319,9 +323,13 @@ void Gia_ManPrintInitClasses( Vec_Int_t * vInits ) else if ( Value == 1 ) printf( "1" ); else if ( Value == 2 ) - printf( "x" ); + printf( "2" ); else if ( Value == 3 ) - printf( "X" ); + printf( "3" ); + else if ( Value == 4 ) + printf( "4" ); + else if ( Value == 5 ) + printf( "5" ); else assert( 0 ); } printf( "\n" ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 9138d212..05200336 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -399,8 +399,9 @@ 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_CommandAbc9Lilac ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Inse ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Maxi ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Bmci ( 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 ); @@ -964,8 +965,9 @@ 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", "&lilac", Abc_CommandAbc9Lilac, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&inse", Abc_CommandAbc9Inse, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&maxi", Abc_CommandAbc9Maxi, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&bmci", Abc_CommandAbc9Bmci, 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 ); @@ -32751,9 +32753,104 @@ usage: SeeAlso [] ***********************************************************************/ -int Abc_CommandAbc9Tulip( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandAbc9Inse( 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 ); + extern Vec_Int_t * Gia_ManInseTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose ); + int c, nFrames = 10, 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_CommandAbc9Inse(): There is no AIG.\n" ); + return 0; + } + if ( Gia_ManRegNum(pAbc->pGia) == 0 ) + { + Abc_Print( -1, "Abc_CommandAbc9Inse(): AIG is combinational.\n" ); + return 0; + } + if ( pAbc->pGia->vInitClasses != NULL ) + { + Abc_Print( 1, "Abc_CommandAbc9Inse(): All-0 initial state is assumed.\n" ); + Vec_IntFreeP( &pAbc->pGia->vInitClasses ); + } + pAbc->pGia->vInitClasses = Gia_ManInseTest( pAbc->pGia, NULL, nFrames, nWords, nTimeOut, fSim, fVerbose ); + return 0; + +usage: + Abc_Print( -2, "usage: &inse [-FWT num] [-svh]\n" ); + Abc_Print( -2, "\t experimental procedure\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_CommandAbc9Maxi( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Vec_Int_t * Gia_ManMaxiTest( 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(); @@ -32808,20 +32905,20 @@ int Abc_CommandAbc9Tulip( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( pAbc->pGia == NULL ) { - Abc_Print( -1, "Abc_CommandAbc9Tulip(): There is no AIG.\n" ); + Abc_Print( -1, "Abc_CommandAbc9Maxi(): There is no AIG.\n" ); return 0; } if ( Gia_ManRegNum(pAbc->pGia) == 0 ) { - Abc_Print( -1, "Abc_CommandAbc9Tulip(): AIG is combinational.\n" ); + Abc_Print( -1, "Abc_CommandAbc9Maxi(): AIG is combinational.\n" ); return 0; } - pAbc->pGia->vInitClasses = Gia_ManTulipTest( pAbc->pGia, vTemp = pAbc->pGia->vInitClasses, nFrames, nWords, nTimeOut, fSim, fVerbose ); + pAbc->pGia->vInitClasses = Gia_ManMaxiTest( pAbc->pGia, vTemp = pAbc->pGia->vInitClasses, nFrames, nWords, nTimeOut, fSim, fVerbose ); Vec_IntFreeP( &vTemp ); return 0; usage: - Abc_Print( -2, "usage: &tulip [-FWT num] [-svh]\n" ); + Abc_Print( -2, "usage: &maxi [-FWT num] [-svh]\n" ); Abc_Print( -2, "\t experimental procedure\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 ); @@ -32843,9 +32940,9 @@ usage: SeeAlso [] ***********************************************************************/ -int Abc_CommandAbc9Lilac( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandAbc9Bmci( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern int Gia_ManLilacTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose ); + extern int Gia_ManBmciTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose ); int c, nFrames = 1000, nWords = 1000, nTimeOut = 0, fSim = 0, fVerbose = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "FWTsvh" ) ) != EOF ) @@ -32899,24 +32996,24 @@ int Abc_CommandAbc9Lilac( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( pAbc->pGia == NULL ) { - Abc_Print( -1, "Abc_CommandAbc9Lilac(): There is no AIG.\n" ); + Abc_Print( -1, "Abc_CommandAbc9Bmci(): There is no AIG.\n" ); return 0; } if ( Gia_ManRegNum(pAbc->pGia) == 0 ) { - Abc_Print( -1, "Abc_CommandAbc9Lilac(): AIG is combinational.\n" ); + Abc_Print( -1, "Abc_CommandAbc9Bmci(): AIG is combinational.\n" ); return 0; } if ( pAbc->pGia->vInitClasses == NULL ) { - Abc_Print( -1, "Abc_CommandAbc9Lilac(): Init array is not given.\n" ); + Abc_Print( -1, "Abc_CommandAbc9Bmci(): Init array is not given.\n" ); return 0; } - Gia_ManLilacTest( pAbc->pGia, pAbc->pGia->vInitClasses, nFrames, nWords, nTimeOut, fSim, fVerbose ); + Gia_ManBmciTest( pAbc->pGia, pAbc->pGia->vInitClasses, nFrames, nWords, nTimeOut, fSim, fVerbose ); return 0; usage: - Abc_Print( -2, "usage: &lilac [-FWT num] [-svh]\n" ); + Abc_Print( -2, "usage: &bmci [-FWT num] [-svh]\n" ); Abc_Print( -2, "\t experimental procedure\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 ); diff --git a/src/sat/bmc/bmcBmci.c b/src/sat/bmc/bmcBmci.c new file mode 100644 index 00000000..ff0fb393 --- /dev/null +++ b/src/sat/bmc/bmcBmci.c @@ -0,0 +1,344 @@ +/**CFile**************************************************************** + + FileName [bmcBmci.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: bmcBmci.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "bmc.h" +#include "sat/cnf/cnf.h" +#include "sat/bsat/satStore.h" +#include "aig/gia/giaAig.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p ) +{ + Cnf_Dat_t * pCnf; + Aig_Man_t * pAig = Gia_ManToAigSimple( p ); + pAig->nRegs = 0; + pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) ); + Aig_ManStop( pAig ); + return pCnf; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Cnf_DataLiftGia( Cnf_Dat_t * p, Gia_Man_t * pGia, int nVarsPlus ) +{ + Gia_Obj_t * pObj; + int v; + Gia_ManForEachObj( pGia, pObj, v ) + if ( p->pVarNums[Gia_ObjId(pGia, pObj)] >= 0 ) + p->pVarNums[Gia_ObjId(pGia, pObj)] += nVarsPlus; + for ( v = 0; v < p->nLiterals; v++ ) + p->pClauses[0][v] += 2*nVarsPlus; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bmc_BmciUnfold( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vFFLits, int fPiReuse ) +{ + Gia_Obj_t * pObj; + int i; + assert( Gia_ManRegNum(p) == Vec_IntSize(vFFLits) ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachRo( p, pObj, i ) + pObj->Value = Vec_IntEntry(vFFLits, i); + Gia_ManForEachPi( p, pObj, i ) + pObj->Value = fPiReuse ? Gia_ObjToLit(pNew, Gia_ManPi(pNew, Gia_ManPiNum(pNew)-Gia_ManPiNum(p)+i)) : Gia_ManAppendCi(pNew); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachRi( p, pObj, i ) + Vec_IntWriteEntry( vFFLits, i, Gia_ObjFanin0Copy(pObj) ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Bmc_BmciPart_rec( Gia_Man_t * pNew, Vec_Int_t * vSatMap, int iIdNew, Gia_Man_t * pPart, Vec_Int_t * vPartMap, Vec_Int_t * vCopies ) +{ + Gia_Obj_t * pObj = Gia_ManObj( pNew, iIdNew ); + int iLitPart0, iLitPart1, iRes; + if ( Vec_IntEntry(vCopies, iIdNew) ) + return Vec_IntEntry(vCopies, iIdNew); + if ( Vec_IntEntry(vSatMap, iIdNew) >= 0 || Gia_ObjIsCi(pObj) ) + { + Vec_IntPush( vPartMap, iIdNew ); + iRes = Gia_ManAppendCi(pPart); + Vec_IntWriteEntry( vCopies, iIdNew, iRes ); + return iRes; + } + assert( Gia_ObjIsAnd(pObj) ); + iLitPart0 = Bmc_BmciPart_rec( pNew, vSatMap, Gia_ObjFaninId0(pObj, iIdNew), pPart, vPartMap, vCopies ); + iLitPart1 = Bmc_BmciPart_rec( pNew, vSatMap, Gia_ObjFaninId1(pObj, iIdNew), pPart, vPartMap, vCopies ); + iLitPart0 = Abc_LitNotCond( iLitPart0, Gia_ObjFaninC0(pObj) ); + iLitPart1 = Abc_LitNotCond( iLitPart1, Gia_ObjFaninC1(pObj) ); + Vec_IntPush( vPartMap, iIdNew ); + iRes = Gia_ManAppendAnd( pPart, iLitPart0, iLitPart1 ); + Vec_IntWriteEntry( vCopies, iIdNew, iRes ); + return iRes; +} +Gia_Man_t * Bmc_BmciPart( Gia_Man_t * pNew, Vec_Int_t * vSatMap, Vec_Int_t * vMiters, Vec_Int_t * vPartMap, Vec_Int_t * vCopies ) +{ + Gia_Man_t * pPart; + int i, iLit, iLitPart; + Vec_IntFill( vCopies, Gia_ManObjNum(pNew), 0 ); + Vec_IntFillExtra( vSatMap, Gia_ManObjNum(pNew), -1 ); + pPart = Gia_ManStart( 1000 ); + pPart->pName = Abc_UtilStrsav( pNew->pName ); + Vec_IntClear( vPartMap ); + Vec_IntPush( vPartMap, 0 ); + Vec_IntForEachEntry( vMiters, iLit, i ) + { + if ( iLit == -1 ) + continue; + assert( iLit >= 2 ); + iLitPart = Bmc_BmciPart_rec( pNew, vSatMap, Abc_Lit2Var(iLit), pPart, vPartMap, vCopies ); + Gia_ManAppendCo( pPart, Abc_LitNotCond(iLitPart, Abc_LitIsCompl(iLit)) ); + Vec_IntPush( vPartMap, -1 ); + } + assert( Gia_ManPoNum(pPart) > 0 ); + assert( Vec_IntSize(vPartMap) == Gia_ManObjNum(pPart) ); + return pPart; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Bmc_BmciPerform( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInit1, int nFrames, int nWords, int nTimeOut, int fVerbose ) +{ + int nSatVars = 1; + Vec_Int_t * vLits0, * vLits1, * vMiters, * vSatMap, * vPartMap, * vCopies; + Gia_Man_t * pNew, * pPart; + Gia_Obj_t * pObj; + Cnf_Dat_t * pCnf; + sat_solver * pSat; + int iVar0, iVar1, iLit, iLit0, iLit1; + int i, f, status, nChanges, nMiters, RetValue = 1; + assert( Vec_IntSize(vInit0) == Gia_ManRegNum(p) ); + assert( Vec_IntSize(vInit1) == Gia_ManRegNum(p) ); + + // start the SAT solver + pSat = sat_solver_new(); + sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 ); + + pNew = Gia_ManStart( 10000 ); + pNew->pName = Abc_UtilStrsav( p->pName ); + Gia_ManHashAlloc( pNew ); + Gia_ManConst0(p)->Value = 0; + + vLits0 = Vec_IntAlloc( Gia_ManRegNum(p) ); + Vec_IntForEachEntry( vInit0, iLit, i ) + Vec_IntPush( vLits0, iLit < 2 ? iLit : Gia_ManAppendCi(pNew) ); + + vLits1 = Vec_IntAlloc( Gia_ManRegNum(p) ); + Vec_IntForEachEntry( vInit1, iLit, i ) + Vec_IntPush( vLits1, iLit < 2 ? iLit : Gia_ManAppendCi(pNew) ); + + vMiters = Vec_IntAlloc( 1000 ); + vSatMap = Vec_IntAlloc( 1000 ); + vPartMap = Vec_IntAlloc( 1000 ); + vCopies = Vec_IntAlloc( 1000 ); + for ( f = 0; f < nFrames; f++ ) + { + abctime clk = Abc_Clock(); + Bmc_BmciUnfold( pNew, p, vLits0, 0 ); + Bmc_BmciUnfold( pNew, p, vLits1, 1 ); + assert( Vec_IntSize(vLits0) == Vec_IntSize(vLits1) ); + nMiters = 0; + Vec_IntClear( vMiters ); + Vec_IntForEachEntryTwo( vLits0, vLits1, iLit0, iLit1, i ) + if ( (iLit0 >= 2 || iLit1 >= 2) && iLit0 != iLit1 ) + Vec_IntPush( vMiters, Gia_ManHashXor(pNew, iLit0, iLit1) ), nMiters++; + else + Vec_IntPush( vMiters, -1 ); + assert( Vec_IntSize(vMiters) == Gia_ManRegNum(p) ); + if ( Vec_IntSum(vMiters) + Vec_IntSize(vLits1) == 0 ) + { + if ( fVerbose ) + printf( "Reached a fixed point after %d frames. \n", f+1 ); + break; + } + // create new part + pPart = Bmc_BmciPart( pNew, vSatMap, vMiters, vPartMap, vCopies ); + pCnf = Cnf_DeriveGiaRemapped( pPart ); + Cnf_DataLiftGia( pCnf, pPart, nSatVars ); + nSatVars += pCnf->nVars; + sat_solver_setnvars( pSat, nSatVars ); + for ( i = 0; i < pCnf->nClauses; i++ ) + if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) + assert( 0 ); + // stitch the clauses + Gia_ManForEachPi( pPart, pObj, i ) + { + iVar0 = pCnf->pVarNums[Gia_ObjId(pPart, pObj)]; + iVar1 = Vec_IntEntry( vSatMap, Vec_IntEntry(vPartMap, Gia_ObjId(pPart, pObj)) ); + if ( iVar1 == -1 ) + continue; + sat_solver_add_buffer( pSat, iVar0, iVar1, 0 ); + } + // transfer variables + Gia_ManForEachCand( pPart, pObj, i ) + if ( pCnf->pVarNums[i] >= 0 ) + { + assert( Gia_ObjIsCi(pObj) || Vec_IntEntry( vSatMap, Vec_IntEntry(vPartMap, i) ) == -1 ); + Vec_IntWriteEntry( vSatMap, Vec_IntEntry(vPartMap, i), pCnf->pVarNums[i] ); + } + Cnf_DataFree( pCnf ); + Gia_ManStop( pPart ); + // perform runs + nChanges = 0; + Vec_IntForEachEntry( vMiters, iLit, i ) + { + if ( iLit == -1 ) + continue; + assert( Vec_IntEntry(vSatMap, Abc_Lit2Var(iLit)) > 0 ); + iLit = Abc_Lit2LitV( Vec_IntArray(vSatMap), iLit ); + status = sat_solver_solve( pSat, &iLit, &iLit + 1, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + if ( status == l_True ) + { + nChanges++; + continue; + } + if ( status == l_Undef ) + { + printf( "Timeout reached after %d seconds. \n", nTimeOut ); + RetValue = 0; + goto cleanup; + } + assert( status == l_False ); + iLit0 = Vec_IntEntry( vLits0, i ); + iLit1 = Vec_IntEntry( vLits1, i ); + assert( (iLit0 >= 2 || iLit1 >= 2) && iLit0 != iLit1 ); + if ( iLit1 >= 2 ) + Vec_IntWriteEntry( vLits1, i, iLit0 ); + else + Vec_IntWriteEntry( vLits0, i, iLit1 ); + iLit0 = Vec_IntEntry( vLits0, i ); + iLit1 = Vec_IntEntry( vLits1, i ); + assert( iLit0 == iLit1 ); + } + if ( fVerbose ) + { + printf( "Frame %4d : ", f+1 ); + printf( "Vars =%7d ", nSatVars ); + printf( "Clause =%10d ", sat_solver_nclauses(pSat) ); + printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) ); + printf( "AIG =%7d ", Gia_ManAndNum(pNew) ); + printf( "Miters =%5d ", nMiters ); + printf( "SAT =%5d ", nChanges ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + } + if ( nChanges == 0 ) + { + printf( "Reached a fixed point after %d frames. \n", f+1 ); + break; + } + } +cleanup: + + sat_solver_delete( pSat ); + Gia_ManStopP( &pNew ); + Vec_IntFree( vLits0 ); + Vec_IntFree( vLits1 ); + Vec_IntFree( vMiters ); + Vec_IntFree( vSatMap ); + Vec_IntFree( vPartMap ); + Vec_IntFree( vCopies ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManBmciTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose ) +{ + Vec_Int_t * vInit0 = Vec_IntStart( Gia_ManRegNum(p) ); + Bmc_BmciPerform( p, vInit, vInit0, nFrames, nWords, nTimeOut, fVerbose ); + Vec_IntFree( vInit0 ); + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bmc/bmcInse.c b/src/sat/bmc/bmcInse.c new file mode 100644 index 00000000..00cd3df3 --- /dev/null +++ b/src/sat/bmc/bmcInse.c @@ -0,0 +1,345 @@ +/**CFile**************************************************************** + + FileName [bmcInse.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: bmcInse.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "bmc.h" +#include "sat/cnf/cnf.h" +#include "sat/bsat/satStore.h" +#include "aig/gia/giaAig.h" + +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 /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManInseInit( 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 ( 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) > 1 ) // X + for ( i = 0; i < p->iData; i++ ) + pData0[i] = pData1[i] = 0; + } +} +void Gia_ManInseSimulateObj( 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 Gia_ManInseHighestScore( 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 Gia_ManInseFindStarting( Gia_Man_t * p, int iPat, Vec_Int_t * vInit, Vec_Int_t * vInputs ) +{ + 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 ); + } + Gia_ManForEachPi( 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( vInputs, 0 ); + else if ( Abc_InfoHasBit( (unsigned *)pData1, iPat ) ) + Vec_IntPush( vInputs, 1 ); + else + Vec_IntPush( vInputs, 2 ); + } +} +Vec_Int_t * Gia_ManInseSimulate( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInputs, Vec_Int_t * vInit ) +{ + Vec_Int_t * vRes; + Gia_Obj_t * pObj, * pObjRo, * pObjRi; + int nFrames = Vec_IntSize(vInputs) / Gia_ManPiNum(p); + int i, f, iBit = 0; + assert( Vec_IntSize(vInputs) % Gia_ManPiNum(p) == 0 ); + assert( Vec_IntSize(vInit0) == Gia_ManRegNum(p) ); + assert( Vec_IntSize(vInit) == Gia_ManRegNum(p) ); + Gia_ManConst0(p)->fMark0 = 0; + Gia_ManForEachRi( p, pObj, i ) + pObj->fMark0 = Vec_IntEntry(vInit0, i); + for ( f = 0; f < nFrames; f++ ) + { + Gia_ManForEachPi( p, pObj, i ) + pObj->fMark0 = Vec_IntEntry(vInputs, iBit++); + Gia_ManForEachAnd( p, pObj, i ) + pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & + (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); + Gia_ManForEachRi( p, pObj, i ) + pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); + Gia_ManForEachRiRo( p, pObjRi, pObjRo, i ) + pObjRo->fMark0 = pObjRi->fMark0; + } + assert( iBit == Vec_IntSize(vInputs) ); + vRes = Vec_IntAlloc( Gia_ManRegNum(p) ); + Gia_ManForEachRo( p, pObj, i ) + assert( Vec_IntEntry(vInit, i) == 2 || Vec_IntEntry(vInit, i) == (int)pObj->fMark0 ); + Gia_ManForEachRo( p, pObj, i ) + Vec_IntPush( vRes, pObj->fMark0 | (Vec_IntEntry(vInit, i) != 2 ? 4 : 0) ); + Gia_ManForEachObj( p, pObj, i ) + pObj->fMark0 = 0; + return vRes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManInsePerform( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, int nWords, int fVerbose ) +{ + Vec_Int_t * vRes, * vInit, * vInputs; + Gia_Obj_t * pObj; + 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(0); Vec_IntFill( vInit, Gia_ManRegNum(p), 2 ); + vInputs = Vec_IntStart( Gia_ManPiNum(p) * nFrames ); + Gia_ParTestAlloc( p, nWords ); + Gia_ManInseInit( 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, Cost0, Cost0 ); + for ( f = 0; f < nFrames; f++ ) + { + clk = Abc_Clock(); + Gia_ManForEachObj( p, pObj, i ) + Gia_ManInseSimulateObj( p, i ); + iPat = Gia_ManInseHighestScore( p, &Cost ); + Gia_ManInseFindStarting( p, iPat, vInit, vInputs ); + Gia_ManInseInit( p, vInit ); + if ( fVerbose ) + printf( "Frame =%6d : Values =%6d (out of %6d) ", f+1, Cost, Cost0 ); + if ( fVerbose ) + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + } + Gia_ParTestFree( p ); + vRes = Gia_ManInseSimulate( p, vInit0, vInputs, vInit ); + Vec_IntFreeP( &vInit ); + Vec_IntFreeP( &vInputs ); + 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 ); + return vRes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManInseTest( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose ) +{ + Vec_Int_t * vRes, * vInit; + vInit = Vec_IntAlloc(0); Vec_IntFill( vInit, Gia_ManRegNum(p), 0 ); + vRes = Gia_ManInsePerform( p, vInit, nFrames, nWords, fVerbose ); + if ( vInit != vInit0 ) + Vec_IntFree( vInit ); + return vRes; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bmc/bmcLilac.c b/src/sat/bmc/bmcLilac.c deleted file mode 100644 index f09d0b66..00000000 --- a/src/sat/bmc/bmcLilac.c +++ /dev/null @@ -1,344 +0,0 @@ -/**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" -#include "sat/cnf/cnf.h" -#include "sat/bsat/satStore.h" -#include "aig/gia/giaAig.h" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p ) -{ - Cnf_Dat_t * pCnf; - Aig_Man_t * pAig = Gia_ManToAigSimple( p ); - pAig->nRegs = 0; - pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) ); - Aig_ManStop( pAig ); - return pCnf; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Cnf_DataLiftGia( Cnf_Dat_t * p, Gia_Man_t * pGia, int nVarsPlus ) -{ - Gia_Obj_t * pObj; - int v; - Gia_ManForEachObj( pGia, pObj, v ) - if ( p->pVarNums[Gia_ObjId(pGia, pObj)] >= 0 ) - p->pVarNums[Gia_ObjId(pGia, pObj)] += nVarsPlus; - for ( v = 0; v < p->nLiterals; v++ ) - p->pClauses[0][v] += 2*nVarsPlus; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Bmc_LilacUnfold( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vFFLits, int fPiReuse ) -{ - Gia_Obj_t * pObj; - int i; - assert( Gia_ManRegNum(p) == Vec_IntSize(vFFLits) ); - Gia_ManConst0(p)->Value = 0; - Gia_ManForEachRo( p, pObj, i ) - pObj->Value = Vec_IntEntry(vFFLits, i); - Gia_ManForEachPi( p, pObj, i ) - pObj->Value = fPiReuse ? Gia_ObjToLit(pNew, Gia_ManPi(pNew, Gia_ManPiNum(pNew)-Gia_ManPiNum(p)+i)) : Gia_ManAppendCi(pNew); - Gia_ManForEachAnd( p, pObj, i ) - pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - Gia_ManForEachRi( p, pObj, i ) - Vec_IntWriteEntry( vFFLits, i, Gia_ObjFanin0Copy(pObj) ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Bmc_LilacPart_rec( Gia_Man_t * pNew, Vec_Int_t * vSatMap, int iIdNew, Gia_Man_t * pPart, Vec_Int_t * vPartMap, Vec_Int_t * vCopies ) -{ - Gia_Obj_t * pObj = Gia_ManObj( pNew, iIdNew ); - int iLitPart0, iLitPart1, iRes; - if ( Vec_IntEntry(vCopies, iIdNew) ) - return Vec_IntEntry(vCopies, iIdNew); - if ( Vec_IntEntry(vSatMap, iIdNew) >= 0 || Gia_ObjIsCi(pObj) ) - { - Vec_IntPush( vPartMap, iIdNew ); - iRes = Gia_ManAppendCi(pPart); - Vec_IntWriteEntry( vCopies, iIdNew, iRes ); - return iRes; - } - assert( Gia_ObjIsAnd(pObj) ); - iLitPart0 = Bmc_LilacPart_rec( pNew, vSatMap, Gia_ObjFaninId0(pObj, iIdNew), pPart, vPartMap, vCopies ); - iLitPart1 = Bmc_LilacPart_rec( pNew, vSatMap, Gia_ObjFaninId1(pObj, iIdNew), pPart, vPartMap, vCopies ); - iLitPart0 = Abc_LitNotCond( iLitPart0, Gia_ObjFaninC0(pObj) ); - iLitPart1 = Abc_LitNotCond( iLitPart1, Gia_ObjFaninC1(pObj) ); - Vec_IntPush( vPartMap, iIdNew ); - iRes = Gia_ManAppendAnd( pPart, iLitPart0, iLitPart1 ); - Vec_IntWriteEntry( vCopies, iIdNew, iRes ); - return iRes; -} -Gia_Man_t * Bmc_LilacPart( Gia_Man_t * pNew, Vec_Int_t * vSatMap, Vec_Int_t * vMiters, Vec_Int_t * vPartMap, Vec_Int_t * vCopies ) -{ - Gia_Man_t * pPart; - int i, iLit, iLitPart; - Vec_IntFill( vCopies, Gia_ManObjNum(pNew), 0 ); - Vec_IntFillExtra( vSatMap, Gia_ManObjNum(pNew), -1 ); - pPart = Gia_ManStart( 1000 ); - pPart->pName = Abc_UtilStrsav( pNew->pName ); - Vec_IntClear( vPartMap ); - Vec_IntPush( vPartMap, 0 ); - Vec_IntForEachEntry( vMiters, iLit, i ) - { - if ( iLit == -1 ) - continue; - assert( iLit >= 2 ); - iLitPart = Bmc_LilacPart_rec( pNew, vSatMap, Abc_Lit2Var(iLit), pPart, vPartMap, vCopies ); - Gia_ManAppendCo( pPart, Abc_LitNotCond(iLitPart, Abc_LitIsCompl(iLit)) ); - Vec_IntPush( vPartMap, -1 ); - } - assert( Gia_ManPoNum(pPart) > 0 ); - assert( Vec_IntSize(vPartMap) == Gia_ManObjNum(pPart) ); - return pPart; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Bmc_LilacPerform( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInit1, int nFrames, int nWords, int nTimeOut, int fVerbose ) -{ - int nSatVars = 1; - Vec_Int_t * vLits0, * vLits1, * vMiters, * vSatMap, * vPartMap, * vCopies; - Gia_Man_t * pNew, * pPart; - Gia_Obj_t * pObj; - Cnf_Dat_t * pCnf; - sat_solver * pSat; - int iVar0, iVar1, iLit, iLit0, iLit1; - int i, f, status, nChanges, nMiters, RetValue = 1; - assert( Vec_IntSize(vInit0) == Gia_ManRegNum(p) ); - assert( Vec_IntSize(vInit1) == Gia_ManRegNum(p) ); - - // start the SAT solver - pSat = sat_solver_new(); - sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 ); - - pNew = Gia_ManStart( 10000 ); - pNew->pName = Abc_UtilStrsav( p->pName ); - Gia_ManHashAlloc( pNew ); - Gia_ManConst0(p)->Value = 0; - - vLits0 = Vec_IntAlloc( Gia_ManRegNum(p) ); - Vec_IntForEachEntry( vInit0, iLit, i ) - Vec_IntPush( vLits0, iLit < 2 ? iLit : Gia_ManAppendCi(pNew) ); - - vLits1 = Vec_IntAlloc( Gia_ManRegNum(p) ); - Vec_IntForEachEntry( vInit1, iLit, i ) - Vec_IntPush( vLits1, iLit < 2 ? iLit : Gia_ManAppendCi(pNew) ); - - vMiters = Vec_IntAlloc( 1000 ); - vSatMap = Vec_IntAlloc( 1000 ); - vPartMap = Vec_IntAlloc( 1000 ); - vCopies = Vec_IntAlloc( 1000 ); - for ( f = 0; f < nFrames; f++ ) - { - abctime clk = Abc_Clock(); - Bmc_LilacUnfold( pNew, p, vLits0, 0 ); - Bmc_LilacUnfold( pNew, p, vLits1, 1 ); - assert( Vec_IntSize(vLits0) == Vec_IntSize(vLits1) ); - nMiters = 0; - Vec_IntClear( vMiters ); - Vec_IntForEachEntryTwo( vLits0, vLits1, iLit0, iLit1, i ) - if ( (iLit0 >= 2 || iLit1 >= 2) && iLit0 != iLit1 ) - Vec_IntPush( vMiters, Gia_ManHashXor(pNew, iLit0, iLit1) ), nMiters++; - else - Vec_IntPush( vMiters, -1 ); - assert( Vec_IntSize(vMiters) == Gia_ManRegNum(p) ); - if ( Vec_IntSum(vMiters) + Vec_IntSize(vLits1) == 0 ) - { - if ( fVerbose ) - printf( "Reached a fixed point after %d frames. \n", f+1 ); - break; - } - // create new part - pPart = Bmc_LilacPart( pNew, vSatMap, vMiters, vPartMap, vCopies ); - pCnf = Cnf_DeriveGiaRemapped( pPart ); - Cnf_DataLiftGia( pCnf, pPart, nSatVars ); - nSatVars += pCnf->nVars; - sat_solver_setnvars( pSat, nSatVars ); - for ( i = 0; i < pCnf->nClauses; i++ ) - if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) - assert( 0 ); - // stitch the clauses - Gia_ManForEachPi( pPart, pObj, i ) - { - iVar0 = pCnf->pVarNums[Gia_ObjId(pPart, pObj)]; - iVar1 = Vec_IntEntry( vSatMap, Vec_IntEntry(vPartMap, Gia_ObjId(pPart, pObj)) ); - if ( iVar1 == -1 ) - continue; - sat_solver_add_buffer( pSat, iVar0, iVar1, 0 ); - } - // transfer variables - Gia_ManForEachCand( pPart, pObj, i ) - if ( pCnf->pVarNums[i] >= 0 ) - { - assert( Gia_ObjIsCi(pObj) || Vec_IntEntry( vSatMap, Vec_IntEntry(vPartMap, i) ) == -1 ); - Vec_IntWriteEntry( vSatMap, Vec_IntEntry(vPartMap, i), pCnf->pVarNums[i] ); - } - Cnf_DataFree( pCnf ); - Gia_ManStop( pPart ); - // perform runs - nChanges = 0; - Vec_IntForEachEntry( vMiters, iLit, i ) - { - if ( iLit == -1 ) - continue; - assert( Vec_IntEntry(vSatMap, Abc_Lit2Var(iLit)) > 0 ); - iLit = Abc_Lit2LitV( Vec_IntArray(vSatMap), iLit ); - status = sat_solver_solve( pSat, &iLit, &iLit + 1, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); - if ( status == l_True ) - { - nChanges++; - continue; - } - if ( status == l_Undef ) - { - printf( "Timeout reached after %d seconds. \n", nTimeOut ); - RetValue = 0; - goto cleanup; - } - assert( status == l_False ); - iLit0 = Vec_IntEntry( vLits0, i ); - iLit1 = Vec_IntEntry( vLits1, i ); - assert( (iLit0 >= 2 || iLit1 >= 2) && iLit0 != iLit1 ); - if ( iLit1 >= 2 ) - Vec_IntWriteEntry( vLits1, i, iLit0 ); - else - Vec_IntWriteEntry( vLits0, i, iLit1 ); - iLit0 = Vec_IntEntry( vLits0, i ); - iLit1 = Vec_IntEntry( vLits1, i ); - assert( iLit0 == iLit1 ); - } - if ( fVerbose ) - { - printf( "Frame %4d : ", f+1 ); - printf( "Vars =%7d ", nSatVars ); - printf( "Clause =%10d ", sat_solver_nclauses(pSat) ); - printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) ); - printf( "AIG =%7d ", Gia_ManAndNum(pNew) ); - printf( "Miters =%5d ", nMiters ); - printf( "SAT =%5d ", nChanges ); - Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); - } - if ( nChanges == 0 ) - { - printf( "Reached a fixed point after %d frames. \n", f+1 ); - break; - } - } -cleanup: - - sat_solver_delete( pSat ); - Gia_ManStopP( &pNew ); - Vec_IntFree( vLits0 ); - Vec_IntFree( vLits1 ); - Vec_IntFree( vMiters ); - Vec_IntFree( vSatMap ); - Vec_IntFree( vPartMap ); - Vec_IntFree( vCopies ); - return RetValue; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ManLilacTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose ) -{ - Vec_Int_t * vInit0 = Vec_IntStart( Gia_ManRegNum(p) ); - Bmc_LilacPerform( p, vInit, vInit0, nFrames, nWords, nTimeOut, fVerbose ); - Vec_IntFree( vInit0 ); - return 1; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - diff --git a/src/sat/bmc/bmcMaxi.c b/src/sat/bmc/bmcMaxi.c new file mode 100644 index 00000000..4a088016 --- /dev/null +++ b/src/sat/bmc/bmcMaxi.c @@ -0,0 +1,282 @@ +/**CFile**************************************************************** + + FileName [bmcMaxi.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: bmcMaxi.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "bmc.h" +#include "sat/cnf/cnf.h" +#include "sat/bsat/satStore.h" +#include "aig/gia/giaAig.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p ) +{ + Cnf_Dat_t * pCnf; + Aig_Man_t * pAig = Gia_ManToAigSimple( p ); + pAig->nRegs = 0; + pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) ); + Aig_ManStop( pAig ); + return pCnf; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManMaxiUnfold( Gia_Man_t * p, int nFrames, int fUseVars, Vec_Int_t * vInit ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i, f; + pNew = Gia_ManStart( fUseVars * 2 * Gia_ManRegNum(p) + nFrames * Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + Gia_ManHashAlloc( pNew ); + Gia_ManConst0(p)->Value = 0; + // control/data variables + Gia_ManForEachRo( p, pObj, i ) + Gia_ManAppendCi( pNew ); + Gia_ManForEachRo( p, pObj, i ) + Gia_ManAppendCi( pNew ); + // build timeframes + assert( !vInit || Vec_IntSize(vInit) == Gia_ManRegNum(p) ); + Gia_ManForEachRo( p, pObj, i ) + { + int Value = Vec_IntEntry( vInit, i ); + int iCtrl = Gia_ManCiLit( pNew, i ); + int iData = Gia_ManCiLit( pNew, Gia_ManRegNum(p)+i ); + // decide based on Value + if ( Value == 0 ) + pObj->Value = fUseVars ? Gia_ManHashAnd(pNew, iCtrl, iData) : 0; + else if ( Value == 1 ) + pObj->Value = fUseVars ? Gia_ManHashOr(pNew, Abc_LitNot(iCtrl), iData) : 1; + else if ( Value == 2 ) + pObj->Value = Gia_ManHashAnd(pNew, iCtrl, iData); + else if ( Value == 3 ) + pObj->Value = Gia_ManHashOr(pNew, Abc_LitNot(iCtrl), iData); + else if ( Value == 4 ) + pObj->Value = 0; + else if ( Value == 5 ) + pObj->Value = 1; + else assert( 0 ); + } + for ( f = 0; f < nFrames; f++ ) + { + Gia_ManForEachPi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachRi( p, pObj, i ) + pObj->Value = Gia_ObjFanin0Copy(pObj); + Gia_ManForEachRo( p, pObj, i ) + pObj->Value = Gia_ObjRoToRi(p, pObj)->Value; + } + Gia_ManForEachRi( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, pObj->Value ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + assert( Gia_ManPiNum(pNew) == 2 * Gia_ManRegNum(p) + nFrames * Gia_ManPiNum(p) ); + return pNew; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManMaxiPerform( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nTimeOut, int fVerbose ) +{ + int nIterMax = 1000000; + int i, iLit, Iter, status; + int nLits, * pLits; + abctime clkTotal = Abc_Clock(); + abctime clkSat = 0; + Vec_Int_t * vLits, * vMap; + sat_solver * pSat; + Gia_Obj_t * pObj; + Gia_Man_t * p0 = Gia_ManMaxiUnfold( p, nFrames, 0, vInit ); + Gia_Man_t * p1 = Gia_ManMaxiUnfold( 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 ); + sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 ); + for ( i = 0; i < pCnf->nClauses; i++ ) + if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) + assert( 0 ); + + // add one large OR clause + vLits = Vec_IntAlloc( Gia_ManCoNum(p) ); + Gia_ManForEachCo( pM, pObj, i ) + Vec_IntPush( vLits, Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pM, pObj)], 0) ); + sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ); + + // create assumptions + Vec_IntClear( vLits ); + Gia_ManForEachPi( pM, pObj, i ) + if ( i == Gia_ManRegNum(p) ) + break; + else if ( Vec_IntEntry(vInit, i) == 0 || Vec_IntEntry(vInit, i) == 1 ) + Vec_IntPush( vLits, Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pM, pObj)], 1) ); + + if ( fVerbose ) + { + printf( "Iter%6d : ", 0 ); + printf( "Var =%10d ", sat_solver_nvars(pSat) ); + printf( "Clause =%10d ", sat_solver_nclauses(pSat) ); + printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) ); + printf( "Subset =%6d ", Vec_IntSize(vLits) ); + Abc_PrintTime( 1, "Time", clkSat ); +// ABC_PRTr( "Solver time", clkSat ); + } + for ( Iter = 0; Iter < nIterMax; Iter++ ) + { + abctime clk = Abc_Clock(); + status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + clkSat += Abc_Clock() - clk; + if ( status == l_Undef ) + { +// if ( fVerbose ) +// printf( "\n" ); + printf( "Timeout reached after %d seconds and %d iterations. ", nTimeOut, Iter ); + break; + } + if ( status == l_True ) + { +// if ( fVerbose ) +// printf( "\n" ); + printf( "The problem is SAT after %d iterations. ", Iter ); + break; + } + assert( status == l_False ); + nLits = sat_solver_final( pSat, &pLits ); + if ( fVerbose ) + { + printf( "Iter%6d : ", Iter+1 ); + printf( "Var =%10d ", sat_solver_nvars(pSat) ); + printf( "Clause =%10d ", sat_solver_nclauses(pSat) ); + printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) ); + printf( "Subset =%6d ", nLits ); + Abc_PrintTime( 1, "Time", clkSat ); +// ABC_PRTr( "Solver time", clkSat ); + } + if ( Vec_IntSize(vLits) == nLits ) + { +// if ( fVerbose ) +// printf( "\n" ); + printf( "Reached fixed point with %d entries after %d iterations. ", Vec_IntSize(vLits), Iter+1 ); + break; + } + // collect used literals + Vec_IntClear( vLits ); + for ( i = 0; i < nLits; i++ ) + Vec_IntPush( vLits, Abc_LitNot(pLits[i]) ); + } + // create map + vMap = Vec_IntStart( pCnf->nVars ); + Vec_IntForEachEntry( vLits, iLit, i ) + Vec_IntWriteEntry( vMap, Abc_Lit2Var(iLit), 1 ); + + // create output + Vec_IntFree( vLits ); + vLits = Vec_IntDup(vInit); + Gia_ManForEachPi( pM, pObj, i ) + if ( i == Gia_ManRegNum(p) ) + break; + else if ( Vec_IntEntry(vLits, i) == 4 || Vec_IntEntry(vLits, i) == 5 ) + Vec_IntWriteEntry( vLits, i, Vec_IntEntry(vLits, i) ); + else if ( (Vec_IntEntry(vLits, i) == 0 || Vec_IntEntry(vLits, i) == 1) && !Vec_IntEntry(vMap, pCnf->pVarNums[Gia_ObjId(pM, pObj)]) ) + Vec_IntWriteEntry( vLits, i, Vec_IntEntry(vLits, i) | 2 ); + Vec_IntFree( vMap ); + + // cleanup + sat_solver_delete( pSat ); + Cnf_DataFree( pCnf ); + Gia_ManStop( pM ); + Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); + return vLits; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManMaxiTest( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose ) +{ + Vec_Int_t * vRes, * vInit; + vInit = vInit0 ? vInit0 : Vec_IntStart( Gia_ManRegNum(p) ); + vRes = Gia_ManMaxiPerform( p, vInit, nFrames, nTimeOut, fVerbose ); + if ( vInit != vInit0 ) + Vec_IntFree( vInit ); + return vRes; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bmc/bmcTulip.c b/src/sat/bmc/bmcTulip.c deleted file mode 100644 index 104b3ee4..00000000 --- a/src/sat/bmc/bmcTulip.c +++ /dev/null @@ -1,514 +0,0 @@ -/**CFile**************************************************************** - - FileName [bmcTulip.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: bmcTulip.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "bmc.h" -#include "sat/cnf/cnf.h" -#include "sat/bsat/satStore.h" -#include "aig/gia/giaAig.h" - -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 /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManRoseInit( 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 ( 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) > 1 ) // X - for ( i = 0; i < p->iData; i++ ) - pData0[i] = pData1[i] = 0; - } -} -void Gia_ManRoseSimulateObj( 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 Gia_ManRoseHighestScore( 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 Gia_ManRoseFindStarting( 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 * 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, 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_IntDup(vInit0); - Gia_ParTestAlloc( p, nWords ); - 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, Cost0, Cost0 ); - for ( f = 0; f < nFrames; f++ ) - { - clk = Abc_Clock(); - Gia_ManForEachObj( p, pObj, i ) - 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, Cost0 ); - 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 ); -// printf( "The resulting init state is invalid.\n" ); - Vec_IntFreeP( &vInit ); - return vInit; -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p ) -{ - Cnf_Dat_t * pCnf; - Aig_Man_t * pAig = Gia_ManToAigSimple( p ); - pAig->nRegs = 0; - pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) ); - Aig_ManStop( pAig ); - return pCnf; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -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; - int i, f; - pNew = Gia_ManStart( fUseVars * 2 * Gia_ManRegNum(p) + nFrames * Gia_ManObjNum(p) ); - pNew->pName = Abc_UtilStrsav( p->pName ); - Gia_ManHashAlloc( pNew ); - Gia_ManConst0(p)->Value = 0; - // control/data variables - Gia_ManForEachRo( p, pObj, i ) - Gia_ManAppendCi( pNew ); - Gia_ManForEachRo( p, pObj, i ) - Gia_ManAppendCi( pNew ); - // build timeframes - assert( !vInit || Vec_IntSize(vInit) == Gia_ManRegNum(p) ); - Gia_ManForEachRo( p, pObj, i ) - { - if ( Vec_IntEntry(vInit, i) == 0 ) - pObj->Value = fUseVars ? Gia_ManHashAnd(pNew, Gia_ManCiLit(pNew, i), Gia_ManCiLit(pNew, Gia_ManRegNum(p)+i)) : 0; - else if ( Vec_IntEntry(vInit, i) == 1 ) - pObj->Value = fUseVars ? Gia_ManHashAnd(pNew, Gia_ManCiLit(pNew, i), Gia_ManCiLit(pNew, Gia_ManRegNum(p)+i)) : 1; - else if ( Vec_IntEntry(vInit, i) == 2 ) - pObj->Value = Gia_ManHashAnd(pNew, Gia_ManCiLit(pNew, i), Gia_ManCiLit(pNew, Gia_ManRegNum(p)+i)); - else if ( Vec_IntEntry(vInit, i) == 3 ) - pObj->Value = Gia_ManHashAnd(pNew, Gia_ManCiLit(pNew, i), Gia_ManCiLit(pNew, Gia_ManRegNum(p)+i)); - else assert( 0 ); - } - for ( f = 0; f < nFrames; f++ ) - { - Gia_ManForEachPi( p, pObj, i ) - pObj->Value = Gia_ManAppendCi( pNew ); - Gia_ManForEachAnd( p, pObj, i ) - pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - Gia_ManForEachRi( p, pObj, i ) - pObj->Value = Gia_ObjFanin0Copy(pObj); - Gia_ManForEachRo( p, pObj, i ) - pObj->Value = Gia_ObjRoToRi(p, pObj)->Value; - } - Gia_ManForEachRi( p, pObj, i ) - pObj->Value = Gia_ManAppendCo( pNew, pObj->Value ); - pNew = Gia_ManCleanup( pTemp = pNew ); - Gia_ManStop( pTemp ); - assert( Gia_ManPiNum(pNew) == 2 * Gia_ManRegNum(p) + nFrames * Gia_ManPiNum(p) ); - return pNew; -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -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; - int nLits, * pLits; - abctime clkTotal = Abc_Clock(); - abctime clkSat = 0; - Vec_Int_t * vLits, * vMap; - sat_solver * pSat; - Gia_Obj_t * pObj; - 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 ); - sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 ); - for ( i = 0; i < pCnf->nClauses; i++ ) - if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) - assert( 0 ); - - // add one large OR clause - vLits = Vec_IntAlloc( Gia_ManCoNum(p) ); - Gia_ManForEachCo( pM, pObj, i ) - Vec_IntPush( vLits, Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pM, pObj)], 0) ); - sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ); - - // create assumptions - Vec_IntClear( vLits ); - Gia_ManForEachPi( pM, pObj, i ) - if ( i == Gia_ManRegNum(p) ) - break; - else if ( !(Vec_IntEntry(vInit, i) & 2) ) - Vec_IntPush( vLits, Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pM, pObj)], 1) ); - - if ( fVerbose ) - { - printf( "Iter%6d : ", 0 ); - printf( "Var =%10d ", sat_solver_nvars(pSat) ); - printf( "Clause =%10d ", sat_solver_nclauses(pSat) ); - printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) ); - printf( "Subset =%6d ", Vec_IntSize(vLits) ); - Abc_PrintTime( 1, "Time", clkSat ); -// ABC_PRTr( "Solver time", clkSat ); - } - for ( Iter = 0; Iter < nIterMax; Iter++ ) - { - abctime clk = Abc_Clock(); - status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); - clkSat += Abc_Clock() - clk; - if ( status == l_Undef ) - { -// if ( fVerbose ) -// printf( "\n" ); - printf( "Timeout reached after %d seconds and %d iterations. ", nTimeOut, Iter ); - break; - } - if ( status == l_True ) - { -// if ( fVerbose ) -// printf( "\n" ); - printf( "The problem is SAT after %d iterations. ", Iter ); - break; - } - assert( status == l_False ); - nLits = sat_solver_final( pSat, &pLits ); - if ( fVerbose ) - { - printf( "Iter%6d : ", Iter+1 ); - printf( "Var =%10d ", sat_solver_nvars(pSat) ); - printf( "Clause =%10d ", sat_solver_nclauses(pSat) ); - printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) ); - printf( "Subset =%6d ", nLits ); - Abc_PrintTime( 1, "Time", clkSat ); -// ABC_PRTr( "Solver time", clkSat ); - } - if ( Vec_IntSize(vLits) == nLits ) - { -// if ( fVerbose ) -// printf( "\n" ); - printf( "Reached fixed point with %d entries after %d iterations. ", Vec_IntSize(vLits), Iter+1 ); - break; - } - // collect used literals - Vec_IntClear( vLits ); - for ( i = 0; i < nLits; i++ ) - Vec_IntPush( vLits, Abc_LitNot(pLits[i]) ); - } - // create map - vMap = Vec_IntStart( pCnf->nVars ); - Vec_IntForEachEntry( vLits, iLit, i ) - Vec_IntWriteEntry( vMap, Abc_Lit2Var(iLit), 1 ); - - // create output - Vec_IntFree( vLits ); - vLits = Vec_IntDup(vInit); - Gia_ManForEachPi( pM, pObj, i ) - if ( i == Gia_ManRegNum(p) ) - break; - else if ( !(Vec_IntEntry(vLits, i) & 2) && !Vec_IntEntry(vMap, pCnf->pVarNums[Gia_ObjId(pM, pObj)]) ) - Vec_IntWriteEntry( vLits, i, Vec_IntEntry(vLits, i) | 2 ); - Vec_IntFree( vMap ); - - // cleanup - sat_solver_delete( pSat ); - Cnf_DataFree( pCnf ); - Gia_ManStop( pM ); - Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); - return vLits; -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Gia_ManTulipTest( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose ) -{ - Vec_Int_t * vRes, * vInit; - if ( fSim ) - { - vInit = Vec_IntAlloc(0); Vec_IntFill( vInit, Gia_ManRegNum(p), 2 ); - vRes = Gia_ManRosePerform( p, vInit, nFrames, nWords, fVerbose ); - } - else - { - vInit = vInit0 ? vInit0 : Vec_IntStart( Gia_ManRegNum(p) ); - vRes = Gia_ManTulipPerform( p, vInit, nFrames, nTimeOut, fVerbose ); - } - if ( vInit != vInit0 ) - Vec_IntFree( vInit ); - return vRes; -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make index df8601e7..3ff4b100 100644 --- a/src/sat/bmc/module.make +++ b/src/sat/bmc/module.make @@ -2,6 +2,7 @@ SRC += src/sat/bmc/bmcBmc.c \ src/sat/bmc/bmcBmc2.c \ src/sat/bmc/bmcBmc3.c \ src/sat/bmc/bmcBmcAnd.c \ + src/sat/bmc/bmcBmci.c \ src/sat/bmc/bmcCexCut.c \ src/sat/bmc/bmcCexDepth.c \ src/sat/bmc/bmcCexMin1.c \ @@ -9,8 +10,8 @@ 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/bmcInse.c \ src/sat/bmc/bmcLoad.c \ + src/sat/bmc/bmcMaxi.c \ src/sat/bmc/bmcMulti.c \ - src/sat/bmc/bmcTulip.c \ src/sat/bmc/bmcUnroll.c -- cgit v1.2.3