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

Printing formula used in &fftest.

This commit is contained in:
Alan Mishchenko 2019-07-03 00:20:59 +03:00
parent fdf0fb2783
commit 544d50c553
1 changed files with 84 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

86
src/sat/bmc/bmcFault.c
View File

@ -614,10 +614,9 @@ void Gia_FormStrTransform( char * pStr, char * pForm )
pStr[k] = 0;
}
/**Function*************************************************************
Synopsis [Implements fault model formula using functional/parameter vars.]
Synopsis [Print formula.]
Description []
@ -643,6 +642,88 @@ char * Gia_ManFormulaEndToken( char * pForm )
assert( 0 );
return NULL;
}
void Gia_ManPrintFormula_rec( char * pBeg, char * pEnd )
{
int Oper = -1;
char * pEndNew;
if ( pBeg + 1 == pEnd )
{
if ( pBeg[0] >= 'a' && pBeg[0] <= 'b' )
printf( "%c", pBeg[0] );
else if ( pBeg[0] >= 'A' && pBeg[0] <= 'B' )
printf( "~%c", pBeg[0]-'A'+'a' );
else if ( pBeg[0] >= 'p' && pBeg[0] <= 'w' ) // pqrstuvw
printf( "%c", pBeg[0] );
else if ( pBeg[0] >= 'P' && pBeg[0] <= 'W' )
printf( "~%c", pBeg[0]-'A'+'a' );
return;
}
if ( pBeg[0] == '(' )
{
pEndNew = Gia_ManFormulaEndToken( pBeg );
if ( pEndNew == pEnd )
{
assert( pBeg[0] == '(' );
assert( pBeg[pEnd-pBeg-1] == ')' );
Gia_ManPrintFormula_rec( pBeg + 1, pEnd - 1 );
return;
}
}
// get first part
pEndNew = Gia_ManFormulaEndToken( pBeg );
printf( "(" );
Gia_ManPrintFormula_rec( pBeg, pEndNew );
printf( ")" );
Oper = pEndNew[0];
// derive the formula
if ( Oper == '&' )
printf( "&" );
else if ( Oper == '|' )
printf( "|" );
else if ( Oper == '^' )
printf( "^" );
else if ( Oper == '?' )
printf( "?" );
else assert( 0 );
// get second part
pBeg = pEndNew + 1;
pEndNew = Gia_ManFormulaEndToken( pBeg );
printf( "(" );
Gia_ManPrintFormula_rec( pBeg, pEndNew );
printf( ")" );
if ( Oper == '?' )
{
printf( ":" );
// get third part
assert( Oper == '?' );
assert( pEndNew[0] == ':' );
pBeg = pEndNew + 1;
pEndNew = Gia_ManFormulaEndToken( pBeg );
printf( "(" );
Gia_ManPrintFormula_rec( pBeg, pEndNew );
printf( ")" );
}
}
void Gia_ManPrintFormula( char * pStr )
{
printf( "Using formula: " );
printf( "(" );
Gia_ManPrintFormula_rec( pStr, pStr + strlen(pStr) );
printf( ")" );
printf( "\n" );
}
/**Function*************************************************************
Synopsis [Implements fault model formula using functional/parameter vars.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManRealizeFormula_rec( Gia_Man_t * p, int * pVars, int * pPars, char * pBeg, char * pEnd, int nPars )
{
int iFans[3], Oper = -1;
@ -709,6 +790,7 @@ Gia_Man_t * Gia_ManFormulaUnfold( Gia_Man_t * p, char * pForm, int fFfOnly )
Gia_FormStrCount( pForm, &nVars, &nPars );
assert( nVars == 2 );
Gia_FormStrTransform( pStr, pForm );
Gia_ManPrintFormula( pStr );
pNew = Gia_ManStart( 5 * Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );