abcBridge-0.10.0.0: abc-build/src/map/if/ifTune.c
/**CFile****************************************************************
FileName [ifTune.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [FPGA mapping based on priority cuts.]
Synopsis [Library tuning.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - November 21, 2006.]
Revision [$Id: ifTune.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
***********************************************************************/
#include "if.h"
#include "aig/gia/giaAig.h"
#include "sat/bsat/satStore.h"
#include "sat/cnf/cnf.h"
#include "misc/extra/extra.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
// network types
typedef enum {
IF_DSD_NONE = 0, // 0: unknown
IF_DSD_CONST0, // 1: constant
IF_DSD_VAR, // 2: variable
IF_DSD_AND, // 3: AND
IF_DSD_XOR, // 4: XOR
IF_DSD_MUX, // 5: MUX
IF_DSD_PRIME // 6: PRIME
} If_DsdType_t;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int If_ManStrCheck( char * pStr, int * pnVars, int * pnObjs )
{
int i, Marks[32] = {0}, MaxVar = 0, MaxDef = 0, RetValue = 1;
for ( i = 0; pStr[i]; i++ )
{
if ( pStr[i] == '=' || pStr[i] == ';' ||
pStr[i] == '(' || pStr[i] == ')' ||
pStr[i] == '[' || pStr[i] == ']' ||
pStr[i] == '<' || pStr[i] == '>' ||
pStr[i] == '{' || pStr[i] == '}' )
continue;
if ( pStr[i] >= 'a' && pStr[i] <= 'z' )
{
if ( pStr[i+1] == '=' )
Marks[pStr[i] - 'a'] = 2, MaxDef = Abc_MaxInt(MaxDef, pStr[i] - 'a');
continue;
}
printf( "String \"%s\" contains unrecognized symbol (%c).\n", pStr, pStr[i] );
RetValue = 0;
}
if ( !RetValue )
return 0;
for ( i = 0; pStr[i]; i++ )
{
if ( pStr[i] == '=' || pStr[i] == ';' ||
pStr[i] == '(' || pStr[i] == ')' ||
pStr[i] == '[' || pStr[i] == ']' ||
pStr[i] == '<' || pStr[i] == '>' ||
pStr[i] == '{' || pStr[i] == '}' )
continue;
if ( pStr[i] >= 'a' && pStr[i] <= 'z' )
{
if ( pStr[i+1] != '=' && Marks[pStr[i] - 'a'] != 2 )
Marks[pStr[i] - 'a'] = 1, MaxVar = Abc_MaxInt(MaxVar, pStr[i] - 'a');
continue;
}
printf( "String \"%s\" contains unrecognized symbol (%c).\n", pStr, pStr[i] );
RetValue = 0;
}
if ( !RetValue )
return 0;
MaxVar++;
MaxDef++;
for ( i = 0; i < MaxDef; i++ )
if ( Marks[i] == 0 )
printf( "String \"%s\" has no symbol (%c).\n", pStr, 'a' + i ), RetValue = 0;
for ( i = 0; i < MaxVar; i++ )
if ( Marks[i] == 2 )
printf( "String \"%s\" has definition of input variable (%c).\n", pStr, 'a' + i ), RetValue = 0;
for ( i = MaxVar; i < MaxDef; i++ )
if ( Marks[i] == 1 )
printf( "String \"%s\" has no definition for internal variable (%c).\n", pStr, 'a' + i ), RetValue = 0;
if ( !RetValue )
return 0;
*pnVars = MaxVar;
*pnObjs = MaxDef;
return 1;
}
int If_ManStrParse( char * pStr, int nVars, int nObjs, int * pTypes, int * pnFans, int ppFans[][6], int * pFirsts, int * pnSatVars )
{
int i, k, n, f, nPars = nVars;
char Next = 0;
assert( nVars < nObjs );
for ( i = nVars; i < nObjs; i++ )
{
for ( k = 0; pStr[k]; k++ )
if ( pStr[k] == 'a' + i && pStr[k+1] == '=' )
break;
assert( pStr[k] );
if ( pStr[k+2] == '(' )
pTypes[i] = IF_DSD_AND, Next = ')';
else if ( pStr[k+2] == '[' )
pTypes[i] = IF_DSD_XOR, Next = ']';
else if ( pStr[k+2] == '<' )
pTypes[i] = IF_DSD_MUX, Next = '>';
else if ( pStr[k+2] == '{' )
pTypes[i] = IF_DSD_PRIME, Next = '}';
else assert( 0 );
for ( n = k + 3; pStr[n]; n++ )
if ( pStr[n] == Next )
break;
assert( pStr[k] );
pnFans[i] = n - k - 3;
assert( pnFans[i] > 0 && pnFans[i] <= 6 );
for ( f = 0; f < pnFans[i]; f++ )
{
ppFans[i][f] = pStr[k + 3 + f] - 'a';
assert( ppFans[i][k] < i );
if ( ppFans[i][f] < 0 || ppFans[i][f] >= nObjs )
printf( "Error!\n" );
}
if ( pTypes[i] != IF_DSD_PRIME )
continue;
pFirsts[i] = nPars;
nPars += (1 << pnFans[i]);
}
*pnSatVars = nPars;
return 1;
}
Gia_Man_t * If_ManStrFindModel( int nVars, int nObjs, int nSatVars, int * pTypes, int * pnFans, int ppFans[][6], int * pFirsts )
{
Gia_Man_t * pNew, * pTemp;
int * pVarsPar, * pVarsObj;
int i, k, n, Step, iLit, nMints, nPars = 0;
pNew = Gia_ManStart( 1000 );
pNew->pName = Abc_UtilStrsav( "model" );
Gia_ManHashStart( pNew );
pVarsPar = ABC_ALLOC( int, nSatVars );
pVarsObj = ABC_ALLOC( int, nObjs );
for ( i = 0; i < nSatVars; i++ )
pVarsPar[i] = Gia_ManAppendCi(pNew);
for ( i = 0; i < nVars; i++ )
pVarsObj[i] = pVarsPar[nSatVars - nVars + i];
for ( i = nVars; i < nObjs; i++ )
{
if ( pTypes[i] == IF_DSD_AND )
{
iLit = 1;
for ( k = 0; k < pnFans[i]; k++ )
iLit = Gia_ManHashAnd( pNew, iLit, pVarsObj[ppFans[i][k]] );
pVarsObj[i] = iLit;
}
else if ( pTypes[i] == IF_DSD_XOR )
{
iLit = 0;
for ( k = 0; k < pnFans[i]; k++ )
iLit = Gia_ManHashXor( pNew, iLit, pVarsObj[ppFans[i][k]] );
pVarsObj[i] = iLit;
}
else if ( pTypes[i] == IF_DSD_MUX )
{
assert( pnFans[i] == 3 );
pVarsObj[i] = Gia_ManHashMux( pNew, pVarsObj[ppFans[i][0]], pVarsObj[ppFans[i][1]], pVarsObj[ppFans[i][2]] );
}
else if ( pTypes[i] == IF_DSD_PRIME )
{
int pVarsData[64];
assert( pnFans[i] >= 1 && pnFans[i] <= 6 );
nMints = (1 << pnFans[i]);
for ( k = 0; k < nMints; k++ )
pVarsData[k] = pVarsPar[nPars++];
for ( Step = 1, k = 0; k < pnFans[i]; k++, Step <<= 1 )
for ( n = 0; n < nMints; n += Step << 1 )
pVarsData[n] = Gia_ManHashMux( pNew, pVarsObj[ppFans[i][k]], pVarsData[n+Step], pVarsData[n] );
assert( Step == nMints );
pVarsObj[i] = pVarsData[0];
}
else assert( 0 );
}
assert( nPars + nVars == nSatVars );
Gia_ManAppendCo( pNew, pVarsObj[nObjs-1] );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
ABC_FREE( pVarsPar );
ABC_FREE( pVarsObj );
assert( Gia_ManPiNum(pNew) == nSatVars );
assert( Gia_ManPoNum(pNew) == 1 );
return pNew;
}
Gia_Man_t * If_ManStrFindCofactors( int nPars, Gia_Man_t * p )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, m, nMints = 1 << (Gia_ManCiNum(p) - nPars);
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
if ( i < nPars )
pObj->Value = Gia_ManAppendCi( pNew );
for ( m = 0; m < nMints; m++ )
{
Gia_ManForEachCi( p, pObj, i )
if ( i >= nPars )
pObj->Value = ((m >> (i - nPars)) & 1);
Gia_ManForEachAnd( p, pObj, i )
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManForEachPo( p, pObj, i )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
}
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p )
{
Cnf_Dat_t * pCnf;
Aig_Man_t * pAig = Gia_ManToAigSimple( p );
pAig->nRegs = 0;
pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
Aig_ManStop( pAig );
return pCnf;
}
sat_solver * If_ManStrFindSolver( Gia_Man_t * p, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars )
{
sat_solver * pSat;
Gia_Obj_t * pObj;
Cnf_Dat_t * pCnf;
int i;
pCnf = Cnf_DeriveGiaRemapped( p );
// start the SAT solver
pSat = sat_solver_new();
sat_solver_setnvars( pSat, pCnf->nVars );
// add timeframe clauses
for ( i = 0; i < pCnf->nClauses; i++ )
if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
assert( 0 );
// inputs/outputs
*pvPiVars = Vec_IntAlloc( Gia_ManPiNum(p) );
Gia_ManForEachCi( p, pObj, i )
Vec_IntPush( *pvPiVars, pCnf->pVarNums[Gia_ObjId(p, pObj)] );
*pvPoVars = Vec_IntAlloc( Gia_ManPoNum(p) );
Gia_ManForEachCo( p, pObj, i )
Vec_IntPush( *pvPoVars, pCnf->pVarNums[Gia_ObjId(p, pObj)] );
Cnf_DataFree( pCnf );
return pSat;
}
sat_solver * If_ManSatBuild( char * pStr, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars )
{
int nVars, nObjs, nSatVars;
int pTypes[32] = {0};
int pnFans[32] = {0};
int ppFans[32][6] = {{0}};
int pFirsts[32] = {0};
Gia_Man_t * p1, * p2;
sat_solver * pSat = NULL;
*pvPiVars = *pvPoVars = NULL;
if ( !If_ManStrCheck(pStr, &nVars, &nObjs) )
return NULL;
if ( !If_ManStrParse(pStr, nVars, nObjs, pTypes, pnFans, ppFans, pFirsts, &nSatVars) )
return NULL;
p1 = If_ManStrFindModel(nVars, nObjs, nSatVars, pTypes, pnFans, ppFans, pFirsts);
if ( p1 == NULL )
return NULL;
// Gia_AigerWrite( p1, "satbuild.aig", 0, 0 );
p2 = If_ManStrFindCofactors( nSatVars - nVars, p1 );
Gia_ManStop( p1 );
if ( p2 == NULL )
return NULL;
// Gia_AigerWrite( p2, "satbuild2.aig", 0, 0 );
pSat = If_ManStrFindSolver( p2, pvPiVars, pvPoVars );
Gia_ManStop( p2 );
return pSat;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void If_ManSatPrintPerm( char * pPerms, int nVars )
{
int i;
for ( i = 0; i < nVars; i++ )
printf( "%c", 'a' + pPerms[i] );
printf( "\n" );
}
int If_ManSatCheckOne( sat_solver * pSat, Vec_Int_t * vPoVars, word * pTruth, int nVars, int * pPerm, int nVarsAll, Vec_Int_t * vLits )
{
int v, Value, m, mNew, nMints = (1 << nVars);
assert( (1 << nVarsAll) == Vec_IntSize(vPoVars) );
assert( nMints <= Vec_IntSize(vPoVars) );
// remap minterms
Vec_IntFill( vLits, Vec_IntSize(vPoVars), -1 );
for ( m = 0; m < nMints; m++ )
{
mNew = 0;
for ( v = 0; v < nVarsAll; v++ )
{
assert( pPerm[v] < nVars );
if ( ((m >> pPerm[v]) & 1) )
mNew |= (1 << v);
}
assert( Vec_IntEntry(vLits, mNew) == -1 );
Vec_IntWriteEntry( vLits, mNew, Abc_TtGetBit(pTruth, m) );
}
// find assumptions
v = 0;
Vec_IntForEachEntry( vLits, Value, m )
if ( Value >= 0 )
Vec_IntWriteEntry( vLits, v++, Abc_Var2Lit(Vec_IntEntry(vPoVars, m), !Value) );
Vec_IntShrink( vLits, v );
// run SAT solver
Value = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
return (int)(Value == l_True);
}
void If_ManSatDeriveOne( sat_solver * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vValues )
{
int i, iVar;
Vec_IntClear( vValues );
Vec_IntForEachEntry( vPiVars, iVar, i )
Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) );
}
int If_ManSatCheckAll_int( sat_solver * pSat, Vec_Int_t * vPoVars, word * pTruth, int nVars, Vec_Int_t * vLits, char ** pPerms, int nPerms )
{
int pPerm[IF_MAX_FUNC_LUTSIZE];
int p, i;
for ( p = 0; p < nPerms; p++ )
{
for ( i = 0; i < nVars; i++ )
pPerm[i] = (int)pPerms[p][i];
if ( If_ManSatCheckOne(pSat, vPoVars, pTruth, nVars, pPerm, nVars, vLits) )
return p;
}
return -1;
}
int If_ManSatCheckAll( sat_solver * pSat, Vec_Int_t * vPoVars, word * pTruth, int nVars, Vec_Int_t * vLits, char ** pPerms, int nPerms )
{
abctime clk = Abc_Clock();
int RetValue = If_ManSatCheckAll_int( pSat, vPoVars, pTruth, nVars, vLits, pPerms, nPerms );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END