luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Add special handling of script-level assertions.

This commit is contained in:
Alan Mishchenko 2019-03-20 22:07:55 +02:00
parent f0efc6e098
commit 4394bc8659
1 changed files with 98 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

100
src/base/cmd/cmdApi.c
View File

@ -85,6 +85,100 @@ void Cmd_CommandAdd( Abc_Frame_t * pAbc, const char * sGroup, const char * sName
assert( !fStatus ); // the command should not be in the table
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cmd_CommandHandleSpecial( Abc_Frame_t * pAbc, const char * sCommand )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
int piCountNew = pNtk ? Abc_NtkCiNum(pNtk) : 0, piCount = 0;
int poCountNew = pNtk ? Abc_NtkCoNum(pNtk) : 0, poCount = 0;
int ndCountNew = pNtk ? Abc_NtkNodeNum(pNtk) : 0, ndCount = 0;
double AreaNew = pNtk ? Abc_NtkGetMappedArea(pNtk) : 0, Area = 0;
int DepthNew = pNtk ? Abc_NtkLevel(pNtk) : 0, Depth = 0;
if ( strstr(sCommand, "#PS") )
{
printf( "pi=%d ", piCountNew );
printf( "po=%d ", poCountNew );
printf( "fn=%d ", ndCountNew );
printf( "ma=%.1f ", AreaNew );
printf( "de=%d ", DepthNew );
printf( "\n" );
return 1;
}
if ( strstr(sCommand, "#CEC") )
{
//int proofStatus = Abc_NtkVerifyUsingCec(pNtk);
int proofStatus = 1;
// -1 (undecided), 0 (different), 1 (equivalent)
printf( "proofStatus=%d\n", proofStatus );
return 1;
}
if ( strstr(sCommand, "#ASSERT") )
{
int Status = 0;
char * pNumb = strrchr( sCommand, '=' );
if ( strstr(sCommand, "_PI_") )
{
piCount = pNumb ? atoi(pNumb+1) : 0;
if ( strstr( sCommand, "==" ) )
Status = piCountNew == piCount;
else if ( strstr( sCommand, "<=" ) )
Status = piCountNew <= piCount;
else return 0;
}
else if ( strstr(sCommand, "_PO_") )
{
poCount = pNumb ? atoi(pNumb+1) : 0;
if ( strstr( sCommand, "==" ) )
Status = poCountNew == poCount;
else if ( strstr( sCommand, "<=" ) )
Status = poCountNew <= poCount;
else return 0;
}
else if ( strstr(sCommand, "_NODE_") )
{
ndCount = pNumb ? atoi(pNumb+1) : 0;
if ( strstr( sCommand, "==" ) )
Status = ndCountNew == ndCount;
else if ( strstr( sCommand, "<=" ) )
Status = ndCountNew <= ndCount;
else return 0;
}
else if ( strstr(sCommand, "_AREA_") )
{
double Eplison = 1.0;
Area = pNumb ? atof(pNumb+1) : 0;
if ( strstr( sCommand, "==" ) )
Status = AreaNew >= Area - Eplison && AreaNew <= Area + Eplison;
else if ( strstr( sCommand, "<=" ) )
Status = AreaNew <= Area + Eplison;
else return 0;
}
else if ( strstr(sCommand, "_DEPTH_") )
{
Depth = pNumb ? atoi(pNumb+1) : 0;
if ( strstr( sCommand, "==" ) )
Status = DepthNew == Depth;
else if ( strstr( sCommand, "<=" ) )
Status = DepthNew <= Depth;
else return 0;
}
else return 0;
printf( "%s\n", Status ? "succeeded" : "failed" );
return 1;
}
return 0;
}
/**Function*************************************************************
Synopsis []
@ -107,12 +201,14 @@ int Cmd_CommandExecute( Abc_Frame_t * pAbc, const char * sCommand )
sCommandNext = sCommand;
do
{
sCommandNext = CmdSplitLine( pAbc, sCommandNext, &argc, &argv );
if ( sCommandNext[0] == '#' && Cmd_CommandHandleSpecial( pAbc, sCommandNext ) )
break;
sCommandNext = CmdSplitLine( pAbc, sCommandNext, &argc, &argv );
loop = 0;
fStatus = CmdApplyAlias( pAbc, &argc, &argv, &loop );
if ( fStatus == 0 )
fStatus = CmdCommandDispatch( pAbc, &argc, &argv );
CmdFreeArgv( argc, argv );
CmdFreeArgv( argc, argv );
}
while ( fStatus == 0 && *sCommandNext != '\0' );
return fStatus;