Updated to &sprove.

This commit is contained in:
Alan Mishchenko 2026-03-23 17:34:59 -07:00
parent ceebb2d167
commit 3881f2de37
8 changed files with 99 additions and 23 deletions

View File

@ -2157,6 +2157,8 @@ void Gia_ManFromIfGetConfig2( Vec_Str_t * vConfigs2, If_Man_t * pIfMan, word * p
{
int i, CellId;
int startPos = Vec_StrSize(vConfigs2);
If_LibCell_t * pCellLib = pIfMan && pIfMan->pPars ? pIfMan->pPars->pCellLib : NULL;
assert( pCellLib != NULL );
// Determine cell type based on the number of leaves and configuration
if ( nLeaves <= 4 ) // 7 bytes = 1 byte CellId + 4 bytes mapping + 2 bytes truth table
@ -2181,7 +2183,7 @@ void Gia_ManFromIfGetConfig2( Vec_Str_t * vConfigs2, If_Man_t * pIfMan, word * p
Truth = Gia_ManFromIfPermuteTruth4( Truth, nLeaves, z );
Vec_StrPush( vConfigs2, (char)((Truth >> 8) & 0xFF) );
Vec_StrPush( vConfigs2, (char)(Truth & 0xFF) );
assert( startPos + 7 == Vec_StrSize(vConfigs2) );
assert( startPos + pCellLib->pCellRecordSizes[CellId] == Vec_StrSize(vConfigs2) );
//Gia_ManConfigPrint( Truth, 0, nLeaves );
}
else // 12 bytes = 1 byte CellId + 7 bytes mapping + 4 bytes truth tables
@ -2226,7 +2228,7 @@ void Gia_ManFromIfGetConfig2( Vec_Str_t * vConfigs2, If_Man_t * pIfMan, word * p
Vec_StrPush( vConfigs2, (char)(Truth1 & 0xFF) );
Vec_StrPush( vConfigs2, (char)((Truth2 >> 8) & 0xFF) );
Vec_StrPush( vConfigs2, (char)(Truth2 & 0xFF) );
assert( startPos + 12 == Vec_StrSize(vConfigs2) );
assert( startPos + pCellLib->pCellRecordSizes[CellId] == Vec_StrSize(vConfigs2) );
}
else // 14 bytes = 1 byte CellId + 9 bytes mapping + 4 bytes truth tables
{
@ -2251,7 +2253,7 @@ void Gia_ManFromIfGetConfig2( Vec_Str_t * vConfigs2, If_Man_t * pIfMan, word * p
Vec_StrPush( vConfigs2, (char)(Truth1 & 0xFF) );
Vec_StrPush( vConfigs2, (char)((Truth2 >> 8) & 0xFF) );
Vec_StrPush( vConfigs2, (char)(Truth2 & 0xFF) );
assert( startPos + 14 == Vec_StrSize(vConfigs2) );
assert( startPos + pCellLib->pCellRecordSizes[CellId] == Vec_StrSize(vConfigs2) );
}
}
if ( pIfMan->pPars->fVerboseTrace )

View File

@ -33,27 +33,26 @@ ABC_NAMESPACE_IMPL_START
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
static int Gia_ManConfig2GetBytePos( Gia_Man_t * p, int iObj )
static int Gia_ManConfig2GetBytePos( Gia_Man_t * p, int iObj, If_LibCell_t * pCellLib )
{
int iLut, bytePos = 0;
if ( p == NULL || p->vConfigs2 == NULL )
if ( p == NULL || p->vConfigs2 == NULL || pCellLib == NULL )
return -1;
Gia_ManForEachLut( p, iLut )
{
unsigned char CellId;
int nRecordSize;
if ( bytePos >= Vec_StrSize(p->vConfigs2) )
return -1;
if ( iLut == iObj )
return bytePos;
CellId = (unsigned char)Vec_StrEntry( p->vConfigs2, bytePos );
if ( CellId == 0 )
bytePos += 7;
else if ( CellId == 1 )
bytePos += 12;
else if ( CellId == 2 )
bytePos += 14;
else
if ( CellId >= IF_MAX_LUTSIZE )
return -1;
nRecordSize = pCellLib->pCellRecordSizes[CellId];
if ( nRecordSize <= 0 )
return -1;
bytePos += nRecordSize;
}
return -1;
}
@ -65,7 +64,7 @@ int Gia_ManConfig2DerivePinDelays( Gia_Man_t * p, int iObj, If_LibCell_t * pCell
return 0;
for ( i = 0; i < nLutSize; i++ )
pPinDelay[i] = 1;
bytePos = Gia_ManConfig2GetBytePos( p, iObj );
bytePos = Gia_ManConfig2GetBytePos( p, iObj, pCellLib );
if ( bytePos < 0 || bytePos >= Vec_StrSize(p->vConfigs2) )
return 0;
CellId = (unsigned char)Vec_StrEntry( p->vConfigs2, bytePos );

View File

@ -203,6 +203,7 @@ struct If_LibCell_t_
char * pName; // the name of the LUT library
int nCellNum; // the number of cells in the library
int nCellInputs[IF_MAX_LUTSIZE];
int pCellRecordSizes[IF_MAX_LUTSIZE];
char * pCellNames[IF_MAX_LUTSIZE];
float pCellAreas[IF_MAX_LUTSIZE];
int pCellPinDelays[IF_MAX_LUTSIZE][IF_MAX_LUTSIZE];
@ -753,4 +754,3 @@ ABC_NAMESPACE_HEADER_END
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

View File

@ -1,6 +1,6 @@
/**CFile****************************************************************
FileName [ifDec07.c]
FileName [ifDecJ.c]
SystemName [ABC: Logic synthesis and verification system.]
@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - November 21, 2006.]
Revision [$Id: ifDec07.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
Revision [$Id: ifDecJ.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
***********************************************************************/
@ -45,9 +45,6 @@ void If_CutComputeIntrinsicJ( If_Man_t * p, word Config, int nLeaves, int * pInt
void If_PermUnpack( unsigned Value, int Pla2Var[9] )
{
}
void Gia_ManDelayTraceDump( Gia_Man_t * p, char * pFileName )
{
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

View File

@ -388,6 +388,39 @@ If_LibCell_t * If_LibCellAlloc( void )
return p;
}
/**Function*************************************************************
Synopsis [Computes the record size.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static int If_LibCellComputeRecordSize( char * pFuncDesc, int nInputs )
{
int i, nMapBytes, nRecordSize;
assert( pFuncDesc != NULL );
nMapBytes = (Abc_Base2Log(nInputs + 2) + 7) / 8;
nRecordSize = 1 + nInputs * nMapBytes;
for ( i = 0; pFuncDesc[i]; i++ )
{
int nLutVars = 0;
if ( pFuncDesc[i] != '{' )
continue;
for ( i++; pFuncDesc[i] && pFuncDesc[i] != '}'; i++ )
if ( pFuncDesc[i] >= 'a' && pFuncDesc[i] <= 'z' )
nLutVars++;
assert( nLutVars < 31 );
nRecordSize += ((1 << nLutVars) + 7) / 8;
if ( pFuncDesc[i] == 0 )
break;
}
return nRecordSize;
}
/**Function*************************************************************
Synopsis [Reads the description of cells from the cell library file.]
@ -471,6 +504,7 @@ If_LibCell_t * If_LibCellRead( char * FileName )
nInputs = maxChar - 'a' + 1;
}
p->nCellInputs[CellId] = nInputs;
p->pCellRecordSizes[CellId] = If_LibCellComputeRecordSize( FuncDesc, nInputs );
// Read Area
pToken = strtok( NULL, " \t\n" );

42
src/map/if/ifTrace.c Normal file
View File

@ -0,0 +1,42 @@
/**CFile****************************************************************
FileName [ifTrace.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [FPGA mapping based on priority cuts.]
Synopsis [Public stub for delay trace dumping.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - March 23, 2026.]
Revision [$Id: ifTrace.c,v 1.00 2026/03/23 00:00:00 alanmi Exp $]
***********************************************************************/
#include "if.h"
#include "aig/gia/gia.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
void Gia_ManDelayTraceDump( Gia_Man_t * p, char * pFileName )
{
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

View File

@ -1031,12 +1031,14 @@ void * If_ManDeriveGiaFromCells2( void * pGia )
{
Gia_Man_t * p = (Gia_Man_t *)pGia;
Gia_Man_t * pNew, * pTemp;
If_LibCell_t * pCellLib = (If_LibCell_t *)p->pCellLib;
Vec_Int_t * vCover, * vLeaves;
Gia_Obj_t * pObj;
unsigned char * pConfigData;
int k, i, iLut, iVar;
int Count = 0;
assert( p->vConfigs2 != NULL );
assert( pCellLib != NULL );
assert( Gia_ManHasMapping(p) );
// create new manager
pNew = Gia_ManStart( 6*Gia_ManObjNum(p)/5 + 100 );
@ -1078,7 +1080,7 @@ void * If_ManDeriveGiaFromCells2( void * pGia )
Truth = Abc_Tt6Stretch( Truth, 4 );
extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
Gia_ManObj(p, iLut)->Value = Kit_TruthToGia( pNew, (unsigned *)&Truth, Vec_IntSize(vLeaves), vCover, vLeaves, 1 );
bytePos += 7; // 1 byte CellId + 4 bytes mapping + 2 bytes truth table
bytePos += pCellLib->pCellRecordSizes[CellId];
}
else if ( CellId == 1 )
{
@ -1122,7 +1124,7 @@ void * If_ManDeriveGiaFromCells2( void * pGia )
iObjLit2 = Kit_TruthToGia( pNew, (unsigned *)&Truth2, Vec_IntSize(vLeavesTemp), vCover, vLeavesTemp, 1 );
Gia_ManObj(p, iLut)->Value = iObjLit2;
Vec_IntFree( vLeavesTemp );
bytePos += 12; // 1 byte CellId + 7 bytes mapping + 4 bytes truth tables
bytePos += pCellLib->pCellRecordSizes[CellId];
}
else if ( CellId == 2 )
{
@ -1177,7 +1179,7 @@ void * If_ManDeriveGiaFromCells2( void * pGia )
iObjLit3 = Gia_ManHashMux( pNew, iSelectLit, iObjLit2, iObjLit1 );
Gia_ManObj(p, iLut)->Value = iObjLit3;
Vec_IntFree( vLeavesTemp );
bytePos += 14; // 1 byte CellId + 9 bytes mapping + 4 bytes truth tables
bytePos += pCellLib->pCellRecordSizes[CellId];
}
else
{
@ -1755,4 +1757,3 @@ void Ifn_NtkRead()
ABC_NAMESPACE_IMPL_END

View File

@ -10,6 +10,7 @@ SRC += src/map/if/ifCom.c \
src/map/if/ifDec66.c \
src/map/if/ifDec75.c \
src/map/if/ifDecJ.c \
src/map/if/ifTrace.c \
src/map/if/ifDelay.c \
src/map/if/ifDsd.c \
src/map/if/ifLibBox.c \