Skip to content

A
abc
Commit 09810301 by Alan Mishchenko
Options

Memory abstraction.

parent 37504a49
Showing with 119 additions and 16 deletions
abclib.dsp
......@@ -807,6 +807,10 @@ SOURCE=.\src\base\wlc\wlcJson.c
# End Source File
# Begin Source File
SOURCE=.\src\base\wlc\wlcMem.c
# End Source File
# Begin Source File
SOURCE=.\src\base\wlc\wlcNdr.c
# End Source File
# Begin Source File
......
src/base/abci/abc.c
......@@ -26581,6 +26581,7 @@ usage:
Abc_Print( -2, "\t a toolkit for constraint manipulation\n" );
Abc_Print( -2, "\t if constraints are absent, detect them functionally\n" );
Abc_Print( -2, "\t if constraints are present, profiles them using random simulation\n" );
Abc_Print( -2, "\t (constraints fail when any of them becomes 1 in any timeframe)\n" );
Abc_Print( -2, "\t-F num : the max number of timeframes to consider [default = %d]\n", nFrames );
Abc_Print( -2, "\t-C num : the max number of conflicts in SAT solving [default = %d]\n", nConfs );
Abc_Print( -2, "\t-P num : the max number of propagations in SAT solving [default = %d]\n", nProps );
......@@ -26818,6 +26819,7 @@ int Abc_CommandFold( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
Abc_Print( -2, "usage: fold [-cvh]\n" );
Abc_Print( -2, "\t folds constraints represented as separate outputs\n" );
Abc_Print( -2, "\t (constraints fail when any of them becomes 1 in any timeframe)\n" );
Abc_Print( -2, "\t-c : toggle complementing constraints while folding [default = %s]\n", fCompl? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
src/base/wlc/module.make
......@@ -6,6 +6,7 @@ SRC += src/base/wlc/wlcAbs.c \
src/base/wlc/wlcCom.c \
src/base/wlc/wlcGraft.c \
src/base/wlc/wlcJson.c \
src/base/wlc/wlcMem.c \
src/base/wlc/wlcNdr.c \
src/base/wlc/wlcNtk.c \
src/base/wlc/wlcReadSmt.c \
......
src/base/wlc/wlc.h
......@@ -61,7 +61,7 @@ typedef enum {
WLC_OBJ_BIT_AND, // 16: bitwise AND
WLC_OBJ_BIT_OR, // 17: bitwise OR
WLC_OBJ_BIT_XOR, // 18: bitwise XOR
WLC_OBJ_BIT_NAND, // 19: bitwise AND
WLC_OBJ_BIT_NAND, // 19: bitwise NAND
WLC_OBJ_BIT_NOR, // 20: bitwise OR
WLC_OBJ_BIT_NXOR, // 21: bitwise NXOR
WLC_OBJ_BIT_SELECT, // 22: bit selection
......@@ -161,6 +161,7 @@ struct Wlc_Ntk_t_
Vec_Int_t vBits; // object mapping into AIG nodes
Vec_Int_t vLevels; // object levels
Vec_Int_t vRefs; // object reference counters
Vec_Int_t vPoPairs; // pairs of primary outputs
};
typedef struct Wlc_Par_t_ Wlc_Par_t;
......@@ -364,6 +365,11 @@ extern int Wlc_NtkAbsCore2( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
extern Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pPars );
/*=== wlcCom.c ========================================================*/
extern void Wlc_SetNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk );
/*=== wlcMem.c ========================================================*/
extern Vec_Int_t * Wlc_NtkCollectMemory( Wlc_Ntk_t * p );
extern void Wlc_NtkPrintMemory( Wlc_Ntk_t * p );
extern Wlc_Ntk_t * Wlc_NtkMemAbstractTest( Wlc_Ntk_t * p );
extern int Wlc_NtkMemAbstract( Wlc_Ntk_t * p, int nIterMax, int fPdrVerbose, int fVerbose );
/*=== wlcNdr.c ========================================================*/
extern Wlc_Ntk_t * Wlc_ReadNdr( char * pFileName );
extern void Wlc_WriteNdr( Wlc_Ntk_t * pNtk, char * pFileName );
......@@ -380,6 +386,7 @@ extern void Wlc_ObjSetCo( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int fFlopIn
extern char * Wlc_ObjName( Wlc_Ntk_t * p, int iObj );
extern void Wlc_ObjUpdateType( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int Type );
extern void Wlc_ObjAddFanins( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vFanins );
extern int Wlc_ObjDup( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, int iObj, Vec_Int_t * vFanins );
extern void Wlc_NtkFree( Wlc_Ntk_t * p );
extern int Wlc_NtkCreateLevels( Wlc_Ntk_t * p );
extern int Wlc_NtkCreateLevelsRev( Wlc_Ntk_t * p );
......@@ -410,6 +417,7 @@ extern void Wlc_NtkDeleteSim( Vec_Ptr_t * p );
/*=== wlcStdin.c ========================================================*/
extern int Wlc_StdinProcessSmt( Abc_Frame_t * pAbc, char * pCmd );
/*=== wlcReadVer.c ========================================================*/
extern char * Wlc_PrsConvertInitValues( Wlc_Ntk_t * p );
extern Wlc_Ntk_t * Wlc_ReadVer( char * pFileName, char * pStr );
/*=== wlcUif.c ========================================================*/
extern Vec_Int_t * Wlc_NtkCollectAddMult( Wlc_Ntk_t * p, Wlc_BstPar_t * pPar, int * pCountA, int * CountM );
......
src/base/wlc/wlcNtk.c
......@@ -85,7 +85,9 @@ static char * Wlc_Names[WLC_OBJ_NUMBER+1] = {
"sqrt", // 51: integer square root
"squar", // 52: integer square
"table", // 53: bit table
NULL // 54: unused
"READ", // 54: mem read port
"WRITE", // 55: mem write port
NULL // 56: unused
};
char * Wlc_ObjTypeName( Wlc_Obj_t * p ) { return Wlc_Names[p->Type]; }
......@@ -252,6 +254,7 @@ void Wlc_NtkFree( Wlc_Ntk_t * p )
Mem_FlexStop( p->pMemFanin, 0 );
if ( p->pMemTable )
Mem_FlexStop( p->pMemTable, 0 );
ABC_FREE( p->vPoPairs.pArray );
Vec_PtrFreeP( &p->vTables );
ABC_FREE( p->vPis.pArray );
ABC_FREE( p->vPos.pArray );
......@@ -466,6 +469,8 @@ void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fTwoSides, int fVerbose )
pObj->Type == WLC_OBJ_BIT_NOT || pObj->Type == WLC_OBJ_LOGIC_NOT || pObj->Type == WLC_OBJ_ARI_MINUS )
Sign = Wlc_NtkPrintDistribMakeSign( Wlc_ObjSign(pObj), Wlc_ObjSign(Wlc_ObjFanin0(p, pObj)), 0 );
// 2-input types (including MUX)
else if ( Wlc_ObjFaninNum(pObj) == 0 )
printf( "Object %d with name \"%s\" has type 0. Looks like it was declared by not defined...\n", i, Wlc_ObjName(p, i) );
else if ( Wlc_ObjFaninNum(pObj) == 1 )
Sign = Wlc_NtkPrintDistribMakeSign( Wlc_ObjSign(pObj), Wlc_ObjSign(Wlc_ObjFanin0(p, pObj)), 0 );
else
......@@ -620,6 +625,16 @@ void Wlc_NtkPrintNode( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )
{
printf( "%8d : ", Wlc_ObjId(p, pObj) );
printf( "%3d%s", Wlc_ObjRange(pObj), Wlc_ObjIsSigned(pObj) ? "s" : " " );
if ( pObj->Type == WLC_OBJ_PI )
{
printf( " PI\n" );
return;
}
if ( pObj->Type == WLC_OBJ_FO )
{
printf( " FO\n" );
return;
}
if ( pObj->Type == WLC_OBJ_CONST )
printf( " " );
else
......@@ -914,6 +929,8 @@ Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq )
if ( p->pSpec )
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Wlc_NtkTransferNames( pNew, p );
if ( Vec_IntSize(&p->vPoPairs) )
Vec_IntAppend( &pNew->vPoPairs, &p->vPoPairs );
return pNew;
}
Wlc_Ntk_t * Wlc_NtkDupDfsAbs( Wlc_Ntk_t * p, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops )
......
src/base/wlc/wlcReadVer.c
......@@ -42,6 +42,7 @@ struct Wlc_Prs_t_
Wlc_Ntk_t * pNtk;
Mem_Flex_t * pMemTable;
Vec_Ptr_t * vTables;
Vec_Str_t * vPoPairs;
int nConsts;
int nNonZero[4];
int nNegative[4];
......@@ -97,6 +98,7 @@ void Wlc_PrsStop( Wlc_Prs_t * p )
Wlc_NtkFree( p->pNtk );
if ( p->pMemTable )
Mem_FlexStop( p->pMemTable, 0 );
Vec_StrFreeP( &p->vPoPairs );
Vec_PtrFreeP( &p->vTables );
Vec_IntFree( p->vLines );
Vec_IntFree( p->vStarts );
......@@ -235,6 +237,20 @@ int Wlc_PrsRemoveComments( Wlc_Prs_t * p )
{
if ( pCur + 5 < pEnd && pCur[2] == 'a' && pCur[3] == 'b' && pCur[4] == 'c' && pCur[5] == '2' )
pCur[0] = pCur[1] = pCur[2] = pCur[3] = pCur[4] = pCur[5] = ' ';
else if ( !strncmp(pCur + 3, "Pair:", 5) )
{
if ( p->vPoPairs == NULL )
p->vPoPairs = Vec_StrAlloc( 100 );
for ( pNext = pCur + 9; *pNext != '\n'; pNext++ )
{
if ( *pNext == ' ' )
Vec_StrPush( p->vPoPairs, '\0' );
else if ( *pNext != '\r' )
Vec_StrPush( p->vPoPairs, *pNext );
}
if ( Vec_StrEntryLast(p->vPoPairs) != 0 )
Vec_StrPush(p->vPoPairs, 0);
}
else
{
pNext = Wlc_PrsFindSymbol( pCur, '\n' );
......@@ -507,7 +523,7 @@ static inline char * Wlc_PrsFindName( char * pStr, char ** ppPlace )
{
static char Buffer[WLV_PRS_MAX_LINE];
char * pThis = *ppPlace = Buffer;
int fNotName = 1;
int fNotName = 1, Count = 0;
pStr = Wlc_PrsSkipSpaces( pStr );
if ( !Wlc_PrsIsChar(pStr) )
return NULL;
......@@ -518,9 +534,16 @@ static inline char * Wlc_PrsFindName( char * pStr, char ** ppPlace )
if ( fNotName && !Wlc_PrsIsChar(pStr) )
break;
if ( *pStr == '\\' )
{
Count++;
fNotName = 0;
}
else if ( !fNotName && *pStr == ' ' )
fNotName = 1;
{
Count--;
if ( !Count )
fNotName = 1;
}
*pThis++ = *pStr++;
}
*pThis = 0;
......@@ -1008,6 +1031,25 @@ startword:
p->pNtk->pInits = Wlc_PrsConvertInitValues( p->pNtk );
//printf( "%s", p->pNtk->pInits );
}
if ( p->vPoPairs )
{
assert( Vec_StrEntryLast(p->vPoPairs) == 0 );
Vec_StrPush( p->vPoPairs, 0 );
pName = Vec_StrArray(p->vPoPairs);
while ( *pName )
{
Wlc_NtkForEachPo( p->pNtk, pObj, i )
if ( !strcmp(Wlc_ObjName(p->pNtk, Wlc_ObjId(p->pNtk, pObj)), pName) )
{
Vec_IntPush( &p->pNtk->vPoPairs, i );
break;
}
assert( i < Wlc_NtkPoNum(p->pNtk) );
pName += strlen(pName) + 1;
}
assert( Vec_IntSize(&p->pNtk->vPoPairs) % 2 == 0 );
printf( "Finished parsing %d output pairs to be checked for equivalence.\n", Vec_IntSize(&p->pNtk->vPoPairs)/2 );
}
break;
}
// these are read as part of the interface
......@@ -1211,13 +1253,13 @@ startword:
pObj = Wlc_NtkObj( p->pNtk, NameIdOut );
Wlc_ObjUpdateType( p->pNtk, pObj, WLC_OBJ_FO );
Vec_IntPush( &p->pNtk->vFfs, NameIdOut );
if ( nBits != Wlc_ObjRange(pObj) )
printf( "Warning! Flop input has bit-width (%d) that differs from the flop declaration (%d)\n", Wlc_ObjRange(pObj), nBits );
//if ( nBits != Wlc_ObjRange(pObj) )
// printf( "Warning! Flop output \"%s\" has bit-width (%d) that differs from the flop declaration (%d)\n", Abc_NamStr(p->pNtk->pManName, NameIdOut), Wlc_ObjRange(pObj), nBits );
// create flop input
pObj = Wlc_NtkObj( p->pNtk, NameIdIn );
Vec_IntPush( &p->pNtk->vFfs, NameIdIn );
if ( nBits != Wlc_ObjRange(pObj) )
printf( "Warning! Flop output has bit-width (%d) that differs from the flop declaration (%d)\n", Wlc_ObjRange(pObj), nBits );
//if ( nBits != Wlc_ObjRange(pObj) )
// printf( "Warning! Flop input \"%s\" has bit-width (%d) that differs from the flop declaration (%d)\n", Abc_NamStr(p->pNtk->pManName, NameIdIn), Wlc_ObjRange(pObj), nBits );
// save flop init value
if ( NameId == -1 )
printf( "Initial value of flop \"%s\" is not specified. Zero is assumed.\n", Abc_NamStr(p->pNtk->pManName, NameIdOut) );
......@@ -1225,11 +1267,13 @@ startword:
{
pObj = Wlc_NtkObj( p->pNtk, NameId );
if ( nBits != Wlc_ObjRange(pObj) )
printf( "Warning! Flop init signal bit-width (%d) is different from the flop declaration (%d)\n", Wlc_ObjRange(pObj), nBits );
printf( "Warning! Flop init signal \"%s\" bit-width (%d) is different from the flop declaration (%d)\n", Abc_NamStr(p->pNtk->pManName, NameId), Wlc_ObjRange(pObj), nBits );
}
if ( p->pNtk->vInits == NULL )
p->pNtk->vInits = Vec_IntAlloc( 100 );
Vec_IntPush( p->pNtk->vInits, NameId > 0 ? NameId : -nBits );
// printf( "Created flop %s with range %d and init value %d (nameId = %d)\n",
// Abc_NamStr(p->pNtk->pManName, NameIdOut), Wlc_ObjRange(pObj), nBits, NameId );
}
else if ( Wlc_PrsStrCmp( pStart, "CPL_MEM_" ) )
{
......@@ -1277,6 +1321,7 @@ startword:
Vec_IntPush( p->vFanins, NameAddr );
if ( !fRead )
Vec_IntPush( p->vFanins, NameDi );
//printf( "Memory %s ", fRead ? "Read" : "Write" ); printf( "Fanins: " ); Vec_IntPrint( p->vFanins );
Wlc_ObjAddFanins( p->pNtk, pObj, p->vFanins );
}
else if ( pStart[0] == '(' && pStart[1] == '*' ) // skip comments
......@@ -1326,8 +1371,11 @@ Wlc_Ntk_t * Wlc_ReadVer( char * pFileName, char * pStr )
if ( !Wlc_PrsDerive( p ) )
goto finish;
// derive topological order
pNtk = Wlc_NtkDupDfs( p->pNtk, 0, 1 );
pNtk->pSpec = Abc_UtilStrsav( pFileName );
if ( p->pNtk )
{
pNtk = Wlc_NtkDupDfs( p->pNtk, 0, 1 );
pNtk->pSpec = Abc_UtilStrsav( pFileName );
}
finish:
Wlc_PrsPrintErrorMessage( p );
Wlc_PrsStop( p );
......
src/base/wlc/wlcShow.c
......@@ -49,7 +49,7 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
Wlc_Obj_t * pNode;
int LevelMax, Prev, Level, i;
if ( Wlc_NtkObjNum(p) > 2000 )
if ( vBold ? (Vec_IntSize(vBold) > 2000) : (Wlc_NtkObjNum(p) > 2000) )
{
fprintf( stdout, "Cannot visualize WLC with more than %d nodes.\n", 2000 );
return;
......@@ -159,6 +159,8 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
// generate the CO nodes
Wlc_NtkForEachCo( p, pNode, i )
{
if ( vBold && !pNode->Mark )
continue;
pNode = Wlc_ObjCo2PoFo(p, i);
fprintf( pFile, " NodePo%d [label = \"%s_in %d\"", Wlc_ObjId(p, pNode), Wlc_ObjName(p, Wlc_ObjId(p, pNode)), Wlc_ObjRange(pNode) );
fprintf( pFile, ", shape = %s", i < Wlc_NtkPoNum(p) ? "invtriangle" : "box" );
......@@ -180,11 +182,20 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
{
if ( (int)Wlc_ObjLevel(p, pNode) != Level )
continue;
if ( vBold && !pNode->Mark )
continue;
if ( pNode->Type == WLC_OBJ_CONST )
{
fprintf( pFile, " Node%d [label = \"0x", i );
Abc_TtPrintHexArrayRev( pFile, (word *)Wlc_ObjConstValue(pNode), (Wlc_ObjRange(pNode) + 3) / 4 );
//char * pName = Wlc_ObjName(p, i);
fprintf( pFile, " Node%d [label = \"%d\'h", i, Wlc_ObjRange(pNode) );
if ( Wlc_ObjRange(pNode) > 64 )
{
Abc_TtPrintHexArrayRev( pFile, (word *)Wlc_ObjConstValue(pNode), 16 );
fprintf( pFile, "..." );
}
else
Abc_TtPrintHexArrayRev( pFile, (word *)Wlc_ObjConstValue(pNode), (Wlc_ObjRange(pNode) + 3) / 4 );
fprintf( pFile, "\"" );
}
else if ( pNode->Type == WLC_OBJ_BUF || pNode->Type == WLC_OBJ_MUX )
......@@ -224,6 +235,8 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
// generate the CI nodes
Wlc_NtkForEachCi( p, pNode, i )
{
if ( vBold && !pNode->Mark )
continue;
fprintf( pFile, " Node%d [label = \"%s %d\"", Wlc_ObjId(p, pNode), Wlc_ObjName(p, Wlc_ObjId(p, pNode)), Wlc_ObjRange(pNode) );
fprintf( pFile, ", shape = %s", i < Wlc_NtkPiNum(p) ? "triangle" : "box" );
fprintf( pFile, ", color = coral, fillcolor = coral" );
......@@ -237,6 +250,8 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
fprintf( pFile, "title1 -> title2 [style = invis];\n" );
Wlc_NtkForEachCo( p, pNode, i )
{
if ( vBold && !pNode->Mark )
continue;
pNode = Wlc_ObjCo2PoFo( p, i );
fprintf( pFile, "title2 -> NodePo%d [style = invis];\n", Wlc_ObjId(p, pNode) );
}
......@@ -245,7 +260,9 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
Wlc_NtkForEachCo( p, pNode, i )
{
pNode = Wlc_ObjCo2PoFo( p, i );
if ( i > 0 )
if ( vBold && !pNode->Mark )
continue;
if ( Prev >= 0 )
fprintf( pFile, "NodePo%d -> NodePo%d [style = invis];\n", Prev, Wlc_ObjId(p, pNode) );
Prev = Wlc_ObjId(p, pNode);
}
......@@ -253,7 +270,9 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
Prev = -1;
Wlc_NtkForEachCi( p, pNode, i )
{
if ( i > 0 )
if ( vBold && !pNode->Mark )
continue;
if ( Prev >= 0 )
fprintf( pFile, "Node%d -> Node%d [style = invis];\n", Prev, Wlc_ObjId(p, pNode) );
Prev = Wlc_ObjId(p, pNode);
}
......@@ -261,6 +280,8 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
// generate edges
Wlc_NtkForEachCo( p, pNode, i )
{
if ( vBold && !pNode->Mark )
continue;
fprintf( pFile, "NodePo%d", Wlc_ObjId(p, Wlc_ObjCo2PoFo(p, i)) );
fprintf( pFile, " -> " );
fprintf( pFile, "Node%d", Wlc_ObjId(p, pNode) );
......@@ -274,6 +295,8 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
int k, iFanin;
if ( Wlc_ObjIsCi(pNode) )
continue;
if ( vBold && !pNode->Mark )
continue;
// generate the edge from this node to the next
Wlc_ObjForEachFanin( pNode, iFanin, k )
{
......
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