mirror of https://github.com/YosysHQ/abc.git
New command 'expand' to expand SOPs against the offset.
This commit is contained in:
Alan Mishchenko
parent
ea7d10d45d
commit
5b6e5b8178
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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,11 +8992,95 @@ 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;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
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 []
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
@ -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 \
|
||||
|
|
|
|||
Loading…
Reference in New Issue