Skip to content

A
abc
Commit fe6bb87e by Bruno Schmitt
Options

Merged alanmi/abc into default

parents f93fbc23 07d074fd
Showing with 590 additions and 61 deletions
abclib.dsp
......@@ -1875,6 +1875,10 @@ SOURCE=.\src\sat\bmc\bmcFx.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\bmc\bmcGen.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\bmc\bmcICheck.c
# End Source File
# Begin Source File
......@@ -2551,6 +2555,10 @@ SOURCE=.\src\opt\sfm\sfm.h
# End Source File
# Begin Source File
SOURCE=.\src\opt\sfm\sfmArea.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\sfm\sfmCnf.c
# End Source File
# Begin Source File
......
src/aig/gia/giaDup.c
......@@ -3747,21 +3747,17 @@ void Gia_ManCollectTopXors_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXo
else
Gia_ManCollectTopXors_rec( p, Gia_ObjFanin1(pObj), vXors );
}
Vec_Int_t * Gia_ManCollectTopXors( Gia_Man_t * p, Vec_Int_t * vPolar )
Vec_Int_t * Gia_ManCollectTopXors( Gia_Man_t * p )
{
int i, iObj, iObj2, fFlip, * pPerm, Count1 = 0;
Vec_Int_t * vXors, * vSizes, * vPart[2], * vOrder;
Gia_Obj_t * pFan[2], * pObj = Gia_ManCo(p, 0);
assert( Gia_ManCoNum(p) == 1 );
Vec_IntClear( vPolar );
if ( !Gia_ObjFaninC0(pObj) )
return NULL;
vXors = Vec_IntAlloc( 100 );
pObj = Gia_ObjFanin0(pObj);
if ( Gia_ObjIsAnd(pObj) )
Gia_ManCollectTopXors_rec( p, pObj, vXors );
if ( Gia_ObjFaninC0(pObj) )
Gia_ManCollectTopXors_rec( p, Gia_ObjFanin0(pObj), vXors );
else
Vec_IntPush( vXors, Gia_ObjId(p, pObj) );
Vec_IntPush( vXors, Gia_ObjId(p, Gia_ObjFanin0(pObj)) );
// order by support size
vSizes = Vec_IntAlloc( 100 );
Vec_IntForEachEntry( vXors, iObj, i )
......@@ -3791,7 +3787,6 @@ Vec_Int_t * Gia_ManCollectTopXors( Gia_Man_t * p, Vec_Int_t * vPolar )
pFan[0] = Gia_Regular(pFan[0]);
pFan[1] = Gia_Regular(pFan[1]);
}
Vec_IntPushTwo( vPolar, 0, fCompl );
fFlip = Gia_ManDecideWhereToAdd( p, vPart, pFan );
Vec_IntPush( vPart[0], Gia_ObjId(p, pFan[fFlip]) );
Vec_IntPush( vPart[1], Gia_ObjId(p, pFan[!fFlip]) );
......@@ -3808,22 +3803,20 @@ Vec_Int_t * Gia_ManCollectTopXors( Gia_Man_t * p, Vec_Int_t * vPolar )
Vec_IntFree( vPart[0] );
Vec_IntFree( vPart[1] );
Vec_IntReverseOrder( vOrder ); // from LSB to MSB
Vec_IntReverseOrder( vPolar );
//Vec_IntPrint( vOrder );
return vOrder;
}
Gia_Man_t * Gia_ManDemiterToDual( Gia_Man_t * p )
{
Gia_Man_t * pNew; Gia_Obj_t * pObj; int i;
Vec_Int_t * vNodes, * vPolar = Vec_IntAlloc( 100 );
Vec_Int_t * vOrder = Gia_ManCollectTopXors( p, vPolar );
Vec_Int_t * vNodes;
Vec_Int_t * vOrder = Gia_ManCollectTopXors( p );
if ( vOrder == NULL )
{
Vec_IntFree( vPolar );
printf( "Cannot demiter because the top-most gate is an AND-gate.\n" );
return NULL;
}
assert( Vec_IntSize(vOrder) == Vec_IntSize(vPolar) );
assert( Vec_IntSize(vOrder) % 2 == 0 );
vNodes = Vec_IntAlloc( Gia_ManObjNum(p) );
Gia_ManIncrementTravId( p );
Gia_ManCollectAnds( p, Vec_IntArray(vOrder), Vec_IntSize(vOrder), vNodes, NULL );
......@@ -3835,9 +3828,9 @@ Gia_Man_t * Gia_ManDemiterToDual( Gia_Man_t * p )
pObj->Value = Gia_ManAppendCi( pNew );
Gia_ManForEachObjVec( vNodes, p, pObj, i )
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManSetPhase( p );
Gia_ManForEachObjVec( vOrder, p, pObj, i )
Gia_ManAppendCo( pNew, Abc_LitNotCond(pObj->Value, Vec_IntEntry(vPolar, i)) );
Vec_IntFree( vPolar );
Gia_ManAppendCo( pNew, Abc_LitNotCond(pObj->Value, pObj->fPhase) );
Vec_IntFree( vNodes );
Vec_IntFree( vOrder );
return pNew;
......
src/aig/gia/giaNf.c
......@@ -178,18 +178,17 @@ int Nf_StoCellIsDominated( Mio_Cell2_t * pCell, int * pFans, int * pProf )
return 0;
return 1; // pCell is dominated
}
void Nf_StoCreateGateAdd( Nf_Man_t * pMan, word uTruth, int * pFans, int nFans, int CellId, Vec_Wec_t * vProfs, Vec_Int_t * vStore )
void Nf_StoCreateGateAdd( Vec_Mem_t * vTtMem, Vec_Wec_t * vTt2Match, Mio_Cell2_t * pCell, word uTruth, int * pFans, int nFans, Vec_Wec_t * vProfs, Vec_Int_t * vStore, int fPinFilter, int fPinPerm, int fPinQuick )
{
Vec_Int_t * vArray, * vArrayProfs = NULL;
Mio_Cell2_t * pCell = Nf_ManCell( pMan, CellId );
int i, k, GateId, Entry, fCompl = (int)(uTruth & 1);
word uFunc = fCompl ? ~uTruth : uTruth;
int iFunc = Vec_MemHashInsert( pMan->vTtMem, &uFunc );
int iFunc = Vec_MemHashInsert( vTtMem, &uFunc );
Nf_Cfg_t Mat = Nf_Int2Cfg(0);
// get match array
if ( iFunc == Vec_WecSize(pMan->vTt2Match) )
Vec_WecPushLevel( pMan->vTt2Match );
vArray = Vec_WecEntry( pMan->vTt2Match, iFunc );
if ( iFunc == Vec_WecSize(vTt2Match) )
Vec_WecPushLevel( vTt2Match );
vArray = Vec_WecEntry( vTt2Match, iFunc );
// create match
Mat.fCompl = fCompl;
assert( nFans == (int)pCell->nFanins );
......@@ -199,10 +198,10 @@ void Nf_StoCreateGateAdd( Nf_Man_t * pMan, word uTruth, int * pFans, int nFans,
Mat.Phase |= (unsigned)(Abc_LitIsCompl(pFans[i]) << Abc_Lit2Var(pFans[i]));
}
// check other profiles
if ( pMan->pPars->fPinFilter )
if ( fPinFilter )
{
// get profile array
assert( Vec_WecSize(pMan->vTt2Match) == Vec_WecSize(vProfs) );
assert( Vec_WecSize(vTt2Match) == Vec_WecSize(vProfs) );
if ( iFunc == Vec_WecSize(vProfs) )
Vec_WecPushLevel( vProfs );
vArrayProfs = Vec_WecEntry( vProfs, iFunc );
......@@ -218,26 +217,26 @@ void Nf_StoCreateGateAdd( Nf_Man_t * pMan, word uTruth, int * pFans, int nFans,
}
}
// check pin permutation
if ( !pMan->pPars->fPinPerm ) // do not use pin-permutation (improves delay when pin-delays differ)
if ( !fPinPerm ) // do not use pin-permutation (improves delay when pin-delays differ)
{
if ( pMan->pPars->fPinQuick ) // reduce the number of matches agressively
if ( fPinQuick ) // reduce the number of matches agressively
{
Vec_IntForEachEntryDouble( vArray, GateId, Entry, i )
if ( GateId == CellId && Abc_TtBitCount8[Nf_Int2Cfg(Entry).Phase] == Abc_TtBitCount8[Mat.Phase] )
if ( GateId == (int)pCell->Id && Abc_TtBitCount8[Nf_Int2Cfg(Entry).Phase] == Abc_TtBitCount8[Mat.Phase] )
return;
}
else // reduce the number of matches less agressively
{
Vec_IntForEachEntryDouble( vArray, GateId, Entry, i )
if ( GateId == CellId && Nf_Int2Cfg(Entry).Phase == Mat.Phase )
if ( GateId == (int)pCell->Id && Nf_Int2Cfg(Entry).Phase == Mat.Phase )
return;
}
}
// save data and profile
Vec_IntPush( vArray, CellId );
Vec_IntPush( vArray, pCell->Id );
Vec_IntPush( vArray, Nf_Cfg2Int(Mat) );
// add delay profile
if ( pMan->pPars->fPinFilter )
if ( fPinFilter )
{
Vec_IntPush( vArrayProfs, Vec_IntSize(vStore) );
Vec_IntPush( vStore, Abc_Float2Int(pCell->AreaF) );
......@@ -245,7 +244,7 @@ void Nf_StoCreateGateAdd( Nf_Man_t * pMan, word uTruth, int * pFans, int nFans,
Vec_IntPush( vStore, pCell->iDelays[Abc_Lit2Var(pFans[k])] );
}
}
void Nf_StoCreateGateMaches( Nf_Man_t * pMan, Mio_Cell2_t * pCell, int ** pComp, int ** pPerm, int * pnPerms, Vec_Wec_t * vProfs, Vec_Int_t * vStore )
void Nf_StoCreateGateMaches( Vec_Mem_t * vTtMem, Vec_Wec_t * vTt2Match, Mio_Cell2_t * pCell, int ** pComp, int ** pPerm, int * pnPerms, Vec_Wec_t * vProfs, Vec_Int_t * vStore, int fPinFilter, int fPinPerm, int fPinQuick )
{
int Perm[NF_LEAF_MAX], * Perm1, * Perm2;
int nPerms = pnPerms[pCell->nFanins];
......@@ -261,7 +260,7 @@ void Nf_StoCreateGateMaches( Nf_Man_t * pMan, Mio_Cell2_t * pCell, int ** pComp,
tTemp2 = tCur;
for ( c = 0; c < nMints; c++ )
{
Nf_StoCreateGateAdd( pMan, tCur, Perm, pCell->nFanins, pCell->Id, vProfs, vStore );
Nf_StoCreateGateAdd( vTtMem, vTt2Match, pCell, tCur, Perm, pCell->nFanins, vProfs, vStore, fPinFilter, fPinPerm, fPinQuick );
// update
tCur = Abc_Tt6Flip( tCur, pComp[pCell->nFanins][c] );
Perm1 = Perm + pComp[pCell->nFanins][c];
......@@ -278,12 +277,14 @@ void Nf_StoCreateGateMaches( Nf_Man_t * pMan, Mio_Cell2_t * pCell, int ** pComp,
}
assert( tTemp1 == tCur );
}
void Nf_StoDeriveMatches( Nf_Man_t * p, int fVerbose )
Mio_Cell2_t * Nf_StoDeriveMatches( Vec_Mem_t * vTtMem, Vec_Wec_t * vTt2Match, int * pnCells, int fPinFilter, int fPinPerm, int fPinQuick )
{
// abctime clk = Abc_Clock();
int fVerbose = 0;
//abctime clk = Abc_Clock();
Vec_Wec_t * vProfs = Vec_WecAlloc( 1000 );
Vec_Int_t * vStore = Vec_IntAlloc( 10000 );
int * pComp[7], * pPerm[7], nPerms[7], i;
Mio_Cell2_t * pCells;
Vec_WecPushLevel( vProfs );
Vec_WecPushLevel( vProfs );
for ( i = 1; i <= 6; i++ )
......@@ -292,18 +293,18 @@ void Nf_StoDeriveMatches( Nf_Man_t * p, int fVerbose )
pPerm[i] = Extra_PermSchedule( i );
for ( i = 1; i <= 6; i++ )
nPerms[i] = Extra_Factorial( i );
p->pCells = Mio_CollectRootsNewDefault2( 6, &p->nCells, fVerbose );
for ( i = 2; i < p->nCells; i++ )
Nf_StoCreateGateMaches( p, p->pCells + i, pComp, pPerm, nPerms, vProfs, vStore );
pCells = Mio_CollectRootsNewDefault2( 6, pnCells, fVerbose );
for ( i = 2; i < *pnCells; i++ )
Nf_StoCreateGateMaches( vTtMem, vTt2Match, pCells+i, pComp, pPerm, nPerms, vProfs, vStore, fPinFilter, fPinPerm, fPinQuick );
for ( i = 1; i <= 6; i++ )
ABC_FREE( pComp[i] );
for ( i = 1; i <= 6; i++ )
ABC_FREE( pPerm[i] );
Vec_WecFree( vProfs );
Vec_IntFree( vStore );
// Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
//Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return pCells;
}
//void Nf_StoPrintOne( Nf_Man_t * p, int Count, int t, int i, int GateId, Pf_Mat_t Mat )
void Nf_StoPrintOne( Nf_Man_t * p, int Count, int t, int i, int GateId, Nf_Cfg_t Mat )
{
Mio_Cell2_t * pC = p->pCells + GateId;
......@@ -398,12 +399,7 @@ Nf_Man_t * Nf_StoCreate( Gia_Man_t * pGia, Jf_Par_t * pPars )
}
Vec_IntFree(vFlowRefs);
// matching
p->vTtMem = Vec_MemAllocForTT( 6, 0 );
p->vTt2Match = Vec_WecAlloc( 1000 );
Vec_WecPushLevel( p->vTt2Match );
Vec_WecPushLevel( p->vTt2Match );
assert( Vec_WecSize(p->vTt2Match) == Vec_MemEntryNum(p->vTtMem) );
Nf_StoDeriveMatches( p, 0 );//pPars->fVerbose );
Mio_LibraryMatchesFetch( (Mio_Library_t *)Abc_FrameReadLibGen(), &p->vTtMem, &p->vTt2Match, &p->pCells, &p->nCells, p->pPars->fPinFilter, p->pPars->fPinPerm, p->pPars->fPinQuick );
p->InvDelayI = p->pCells[3].iDelays[0];
p->InvAreaW = p->pCells[3].AreaW;
p->InvAreaF = p->pCells[3].AreaF;
......@@ -424,11 +420,6 @@ void Nf_StoDelete( Nf_Man_t * p )
ABC_FREE( p->vCutDelays.pArray );
ABC_FREE( p->vBackup.pArray );
ABC_FREE( p->pNfObjs );
// matching
Vec_WecFree( p->vTt2Match );
Vec_MemHashFree( p->vTtMem );
Vec_MemFree( p->vTtMem );
ABC_FREE( p->pCells );
ABC_FREE( p );
}
......
src/base/abci/abc.c
......@@ -41422,6 +41422,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// Gia_ManCheckFalseTest( pAbc->pGia, nFrames );
// Gia_ParTest( pAbc->pGia, nWords, nProcs );
// Gia_PolynExplore( pAbc->pGia );
// Gia_ManTestSatEnum( pAbc->pGia );
// printf( "\nThis command is currently disabled.\n\n" );
return 0;
src/base/wlc/wlc.c
......@@ -19,6 +19,7 @@
***********************************************************************/
#include "wlc.h"
#include "sat/bsat/satStore.h"
ABC_NAMESPACE_IMPL_START
......@@ -127,6 +128,143 @@ void Wlc_GenerateCodeMax4( int nBits )
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Wlc_BlastFullAdderCtrlCnf( sat_solver * pSat, int a, int ac, int b, int c, int * pc, int * ps, int * piVars )
{
int Cnf[12][6] = { // xabc cs // abc cs
{ -1, 0, 0, 0, 0, 0 }, // -000 00 // 000 00
{ -1, 0, 0, 1, 0, 1 }, // -001 01 // 001 01
{ -1, 0, 1, 0, 0, 1 }, // -010 01 // 010 01
{ -1, 0, 1, 1, 1, 0 }, // -011 10 // 011 10
{ 0,-1, 0, 0, 0, 0 }, // 0-00 00
{ 0,-1, 0, 1, 0, 1 }, // 0-01 01
{ 0,-1, 1, 0, 0, 1 }, // 0-10 01
{ 0,-1, 1, 1, 1, 0 }, // 0-11 10
{ 1, 1, 0, 0, 0, 1 }, // 1100 01 // 100 01
{ 1, 1, 0, 1, 1, 0 }, // 1101 10 // 101 10
{ 1, 1, 1, 0, 1, 0 }, // 1110 10 // 110 10
{ 1, 1, 1, 1, 1, 1 } // 1111 11 // 111 11
};
int pVars[6] = {a, ac, b, c, *piVars, *piVars+1};
int i, v, nLits, pLits[6];
for ( i = 0; i < 12; i++ )
{
nLits = 0;
for ( v = 0; v < 6; v++ )
{
if ( Cnf[i][v] == -1 )
continue;
if ( pVars[v] == 0 ) // const 0
{
if ( Cnf[i][v] == 0 )
continue;
if ( Cnf[i][v] == 1 )
break;
}
if ( pVars[v] == -1 ) // const -1
{
if ( Cnf[i][v] == 0 )
break;
if ( Cnf[i][v] == 1 )
continue;
}
pLits[nLits++] = Abc_Var2Lit( pVars[v], Cnf[i][v] );
}
if ( v < 6 )
continue;
assert( nLits > 2 );
sat_solver_addclause( pSat, pLits, pLits + nLits );
}
*pc = (*piVars)++;
*ps = (*piVars)++;
}
void Wlc_BlastMultiplierCnf( sat_solver * pSat, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vTemp, Vec_Int_t * vRes, int * piVars )
{
int * pRes, * pArgC, * pArgS, a, b, Carry = 0;
assert( nArgA > 0 && nArgB > 0 );
// prepare result
Vec_IntFill( vRes, nArgA + nArgB, 0 );
pRes = Vec_IntArray( vRes );
// prepare intermediate storage
Vec_IntFill( vTemp, 2 * nArgA, 0 );
pArgC = Vec_IntArray( vTemp );
pArgS = pArgC + nArgA;
// create matrix
for ( b = 0; b < nArgB; b++ )
for ( a = 0; a < nArgA; a++ )
Wlc_BlastFullAdderCtrlCnf( pSat, pArgA[a], pArgB[b], pArgS[a], pArgC[a], &pArgC[a], a ? &pArgS[a-1] : &pRes[b], piVars );
// final addition
pArgS[nArgA-1] = 0;
for ( a = 0; a < nArgA; a++ )
Wlc_BlastFullAdderCtrlCnf( pSat, -1, pArgC[a], pArgS[a], Carry, &Carry, &pRes[nArgB+a], piVars );
}
sat_solver * Wlc_BlastMultiplierCnfMain( int nBits )
{
Vec_Int_t * vRes1 = Vec_IntAlloc( 2*nBits );
Vec_Int_t * vRes2 = Vec_IntAlloc( 2*nBits );
Vec_Int_t * vTemp = Vec_IntAlloc( 2*nBits );
int * pArgA = ABC_ALLOC( int, nBits );
int * pArgB = ABC_ALLOC( int, nBits );
int i, Ent1, Ent2, nVars = 1 + 2*nBits;
int nVarsAll = 1 + 4*nBits + 4*nBits*(nBits + 1);
sat_solver * pSat = sat_solver_new();
sat_solver_setnvars( pSat, nVarsAll );
for ( i = 0; i < nBits; i++ )
pArgA[i] = 1 + i, pArgB[i] = 1 + nBits + i;
Wlc_BlastMultiplierCnf( pSat, pArgA, pArgB, nBits, nBits, vTemp, vRes1, &nVars );
for ( i = 0; i < nBits; i++ )
pArgA[i] = 1 + nBits + i, pArgB[i] = 1 + i;
Wlc_BlastMultiplierCnf( pSat, pArgA, pArgB, nBits, nBits, vTemp, vRes2, &nVars );
Vec_IntClear( vTemp );
Vec_IntForEachEntryTwo( vRes1, vRes2, Ent1, Ent2, i )
{
Vec_IntPush( vTemp, Abc_Var2Lit(nVars, 0) );
sat_solver_add_xor( pSat, Ent1, Ent2, nVars++, 0 );
}
assert( nVars == nVarsAll );
sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
ABC_FREE( pArgA );
ABC_FREE( pArgB );
Vec_IntFree( vRes1 );
Vec_IntFree( vRes2 );
Vec_IntFree( vTemp );
return pSat;
}
void Wlc_BlastMultiplierCnfTest( int nBits )
{
abctime clk = Abc_Clock();
sat_solver * pSat = Wlc_BlastMultiplierCnfMain( nBits );
int i, status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
Sat_SolverWriteDimacs( pSat, "test_mult.cnf", NULL, NULL, 0 );
for ( i = 0; i < sat_solver_nvars(pSat); i++ )
printf( "%d=%d ", i, sat_solver_var_value(pSat, i) );
printf( "\n" );
printf( "Verifying for %d bits: %s ", nBits, status == l_True ? "SAT" : "UNSAT" );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
sat_solver_delete( pSat );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/map/mio/mio.c
......@@ -286,18 +286,14 @@ int Mio_CommandReadGenlib( Abc_Frame_t * pAbc, int argc, char **argv )
Amap_Lib_t * pLib2;
char * pFileName;
char * pExcludeFile = NULL;
int fVerbose;
double WireDelay;
int c;
double WireDelay = 0.0;
int fShortNames = 0;
int c, fVerbose = 1;
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set the defaults
WireDelay = 0.0;
fVerbose = 1;
Extra_UtilGetoptReset();
while ( (c = Extra_UtilGetopt(argc, argv, "WEvh")) != EOF )
while ( (c = Extra_UtilGetopt(argc, argv, "WEnvh")) != EOF )
{
switch (c)
{
......@@ -321,6 +317,9 @@ int Mio_CommandReadGenlib( Abc_Frame_t * pAbc, int argc, char **argv )
pExcludeFile = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'n':
fShortNames ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
......@@ -358,6 +357,10 @@ int Mio_CommandReadGenlib( Abc_Frame_t * pAbc, int argc, char **argv )
if ( fVerbose )
printf( "Entered genlib library with %d gates from file \"%s\".\n", Mio_LibraryReadGateNum(pLib), pFileName );
// convert the library if needed
if ( fShortNames )
Mio_LibraryShortNames( pLib );
// add the fixed number (wire delay) to all delays in the library
if ( WireDelay != 0.0 )
Mio_LibraryShiftDelay( pLib, WireDelay );
......@@ -376,13 +379,14 @@ int Mio_CommandReadGenlib( Abc_Frame_t * pAbc, int argc, char **argv )
return 0;
usage:
fprintf( pErr, "usage: read_genlib [-W float] [-E filename] [-vh]\n");
fprintf( pErr, "usage: read_genlib [-W float] [-E filename] [-nvh]\n");
fprintf( pErr, "\t read the library from a genlib file\n" );
fprintf( pErr, "\t (if the library contains more than one gate\n" );
fprintf( pErr, "\t with the same Boolean function, only the gate\n" );
fprintf( pErr, "\t with the smallest area will be used)\n" );
fprintf( pErr, "\t-W float : wire delay (added to pin-to-pin gate delays) [default = %g]\n", WireDelay );
fprintf( pErr, "\t-E file : the file name with gates to be excluded [default = none]\n" );
fprintf( pErr, "\t-n : toggle replacing gate/pin names by short strings [default = %s]\n", fShortNames? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : enable verbose output\n");
return 1;
......
src/map/mio/mio.h
......@@ -213,6 +213,11 @@ extern void Mio_LibraryTransferProfile( Mio_Library_t * pLibDst, Mi
extern void Mio_LibraryTransferProfile2( Mio_Library_t * pLibDst, Mio_Library_t * pLibSrc );
extern int Mio_LibraryHasProfile( Mio_Library_t * pLib );
extern void Mio_LibraryCleanProfile2( Mio_Library_t * pLib );
extern void Mio_LibraryShortNames( Mio_Library_t * pLib );
extern void Mio_LibraryMatchesStop( Mio_Library_t * pLib );
extern void Mio_LibraryMatchesStart( Mio_Library_t * pLib, int fPinFilter, int fPinPerm, int fPinQuick );
extern void Mio_LibraryMatchesFetch( Mio_Library_t * pLib, Vec_Mem_t ** pvTtMem, Vec_Wec_t ** pvTt2Match, Mio_Cell2_t ** ppCells, int * pnCells, int fPinFilter, int fPinPerm, int fPinQuick );
/*=== sclUtil.c =========================================================*/
extern Mio_Library_t * Abc_SclDeriveGenlibSimple( void * pScl );
......
src/map/mio/mioInt.h
......@@ -76,6 +76,14 @@ struct Mio_LibraryStruct_t_
st__table * tName2Gate; // the mapping of gate names into their pointer
Mem_Flex_t * pMmFlex; // the memory manaqer for SOPs
Vec_Str_t * vCube; // temporary cube
// matching
int fPinFilter; // pin filtering
int fPinPerm; // pin permutation
int fPinQuick; // pin permutation
Vec_Mem_t * vTtMem; // truth tables
Vec_Wec_t * vTt2Match; // matches for truth tables
Mio_Cell2_t * pCells; // library gates
int nCells; // library gate count
};
struct Mio_GateStruct_t_
......
src/map/mio/mioUtils.c
......@@ -53,6 +53,7 @@ void Mio_LibraryDelete( Mio_Library_t * pLib )
Mio_Gate_t * pGate, * pGate2;
if ( pLib == NULL )
return;
Mio_LibraryMatchesStop( pLib );
// free the bindings of nodes to gates from this library for all networks
Abc_FrameUnmapAllNetworks( Abc_FrameGetGlobalFrame() );
// free the library
......@@ -732,8 +733,13 @@ Mio_Cell2_t * Mio_CollectRootsNew2( Mio_Library_t * pLib, int nInputs, int * pnG
assert( Mio_AreaCompare2( ppCells + 4, ppCells + iCell - 1 ) <= 0 );
}
// assign IDs
Mio_LibraryForEachGate( pLib, pGate0 )
Mio_GateSetCell( pGate0, -1 );
for ( i = 0; i < iCell; i++ )
{
ppCells[i].Id = ppCells[i].pName ? i : -1;
Mio_GateSetCell( (Mio_Gate_t *)ppCells[i].pMioGate, i );
}
// report
if ( fVerbose )
......@@ -1465,6 +1471,177 @@ void Mio_LibraryCleanProfile2( Mio_Library_t * pLib )
Mio_GateSetProfile2( pGate, 0 );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Mio_LibraryHashGates( Mio_Library_t * pLib )
{
Mio_Gate_t * pGate;
Mio_LibraryForEachGate( pLib, pGate )
if ( pGate->pTwin )
{
printf( "Gates with multiple outputs are not supported.\n" );
return;
}
if ( pLib->tName2Gate )
st__free_table( pLib->tName2Gate );
pLib->tName2Gate = st__init_table(strcmp, st__strhash);
Mio_LibraryForEachGate( pLib, pGate )
st__insert( pLib->tName2Gate, pGate->pName, (char *)pGate );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Abc_SclIsChar( char c )
{
return (c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z') || c == '_';
}
static inline int Abc_SclIsName( char c )
{
return Abc_SclIsChar(c) || (c >= '0' && c <= '9');
}
static inline char * Abc_SclFindLimit( char * pName )
{
assert( Abc_SclIsChar(*pName) );
while ( Abc_SclIsName(*pName) )
pName++;
return pName;
}
static inline int Abc_SclAreEqual( char * pBase, char * pName, char * pLimit )
{
return !strncmp( pBase, pName, pLimit - pName );
}
void Mio_LibraryShortFormula( Mio_Gate_t * pCell, char * pForm, char * pBuffer )
{
Mio_Pin_t * pPin;
char * pTemp, * pLimit; int i;
if ( !strncmp(pForm, "CONST", 5) )
{
sprintf( pBuffer, "%s", pForm );
return;
}
for ( pTemp = pForm; *pTemp; )
{
if ( !Abc_SclIsChar(*pTemp) )
{
*pBuffer++ = *pTemp++;
continue;
}
pLimit = Abc_SclFindLimit( pTemp );
i = 0;
Mio_GateForEachPin( pCell, pPin )
{
if ( Abc_SclAreEqual( pPin->pName, pTemp, pLimit ) )
{
*pBuffer++ = 'a' + i;
break;
}
i++;
}
pTemp = pLimit;
}
*pBuffer++ = 0;
}
void Mio_LibraryShortNames( Mio_Library_t * pLib )
{
char Buffer[10000];
Mio_Gate_t * pGate; Mio_Pin_t * pPin;
int c = 0, i, nDigits = Abc_Base10Log( Mio_LibraryReadGateNum(pLib) );
// itereate through classes
Mio_LibraryForEachGate( pLib, pGate )
{
ABC_FREE( pGate->pName );
sprintf( Buffer, "g%0*d", nDigits, ++c );
pGate->pName = Abc_UtilStrsav( Buffer );
// update formula
Mio_LibraryShortFormula( pGate, pGate->pForm, Buffer );
ABC_FREE( pGate->pForm );
pGate->pForm = Abc_UtilStrsav( Buffer );
// pin names
i = 0;
Mio_GateForEachPin( pGate, pPin )
{
ABC_FREE( pPin->pName );
sprintf( Buffer, "%c", 'a'+i );
pPin->pName = Abc_UtilStrsav( Buffer );
i++;
}
// output pin
ABC_FREE( pGate->pOutName );
sprintf( Buffer, "z" );
pGate->pOutName = Abc_UtilStrsav( Buffer );
}
Mio_LibraryHashGates( pLib );
// update library name
printf( "Renaming library \"%s\" into \"%s%d\".\n", pLib->pName, "lib", Mio_LibraryReadGateNum(pLib) );
ABC_FREE( pLib->pName );
sprintf( Buffer, "lib%d", Mio_LibraryReadGateNum(pLib) );
pLib->pName = Abc_UtilStrsav( Buffer );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Mio_LibraryMatchesStop( Mio_Library_t * pLib )
{
if ( !pLib->vTtMem )
return;
Vec_WecFree( pLib->vTt2Match );
Vec_MemHashFree( pLib->vTtMem );
Vec_MemFree( pLib->vTtMem );
ABC_FREE( pLib->pCells );
}
void Mio_LibraryMatchesStart( Mio_Library_t * pLib, int fPinFilter, int fPinPerm, int fPinQuick )
{
extern Mio_Cell2_t * Nf_StoDeriveMatches( Vec_Mem_t * vTtMem, Vec_Wec_t * vTt2Match, int * pnCells, int fPinFilter, int fPinPerm, int fPinQuick );
if ( pLib->vTtMem && pLib->fPinFilter == fPinFilter && pLib->fPinPerm == fPinPerm && pLib->fPinQuick == fPinQuick )
return;
if ( pLib->vTtMem )
Mio_LibraryMatchesStop( pLib );
pLib->fPinFilter = fPinFilter; // pin filtering
pLib->fPinPerm = fPinPerm; // pin permutation
pLib->fPinQuick = fPinQuick; // pin permutation
pLib->vTtMem = Vec_MemAllocForTT( 6, 0 );
pLib->vTt2Match = Vec_WecAlloc( 1000 );
Vec_WecPushLevel( pLib->vTt2Match );
Vec_WecPushLevel( pLib->vTt2Match );
assert( Vec_WecSize(pLib->vTt2Match) == Vec_MemEntryNum(pLib->vTtMem) );
pLib->pCells = Nf_StoDeriveMatches( pLib->vTtMem, pLib->vTt2Match, &pLib->nCells, fPinFilter, fPinPerm, fPinQuick );
}
void Mio_LibraryMatchesFetch( Mio_Library_t * pLib, Vec_Mem_t ** pvTtMem, Vec_Wec_t ** pvTt2Match, Mio_Cell2_t ** ppCells, int * pnCells, int fPinFilter, int fPinPerm, int fPinQuick )
{
Mio_LibraryMatchesStart( pLib, fPinFilter, fPinPerm, fPinQuick );
*pvTtMem = pLib->vTtMem; // truth tables
*pvTt2Match = pLib->vTt2Match; // matches for truth tables
*ppCells = pLib->pCells; // library gates
*pnCells = pLib->nCells; // library gate count
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/misc/vec/vec.h
......@@ -36,6 +36,8 @@
#include "vecAtt.h"
#include "vecWrd.h"
#include "vecBit.h"
#include "vecMem.h"
#include "vecWec.h"
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
......
src/opt/fxch/module.make
SRC += src/opt/fxch/Fxch.c \
src/opt/fxch/FxchDiv.c \
src/opt/fxch/FxchMan.c \
src/opt/fxch/FxchSCHashTable.c \
src/opt/fxch/FxchSCHashTable.c
src/opt/sfm/module.make
SRC += src/opt/sfm/sfmCnf.c \
SRC += src/opt/sfm/sfmArea.c \
src/opt/sfm/sfmCnf.c \
src/opt/sfm/sfmCore.c \
src/opt/sfm/sfmDec.c \
src/opt/sfm/sfmLib.c \
......
src/opt/sfm/sfmDec.c
......@@ -2152,6 +2152,11 @@ void Abc_NtkPerformMfs3( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars )
if ( pPars->fLibVerbose )
Sfm_LibPrint( p->pLib );
Sfm_DecStop( p );
if ( pPars->fArea )
{
extern void Abc_NtkChangePerform( Abc_Ntk_t * pNtk, int fVerbose );
Abc_NtkChangePerform( pNtk, pPars->fVerbose );
}
}
////////////////////////////////////////////////////////////////////////
......
src/sat/bmc/bmcGen.c 0 → 100644
/**CFile****************************************************************
FileName [bmcGen.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT-based bounded model checking.]
Synopsis [Generating satisfying assignments.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: bmcGen.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"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline word * Gia_ManMoObj( Gia_Man_t * p, int iObj )
{
return Vec_WrdEntryP( p->vSims, iObj * p->iPatsPi );
}
static inline void Gia_ManMoSetCi( Gia_Man_t * p, int iObj )
{
int w;
word * pSims = Gia_ManMoObj( p, iObj );
for ( w = 0; w < p->iPatsPi; w++ )
pSims[w] = Gia_ManRandomW( 0 );
}
static inline void Gia_ManMoSimAnd( Gia_Man_t * p, int iObj )
{
int w;
Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
word * pSims = Gia_ManMoObj( p, iObj );
word * pSims0 = Gia_ManMoObj( p, Gia_ObjFaninId0(pObj, iObj) );
word * pSims1 = Gia_ManMoObj( p, Gia_ObjFaninId1(pObj, iObj) );
if ( Gia_ObjFaninC0(pObj) )
{
if ( Gia_ObjFaninC1(pObj) )
for ( w = 0; w < p->iPatsPi; w++ )
pSims[w] = ~(pSims0[w] | pSims1[w]);
else
for ( w = 0; w < p->iPatsPi; w++ )
pSims[w] = ~pSims0[w] & pSims1[w];
}
else
{
if ( Gia_ObjFaninC1(pObj) )
for ( w = 0; w < p->iPatsPi; w++ )
pSims[w] = pSims0[w] & ~pSims1[w];
else
for ( w = 0; w < p->iPatsPi; w++ )
pSims[w] = pSims0[w] & pSims1[w];
}
}
static inline void Gia_ManMoSetCo( Gia_Man_t * p, int iObj )
{
int w;
Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
word * pSims = Gia_ManMoObj( p, iObj );
word * pSims0 = Gia_ManMoObj( p, Gia_ObjFaninId0(pObj, iObj) );
if ( Gia_ObjFaninC0(pObj) )
{
for ( w = 0; w < p->iPatsPi; w++ )
pSims[w] = ~pSims0[w];
}
else
{
for ( w = 0; w < p->iPatsPi; w++ )
pSims[w] = pSims0[w];
}
}
void Gia_ManMoFindSimulate( Gia_Man_t * p, int nWords )
{
int i, iObj;
Gia_ManRandomW( 1 );
p->iPatsPi = nWords;
if ( p->vSims )
Vec_WrdFill( p->vSims, nWords * Gia_ManObjNum(p), 0 );
else
p->vSims = Vec_WrdStart( nWords * Gia_ManObjNum(p) );
Gia_ManForEachCiId( p, iObj, i )
Gia_ManMoSetCi( p, iObj );
Gia_ManForEachAndId( p, iObj )
Gia_ManMoSimAnd( p, iObj );
Gia_ManForEachCoId( p, iObj, i )
Gia_ManMoSetCo( p, iObj );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManTestSatEnum( Gia_Man_t * p )
{
abctime clk = Abc_Clock(), clk2, clkTotal = 0;
Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
int i, v, status, iLit, nWords = 1, iOutVar = 1, Count = 0;
Vec_Int_t * vVars = Vec_IntAlloc( 1000 );
word * pSimInfo;
// add literals to the solver
iLit = Abc_Var2Lit( iOutVar, 0 );
status = sat_solver_addclause( pSat, &iLit, &iLit + 1 );
assert( status );
// simulate the AIG
Gia_ManMoFindSimulate( p, nWords );
// print outputs
pSimInfo = Gia_ManMoObj( p, Gia_ObjId(p, Gia_ManCo(p, 0)) );
for ( i = 0; i < 64*nWords; i++ )
printf( "%d", Abc_InfoHasBit( (unsigned *)pSimInfo, i ) );
printf( "\n" );
// iterate through the assignments
for ( i = 0; i < 64*nWords; i++ )
{
Vec_IntClear( vVars );
for ( v = 0; v < Gia_ManObjNum(p); v++ )
{
if ( pCnf->pVarNums[v] == -1 )
continue;
pSimInfo = Gia_ManMoObj( p, v );
if ( !Abc_InfoHasBit( (unsigned *)pSimInfo, i ) )
continue;
Vec_IntPush( vVars, pCnf->pVarNums[v] );
}
//sat_solver_act_var_clear( pSat );
//sat_solver_set_polarity( pSat, Vec_IntArray(vVars), Vec_IntSize(vVars) );
clk2 = Abc_Clock();
status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
clkTotal += Abc_Clock() - clk2;
printf( "%c", status == l_True ? '+' : '-' );
if ( status == l_True )
Count++;
}
printf( "\n" );
printf( "Finished generating %d assignments. ", Count );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
Abc_PrintTime( 1, "SAT solver time", clkTotal );
Vec_WrdFreeP( &p->vSims );
Vec_IntFree( vVars );
sat_solver_delete( pSat );
Cnf_DataFree( pCnf );
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
src/sat/bmc/module.make
......@@ -16,6 +16,7 @@ SRC += src/sat/bmc/bmcBCore.c \
src/sat/bmc/bmcExpand.c \
src/sat/bmc/bmcFault.c \
src/sat/bmc/bmcFx.c \
src/sat/bmc/bmcGen.c \
src/sat/bmc/bmcICheck.c \
src/sat/bmc/bmcInse.c \
src/sat/bmc/bmcLoad.c \
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment