diff options
| -rw-r--r-- | abclib.dsp | 4 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 88 | ||||
| -rw-r--r-- | src/sat/bmc/bmcExpand.c | 174 | ||||
| -rw-r--r-- | src/sat/bmc/module.make | 1 |
4 files changed, 266 insertions, 1 deletions
@@ -1863,6 +1863,10 @@ SOURCE=.\src\sat\bmc\bmcEco.c # End Source File # Begin Source File +SOURCE=.\src\sat\bmc\bmcExpand.c +# End Source File +# Begin Source File + SOURCE=.\src\sat\bmc\bmcFault.c # End Source File # Begin Source File diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 302b8553..94de213b 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -158,6 +158,7 @@ static int Abc_CommandBidec ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandOrder ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandMuxes ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandCubes ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandExpand ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSplitSop ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandExtSeqDcs ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandReach ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -793,6 +794,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "order", Abc_CommandOrder, 0 ); Cmd_CommandAdd( pAbc, "Various", "muxes", Abc_CommandMuxes, 1 ); Cmd_CommandAdd( pAbc, "Various", "cubes", Abc_CommandCubes, 1 ); + Cmd_CommandAdd( pAbc, "Various", "expand", Abc_CommandExpand, 1 ); Cmd_CommandAdd( pAbc, "Various", "splitsop", Abc_CommandSplitSop, 1 ); Cmd_CommandAdd( pAbc, "Various", "ext_seq_dcs", Abc_CommandExtSeqDcs, 0 ); Cmd_CommandAdd( pAbc, "Various", "reach", Abc_CommandReach, 0 ); @@ -8990,7 +8992,7 @@ usage: Abc_Print( -2, "usage: cubes [-xh]\n" ); Abc_Print( -2, "\t converts the current network into a network derived by creating\n" ); Abc_Print( -2, "\t a separate node for each product and sum in the local SOPs\n" ); - Abc_Print( -2, "\t-v : toggle using XOR instead of OR [default = %s]\n", fXor? "yes": "no" ); + Abc_Print( -2, "\t-x : toggle using XOR instead of OR [default = %s]\n", fXor? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -9006,6 +9008,90 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandExpand( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Gia_Man_t * Abc_NtkClpGia( Abc_Ntk_t * pNtk ); + extern void Abc_NtkExpandCubes( Abc_Ntk_t * pNtk, Gia_Man_t * pGia, int fVerbose ); + Abc_Ntk_t * pStrash, * pNtk2, * pNtk = Abc_FrameReadNtk(pAbc); + Gia_Man_t * pGia; int c, fVerbose; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + Abc_Print( -1, "Empty network.\n" ); + return 1; + } + if ( !Abc_NtkIsSopLogic(pNtk) ) + { + Abc_Print( -1, "Only a SOP logic network can be transformed into cubes.\n" ); + return 1; + } + if ( Abc_NtkLevel(pNtk) > 1 ) + { + Abc_Print( -1, "The number of logic levels is more than 1 (collapse the network and try again).\n" ); + return 1; + } + // read the offset representation + if ( argc != globalUtilOptind + 1 ) + { + Abc_Print( 0, "Using the complement of the current network as its offset.\n" ); + pNtk2 = Abc_NtkDup( pNtk ); + } + else + { + char * FileName = argv[globalUtilOptind]; + pNtk2 = Io_Read( FileName, Io_ReadFileType(FileName), 1, 0 ); + if ( pNtk2 == NULL ) + { + Abc_Print( -1, "Failed to read the current network from file \"%s\".\n", FileName ); + return 1; + } + } + // strash the network + pStrash = Abc_NtkStrash( pNtk2, 0, 1, 0 ); + Abc_NtkDelete( pNtk2 ); + // convert it into an AIG + pGia = Abc_NtkClpGia( pStrash ); + //Gia_AigerWrite( pGia, "aig_dump.aig", 0, 0 ); + Abc_NtkDelete( pStrash ); + // get the new network + Abc_NtkExpandCubes( pNtk, pGia, fVerbose ); + Gia_ManStop( pGia ); + return 0; + +usage: + Abc_Print( -2, "usage: expand [-vh] <file>\n" ); + Abc_Print( -2, "\t expands cubes against the offset\n" ); + Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "\tfile : (optional) representation of on-set plus dc-set\n"); + + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandSplitSop( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern Abc_Ntk_t * Abc_NtkSplitSop( Abc_Ntk_t * pNtk, int nCubesMax, int fVerbose ); diff --git a/src/sat/bmc/bmcExpand.c b/src/sat/bmc/bmcExpand.c new file mode 100644 index 00000000..f3ec999e --- /dev/null +++ b/src/sat/bmc/bmcExpand.c @@ -0,0 +1,174 @@ +/**CFile**************************************************************** + + FileName [bmcExpand.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT-based bounded model checking.] + + Synopsis [Expanding cubes against the offset.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: bmcExpand.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 "base/abc/abc.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// iterator thought the cubes +#define Bmc_SopForEachCube( pSop, nVars, pCube ) for ( pCube = (pSop); *pCube; pCube += (nVars) + 3 ) + +extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Expands cubes against the offset given as an AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_ObjExpandCubesTry( Vec_Str_t * vSop, sat_solver * pSat, Vec_Int_t * vVars ) +{ + extern int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit, int fCanon, int fOnOffSetLit ); + + char * pCube, * pSop = Vec_StrArray(vSop); + int nCubes = Abc_SopGetCubeNum(pSop); + int nVars = Abc_SopGetVarNum(pSop); + + Vec_Int_t * vLits = Vec_IntAlloc( nVars ); + Vec_Int_t * vTemp = Vec_IntAlloc( nVars ); + + assert( nVars == Vec_IntSize(vVars) ); + assert( Vec_StrSize(vSop) == nCubes * (nVars + 3) + 1 ); + Bmc_SopForEachCube( pSop, nVars, pCube ) + { + int k, Entry; + // collect literals and clean cube + Vec_IntFill( vLits, nVars, -1 ); + for ( k = 0; k < nVars; k++ ) + { + if ( pCube[k] == '-' ) + continue; + Vec_IntWriteEntry( vLits, k, Abc_Var2Lit(Vec_IntEntry(vVars, k), pCube[k] == '0') ); + pCube[k] = '-'; + } + // expand cube + Bmc_CollapseExpandRound( pSat, NULL, vLits, NULL, vTemp, 0, 0, -1 ); + // insert literals + Vec_IntForEachEntry( vLits, Entry, k ) + if ( Entry != -1 ) + pCube[k] = '1' - Abc_LitIsCompl(Entry); + } + + Vec_IntFree( vLits ); + Vec_IntFree( vTemp ); + return nCubes; +} +int Abc_ObjExpandCubes( Vec_Str_t * vSop, Gia_Man_t * p, int nVars ) +{ + extern int Bmc_CollapseIrredundantFull( Vec_Str_t * vSop, int nCubes, int nVars ); + + int fReverse = 0; + Vec_Int_t * vVars = Vec_IntAlloc( nVars ); + Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 ); + sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0); + int v, n, iLit, status, nCubesNew, iCiVarBeg = sat_solver_nvars(pSat) - nVars; + + // check that on-set/off-set is sat + int iOutVar = 1; + for ( n = 0; n < 2; n++ ) + { + iLit = Abc_Var2Lit( iOutVar, n ); // n=0 => F=1 n=1 => F=0 + status = sat_solver_solve( pSat, &iLit, &iLit + 1, 0, 0, 0, 0 ); + if ( status == l_False ) + { + Vec_StrClear( vSop ); + Vec_StrPrintStr( vSop, n ? " 1\n" : " 0\n" ); + Vec_StrPush( vSop, '\0' ); + return 1; + } + } + + // add literals to the solver + iLit = Abc_Var2Lit( iOutVar, 1 ); + status = sat_solver_addclause( pSat, &iLit, &iLit + 1 ); + assert( status ); + + // collect variables + if ( fReverse ) + for ( v = nVars - 1; v >= 0; v-- ) + Vec_IntPush( vVars, iCiVarBeg + v ); + else + for ( v = 0; v < nVars; v++ ) + Vec_IntPush( vVars, iCiVarBeg + v ); + + nCubesNew = Abc_ObjExpandCubesTry( vSop, pSat, vVars ); + + sat_solver_delete( pSat ); + Cnf_DataFree( pCnf ); + Vec_IntFree( vVars ); + if ( nCubesNew > 1 ) + Bmc_CollapseIrredundantFull( vSop, nCubesNew, nVars ); + return 0; +} +void Abc_NtkExpandCubes( Abc_Ntk_t * pNtk, Gia_Man_t * pGia, int fVerbose ) +{ + Gia_Man_t * pNew; + Abc_Obj_t * pObj; int i; + Vec_Str_t * vSop = Vec_StrAlloc( 1000 ); + assert( Abc_NtkIsSopLogic(pNtk) ); + assert( Abc_NtkCiNum(pNtk) == Gia_ManCiNum(pGia) ); + assert( Abc_NtkCoNum(pNtk) == Gia_ManCoNum(pGia) ); + Abc_NtkForEachCo( pNtk, pObj, i ) + { + pObj = Abc_ObjFanin0(pObj); + if ( !Abc_ObjIsNode(pObj) || Abc_ObjFaninNum(pObj) == 0 ) + continue; + assert( Abc_ObjFaninNum(pObj) == Gia_ManCiNum(pGia) ); + + Vec_StrClear( vSop ); + Vec_StrAppend( vSop, (char *)pObj->pData ); + Vec_StrPush( vSop, '\0' ); + + pNew = Gia_ManDupCones( pGia, &i, 1, 0 ); + assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(pGia) ); + if ( Abc_ObjExpandCubes( vSop, pNew, Abc_ObjFaninNum(pObj) ) ) + Vec_IntClear( &pObj->vFanins ); + Gia_ManStop( pNew ); + + pObj->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, Vec_StrArray(vSop) ); + } + Vec_StrFree( vSop ); + Abc_NtkSortSops( pNtk ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make index 6d09b15c..e1777df8 100644 --- a/src/sat/bmc/module.make +++ b/src/sat/bmc/module.make @@ -13,6 +13,7 @@ SRC += src/sat/bmc/bmcBCore.c \ src/sat/bmc/bmcChain.c \ src/sat/bmc/bmcClp.c \ src/sat/bmc/bmcEco.c \ + src/sat/bmc/bmcExpand.c \ src/sat/bmc/bmcFault.c \ src/sat/bmc/bmcFx.c \ src/sat/bmc/bmcICheck.c \ |