mirror of https://github.com/YosysHQ/abc.git
Merge remote-tracking branch 'upstream/master' into yosys-experimental
This commit is contained in:
Miodrag Milanovic
commit
89b0b366a2
2
Makefile
2
Makefile
|
|
@ -35,7 +35,7 @@ OS := $(shell uname -s)
|
|||
MODULES := \
|
||||
$(wildcard src/ext*) \
|
||||
src/base/abc src/base/abci src/base/cmd src/base/io src/base/main src/base/exor \
|
||||
src/base/ver src/base/wlc src/base/wln src/base/acb src/base/pla src/base/test \
|
||||
src/base/ver src/base/wlc src/base/wln src/base/sn src/base/acb src/base/pla src/base/test \
|
||||
src/map/mapper src/map/mio src/map/super src/map/if src/map/if/acd \
|
||||
src/map/amap src/map/cov src/map/scl src/map/mpm src/map/emap \
|
||||
src/misc/extra src/misc/mvc src/misc/st src/misc/util src/misc/nm \
|
||||
|
|
|
|||
80
abclib.dsp
80
abclib.dsp
|
|
@ -971,10 +971,6 @@ SOURCE=.\src\base\acb\acbAig.c
|
|||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\acb\acbCom.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\acb\acbFunc.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
|
@ -1008,6 +1004,14 @@ SOURCE=.\src\base\acb\acbUtil.c
|
|||
# End Group
|
||||
# Begin Group "wln"
|
||||
|
||||
SOURCE=.\src\base\acb\acbXec.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\acb\acbXec.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
# PROP Default_Filter ""
|
||||
# Begin Source File
|
||||
|
||||
|
|
@ -1066,6 +1070,74 @@ SOURCE=.\src\base\wln\wlnWlc.c
|
|||
SOURCE=.\src\base\wln\wlnWriteVer.c
|
||||
# End Source File
|
||||
# End Group
|
||||
# Begin Group "sn"
|
||||
|
||||
# PROP Default_Filter ""
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\sn\sn.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\sn\snTech.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\sn\snMapDsp.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\sn\snMapMem.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\sn\snMapAdd.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\sn\snMapTech.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\sn\snCheck.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\sn\snBoundary.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\sn\snMapLut.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\sn\snPth.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\sn\snBlast.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\sn\snMiniAig.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\sn\snMiniLut.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\sn\snMiniGate.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\sn\snMux.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\sn\snCom.c
|
||||
# End Source File
|
||||
# End Group
|
||||
# End Group
|
||||
# Begin Group "bdd"
|
||||
|
||||
|
|
|
|||
|
|
@ -351,6 +351,20 @@ static int Mini_AigAndMulti( Mini_Aig_t * p, int * pLits, int nLits )
|
|||
}
|
||||
return pLits[0];
|
||||
}
|
||||
static int Mini_AigXorMulti( Mini_Aig_t * p, int * pLits, int nLits )
|
||||
{
|
||||
int i;
|
||||
assert( nLits > 0 );
|
||||
while ( nLits > 1 )
|
||||
{
|
||||
for ( i = 0; i < nLits/2; i++ )
|
||||
pLits[i] = Mini_AigXor(p, pLits[2*i], pLits[2*i+1]);
|
||||
if ( nLits & 1 )
|
||||
pLits[i++] = pLits[nLits-1];
|
||||
nLits = i;
|
||||
}
|
||||
return pLits[0];
|
||||
}
|
||||
static int Mini_AigMuxMulti( Mini_Aig_t * p, int * pCtrl, int nCtrl, int * pData, int nData )
|
||||
{
|
||||
int i, c;
|
||||
|
|
@ -847,4 +861,3 @@ ABC_NAMESPACE_HEADER_END
|
|||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
|
|
|||
|
|
@ -7813,14 +7813,17 @@ usage:
|
|||
***********************************************************************/
|
||||
int Abc_CommandRunTest( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||
{
|
||||
extern void Acb_NtkRunTest( char * pFileNames[4], int fFancy, int fVerbose );
|
||||
extern void Acb_NtkRunTest( char * pFileNames[4], int fFancy, int fVerbose, int fUseCadical );
|
||||
char * pFileNames[4] = {NULL};
|
||||
int c, fFancy = 0, fVerbose = 0;
|
||||
int c, fFancy = 0, fVerbose = 0, fUseCadical = 0;
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "fvh" ) ) != EOF )
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "cfvh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
case 'c':
|
||||
fUseCadical ^= 1;
|
||||
break;
|
||||
case 'f':
|
||||
fFancy ^= 1;
|
||||
break;
|
||||
|
|
@ -7840,12 +7843,13 @@ int Abc_CommandRunTest( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
}
|
||||
for ( c = 0; c < argc - globalUtilOptind; c++ )
|
||||
pFileNames[c] = argv[globalUtilOptind+c];
|
||||
Acb_NtkRunTest( pFileNames, fFancy, fVerbose );
|
||||
Acb_NtkRunTest( pFileNames, fFancy, fVerbose, fUseCadical );
|
||||
return 0;
|
||||
|
||||
usage:
|
||||
Abc_Print( -2, "usage: xec [-fvh] <file1> <file2>\n" );
|
||||
Abc_Print( -2, "usage: xec [-cfvh] <file1> <file2>\n" );
|
||||
Abc_Print( -2, "\t combinational equivalence checking with x-values\n" );
|
||||
Abc_Print( -2, "\t-c : toggle using CaDiCaL SAT-only solving [default = %s]\n", fUseCadical? "yes": "no" );
|
||||
Abc_Print( -2, "\t-f : toggle using experimental feature [default = %s]\n", fFancy? "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");
|
||||
|
|
@ -43736,6 +43740,29 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileNam
|
|||
return pGia;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Returns 1 if all outputs of the swept miter are constant 0.]
|
||||
|
||||
Description [The equivalence check below concludes from the swept miter
|
||||
having no AND nodes. An AND-free GIA can still have outputs that are
|
||||
constant 1 or CI literals, which are satisfiable, so the outputs are
|
||||
checked here as well.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static int Abc_CecSweptMiterIsConst0( Gia_Man_t * p )
|
||||
{
|
||||
int i;
|
||||
for ( i = 0; i < Gia_ManPoNum(p); i++ )
|
||||
if ( !Gia_ManPoIsConst0(p, i) )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
|
@ -44164,10 +44191,12 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
abctime clk = Abc_Clock();
|
||||
extern Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose );
|
||||
Gia_Man_t * pNew = Cec4_ManSimulateTest3( pMiter, pPars->nBTLimit, pPars->fVerbose );
|
||||
if ( Gia_ManAndNum(pNew) == 0 )
|
||||
if ( Gia_ManAndNum(pNew) != 0 )
|
||||
Abc_Print( 1, "Networks are UNDECIDED. " );
|
||||
else if ( Abc_CecSweptMiterIsConst0(pNew) )
|
||||
Abc_Print( 1, "Networks are equivalent. " );
|
||||
else
|
||||
Abc_Print( 1, "Networks are UNDECIDED. " );
|
||||
Abc_Print( 1, "Networks are NOT equivalent. " );
|
||||
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
|
||||
Gia_ManStop( pNew );
|
||||
}
|
||||
|
|
@ -44176,10 +44205,12 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
abctime clk = Abc_Clock();
|
||||
extern Gia_Man_t * Cec5_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose );
|
||||
Gia_Man_t * pNew = Cec5_ManSimulateTest3( pMiter, pPars->nBTLimit, pPars->fVerbose );
|
||||
if ( Gia_ManAndNum(pNew) == 0 )
|
||||
if ( Gia_ManAndNum(pNew) != 0 )
|
||||
Abc_Print( 1, "Networks are UNDECIDED. " );
|
||||
else if ( Abc_CecSweptMiterIsConst0(pNew) )
|
||||
Abc_Print( 1, "Networks are equivalent. " );
|
||||
else
|
||||
Abc_Print( 1, "Networks are UNDECIDED. " );
|
||||
Abc_Print( 1, "Networks are NOT equivalent. " );
|
||||
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
|
||||
Gia_ManStop( pNew );
|
||||
}
|
||||
|
|
@ -44380,10 +44411,12 @@ int Abc_CommandAbc9ICec( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
abctime clk = Abc_Clock();
|
||||
extern Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose );
|
||||
Gia_Man_t * pNew = Cec4_ManSimulateTest3( pMiter, pPars->nBTLimit, pPars->fVerbose );
|
||||
if ( Gia_ManAndNum(pNew) == 0 )
|
||||
if ( Gia_ManAndNum(pNew) != 0 )
|
||||
Abc_Print( 1, "Networks are UNDECIDED. " );
|
||||
else if ( Abc_CecSweptMiterIsConst0(pNew) )
|
||||
Abc_Print( 1, "Networks are equivalent. " );
|
||||
else
|
||||
Abc_Print( 1, "Networks are UNDECIDED. " );
|
||||
Abc_Print( 1, "Networks are NOT equivalent. " );
|
||||
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
|
||||
Gia_ManStop( pNew );
|
||||
}
|
||||
|
|
|
|||
|
|
@ -670,13 +670,29 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtkAdd )
|
|||
extern int Abc_NodeCompareCiCo( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew );
|
||||
if ( !Abc_NodeCompareCiCo(pNtk, (Abc_Ntk_t *)Vec_PtrEntry(vStore, 0)) )
|
||||
{
|
||||
// Abc_NtkCompareSignals() sorts the PIs/POs/boxes of both networks by name as a
|
||||
// side effect, which is what makes the comparison meaningful when the two do use
|
||||
// the same names. When they do not, the comparison fails, the store is reset and
|
||||
// this network is kept -- so the sort has to be undone here. Otherwise the stored
|
||||
// network is a permutation of the one the caller read in, and everything after it
|
||||
// is off by that permutation with nothing to indicate it.
|
||||
Vec_Ptr_t * vPis = Vec_PtrDup( pNtk->vPis );
|
||||
Vec_Ptr_t * vPos = Vec_PtrDup( pNtk->vPos );
|
||||
Vec_Ptr_t * vBoxes = Vec_PtrDup( pNtk->vBoxes );
|
||||
// reorder PIs of pNtk2 according to pNtk1
|
||||
if ( !Abc_NtkCompareSignals( pNtk, (Abc_Ntk_t *)Vec_PtrEntry(vStore, 0), 1, 1 ) )
|
||||
{
|
||||
Vec_PtrFree( pNtk->vPis ); pNtk->vPis = vPis; vPis = NULL;
|
||||
Vec_PtrFree( pNtk->vPos ); pNtk->vPos = vPos; vPos = NULL;
|
||||
Vec_PtrFree( pNtk->vBoxes ); pNtk->vBoxes = vBoxes; vBoxes = NULL;
|
||||
Abc_NtkOrderCisCos( pNtk );
|
||||
printf( "Trying to store the network with different primary inputs.\n" );
|
||||
printf( "The previously stored networks are deleted and this one is added.\n" );
|
||||
Abc_NtkFraigStoreClean();
|
||||
}
|
||||
if ( vPis ) Vec_PtrFree( vPis );
|
||||
if ( vPos ) Vec_PtrFree( vPos );
|
||||
if ( vBoxes ) Vec_PtrFree( vBoxes );
|
||||
}
|
||||
}
|
||||
Vec_PtrPush( vStore, pNtk );
|
||||
|
|
|
|||
|
|
@ -1,735 +0,0 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [acbCom.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Hierarchical word-level netlist.]
|
||||
|
||||
Synopsis [Command handlers.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - November 29, 2014.]
|
||||
|
||||
Revision [$Id: acbCom.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "acb.h"
|
||||
#include "proof/cec/cec.h"
|
||||
#include "base/main/mainInt.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
#if 0
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
static int Acb_CommandRead ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Acb_CommandWrite ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Acb_CommandPs ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Acb_CommandPut ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Acb_CommandGet ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Acb_CommandClp ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Acb_CommandBlast ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Acb_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Acb_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
|
||||
static inline Acb_Man_t * Acb_AbcGetMan( Abc_Frame_t * pAbc ) { return (Acb_Man_t *)pAbc->pAbcCba; }
|
||||
static inline void Acb_AbcFreeMan( Abc_Frame_t * pAbc ) { if ( pAbc->pAbcCba ) Acb_ManFree(Acb_AbcGetMan(pAbc)); }
|
||||
static inline void Acb_AbcUpdateMan( Abc_Frame_t * pAbc, Acb_Man_t * p ) { Acb_AbcFreeMan(pAbc); pAbc->pAbcCba = p; }
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function********************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
******************************************************************************/
|
||||
void Acb_Init( Abc_Frame_t * pAbc )
|
||||
{
|
||||
Cmd_CommandAdd( pAbc, "New word level", "@read", Acb_CommandRead, 0 );
|
||||
Cmd_CommandAdd( pAbc, "New word level", "@write", Acb_CommandWrite, 0 );
|
||||
Cmd_CommandAdd( pAbc, "New word level", "@ps", Acb_CommandPs, 0 );
|
||||
Cmd_CommandAdd( pAbc, "New word level", "@put", Acb_CommandPut, 0 );
|
||||
Cmd_CommandAdd( pAbc, "New word level", "@get", Acb_CommandGet, 0 );
|
||||
Cmd_CommandAdd( pAbc, "New word level", "@clp", Acb_CommandClp, 0 );
|
||||
Cmd_CommandAdd( pAbc, "New word level", "@blast", Acb_CommandBlast, 0 );
|
||||
Cmd_CommandAdd( pAbc, "New word level", "@cec", Acb_CommandCec, 0 );
|
||||
Cmd_CommandAdd( pAbc, "New word level", "@test", Acb_CommandTest, 0 );
|
||||
}
|
||||
|
||||
/**Function********************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
******************************************************************************/
|
||||
void Acb_End( Abc_Frame_t * pAbc )
|
||||
{
|
||||
Acb_AbcFreeMan( pAbc );
|
||||
}
|
||||
|
||||
|
||||
/**Function********************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
******************************************************************************/
|
||||
int Acb_CommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||
{
|
||||
FILE * pFile;
|
||||
Acb_Man_t * p = NULL;
|
||||
char * pFileName = NULL;
|
||||
int c, fTest = 0, fDfs = 0, fVerbose = 0;
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "tdvh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
case 't':
|
||||
fTest ^= 1;
|
||||
break;
|
||||
case 'd':
|
||||
fDfs ^= 1;
|
||||
break;
|
||||
case 'v':
|
||||
fVerbose ^= 1;
|
||||
break;
|
||||
case 'h':
|
||||
goto usage;
|
||||
default:
|
||||
goto usage;
|
||||
}
|
||||
}
|
||||
if ( argc != globalUtilOptind + 1 )
|
||||
{
|
||||
printf( "Acb_CommandRead(): Input file name should be given on the command line.\n" );
|
||||
return 0;
|
||||
}
|
||||
// get the file name
|
||||
pFileName = argv[globalUtilOptind];
|
||||
if ( (pFile = fopen( pFileName, "r" )) == NULL )
|
||||
{
|
||||
Abc_Print( 1, "Cannot open input file \"%s\". ", pFileName );
|
||||
if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".v", ".blif", ".smt", ".acb", NULL )) )
|
||||
Abc_Print( 1, "Did you mean \"%s\"?", pFileName );
|
||||
Abc_Print( 1, "\n" );
|
||||
return 0;
|
||||
}
|
||||
fclose( pFile );
|
||||
if ( fTest )
|
||||
{
|
||||
if ( !strcmp( Extra_FileNameExtension(pFileName), "blif" ) )
|
||||
Prs_ManReadBlifTest( pFileName );
|
||||
else if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) )
|
||||
Prs_ManReadVerilogTest( pFileName );
|
||||
else
|
||||
{
|
||||
printf( "Unrecognized input file extension.\n" );
|
||||
return 0;
|
||||
}
|
||||
return 0;
|
||||
}
|
||||
if ( !strcmp( Extra_FileNameExtension(pFileName), "blif" ) )
|
||||
p = Acb_ManReadBlif( pFileName );
|
||||
else if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) )
|
||||
p = Acb_ManReadVerilog( pFileName );
|
||||
else if ( !strcmp( Extra_FileNameExtension(pFileName), "acb" ) )
|
||||
p = Acb_ManReadCba( pFileName );
|
||||
else
|
||||
{
|
||||
printf( "Unrecognized input file extension.\n" );
|
||||
return 0;
|
||||
}
|
||||
if ( fDfs )
|
||||
{
|
||||
Acb_Man_t * pTemp;
|
||||
p = Acb_ManDup( pTemp = p, Acb_NtkCollectDfs );
|
||||
Acb_ManFree( pTemp );
|
||||
}
|
||||
Acb_AbcUpdateMan( pAbc, p );
|
||||
return 0;
|
||||
usage:
|
||||
Abc_Print( -2, "usage: @read [-tdvh] <file_name>\n" );
|
||||
Abc_Print( -2, "\t reads hierarchical design\n" );
|
||||
Abc_Print( -2, "\t-t : toggle testing the parser [default = %s]\n", fTest? "yes": "no" );
|
||||
Abc_Print( -2, "\t-d : toggle computing DFS ordering [default = %s]\n", fDfs? "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");
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function********************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
******************************************************************************/
|
||||
int Acb_CommandWrite( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||
{
|
||||
Acb_Man_t * p = Acb_AbcGetMan(pAbc);
|
||||
char * pFileName = NULL;
|
||||
int fInclineCats = 0;
|
||||
int c, fVerbose = 0;
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "cvh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
case 'c':
|
||||
fInclineCats ^= 1;
|
||||
break;
|
||||
case 'v':
|
||||
fVerbose ^= 1;
|
||||
break;
|
||||
case 'h':
|
||||
goto usage;
|
||||
default:
|
||||
goto usage;
|
||||
}
|
||||
}
|
||||
if ( p == NULL )
|
||||
{
|
||||
Abc_Print( 1, "Acb_CommandWrite(): There is no current design.\n" );
|
||||
return 0;
|
||||
}
|
||||
|
||||
if ( argc == globalUtilOptind + 1 )
|
||||
pFileName = argv[globalUtilOptind];
|
||||
else if ( argc == globalUtilOptind && p )
|
||||
{
|
||||
pFileName = Extra_FileNameGenericAppend( Acb_ManSpec(p) ? Acb_ManSpec(p) : Acb_ManName(p), "_out.v" );
|
||||
printf( "Generated output file name \"%s\".\n", pFileName );
|
||||
}
|
||||
else
|
||||
{
|
||||
printf( "Output file name should be given on the command line.\n" );
|
||||
return 0;
|
||||
}
|
||||
// perform writing
|
||||
if ( !strcmp( Extra_FileNameExtension(pFileName), "blif" ) )
|
||||
Acb_ManWriteBlif( pFileName, p );
|
||||
else if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) )
|
||||
Acb_ManWriteVerilog( pFileName, p, fInclineCats );
|
||||
else if ( !strcmp( Extra_FileNameExtension(pFileName), "acb" ) )
|
||||
Acb_ManWriteCba( pFileName, p );
|
||||
else
|
||||
{
|
||||
printf( "Unrecognized output file extension.\n" );
|
||||
return 0;
|
||||
}
|
||||
return 0;
|
||||
usage:
|
||||
Abc_Print( -2, "usage: @write [-cvh]\n" );
|
||||
Abc_Print( -2, "\t writes the design into a file in BLIF or Verilog\n" );
|
||||
Abc_Print( -2, "\t-c : toggle inlining input concatenations [default = %s]\n", fInclineCats? "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");
|
||||
return 1;
|
||||
}
|
||||
|
||||
|
||||
/**Function********************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
******************************************************************************/
|
||||
int Acb_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||
{
|
||||
Acb_Man_t * p = Acb_AbcGetMan(pAbc);
|
||||
int nModules = 0;
|
||||
int fShowMulti = 0;
|
||||
int fShowAdder = 0;
|
||||
int fDistrib = 0;
|
||||
int c, fVerbose = 0;
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "Mmadvh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
case 'M':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
nModules = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( nModules < 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'm':
|
||||
fShowMulti ^= 1;
|
||||
break;
|
||||
case 'a':
|
||||
fShowAdder ^= 1;
|
||||
break;
|
||||
case 'd':
|
||||
fDistrib ^= 1;
|
||||
break;
|
||||
case 'v':
|
||||
fVerbose ^= 1;
|
||||
break;
|
||||
case 'h':
|
||||
goto usage;
|
||||
default:
|
||||
goto usage;
|
||||
}
|
||||
}
|
||||
if ( p == NULL )
|
||||
{
|
||||
Abc_Print( 1, "Acb_CommandPs(): There is no current design.\n" );
|
||||
return 0;
|
||||
}
|
||||
if ( nModules )
|
||||
{
|
||||
Acb_ManPrintStats( p, nModules, fVerbose );
|
||||
return 0;
|
||||
}
|
||||
Acb_NtkPrintStatsFull( Acb_ManRoot(p), fDistrib, fVerbose );
|
||||
if ( fShowMulti )
|
||||
Acb_NtkPrintNodes( Acb_ManRoot(p), ABC_OPER_ARI_MUL );
|
||||
if ( fShowAdder )
|
||||
Acb_NtkPrintNodes( Acb_ManRoot(p), ABC_OPER_ARI_ADD );
|
||||
return 0;
|
||||
usage:
|
||||
Abc_Print( -2, "usage: @ps [-M num] [-madvh]\n" );
|
||||
Abc_Print( -2, "\t prints statistics\n" );
|
||||
Abc_Print( -2, "\t-M num : the number of first modules to report [default = %d]\n", nModules );
|
||||
Abc_Print( -2, "\t-m : toggle printing multipliers [default = %s]\n", fShowMulti? "yes": "no" );
|
||||
Abc_Print( -2, "\t-a : toggle printing adders [default = %s]\n", fShowAdder? "yes": "no" );
|
||||
Abc_Print( -2, "\t-d : toggle printing distrubition [default = %s]\n", fDistrib? "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");
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function********************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
******************************************************************************/
|
||||
int Acb_CommandPut( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||
{
|
||||
Acb_Man_t * p = Acb_AbcGetMan(pAbc);
|
||||
Gia_Man_t * pGia = NULL;
|
||||
int c, fBarBufs = 1, fSeq = 0, fVerbose = 0;
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "bsvh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
case 'b':
|
||||
fBarBufs ^= 1;
|
||||
break;
|
||||
case 's':
|
||||
fSeq ^= 1;
|
||||
break;
|
||||
case 'v':
|
||||
fVerbose ^= 1;
|
||||
break;
|
||||
case 'h':
|
||||
goto usage;
|
||||
default:
|
||||
goto usage;
|
||||
}
|
||||
}
|
||||
if ( p == NULL )
|
||||
{
|
||||
Abc_Print( 1, "Acb_CommandPut(): There is no current design.\n" );
|
||||
return 0;
|
||||
}
|
||||
pGia = Acb_ManBlast( p, fBarBufs, fSeq, fVerbose );
|
||||
if ( pGia == NULL )
|
||||
{
|
||||
Abc_Print( 1, "Acb_CommandPut(): Conversion to AIG has failed.\n" );
|
||||
return 0;
|
||||
}
|
||||
Abc_FrameUpdateGia( pAbc, pGia );
|
||||
return 0;
|
||||
usage:
|
||||
Abc_Print( -2, "usage: @put [-bsvh]\n" );
|
||||
Abc_Print( -2, "\t extracts AIG from the hierarchical design\n" );
|
||||
Abc_Print( -2, "\t-b : toggle using barrier buffers [default = %s]\n", fBarBufs? "yes": "no" );
|
||||
Abc_Print( -2, "\t-s : toggle blasting sequential elements [default = %s]\n", fSeq? "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");
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function********************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
******************************************************************************/
|
||||
int Acb_CommandGet( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||
{
|
||||
Acb_Man_t * pNew = NULL, * p = Acb_AbcGetMan(pAbc);
|
||||
int c, fMapped = 0, fVerbose = 0;
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "mvh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
case 'm':
|
||||
fMapped ^= 1;
|
||||
break;
|
||||
case 'v':
|
||||
fVerbose ^= 1;
|
||||
break;
|
||||
case 'h':
|
||||
goto usage;
|
||||
default:
|
||||
goto usage;
|
||||
}
|
||||
}
|
||||
if ( p == NULL )
|
||||
{
|
||||
Abc_Print( 1, "Acb_CommandGet(): There is no current design.\n" );
|
||||
return 0;
|
||||
}
|
||||
|
||||
if ( fMapped )
|
||||
{
|
||||
if ( pAbc->pNtkCur == NULL )
|
||||
{
|
||||
Abc_Print( 1, "Acb_CommandGet(): There is no current mapped design.\n" );
|
||||
return 0;
|
||||
}
|
||||
pNew = Acb_ManInsertAbc( p, pAbc->pNtkCur );
|
||||
}
|
||||
else
|
||||
{
|
||||
if ( pAbc->pGia == NULL )
|
||||
{
|
||||
Abc_Print( 1, "Acb_CommandGet(): There is no current AIG.\n" );
|
||||
return 0;
|
||||
}
|
||||
pNew = Acb_ManInsertGia( p, pAbc->pGia );
|
||||
}
|
||||
Acb_AbcUpdateMan( pAbc, pNew );
|
||||
return 0;
|
||||
usage:
|
||||
Abc_Print( -2, "usage: @get [-mvh]\n" );
|
||||
Abc_Print( -2, "\t extracts AIG or mapped network into the hierarchical design\n" );
|
||||
Abc_Print( -2, "\t-m : toggle using mapped network from main-space [default = %s]\n", fMapped? "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");
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function********************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
******************************************************************************/
|
||||
int Acb_CommandClp( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||
{
|
||||
Acb_Man_t * pNew = NULL, * p = Acb_AbcGetMan(pAbc);
|
||||
int c, fVerbose = 0;
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
case 'v':
|
||||
fVerbose ^= 1;
|
||||
break;
|
||||
case 'h':
|
||||
goto usage;
|
||||
default:
|
||||
goto usage;
|
||||
}
|
||||
}
|
||||
if ( p == NULL )
|
||||
{
|
||||
Abc_Print( 1, "Acb_CommandGet(): There is no current design.\n" );
|
||||
return 0;
|
||||
}
|
||||
pNew = Acb_ManCollapse( p );
|
||||
Acb_AbcUpdateMan( pAbc, pNew );
|
||||
return 0;
|
||||
usage:
|
||||
Abc_Print( -2, "usage: @clp [-vh]\n" );
|
||||
Abc_Print( -2, "\t collapses the current hierarchical design\n" );
|
||||
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");
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function********************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
******************************************************************************/
|
||||
int Acb_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||
{
|
||||
Gia_Man_t * pNew = NULL;
|
||||
Acb_Man_t * p = Acb_AbcGetMan(pAbc);
|
||||
int c, fSeq = 0, fVerbose = 0;
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
case 's':
|
||||
fSeq ^= 1;
|
||||
break;
|
||||
case 'v':
|
||||
fVerbose ^= 1;
|
||||
break;
|
||||
case 'h':
|
||||
goto usage;
|
||||
default:
|
||||
goto usage;
|
||||
}
|
||||
}
|
||||
if ( p == NULL )
|
||||
{
|
||||
Abc_Print( 1, "Acb_CommandBlast(): There is no current design.\n" );
|
||||
return 0;
|
||||
}
|
||||
pNew = Acb_ManBlast( p, 0, fSeq, fVerbose );
|
||||
if ( pNew == NULL )
|
||||
{
|
||||
Abc_Print( 1, "Acb_CommandBlast(): Bit-blasting has failed.\n" );
|
||||
return 0;
|
||||
}
|
||||
Abc_FrameUpdateGia( pAbc, pNew );
|
||||
return 0;
|
||||
usage:
|
||||
Abc_Print( -2, "usage: @blast [-svh]\n" );
|
||||
Abc_Print( -2, "\t performs bit-blasting of the word-level design\n" );
|
||||
Abc_Print( -2, "\t-s : toggle blasting sequential elements [default = %s]\n", fSeq? "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");
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function********************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
******************************************************************************/
|
||||
int Acb_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||
{
|
||||
Acb_Man_t * p = Acb_AbcGetMan(pAbc), * pTemp;
|
||||
Gia_Man_t * pFirst, * pSecond, * pMiter;
|
||||
Cec_ParCec_t ParsCec, * pPars = &ParsCec;
|
||||
char * pFileName, * pStr, ** pArgvNew;
|
||||
int c, nArgcNew, fDumpMiter = 0;
|
||||
FILE * pFile;
|
||||
Cec_ManCecSetDefaultParams( pPars );
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
case 'v':
|
||||
pPars->fVerbose ^= 1;
|
||||
break;
|
||||
case 'h':
|
||||
goto usage;
|
||||
default:
|
||||
goto usage;
|
||||
}
|
||||
}
|
||||
if ( p == NULL )
|
||||
{
|
||||
Abc_Print( 1, "Acb_CommandCec(): There is no current design.\n" );
|
||||
return 0;
|
||||
}
|
||||
|
||||
pArgvNew = argv + globalUtilOptind;
|
||||
nArgcNew = argc - globalUtilOptind;
|
||||
if ( nArgcNew != 1 )
|
||||
{
|
||||
if ( p->pSpec == NULL )
|
||||
{
|
||||
Abc_Print( -1, "File name is not given on the command line.\n" );
|
||||
return 1;
|
||||
}
|
||||
pFileName = p->pSpec;
|
||||
}
|
||||
else
|
||||
pFileName = pArgvNew[0];
|
||||
// fix the wrong symbol
|
||||
for ( pStr = pFileName; *pStr; pStr++ )
|
||||
if ( *pStr == '>' )
|
||||
*pStr = '\\';
|
||||
if ( (pFile = fopen( pFileName, "r" )) == NULL )
|
||||
{
|
||||
Abc_Print( -1, "Cannot open input file \"%s\". ", pFileName );
|
||||
if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".v", ".blif", NULL, NULL, NULL )) )
|
||||
Abc_Print( 1, "Did you mean \"%s\"?", pFileName );
|
||||
Abc_Print( 1, "\n" );
|
||||
return 1;
|
||||
}
|
||||
fclose( pFile );
|
||||
|
||||
// extract AIG from the current design
|
||||
pFirst = Acb_ManBlast( p, 0, 0, 0 );
|
||||
if ( pFirst == NULL )
|
||||
{
|
||||
Abc_Print( -1, "Extracting AIG from the current design has failed.\n" );
|
||||
return 0;
|
||||
}
|
||||
// extract AIG from the second design
|
||||
|
||||
if ( !strcmp( Extra_FileNameExtension(pFileName), "blif" ) )
|
||||
pTemp = Acb_ManReadBlif( pFileName );
|
||||
else if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) )
|
||||
pTemp = Acb_ManReadVerilog( pFileName );
|
||||
else if ( !strcmp( Extra_FileNameExtension(pFileName), "acb" ) )
|
||||
pTemp = Acb_ManReadCba( pFileName );
|
||||
else assert( 0 );
|
||||
pSecond = Acb_ManBlast( pTemp, 0, 0, 0 );
|
||||
Acb_ManFree( pTemp );
|
||||
if ( pSecond == NULL )
|
||||
{
|
||||
Gia_ManStop( pFirst );
|
||||
Abc_Print( -1, "Extracting AIG from the original design has failed.\n" );
|
||||
return 0;
|
||||
}
|
||||
// compute the miter
|
||||
pMiter = Gia_ManMiter( pFirst, pSecond, 0, 1, 0, 0, pPars->fVerbose );
|
||||
if ( pMiter )
|
||||
{
|
||||
if ( fDumpMiter )
|
||||
{
|
||||
Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "cec_miter.aig" );
|
||||
Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0, 0 );
|
||||
}
|
||||
pAbc->Status = Cec_ManVerify( pMiter, pPars );
|
||||
//Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb );
|
||||
Gia_ManStop( pMiter );
|
||||
}
|
||||
Gia_ManStop( pFirst );
|
||||
Gia_ManStop( pSecond );
|
||||
return 0;
|
||||
usage:
|
||||
Abc_Print( -2, "usage: @cec [-vh]\n" );
|
||||
Abc_Print( -2, "\t combinational equivalence checking\n" );
|
||||
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
|
||||
Abc_Print( -2, "\t-h : print the command usage\n");
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function********************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
******************************************************************************/
|
||||
int Acb_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||
{
|
||||
Acb_Man_t * p = Acb_AbcGetMan(pAbc);
|
||||
int c, fVerbose = 0;
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
case 'v':
|
||||
fVerbose ^= 1;
|
||||
break;
|
||||
case 'h':
|
||||
goto usage;
|
||||
default:
|
||||
goto usage;
|
||||
}
|
||||
}
|
||||
if ( p == NULL )
|
||||
{
|
||||
Abc_Print( 1, "Acb_CommandTest(): There is no current design.\n" );
|
||||
return 0;
|
||||
}
|
||||
return 0;
|
||||
usage:
|
||||
Abc_Print( -2, "usage: @test [-vh]\n" );
|
||||
Abc_Print( -2, "\t experiments with word-level networks\n" );
|
||||
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");
|
||||
return 1;
|
||||
}
|
||||
|
||||
#endif
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
File diff suppressed because it is too large
Load Diff
|
|
@ -0,0 +1,368 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [acbXec.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Hierarchical word-level netlist.]
|
||||
|
||||
Synopsis [Reusable XEC proof helpers.]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "acbXec.h"
|
||||
#include "aig/gia/giaAig.h"
|
||||
#include "base/abc/abc.h"
|
||||
#include "opt/dar/dar.h"
|
||||
#include "sat/cadical/cadicalSolver.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
typedef enum Acb_SatStatus_t_
|
||||
{
|
||||
ACB_SAT_UNSAT = -1,
|
||||
ACB_SAT_UNDEC = 0,
|
||||
ACB_SAT_SAT = 1
|
||||
} Acb_SatStatus_t;
|
||||
|
||||
int Acb_CnfCoDriverLit( Cnf_Dat_t * pCnf, int iCo, int * pLit )
|
||||
{
|
||||
Aig_Obj_t * pCo = Aig_ManCo( pCnf->pMan, iCo );
|
||||
Aig_Obj_t * pFan = Aig_ObjFanin0( pCo );
|
||||
int fCompl = Aig_ObjFaninC0( pCo );
|
||||
int Var;
|
||||
if ( Aig_ObjIsConst1(pFan) )
|
||||
return fCompl ? -1 : 0;
|
||||
Var = pCnf->pVarNums[pFan->Id];
|
||||
if ( Var < 0 )
|
||||
return -2;
|
||||
*pLit = Abc_Var2Lit( Var, fCompl );
|
||||
return 1;
|
||||
}
|
||||
|
||||
static int Acb_GiaPoIsConst0( Gia_Man_t * p, int iPo )
|
||||
{
|
||||
Gia_Obj_t * pObj;
|
||||
if ( iPo < 0 || iPo >= Gia_ManCoNum(p) )
|
||||
return 0;
|
||||
pObj = Gia_ManCo( p, iPo );
|
||||
return Gia_ObjFanin0(pObj) == Gia_ManConst0(p) && !Gia_ObjFaninC0(pObj);
|
||||
}
|
||||
|
||||
int Acb_GiaAllPosConst0( Gia_Man_t * p )
|
||||
{
|
||||
int i;
|
||||
for ( i = 0; i < Gia_ManCoNum(p); i++ )
|
||||
if ( !Acb_GiaPoIsConst0(p, i) )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
|
||||
static word Acb_XecGiaVarWord( int iVar, ABC_UINT64_T iWord )
|
||||
{
|
||||
static word Truth6[6] = {
|
||||
ABC_CONST(0xAAAAAAAAAAAAAAAA),
|
||||
ABC_CONST(0xCCCCCCCCCCCCCCCC),
|
||||
ABC_CONST(0xF0F0F0F0F0F0F0F0),
|
||||
ABC_CONST(0xFF00FF00FF00FF00),
|
||||
ABC_CONST(0xFFFF0000FFFF0000),
|
||||
ABC_CONST(0xFFFFFFFF00000000)
|
||||
};
|
||||
if ( iVar < 6 )
|
||||
return Truth6[iVar];
|
||||
return ((iWord >> (iVar - 6)) & 1) ? ~(word)0 : 0;
|
||||
}
|
||||
static inline word Acb_XecGiaLitWord( Vec_Wrd_t * vSims, int nWords, int Lit, int w )
|
||||
{
|
||||
word Res = Vec_WrdEntry( vSims, Abc_Lit2Var(Lit) * nWords + w );
|
||||
return Abc_LitIsCompl(Lit) ? ~Res : Res;
|
||||
}
|
||||
int * Acb_NtkSolveCadicalLimit( Gia_Man_t * p, int fUseHeavyOpt, int fVerbose, int * pStatus, int nSatTimeLimit, const char * pLabel, int fUseXecOutputClauses )
|
||||
{
|
||||
Aig_Man_t * pMan = NULL;
|
||||
Cnf_Dat_t * pCnf = NULL;
|
||||
cadical_solver * pSat = NULL;
|
||||
Vec_Int_t * vPoLits = NULL;
|
||||
Gia_Man_t * pGiaOpt = NULL, * pGiaTemp = NULL;
|
||||
Gia_Man_t * pGia = p;
|
||||
Aig_Obj_t * pObj;
|
||||
int i, Ret, Lit, Status = ACB_SAT_UNDEC, * pBeg, * pEnd, * pModel = NULL;
|
||||
int fRunSolve = 0, fSolvedSat = 0;
|
||||
abctime clk = Abc_Clock();
|
||||
(void)fUseXecOutputClauses;
|
||||
if ( pStatus )
|
||||
*pStatus = ACB_XEC_UNDEC;
|
||||
if ( p == NULL )
|
||||
return NULL;
|
||||
if ( Gia_ManCoNum(p) == 0 || Acb_GiaAllPosConst0(p) )
|
||||
{
|
||||
if ( pStatus )
|
||||
*pStatus = ACB_XEC_EQ;
|
||||
if ( pLabel )
|
||||
{
|
||||
printf( "The networks are equivalent by %s. ", pLabel );
|
||||
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
|
||||
}
|
||||
return NULL;
|
||||
}
|
||||
if ( fUseHeavyOpt && Gia_ManAndNum(p) > 0 )
|
||||
{
|
||||
pGiaTemp = Gia_ManCompress2( p, 1, 0 );
|
||||
if ( pGiaTemp )
|
||||
{
|
||||
pGiaOpt = pGiaTemp;
|
||||
pGiaTemp = NULL;
|
||||
pGia = pGiaOpt;
|
||||
assert( Gia_ManCiNum(pGia) == Gia_ManCiNum(p) );
|
||||
}
|
||||
}
|
||||
pMan = Gia_ManToAig( pGia, 0 );
|
||||
pCnf = pMan ? Cnf_Derive( pMan, Aig_ManCoNum(pMan) ) : NULL;
|
||||
pSat = pCnf ? cadical_solver_new() : NULL;
|
||||
if ( pCnf && pSat )
|
||||
{
|
||||
fRunSolve = 1;
|
||||
cadical_solver_setnvars( pSat, pCnf->nVars );
|
||||
Cnf_CnfForClause( pCnf, pBeg, pEnd, i )
|
||||
{
|
||||
if ( !cadical_solver_addclause( pSat, pBeg, pEnd ) )
|
||||
{
|
||||
Status = ACB_SAT_UNSAT;
|
||||
fRunSolve = 0;
|
||||
break;
|
||||
}
|
||||
}
|
||||
if ( fRunSolve )
|
||||
{
|
||||
vPoLits = Vec_IntAlloc( Gia_ManCoNum(pGia) );
|
||||
for ( i = 0; i < Gia_ManCoNum(pGia); i++ )
|
||||
{
|
||||
Ret = Acb_CnfCoDriverLit( pCnf, i, &Lit );
|
||||
if ( Ret == -2 )
|
||||
{
|
||||
Status = ACB_SAT_UNDEC;
|
||||
fRunSolve = 0;
|
||||
break;
|
||||
}
|
||||
if ( Ret == -1 )
|
||||
continue;
|
||||
if ( Ret == 0 )
|
||||
{
|
||||
Status = ACB_SAT_SAT;
|
||||
fRunSolve = 0;
|
||||
break;
|
||||
}
|
||||
Vec_IntPush( vPoLits, Lit );
|
||||
}
|
||||
}
|
||||
if ( fRunSolve && Vec_IntSize(vPoLits) == 0 )
|
||||
{
|
||||
Status = ACB_SAT_UNSAT;
|
||||
fRunSolve = 0;
|
||||
}
|
||||
if ( fRunSolve && !cadical_solver_addclause( pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits) ) )
|
||||
{
|
||||
Status = ACB_SAT_UNSAT;
|
||||
fRunSolve = 0;
|
||||
}
|
||||
if ( fRunSolve && fVerbose )
|
||||
{
|
||||
printf( "CaDiCaL CNF: Var = %d. Cla = %d. PO = %d.\n",
|
||||
pCnf->nVars, pCnf->nClauses + 1, Gia_ManCoNum(pGia) );
|
||||
if ( nSatTimeLimit > 0 )
|
||||
printf( "CaDiCaL SAT runtime limit: %d sec.\n", nSatTimeLimit );
|
||||
}
|
||||
if ( fRunSolve )
|
||||
{
|
||||
Status = cadical_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
|
||||
fSolvedSat = Status == ACB_SAT_SAT;
|
||||
}
|
||||
if ( fVerbose )
|
||||
printf( "CaDiCaL stats: conflicts = %d. learned = %d.\n",
|
||||
cadical_solver_nconflicts(pSat), cadical_solver_nlearned(pSat) );
|
||||
}
|
||||
if ( Status == ACB_SAT_UNSAT )
|
||||
{
|
||||
if ( pStatus )
|
||||
*pStatus = ACB_XEC_EQ;
|
||||
if ( pLabel )
|
||||
{
|
||||
printf( "The networks are equivalent by %s. ", pLabel );
|
||||
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
|
||||
}
|
||||
}
|
||||
else if ( Status == ACB_SAT_SAT )
|
||||
{
|
||||
if ( pStatus )
|
||||
*pStatus = ACB_XEC_NEQ;
|
||||
if ( fSolvedSat )
|
||||
pModel = ABC_CALLOC( int, Gia_ManCiNum(pGia) );
|
||||
if ( pModel && pSat && pCnf && pMan )
|
||||
Aig_ManForEachCi( pMan, pObj, i )
|
||||
{
|
||||
int Var = pCnf->pVarNums[pObj->Id];
|
||||
pModel[i] = Var >= 0 ? cadical_solver_get_var_value( pSat, Var ) : 0;
|
||||
}
|
||||
if ( pLabel )
|
||||
{
|
||||
printf( "The networks are NOT equivalent by %s. ", pLabel );
|
||||
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
if ( pStatus )
|
||||
*pStatus = ACB_XEC_UNDEC;
|
||||
if ( fVerbose && pLabel )
|
||||
{
|
||||
printf( "The networks are UNDECIDED by %s. ", pLabel );
|
||||
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
|
||||
}
|
||||
}
|
||||
if ( pSat )
|
||||
cadical_solver_delete( pSat );
|
||||
if ( pCnf )
|
||||
Cnf_DataFree( pCnf );
|
||||
if ( pMan )
|
||||
Aig_ManStop( pMan );
|
||||
if ( pGiaOpt )
|
||||
Gia_ManStop( pGiaOpt );
|
||||
Vec_IntFreeP( &vPoLits );
|
||||
return pModel;
|
||||
}
|
||||
int Acb_XecGiaSolveSmallConeExhaustive( Gia_Man_t * p, int fVerbose, int nTotalLimit )
|
||||
{
|
||||
Vec_Wrd_t * vSims = NULL;
|
||||
Gia_Obj_t * pObj;
|
||||
ABC_UINT64_T nWordsTotal, nWordBudget, iWordBase, nWordsDone = 0;
|
||||
int i, w, nWords, nWordsChunk, nObjs, nCis, nHiVars, Status = ACB_XEC_EQ, fDone = 0;
|
||||
abctime clk = Abc_Clock();
|
||||
abctime clkLimit = nTotalLimit > 0 ? clk + nTotalLimit * CLOCKS_PER_SEC : 0;
|
||||
if ( Gia_ManCoNum(p) != 1 || Gia_ManAndNum(p) > 5000 )
|
||||
return ACB_XEC_UNDEC;
|
||||
nCis = Gia_ManCiNum(p);
|
||||
nHiVars = Abc_MaxInt( 0, nCis - 6 );
|
||||
if ( nHiVars >= 63 )
|
||||
{
|
||||
if ( fVerbose )
|
||||
printf( "Skipping small-cone exhaustive word proof: CI = %d needs more than 2^63 simulation words.\n", nCis );
|
||||
return ACB_XEC_UNDEC;
|
||||
}
|
||||
nWordsChunk = nCis >= 31 ? 4096 : (nCis >= 28 ? 8192 : 16384);
|
||||
nWordsTotal = nHiVars ? ((ABC_UINT64_T)1 << nHiVars) : 1;
|
||||
nWordBudget = nTotalLimit > 0 ? (ABC_UINT64_T)200000 * nTotalLimit : (ABC_UINT64_T)60000000;
|
||||
if ( nWordBudget < (ABC_UINT64_T)8000000 )
|
||||
nWordBudget = (ABC_UINT64_T)8000000;
|
||||
if ( nWordsTotal > nWordBudget )
|
||||
{
|
||||
if ( fVerbose )
|
||||
printf( "Skipping small-cone exhaustive word proof: CI = %d needs %llu words, budget = %llu words.\n",
|
||||
nCis, (unsigned long long)nWordsTotal, (unsigned long long)nWordBudget );
|
||||
return ACB_XEC_UNDEC;
|
||||
}
|
||||
nObjs = Gia_ManObjNum(p);
|
||||
vSims = Vec_WrdStart( nObjs * nWordsChunk );
|
||||
if ( fVerbose )
|
||||
printf( "Trying small-cone exhaustive word proof: CI = %d. AND = %d. chunks = %llu x %d words. limit = %d sec.\n",
|
||||
nCis, Gia_ManAndNum(p), (unsigned long long)((nWordsTotal + nWordsChunk - 1) / nWordsChunk), nWordsChunk, nTotalLimit );
|
||||
for ( iWordBase = 0; iWordBase < nWordsTotal && !fDone; iWordBase += nWordsChunk )
|
||||
{
|
||||
ABC_UINT64_T nWordsLeft = nWordsTotal - iWordBase;
|
||||
nWords = nWordsLeft < (ABC_UINT64_T)nWordsChunk ? (int)nWordsLeft : nWordsChunk;
|
||||
if ( clkLimit && Abc_Clock() >= clkLimit )
|
||||
{
|
||||
Status = ACB_XEC_UNDEC;
|
||||
break;
|
||||
}
|
||||
/* Only the active words [0..nWords) are consumed in this chunk; other words may retain previous data. */
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
Vec_WrdWriteEntry( vSims, w, 0 );
|
||||
Gia_ManForEachCi( p, pObj, i )
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
Vec_WrdWriteEntry( vSims, Gia_ObjId(p, pObj) * nWordsChunk + w, Acb_XecGiaVarWord(i, iWordBase + w) );
|
||||
Gia_ManForEachAnd( p, pObj, i )
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
Vec_WrdWriteEntry( vSims, Gia_ObjId(p, pObj) * nWordsChunk + w,
|
||||
Acb_XecGiaLitWord(vSims, nWordsChunk, Gia_ObjFaninLit0p(p, pObj), w) &
|
||||
Acb_XecGiaLitWord(vSims, nWordsChunk, Gia_ObjFaninLit1p(p, pObj), w) );
|
||||
pObj = Gia_ManCo( p, 0 );
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
{
|
||||
word Res = Acb_XecGiaLitWord(vSims, nWordsChunk, Gia_ObjFaninLit0p(p, pObj), w);
|
||||
if ( iWordBase + w + 1 == nWordsTotal && nCis < 6 )
|
||||
Res &= (((word)1) << (1 << nCis)) - 1;
|
||||
if ( Res )
|
||||
{
|
||||
Status = ACB_XEC_UNDEC;
|
||||
fDone = 1;
|
||||
break;
|
||||
}
|
||||
}
|
||||
nWordsDone += nWords;
|
||||
}
|
||||
if ( fVerbose )
|
||||
{
|
||||
printf( "Small-cone exhaustive word proof: %s. checked words = %llu/%llu. ",
|
||||
Status == ACB_XEC_EQ ? "UNSAT" : "UNDECIDED",
|
||||
(unsigned long long)nWordsDone, (unsigned long long)nWordsTotal );
|
||||
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
|
||||
}
|
||||
Vec_WrdFree( vSims );
|
||||
return Status;
|
||||
}
|
||||
Gia_Man_t * Acb_XecGiaSmallConeXorRewrite( Gia_Man_t * p, int fVerbose )
|
||||
{
|
||||
Aig_Man_t * pAig = NULL, * pAigTemp = NULL;
|
||||
Gia_Man_t * pGia = NULL, * pTemp = NULL;
|
||||
int nAndStart = Gia_ManAndNum(p);
|
||||
abctime clk = Abc_Clock();
|
||||
if ( Gia_ManCoNum(p) != 1 || Gia_ManCiNum(p) > 64 || nAndStart > 8000 )
|
||||
return NULL;
|
||||
if ( fVerbose )
|
||||
printf( "Small-cone XOR structural rewrite: CI = %d. AND = %d.\n",
|
||||
Gia_ManCiNum(p), nAndStart );
|
||||
pAig = Gia_ManToAig( p, 0 );
|
||||
if ( pAig == NULL )
|
||||
return NULL;
|
||||
pAig = Dar_ManBalanceXor( pAigTemp = pAig, 1, 1, 0 );
|
||||
Aig_ManStop( pAigTemp );
|
||||
if ( pAig == NULL )
|
||||
return NULL;
|
||||
pAig = Dar_ManRwsat( pAigTemp = pAig, 1, 0 );
|
||||
Aig_ManStop( pAigTemp );
|
||||
if ( pAig == NULL )
|
||||
return NULL;
|
||||
pGia = Gia_ManFromAig( pAig );
|
||||
Aig_ManStop( pAig );
|
||||
if ( pGia == NULL )
|
||||
return NULL;
|
||||
pTemp = Gia_ManCompress2( pGia, 1, 0 );
|
||||
if ( pTemp )
|
||||
{
|
||||
Gia_ManStop( pGia );
|
||||
pGia = pTemp;
|
||||
}
|
||||
if ( fVerbose )
|
||||
{
|
||||
printf( "Small-cone XOR structural rewrite: AND = %d -> %d. Lev = %d -> %d. ",
|
||||
nAndStart, Gia_ManAndNum(pGia), Gia_ManLevelNum(p), Gia_ManLevelNum(pGia) );
|
||||
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
|
||||
}
|
||||
if ( Gia_ManCoNum(pGia) != Gia_ManCoNum(p) ||
|
||||
(!Acb_GiaAllPosConst0(pGia) && Gia_ManAndNum(pGia) >= nAndStart) )
|
||||
{
|
||||
Gia_ManStop( pGia );
|
||||
return NULL;
|
||||
}
|
||||
return pGia;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
|
@ -0,0 +1,70 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [acbXec.h]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Hierarchical word-level netlist.]
|
||||
|
||||
Synopsis [Shared XEC proof helper API.]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#ifndef ABC__base__acb__acbXec_h
|
||||
#define ABC__base__acb__acbXec_h
|
||||
|
||||
#include "acb.h"
|
||||
#include "sat/cnf/cnf.h"
|
||||
|
||||
ABC_NAMESPACE_HEADER_START
|
||||
|
||||
/*
|
||||
* XEC/network-level proof status:
|
||||
* ACB_XEC_EQ : networks/output are proven equivalent/UNSAT miter
|
||||
* ACB_XEC_NEQ : networks/output are proven different/SAT miter
|
||||
* ACB_XEC_UNDEC : proof was inconclusive
|
||||
* ACB_XEC_ONE_HARD : local sweep proved all but one output
|
||||
* ACB_XEC_MANY_HARD : local sweep left multiple hard outputs
|
||||
*
|
||||
*/
|
||||
typedef enum Acb_XecStatus_t_
|
||||
{
|
||||
ACB_XEC_MANY_HARD = -3,
|
||||
ACB_XEC_ONE_HARD = -2,
|
||||
ACB_XEC_UNDEC = -1,
|
||||
ACB_XEC_NEQ = 0,
|
||||
ACB_XEC_EQ = 1
|
||||
} Acb_XecStatus_t;
|
||||
|
||||
static inline void Acb_NtkPrintUnsupportedObj( Acb_Ntk_t * p, int iObj, const char * pWhere, int ExpectedFans, int ActualFans )
|
||||
{
|
||||
printf( "%s unsupported ACB object: obj = %d", pWhere ? pWhere : "XEC" , iObj );
|
||||
if ( p && iObj >= 0 && iObj < Acb_NtkObjNumMax(p) )
|
||||
printf( ", type = %d", Acb_ObjType(p, iObj) );
|
||||
if ( ExpectedFans >= 0 || ActualFans >= 0 )
|
||||
printf( ", fanins = %d, expected = %d", ActualFans, ExpectedFans );
|
||||
printf( ".\n" );
|
||||
}
|
||||
|
||||
static inline void Acb_XecMergeTargetStatus( int StatusTarget, int fHasModel, int * pStatus, int * pCheckModel )
|
||||
{
|
||||
if ( fHasModel && pCheckModel )
|
||||
*pCheckModel = 1;
|
||||
if ( pStatus == NULL )
|
||||
return;
|
||||
if ( StatusTarget == ACB_XEC_EQ )
|
||||
*pStatus = ACB_XEC_EQ;
|
||||
else if ( StatusTarget == ACB_XEC_NEQ )
|
||||
*pStatus = ACB_XEC_NEQ;
|
||||
}
|
||||
|
||||
extern int * Acb_NtkSolveCadicalLimit( Gia_Man_t * p, int fUseHeavyOpt, int fVerbose, int * pStatus, int nSatTimeLimit, const char * pLabel, int fUseXecOutputClauses );
|
||||
extern int Acb_CnfCoDriverLit( Cnf_Dat_t * pCnf, int iCo, int * pLit );
|
||||
extern int Acb_GiaAllPosConst0( Gia_Man_t * p );
|
||||
|
||||
extern int Acb_XecGiaSolveSmallConeExhaustive( Gia_Man_t * p, int fVerbose, int nTotalLimit );
|
||||
extern Gia_Man_t *Acb_XecGiaSmallConeXorRewrite( Gia_Man_t * p, int fVerbose );
|
||||
|
||||
ABC_NAMESPACE_HEADER_END
|
||||
|
||||
#endif
|
||||
|
|
@ -1,9 +1,9 @@
|
|||
SRC += src/base/acb/acbAbc.c \
|
||||
src/base/acb/acbAig.c \
|
||||
src/base/acb/acbCom.c \
|
||||
src/base/acb/acbFunc.c \
|
||||
src/base/acb/acbMfs.c \
|
||||
src/base/acb/acbPush.c \
|
||||
src/base/acb/acbSets.c \
|
||||
src/base/acb/acbTest.c \
|
||||
src/base/acb/acbUtil.c
|
||||
src/base/acb/acbUtil.c \
|
||||
src/base/acb/acbXec.c
|
||||
|
|
|
|||
|
|
@ -53,6 +53,8 @@ extern void Wlc_Init( Abc_Frame_t * pAbc );
|
|||
extern void Wlc_End( Abc_Frame_t * pAbc );
|
||||
extern void Wln_Init( Abc_Frame_t * pAbc );
|
||||
extern void Wln_End( Abc_Frame_t * pAbc );
|
||||
extern void Sn_Init( Abc_Frame_t * pAbc );
|
||||
extern void Sn_End( Abc_Frame_t * pAbc );
|
||||
extern void Pla_Init( Abc_Frame_t * pAbc );
|
||||
extern void Pla_End( Abc_Frame_t * pAbc );
|
||||
extern void Sim_Init( Abc_Frame_t * pAbc );
|
||||
|
|
@ -119,6 +121,7 @@ void Abc_FrameInit( Abc_Frame_t * pAbc )
|
|||
Emap_Init( pAbc );
|
||||
Wlc_Init( pAbc );
|
||||
Wln_Init( pAbc );
|
||||
Sn_Init( pAbc );
|
||||
Pla_Init( pAbc );
|
||||
Test_Init( pAbc );
|
||||
Ufar_Init( pAbc );
|
||||
|
|
@ -160,6 +163,7 @@ void Abc_FrameEnd( Abc_Frame_t * pAbc )
|
|||
Scl_End( pAbc );
|
||||
Wlc_End( pAbc );
|
||||
Wln_End( pAbc );
|
||||
Sn_End( pAbc );
|
||||
Pla_End( pAbc );
|
||||
Test_End( pAbc );
|
||||
Glucose_End( pAbc );
|
||||
|
|
|
|||
|
|
@ -149,6 +149,7 @@ struct Abc_Frame_t_
|
|||
void * pAbcWlc;
|
||||
Vec_Int_t * pAbcWlcInv;
|
||||
void * pAbcRtl;
|
||||
void * pAbcSn;
|
||||
void * pAbcPla;
|
||||
Abc_Nam_t * pJsonStrs;
|
||||
Vec_Wec_t * vJsonObjs;
|
||||
|
|
|
|||
|
|
@ -0,0 +1 @@
|
|||
SRC += src/base/sn/snCom.c
|
||||
|
|
@ -0,0 +1,253 @@
|
|||
# Simple Netlist in ABC
|
||||
|
||||
This directory contains the Slang-independent Simple Netlist (SN) representation and algorithms.
|
||||
|
||||
The external `sn_slang` executable parses and elaborates Verilog/SystemVerilog using Mike Popoloski's excellent
|
||||
[slang SystemVerilog compiler](https://github.com/MikePopoloski/slang) and writes a binary `.sn` design. ABC does
|
||||
not link slang or require its C++20 dependencies.
|
||||
|
||||
The frontend architecture benefited from [yosys-slang](https://github.com/povik/yosys-slang), developed by
|
||||
Martin Povišer. It has been both an inspiration and a helpful practical guideline for working from slang's
|
||||
elaborated model, particularly for lvalue analysis, procedural state, timing patterns, memory eligibility, resolved
|
||||
nets, and diagnostics. The SN representation and lowering are independently developed, with warm thanks to Martin
|
||||
for his work and advice.
|
||||
|
||||
ABC holds the SN design and the `&`-space GIA as independent representations. Commands move data between them only
|
||||
when explicitly requested:
|
||||
|
||||
| Command | Reads | Writes |
|
||||
| --- | --- | --- |
|
||||
| `@slang`, `@read` | HDL or `.sn` | Current SN design |
|
||||
| `@map_*`, `@opt_mux`, `@collapse` | SN | New SN design revision |
|
||||
| `@blast` | SN | Current `&`-space GIA plus a saved boundary |
|
||||
| `&...` commands | GIA | GIA |
|
||||
| `@put` | GIA plus saved boundary | Module selected by the preceding `@blast` |
|
||||
| `@write` | SN | `.sn` or Verilog |
|
||||
|
||||
`@status` reports both representations, the monotonically increasing SN revision, and whether the saved boundary is
|
||||
compatible with the current SN design and GIA. In particular, reading or transforming SN does not clear or update an
|
||||
old `&`-space network; it makes that network unavailable for `@put` until another combinational `@blast` records a
|
||||
matching boundary.
|
||||
|
||||
## Commands
|
||||
|
||||
The commands appear under `New word level commands` in ABC's `help` output.
|
||||
|
||||
```text
|
||||
set snslang /path/to/sn_slang
|
||||
@slang -M top rtl1.sv rtl2.sv
|
||||
@status
|
||||
@check
|
||||
@ps -v
|
||||
@map_mem -v
|
||||
@check
|
||||
@map_dsp -v
|
||||
@check
|
||||
@map_add -v
|
||||
@check
|
||||
@opt_mux -v
|
||||
@check
|
||||
@blast -M top -c -v
|
||||
&resyn3
|
||||
&if -m -K 6
|
||||
&ps
|
||||
@status
|
||||
@put -v
|
||||
@check
|
||||
@collapse -v
|
||||
@check
|
||||
@write mapped_logic.v
|
||||
@write mapped_logic.sn
|
||||
```
|
||||
|
||||
`@slang` uses `sn_slang` from `PATH` unless the `snslang` setting overrides it. It accepts `-M` for the top module,
|
||||
repeatable `-D NAME` or `-D NAME=value` preprocessor definitions, `-F` for one additional source file, and any number
|
||||
of positional source files. For example, `-D WIDTH=8 -D SIGNED=1` defines two macros. `-T` is not used because ABC
|
||||
conventionally reserves it for a time limit. `-v` prints the external command and frontend timing. A module declared
|
||||
inside SystemVerilog `` `celldefine`` / `` `endcelldefine``, or marked by a nonzero `black_box` or `syn_black_box`
|
||||
module attribute, is imported as an opaque technology primitive with its elaborated PI/PO interface; its simulation
|
||||
body is not lowered. For example, both `` `celldefine`` around a module definition and
|
||||
`(* syn_black_box = 1 *) module macro (...);` create an opaque leaf. An explicit zero or false attribute does not.
|
||||
The declaration is still required: slang must know every port's name, direction, width, and signedness, so an
|
||||
undefined-module inst remains an error. Undefined-module patterns and include-directory options remain unsupported.
|
||||
|
||||
`@read` and `@write` provide binary persistence. `@write` selects SN or Verilog output from the `.sn`, `.v`, or
|
||||
`.sv` extension. `@read -M module` selects the top stored in a multi-top design; otherwise the last top is used.
|
||||
Before installing external binary data, `@read` validates the encoding and runs the same non-aborting structural and
|
||||
semantic checks as `@check`. A failed `@write` removes its incomplete output file. Every design installed in ABC is
|
||||
topologically ordered. The current writer emits binary format version 6; the reader also accepts version 5 and treats
|
||||
its modules as ordinary non-black-box modules because that format predates module flags.
|
||||
|
||||
`@status` prints the current design and top names, SN revision, selected technology, hierarchy form, last extraction
|
||||
mode/module/revision, saved boundary hash, current GIA dimensions, and `@put` compatibility. A new `@read` or `@slang`
|
||||
design starts at revision 1. Each transformation that installs a replacement SN design, and each successful `@put`,
|
||||
advances the revision; `&` commands do not. An optimization that finds no profitable rewrite leaves the design and its
|
||||
revision unchanged.
|
||||
|
||||
`@blast` gives every GIA input and output a unique ordered name containing the retained SN signal name, bit index, and
|
||||
interface index. It also hashes the selected module identity and all saved boundary occurrences, primitives, registers,
|
||||
loops, and input/output endpoint records. Before insertion, `@put` verifies the SN revision, module ID and name,
|
||||
boundary hash, GIA dimensions, and ordered GIA-name signature. It rejects a GIA whose interface was reordered, renamed,
|
||||
or stripped of names, even if its input and output counts still match. The GIA must also remain combinational, with zero
|
||||
registers. Normal interface-preserving `&` synthesis commands retain the names and remain compatible.
|
||||
|
||||
MiniAIG has only an edge-triggered register convention. Therefore `@blast` and `@map_lut` explicitly reject any
|
||||
level-sensitive `SN_REG_LATCH` reachable from the selected module until a semantics-preserving latch flow is available.
|
||||
|
||||
`@check` performs a non-aborting consistency audit of the complete SN design. It validates core and type-specific
|
||||
attribute vectors, fanin storage, object IDs, widths, names, constants, topology, state pairing, memory-port ownership,
|
||||
instance/FAN ordering, hierarchy recursion, LUTs, gates, and mapped primitive interfaces. `@check -v` adds one summary
|
||||
line per module. Memory, DSP, and carry mapping commands run the same checker transactionally before and after each
|
||||
transformation, so an invalid result is diagnosed and rejected without replacing the current design.
|
||||
|
||||
`@ps` prints compact statistics for every module definition by default. `@ps -M module` prints the selected module
|
||||
instead and uses it as the root for optional hierarchy and detailed reports. `@ps -v` adds the selected hierarchy and
|
||||
keeps opaque definitions annotated with `[blackbox]`. Like `%ps -d`, `@ps -d` prints occurrences by object type and
|
||||
output/input width signature. It also reports every reachable black-box type, its instance-occurrence multiplicity,
|
||||
PI/PO port and bit counts, and totals for abstract AIG inputs and outputs. Counts cover the elaborated hierarchy rooted
|
||||
at the selected module (or the current design top when `-M` is absent), including repeated insts. Hierarchical totals
|
||||
are accumulated over the module DAG rather than by recursively revisiting every inst, so statistics remain practical
|
||||
for deeply repeated hierarchy. Memory is reported as used/allocated storage with rounded K, M, or G suffixes.
|
||||
|
||||
`@map_mem`, `@map_dsp`, and `@map_add` map into the initial AMD/Xilinx UltraScale+ technology description.
|
||||
Transformations are transactional and keep the original user-visible top-module name. `@map_add` replaces word-level
|
||||
addition and subtraction of at least three bits by chains of behavioral `__sn_CARRY4` primitive insts. Propagate,
|
||||
operand inversion, extension, and final slicing remain ordinary SN logic for subsequent LUT mapping. Run DSP mapping
|
||||
before carry mapping so future DSP preadder and postadder recognition is not hidden. `@collapse` flattens user hierarchy
|
||||
while retaining mapped hard-block leaf instances.
|
||||
|
||||
Opaque `SN_MODULE_BLACKBOX` insts are preserved by hierarchy collapse even when ordinary user hierarchy is flattened.
|
||||
During `@blast`, each opaque output is an additional GIA input and each opaque input is an additional GIA output, in
|
||||
natural port and LSB-first bit order. A black-box `SN_PO` has `SN_INVALID_ID` as its sole fanin, explicitly recording
|
||||
that its value has no SN implementation; no zero-valued placeholder is created. `@write` emits the preserved interface
|
||||
as a port-only `(* blackbox *)` module. Internally an opaque module contains only its declared `SN_PI` and `SN_PO`
|
||||
objects; an `inout` is a same-named PI/PO pair. Its body and descendants are absent from SN. `@check` permits the
|
||||
invalid PO fanin only for this boundary representation, and `@ps -v` / `@ps -d` expose the retained black boxes and
|
||||
their reachable occurrence counts.
|
||||
|
||||
`SN_CAST` is a one-fanin operator whose object width and signedness define the result type. It does not permute bits.
|
||||
An equal-width cast only changes the signedness annotation; widening sign-extends a signed result and zero-extends an
|
||||
unsigned result; narrowing discards high bits and retains the LSB-first low-order portion. `sn_slang` adds casts for
|
||||
explicit and implicit slang conversions, `$signed` / `$unsigned`, dynamic selected-value normalization, packed-value
|
||||
updates, and final normalization of `SN_MUX` data branches to the mux result width. Memory, DSP, and carry mapping may
|
||||
also introduce casts while adapting word-level values to primitive interfaces. The Verilog writer uses `$signed` or
|
||||
`$unsigned` on a result-width wire, and the bit-blaster implements the same extension or truncation directly.
|
||||
|
||||
`@opt_mux` restructures register mux cones by collecting root-to-terminal paths, grouping structurally identical
|
||||
LSB-first word values, and ORing the corresponding path conditions. A register-output terminal is converted into an
|
||||
explicit enable when the path controls are provably exclusive. The pass currently recognizes ordinary `SN_MUX`
|
||||
trees and packed `SN_PMUX` alternatives; separately created casts, slices, repetitions, concatenations, and constants
|
||||
are compared structurally. Rewritten modules are restored at their stable hierarchy IDs and retain every register
|
||||
pair so that the canonical transition interface remains unchanged. The default profitability filter requires at
|
||||
least 4-bit data, six paths, two eliminated paths, and a path-to-distinct-terminal ratio of at least 2:1. This avoids
|
||||
increasing logic for narrow control muxes while retaining the intended wide datapath transformations.
|
||||
|
||||
`@blast` traverses hierarchy directly without first allocating a flat SN module. Sequential extraction is the
|
||||
default; `-c` selects combinational extraction. `-t` emits the same effective next-state functions as a purely
|
||||
combinational transition AIG for equivalence checking.
|
||||
`-M module` selects the module to
|
||||
extract; the default is the current SN top. ABC records the selected module and the exact LSB-first boundary mapping,
|
||||
then installs the resulting GIA as the current `&` network. The user may apply any `&`-space combinational synthesis
|
||||
and mapping commands that preserve the number and order of combinational inputs and outputs. Nothing requires the
|
||||
logic to be put back into SN: omitting `@put` leaves the SN design unchanged.
|
||||
|
||||
Adders use a Brent-Kung parallel-prefix network by default. `@blast -r` selects ripple-carry adders instead. This
|
||||
choice also applies to adder networks used while blasting subtraction and other arithmetic operators; `-b` separately
|
||||
selects Booth rather than the direct-unsigned/Baugh-Wooley multiplier. Signed and unsigned relational operators use
|
||||
a balanced, delay-oriented comparator by default; `@blast -d` toggles to the minimum-node topology implemented by ABC's
|
||||
`&gencomp`. Equality comparison remains balanced in both modes. Ripple adders and multiplier compressor trees share
|
||||
the seven-node full-adder construction from `Wlc_BlastFullAdder()`. Direct unsigned, signed Baugh-Wooley, and radix-4
|
||||
Booth partial products use the delay-aware, level-ordered matrix reduction adapted from `Wlc_BlastReduceMatrix()`,
|
||||
followed by the selected Brent-Kung or ripple final adder. The radix-4 Booth recoding, signed correction, rectangular
|
||||
operand handling, and unsigned zero extension follow `Wlc_BlastBooth()`. Binary mux trees use `Mini_AigMuxMulti()`,
|
||||
while AND/OR reductions and equality aggregation use balanced `Mini_AigAndMulti()` trees over copied temporary
|
||||
literals. One-hot priority muxes use a balanced sum-of-products tree; their result for a multi-hot select remains
|
||||
intentionally undefined. Variable shifts instantiate only the useful barrel stages and combine all higher shift bits
|
||||
into one balanced overshift condition.
|
||||
|
||||
Unnamed constants are interned by width, signedness, and packed value within each module. Concatenations whose inputs
|
||||
are all constant are folded into one packed `SN_CONST`, including tables wider than the per-object fanin-count limit.
|
||||
When such a constant drives an `SN_BMUX`, blasting reads one output-bit column at a time and simplifies constant and
|
||||
equal mux branches before creating MiniAIG nodes; it never materializes the complete packed table as an integer-literal
|
||||
array. The Verilog writer splits very large constants into bounded-size hexadecimal concatenation chunks.
|
||||
|
||||
In combinational mode (`@blast -c`), flop outputs become additional inputs, while raw data and synchronous control
|
||||
inputs become separate outputs for later stitching; clock and asynchronous controls remain outside this boundary.
|
||||
Mapped RAM/DSP and CARRY4 outputs and inputs are likewise exposed as additional cloud endpoints. `@put` checks the saved
|
||||
interface and reconnects registers and mapped primitive instances. With the default sequential `@blast`, the AIG
|
||||
transition functions elaborate synchronous reset, set, and enable controls in SN priority order; clock and asynchronous
|
||||
controls remain outside the transition relation. Sequential-AIG insertion is deliberately rejected for now.
|
||||
|
||||
`@map_lut` applies this combinational extraction and reconstruction module by module while preserving the natural SN
|
||||
hierarchy. Child instances, registers, and mapped RAM/DSP/CARRY4 instances are partition boundaries, matching the broad
|
||||
structure of Yosys's per-module ABC flow. `@map_lut -S "&resyn3; &if -m -K 6"` supplies an inline per-partition ABC
|
||||
script; `-F script.abc` sources it from a file. The default is the same `&resyn3; &if -m -K 6` sequence. Every script
|
||||
must preserve CI/CO order and leave a LUT-mapped GIA. Generic-memory modules left unsupported by `@map_mem` remain
|
||||
unchanged and are reported as skipped partitions. Mapped nodes wider than the physical SN LUT6 primitive are
|
||||
decomposed deterministically by Shannon expansion. The pass maps a duplicate design and commits it only after every
|
||||
reachable non-primitive module succeeds. `-P num` runs the independent partition jobs concurrently using `num - 1`
|
||||
pthread workers and one coordinating process. `-P 1` uses the current ABC process directly, so its last partition
|
||||
becomes the current `&`-space GIA; use `-P 2` or more when the preexisting `&`-space network must remain untouched.
|
||||
SN pthread support is compiled out on Windows, where `-P 1` remains fully supported and larger values are rejected.
|
||||
`@map_lut -E prefix` stops at the same partition boundary, writes each nontrivial job as
|
||||
`prefix_<module-id>_<module-name>.aig` with a `.txt` interface-statistics sidecar, and does not run synthesis or modify
|
||||
the SN design. This mode cannot be combined with `-S` or `-F`, currently requires `-P 1`, and is intended for
|
||||
developing or benchmarking an external per-partition synthesis flow.
|
||||
Generated clock and asynchronous-control cones remain outside the mapped cloud and are copied with per-occurrence
|
||||
memoization when registers are reconnected.
|
||||
|
||||
The transition AIG orders state bits canonically by depth-first natural instance type ID, natural `SN_REG_OUT` type
|
||||
ID within each occurrence, and LSB-first bit index. Both hierarchy duplication and mux sharing preserve these IDs.
|
||||
Consequently, the transition AIGs made before and after `@opt_mux` have identical CI/CO order and can be compared
|
||||
directly with `&cec before.aig after.aig`. For large, structurally different cones, explicitly constructing the miter
|
||||
is often much faster: `&r before.aig; &miter after.aig; &cec -m`. Transition-AIG insertion through `@put` is
|
||||
deliberately rejected.
|
||||
|
||||
`@put` replaces only the module selected by the preceding `@blast`. Its module ID, name, and port interface remain
|
||||
stable, so parent instances and every other module in an uncollapsed hierarchical design are preserved. The current
|
||||
GIA determines the reconstructed representation:
|
||||
|
||||
- An unmapped GIA becomes explicit one-bit `SN_BIT_AND` and `SN_BIT_NOT` objects.
|
||||
- A LUT-mapped GIA becomes `SN_LUT` objects with truth tables transferred through MiniLUT.
|
||||
- A cell-mapped GIA becomes `SN_GATE` objects annotated with current genlib gate IDs and cell names through ABC's
|
||||
mini-mapping format. Insertion requires the current genlib to contain every referenced gate.
|
||||
|
||||
For example, `@blast -c; &resyn3; &if -m -K 6; @put` implements the former canned LUT-mapping flow without hiding
|
||||
the ABC script. `@blast -c; &dc2; @put` reinserts an optimized unmapped AIG, while
|
||||
`read_genlib library.genlib; @blast -c; &nf; @put` reinserts standard cells. The Verilog writer emits LUT and gate
|
||||
instances as well as ordinary SN logic.
|
||||
|
||||
Mapped RAM/DSP/CARRY4 instances are reconstructed as technology leaf instances. SN loop-breaker pairs connect their
|
||||
output ports while the new flat module is built and are placed into a legal order by the final topological reorder.
|
||||
Temporary primitive-output loop pairs are pruned after reconnection unless an actual feedback dependency remains, so
|
||||
acyclic datapaths do not gain artificial loop-breakers. Explicit loop boundaries extracted from the original SN module
|
||||
are reconstructed unchanged; they are not currently re-proved unnecessary after `&`-space optimization. Generic
|
||||
unmapped memory endpoints are recorded and abstracted by `@blast`, but `@put` currently rejects them because the
|
||||
boundary does not yet retain enough per-memory-port ownership data. This check prevents silent loss or misconnection
|
||||
of stateful memories.
|
||||
|
||||
## Source files
|
||||
|
||||
The package uses ABC-style filenames:
|
||||
|
||||
```text
|
||||
sn.h core representation, hierarchy, serialization, and Verilog writer
|
||||
snCheck.h non-aborting design, module, hierarchy, and technology-interface consistency checker
|
||||
snTech.h target technology descriptions
|
||||
snMapMem.h memory mapping support
|
||||
snMapDsp.h DSP mapping support
|
||||
snMapAdd.h CARRY4 mapping support
|
||||
snMapTech.h combined hierarchy mapping
|
||||
snMapLut.h natural-hierarchy LUT-mapping harness
|
||||
snPth.h bounded pthread worker harness
|
||||
snBlast.h direct hierarchical MiniAIG construction
|
||||
snMux.h register mux-path sharing and restructuring
|
||||
snBoundary.h saved boundary and combinational register reconnection
|
||||
snMiniAig.h unmapped MiniAIG reconstruction
|
||||
snMiniLut.h MiniLUT analysis and SN_LUT reconstruction
|
||||
snMiniGate.h mini-mapping and SN_GATE reconstruction
|
||||
snCom.c ABC manager ownership and command handlers
|
||||
```
|
||||
|
||||
The external frontend must compile against this directory through a configured include path. Representation changes
|
||||
are made here first and must update the binary-format version when serialization compatibility changes.
|
||||
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
|
|
@ -0,0 +1,874 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [snBoundary.h]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [New word-level design interface.]
|
||||
|
||||
Synopsis [Reconstruction and reconnection of extracted combinational boundaries.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: snBoundary.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#ifndef ABC__base__sn__snBoundary_h
|
||||
#define ABC__base__sn__snBoundary_h
|
||||
|
||||
#include "snBlast.h"
|
||||
|
||||
ABC_NAMESPACE_HEADER_START
|
||||
|
||||
typedef struct sn_boundary_regs_t
|
||||
{
|
||||
sn_design_t* design;
|
||||
const sn_blast_boundary_t* boundary;
|
||||
sn_module_t* result;
|
||||
sn_obj_id_t* top_inputs;
|
||||
sn_obj_pair_t* pairs;
|
||||
sn_obj_pair_t* loops;
|
||||
sn_obj_pair_t* primitive_pairs;
|
||||
uint32_t* primitive_offsets;
|
||||
sn_obj_id_t** external_copies;
|
||||
struct sn_boundary_link_t* links;
|
||||
size_t link_cap;
|
||||
} sn_boundary_regs_t;
|
||||
|
||||
typedef struct sn_boundary_link_t
|
||||
{
|
||||
uint64_t key;
|
||||
uint32_t primitive;
|
||||
uint32_t child;
|
||||
uint32_t reg;
|
||||
uint32_t loop;
|
||||
} sn_boundary_link_t;
|
||||
|
||||
typedef struct sn_boundary_external_frame_t
|
||||
{
|
||||
sn_blast_hier_ref_t ref;
|
||||
sn_blast_hier_ref_t dependency;
|
||||
sn_obj_id_t result;
|
||||
uint32_t next_fanin;
|
||||
uint8_t phase;
|
||||
} sn_boundary_external_frame_t;
|
||||
|
||||
enum
|
||||
{
|
||||
SN_BOUNDARY_EXTERNAL_START,
|
||||
SN_BOUNDARY_EXTERNAL_ALIAS,
|
||||
SN_BOUNDARY_EXTERNAL_OPERATOR
|
||||
};
|
||||
|
||||
static inline uint64_t sn_boundary_link_key(uint32_t occurrence, sn_obj_id_t object)
|
||||
{
|
||||
return ((uint64_t)occurrence << 32) | object;
|
||||
}
|
||||
|
||||
static inline size_t sn_boundary_link_hash(uint64_t key, size_t mask)
|
||||
{
|
||||
key ^= key >> 33;
|
||||
key *= UINT64_C(0xff51afd7ed558ccd);
|
||||
key ^= key >> 33;
|
||||
return (size_t)key & mask;
|
||||
}
|
||||
|
||||
static inline sn_boundary_link_t* sn_boundary_link_find(sn_boundary_regs_t* regs, uint32_t occurrence,
|
||||
sn_obj_id_t object, bool create)
|
||||
{
|
||||
if (!regs->link_cap)
|
||||
return NULL;
|
||||
uint64_t key = sn_boundary_link_key(occurrence, object);
|
||||
size_t slot = sn_boundary_link_hash(key, regs->link_cap - 1);
|
||||
while (regs->links[slot].key != UINT64_MAX && regs->links[slot].key != key)
|
||||
slot = (slot + 1) & (regs->link_cap - 1);
|
||||
if (regs->links[slot].key == UINT64_MAX)
|
||||
{
|
||||
if (!create)
|
||||
return NULL;
|
||||
regs->links[slot].key = key;
|
||||
}
|
||||
return ®s->links[slot];
|
||||
}
|
||||
|
||||
static inline sn_obj_id_t* sn_boundary_external_copies(sn_boundary_regs_t* regs, sn_blast_hier_ref_t ref,
|
||||
const sn_module_t** returned_module)
|
||||
{
|
||||
const sn_blast_occurrence_t* occurrence =
|
||||
&sn_vec_at(sn_blast_occurrence_t, ®s->boundary->occurrences, ref.occurrence);
|
||||
const sn_module_t* module = sn_design_get_module_const(regs->design, occurrence->module);
|
||||
sn_obj_id_t* copies = regs->external_copies[ref.occurrence];
|
||||
assert(ref.object < module->obj_types.size);
|
||||
if (!copies)
|
||||
{
|
||||
copies = (sn_obj_id_t*)malloc(sizeof(sn_obj_id_t) * module->obj_types.size);
|
||||
assert(copies);
|
||||
for (size_t i = 0; i < module->obj_types.size; i++)
|
||||
copies[i] = SN_INVALID_ID;
|
||||
regs->external_copies[ref.occurrence] = copies;
|
||||
}
|
||||
if (returned_module)
|
||||
*returned_module = module;
|
||||
return copies;
|
||||
}
|
||||
|
||||
static inline sn_obj_id_t sn_boundary_pack_bits(sn_module_t* module, const sn_obj_id_t* bits, uint32_t width,
|
||||
const char* name)
|
||||
{
|
||||
assert(module && bits && width);
|
||||
return width == 1 ? bits[0] : sn_module_add_operator(module, SN_CONCAT, width, false, width, bits, name);
|
||||
}
|
||||
|
||||
static inline sn_blast_hier_ref_t sn_boundary_parent_ref(const sn_design_t* design,
|
||||
const sn_blast_boundary_t* boundary,
|
||||
sn_blast_hier_ref_t ref)
|
||||
{
|
||||
const sn_blast_occurrence_t* occurrence;
|
||||
const sn_module_t* module;
|
||||
const sn_module_t* parent;
|
||||
sn_obj_id_t parent_fanin;
|
||||
assert(ref.occurrence < boundary->occurrences.size);
|
||||
occurrence = &sn_vec_at(sn_blast_occurrence_t, &boundary->occurrences, ref.occurrence);
|
||||
module = sn_design_get_module_const(design, occurrence->module);
|
||||
assert(sn_obj_type(module, ref.object) == SN_PI && occurrence->parent_occurrence != SN_INVALID_ID);
|
||||
parent = sn_design_get_module_const(
|
||||
design, sn_vec_at(sn_blast_occurrence_t, &boundary->occurrences, occurrence->parent_occurrence).module);
|
||||
parent_fanin = sn_obj_fanin(parent, occurrence->parent_inst, sn_obj_type_id(module, ref.object));
|
||||
ref.occurrence = occurrence->parent_occurrence;
|
||||
ref.object = parent_fanin;
|
||||
return ref;
|
||||
}
|
||||
|
||||
// Resolves clocks, asynchronous controls, and initialization constants that @blast intentionally leaves outside the
|
||||
// combinational cloud. Hierarchical PI bindings are followed to the root. Generated combinational control cones are
|
||||
// copied and memoized per hierarchy occurrence; an explicit DFS stack avoids overflowing the C stack on deep control
|
||||
// cones. The link table resolves inst, primitive, register, and loop endpoints in expected constant time.
|
||||
static inline sn_obj_id_t sn_boundary_resolve_external(sn_boundary_regs_t* regs, sn_blast_hier_ref_t ref)
|
||||
{
|
||||
sn_blast_hier_ref_t root = ref;
|
||||
sn_vec_t stack;
|
||||
sn_vec_init(&stack);
|
||||
sn_boundary_external_frame_t* initial = sn_vec_push(sn_boundary_external_frame_t, &stack);
|
||||
memset(initial, 0, sizeof(*initial));
|
||||
initial->ref = ref;
|
||||
while (stack.size)
|
||||
{
|
||||
sn_boundary_external_frame_t* frame =
|
||||
&sn_vec_at(sn_boundary_external_frame_t, &stack, stack.size - 1);
|
||||
ref = frame->ref;
|
||||
const sn_blast_occurrence_t* occurrence =
|
||||
&sn_vec_at(sn_blast_occurrence_t, ®s->boundary->occurrences, ref.occurrence);
|
||||
const sn_module_t* module;
|
||||
sn_obj_id_t* copies = sn_boundary_external_copies(regs, ref, &module);
|
||||
if (frame->phase == SN_BOUNDARY_EXTERNAL_ALIAS)
|
||||
{
|
||||
const sn_module_t* dependency_module;
|
||||
sn_obj_id_t* dependency_copies =
|
||||
sn_boundary_external_copies(regs, frame->dependency, &dependency_module);
|
||||
(void)dependency_module;
|
||||
assert(dependency_copies[frame->dependency.object] != SN_INVALID_ID);
|
||||
copies[ref.object] = dependency_copies[frame->dependency.object];
|
||||
stack.size--;
|
||||
continue;
|
||||
}
|
||||
if (frame->phase == SN_BOUNDARY_EXTERNAL_OPERATOR)
|
||||
{
|
||||
uint32_t count = sn_obj_fanin_count(module, ref.object);
|
||||
if (frame->next_fanin == count)
|
||||
{
|
||||
stack.size--;
|
||||
continue;
|
||||
}
|
||||
uint32_t index = frame->next_fanin;
|
||||
sn_obj_id_t old_fanin = sn_obj_fanin(module, ref.object, index);
|
||||
if (old_fanin == SN_INVALID_ID)
|
||||
{
|
||||
sn_obj_connect(regs->result, frame->result, index, SN_INVALID_ID);
|
||||
frame->next_fanin++;
|
||||
continue;
|
||||
}
|
||||
sn_blast_hier_ref_t dependency = {ref.occurrence, old_fanin, 0};
|
||||
sn_obj_id_t* dependency_copies = sn_boundary_external_copies(regs, dependency, NULL);
|
||||
if (dependency_copies[old_fanin] != SN_INVALID_ID)
|
||||
{
|
||||
sn_obj_connect(regs->result, frame->result, index, dependency_copies[old_fanin]);
|
||||
frame->next_fanin++;
|
||||
continue;
|
||||
}
|
||||
sn_boundary_external_frame_t* child = sn_vec_push(sn_boundary_external_frame_t, &stack);
|
||||
memset(child, 0, sizeof(*child));
|
||||
child->ref = dependency;
|
||||
continue;
|
||||
}
|
||||
if (copies[ref.object] != SN_INVALID_ID)
|
||||
{
|
||||
stack.size--;
|
||||
continue;
|
||||
}
|
||||
sn_obj_type_t type = sn_obj_type(module, ref.object);
|
||||
if (type == SN_PI && occurrence->parent_occurrence != SN_INVALID_ID)
|
||||
{
|
||||
frame->phase = SN_BOUNDARY_EXTERNAL_ALIAS;
|
||||
frame->dependency = sn_boundary_parent_ref(regs->design, regs->boundary, ref);
|
||||
sn_obj_id_t* dependency_copies = sn_boundary_external_copies(regs, frame->dependency, NULL);
|
||||
if (dependency_copies[frame->dependency.object] == SN_INVALID_ID)
|
||||
{
|
||||
sn_boundary_external_frame_t* child = sn_vec_push(sn_boundary_external_frame_t, &stack);
|
||||
memset(child, 0, sizeof(*child));
|
||||
child->ref = frame->dependency;
|
||||
}
|
||||
continue;
|
||||
}
|
||||
if (type == SN_PI)
|
||||
{
|
||||
assert(ref.occurrence == 0 && regs->top_inputs[ref.object] != SN_INVALID_ID);
|
||||
copies[ref.object] = regs->top_inputs[ref.object];
|
||||
stack.size--;
|
||||
continue;
|
||||
}
|
||||
if (type == SN_INST || type == SN_FAN)
|
||||
{
|
||||
sn_obj_id_t inst = type == SN_INST ? ref.object : sn_fan_inst_id(module, ref.object);
|
||||
uint32_t output = type == SN_INST ? 0 : sn_fan_output_index(module, ref.object);
|
||||
sn_boundary_link_t* link = sn_boundary_link_find(regs, ref.occurrence, inst, false);
|
||||
assert(link);
|
||||
if (link->primitive != SN_INVALID_ID)
|
||||
{
|
||||
const sn_blast_primitive_t* primitive =
|
||||
&sn_vec_at(sn_blast_primitive_t, ®s->boundary->primitives, link->primitive);
|
||||
assert(output < sn_design_module_output_count(regs->design, primitive->module));
|
||||
(void)primitive;
|
||||
copies[ref.object] = regs->primitive_pairs[regs->primitive_offsets[link->primitive] + output].out;
|
||||
stack.size--;
|
||||
continue;
|
||||
}
|
||||
if (link->child != SN_INVALID_ID)
|
||||
{
|
||||
const sn_blast_occurrence_t* child_occurrence =
|
||||
&sn_vec_at(sn_blast_occurrence_t, ®s->boundary->occurrences, link->child);
|
||||
const sn_module_t* child = sn_design_get_module_const(regs->design, child_occurrence->module);
|
||||
assert(output < child->type_objects[SN_PO].size);
|
||||
sn_obj_id_t child_po = sn_vec_at(sn_obj_id_t, &child->type_objects[SN_PO], output);
|
||||
sn_obj_id_t child_fanin = sn_obj_fanin(child, child_po, 0);
|
||||
assert(child_fanin != SN_INVALID_ID);
|
||||
frame->phase = SN_BOUNDARY_EXTERNAL_ALIAS;
|
||||
frame->dependency.occurrence = link->child;
|
||||
frame->dependency.object = child_fanin;
|
||||
frame->dependency.bit = 0;
|
||||
sn_obj_id_t* dependency_copies = sn_boundary_external_copies(regs, frame->dependency, NULL);
|
||||
if (dependency_copies[child_fanin] == SN_INVALID_ID)
|
||||
{
|
||||
sn_boundary_external_frame_t* child_frame =
|
||||
sn_vec_push(sn_boundary_external_frame_t, &stack);
|
||||
memset(child_frame, 0, sizeof(*child_frame));
|
||||
child_frame->ref = frame->dependency;
|
||||
}
|
||||
continue;
|
||||
}
|
||||
assert(false);
|
||||
}
|
||||
if (type == SN_CONST0 || type == SN_CONST1 || type == SN_CONST)
|
||||
{
|
||||
uint32_t width = sn_obj_width(module, ref.object);
|
||||
uint32_t* words = (uint32_t*)calloc(sn_const_word_count(width), sizeof(uint32_t));
|
||||
assert(words);
|
||||
for (uint32_t bit = 0; bit < width; bit++)
|
||||
words[bit >> 5] |= (uint32_t)sn_const_bit(module, ref.object, bit) << (bit & 31);
|
||||
const char* name = sn_obj_name_id(module, ref.object) == SN_INVALID_ID
|
||||
? NULL
|
||||
: sn_obj_name(module, ref.object);
|
||||
sn_obj_id_t result = sn_module_add_const(regs->result, width, sn_obj_is_signed(module, ref.object), words,
|
||||
name);
|
||||
free(words);
|
||||
copies[ref.object] = result;
|
||||
stack.size--;
|
||||
continue;
|
||||
}
|
||||
if (type == SN_REG_OUT)
|
||||
{
|
||||
sn_boundary_link_t* link = sn_boundary_link_find(regs, ref.occurrence, ref.object, false);
|
||||
assert(link && link->reg != SN_INVALID_ID);
|
||||
copies[ref.object] = regs->pairs[link->reg].out;
|
||||
stack.size--;
|
||||
continue;
|
||||
}
|
||||
if (type == SN_LOOP_OUT)
|
||||
{
|
||||
sn_boundary_link_t* link = sn_boundary_link_find(regs, ref.occurrence, ref.object, false);
|
||||
assert(link && link->loop != SN_INVALID_ID);
|
||||
copies[ref.object] = regs->loops[link->loop].out;
|
||||
stack.size--;
|
||||
continue;
|
||||
}
|
||||
assert(type == SN_BUF || (type >= SN_POS && type <= SN_GATE));
|
||||
frame->result = sn_module_dup_obj_skeleton(regs->result, module, ref.object);
|
||||
copies[ref.object] = frame->result;
|
||||
sn_module_dup_obj_metadata(regs->result, sn_obj_type_id(regs->result, frame->result), module, ref.object);
|
||||
frame->phase = SN_BOUNDARY_EXTERNAL_OPERATOR;
|
||||
frame->next_fanin = 0;
|
||||
}
|
||||
sn_obj_id_t* root_copies = sn_boundary_external_copies(regs, root, NULL);
|
||||
assert(root_copies[root.object] != SN_INVALID_ID);
|
||||
sn_obj_id_t result = root_copies[root.object];
|
||||
sn_vec_destroy(&stack);
|
||||
return result;
|
||||
}
|
||||
|
||||
static inline void sn_boundary_regs_init(sn_boundary_regs_t* regs, sn_design_t* design,
|
||||
const sn_blast_boundary_t* boundary, sn_module_t* result,
|
||||
sn_obj_id_t* top_inputs)
|
||||
{
|
||||
assert(regs && design && boundary && result && top_inputs);
|
||||
regs->design = design;
|
||||
regs->boundary = boundary;
|
||||
regs->result = result;
|
||||
regs->top_inputs = top_inputs;
|
||||
regs->external_copies = boundary->occurrences.size
|
||||
? (sn_obj_id_t**)calloc(boundary->occurrences.size, sizeof(sn_obj_id_t*))
|
||||
: NULL;
|
||||
assert(regs->external_copies || boundary->occurrences.size == 0);
|
||||
regs->links = NULL;
|
||||
regs->link_cap = 0;
|
||||
regs->primitive_offsets = boundary->primitives.size
|
||||
? (uint32_t*)malloc(sizeof(uint32_t) * (boundary->primitives.size + 1))
|
||||
: NULL;
|
||||
assert(regs->primitive_offsets || boundary->primitives.size == 0);
|
||||
uint32_t primitive_output_count = 0;
|
||||
for (size_t i = 0; i < boundary->primitives.size; i++)
|
||||
{
|
||||
const sn_blast_primitive_t* entry = &sn_vec_at(sn_blast_primitive_t, &boundary->primitives, i);
|
||||
regs->primitive_offsets[i] = primitive_output_count;
|
||||
primitive_output_count += sn_design_module_output_count(design, entry->module);
|
||||
}
|
||||
if (boundary->primitives.size)
|
||||
regs->primitive_offsets[boundary->primitives.size] = primitive_output_count;
|
||||
regs->primitive_pairs = primitive_output_count
|
||||
? (sn_obj_pair_t*)malloc(sizeof(sn_obj_pair_t) * primitive_output_count)
|
||||
: NULL;
|
||||
assert(regs->primitive_pairs || primitive_output_count == 0);
|
||||
for (size_t i = 0; i < boundary->primitives.size; i++)
|
||||
{
|
||||
const sn_blast_primitive_t* entry = &sn_vec_at(sn_blast_primitive_t, &boundary->primitives, i);
|
||||
const sn_blast_occurrence_t* occurrence =
|
||||
&sn_vec_at(sn_blast_occurrence_t, &boundary->occurrences, entry->occurrence);
|
||||
const sn_module_t* module = sn_design_get_module_const(design, occurrence->module);
|
||||
const sn_module_t* child = sn_design_get_module_const(design, entry->module);
|
||||
for (size_t output = 0; output < child->type_objects[SN_PO].size; output++)
|
||||
{
|
||||
sn_obj_id_t old_output = child->type_objects[SN_PO].size == 1
|
||||
? entry->inst
|
||||
: sn_inst_output(module, entry->inst, (uint32_t)output);
|
||||
const char* output_name = sn_obj_name_id(module, old_output) == SN_INVALID_ID
|
||||
? NULL
|
||||
: sn_obj_name(module, old_output);
|
||||
regs->primitive_pairs[regs->primitive_offsets[i] + output] =
|
||||
sn_module_add_loop_pair(result, sn_obj_width(module, old_output),
|
||||
sn_obj_is_signed(module, old_output), output_name, "primitive_boundary_input");
|
||||
}
|
||||
}
|
||||
regs->pairs = boundary->registers.size
|
||||
? (sn_obj_pair_t*)malloc(sizeof(sn_obj_pair_t) * boundary->registers.size)
|
||||
: NULL;
|
||||
assert(regs->pairs || boundary->registers.size == 0);
|
||||
for (size_t i = 0; i < boundary->registers.size; i++)
|
||||
{
|
||||
const sn_blast_register_t* entry = &sn_vec_at(sn_blast_register_t, &boundary->registers, i);
|
||||
const sn_blast_occurrence_t* occurrence =
|
||||
&sn_vec_at(sn_blast_occurrence_t, &boundary->occurrences, entry->occurrence);
|
||||
const sn_module_t* module = sn_design_get_module_const(design, occurrence->module);
|
||||
sn_obj_id_t old_out = entry->reg_out;
|
||||
sn_obj_id_t old_in = sn_obj_pair_in(module, old_out);
|
||||
const char* out_name = sn_obj_name_id(module, old_out) == SN_INVALID_ID ? NULL : sn_obj_name(module, old_out);
|
||||
const char* in_name = sn_obj_name_id(module, old_in) == SN_INVALID_ID ? NULL : sn_obj_name(module, old_in);
|
||||
regs->pairs[i] = sn_module_add_reg_pair(result, entry->width, sn_obj_is_signed(module, old_out),
|
||||
out_name, in_name, SN_INVALID_ID);
|
||||
sn_reg_set_flags(result, regs->pairs[i].out, sn_obj_reg_flags(module, old_out));
|
||||
}
|
||||
regs->loops = boundary->loops.size ? (sn_obj_pair_t*)malloc(sizeof(sn_obj_pair_t) * boundary->loops.size) : NULL;
|
||||
assert(regs->loops || boundary->loops.size == 0);
|
||||
for (size_t i = 0; i < boundary->loops.size; i++)
|
||||
{
|
||||
const sn_blast_loop_t* entry = &sn_vec_at(sn_blast_loop_t, &boundary->loops, i);
|
||||
const sn_blast_occurrence_t* occurrence =
|
||||
&sn_vec_at(sn_blast_occurrence_t, &boundary->occurrences, entry->occurrence);
|
||||
const sn_module_t* module = sn_design_get_module_const(design, occurrence->module);
|
||||
sn_obj_id_t old_in = sn_obj_pair_in(module, entry->loop_out);
|
||||
const char* out_name = sn_obj_name_id(module, entry->loop_out) == SN_INVALID_ID
|
||||
? NULL
|
||||
: sn_obj_name(module, entry->loop_out);
|
||||
const char* in_name = sn_obj_name_id(module, old_in) == SN_INVALID_ID ? NULL : sn_obj_name(module, old_in);
|
||||
regs->loops[i] = sn_module_add_loop_pair(result, entry->width,
|
||||
sn_obj_is_signed(module, entry->loop_out), out_name, in_name);
|
||||
}
|
||||
|
||||
size_t link_count = boundary->primitives.size + boundary->registers.size + boundary->loops.size;
|
||||
if (boundary->occurrences.size)
|
||||
link_count += boundary->occurrences.size - 1;
|
||||
if (link_count)
|
||||
{
|
||||
regs->link_cap = 2;
|
||||
while (regs->link_cap < 2 * link_count)
|
||||
regs->link_cap <<= 1;
|
||||
regs->links = (sn_boundary_link_t*)malloc(regs->link_cap * sizeof(sn_boundary_link_t));
|
||||
assert(regs->links);
|
||||
for (size_t i = 0; i < regs->link_cap; i++)
|
||||
{
|
||||
regs->links[i].key = UINT64_MAX;
|
||||
regs->links[i].primitive = SN_INVALID_ID;
|
||||
regs->links[i].child = SN_INVALID_ID;
|
||||
regs->links[i].reg = SN_INVALID_ID;
|
||||
regs->links[i].loop = SN_INVALID_ID;
|
||||
}
|
||||
for (size_t i = 0; i < boundary->primitives.size; i++)
|
||||
{
|
||||
const sn_blast_primitive_t* entry = &sn_vec_at(sn_blast_primitive_t, &boundary->primitives, i);
|
||||
sn_boundary_link_find(regs, entry->occurrence, entry->inst, true)->primitive = (uint32_t)i;
|
||||
}
|
||||
for (size_t i = 1; i < boundary->occurrences.size; i++)
|
||||
{
|
||||
const sn_blast_occurrence_t* entry = &sn_vec_at(sn_blast_occurrence_t, &boundary->occurrences, i);
|
||||
sn_boundary_link_find(regs, entry->parent_occurrence, entry->parent_inst, true)->child = (uint32_t)i;
|
||||
}
|
||||
for (size_t i = 0; i < boundary->registers.size; i++)
|
||||
{
|
||||
const sn_blast_register_t* entry = &sn_vec_at(sn_blast_register_t, &boundary->registers, i);
|
||||
sn_boundary_link_find(regs, entry->occurrence, entry->reg_out, true)->reg = (uint32_t)i;
|
||||
}
|
||||
for (size_t i = 0; i < boundary->loops.size; i++)
|
||||
{
|
||||
const sn_blast_loop_t* entry = &sn_vec_at(sn_blast_loop_t, &boundary->loops, i);
|
||||
sn_boundary_link_find(regs, entry->occurrence, entry->loop_out, true)->loop = (uint32_t)i;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
static inline sn_obj_id_t sn_boundary_primitive_output_bit(sn_boundary_regs_t* regs, uint32_t owner,
|
||||
uint32_t port, uint32_t bit)
|
||||
{
|
||||
assert(owner < regs->boundary->primitives.size);
|
||||
const sn_blast_primitive_t* entry = &sn_vec_at(sn_blast_primitive_t, ®s->boundary->primitives, owner);
|
||||
assert(port < sn_design_module_output_count(regs->design, entry->module));
|
||||
(void)entry;
|
||||
sn_obj_id_t output = regs->primitive_pairs[regs->primitive_offsets[owner] + port].out;
|
||||
assert(bit < sn_obj_width(regs->result, output));
|
||||
return sn_module_add_slice(regs->result, output, (int32_t)bit, (int32_t)bit, "primitive_output_bit");
|
||||
}
|
||||
|
||||
static inline sn_obj_id_t sn_boundary_reg_output_bit(sn_boundary_regs_t* regs, uint32_t owner, uint32_t bit)
|
||||
{
|
||||
assert(owner < regs->boundary->registers.size);
|
||||
assert(bit < sn_obj_width(regs->result, regs->pairs[owner].out));
|
||||
return sn_module_add_slice(regs->result, regs->pairs[owner].out, (int32_t)bit, (int32_t)bit, "reg_q_bit");
|
||||
}
|
||||
|
||||
static inline sn_obj_id_t sn_boundary_loop_output_bit(sn_boundary_regs_t* regs, uint32_t owner, uint32_t bit)
|
||||
{
|
||||
assert(owner < regs->boundary->loops.size);
|
||||
assert(bit < sn_obj_width(regs->result, regs->loops[owner].out));
|
||||
return sn_module_add_slice(regs->result, regs->loops[owner].out, (int32_t)bit, (int32_t)bit, "loop_q_bit");
|
||||
}
|
||||
|
||||
static inline sn_obj_id_t sn_boundary_co_word(sn_boundary_regs_t* regs, const sn_obj_id_t* co_drivers,
|
||||
uint32_t begin, sn_blast_boundary_kind_t kind, uint32_t owner,
|
||||
uint32_t port, uint32_t width)
|
||||
{
|
||||
assert(begin <= regs->boundary->cos.size && width <= regs->boundary->cos.size - begin);
|
||||
for (uint32_t bit = 0; bit < width; bit++)
|
||||
{
|
||||
sn_blast_boundary_bit_t endpoint =
|
||||
sn_vec_at(sn_blast_boundary_bit_t, ®s->boundary->cos, begin + bit);
|
||||
assert(endpoint.kind == kind && endpoint.owner == owner &&
|
||||
(port == SN_INVALID_ID || endpoint.port == port) && endpoint.signal.bit == bit);
|
||||
}
|
||||
return sn_boundary_pack_bits(regs->result, co_drivers + begin, width, "boundary_word");
|
||||
}
|
||||
|
||||
typedef struct sn_boundary_dfs_frame_t
|
||||
{
|
||||
sn_obj_id_t object;
|
||||
uint32_t next_fanout;
|
||||
} sn_boundary_dfs_frame_t;
|
||||
|
||||
// Marks tentative primitive-output substitutions that create combinational feedback. All temporary pair outputs
|
||||
// have already been replaced by the corresponding primitive outputs. One iterative Kosaraju traversal identifies
|
||||
// the resulting strongly connected components; a substituted edge whose endpoints share a component must retain
|
||||
// its loop pair. This replaces one complete cone walk per primitive output by linear whole-module graph work.
|
||||
static inline void sn_boundary_mark_feedback_pairs(sn_module_t* module, const sn_obj_id_t* actual_to_pair,
|
||||
uint8_t* keep)
|
||||
{
|
||||
size_t object_count = module->obj_types.size;
|
||||
uint8_t* visited = (uint8_t*)calloc(object_count, sizeof(uint8_t));
|
||||
uint32_t* components = object_count ? (uint32_t*)malloc(object_count * sizeof(uint32_t)) : NULL;
|
||||
sn_vec_t order, stack;
|
||||
assert(visited && (components || object_count == 0));
|
||||
sn_vec_init(&order);
|
||||
sn_vec_init(&stack);
|
||||
sn_vec_reserve(sn_obj_id_t, &order, object_count);
|
||||
sn_module_build_fanouts(module);
|
||||
|
||||
for (sn_obj_id_t start = 0; start < object_count; start++)
|
||||
{
|
||||
if (visited[start])
|
||||
continue;
|
||||
visited[start] = 1;
|
||||
sn_boundary_dfs_frame_t* first = sn_vec_push(sn_boundary_dfs_frame_t, &stack);
|
||||
first->object = start;
|
||||
first->next_fanout = 0;
|
||||
while (stack.size)
|
||||
{
|
||||
sn_boundary_dfs_frame_t* frame =
|
||||
&sn_vec_at(sn_boundary_dfs_frame_t, &stack, stack.size - 1);
|
||||
uint32_t count = sn_obj_fanout_count(module, frame->object);
|
||||
if (frame->next_fanout < count)
|
||||
{
|
||||
sn_obj_id_t fanout = sn_obj_fanout(module, frame->object, frame->next_fanout++);
|
||||
if (!visited[fanout])
|
||||
{
|
||||
visited[fanout] = 1;
|
||||
sn_boundary_dfs_frame_t* child = sn_vec_push(sn_boundary_dfs_frame_t, &stack);
|
||||
child->object = fanout;
|
||||
child->next_fanout = 0;
|
||||
}
|
||||
continue;
|
||||
}
|
||||
*sn_vec_push(sn_obj_id_t, &order) = frame->object;
|
||||
stack.size--;
|
||||
}
|
||||
}
|
||||
|
||||
for (sn_obj_id_t object = 0; object < object_count; object++)
|
||||
components[object] = UINT32_MAX;
|
||||
uint32_t component_count = 0;
|
||||
for (size_t i = order.size; i-- > 0;)
|
||||
{
|
||||
sn_obj_id_t start = sn_vec_at(sn_obj_id_t, &order, i);
|
||||
if (components[start] != UINT32_MAX)
|
||||
continue;
|
||||
components[start] = component_count;
|
||||
*sn_vec_push(sn_obj_id_t, &stack) = start;
|
||||
while (stack.size)
|
||||
{
|
||||
sn_obj_id_t object = sn_vec_at(sn_obj_id_t, &stack, --stack.size);
|
||||
for (uint32_t k = 0; k < sn_obj_fanin_count(module, object); k++)
|
||||
{
|
||||
sn_obj_id_t fanin = sn_obj_fanin(module, object, k);
|
||||
if (fanin != SN_INVALID_ID && components[fanin] == UINT32_MAX)
|
||||
{
|
||||
components[fanin] = component_count;
|
||||
*sn_vec_push(sn_obj_id_t, &stack) = fanin;
|
||||
}
|
||||
}
|
||||
}
|
||||
component_count++;
|
||||
}
|
||||
|
||||
for (sn_obj_id_t object = 0; object < object_count; object++)
|
||||
for (uint32_t i = 0; i < sn_obj_fanin_count(module, object); i++)
|
||||
{
|
||||
sn_obj_id_t actual = sn_obj_fanin(module, object, i);
|
||||
sn_obj_id_t pair_out = actual == SN_INVALID_ID ? SN_INVALID_ID : actual_to_pair[actual];
|
||||
if (pair_out != SN_INVALID_ID && components[actual] == components[object])
|
||||
keep[pair_out] = 1;
|
||||
}
|
||||
|
||||
sn_module_invalidate_fanouts(module);
|
||||
sn_vec_destroy(&order);
|
||||
sn_vec_destroy(&stack);
|
||||
free(components);
|
||||
free(visited);
|
||||
}
|
||||
|
||||
// Duplicates a module in topological order while omitting an explicitly unreferenced set of objects. This is used
|
||||
// to remove temporary primitive-output loop pairs after their consumers have been redirected to the real outputs.
|
||||
static inline sn_module_id_t sn_boundary_dup_filtered_topo(sn_design_t* design, sn_module_id_t source_id,
|
||||
const uint8_t* remove, const char* name)
|
||||
{
|
||||
sn_module_t* source = sn_design_get_module(design, source_id);
|
||||
size_t object_count = source->obj_types.size;
|
||||
uint8_t* marks = (uint8_t*)calloc(object_count, sizeof(uint8_t));
|
||||
sn_vec_t order;
|
||||
assert(marks);
|
||||
sn_vec_init(&order);
|
||||
sn_vec_reserve(sn_obj_id_t, &order, object_count);
|
||||
for (sn_obj_id_t object = 0; object < object_count; object++)
|
||||
if (remove[object])
|
||||
marks[object] = SN_TOPO_DONE;
|
||||
for (size_t i = 0; i < source->type_objects[SN_PI].size; i++)
|
||||
{
|
||||
sn_obj_id_t object = sn_vec_at(sn_obj_id_t, &source->type_objects[SN_PI], i);
|
||||
assert(!remove[object]);
|
||||
marks[object] = SN_TOPO_DONE;
|
||||
*sn_vec_push(sn_obj_id_t, &order) = object;
|
||||
}
|
||||
for (sn_obj_id_t object = 0; object < object_count; object++)
|
||||
if (!remove[object] && sn_obj_type_is_pair_out(sn_obj_type(source, object)))
|
||||
{
|
||||
marks[object] = SN_TOPO_DONE;
|
||||
*sn_vec_push(sn_obj_id_t, &order) = object;
|
||||
}
|
||||
sn_topo_context_t context = {source, &order, marks};
|
||||
for (size_t i = 0; i < source->type_objects[SN_PO].size; i++)
|
||||
{
|
||||
sn_obj_id_t output = sn_vec_at(sn_obj_id_t, &source->type_objects[SN_PO], i);
|
||||
for (uint32_t j = 0; j < sn_obj_fanin_count(source, output); j++)
|
||||
{
|
||||
sn_obj_id_t fanin = sn_obj_fanin(source, output, j);
|
||||
if (fanin != SN_INVALID_ID)
|
||||
sn_module_topo_visit(&context, fanin);
|
||||
}
|
||||
}
|
||||
for (sn_obj_id_t object = 0; object < object_count; object++)
|
||||
{
|
||||
sn_obj_type_t type = sn_obj_type(source, object);
|
||||
if (type != SN_PI && type != SN_PO && marks[object] == SN_TOPO_UNSEEN)
|
||||
sn_module_topo_visit(&context, object);
|
||||
}
|
||||
for (size_t i = 0; i < source->type_objects[SN_PO].size; i++)
|
||||
{
|
||||
sn_obj_id_t output = sn_vec_at(sn_obj_id_t, &source->type_objects[SN_PO], i);
|
||||
marks[output] = SN_TOPO_DONE;
|
||||
*sn_vec_push(sn_obj_id_t, &order) = output;
|
||||
}
|
||||
|
||||
sn_module_id_t target_id = sn_design_add_module(design, name);
|
||||
sn_module_t* target = sn_design_get_module(design, target_id);
|
||||
sn_vec_resize(sn_obj_id_t, &source->copy_ids, object_count);
|
||||
for (sn_obj_id_t object = 0; object < object_count; object++)
|
||||
sn_vec_at(sn_obj_id_t, &source->copy_ids, object) = SN_INVALID_ID;
|
||||
for (size_t i = 0; i < order.size; i++)
|
||||
{
|
||||
sn_obj_id_t old_object = sn_vec_at(sn_obj_id_t, &order, i);
|
||||
sn_vec_at(sn_obj_id_t, &source->copy_ids, old_object) =
|
||||
sn_module_dup_obj_skeleton(target, source, old_object);
|
||||
}
|
||||
sn_module_clean_rebuild_pair_ids(target, source, SN_REG_OUT, SN_REG_IN);
|
||||
sn_module_clean_rebuild_pair_ids(target, source, SN_MEM_OUT, SN_MEM_IN);
|
||||
sn_module_clean_rebuild_pair_ids(target, source, SN_LOOP_OUT, SN_LOOP_IN);
|
||||
for (size_t i = 0; i < order.size; i++)
|
||||
{
|
||||
sn_obj_id_t old_object = sn_vec_at(sn_obj_id_t, &order, i);
|
||||
sn_obj_id_t new_object = sn_vec_at(sn_obj_id_t, &source->copy_ids, old_object);
|
||||
sn_obj_type_t type = sn_obj_type(source, old_object);
|
||||
sn_module_dup_obj_metadata(target, sn_obj_type_id(target, new_object), source, old_object);
|
||||
if (type == SN_FAN)
|
||||
sn_vec_at(sn_obj_id_t, &target->fan_insts, sn_obj_type_id(target, new_object)) =
|
||||
sn_vec_at(sn_obj_id_t, &source->copy_ids, sn_fan_inst_id(source, old_object));
|
||||
for (uint32_t j = 0; j < sn_obj_fanin_count(source, old_object); j++)
|
||||
{
|
||||
sn_obj_id_t old_fanin = sn_obj_fanin(source, old_object, j);
|
||||
sn_obj_id_t new_fanin = old_fanin == SN_INVALID_ID
|
||||
? SN_INVALID_ID
|
||||
: sn_vec_at(sn_obj_id_t, &source->copy_ids, old_fanin);
|
||||
assert(new_fanin != SN_INVALID_ID || old_fanin == SN_INVALID_ID);
|
||||
sn_obj_connect(target, new_object, j, new_fanin);
|
||||
}
|
||||
}
|
||||
source->copy_module = target_id;
|
||||
sn_vec_destroy(&order);
|
||||
free(marks);
|
||||
assert(sn_module_is_topo(target));
|
||||
return target_id;
|
||||
}
|
||||
|
||||
static inline void sn_boundary_prune_primitive_pairs(sn_boundary_regs_t* regs)
|
||||
{
|
||||
sn_module_t* source = regs->result;
|
||||
size_t object_count = source->obj_types.size;
|
||||
uint8_t* remove = (uint8_t*)calloc(object_count, sizeof(uint8_t));
|
||||
uint8_t* keep = (uint8_t*)calloc(object_count, sizeof(uint8_t));
|
||||
sn_obj_id_t* replacement = object_count ? (sn_obj_id_t*)malloc(object_count * sizeof(sn_obj_id_t)) : NULL;
|
||||
sn_obj_id_t* actual_to_pair = object_count ? (sn_obj_id_t*)malloc(object_count * sizeof(sn_obj_id_t)) : NULL;
|
||||
size_t remove_count = 0;
|
||||
assert(remove && keep && (replacement || object_count == 0) && (actual_to_pair || object_count == 0));
|
||||
for (sn_obj_id_t object = 0; object < object_count; object++)
|
||||
replacement[object] = actual_to_pair[object] = SN_INVALID_ID;
|
||||
for (size_t i = 0; i < regs->boundary->primitives.size; i++)
|
||||
{
|
||||
const sn_blast_primitive_t* entry = &sn_vec_at(sn_blast_primitive_t, ®s->boundary->primitives, i);
|
||||
uint32_t output_count = sn_design_module_output_count(regs->design, entry->module);
|
||||
for (uint32_t output = 0; output < output_count; output++)
|
||||
{
|
||||
sn_obj_pair_t pair = regs->primitive_pairs[regs->primitive_offsets[i] + output];
|
||||
sn_obj_id_t actual = sn_obj_fanin(source, pair.in, 0);
|
||||
assert(replacement[pair.out] == SN_INVALID_ID && actual_to_pair[actual] == SN_INVALID_ID);
|
||||
replacement[pair.out] = actual;
|
||||
actual_to_pair[actual] = pair.out;
|
||||
}
|
||||
}
|
||||
for (size_t i = 0; i < source->fanins.size; i++)
|
||||
{
|
||||
sn_obj_id_t fanin = sn_vec_at(sn_obj_id_t, &source->fanins, i);
|
||||
if (fanin != SN_INVALID_ID && replacement[fanin] != SN_INVALID_ID)
|
||||
sn_vec_at(sn_obj_id_t, &source->fanins, i) = replacement[fanin];
|
||||
}
|
||||
sn_module_invalidate_fanouts(source);
|
||||
sn_boundary_mark_feedback_pairs(source, actual_to_pair, keep);
|
||||
for (sn_obj_id_t object = 0; object < object_count; object++)
|
||||
for (uint32_t i = 0; i < sn_obj_fanin_count(source, object); i++)
|
||||
{
|
||||
sn_obj_id_t actual = sn_obj_fanin(source, object, i);
|
||||
sn_obj_id_t pair_out = actual == SN_INVALID_ID ? SN_INVALID_ID : actual_to_pair[actual];
|
||||
if (pair_out != SN_INVALID_ID && keep[pair_out] && object != sn_obj_pair_in(source, pair_out))
|
||||
sn_obj_connect(source, object, i, pair_out);
|
||||
}
|
||||
for (sn_obj_id_t pair_out = 0; pair_out < object_count; pair_out++)
|
||||
if (replacement[pair_out] != SN_INVALID_ID && !keep[pair_out])
|
||||
{
|
||||
sn_obj_id_t actual = replacement[pair_out];
|
||||
sn_obj_id_t pair_in = sn_obj_pair_in(source, pair_out);
|
||||
if (sn_obj_type(source, actual) == SN_FAN && sn_obj_name_id(source, actual) == SN_INVALID_ID &&
|
||||
sn_obj_name_id(source, pair_out) != SN_INVALID_ID)
|
||||
sn_vec_at(sn_name_id_t, &source->name_ids, actual) = sn_obj_name_id(source, pair_out);
|
||||
remove[pair_out] = remove[pair_in] = 1;
|
||||
remove_count += 2;
|
||||
}
|
||||
sn_module_invalidate_fanouts(source);
|
||||
if (remove_count)
|
||||
{
|
||||
char name[96];
|
||||
uint32_t suffix = 0;
|
||||
do
|
||||
{
|
||||
int length = snprintf(name, sizeof(name), "__sn_boundary_%u_%u", source->id, suffix++);
|
||||
assert(length >= 0 && (size_t)length < sizeof(name) && suffix != 0);
|
||||
} while (sn_name_find(®s->design->names, name) != SN_INVALID_ID);
|
||||
sn_module_id_t source_id = source->id;
|
||||
sn_name_id_t source_name = source->name;
|
||||
bool interface_locked = source->interface_locked;
|
||||
sn_module_id_t filtered_id = sn_boundary_dup_filtered_topo(regs->design, source_id, remove, name);
|
||||
sn_module_t* filtered = sn_design_get_module(regs->design, filtered_id);
|
||||
sn_name_id_t temporary_name = filtered->name;
|
||||
sn_design_invalidate_copies_to_module(regs->design, source_id);
|
||||
sn_module_destroy(source);
|
||||
free(source);
|
||||
filtered->id = source_id;
|
||||
filtered->name = source_name;
|
||||
filtered->interface_locked = interface_locked;
|
||||
sn_vec_at(sn_module_t*, ®s->design->modules, source_id) = filtered;
|
||||
regs->design->modules.size--;
|
||||
sn_name_remove_last(®s->design->names, temporary_name);
|
||||
regs->result = filtered;
|
||||
}
|
||||
free(actual_to_pair);
|
||||
free(replacement);
|
||||
free(keep);
|
||||
free(remove);
|
||||
}
|
||||
|
||||
static inline void sn_boundary_regs_finish(sn_boundary_regs_t* regs, const sn_obj_id_t* co_drivers)
|
||||
{
|
||||
for (size_t i = 0; i < regs->boundary->primitives.size; i++)
|
||||
{
|
||||
const sn_blast_primitive_t* entry = &sn_vec_at(sn_blast_primitive_t, ®s->boundary->primitives, i);
|
||||
const sn_blast_occurrence_t* occurrence =
|
||||
&sn_vec_at(sn_blast_occurrence_t, ®s->boundary->occurrences, entry->occurrence);
|
||||
const sn_module_t* module = sn_design_get_module_const(regs->design, occurrence->module);
|
||||
const sn_module_t* child = sn_design_get_module_const(regs->design, entry->module);
|
||||
uint32_t input_count = (uint32_t)child->type_objects[SN_PI].size;
|
||||
sn_obj_id_t* inputs = input_count ? (sn_obj_id_t*)malloc(sizeof(sn_obj_id_t) * input_count) : NULL;
|
||||
assert(inputs || input_count == 0);
|
||||
uint32_t co_begin = entry->co_begin;
|
||||
for (uint32_t input = 0; input < input_count; input++)
|
||||
{
|
||||
sn_obj_id_t port = sn_vec_at(sn_obj_id_t, &child->type_objects[SN_PI], input);
|
||||
uint32_t width = sn_obj_width(child, port);
|
||||
inputs[input] = sn_boundary_co_word(regs, co_drivers, co_begin, SN_BLAST_BOUNDARY_PRIMITIVE_INPUT,
|
||||
(uint32_t)i, input, width);
|
||||
co_begin += width;
|
||||
}
|
||||
assert(co_begin == entry->co_begin + entry->co_count);
|
||||
const char* inst_name = sn_obj_name_id(module, entry->inst) == SN_INVALID_ID
|
||||
? NULL
|
||||
: sn_obj_name(module, entry->inst);
|
||||
sn_obj_id_t inst = sn_module_add_inst(regs->result, entry->module, input_count, inputs, inst_name, NULL);
|
||||
free(inputs);
|
||||
for (uint32_t output = 0; output < child->type_objects[SN_PO].size; output++)
|
||||
{
|
||||
sn_obj_pair_t pair = regs->primitive_pairs[regs->primitive_offsets[i] + output];
|
||||
sn_obj_connect(regs->result, pair.in, 0, sn_inst_output(regs->result, inst, output));
|
||||
}
|
||||
}
|
||||
for (size_t i = 0; i < regs->boundary->loops.size; i++)
|
||||
{
|
||||
const sn_blast_loop_t* entry = &sn_vec_at(sn_blast_loop_t, ®s->boundary->loops, i);
|
||||
sn_obj_id_t data = sn_boundary_co_word(regs, co_drivers, entry->co_begin, SN_BLAST_BOUNDARY_LOOP_INPUT,
|
||||
(uint32_t)i, SN_INVALID_ID, entry->width);
|
||||
sn_obj_connect(regs->result, regs->loops[i].in, 0, data);
|
||||
}
|
||||
for (size_t i = 0; i < regs->boundary->registers.size; i++)
|
||||
{
|
||||
const sn_blast_register_t* entry = &sn_vec_at(sn_blast_register_t, ®s->boundary->registers, i);
|
||||
const sn_blast_occurrence_t* occurrence =
|
||||
&sn_vec_at(sn_blast_occurrence_t, ®s->boundary->occurrences, entry->occurrence);
|
||||
const sn_module_t* module = sn_design_get_module_const(regs->design, occurrence->module);
|
||||
sn_obj_id_t old_out = entry->reg_out;
|
||||
sn_obj_pair_t pair = regs->pairs[i];
|
||||
sn_obj_id_t old_clock = sn_obj_fanin(module, old_out, SN_REG_CLOCK);
|
||||
if (old_clock != SN_INVALID_ID)
|
||||
{
|
||||
sn_blast_hier_ref_t ref = {entry->occurrence, old_clock, 0};
|
||||
sn_reg_set_fanin(regs->result, pair.out, SN_REG_CLOCK, sn_boundary_resolve_external(regs, ref));
|
||||
}
|
||||
const uint32_t slots[] = {SN_REG_ENABLE, SN_REG_SET, SN_REG_RESET, SN_REG_RESET_VALUE};
|
||||
for (size_t k = 0; k < sizeof(slots) / sizeof(slots[0]); k++)
|
||||
{
|
||||
uint32_t slot = slots[k];
|
||||
sn_obj_id_t old_fanin = sn_obj_fanin(module, old_out, slot);
|
||||
if (old_fanin == SN_INVALID_ID)
|
||||
continue;
|
||||
bool in_cloud = sn_blast_reg_control_is_comb_output(module, old_out, slot);
|
||||
sn_obj_id_t fanin;
|
||||
if (in_cloud)
|
||||
{
|
||||
assert(entry->control_co_begin[slot] != SN_INVALID_ID);
|
||||
fanin = sn_boundary_co_word(regs, co_drivers, entry->control_co_begin[slot],
|
||||
SN_BLAST_BOUNDARY_REG_CONTROL, (uint32_t)i, slot,
|
||||
sn_obj_width(module, old_fanin));
|
||||
}
|
||||
else
|
||||
{
|
||||
sn_blast_hier_ref_t ref = {entry->occurrence, old_fanin, 0};
|
||||
fanin = sn_boundary_resolve_external(regs, ref);
|
||||
}
|
||||
sn_reg_set_fanin(regs->result, pair.out, (sn_reg_fanin_t)slot, fanin);
|
||||
}
|
||||
for (uint32_t slot = SN_REG_INIT_DATA; slot <= SN_REG_INIT_MASK; slot++)
|
||||
{
|
||||
sn_obj_id_t old_fanin = sn_obj_fanin(module, old_out, slot);
|
||||
if (old_fanin != SN_INVALID_ID)
|
||||
{
|
||||
sn_blast_hier_ref_t ref = {entry->occurrence, old_fanin, 0};
|
||||
sn_reg_set_fanin(regs->result, pair.out, (sn_reg_fanin_t)slot,
|
||||
sn_boundary_resolve_external(regs, ref));
|
||||
}
|
||||
}
|
||||
sn_obj_id_t data = sn_boundary_co_word(regs, co_drivers, entry->co_begin, SN_BLAST_BOUNDARY_REG_INPUT,
|
||||
(uint32_t)i, SN_INVALID_ID, entry->width);
|
||||
sn_obj_connect(regs->result, pair.in, 0, data);
|
||||
}
|
||||
sn_boundary_prune_primitive_pairs(regs);
|
||||
free(regs->pairs);
|
||||
free(regs->loops);
|
||||
free(regs->primitive_pairs);
|
||||
free(regs->primitive_offsets);
|
||||
free(regs->links);
|
||||
for (size_t i = 0; i < regs->boundary->occurrences.size; i++)
|
||||
free(regs->external_copies[i]);
|
||||
free(regs->external_copies);
|
||||
regs->pairs = NULL;
|
||||
regs->loops = NULL;
|
||||
regs->primitive_pairs = NULL;
|
||||
regs->primitive_offsets = NULL;
|
||||
regs->external_copies = NULL;
|
||||
regs->links = NULL;
|
||||
regs->link_cap = 0;
|
||||
}
|
||||
|
||||
ABC_NAMESPACE_HEADER_END
|
||||
|
||||
#endif
|
||||
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
|
|
@ -0,0 +1,167 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [snMapAdd.h]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [New word-level design interface.]
|
||||
|
||||
Synopsis [Mapping word-level adders and subtractors into FPGA carry primitives.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: snMapAdd.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#ifndef SN_MAP_ADD_H
|
||||
#define SN_MAP_ADD_H
|
||||
|
||||
// Maps word-level addition and subtraction into preserved FPGA carry-chain
|
||||
// primitive insts. The surrounding propagate/invert logic remains ordinary SN
|
||||
// logic and can subsequently be mapped into LUTs.
|
||||
|
||||
#include "sn.h"
|
||||
#include "snTech.h"
|
||||
|
||||
ABC_NAMESPACE_HEADER_START
|
||||
|
||||
typedef struct sn_add_map_options_t
|
||||
{
|
||||
uint32_t min_width;
|
||||
bool map_add;
|
||||
bool map_sub;
|
||||
bool preserve_names;
|
||||
} sn_add_map_options_t;
|
||||
|
||||
static inline sn_add_map_options_t sn_add_map_default_options(void)
|
||||
{
|
||||
sn_add_map_options_t options = {0, true, true, true};
|
||||
return options;
|
||||
}
|
||||
|
||||
static inline bool sn_add_tech_supports(const sn_carry_tech_t* tech, const sn_add_map_options_t* options,
|
||||
sn_obj_type_t type, uint32_t width)
|
||||
{
|
||||
assert(tech && options);
|
||||
uint32_t min_width = options->min_width ? options->min_width : tech->min_op_width;
|
||||
return width >= min_width && ((type == SN_ADD && options->map_add) || (type == SN_SUB && options->map_sub));
|
||||
}
|
||||
|
||||
static inline sn_obj_id_t sn_add_slice_bit(sn_module_t* module, sn_obj_id_t value, uint32_t bit)
|
||||
{
|
||||
assert(bit < sn_obj_width(module, value));
|
||||
return sn_module_add_slice(module, value, (int32_t)bit, (int32_t)bit, NULL);
|
||||
}
|
||||
|
||||
// The behavioral body is identical to the Xilinx CARRY4 simulation model. It
|
||||
// permits standalone SN simulation and CEC while the __sn_ prefix marks the
|
||||
// module as a hard primitive that hierarchy collapse and LUT mapping preserve.
|
||||
static inline sn_module_id_t sn_add_carry_primitive_module(sn_design_t* design, const sn_carry_tech_t* tech)
|
||||
{
|
||||
assert(design && tech && tech->width == 4);
|
||||
char name[64];
|
||||
int length = snprintf(name, sizeof(name), "__sn_%s", tech->name);
|
||||
assert(length >= 0 && (size_t)length < sizeof(name));
|
||||
sn_module_id_t existing = sn_design_find_module(design, name);
|
||||
if (existing != SN_INVALID_ID)
|
||||
return existing;
|
||||
|
||||
sn_module_id_t id = sn_design_add_module(design, name);
|
||||
sn_module_t* module = sn_design_get_module(design, id);
|
||||
sn_obj_id_t ci = sn_module_add_pi(module, 1, false, "CI");
|
||||
sn_obj_id_t cyinit = sn_module_add_pi(module, 1, false, "CYINIT");
|
||||
sn_obj_id_t di = sn_module_add_pi(module, 4, false, "DI");
|
||||
sn_obj_id_t s = sn_module_add_pi(module, 4, false, "S");
|
||||
sn_obj_id_t init_fanins[2] = {ci, cyinit};
|
||||
sn_obj_id_t carry = sn_module_add_operator(module, SN_BIT_OR, 1, false, 2, init_fanins, NULL);
|
||||
sn_obj_id_t o_bits[4], co_bits[4];
|
||||
for (uint32_t bit = 0; bit < 4; bit++)
|
||||
{
|
||||
sn_obj_id_t s_bit = sn_add_slice_bit(module, s, bit);
|
||||
sn_obj_id_t di_bit = sn_add_slice_bit(module, di, bit);
|
||||
sn_obj_id_t xor_fanins[2] = {s_bit, carry};
|
||||
o_bits[bit] = sn_module_add_operator(module, SN_BIT_XOR, 1, false, 2, xor_fanins, NULL);
|
||||
co_bits[bit] = sn_module_add_mux(module, s_bit, carry, di_bit, NULL);
|
||||
carry = co_bits[bit];
|
||||
}
|
||||
sn_obj_id_t o = sn_module_add_concat(module, 4, o_bits, NULL);
|
||||
sn_obj_id_t co = sn_module_add_concat(module, 4, co_bits, NULL);
|
||||
sn_module_add_po(module, 4, false, "O", o);
|
||||
sn_module_add_po(module, 4, false, "CO", co);
|
||||
assert(sn_module_is_topo(module));
|
||||
return id;
|
||||
}
|
||||
|
||||
static inline sn_obj_id_t sn_add_resize(sn_module_t* module, sn_obj_id_t value, uint32_t width, bool is_signed)
|
||||
{
|
||||
if (sn_obj_width(module, value) == width && sn_obj_is_signed(module, value) == is_signed)
|
||||
return value;
|
||||
return sn_module_add_operator(module, SN_CAST, width, is_signed, 1, &value, NULL);
|
||||
}
|
||||
|
||||
static inline sn_obj_id_t sn_add_pad_chunk(sn_module_t* module, sn_obj_id_t value, uint32_t width)
|
||||
{
|
||||
assert(width && width <= 4 && sn_obj_width(module, value) == width);
|
||||
if (width == 4)
|
||||
return value;
|
||||
sn_obj_id_t zero = sn_module_add_named_obj(module, SN_CONST0, 4 - width, false, 0, NULL);
|
||||
sn_obj_id_t fanins[2] = {value, zero};
|
||||
return sn_module_add_concat(module, 2, fanins, NULL);
|
||||
}
|
||||
|
||||
// Implements A+B or A-B exactly as Yosys's Xilinx $alu mapping: DI=A,
|
||||
// S=A^B (or A^~B), and subtraction starts the carry chain at one.
|
||||
static inline sn_obj_id_t sn_add_map_carry_chain(sn_module_t* module, const sn_carry_tech_t* tech,
|
||||
sn_obj_type_t type, sn_obj_id_t a, sn_obj_id_t b,
|
||||
uint32_t result_width, bool result_signed, const char* name)
|
||||
{
|
||||
assert(module && tech && tech->width == 4 && (type == SN_ADD || type == SN_SUB));
|
||||
assert(a < module->obj_types.size && b < module->obj_types.size && result_width);
|
||||
bool signed_operands = sn_obj_is_signed(module, a) && sn_obj_is_signed(module, b);
|
||||
a = sn_add_resize(module, a, result_width, signed_operands);
|
||||
b = sn_add_resize(module, b, result_width, signed_operands);
|
||||
if (type == SN_SUB)
|
||||
b = sn_module_add_operator(module, SN_BIT_NOT, result_width, signed_operands, 1, &b, NULL);
|
||||
sn_obj_id_t xor_fanins[2] = {a, b};
|
||||
sn_obj_id_t propagate =
|
||||
sn_module_add_operator(module, SN_BIT_XOR, result_width, false, 2, xor_fanins, NULL);
|
||||
sn_obj_id_t zero = sn_module_add_named_obj(module, SN_CONST0, 1, false, 0, NULL);
|
||||
sn_obj_id_t one = sn_module_add_named_obj(module, SN_CONST1, 1, false, 0, NULL);
|
||||
sn_obj_id_t carry = zero;
|
||||
sn_module_id_t primitive = sn_add_carry_primitive_module(module->design, tech);
|
||||
uint32_t chunk_count = (result_width + 3) / 4;
|
||||
sn_obj_id_t* chunks = (sn_obj_id_t*)malloc(sizeof(sn_obj_id_t) * chunk_count);
|
||||
assert(chunks);
|
||||
for (uint32_t chunk = 0; chunk < chunk_count; chunk++)
|
||||
{
|
||||
uint32_t offset = chunk * 4;
|
||||
uint32_t width = result_width - offset < 4 ? result_width - offset : 4;
|
||||
sn_obj_id_t di = sn_module_add_slice(module, a, (int32_t)(offset + width - 1), (int32_t)offset, NULL);
|
||||
sn_obj_id_t s =
|
||||
sn_module_add_slice(module, propagate, (int32_t)(offset + width - 1), (int32_t)offset, NULL);
|
||||
di = sn_add_pad_chunk(module, di, width);
|
||||
s = sn_add_pad_chunk(module, s, width);
|
||||
sn_obj_id_t inputs[4] = {carry, chunk == 0 && type == SN_SUB ? one : zero, di, s};
|
||||
const char* output_names[2] = {NULL, NULL};
|
||||
sn_obj_id_t inst = sn_module_add_inst(module, primitive, 4, inputs, NULL, output_names);
|
||||
chunks[chunk] = sn_inst_output(module, inst, 0);
|
||||
sn_obj_id_t co = sn_inst_output(module, inst, 1);
|
||||
carry = sn_add_slice_bit(module, co, 3);
|
||||
}
|
||||
sn_obj_id_t result = chunk_count == 1 ? chunks[0] : sn_module_add_concat(module, chunk_count, chunks, NULL);
|
||||
free(chunks);
|
||||
if (sn_obj_width(module, result) != result_width)
|
||||
result = sn_module_add_slice(module, result, (int32_t)result_width - 1, 0, NULL);
|
||||
if (sn_obj_is_signed(module, result) != result_signed)
|
||||
result = sn_module_add_operator(module, SN_CAST, result_width, result_signed, 1, &result, name);
|
||||
return result;
|
||||
}
|
||||
|
||||
ABC_NAMESPACE_HEADER_END
|
||||
|
||||
#endif
|
||||
|
|
@ -0,0 +1,85 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [snMapDsp.h]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [New word-level design interface.]
|
||||
|
||||
Synopsis [Mapping word-level multipliers into FPGA DSP primitives.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: snMapDsp.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#ifndef SN_MAP_DSP_H
|
||||
#define SN_MAP_DSP_H
|
||||
|
||||
#include "sn.h"
|
||||
#include "snTech.h"
|
||||
|
||||
ABC_NAMESPACE_HEADER_START
|
||||
|
||||
typedef struct sn_dsp_map_options_t
|
||||
{
|
||||
bool allow_soft_fallback;
|
||||
bool use_preadder;
|
||||
bool use_postadder;
|
||||
bool preserve_names;
|
||||
bool balance_adders;
|
||||
bool prune_unused_high_products;
|
||||
uint32_t a_unsigned_chunk_width;
|
||||
uint32_t b_unsigned_chunk_width;
|
||||
uint32_t max_dsps_per_multiply;
|
||||
} sn_dsp_map_options_t;
|
||||
|
||||
static inline sn_dsp_map_options_t sn_dsp_map_default_options(void)
|
||||
{
|
||||
sn_dsp_map_options_t options = {true, false, false, true, true, true, 0, 0, 0};
|
||||
return options;
|
||||
}
|
||||
|
||||
static inline bool sn_dsp_tech_supports_mul(const sn_dsp_tech_t* tech, uint32_t a_width, uint32_t b_width,
|
||||
uint32_t result_width, bool a_signed, bool b_signed)
|
||||
{
|
||||
assert(tech);
|
||||
if (!a_width || !b_width || !result_width || a_width > tech->a_width || b_width > tech->b_width ||
|
||||
result_width > tech->p_width)
|
||||
return false;
|
||||
if (a_width < tech->min_a_width || b_width < tech->min_b_width || result_width < tech->min_p_width)
|
||||
return false;
|
||||
if (tech->signed_only && (!a_signed || !b_signed))
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
|
||||
static inline sn_module_id_t sn_map_dsp_primitive_module(sn_design_t* design, const sn_dsp_tech_t* tech,
|
||||
uint32_t a_width, uint32_t b_width, uint32_t y_width,
|
||||
bool a_signed, bool b_signed)
|
||||
{
|
||||
char name[128];
|
||||
int length = snprintf(name, sizeof(name), "__sn_%s_mul_%u_%u_%u_s%u%u", tech->name, a_width, b_width,
|
||||
y_width, a_signed ? 1u : 0u, b_signed ? 1u : 0u);
|
||||
assert(length >= 0 && (size_t)length < sizeof(name));
|
||||
sn_module_id_t existing = sn_design_find_module(design, name);
|
||||
if (existing != SN_INVALID_ID)
|
||||
return existing;
|
||||
sn_module_id_t id = sn_design_add_module(design, name);
|
||||
sn_module_t* module = sn_design_get_module(design, id);
|
||||
sn_obj_id_t a = sn_module_add_pi(module, a_width, a_signed, "A");
|
||||
sn_obj_id_t b = sn_module_add_pi(module, b_width, b_signed, "B");
|
||||
sn_obj_id_t fanins[] = {a, b};
|
||||
sn_obj_id_t product = sn_module_add_operator(module, SN_MUL, y_width, a_signed || b_signed, 2, fanins, "P");
|
||||
sn_module_add_po(module, y_width, a_signed || b_signed, "Y", product);
|
||||
return id;
|
||||
}
|
||||
|
||||
ABC_NAMESPACE_HEADER_END
|
||||
|
||||
#endif
|
||||
|
|
@ -0,0 +1,270 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [snMapLut.h]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [New word-level design interface.]
|
||||
|
||||
Synopsis [Partitioned synthesis and LUT mapping of hierarchical SN designs.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: snMapLut.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#ifndef SN_MAP_LUT_H
|
||||
#define SN_MAP_LUT_H
|
||||
|
||||
// Natural-hierarchy LUT-mapping harness. Each reachable user module is extracted as one combinational MiniAIG while
|
||||
// child instances, registers, and mapped hard blocks remain boundary terminals. A caller-supplied callback maps this
|
||||
// partition and returns a MiniLUT. The harness reconstructs the module at its stable ID, preserving parent references.
|
||||
|
||||
#include "snBlast.h"
|
||||
#include "snMiniLut.h"
|
||||
#include "snPth.h"
|
||||
|
||||
ABC_NAMESPACE_HEADER_START
|
||||
|
||||
typedef Mini_Lut_t* (*sn_map_lut_partition_fn)(void* context, sn_module_id_t module, const char* name,
|
||||
Mini_Aig_t* aig, const sn_blast_boundary_t* boundary);
|
||||
|
||||
typedef struct sn_map_lut_stats_t
|
||||
{
|
||||
uint32_t reachable_modules;
|
||||
uint32_t mapped_modules;
|
||||
uint32_t trivial_modules;
|
||||
uint32_t primitive_modules;
|
||||
uint32_t generic_memory_modules;
|
||||
uint64_t input_ands;
|
||||
uint64_t output_luts;
|
||||
sn_module_id_t failed_module;
|
||||
} sn_map_lut_stats_t;
|
||||
|
||||
typedef struct sn_map_lut_job_t
|
||||
{
|
||||
sn_module_id_t module;
|
||||
sn_name_id_t name;
|
||||
Mini_Aig_t* aig;
|
||||
Mini_Lut_t* lut;
|
||||
sn_blast_boundary_t boundary;
|
||||
} sn_map_lut_job_t;
|
||||
|
||||
typedef struct sn_map_lut_runner_t
|
||||
{
|
||||
sn_design_t* design;
|
||||
sn_map_lut_partition_fn function;
|
||||
void* context;
|
||||
} sn_map_lut_runner_t;
|
||||
|
||||
static inline void sn_map_lut_run_job(void* argument, void* job_argument)
|
||||
{
|
||||
sn_map_lut_runner_t* runner = (sn_map_lut_runner_t*)argument;
|
||||
sn_map_lut_job_t* job = (sn_map_lut_job_t*)job_argument;
|
||||
job->lut = runner->function(runner->context, job->module,
|
||||
sn_name_get(&runner->design->names, job->name), job->aig, &job->boundary);
|
||||
}
|
||||
|
||||
static inline bool sn_map_lut_boundary_has_generic_memories(const sn_blast_boundary_t* boundary)
|
||||
{
|
||||
for (size_t i = 0; i < boundary->cis.size; i++)
|
||||
if (sn_vec_at(sn_blast_boundary_bit_t, &boundary->cis, i).kind == SN_BLAST_BOUNDARY_MEMORY_OUTPUT)
|
||||
return true;
|
||||
for (size_t i = 0; i < boundary->cos.size; i++)
|
||||
if (sn_vec_at(sn_blast_boundary_bit_t, &boundary->cos, i).kind == SN_BLAST_BOUNDARY_MEMORY_INPUT)
|
||||
return true;
|
||||
return false;
|
||||
}
|
||||
|
||||
static inline void sn_design_replace_appended_module(sn_design_t* design, sn_module_id_t module,
|
||||
sn_name_id_t name, sn_module_id_t temporary)
|
||||
{
|
||||
sn_module_t* old_module;
|
||||
sn_module_t* new_module;
|
||||
bool interface_locked;
|
||||
assert(design && module < design->modules.size);
|
||||
old_module = sn_design_get_module(design, module);
|
||||
assert(old_module->name == name);
|
||||
assert(temporary + 1 == design->modules.size && temporary != module);
|
||||
new_module = sn_design_get_module(design, temporary);
|
||||
interface_locked = old_module->interface_locked;
|
||||
sn_module_destroy(old_module);
|
||||
free(old_module);
|
||||
new_module->id = module;
|
||||
new_module->name = name;
|
||||
new_module->interface_locked = interface_locked;
|
||||
sn_vec_at(sn_module_t*, &design->modules, module) = new_module;
|
||||
design->modules.size--;
|
||||
}
|
||||
|
||||
// Maps all user modules reachable from root. The callback borrows aig and boundary for the duration of the call and
|
||||
// returns a newly allocated MiniLUT owned by this harness. A NULL result aborts the pass. Modules containing generic
|
||||
// memories are skipped; map their memories into primitive instances first if their surrounding logic should be mapped.
|
||||
// The operation is in-place, so a transactional client should invoke it on a duplicate design and install that design
|
||||
// only after this API succeeds.
|
||||
static inline bool sn_design_map_lut_hierarchy(sn_design_t* design, sn_module_id_t root,
|
||||
sn_map_lut_partition_fn map_partition, void* context,
|
||||
unsigned processes, bool extract_only,
|
||||
sn_map_lut_stats_t* returned_stats)
|
||||
{
|
||||
sn_map_lut_stats_t stats = {0};
|
||||
size_t module_count;
|
||||
bool* reachable;
|
||||
sn_vec_t pending;
|
||||
sn_vec_t jobs;
|
||||
stats.failed_module = SN_INVALID_ID;
|
||||
assert(design && root < design->modules.size && map_partition && processes >= 1);
|
||||
module_count = design->modules.size;
|
||||
// Module replacement invalidates optional duplication maps that may have been cached by earlier mapping passes.
|
||||
for (sn_module_id_t module_id = 0; module_id < module_count; module_id++)
|
||||
{
|
||||
sn_module_t* module = sn_design_get_module(design, module_id);
|
||||
sn_vec_destroy(&module->copy_ids);
|
||||
sn_vec_init(&module->copy_ids);
|
||||
module->copy_module = SN_INVALID_ID;
|
||||
}
|
||||
reachable = (bool*)calloc(module_count, sizeof(bool));
|
||||
assert(reachable);
|
||||
sn_vec_init(&pending);
|
||||
sn_vec_init(&jobs);
|
||||
*sn_vec_push(sn_module_id_t, &pending) = root;
|
||||
while (pending.size)
|
||||
{
|
||||
sn_module_id_t module_id = sn_vec_at(sn_module_id_t, &pending, --pending.size);
|
||||
const sn_module_t* module;
|
||||
if (reachable[module_id])
|
||||
continue;
|
||||
reachable[module_id] = true;
|
||||
stats.reachable_modules++;
|
||||
module = sn_design_get_module_const(design, module_id);
|
||||
for (size_t i = 0; i < module->inst_modules.size; i++)
|
||||
*sn_vec_push(sn_module_id_t, &pending) = sn_vec_at(sn_module_id_t, &module->inst_modules, i);
|
||||
}
|
||||
for (sn_module_id_t module_id = 0; module_id < module_count; module_id++)
|
||||
{
|
||||
const sn_module_t* module;
|
||||
sn_name_id_t name_id;
|
||||
sn_blast_options_t options;
|
||||
sn_blast_boundary_t boundary;
|
||||
Mini_Aig_t* aig;
|
||||
if (!reachable[module_id])
|
||||
continue;
|
||||
module = sn_design_get_module_const(design, module_id);
|
||||
if (sn_module_is_technology_primitive(module))
|
||||
{
|
||||
stats.primitive_modules++;
|
||||
continue;
|
||||
}
|
||||
name_id = module->name;
|
||||
options = sn_blast_default_options();
|
||||
options.mode = SN_BLAST_COMB;
|
||||
options.abstract_instances = true;
|
||||
sn_blast_boundary_init(&boundary);
|
||||
aig = sn_design_blast_hier_boundary_options(design, module_id, options, NULL, &boundary);
|
||||
if (sn_map_lut_boundary_has_generic_memories(&boundary))
|
||||
{
|
||||
stats.generic_memory_modules++;
|
||||
Mini_AigStop(aig);
|
||||
sn_blast_boundary_destroy(&boundary);
|
||||
continue;
|
||||
}
|
||||
if (Mini_AigAndNum(aig) == 0)
|
||||
{
|
||||
stats.trivial_modules++;
|
||||
Mini_AigStop(aig);
|
||||
sn_blast_boundary_destroy(&boundary);
|
||||
continue;
|
||||
}
|
||||
stats.input_ands += (uint64_t)Mini_AigAndNum(aig);
|
||||
if (processes == 1)
|
||||
{
|
||||
Mini_Lut_t* lut = map_partition(context, module_id, sn_name_get(&design->names, name_id), aig, &boundary);
|
||||
Mini_AigStop(aig);
|
||||
if (!lut)
|
||||
{
|
||||
stats.failed_module = module_id;
|
||||
sn_blast_boundary_destroy(&boundary);
|
||||
sn_vec_destroy(&pending);
|
||||
sn_vec_destroy(&jobs);
|
||||
free(reachable);
|
||||
if (returned_stats)
|
||||
*returned_stats = stats;
|
||||
return false;
|
||||
}
|
||||
if (extract_only)
|
||||
{
|
||||
Mini_LutStop(lut);
|
||||
sn_blast_boundary_destroy(&boundary);
|
||||
stats.mapped_modules++;
|
||||
continue;
|
||||
}
|
||||
sn_lut_stats_t lut_stats = sn_lut_analyze(lut, &boundary);
|
||||
sn_module_id_t temporary = sn_design_add_lut_module(design, module_id, lut, &boundary,
|
||||
"__sn_lut_partition");
|
||||
Mini_LutStop(lut);
|
||||
sn_blast_boundary_destroy(&boundary);
|
||||
sn_design_replace_appended_module(design, module_id, name_id, temporary);
|
||||
stats.mapped_modules++;
|
||||
stats.output_luts += lut_stats.lut_count;
|
||||
continue;
|
||||
}
|
||||
sn_map_lut_job_t* job = sn_vec_push(sn_map_lut_job_t, &jobs);
|
||||
job->module = module_id;
|
||||
job->name = name_id;
|
||||
job->aig = aig;
|
||||
job->lut = NULL;
|
||||
job->boundary = boundary;
|
||||
}
|
||||
void** job_pointers = jobs.size ? (void**)malloc(sizeof(void*) * jobs.size) : NULL;
|
||||
assert(job_pointers || jobs.size == 0);
|
||||
for (size_t i = 0; i < jobs.size; i++)
|
||||
job_pointers[i] = &sn_vec_at(sn_map_lut_job_t, &jobs, i);
|
||||
sn_map_lut_runner_t runner = {design, map_partition, context};
|
||||
sn_pth_process(job_pointers, jobs.size, processes, sn_map_lut_run_job, &runner);
|
||||
free(job_pointers);
|
||||
bool success = true;
|
||||
for (size_t i = 0; i < jobs.size; i++)
|
||||
if (!sn_vec_at(sn_map_lut_job_t, &jobs, i).lut)
|
||||
{
|
||||
stats.failed_module = sn_vec_at(sn_map_lut_job_t, &jobs, i).module;
|
||||
success = false;
|
||||
break;
|
||||
}
|
||||
if (success && !extract_only)
|
||||
for (size_t i = 0; i < jobs.size; i++)
|
||||
{
|
||||
sn_map_lut_job_t* job = &sn_vec_at(sn_map_lut_job_t, &jobs, i);
|
||||
sn_lut_stats_t lut_stats = sn_lut_analyze(job->lut, &job->boundary);
|
||||
sn_module_id_t temporary = sn_design_add_lut_module(design, job->module, job->lut, &job->boundary,
|
||||
"__sn_lut_partition");
|
||||
sn_design_replace_appended_module(design, job->module, job->name, temporary);
|
||||
stats.mapped_modules++;
|
||||
stats.output_luts += lut_stats.lut_count;
|
||||
}
|
||||
else if (success)
|
||||
stats.mapped_modules += (uint32_t)jobs.size;
|
||||
for (size_t i = 0; i < jobs.size; i++)
|
||||
{
|
||||
sn_map_lut_job_t* job = &sn_vec_at(sn_map_lut_job_t, &jobs, i);
|
||||
Mini_AigStop(job->aig);
|
||||
if (job->lut)
|
||||
Mini_LutStop(job->lut);
|
||||
sn_blast_boundary_destroy(&job->boundary);
|
||||
}
|
||||
sn_vec_destroy(&pending);
|
||||
sn_vec_destroy(&jobs);
|
||||
free(reachable);
|
||||
assert(!success || sn_design_is_topo(design));
|
||||
if (returned_stats)
|
||||
*returned_stats = stats;
|
||||
return success;
|
||||
}
|
||||
|
||||
ABC_NAMESPACE_HEADER_END
|
||||
|
||||
#endif
|
||||
|
|
@ -0,0 +1,101 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [snMapMem.h]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [New word-level design interface.]
|
||||
|
||||
Synopsis [Mapping technology-independent memories into FPGA memory primitives.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: snMapMem.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#ifndef SN_MAP_MEM_H
|
||||
#define SN_MAP_MEM_H
|
||||
|
||||
#include "sn.h"
|
||||
#include "snTech.h"
|
||||
|
||||
ABC_NAMESPACE_HEADER_START
|
||||
|
||||
typedef enum sn_mem_split_order_t
|
||||
{
|
||||
SN_MEM_SPLIT_AUTO = 0,
|
||||
SN_MEM_SPLIT_WIDTH_FIRST,
|
||||
SN_MEM_SPLIT_DEPTH_FIRST
|
||||
} sn_mem_split_order_t;
|
||||
|
||||
typedef struct sn_mem_map_options_t
|
||||
{
|
||||
bool allow_lutram_fallback;
|
||||
bool allow_register_fallback;
|
||||
bool preserve_names;
|
||||
uint32_t min_memory_bits;
|
||||
uint32_t max_primitives_per_memory;
|
||||
sn_mem_split_order_t split_order;
|
||||
} sn_mem_map_options_t;
|
||||
|
||||
static inline sn_mem_map_options_t sn_mem_map_default_options(void)
|
||||
{
|
||||
sn_mem_map_options_t options = {false, false, true, 0, 0, SN_MEM_SPLIT_AUTO};
|
||||
return options;
|
||||
}
|
||||
|
||||
// Returns true when a memory's dimensions and port protocol can be represented
|
||||
// by one technology primitive. This conservative predicate is used before the
|
||||
// rewriting pass; splitting, packing, and primitive-inst construction are
|
||||
// the next mapper milestone.
|
||||
static inline bool sn_mem_tech_supports(const sn_mem_tech_t* tech, uint32_t width, uint32_t depth,
|
||||
sn_mem_port_mode_t port_mode)
|
||||
{
|
||||
assert(tech);
|
||||
if (port_mode != tech->port_mode || !width || !depth || width > UINT32_MAX / depth)
|
||||
return false;
|
||||
if (width * depth > tech->cap_bits)
|
||||
return false;
|
||||
if (depth > (1u << tech->address_bits))
|
||||
return false;
|
||||
for (size_t i = 0; i < tech->width_count; i++)
|
||||
if (tech->widths[i] == width)
|
||||
return true;
|
||||
return false;
|
||||
}
|
||||
|
||||
// Creates a behavioral wrapper for one technology memory shape. Keeping the
|
||||
// wrapper as an SN module makes the mapped result simulatable; a later Verilog
|
||||
// technology writer can replace this module by RAMB/URAM cells.
|
||||
static inline sn_module_id_t sn_map_mem_primitive_module(sn_design_t* design, const sn_mem_tech_t* tech,
|
||||
uint32_t width, uint32_t depth)
|
||||
{
|
||||
char name[128];
|
||||
int length = snprintf(name, sizeof(name), "__sn_%s_mem_%u_%u", tech->name, width, depth);
|
||||
assert(length >= 0 && (size_t)length < sizeof(name));
|
||||
sn_module_id_t existing = sn_design_find_module(design, name);
|
||||
if (existing != SN_INVALID_ID)
|
||||
return existing;
|
||||
sn_module_id_t id = sn_design_add_module(design, name);
|
||||
sn_module_t* module = sn_design_get_module(design, id);
|
||||
sn_obj_id_t clock = sn_module_add_pi(module, 1, false, "clock");
|
||||
sn_obj_id_t enable = sn_module_add_pi(module, 1, false, "enable");
|
||||
sn_obj_id_t write_address = sn_module_add_pi(module, 32, false, "write_address");
|
||||
sn_obj_id_t data = sn_module_add_pi(module, width, false, "write_data");
|
||||
sn_obj_id_t read_address = sn_module_add_pi(module, 32, false, "read_address");
|
||||
sn_obj_pair_t pair = sn_module_add_mem_pair(module, width, false, depth, "mem_out", "mem_in");
|
||||
sn_module_add_mem_write(module, pair.in, clock, enable, data, write_address, "write");
|
||||
sn_obj_id_t read = sn_module_add_mem_read(module, pair.out, SN_INVALID_ID, SN_INVALID_ID, read_address, "read");
|
||||
sn_module_add_po(module, width, false, "read_data", read);
|
||||
sn_design_reorder_module_topo(design, id);
|
||||
return id;
|
||||
}
|
||||
|
||||
ABC_NAMESPACE_HEADER_END
|
||||
|
||||
#endif
|
||||
File diff suppressed because it is too large
Load Diff
|
|
@ -0,0 +1,143 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [snMiniAig.h]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [New word-level design interface.]
|
||||
|
||||
Synopsis [Reconstruction of SN logic from an unmapped MiniAIG network.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: snMiniAig.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#ifndef ABC__base__sn__snMiniAig_h
|
||||
#define ABC__base__sn__snMiniAig_h
|
||||
|
||||
#include "snMiniLut.h"
|
||||
|
||||
ABC_NAMESPACE_HEADER_START
|
||||
|
||||
static inline sn_obj_id_t sn_aig_lit_object(sn_module_t* module, Mini_Aig_t* aig, const sn_obj_id_t* objects, int lit)
|
||||
{
|
||||
int variable = Mini_AigLit2Var(lit);
|
||||
assert(variable >= 0 && variable < Mini_AigNodeNum(aig));
|
||||
sn_obj_id_t object = objects[variable];
|
||||
assert(object != SN_INVALID_ID);
|
||||
if (!Mini_AigLitIsCompl(lit))
|
||||
return object;
|
||||
if (variable == 0)
|
||||
{
|
||||
uint32_t one = 1;
|
||||
return sn_module_add_const(module, 1, false, &one, "aig_const1");
|
||||
}
|
||||
return sn_module_add_operator(module, SN_BIT_NOT, 1, false, 1, &object, "aig_inv");
|
||||
}
|
||||
|
||||
// Reconstructs an unmapped combinational MiniAIG as explicit one-bit SN_BIT_AND and SN_BIT_NOT objects. The MiniAIG
|
||||
// CI/CO order is matched positionally against the boundary recorded by @blast. Register endpoints are reconnected by
|
||||
// the shared boundary reconstruction stage; RAM/DSP endpoints are rejected by the command until they are supported.
|
||||
static inline sn_module_id_t sn_design_add_aig_module(sn_design_t* design, sn_module_id_t source_top_id,
|
||||
Mini_Aig_t* aig, const sn_blast_boundary_t* boundary,
|
||||
const char* module_name)
|
||||
{
|
||||
assert(design && source_top_id < design->modules.size && aig && boundary && module_name);
|
||||
assert(Mini_AigRegNum(aig) == 0);
|
||||
assert((size_t)Mini_AigPiNum(aig) == boundary->cis.size);
|
||||
assert((size_t)Mini_AigPoNum(aig) == boundary->cos.size);
|
||||
|
||||
const sn_module_t* source = sn_design_get_module_const(design, source_top_id);
|
||||
sn_module_id_t result_id = sn_design_add_module(design, module_name);
|
||||
sn_module_t* result = sn_design_get_module(design, result_id);
|
||||
sn_obj_id_t* top_inputs = (sn_obj_id_t*)malloc(sizeof(sn_obj_id_t) * source->obj_types.size);
|
||||
sn_obj_id_t* objects = (sn_obj_id_t*)malloc(sizeof(sn_obj_id_t) * Mini_AigNodeNum(aig));
|
||||
sn_obj_id_t* drivers = (sn_obj_id_t*)malloc(sizeof(sn_obj_id_t) * boundary->cos.size);
|
||||
sn_boundary_regs_t regs;
|
||||
assert(top_inputs && objects && drivers);
|
||||
for (size_t i = 0; i < source->obj_types.size; i++)
|
||||
top_inputs[i] = SN_INVALID_ID;
|
||||
for (int i = 0; i < Mini_AigNodeNum(aig); i++)
|
||||
objects[i] = SN_INVALID_ID;
|
||||
|
||||
for (size_t i = 0; i < source->type_objects[SN_PI].size; i++)
|
||||
{
|
||||
sn_obj_id_t old_pi = sn_vec_at(sn_obj_id_t, &source->type_objects[SN_PI], i);
|
||||
top_inputs[old_pi] = sn_module_add_pi(result, sn_obj_width(source, old_pi), sn_obj_is_signed(source, old_pi),
|
||||
sn_obj_name(source, old_pi));
|
||||
}
|
||||
sn_boundary_regs_init(®s, design, boundary, result, top_inputs);
|
||||
uint32_t zero = 0;
|
||||
objects[0] = sn_module_add_const(result, 1, false, &zero, "aig_const0");
|
||||
|
||||
uint32_t ci_index = 0;
|
||||
int mini_object;
|
||||
Mini_AigForEachPi(aig, mini_object)
|
||||
{
|
||||
sn_blast_boundary_bit_t bit = sn_vec_at(sn_blast_boundary_bit_t, &boundary->cis, ci_index++);
|
||||
if (bit.kind == SN_BLAST_BOUNDARY_TOP_PI)
|
||||
{
|
||||
assert(bit.signal.occurrence == 0 && top_inputs[bit.signal.object] != SN_INVALID_ID);
|
||||
objects[mini_object] = sn_module_add_slice(result, top_inputs[bit.signal.object], (int32_t)bit.signal.bit,
|
||||
(int32_t)bit.signal.bit, "aig_pi_bit");
|
||||
}
|
||||
else if (bit.kind == SN_BLAST_BOUNDARY_REG_OUTPUT)
|
||||
objects[mini_object] = sn_boundary_reg_output_bit(®s, bit.owner, bit.signal.bit);
|
||||
else if (bit.kind == SN_BLAST_BOUNDARY_LOOP_OUTPUT)
|
||||
objects[mini_object] = sn_boundary_loop_output_bit(®s, bit.owner, bit.signal.bit);
|
||||
else if (bit.kind == SN_BLAST_BOUNDARY_PRIMITIVE_OUTPUT)
|
||||
objects[mini_object] = sn_boundary_primitive_output_bit(®s, bit.owner, bit.port, bit.signal.bit);
|
||||
else
|
||||
assert(false);
|
||||
}
|
||||
assert(ci_index == boundary->cis.size);
|
||||
|
||||
Mini_AigForEachAnd(aig, mini_object)
|
||||
{
|
||||
sn_obj_id_t fanins[2] = {
|
||||
sn_aig_lit_object(result, aig, objects, Mini_AigNodeFanin0(aig, mini_object)),
|
||||
sn_aig_lit_object(result, aig, objects, Mini_AigNodeFanin1(aig, mini_object))};
|
||||
objects[mini_object] = sn_module_add_operator(result, SN_BIT_AND, 1, false, 2, fanins, "aig_and");
|
||||
}
|
||||
|
||||
uint32_t co_index = 0;
|
||||
Mini_AigForEachPo(aig, mini_object)
|
||||
drivers[co_index++] = sn_aig_lit_object(result, aig, objects, Mini_AigNodeFanin0(aig, mini_object));
|
||||
assert(co_index <= boundary->cos.size);
|
||||
|
||||
co_index = 0;
|
||||
for (size_t i = 0; i < source->type_objects[SN_PO].size; i++)
|
||||
{
|
||||
sn_obj_id_t old_po = sn_vec_at(sn_obj_id_t, &source->type_objects[SN_PO], i);
|
||||
uint32_t width = sn_obj_width(source, old_po);
|
||||
for (uint32_t bit = 0; bit < width; bit++)
|
||||
{
|
||||
sn_blast_boundary_bit_t endpoint = sn_vec_at(sn_blast_boundary_bit_t, &boundary->cos, co_index + bit);
|
||||
assert(endpoint.kind == SN_BLAST_BOUNDARY_TOP_PO && endpoint.port == i && endpoint.signal.bit == bit);
|
||||
}
|
||||
sn_obj_id_t driver = sn_lut_pack_bits(result, drivers + co_index, width, "aig_po_word");
|
||||
sn_module_add_po(result, width, sn_obj_is_signed(source, old_po), sn_obj_name(source, old_po), driver);
|
||||
co_index += width;
|
||||
}
|
||||
assert(co_index <= boundary->cos.size);
|
||||
sn_boundary_regs_finish(®s, drivers);
|
||||
result = sn_design_get_module(design, result_id);
|
||||
|
||||
free(drivers);
|
||||
free(objects);
|
||||
free(top_inputs);
|
||||
if (!sn_module_is_topo(result))
|
||||
sn_design_reorder_module_topo(design, result_id);
|
||||
assert(sn_module_is_topo(sn_design_get_module_const(design, result_id)));
|
||||
return result_id;
|
||||
}
|
||||
|
||||
ABC_NAMESPACE_HEADER_END
|
||||
|
||||
#endif
|
||||
|
|
@ -0,0 +1,215 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [snMiniGate.h]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [New word-level design interface.]
|
||||
|
||||
Synopsis [Reconstruction of technology-mapped SN gates from mini-mapping data.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: snMiniGate.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#ifndef ABC__base__sn__snMiniGate_h
|
||||
#define ABC__base__sn__snMiniGate_h
|
||||
|
||||
#include "snMiniLut.h"
|
||||
|
||||
ABC_NAMESPACE_HEADER_START
|
||||
|
||||
typedef uint32_t (*sn_gate_id_resolver_t)(void* context, const char* gate_name);
|
||||
|
||||
// Reconstructs ABC's mini-mapping array as one-bit SN_GATE objects. Mini-mapping numbers CIs first and mapped nodes
|
||||
// afterward in topological order. Gate names stored at the end of the array are resolved into the current library's
|
||||
// stable gate IDs; the name is also retained as the SN object name for structural Verilog emission.
|
||||
static inline sn_module_id_t sn_design_add_gate_module(sn_design_t* design, sn_module_id_t source_top_id,
|
||||
const int* mapping, size_t mapping_count,
|
||||
const sn_blast_boundary_t* boundary,
|
||||
sn_gate_id_resolver_t resolver, void* resolver_context,
|
||||
const char* module_name)
|
||||
{
|
||||
assert(design && source_top_id < design->modules.size && mapping && boundary && resolver && module_name);
|
||||
if (mapping_count < 4 || mapping[0] < 0 || mapping[1] < 0 || mapping[2] < 0 || mapping[3] < 0)
|
||||
return SN_INVALID_ID;
|
||||
uint32_t ci_count = (uint32_t)mapping[0];
|
||||
uint32_t co_count = (uint32_t)mapping[1];
|
||||
uint32_t node_count = (uint32_t)mapping[2];
|
||||
uint32_t reg_count = (uint32_t)mapping[3];
|
||||
if (reg_count != 0 || ci_count != boundary->cis.size || co_count != boundary->cos.size ||
|
||||
node_count > UINT32_MAX - ci_count)
|
||||
return SN_INVALID_ID;
|
||||
|
||||
// Validate the complete structural prefix and resolve all bounded gate-name strings before mutating the design.
|
||||
// A changed genlib or malformed mini-mapping can otherwise leave a partially constructed module behind.
|
||||
size_t position = 4;
|
||||
uint32_t* fanin_counts = node_count ? (uint32_t*)malloc(sizeof(uint32_t) * node_count) : NULL;
|
||||
const uint32_t** fanin_indices =
|
||||
node_count ? (const uint32_t**)malloc(sizeof(uint32_t*) * node_count) : NULL;
|
||||
uint32_t* gate_ids = node_count ? (uint32_t*)malloc(sizeof(uint32_t) * node_count) : NULL;
|
||||
bool valid = true;
|
||||
assert((fanin_counts && fanin_indices && gate_ids) || node_count == 0);
|
||||
for (uint32_t i = 0; valid && i < node_count; i++)
|
||||
{
|
||||
if (position >= mapping_count || mapping[position] < 0)
|
||||
{
|
||||
valid = false;
|
||||
break;
|
||||
}
|
||||
uint32_t count = (uint32_t)mapping[position++];
|
||||
if (count > mapping_count - position)
|
||||
{
|
||||
valid = false;
|
||||
break;
|
||||
}
|
||||
fanin_counts[i] = count;
|
||||
fanin_indices[i] = (const uint32_t*)(mapping + position);
|
||||
for (uint32_t k = 0; k < count; k++)
|
||||
if (mapping[position + k] < 0 || (uint32_t)mapping[position + k] >= ci_count + i)
|
||||
valid = false;
|
||||
position += count;
|
||||
}
|
||||
if (valid && co_count > mapping_count - position)
|
||||
valid = false;
|
||||
const uint32_t* output_indices = valid ? (const uint32_t*)(mapping + position) : NULL;
|
||||
for (uint32_t i = 0; valid && i < co_count; i++)
|
||||
if (mapping[position + i] < 0 || (uint32_t)mapping[position + i] >= ci_count + node_count)
|
||||
valid = false;
|
||||
if (valid)
|
||||
position += co_count;
|
||||
const char* gate_names = valid ? (const char*)(mapping + position) : NULL;
|
||||
const char* gate_name = gate_names;
|
||||
size_t name_bytes = valid ? (mapping_count - position) * sizeof(int) : 0;
|
||||
for (uint32_t i = 0; valid && i < node_count; i++)
|
||||
{
|
||||
const char* end = (const char*)memchr(gate_name, '\0', name_bytes);
|
||||
if (!end || end == gate_name)
|
||||
{
|
||||
valid = false;
|
||||
break;
|
||||
}
|
||||
gate_ids[i] = resolver(resolver_context, gate_name);
|
||||
if (gate_ids[i] == SN_INVALID_ID)
|
||||
{
|
||||
valid = false;
|
||||
break;
|
||||
}
|
||||
size_t length = (size_t)(end - gate_name) + 1;
|
||||
gate_name += length;
|
||||
name_bytes -= length;
|
||||
}
|
||||
if (!valid)
|
||||
{
|
||||
free(gate_ids);
|
||||
free(fanin_indices);
|
||||
free(fanin_counts);
|
||||
return SN_INVALID_ID;
|
||||
}
|
||||
|
||||
const sn_module_t* source = sn_design_get_module_const(design, source_top_id);
|
||||
sn_module_id_t result_id = sn_design_add_module(design, module_name);
|
||||
sn_module_t* result = sn_design_get_module(design, result_id);
|
||||
sn_obj_id_t* top_inputs = (sn_obj_id_t*)malloc(sizeof(sn_obj_id_t) * source->obj_types.size);
|
||||
sn_obj_id_t* objects = (sn_obj_id_t*)malloc(sizeof(sn_obj_id_t) * (ci_count + node_count));
|
||||
sn_boundary_regs_t regs;
|
||||
assert(top_inputs && objects);
|
||||
for (size_t i = 0; i < source->obj_types.size; i++)
|
||||
top_inputs[i] = SN_INVALID_ID;
|
||||
for (uint32_t i = 0; i < ci_count + node_count; i++)
|
||||
objects[i] = SN_INVALID_ID;
|
||||
|
||||
for (size_t i = 0; i < source->type_objects[SN_PI].size; i++)
|
||||
{
|
||||
sn_obj_id_t old_pi = sn_vec_at(sn_obj_id_t, &source->type_objects[SN_PI], i);
|
||||
top_inputs[old_pi] = sn_module_add_pi(result, sn_obj_width(source, old_pi), sn_obj_is_signed(source, old_pi),
|
||||
sn_obj_name(source, old_pi));
|
||||
}
|
||||
sn_boundary_regs_init(®s, design, boundary, result, top_inputs);
|
||||
for (uint32_t i = 0; i < ci_count; i++)
|
||||
{
|
||||
sn_blast_boundary_bit_t bit = sn_vec_at(sn_blast_boundary_bit_t, &boundary->cis, i);
|
||||
if (bit.kind == SN_BLAST_BOUNDARY_TOP_PI)
|
||||
{
|
||||
assert(bit.signal.occurrence == 0 && top_inputs[bit.signal.object] != SN_INVALID_ID);
|
||||
objects[i] = sn_module_add_slice(result, top_inputs[bit.signal.object], (int32_t)bit.signal.bit,
|
||||
(int32_t)bit.signal.bit, "gate_pi_bit");
|
||||
}
|
||||
else if (bit.kind == SN_BLAST_BOUNDARY_REG_OUTPUT)
|
||||
objects[i] = sn_boundary_reg_output_bit(®s, bit.owner, bit.signal.bit);
|
||||
else if (bit.kind == SN_BLAST_BOUNDARY_LOOP_OUTPUT)
|
||||
objects[i] = sn_boundary_loop_output_bit(®s, bit.owner, bit.signal.bit);
|
||||
else if (bit.kind == SN_BLAST_BOUNDARY_PRIMITIVE_OUTPUT)
|
||||
objects[i] = sn_boundary_primitive_output_bit(®s, bit.owner, bit.port, bit.signal.bit);
|
||||
else
|
||||
assert(false);
|
||||
}
|
||||
|
||||
gate_name = gate_names;
|
||||
|
||||
for (uint32_t i = 0; i < node_count; i++)
|
||||
{
|
||||
uint32_t count = fanin_counts[i];
|
||||
sn_obj_id_t* fanins = count ? (sn_obj_id_t*)malloc(sizeof(sn_obj_id_t) * count) : NULL;
|
||||
assert(fanins || count == 0);
|
||||
for (uint32_t k = 0; k < count; k++)
|
||||
{
|
||||
uint32_t fanin = fanin_indices[i][k];
|
||||
assert(fanin < ci_count + i && objects[fanin] != SN_INVALID_ID);
|
||||
fanins[k] = objects[fanin];
|
||||
}
|
||||
objects[ci_count + i] = sn_module_add_gate(result, count, fanins, gate_ids[i], gate_name);
|
||||
free(fanins);
|
||||
gate_name += strlen(gate_name) + 1;
|
||||
}
|
||||
|
||||
uint32_t co_index = 0;
|
||||
for (size_t i = 0; i < source->type_objects[SN_PO].size; i++)
|
||||
{
|
||||
sn_obj_id_t old_po = sn_vec_at(sn_obj_id_t, &source->type_objects[SN_PO], i);
|
||||
uint32_t width = sn_obj_width(source, old_po);
|
||||
sn_obj_id_t* bits = (sn_obj_id_t*)malloc(sizeof(sn_obj_id_t) * width);
|
||||
assert(bits);
|
||||
for (uint32_t bit = 0; bit < width; bit++)
|
||||
{
|
||||
sn_blast_boundary_bit_t endpoint = sn_vec_at(sn_blast_boundary_bit_t, &boundary->cos, co_index);
|
||||
assert(endpoint.kind == SN_BLAST_BOUNDARY_TOP_PO && endpoint.port == i && endpoint.signal.bit == bit);
|
||||
assert(output_indices[co_index] < ci_count + node_count);
|
||||
bits[bit] = objects[output_indices[co_index++]];
|
||||
}
|
||||
sn_obj_id_t driver = sn_lut_pack_bits(result, bits, width, "gate_po_word");
|
||||
sn_module_add_po(result, width, sn_obj_is_signed(source, old_po), sn_obj_name(source, old_po), driver);
|
||||
free(bits);
|
||||
}
|
||||
assert(co_index <= co_count);
|
||||
sn_obj_id_t* co_drivers = (sn_obj_id_t*)malloc(sizeof(sn_obj_id_t) * co_count);
|
||||
assert(co_drivers || co_count == 0);
|
||||
for (uint32_t i = 0; i < co_count; i++)
|
||||
{
|
||||
assert(output_indices[i] < ci_count + node_count);
|
||||
co_drivers[i] = objects[output_indices[i]];
|
||||
}
|
||||
sn_boundary_regs_finish(®s, co_drivers);
|
||||
result = sn_design_get_module(design, result_id);
|
||||
|
||||
free(co_drivers);
|
||||
free(fanin_indices);
|
||||
free(fanin_counts);
|
||||
free(gate_ids);
|
||||
free(objects);
|
||||
free(top_inputs);
|
||||
if (!sn_module_is_topo(result))
|
||||
sn_design_reorder_module_topo(design, result_id);
|
||||
assert(sn_module_is_topo(sn_design_get_module_const(design, result_id)));
|
||||
return result_id;
|
||||
}
|
||||
|
||||
ABC_NAMESPACE_HEADER_END
|
||||
|
||||
#endif
|
||||
|
|
@ -0,0 +1,407 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [snMiniLut.h]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [New word-level design interface.]
|
||||
|
||||
Synopsis [Analysis and reconstruction of SN LUTs from MiniLUT networks.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: snMiniLut.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#ifndef SN_MINI_LUT_H
|
||||
#define SN_MINI_LUT_H
|
||||
|
||||
// Utilities for validating and analyzing the MiniLUT files written by ABC's
|
||||
// "&write -l" command.
|
||||
|
||||
#include "snBoundary.h"
|
||||
#include "aig/miniaig/minilut.h"
|
||||
|
||||
#include <assert.h>
|
||||
#include <stdint.h>
|
||||
#include <stdlib.h>
|
||||
|
||||
ABC_NAMESPACE_HEADER_START
|
||||
|
||||
typedef struct sn_lut_stats_t
|
||||
{
|
||||
uint32_t pi_count;
|
||||
uint32_t po_count;
|
||||
uint32_t register_count;
|
||||
uint32_t lut_count;
|
||||
uint32_t lut_size;
|
||||
uint32_t lut_levels;
|
||||
uint32_t top_output_levels;
|
||||
uint32_t register_control_levels;
|
||||
uint32_t memory_input_levels;
|
||||
uint32_t primitive_input_levels;
|
||||
uint32_t loop_input_levels;
|
||||
uint32_t register_input_levels;
|
||||
} sn_lut_stats_t;
|
||||
|
||||
static inline uint32_t sn_lut_max_u32(uint32_t a, uint32_t b)
|
||||
{
|
||||
return a > b ? a : b;
|
||||
}
|
||||
|
||||
static inline Mini_Lut_t* sn_lut_load(const char* file_name)
|
||||
{
|
||||
if (!file_name)
|
||||
return NULL;
|
||||
FILE* file = fopen(file_name, "rb");
|
||||
if (!file)
|
||||
return NULL;
|
||||
int32_t node_count = 0, register_count = 0, lut_size = 0;
|
||||
bool valid = fread(&node_count, sizeof(node_count), 1, file) == 1 &&
|
||||
fread(®ister_count, sizeof(register_count), 1, file) == 1 &&
|
||||
fread(&lut_size, sizeof(lut_size), 1, file) == 1;
|
||||
uint64_t array_count = 0, truth_count = 0;
|
||||
if (valid && node_count >= 2 && register_count >= 0 && register_count <= node_count && lut_size >= 2 &&
|
||||
lut_size <= 16)
|
||||
{
|
||||
array_count = (uint64_t)(uint32_t)node_count * (uint32_t)lut_size;
|
||||
truth_count = (uint64_t)(uint32_t)node_count * (uint32_t)Mini_LutWordNum(lut_size);
|
||||
valid = array_count <= SIZE_MAX / sizeof(int) && truth_count <= SIZE_MAX / sizeof(unsigned);
|
||||
}
|
||||
else
|
||||
valid = false;
|
||||
if (valid)
|
||||
{
|
||||
uint64_t payload_bytes = (array_count + truth_count) * sizeof(uint32_t);
|
||||
#if defined(_WIN32)
|
||||
__int64 position = _ftelli64(file);
|
||||
valid = position >= 0 && _fseeki64(file, 0, SEEK_END) == 0;
|
||||
__int64 end = valid ? _ftelli64(file) : -1;
|
||||
valid = end >= position && (uint64_t)(end - position) == payload_bytes &&
|
||||
_fseeki64(file, position, SEEK_SET) == 0;
|
||||
#else
|
||||
long position = ftell(file);
|
||||
valid = position >= 0 && fseek(file, 0, SEEK_END) == 0;
|
||||
long end = valid ? ftell(file) : -1;
|
||||
valid = end >= position && (uint64_t)(end - position) == payload_bytes && fseek(file, position, SEEK_SET) == 0;
|
||||
#endif
|
||||
}
|
||||
Mini_Lut_t* lut = valid ? (Mini_Lut_t*)calloc(1, sizeof(Mini_Lut_t)) : NULL;
|
||||
if (lut)
|
||||
{
|
||||
lut->nSize = lut->nCap = node_count;
|
||||
lut->nRegs = register_count;
|
||||
lut->LutSize = lut_size;
|
||||
lut->pArray = (int*)malloc((size_t)array_count * sizeof(int));
|
||||
lut->pTruths = (unsigned*)malloc((size_t)truth_count * sizeof(unsigned));
|
||||
if (!lut->pArray || !lut->pTruths)
|
||||
valid = false;
|
||||
else
|
||||
valid = fread(lut->pArray, sizeof(int), (size_t)array_count, file) == array_count &&
|
||||
fread(lut->pTruths, sizeof(unsigned), (size_t)truth_count, file) == truth_count &&
|
||||
fgetc(file) == EOF && !ferror(file);
|
||||
}
|
||||
if (fclose(file) != 0)
|
||||
valid = false;
|
||||
if (!valid || !lut)
|
||||
{
|
||||
if (lut)
|
||||
Mini_LutStop(lut);
|
||||
return NULL;
|
||||
}
|
||||
for (int object = 2; object < node_count; object++)
|
||||
{
|
||||
int* fanins = lut->pArray + (size_t)object * lut_size;
|
||||
if (fanins[0] == MINI_LUT_NULL)
|
||||
{
|
||||
for (int i = 1; i < lut_size; i++)
|
||||
valid &= fanins[i] == MINI_LUT_NULL;
|
||||
continue;
|
||||
}
|
||||
if (fanins[0] < 0 || fanins[0] >= object)
|
||||
valid = false;
|
||||
else if (fanins[0] >= 2)
|
||||
{
|
||||
int* source = lut->pArray + (size_t)fanins[0] * lut_size;
|
||||
if (source[0] != MINI_LUT_NULL && source[1] == MINI_LUT_NULL2)
|
||||
valid = false;
|
||||
}
|
||||
if (fanins[1] == MINI_LUT_NULL2)
|
||||
{
|
||||
for (int i = 2; i < lut_size; i++)
|
||||
valid &= fanins[i] == MINI_LUT_NULL;
|
||||
continue;
|
||||
}
|
||||
bool padding = false;
|
||||
for (int i = 0; i < lut_size; i++)
|
||||
if (fanins[i] == MINI_LUT_NULL)
|
||||
padding = true;
|
||||
else if (padding || fanins[i] < 0 || fanins[i] >= object || fanins[i] == MINI_LUT_NULL2)
|
||||
valid = false;
|
||||
else if (fanins[i] >= 2)
|
||||
{
|
||||
int* source = lut->pArray + (size_t)fanins[i] * lut_size;
|
||||
if (source[0] != MINI_LUT_NULL && source[1] == MINI_LUT_NULL2)
|
||||
valid = false;
|
||||
}
|
||||
}
|
||||
if (!valid)
|
||||
{
|
||||
Mini_LutStop(lut);
|
||||
return NULL;
|
||||
}
|
||||
return lut;
|
||||
}
|
||||
|
||||
static inline bool sn_lut_interface_matches(Mini_Lut_t* lut, const sn_blast_boundary_t* boundary)
|
||||
{
|
||||
if (!lut || !boundary)
|
||||
return false;
|
||||
uint32_t pi_count = 0, po_count = 0;
|
||||
int object;
|
||||
Mini_LutForEachPi(lut, object)
|
||||
pi_count++;
|
||||
Mini_LutForEachPo(lut, object)
|
||||
po_count++;
|
||||
uint32_t register_count = (uint32_t)Mini_LutRegNum(lut);
|
||||
if (pi_count != boundary->cis.size || po_count != boundary->cos.size ||
|
||||
register_count != boundary->register_bits || register_count > pi_count || register_count > po_count)
|
||||
return false;
|
||||
for (uint32_t i = 0; i < register_count; i++)
|
||||
if (sn_vec_at(sn_blast_boundary_bit_t, &boundary->cis, pi_count - register_count + i).kind !=
|
||||
SN_BLAST_BOUNDARY_REG_OUTPUT ||
|
||||
sn_vec_at(sn_blast_boundary_bit_t, &boundary->cos, po_count - register_count + i).kind !=
|
||||
SN_BLAST_BOUNDARY_REG_INPUT)
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
|
||||
// Validates MiniLUT topology and its positional interface against the boundary
|
||||
// saved while deriving the pre-ABC MiniAIG. Levels count LUTs; constants and
|
||||
// CIs have level zero. The boundary CO vector is in the same order as MiniLUT
|
||||
// POs, so depths can be reported separately for top outputs, hard-block inputs,
|
||||
// register controls, and register inputs.
|
||||
static inline sn_lut_stats_t sn_lut_analyze(Mini_Lut_t* lut, const sn_blast_boundary_t* boundary)
|
||||
{
|
||||
assert(lut && boundary);
|
||||
assert(sn_lut_interface_matches(lut, boundary));
|
||||
assert(Mini_LutSize(lut) >= 2 && Mini_LutSize(lut) <= 16);
|
||||
size_t object_count = (size_t)Mini_LutNodeNum(lut);
|
||||
uint32_t* levels = (uint32_t*)calloc(object_count, sizeof(uint32_t));
|
||||
assert(levels);
|
||||
sn_lut_stats_t stats = {0};
|
||||
stats.lut_size = (uint32_t)Mini_LutSize(lut);
|
||||
|
||||
for (int object = 0; object < Mini_LutNodeNum(lut); object++)
|
||||
{
|
||||
if (Mini_LutNodeIsConst(lut, object))
|
||||
continue;
|
||||
if (Mini_LutNodeIsPi(lut, object))
|
||||
{
|
||||
stats.pi_count++;
|
||||
continue;
|
||||
}
|
||||
if (Mini_LutNodeIsNode(lut, object))
|
||||
{
|
||||
uint32_t level = 0;
|
||||
int fanin, slot;
|
||||
Mini_LutForEachFanin(lut, object, fanin, slot)
|
||||
{
|
||||
assert(fanin >= 0 && fanin < object);
|
||||
level = sn_lut_max_u32(level, levels[fanin]);
|
||||
}
|
||||
levels[object] = level + 1;
|
||||
stats.lut_levels = sn_lut_max_u32(stats.lut_levels, levels[object]);
|
||||
stats.lut_count++;
|
||||
continue;
|
||||
}
|
||||
assert(Mini_LutNodeIsPo(lut, object));
|
||||
int fanin = Mini_LutNodeFanin(lut, object, 0);
|
||||
assert(fanin >= 0 && fanin < object);
|
||||
levels[object] = levels[fanin];
|
||||
stats.po_count++;
|
||||
}
|
||||
|
||||
stats.register_count = (uint32_t)Mini_LutRegNum(lut);
|
||||
|
||||
uint32_t po_index = 0;
|
||||
int object;
|
||||
Mini_LutForEachPo(lut, object)
|
||||
{
|
||||
sn_blast_boundary_kind_t kind =
|
||||
sn_vec_at(sn_blast_boundary_bit_t, &boundary->cos, po_index++).kind;
|
||||
uint32_t level = levels[object];
|
||||
if (kind == SN_BLAST_BOUNDARY_TOP_PO)
|
||||
stats.top_output_levels = sn_lut_max_u32(stats.top_output_levels, level);
|
||||
else if (kind == SN_BLAST_BOUNDARY_REG_CONTROL)
|
||||
stats.register_control_levels = sn_lut_max_u32(stats.register_control_levels, level);
|
||||
else if (kind == SN_BLAST_BOUNDARY_MEMORY_INPUT)
|
||||
stats.memory_input_levels = sn_lut_max_u32(stats.memory_input_levels, level);
|
||||
else if (kind == SN_BLAST_BOUNDARY_PRIMITIVE_INPUT)
|
||||
stats.primitive_input_levels = sn_lut_max_u32(stats.primitive_input_levels, level);
|
||||
else if (kind == SN_BLAST_BOUNDARY_LOOP_INPUT)
|
||||
stats.loop_input_levels = sn_lut_max_u32(stats.loop_input_levels, level);
|
||||
else if (kind == SN_BLAST_BOUNDARY_REG_INPUT)
|
||||
stats.register_input_levels = sn_lut_max_u32(stats.register_input_levels, level);
|
||||
else
|
||||
assert(false);
|
||||
}
|
||||
assert(po_index == stats.po_count);
|
||||
free(levels);
|
||||
return stats;
|
||||
}
|
||||
|
||||
static inline sn_obj_id_t sn_lut_pack_bits(sn_module_t* module, const sn_obj_id_t* bits, uint32_t width,
|
||||
const char* name)
|
||||
{
|
||||
assert(width && bits);
|
||||
if (width == 1)
|
||||
return bits[0];
|
||||
return sn_module_add_operator(module, SN_CONCAT, width, false, width, bits, name);
|
||||
}
|
||||
|
||||
static inline uint64_t sn_lut_node_truth(Mini_Lut_t* lut, int object)
|
||||
{
|
||||
unsigned* words = Mini_LutNodeTruth(lut, object);
|
||||
return (uint64_t)words[0] | (Mini_LutWordNum(Mini_LutSize(lut)) > 1 ? (uint64_t)words[1] << 32 : 0);
|
||||
}
|
||||
|
||||
// Decomposes a mapped LUT wider than the physical SN_LUT6 primitive by Shannon expansion on its most-significant
|
||||
// inputs. The leaves are LUT6 objects and each internal selector is another LUT3. MiniLUT and SN both use fanin 0 as
|
||||
// the least-significant truth-table variable, so each cofactor is a contiguous truth-table interval.
|
||||
static inline sn_obj_id_t sn_lut_add_physical_rec(sn_module_t* module, const sn_obj_id_t* fanins,
|
||||
uint32_t count, const unsigned* truth, uint32_t offset)
|
||||
{
|
||||
assert(module && fanins && truth && count > 0 && count <= 16);
|
||||
if (count <= 6)
|
||||
{
|
||||
uint64_t leaf_truth = 0;
|
||||
for (uint32_t bit = 0; bit < (UINT32_C(1) << count); bit++)
|
||||
leaf_truth |= (uint64_t)((truth[(offset + bit) >> 5] >> ((offset + bit) & 31)) & 1) << bit;
|
||||
return sn_module_add_lut(module, count, fanins, leaf_truth, "lut");
|
||||
}
|
||||
uint32_t select_bit = count - 1;
|
||||
sn_obj_id_t low = sn_lut_add_physical_rec(module, fanins, select_bit, truth, offset);
|
||||
sn_obj_id_t high = sn_lut_add_physical_rec(module, fanins, select_bit, truth,
|
||||
offset + (UINT32_C(1) << select_bit));
|
||||
sn_obj_id_t mux_fanins[3] = {fanins[select_bit], high, low};
|
||||
return sn_module_add_lut(module, 3, mux_fanins, UINT64_C(0xd8), "lut_wide_mux");
|
||||
}
|
||||
|
||||
// Reconstructs the MiniLUT combinational network and its top-level/register
|
||||
// boundary as a new flat SN module. Hard-block and control reconnection is
|
||||
// added by subsequent reconstruction stages; this core establishes the direct
|
||||
// MiniLUT-object-to-SN-object mapping and preserves MiniLUT register order.
|
||||
static inline sn_module_id_t sn_design_add_lut_module(sn_design_t* design, sn_module_id_t source_top_id,
|
||||
Mini_Lut_t* lut, const sn_blast_boundary_t* boundary,
|
||||
const char* module_name)
|
||||
{
|
||||
assert(design && source_top_id < design->modules.size && lut && boundary && module_name);
|
||||
sn_lut_analyze(lut, boundary);
|
||||
const sn_module_t* source = sn_design_get_module_const(design, source_top_id);
|
||||
sn_module_id_t result_id = sn_design_add_module(design, module_name);
|
||||
sn_module_t* result = sn_design_get_module(design, result_id);
|
||||
sn_obj_id_t* top_inputs = (sn_obj_id_t*)malloc(sizeof(sn_obj_id_t) * source->obj_types.size);
|
||||
sn_obj_id_t* mini_objects = (sn_obj_id_t*)malloc(sizeof(sn_obj_id_t) * Mini_LutNodeNum(lut));
|
||||
sn_obj_id_t* co_drivers = (sn_obj_id_t*)malloc(sizeof(sn_obj_id_t) * boundary->cos.size);
|
||||
sn_boundary_regs_t regs;
|
||||
assert(top_inputs && mini_objects && co_drivers);
|
||||
for (size_t i = 0; i < source->obj_types.size; i++)
|
||||
top_inputs[i] = SN_INVALID_ID;
|
||||
for (int i = 0; i < Mini_LutNodeNum(lut); i++)
|
||||
mini_objects[i] = SN_INVALID_ID;
|
||||
|
||||
for (size_t i = 0; i < source->type_objects[SN_PI].size; i++)
|
||||
{
|
||||
sn_obj_id_t old_pi = sn_vec_at(sn_obj_id_t, &source->type_objects[SN_PI], i);
|
||||
top_inputs[old_pi] = sn_module_add_pi(result, sn_obj_width(source, old_pi), sn_obj_is_signed(source, old_pi),
|
||||
sn_obj_name(source, old_pi));
|
||||
}
|
||||
sn_boundary_regs_init(®s, design, boundary, result, top_inputs);
|
||||
uint32_t zero_word = 0, one_word = 1;
|
||||
mini_objects[Mini_LutNodeConst0()] = sn_module_add_const(result, 1, false, &zero_word, "lut_const0");
|
||||
mini_objects[Mini_LutNodeConst1()] = sn_module_add_const(result, 1, false, &one_word, "lut_const1");
|
||||
|
||||
uint32_t ci_index = 0;
|
||||
int mini_object;
|
||||
Mini_LutForEachPi(lut, mini_object)
|
||||
{
|
||||
sn_blast_boundary_bit_t bit = sn_vec_at(sn_blast_boundary_bit_t, &boundary->cis, ci_index++);
|
||||
if (bit.kind == SN_BLAST_BOUNDARY_TOP_PI)
|
||||
{
|
||||
assert(bit.signal.occurrence == 0 && top_inputs[bit.signal.object] != SN_INVALID_ID);
|
||||
mini_objects[mini_object] =
|
||||
sn_module_add_slice(result, top_inputs[bit.signal.object], (int32_t)bit.signal.bit,
|
||||
(int32_t)bit.signal.bit, "lut_pi_bit");
|
||||
}
|
||||
else if (bit.kind == SN_BLAST_BOUNDARY_REG_OUTPUT)
|
||||
mini_objects[mini_object] = sn_boundary_reg_output_bit(®s, bit.owner, bit.signal.bit);
|
||||
else if (bit.kind == SN_BLAST_BOUNDARY_LOOP_OUTPUT)
|
||||
mini_objects[mini_object] = sn_boundary_loop_output_bit(®s, bit.owner, bit.signal.bit);
|
||||
else if (bit.kind == SN_BLAST_BOUNDARY_PRIMITIVE_OUTPUT)
|
||||
mini_objects[mini_object] =
|
||||
sn_boundary_primitive_output_bit(®s, bit.owner, bit.port, bit.signal.bit);
|
||||
else
|
||||
assert(false);
|
||||
}
|
||||
assert(ci_index == boundary->cis.size);
|
||||
|
||||
Mini_LutForEachNode(lut, mini_object)
|
||||
{
|
||||
sn_obj_id_t fanins[16];
|
||||
int fanin, slot, count = 0;
|
||||
Mini_LutForEachFanin(lut, mini_object, fanin, slot)
|
||||
{
|
||||
assert(count < 16 && mini_objects[fanin] != SN_INVALID_ID);
|
||||
fanins[count++] = mini_objects[fanin];
|
||||
}
|
||||
mini_objects[mini_object] = count <= 6
|
||||
? sn_module_add_lut(result, (uint32_t)count, fanins,
|
||||
sn_lut_node_truth(lut, mini_object), "lut")
|
||||
: sn_lut_add_physical_rec(result, fanins, (uint32_t)count,
|
||||
Mini_LutNodeTruth(lut, mini_object), 0);
|
||||
}
|
||||
uint32_t co_index = 0;
|
||||
Mini_LutForEachPo(lut, mini_object)
|
||||
{
|
||||
int fanin = Mini_LutNodeFanin(lut, mini_object, 0);
|
||||
assert(mini_objects[fanin] != SN_INVALID_ID);
|
||||
co_drivers[co_index++] = mini_objects[fanin];
|
||||
}
|
||||
assert(co_index == boundary->cos.size);
|
||||
|
||||
co_index = 0;
|
||||
for (size_t i = 0; i < source->type_objects[SN_PO].size; i++)
|
||||
{
|
||||
sn_obj_id_t old_po = sn_vec_at(sn_obj_id_t, &source->type_objects[SN_PO], i);
|
||||
uint32_t width = sn_obj_width(source, old_po);
|
||||
sn_obj_id_t* bits = co_drivers + co_index;
|
||||
for (uint32_t bit = 0; bit < width; bit++)
|
||||
{
|
||||
sn_blast_boundary_bit_t endpoint = sn_vec_at(sn_blast_boundary_bit_t, &boundary->cos, co_index + bit);
|
||||
assert(endpoint.kind == SN_BLAST_BOUNDARY_TOP_PO && endpoint.port == i && endpoint.signal.bit == bit);
|
||||
}
|
||||
co_index += width;
|
||||
sn_obj_id_t driver = sn_lut_pack_bits(result, bits, width, "lut_po_word");
|
||||
sn_module_add_po(result, width, sn_obj_is_signed(source, old_po), sn_obj_name(source, old_po), driver);
|
||||
}
|
||||
sn_boundary_regs_finish(®s, co_drivers);
|
||||
result = sn_design_get_module(design, result_id);
|
||||
|
||||
free(co_drivers);
|
||||
free(mini_objects);
|
||||
free(top_inputs);
|
||||
if (!sn_module_is_topo(result))
|
||||
sn_design_reorder_module_topo(design, result_id);
|
||||
assert(sn_module_is_topo(sn_design_get_module_const(design, result_id)));
|
||||
return result_id;
|
||||
}
|
||||
|
||||
ABC_NAMESPACE_HEADER_END
|
||||
|
||||
#endif
|
||||
|
|
@ -0,0 +1,921 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [snMux.h]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [New word-level design interface.]
|
||||
|
||||
Synopsis [Mux-path sharing and restructuring for word-level SN designs.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: snMux.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#ifndef SN_MUX_H
|
||||
#define SN_MUX_H
|
||||
|
||||
// Word-level mux-path sharing for register-fed SN_MUX trees and nested SN_PMUX objects. Root-to-terminal paths are
|
||||
// enumerated, structurally equal LSB-first words are represented once, and their path conditions are ORed. A hold
|
||||
// terminal is moved into SN_REG_ENABLE when controls are provably exclusive. General PMUX alternatives preserve SN's
|
||||
// one-hot-select semantics; as for SN_PMUX itself, behavior for multi-hot selects is unspecified. Modules are
|
||||
// duplicated and rewritten transactionally; hierarchy, stable module IDs, and the complete canonical register
|
||||
// interface are preserved.
|
||||
|
||||
#include "sn.h"
|
||||
|
||||
#include <assert.h>
|
||||
#include <stdbool.h>
|
||||
#include <stdint.h>
|
||||
#include <stdlib.h>
|
||||
|
||||
ABC_NAMESPACE_HEADER_START
|
||||
|
||||
typedef struct sn_share_options_t
|
||||
{
|
||||
uint32_t min_width;
|
||||
uint32_t min_alternatives;
|
||||
uint32_t min_saved_paths;
|
||||
} sn_share_options_t;
|
||||
|
||||
typedef struct sn_share_stats_t
|
||||
{
|
||||
uint64_t modules;
|
||||
uint64_t registers;
|
||||
uint64_t muxes;
|
||||
uint64_t paths_before;
|
||||
uint64_t paths_after;
|
||||
} sn_share_stats_t;
|
||||
|
||||
typedef struct sn_share_step_t
|
||||
{
|
||||
sn_obj_id_t select;
|
||||
uint32_t bit;
|
||||
bool positive;
|
||||
} sn_share_step_t;
|
||||
|
||||
typedef struct sn_share_path_t
|
||||
{
|
||||
sn_obj_id_t term;
|
||||
uint32_t step_offset;
|
||||
uint32_t step_count;
|
||||
uint32_t group;
|
||||
} sn_share_path_t;
|
||||
|
||||
enum
|
||||
{
|
||||
SN_SHARE_MAX_PATHS = 1 << 20,
|
||||
SN_SHARE_MAX_DEPTH = 4096,
|
||||
SN_SHARE_MAX_STEPS = 1 << 24
|
||||
};
|
||||
|
||||
static inline sn_share_options_t sn_share_default_options(void)
|
||||
{
|
||||
sn_share_options_t options = {4, 6, 2};
|
||||
return options;
|
||||
}
|
||||
|
||||
static inline sn_obj_id_t sn_share_strip_value(const sn_module_t* module, sn_obj_id_t object)
|
||||
{
|
||||
while (object != SN_INVALID_ID)
|
||||
{
|
||||
sn_obj_type_t type = sn_obj_type(module, object);
|
||||
if ((type != SN_BUF && type != SN_POS && type != SN_CAST) || sn_obj_fanin_count(module, object) != 1 ||
|
||||
sn_obj_width(module, object) != sn_obj_width(module, sn_obj_fanin(module, object, 0)))
|
||||
break;
|
||||
object = sn_obj_fanin(module, object, 0);
|
||||
}
|
||||
return object;
|
||||
}
|
||||
|
||||
static inline bool sn_share_const_equal(const sn_module_t* module, sn_obj_id_t a, sn_obj_id_t b)
|
||||
{
|
||||
if (sn_obj_width(module, a) != sn_obj_width(module, b))
|
||||
return false;
|
||||
sn_obj_type_t ta = sn_obj_type(module, a), tb = sn_obj_type(module, b);
|
||||
if ((ta != SN_CONST0 && ta != SN_CONST1 && ta != SN_CONST) ||
|
||||
(tb != SN_CONST0 && tb != SN_CONST1 && tb != SN_CONST))
|
||||
return false;
|
||||
uint32_t width = sn_obj_width(module, a);
|
||||
for (uint32_t bit = 0; bit < width; bit++)
|
||||
{
|
||||
bool av = (ta == SN_CONST1 && bit == 0) ||
|
||||
(ta == SN_CONST && ((sn_const_words(module, a)[bit >> 5] >> (bit & 31)) & 1));
|
||||
bool bv = (tb == SN_CONST1 && bit == 0) ||
|
||||
(tb == SN_CONST && ((sn_const_words(module, b)[bit >> 5] >> (bit & 31)) & 1));
|
||||
if (av != bv)
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
// Returns the unique raw selector value accepted by an equality comparison,
|
||||
// accounting for the comparison's signed extension. A wider constant whose
|
||||
// high bits cannot equal the extended selector makes the predicate impossible.
|
||||
static inline bool sn_share_decode_value(const sn_module_t* module, sn_obj_id_t value,
|
||||
sn_obj_id_t constant, uint32_t* decoded)
|
||||
{
|
||||
uint32_t value_width = sn_obj_width(module, value);
|
||||
uint32_t constant_width = sn_obj_width(module, constant);
|
||||
bool sign = sn_obj_is_signed(module, value) && sn_obj_is_signed(module, constant);
|
||||
if (!value_width || value_width >= 31)
|
||||
return false;
|
||||
uint32_t result = 0;
|
||||
for (uint32_t bit = 0; bit < value_width; bit++)
|
||||
{
|
||||
bool constant_bit = bit < constant_width ? sn_const_bit(module, constant, bit)
|
||||
: sign && sn_const_bit(module, constant, constant_width - 1);
|
||||
result |= (uint32_t)constant_bit << bit;
|
||||
}
|
||||
if (constant_width > value_width)
|
||||
{
|
||||
bool extension = sign && ((result >> (value_width - 1)) & 1);
|
||||
for (uint32_t bit = value_width; bit < constant_width; bit++)
|
||||
if (sn_const_bit(module, constant, bit) != extension)
|
||||
return false;
|
||||
}
|
||||
*decoded = result;
|
||||
return true;
|
||||
}
|
||||
|
||||
// Structural word identity through the inexpensive wiring operators used heavily by Slang lowering. This is the
|
||||
// object-level counterpart of UtilMux's canonical bit-vector IDs: separately-created slices/concatenations of the
|
||||
// same LSB-first source bits are recognized as the same mux terminal without bit-blasting the module.
|
||||
static inline bool sn_share_value_equal(const sn_module_t* module, sn_obj_id_t a, sn_obj_id_t b)
|
||||
{
|
||||
a = sn_share_strip_value(module, a);
|
||||
b = sn_share_strip_value(module, b);
|
||||
if (a == b)
|
||||
return true;
|
||||
if (sn_obj_width(module, a) != sn_obj_width(module, b))
|
||||
return false;
|
||||
sn_obj_type_t ta = sn_obj_type(module, a), tb = sn_obj_type(module, b);
|
||||
if ((ta == SN_CONST0 || ta == SN_CONST1 || ta == SN_CONST) &&
|
||||
(tb == SN_CONST0 || tb == SN_CONST1 || tb == SN_CONST))
|
||||
return sn_share_const_equal(module, a, b);
|
||||
if (ta != tb)
|
||||
return false;
|
||||
if (ta == SN_SLICE)
|
||||
{
|
||||
const sn_slice_info_t* ia = sn_obj_slice_info(module, a);
|
||||
const sn_slice_info_t* ib = sn_obj_slice_info(module, b);
|
||||
return ia->left_index == ib->left_index && ia->right_index == ib->right_index &&
|
||||
sn_share_value_equal(module, sn_obj_fanin(module, a, 0), sn_obj_fanin(module, b, 0));
|
||||
}
|
||||
if (ta == SN_REPLICATE)
|
||||
return sn_obj_repeat_count(module, a) == sn_obj_repeat_count(module, b) &&
|
||||
sn_share_value_equal(module, sn_obj_fanin(module, a, 0), sn_obj_fanin(module, b, 0));
|
||||
if (ta == SN_CONCAT && sn_obj_fanin_count(module, a) == sn_obj_fanin_count(module, b))
|
||||
{
|
||||
for (uint32_t i = 0; i < sn_obj_fanin_count(module, a); i++)
|
||||
if (!sn_share_value_equal(module, sn_obj_fanin(module, a, i), sn_obj_fanin(module, b, i)))
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
static inline uint64_t sn_share_hash_mix(uint64_t hash, uint64_t value)
|
||||
{
|
||||
hash ^= value;
|
||||
return hash * UINT64_C(1099511628211);
|
||||
}
|
||||
|
||||
// Compute structural hashes for the inexpensive wiring words recognized by sn_share_value_equal(). Modules entering
|
||||
// @opt_mux are topologically ordered, so every hashed wiring fanin is already available. Unsupported terminals retain
|
||||
// object identity. Hash collisions are always resolved with the exact structural comparison.
|
||||
static inline uint64_t* sn_share_value_hashes(const sn_module_t* module)
|
||||
{
|
||||
uint64_t* hashes = (uint64_t*)calloc(module->obj_types.size, sizeof(uint64_t));
|
||||
assert(hashes || module->obj_types.size == 0);
|
||||
for (sn_obj_id_t object = 0; object < module->obj_types.size; object++)
|
||||
{
|
||||
sn_obj_type_t type = sn_obj_type(module, object);
|
||||
uint64_t hash = sn_share_hash_mix(UINT64_C(1469598103934665603), sn_obj_width(module, object));
|
||||
if (type == SN_BUF || type == SN_POS || type == SN_CAST)
|
||||
{
|
||||
sn_obj_id_t fanin = sn_obj_fanin(module, object, 0);
|
||||
hashes[object] = sn_obj_width(module, object) == sn_obj_width(module, fanin)
|
||||
? hashes[fanin] : sn_share_hash_mix(hash, object);
|
||||
continue;
|
||||
}
|
||||
if (type == SN_CONST0 || type == SN_CONST1 || type == SN_CONST)
|
||||
{
|
||||
uint32_t count = sn_const_word_count(sn_obj_width(module, object));
|
||||
for (uint32_t i = 0; i < count; i++)
|
||||
{
|
||||
uint32_t word = type == SN_CONST ? sn_const_words(module, object)[i]
|
||||
: type == SN_CONST1 && i == 0 ? 1 : 0;
|
||||
if (i + 1 == count && (sn_obj_width(module, object) & 31))
|
||||
word &= (UINT32_C(1) << (sn_obj_width(module, object) & 31)) - 1;
|
||||
hash = sn_share_hash_mix(hash, word);
|
||||
}
|
||||
hashes[object] = hash;
|
||||
continue;
|
||||
}
|
||||
hash = sn_share_hash_mix(hash, type);
|
||||
if (type == SN_SLICE)
|
||||
{
|
||||
const sn_slice_info_t* info = sn_obj_slice_info(module, object);
|
||||
hash = sn_share_hash_mix(hash, (uint32_t)info->left_index);
|
||||
hash = sn_share_hash_mix(hash, (uint32_t)info->right_index);
|
||||
hash = sn_share_hash_mix(hash, hashes[sn_obj_fanin(module, object, 0)]);
|
||||
}
|
||||
else if (type == SN_REPLICATE)
|
||||
{
|
||||
hash = sn_share_hash_mix(hash, sn_obj_repeat_count(module, object));
|
||||
hash = sn_share_hash_mix(hash, hashes[sn_obj_fanin(module, object, 0)]);
|
||||
}
|
||||
else if (type == SN_CONCAT)
|
||||
for (uint32_t i = 0; i < sn_obj_fanin_count(module, object); i++)
|
||||
hash = sn_share_hash_mix(hash, hashes[sn_obj_fanin(module, object, i)]);
|
||||
else
|
||||
hash = sn_share_hash_mix(hash, object);
|
||||
hashes[object] = hash;
|
||||
}
|
||||
return hashes;
|
||||
}
|
||||
|
||||
static inline bool sn_share_hashed_equal(const sn_module_t* module, const uint64_t* hashes,
|
||||
sn_obj_id_t a, sn_obj_id_t b)
|
||||
{
|
||||
a = sn_share_strip_value(module, a);
|
||||
b = sn_share_strip_value(module, b);
|
||||
return hashes[a] == hashes[b] && sn_share_value_equal(module, a, b);
|
||||
}
|
||||
|
||||
// Recognize a binary decode. The equality predicates compare one common selector against distinct constants, so at
|
||||
// most one PMUX select bit is true and ordinary combinational CEC is valid. An incomplete decode uses the PMUX default.
|
||||
static inline bool sn_share_select_is_decode(const sn_module_t* module, sn_obj_id_t select)
|
||||
{
|
||||
if (sn_obj_type(module, select) != SN_CONCAT || sn_obj_fanin_count(module, select) < 2)
|
||||
return false;
|
||||
sn_obj_id_t common = SN_INVALID_ID;
|
||||
sn_vec_t decoded_values;
|
||||
sn_vec_init(&decoded_values);
|
||||
for (uint32_t i = 0; i < sn_obj_fanin_count(module, select); i++)
|
||||
{
|
||||
sn_obj_id_t compare = sn_obj_fanin(module, select, i);
|
||||
sn_obj_type_t type = sn_obj_type(module, compare);
|
||||
if ((type != SN_EQ && type != SN_CASE_EQ) || sn_obj_fanin_count(module, compare) != 2)
|
||||
{
|
||||
sn_vec_destroy(&decoded_values);
|
||||
return false;
|
||||
}
|
||||
sn_obj_id_t value = sn_obj_fanin(module, compare, 0), constant = sn_obj_fanin(module, compare, 1);
|
||||
sn_obj_type_t constant_type = sn_obj_type(module, constant);
|
||||
if (constant_type != SN_CONST0 && constant_type != SN_CONST1 && constant_type != SN_CONST)
|
||||
{
|
||||
sn_vec_destroy(&decoded_values);
|
||||
return false;
|
||||
}
|
||||
if (common == SN_INVALID_ID)
|
||||
common = value;
|
||||
else if (sn_share_strip_value(module, value) != sn_share_strip_value(module, common) ||
|
||||
sn_obj_width(module, value) != sn_obj_width(module, common) ||
|
||||
sn_obj_is_signed(module, value) != sn_obj_is_signed(module, common))
|
||||
{
|
||||
sn_vec_destroy(&decoded_values);
|
||||
return false;
|
||||
}
|
||||
uint32_t decoded;
|
||||
if (!sn_share_decode_value(module, value, constant, &decoded))
|
||||
continue;
|
||||
for (size_t j = 0; j < decoded_values.size; j++)
|
||||
if (sn_vec_at(uint32_t, &decoded_values, j) == decoded)
|
||||
{
|
||||
sn_vec_destroy(&decoded_values);
|
||||
return false;
|
||||
}
|
||||
*sn_vec_push(uint32_t, &decoded_values) = decoded;
|
||||
}
|
||||
uint32_t width = sn_obj_width(module, common);
|
||||
bool result = width < 31 && sn_obj_fanin_count(module, select) <= (UINT32_C(1) << width);
|
||||
sn_vec_destroy(&decoded_values);
|
||||
return result;
|
||||
}
|
||||
|
||||
static inline bool sn_share_pmux_words(const sn_module_t* module, sn_obj_id_t pmux, sn_vec_t* words)
|
||||
{
|
||||
assert(sn_obj_type(module, pmux) == SN_PMUX);
|
||||
sn_obj_id_t select = sn_obj_fanin(module, pmux, SN_PMUX_SELECT);
|
||||
sn_obj_id_t packed = sn_obj_fanin(module, pmux, SN_PMUX_ALTERNATIVES);
|
||||
uint32_t count = sn_obj_width(module, select), width = sn_obj_width(module, pmux);
|
||||
sn_vec_init(words);
|
||||
if (sn_obj_type(module, packed) != SN_CONCAT || sn_obj_fanin_count(module, packed) != count)
|
||||
return false;
|
||||
sn_vec_reserve(sn_obj_id_t, words, count);
|
||||
for (uint32_t i = 0; i < count; i++)
|
||||
{
|
||||
sn_obj_id_t word = sn_obj_fanin(module, packed, i);
|
||||
if (sn_obj_width(module, word) != width)
|
||||
{
|
||||
sn_vec_destroy(words);
|
||||
sn_vec_init(words);
|
||||
return false;
|
||||
}
|
||||
*sn_vec_push(sn_obj_id_t, words) = sn_share_strip_value(module, word);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
static inline sn_obj_id_t sn_share_or(sn_module_t* module, const sn_obj_id_t* values, uint32_t count)
|
||||
{
|
||||
assert(count);
|
||||
if (count == 1)
|
||||
return values[0];
|
||||
sn_vec_t level, next;
|
||||
sn_vec_init(&level);
|
||||
sn_vec_init(&next);
|
||||
sn_vec_reserve(sn_obj_id_t, &level, count);
|
||||
for (uint32_t i = 0; i < count; i++)
|
||||
*sn_vec_push(sn_obj_id_t, &level) = values[i];
|
||||
while (level.size > 1)
|
||||
{
|
||||
next.size = 0;
|
||||
for (size_t i = 0; i < level.size; i += 2)
|
||||
{
|
||||
if (i + 1 == level.size)
|
||||
*sn_vec_push(sn_obj_id_t, &next) = sn_vec_at(sn_obj_id_t, &level, i);
|
||||
else
|
||||
{
|
||||
sn_obj_id_t fanins[2] = {sn_vec_at(sn_obj_id_t, &level, i),
|
||||
sn_vec_at(sn_obj_id_t, &level, i + 1)};
|
||||
*sn_vec_push(sn_obj_id_t, &next) =
|
||||
sn_module_add_operator(module, SN_BIT_OR, 1, false, 2, fanins, NULL);
|
||||
}
|
||||
}
|
||||
sn_vec_t swap = level;
|
||||
level = next;
|
||||
next = swap;
|
||||
}
|
||||
sn_obj_id_t result = sn_vec_at(sn_obj_id_t, &level, 0);
|
||||
sn_vec_destroy(&level);
|
||||
sn_vec_destroy(&next);
|
||||
return result;
|
||||
}
|
||||
|
||||
static inline sn_obj_id_t sn_share_and(sn_module_t* module, const sn_obj_id_t* values, uint32_t count)
|
||||
{
|
||||
assert(count);
|
||||
if (count == 1)
|
||||
return values[0];
|
||||
sn_vec_t level, next;
|
||||
sn_vec_init(&level);
|
||||
sn_vec_init(&next);
|
||||
for (uint32_t i = 0; i < count; i++)
|
||||
*sn_vec_push(sn_obj_id_t, &level) = values[i];
|
||||
while (level.size > 1)
|
||||
{
|
||||
next.size = 0;
|
||||
for (size_t i = 0; i < level.size; i += 2)
|
||||
{
|
||||
if (i + 1 == level.size)
|
||||
*sn_vec_push(sn_obj_id_t, &next) = sn_vec_at(sn_obj_id_t, &level, i);
|
||||
else
|
||||
{
|
||||
sn_obj_id_t fanins[2] = {sn_vec_at(sn_obj_id_t, &level, i),
|
||||
sn_vec_at(sn_obj_id_t, &level, i + 1)};
|
||||
*sn_vec_push(sn_obj_id_t, &next) =
|
||||
sn_module_add_operator(module, SN_BIT_AND, 1, false, 2, fanins, NULL);
|
||||
}
|
||||
}
|
||||
sn_vec_t swap = level;
|
||||
level = next;
|
||||
next = swap;
|
||||
}
|
||||
sn_obj_id_t result = sn_vec_at(sn_obj_id_t, &level, 0);
|
||||
sn_vec_destroy(&level);
|
||||
sn_vec_destroy(&next);
|
||||
return result;
|
||||
}
|
||||
|
||||
static inline void sn_share_collect_mux_paths(const sn_module_t* module, sn_obj_id_t object, sn_vec_t* stack,
|
||||
sn_vec_t* steps, sn_vec_t* paths, uint8_t* active, bool* exclusive,
|
||||
bool* overflow)
|
||||
{
|
||||
if (*overflow)
|
||||
return;
|
||||
if (stack->size >= SN_SHARE_MAX_DEPTH || paths->size >= SN_SHARE_MAX_PATHS ||
|
||||
steps->size > SN_SHARE_MAX_STEPS - stack->size)
|
||||
{
|
||||
*overflow = true;
|
||||
return;
|
||||
}
|
||||
object = sn_share_strip_value(module, object);
|
||||
if (sn_obj_type(module, object) == SN_MUX && !active[object])
|
||||
{
|
||||
active[object] = 1;
|
||||
sn_share_step_t* step = sn_vec_push(sn_share_step_t, stack);
|
||||
step->select = sn_obj_fanin(module, object, SN_MUX_SELECT);
|
||||
step->bit = 0;
|
||||
step->positive = true;
|
||||
sn_share_collect_mux_paths(module, sn_obj_fanin(module, object, SN_MUX_SELECTED), stack, steps, paths,
|
||||
active, exclusive, overflow);
|
||||
sn_vec_at(sn_share_step_t, stack, stack->size - 1).positive = false;
|
||||
sn_share_collect_mux_paths(module, sn_obj_fanin(module, object, SN_MUX_DEFAULT), stack, steps, paths,
|
||||
active, exclusive, overflow);
|
||||
stack->size--;
|
||||
active[object] = 0;
|
||||
return;
|
||||
}
|
||||
if (sn_obj_type(module, object) == SN_PMUX && !active[object])
|
||||
{
|
||||
sn_obj_id_t select = sn_obj_fanin(module, object, SN_PMUX_SELECT);
|
||||
sn_vec_t words;
|
||||
sn_vec_init(&words);
|
||||
if (sn_share_pmux_words(module, object, &words))
|
||||
{
|
||||
if (!sn_share_select_is_decode(module, select))
|
||||
*exclusive = false;
|
||||
active[object] = 1;
|
||||
for (uint32_t i = 0; i < words.size; i++)
|
||||
{
|
||||
sn_share_step_t* step = sn_vec_push(sn_share_step_t, stack);
|
||||
step->select = select;
|
||||
step->bit = i;
|
||||
step->positive = true;
|
||||
sn_share_collect_mux_paths(module, sn_vec_at(sn_obj_id_t, &words, i), stack, steps, paths, active,
|
||||
exclusive, overflow);
|
||||
stack->size--;
|
||||
}
|
||||
size_t old_stack_size = stack->size;
|
||||
for (uint32_t i = 0; i < words.size; i++)
|
||||
{
|
||||
sn_share_step_t* step = sn_vec_push(sn_share_step_t, stack);
|
||||
step->select = select;
|
||||
step->bit = i;
|
||||
step->positive = false;
|
||||
}
|
||||
sn_share_collect_mux_paths(module, sn_obj_fanin(module, object, SN_PMUX_DEFAULT), stack, steps, paths,
|
||||
active, exclusive, overflow);
|
||||
stack->size = old_stack_size;
|
||||
active[object] = 0;
|
||||
sn_vec_destroy(&words);
|
||||
return;
|
||||
}
|
||||
sn_vec_destroy(&words);
|
||||
}
|
||||
assert(steps->size <= UINT32_MAX && stack->size <= UINT32_MAX);
|
||||
sn_share_path_t* path = sn_vec_push(sn_share_path_t, paths);
|
||||
path->term = object;
|
||||
path->step_offset = (uint32_t)steps->size;
|
||||
path->step_count = (uint32_t)stack->size;
|
||||
path->group = SN_INVALID_ID;
|
||||
sn_vec_reserve(sn_share_step_t, steps, steps->size + stack->size);
|
||||
for (size_t i = 0; i < stack->size; i++)
|
||||
*sn_vec_push(sn_share_step_t, steps) = sn_vec_at(sn_share_step_t, stack, i);
|
||||
}
|
||||
|
||||
static inline sn_obj_id_t sn_share_path_condition(sn_module_t* target, const sn_module_t* source,
|
||||
const sn_share_path_t* path, const sn_vec_t* steps)
|
||||
{
|
||||
sn_vec_t literals;
|
||||
sn_vec_init(&literals);
|
||||
for (uint32_t i = 0; i < path->step_count; i++)
|
||||
{
|
||||
sn_share_step_t step = sn_vec_at(sn_share_step_t, steps, path->step_offset + i);
|
||||
sn_obj_id_t literal = sn_obj_dup(source, step.select);
|
||||
if (sn_obj_width(target, literal) != 1)
|
||||
literal = sn_module_add_slice(target, literal, (int32_t)step.bit, (int32_t)step.bit, NULL);
|
||||
if (!step.positive)
|
||||
literal = sn_module_add_operator(target, SN_LOG_NOT, 1, false, 1, &literal, NULL);
|
||||
*sn_vec_push(sn_obj_id_t, &literals) = literal;
|
||||
}
|
||||
sn_obj_id_t result = sn_share_and(target, sn_vec_data(sn_obj_id_t, &literals), (uint32_t)literals.size);
|
||||
sn_vec_destroy(&literals);
|
||||
return result;
|
||||
}
|
||||
|
||||
static inline bool sn_share_reg_mux_tree(sn_module_t* target, const sn_module_t* source, sn_obj_id_t old_reg,
|
||||
const uint64_t* hashes, sn_share_options_t options, sn_share_stats_t* stats)
|
||||
{
|
||||
sn_obj_id_t old_in = sn_obj_pair_in(source, old_reg);
|
||||
sn_obj_id_t old_root = sn_obj_fanin(source, old_in, 0);
|
||||
if (old_root == SN_INVALID_ID || sn_obj_type(source, sn_share_strip_value(source, old_root)) != SN_MUX)
|
||||
return false;
|
||||
if (sn_obj_width(source, old_reg) < options.min_width)
|
||||
return false;
|
||||
sn_vec_t stack, steps, paths, terms, term_hashes, term_links, data_terms, controls;
|
||||
sn_obj_id_t hold = SN_INVALID_ID, data = SN_INVALID_ID, new_reg = SN_INVALID_ID;
|
||||
uint32_t* term_buckets = NULL;
|
||||
uint32_t* group_heads = NULL;
|
||||
uint32_t* path_links = NULL;
|
||||
uint32_t term_bucket_count = 0;
|
||||
size_t hold_index = 0;
|
||||
bool exclusive = true, overflow = false;
|
||||
sn_vec_init(&stack);
|
||||
sn_vec_init(&steps);
|
||||
sn_vec_init(&paths);
|
||||
sn_vec_init(&terms);
|
||||
sn_vec_init(&term_hashes);
|
||||
sn_vec_init(&term_links);
|
||||
sn_vec_init(&data_terms);
|
||||
sn_vec_init(&controls);
|
||||
uint8_t* active = (uint8_t*)calloc(source->obj_types.size, sizeof(uint8_t));
|
||||
assert(active);
|
||||
sn_share_collect_mux_paths(source, old_root, &stack, &steps, &paths, active, &exclusive, &overflow);
|
||||
free(active);
|
||||
if (overflow)
|
||||
goto unchanged;
|
||||
if (paths.size < options.min_alternatives)
|
||||
goto unchanged;
|
||||
term_bucket_count = 1;
|
||||
while (term_bucket_count < 2 * paths.size)
|
||||
term_bucket_count <<= 1;
|
||||
term_buckets = (uint32_t*)malloc((size_t)term_bucket_count * sizeof(uint32_t));
|
||||
assert(term_buckets);
|
||||
memset(term_buckets, 0xff, (size_t)term_bucket_count * sizeof(uint32_t));
|
||||
for (size_t i = 0; i < paths.size; i++)
|
||||
{
|
||||
sn_share_path_t* path = &sn_vec_at(sn_share_path_t, &paths, i);
|
||||
sn_obj_id_t term = path->term;
|
||||
uint64_t term_hash = hashes[sn_share_strip_value(source, term)];
|
||||
uint32_t bucket = (uint32_t)term_hash & (term_bucket_count - 1);
|
||||
uint32_t k;
|
||||
for (k = term_buckets[bucket]; k != SN_INVALID_ID; k = sn_vec_at(uint32_t, &term_links, k))
|
||||
if (sn_vec_at(uint64_t, &term_hashes, k) == term_hash &&
|
||||
sn_share_value_equal(source, sn_vec_at(sn_obj_id_t, &terms, k), term))
|
||||
break;
|
||||
if (k == SN_INVALID_ID)
|
||||
{
|
||||
k = (uint32_t)terms.size;
|
||||
*sn_vec_push(sn_obj_id_t, &terms) = term;
|
||||
*sn_vec_push(uint64_t, &term_hashes) = term_hash;
|
||||
*sn_vec_push(uint32_t, &term_links) = term_buckets[bucket];
|
||||
term_buckets[bucket] = k;
|
||||
}
|
||||
path->group = k;
|
||||
}
|
||||
if (paths.size <= terms.size || paths.size - terms.size < options.min_saved_paths || paths.size < 2 * terms.size)
|
||||
goto unchanged;
|
||||
group_heads = (uint32_t*)malloc(terms.size * sizeof(uint32_t));
|
||||
path_links = (uint32_t*)malloc(paths.size * sizeof(uint32_t));
|
||||
assert(group_heads && path_links);
|
||||
for (size_t k = 0; k < terms.size; k++)
|
||||
group_heads[k] = SN_INVALID_ID;
|
||||
for (size_t i = 0; i < paths.size; i++)
|
||||
{
|
||||
uint32_t group = sn_vec_at(sn_share_path_t, &paths, i).group;
|
||||
assert(group < terms.size);
|
||||
path_links[i] = group_heads[group];
|
||||
group_heads[group] = (uint32_t)i;
|
||||
}
|
||||
|
||||
hold = sn_share_strip_value(source, old_reg);
|
||||
hold_index = terms.size;
|
||||
if (exclusive)
|
||||
for (size_t k = 0; k < terms.size; k++)
|
||||
if (sn_share_hashed_equal(source, hashes, sn_vec_at(sn_obj_id_t, &terms, k), hold))
|
||||
hold_index = k;
|
||||
for (size_t k = 0; k < terms.size; k++)
|
||||
{
|
||||
if (k == hold_index)
|
||||
continue;
|
||||
sn_vec_t cubes;
|
||||
sn_vec_init(&cubes);
|
||||
for (uint32_t i = group_heads[k]; i != SN_INVALID_ID; i = path_links[i])
|
||||
{
|
||||
sn_share_path_t* path = &sn_vec_at(sn_share_path_t, &paths, i);
|
||||
*sn_vec_push(sn_obj_id_t, &cubes) = sn_share_path_condition(target, source, path, &steps);
|
||||
}
|
||||
*sn_vec_push(sn_obj_id_t, &controls) =
|
||||
sn_share_or(target, sn_vec_data(sn_obj_id_t, &cubes), (uint32_t)cubes.size);
|
||||
*sn_vec_push(sn_obj_id_t, &data_terms) = sn_obj_dup(source, sn_vec_at(sn_obj_id_t, &terms, k));
|
||||
sn_vec_destroy(&cubes);
|
||||
}
|
||||
if (!data_terms.size)
|
||||
{
|
||||
goto unchanged;
|
||||
}
|
||||
data = sn_vec_at(sn_obj_id_t, &data_terms, data_terms.size - 1);
|
||||
if (data_terms.size > 1)
|
||||
{
|
||||
sn_obj_id_t packed_select =
|
||||
sn_module_add_concat(target, (uint32_t)controls.size, sn_vec_data(sn_obj_id_t, &controls), NULL);
|
||||
sn_obj_id_t packed_data =
|
||||
sn_module_add_concat(target, (uint32_t)data_terms.size, sn_vec_data(sn_obj_id_t, &data_terms), NULL);
|
||||
data = sn_module_add_pmux(target, packed_select, packed_data, data, NULL);
|
||||
}
|
||||
new_reg = sn_obj_dup(source, old_reg);
|
||||
sn_obj_connect(target, sn_obj_pair_in(target, new_reg), 0, data);
|
||||
if (hold_index < terms.size)
|
||||
{
|
||||
sn_obj_id_t update = sn_share_or(target, sn_vec_data(sn_obj_id_t, &controls), (uint32_t)controls.size);
|
||||
sn_obj_id_t enable = sn_obj_fanin(target, new_reg, SN_REG_ENABLE);
|
||||
if (enable != SN_INVALID_ID)
|
||||
{
|
||||
sn_obj_id_t fanins[2] = {enable, update};
|
||||
update = sn_module_add_operator(target, SN_BIT_AND, 1, false, 2, fanins, NULL);
|
||||
}
|
||||
sn_reg_set_fanin(target, new_reg, SN_REG_ENABLE, update);
|
||||
}
|
||||
stats->registers++;
|
||||
stats->muxes++;
|
||||
stats->paths_before += paths.size;
|
||||
stats->paths_after += terms.size;
|
||||
sn_vec_destroy(&data_terms);
|
||||
sn_vec_destroy(&controls);
|
||||
sn_vec_destroy(&stack);
|
||||
sn_vec_destroy(&steps);
|
||||
sn_vec_destroy(&paths);
|
||||
sn_vec_destroy(&terms);
|
||||
sn_vec_destroy(&term_hashes);
|
||||
sn_vec_destroy(&term_links);
|
||||
free(path_links);
|
||||
free(group_heads);
|
||||
free(term_buckets);
|
||||
return true;
|
||||
|
||||
unchanged:
|
||||
sn_vec_destroy(&stack);
|
||||
sn_vec_destroy(&steps);
|
||||
sn_vec_destroy(&paths);
|
||||
sn_vec_destroy(&terms);
|
||||
sn_vec_destroy(&term_hashes);
|
||||
sn_vec_destroy(&term_links);
|
||||
free(path_links);
|
||||
free(group_heads);
|
||||
free(term_buckets);
|
||||
sn_vec_destroy(&data_terms);
|
||||
sn_vec_destroy(&controls);
|
||||
return false;
|
||||
}
|
||||
|
||||
static inline sn_obj_id_t sn_share_select_bit(sn_module_t* module, sn_obj_id_t select, uint32_t bit)
|
||||
{
|
||||
if (sn_obj_width(module, select) == 1)
|
||||
return select;
|
||||
return sn_module_add_slice(module, select, (int32_t)bit, (int32_t)bit, NULL);
|
||||
}
|
||||
|
||||
static inline bool sn_share_reg_pmux(sn_module_t* target, const sn_module_t* source, sn_obj_id_t old_reg,
|
||||
const uint64_t* hashes, sn_share_options_t options, sn_share_stats_t* stats)
|
||||
{
|
||||
sn_obj_id_t old_in = sn_obj_pair_in(source, old_reg);
|
||||
sn_obj_id_t old_root = sn_obj_fanin(source, old_in, 0);
|
||||
if (old_root != SN_INVALID_ID)
|
||||
old_root = sn_share_strip_value(source, old_root);
|
||||
if (old_root == SN_INVALID_ID || sn_obj_type(source, old_root) != SN_PMUX)
|
||||
return false;
|
||||
if (sn_obj_width(source, old_reg) < options.min_width)
|
||||
return false;
|
||||
sn_vec_t words;
|
||||
if (!sn_share_pmux_words(source, old_root, &words))
|
||||
return false;
|
||||
uint32_t count = (uint32_t)words.size;
|
||||
if (count < options.min_alternatives || count > UINT16_MAX)
|
||||
{
|
||||
sn_vec_destroy(&words);
|
||||
return false;
|
||||
}
|
||||
sn_obj_id_t old_default = sn_share_strip_value(source, sn_obj_fanin(source, old_root, SN_PMUX_DEFAULT));
|
||||
sn_obj_id_t old_hold = sn_share_strip_value(source, old_reg);
|
||||
bool extracts_hold = sn_share_select_is_decode(source, sn_obj_fanin(source, old_root, SN_PMUX_SELECT)) &&
|
||||
sn_share_hashed_equal(source, hashes, old_default, old_hold);
|
||||
sn_vec_t unique, unique_hashes, unique_links, conditions, members;
|
||||
sn_vec_init(&unique);
|
||||
sn_vec_init(&unique_hashes);
|
||||
sn_vec_init(&unique_links);
|
||||
sn_vec_init(&conditions);
|
||||
sn_vec_init(&members);
|
||||
uint32_t bucket_count = 1;
|
||||
while (bucket_count < 2 * count)
|
||||
bucket_count <<= 1;
|
||||
uint32_t* buckets = (uint32_t*)malloc((size_t)bucket_count * sizeof(uint32_t));
|
||||
uint32_t* member_heads = NULL;
|
||||
uint32_t* member_links = NULL;
|
||||
assert(buckets);
|
||||
memset(buckets, 0xff, (size_t)bucket_count * sizeof(uint32_t));
|
||||
for (uint32_t i = 0; i < count; i++)
|
||||
{
|
||||
sn_obj_id_t value = sn_vec_at(sn_obj_id_t, &words, i);
|
||||
if (extracts_hold && sn_share_hashed_equal(source, hashes, value, old_hold))
|
||||
continue;
|
||||
uint64_t value_hash = hashes[sn_share_strip_value(source, value)];
|
||||
uint32_t bucket = (uint32_t)value_hash & (bucket_count - 1);
|
||||
uint32_t k;
|
||||
for (k = buckets[bucket]; k != SN_INVALID_ID; k = sn_vec_at(uint32_t, &unique_links, k))
|
||||
if (sn_vec_at(uint64_t, &unique_hashes, k) == value_hash &&
|
||||
sn_share_value_equal(source, sn_vec_at(sn_obj_id_t, &unique, k), value))
|
||||
break;
|
||||
if (k == SN_INVALID_ID)
|
||||
{
|
||||
k = (uint32_t)unique.size;
|
||||
*sn_vec_push(sn_obj_id_t, &unique) = value;
|
||||
*sn_vec_push(uint64_t, &unique_hashes) = value_hash;
|
||||
*sn_vec_push(uint32_t, &unique_links) = buckets[bucket];
|
||||
buckets[bucket] = k;
|
||||
}
|
||||
assert(k <= UINT16_MAX && i <= UINT16_MAX);
|
||||
*sn_vec_push(uint32_t, &members) = ((uint32_t)k << 16) | i;
|
||||
}
|
||||
uint32_t after = (uint32_t)unique.size;
|
||||
uint32_t before = count + 1;
|
||||
if (!extracts_hold)
|
||||
after++;
|
||||
if (!unique.size || before <= after || before - after < options.min_saved_paths || before < 2 * after)
|
||||
{
|
||||
sn_vec_destroy(&words);
|
||||
sn_vec_destroy(&unique);
|
||||
sn_vec_destroy(&unique_hashes);
|
||||
sn_vec_destroy(&unique_links);
|
||||
sn_vec_destroy(&conditions);
|
||||
sn_vec_destroy(&members);
|
||||
free(buckets);
|
||||
return false;
|
||||
}
|
||||
member_heads = (uint32_t*)malloc(unique.size * sizeof(uint32_t));
|
||||
member_links = (uint32_t*)malloc(members.size * sizeof(uint32_t));
|
||||
assert(member_heads && member_links);
|
||||
for (size_t k = 0; k < unique.size; k++)
|
||||
member_heads[k] = SN_INVALID_ID;
|
||||
for (size_t j = 0; j < members.size; j++)
|
||||
{
|
||||
uint32_t group = sn_vec_at(uint32_t, &members, j) >> 16;
|
||||
assert(group < unique.size);
|
||||
member_links[j] = member_heads[group];
|
||||
member_heads[group] = (uint32_t)j;
|
||||
}
|
||||
|
||||
sn_obj_id_t new_reg = sn_obj_dup(source, old_reg);
|
||||
sn_obj_id_t new_in = sn_obj_pair_in(target, new_reg);
|
||||
sn_obj_id_t new_select = sn_obj_dup(source, sn_obj_fanin(source, old_root, SN_PMUX_SELECT));
|
||||
for (size_t k = 0; k < unique.size; k++)
|
||||
{
|
||||
sn_vec_t bits;
|
||||
sn_vec_init(&bits);
|
||||
for (uint32_t j = member_heads[k]; j != SN_INVALID_ID; j = member_links[j])
|
||||
{
|
||||
uint32_t member = sn_vec_at(uint32_t, &members, j);
|
||||
*sn_vec_push(sn_obj_id_t, &bits) = sn_share_select_bit(target, new_select, member & UINT16_MAX);
|
||||
}
|
||||
*sn_vec_push(sn_obj_id_t, &conditions) =
|
||||
sn_share_or(target, sn_vec_data(sn_obj_id_t, &bits), (uint32_t)bits.size);
|
||||
sn_vec_destroy(&bits);
|
||||
}
|
||||
sn_obj_id_t new_data;
|
||||
if (unique.size == 1)
|
||||
{
|
||||
sn_obj_id_t alternative = sn_obj_dup(source, sn_vec_at(sn_obj_id_t, &unique, 0));
|
||||
new_data = extracts_hold ? alternative
|
||||
: sn_module_add_mux(target, sn_vec_at(sn_obj_id_t, &conditions, 0), alternative,
|
||||
sn_obj_dup(source, old_default), NULL);
|
||||
}
|
||||
else
|
||||
{
|
||||
sn_vec_t alternatives;
|
||||
sn_vec_init(&alternatives);
|
||||
for (size_t k = 0; k < unique.size; k++)
|
||||
*sn_vec_push(sn_obj_id_t, &alternatives) = sn_obj_dup(source, sn_vec_at(sn_obj_id_t, &unique, k));
|
||||
sn_obj_id_t packed_select =
|
||||
sn_module_add_concat(target, (uint32_t)conditions.size, sn_vec_data(sn_obj_id_t, &conditions), NULL);
|
||||
sn_obj_id_t packed_data =
|
||||
sn_module_add_concat(target, (uint32_t)alternatives.size, sn_vec_data(sn_obj_id_t, &alternatives), NULL);
|
||||
sn_obj_id_t default_data = extracts_hold ? sn_vec_at(sn_obj_id_t, &alternatives, alternatives.size - 1)
|
||||
: sn_obj_dup(source, old_default);
|
||||
new_data = sn_module_add_pmux(target, packed_select, packed_data, default_data, NULL);
|
||||
sn_vec_destroy(&alternatives);
|
||||
}
|
||||
sn_obj_connect(target, new_in, 0, new_data);
|
||||
if (extracts_hold)
|
||||
{
|
||||
sn_obj_id_t update =
|
||||
sn_share_or(target, sn_vec_data(sn_obj_id_t, &conditions), (uint32_t)conditions.size);
|
||||
sn_obj_id_t enable = sn_obj_fanin(target, new_reg, SN_REG_ENABLE);
|
||||
if (enable != SN_INVALID_ID)
|
||||
{
|
||||
sn_obj_id_t fanins[2] = {enable, update};
|
||||
update = sn_module_add_operator(target, SN_BIT_AND, 1, false, 2, fanins, NULL);
|
||||
}
|
||||
sn_reg_set_fanin(target, new_reg, SN_REG_ENABLE, update);
|
||||
}
|
||||
stats->registers++;
|
||||
stats->muxes++;
|
||||
stats->paths_before += before;
|
||||
stats->paths_after += after;
|
||||
sn_vec_destroy(&words);
|
||||
sn_vec_destroy(&unique);
|
||||
sn_vec_destroy(&unique_hashes);
|
||||
sn_vec_destroy(&unique_links);
|
||||
sn_vec_destroy(&conditions);
|
||||
sn_vec_destroy(&members);
|
||||
free(member_links);
|
||||
free(member_heads);
|
||||
free(buckets);
|
||||
return true;
|
||||
}
|
||||
|
||||
static inline void sn_share_replace_module(sn_design_t* design, sn_module_id_t old_id, sn_module_id_t new_id)
|
||||
{
|
||||
assert(new_id + 1 == design->modules.size && old_id != new_id);
|
||||
sn_module_t* old_module = sn_design_get_module(design, old_id);
|
||||
sn_module_t* new_module = sn_design_get_module(design, new_id);
|
||||
sn_name_id_t temporary_name_id = new_module->name;
|
||||
sn_name_id_t name = old_module->name;
|
||||
bool interface_locked = old_module->interface_locked;
|
||||
sn_design_invalidate_copies_to_module(design, old_id);
|
||||
sn_module_destroy(old_module);
|
||||
free(old_module);
|
||||
new_module->id = old_id;
|
||||
new_module->name = name;
|
||||
new_module->interface_locked = interface_locked;
|
||||
sn_vec_at(sn_module_t*, &design->modules, old_id) = new_module;
|
||||
design->modules.size--;
|
||||
sn_name_remove_last(&design->names, temporary_name_id);
|
||||
}
|
||||
|
||||
static inline bool sn_share_module_has_candidate(const sn_module_t* module, sn_share_options_t options)
|
||||
{
|
||||
for (size_t i = 0; i < module->type_objects[SN_REG_OUT].size; i++)
|
||||
{
|
||||
sn_obj_id_t reg = sn_vec_at(sn_obj_id_t, &module->type_objects[SN_REG_OUT], i);
|
||||
if (sn_obj_width(module, reg) < options.min_width)
|
||||
continue;
|
||||
sn_obj_id_t root = sn_obj_fanin(module, sn_obj_pair_in(module, reg), 0);
|
||||
if (root == SN_INVALID_ID)
|
||||
continue;
|
||||
root = sn_share_strip_value(module, root);
|
||||
if (sn_obj_type(module, root) == SN_MUX)
|
||||
return true;
|
||||
if (sn_obj_type(module, root) == SN_PMUX)
|
||||
{
|
||||
sn_obj_id_t select = sn_obj_fanin(module, root, SN_PMUX_SELECT);
|
||||
sn_obj_id_t alternatives = sn_obj_fanin(module, root, SN_PMUX_ALTERNATIVES);
|
||||
uint32_t count = sn_obj_width(module, select);
|
||||
if (count >= options.min_alternatives &&
|
||||
(uint64_t)count * sn_obj_width(module, root) == sn_obj_width(module, alternatives))
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
static inline bool sn_design_share_module(sn_design_t* design, sn_module_id_t module_id,
|
||||
sn_share_options_t options, sn_share_stats_t* stats)
|
||||
{
|
||||
sn_module_t* source = sn_design_get_module(design, module_id);
|
||||
if (!sn_share_module_has_candidate(source, options))
|
||||
return false;
|
||||
char name[96];
|
||||
uint32_t suffix = 0;
|
||||
do
|
||||
{
|
||||
int length = snprintf(name, sizeof(name), "__sn_share_%u_%u", module_id, suffix++);
|
||||
assert(length > 0 && (size_t)length < sizeof(name) && suffix != 0);
|
||||
(void)length;
|
||||
} while (sn_name_find(&design->names, name) != SN_INVALID_ID);
|
||||
sn_module_id_t target_id = sn_design_dup_module_topo(design, module_id, name);
|
||||
sn_module_t* target = sn_design_get_module(design, target_id);
|
||||
uint64_t* hashes = sn_share_value_hashes(source);
|
||||
bool changed = false;
|
||||
for (size_t i = 0; i < source->type_objects[SN_REG_OUT].size; i++)
|
||||
{
|
||||
sn_obj_id_t reg = sn_vec_at(sn_obj_id_t, &source->type_objects[SN_REG_OUT], i);
|
||||
bool reg_changed = sn_share_reg_mux_tree(target, source, reg, hashes, options, stats);
|
||||
if (!reg_changed)
|
||||
reg_changed = sn_share_reg_pmux(target, source, reg, hashes, options, stats);
|
||||
changed |= reg_changed;
|
||||
}
|
||||
free(hashes);
|
||||
if (!changed)
|
||||
{
|
||||
sn_name_id_t temporary_name_id = target->name;
|
||||
sn_module_destroy(target);
|
||||
free(target);
|
||||
design->modules.size--;
|
||||
sn_name_remove_last(&design->names, temporary_name_id);
|
||||
sn_vec_destroy(&source->copy_ids);
|
||||
sn_vec_init(&source->copy_ids);
|
||||
source->copy_module = SN_INVALID_ID;
|
||||
return false;
|
||||
}
|
||||
sn_share_replace_module(design, module_id, target_id);
|
||||
// Do not use observable-cone cleanup here: even a constant or externally unobservable register is part of the
|
||||
// canonical transition interface used by pre/post CEC. Reordering preserves every pair and its type ID. Dangling
|
||||
// mux objects retained by this first implementation are harmless because hierarchical blasting is demand-driven.
|
||||
sn_design_reorder_module_topo(design, module_id);
|
||||
stats->modules++;
|
||||
return true;
|
||||
}
|
||||
|
||||
static inline sn_share_stats_t sn_design_share(sn_design_t* design, sn_share_options_t options)
|
||||
{
|
||||
assert(design && sn_design_is_topo(design));
|
||||
sn_share_stats_t stats = {0};
|
||||
size_t module_count = design->modules.size;
|
||||
for (sn_module_id_t module = 0; module < module_count; module++)
|
||||
sn_design_share_module(design, module, options, &stats);
|
||||
assert(design->modules.size == module_count && sn_design_is_topo(design));
|
||||
return stats;
|
||||
}
|
||||
|
||||
ABC_NAMESPACE_HEADER_END
|
||||
|
||||
#endif
|
||||
|
|
@ -0,0 +1,148 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [snPth.h]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [New word-level design interface.]
|
||||
|
||||
Synopsis [Bounded worker support for parallel SN mapping jobs.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: snPth.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#ifndef SN_PTH_H
|
||||
#define SN_PTH_H
|
||||
|
||||
// Small self-contained pthread scheduler for SN passes. The requested process count includes the coordinating caller,
|
||||
// so P > 1 creates exactly P-1 workers. Windows and builds without ABC_USE_PTHREADS compile this scheduler as a
|
||||
// sequential loop, avoiding any SN dependency on pthreads while retaining full P=1 functionality.
|
||||
|
||||
#include <assert.h>
|
||||
#include <stddef.h>
|
||||
#include <stdlib.h>
|
||||
|
||||
#if defined(ABC_USE_PTHREADS) && !defined(_WIN32)
|
||||
#define SN_PTH_USE_THREADS 1
|
||||
#include <pthread.h>
|
||||
#else
|
||||
#define SN_PTH_USE_THREADS 0
|
||||
#endif
|
||||
|
||||
ABC_NAMESPACE_HEADER_START
|
||||
|
||||
typedef void (*sn_pth_job_fn)(void* context, void* job);
|
||||
|
||||
typedef struct sn_pth_pool_t
|
||||
{
|
||||
void** jobs;
|
||||
size_t count;
|
||||
size_t next;
|
||||
void* context;
|
||||
sn_pth_job_fn function;
|
||||
#if SN_PTH_USE_THREADS
|
||||
pthread_mutex_t mutex;
|
||||
#endif
|
||||
} sn_pth_pool_t;
|
||||
|
||||
#if SN_PTH_USE_THREADS
|
||||
static inline void* sn_pth_worker(void* argument)
|
||||
{
|
||||
sn_pth_pool_t* pool = (sn_pth_pool_t*)argument;
|
||||
for (;;)
|
||||
{
|
||||
size_t index;
|
||||
int status = pthread_mutex_lock(&pool->mutex);
|
||||
if (status != 0)
|
||||
return NULL;
|
||||
index = pool->next++;
|
||||
status = pthread_mutex_unlock(&pool->mutex);
|
||||
assert(status == 0);
|
||||
(void)status;
|
||||
if (index >= pool->count)
|
||||
return NULL;
|
||||
pool->function(pool->context, pool->jobs[index]);
|
||||
}
|
||||
}
|
||||
#endif
|
||||
|
||||
static inline int sn_pth_parallel_available(void)
|
||||
{
|
||||
return SN_PTH_USE_THREADS;
|
||||
}
|
||||
|
||||
static inline void sn_pth_process(void** jobs, size_t count, unsigned processes,
|
||||
sn_pth_job_fn function, void* context)
|
||||
{
|
||||
assert((jobs || count == 0) && processes >= 1 && function);
|
||||
#if !SN_PTH_USE_THREADS
|
||||
(void)processes;
|
||||
for (size_t i = 0; i < count; i++)
|
||||
function(context, jobs[i]);
|
||||
#else
|
||||
if (processes == 1 || count < 2)
|
||||
{
|
||||
for (size_t i = 0; i < count; i++)
|
||||
function(context, jobs[i]);
|
||||
return;
|
||||
}
|
||||
unsigned worker_count = processes - 1;
|
||||
if (worker_count > count)
|
||||
worker_count = (unsigned)count;
|
||||
sn_pth_pool_t pool;
|
||||
pool.jobs = jobs;
|
||||
pool.count = count;
|
||||
pool.next = 0;
|
||||
pool.context = context;
|
||||
pool.function = function;
|
||||
int status = pthread_mutex_init(&pool.mutex, NULL);
|
||||
if (status != 0)
|
||||
{
|
||||
for (size_t i = 0; i < count; i++)
|
||||
function(context, jobs[i]);
|
||||
return;
|
||||
}
|
||||
pthread_t* workers = (pthread_t*)malloc(sizeof(pthread_t) * worker_count);
|
||||
if (!workers)
|
||||
{
|
||||
status = pthread_mutex_destroy(&pool.mutex);
|
||||
assert(status == 0);
|
||||
(void)status;
|
||||
for (size_t i = 0; i < count; i++)
|
||||
function(context, jobs[i]);
|
||||
return;
|
||||
}
|
||||
unsigned created = 0;
|
||||
for (; created < worker_count; created++)
|
||||
{
|
||||
if (pthread_create(&workers[created], NULL, sn_pth_worker, &pool) != 0)
|
||||
break;
|
||||
}
|
||||
for (unsigned i = 0; i < created; i++)
|
||||
{
|
||||
int status = pthread_join(workers[i], NULL);
|
||||
assert(status == 0);
|
||||
(void)status;
|
||||
}
|
||||
// A worker that could not use the mutex leaves its unclaimed suffix for the coordinator.
|
||||
while (pool.next < count)
|
||||
function(context, jobs[pool.next++]);
|
||||
status = pthread_mutex_destroy(&pool.mutex);
|
||||
assert(status == 0);
|
||||
(void)status;
|
||||
free(workers);
|
||||
#endif
|
||||
}
|
||||
|
||||
#undef SN_PTH_USE_THREADS
|
||||
|
||||
ABC_NAMESPACE_HEADER_END
|
||||
|
||||
#endif
|
||||
|
|
@ -0,0 +1,137 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [snTech.h]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [New word-level design interface.]
|
||||
|
||||
Synopsis [Target-technology descriptions for SN mapping passes.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: snTech.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#ifndef SN_TECH_H
|
||||
#define SN_TECH_H
|
||||
|
||||
// Technology-independent descriptions used by the SN memory and DSP mappers.
|
||||
// These describe legal primitive configurations and mapping costs; they do not
|
||||
// describe device placement or the total number of resources on a die.
|
||||
|
||||
#include <stdbool.h>
|
||||
#include <stddef.h>
|
||||
#include <stdint.h>
|
||||
|
||||
#include "misc/util/abc_namespaces.h"
|
||||
|
||||
ABC_NAMESPACE_HEADER_START
|
||||
|
||||
typedef enum sn_mem_port_mode_t
|
||||
{
|
||||
SN_MEM_PORT_SINGLE = 0,
|
||||
SN_MEM_PORT_SIMPLE_DUAL,
|
||||
SN_MEM_PORT_TRUE_DUAL
|
||||
} sn_mem_port_mode_t;
|
||||
|
||||
typedef enum sn_mem_read_write_mode_t
|
||||
{
|
||||
SN_MEM_READ_WRITE_NO_CHANGE = 0,
|
||||
SN_MEM_READ_WRITE_READ_FIRST,
|
||||
SN_MEM_READ_WRITE_WRITE_FIRST
|
||||
} sn_mem_read_write_mode_t;
|
||||
|
||||
typedef struct sn_mem_tech_t
|
||||
{
|
||||
const char* name;
|
||||
uint32_t cap_bits;
|
||||
uint32_t address_bits;
|
||||
const uint32_t* widths;
|
||||
size_t width_count;
|
||||
sn_mem_port_mode_t port_mode;
|
||||
uint32_t byte_width;
|
||||
bool synchronous_read;
|
||||
bool has_clock_enable;
|
||||
bool has_byte_enable;
|
||||
bool supports_init;
|
||||
bool supports_read_first;
|
||||
bool supports_write_first;
|
||||
bool supports_no_change;
|
||||
uint32_t mapping_cost;
|
||||
const uint32_t* simple_dual_widths;
|
||||
size_t simple_dual_width_count;
|
||||
} sn_mem_tech_t;
|
||||
|
||||
typedef struct sn_dsp_tech_t
|
||||
{
|
||||
const char* name;
|
||||
uint32_t a_width;
|
||||
uint32_t b_width;
|
||||
uint32_t p_width;
|
||||
uint32_t preadder_width;
|
||||
uint32_t min_a_width;
|
||||
uint32_t min_b_width;
|
||||
uint32_t min_p_width;
|
||||
bool signed_only;
|
||||
bool has_preadder;
|
||||
bool has_postadder;
|
||||
bool has_simd;
|
||||
bool has_cascade;
|
||||
uint32_t max_cascade_length;
|
||||
uint32_t latency;
|
||||
uint32_t mapping_cost;
|
||||
} sn_dsp_tech_t;
|
||||
|
||||
typedef struct sn_carry_tech_t
|
||||
{
|
||||
const char* name;
|
||||
uint32_t width;
|
||||
uint32_t min_op_width;
|
||||
uint32_t mapping_cost;
|
||||
} sn_carry_tech_t;
|
||||
|
||||
typedef struct sn_tech_t
|
||||
{
|
||||
const sn_mem_tech_t* memories;
|
||||
size_t memory_count;
|
||||
const sn_dsp_tech_t* dsps;
|
||||
size_t dsp_count;
|
||||
const sn_carry_tech_t* carries;
|
||||
size_t carry_count;
|
||||
} sn_tech_t;
|
||||
|
||||
// AMD/Xilinx UltraScale+ primitives used by the initial mapper. Width lists
|
||||
// follow the legal BRAM/URAM port widths in the Yosys Xilinx memory library.
|
||||
static inline sn_tech_t sn_tech_xilinx_ultrascale(void)
|
||||
{
|
||||
static const uint32_t bram18_widths[] = {1, 2, 4, 9, 18};
|
||||
static const uint32_t bram36_widths[] = {1, 2, 4, 9, 18, 36};
|
||||
static const uint32_t bram18_sdp_widths[] = {1, 2, 4, 9, 18, 36};
|
||||
static const uint32_t bram36_sdp_widths[] = {1, 2, 4, 9, 18, 36, 72};
|
||||
static const uint32_t uram_widths[] = {72, 144};
|
||||
static const sn_mem_tech_t memories[] = {
|
||||
{"RAMB18E2", 18u * 1024u, 14, bram18_widths, 5, SN_MEM_PORT_TRUE_DUAL, 9, true, true, true, true, true,
|
||||
true, true, 129, bram18_sdp_widths, 6},
|
||||
{"RAMB36E2", 36u * 1024u, 15, bram36_widths, 6, SN_MEM_PORT_TRUE_DUAL, 9, true, true, true, true, true,
|
||||
true, true, 257, bram36_sdp_widths, 7},
|
||||
{"URAM288", 288u * 1024u, 12, uram_widths, 2, SN_MEM_PORT_TRUE_DUAL, 9, true, true, true, true, false,
|
||||
true, true, 1024, NULL, 0},
|
||||
};
|
||||
static const sn_dsp_tech_t dsps[] = {
|
||||
{"DSP48E2", 27, 18, 48, 27, 2, 2, 9, true, true, true, true, true, 20, 0, 1},
|
||||
};
|
||||
static const sn_carry_tech_t carries[] = {{"CARRY4", 4, 3, 1}};
|
||||
sn_tech_t result = {memories, sizeof(memories) / sizeof(memories[0]), dsps, sizeof(dsps) / sizeof(dsps[0]),
|
||||
carries, sizeof(carries) / sizeof(carries[0])};
|
||||
return result;
|
||||
}
|
||||
|
||||
ABC_NAMESPACE_HEADER_END
|
||||
|
||||
#endif
|
||||
|
|
@ -482,6 +482,11 @@ private:
|
|||
for ( uint32_t i = 0; i < num_vars; ++i )
|
||||
{
|
||||
pComb[i] = pInvPerm[i] = i;
|
||||
/* bestPerm is written only when some combination beats the initial
|
||||
* best_cost. When none does, the loop below still evaluates
|
||||
* permutations[bestPerm[i]], which reads uninitialised stack and then
|
||||
* indexes permutations[] with it. Seed the identity permutation. */
|
||||
bestPerm[i] = i;
|
||||
}
|
||||
|
||||
/* early bail-out conditions */
|
||||
|
|
@ -1317,7 +1322,10 @@ private:
|
|||
{
|
||||
auto mask = *tt.begin();
|
||||
|
||||
for ( auto i = real_num_vars; i < num_vars; ++i )
|
||||
/* Replicate within the word only. Variables 6 and above are replicated by the
|
||||
* std::fill below, and shifting a 64-bit word by (1 << i) for i >= 6 is undefined
|
||||
* behaviour rather than a no-op. */
|
||||
for ( auto i = real_num_vars; i < std::min( num_vars, 6u ); ++i )
|
||||
{
|
||||
mask |= ( mask << ( 1 << i ) );
|
||||
}
|
||||
|
|
|
|||
|
|
@ -121,9 +121,8 @@ namespace eSLIM {
|
|||
}
|
||||
|
||||
std::vector<bool> DelayEngine::reduceDelay(unsigned int max_size, unsigned int initial_delay) {
|
||||
assert (delay_selectors.find(initial_delay) != delay_selectors.end());
|
||||
std::vector<bool> last_model;
|
||||
for( auto it = delay_selectors.find(initial_delay); it != delay_selectors.end(); ++it ) {
|
||||
for( auto it = delay_selectors.lower_bound(initial_delay); it != delay_selectors.end(); ++it ) {
|
||||
int d = it->first;
|
||||
double timeout = getDynamicTimeout(max_size);
|
||||
int status = existsReplacement(max_size, d, timeout);
|
||||
|
|
|
|||
|
|
@ -202,6 +202,24 @@ pMan->timeEvalMuxAn += Abc_Clock() - clk;
|
|||
assert( pResMux == NULL || pResDsd == NULL );
|
||||
if ( pResMux )
|
||||
{
|
||||
// Lpk_MuxAnalize() decides feasibility from the cached cofactor supports in
|
||||
// p->puSupps. Those may have come from Lpk_ComputeSupports(), which derives
|
||||
// them from two BDDs built in opposite variable orders and stitches the halves
|
||||
// together, and that estimate can be a strict SUBSET of the true cofactor
|
||||
// support. When it is, the component retained by the split below ends up with
|
||||
// no vacant fanin slot for the component that is split off, and Lpk_MuxSplit()
|
||||
// fails its assertion `iVarVac < (int)p->nVars'. Re-derive the one support the
|
||||
// split actually depends on and decline the MUX decomposition if it does not fit.
|
||||
unsigned * pTruthThis = Lpk_FunTruth( p, 0 );
|
||||
unsigned * pTruthCof = Lpk_FunTruth( p, 1 );
|
||||
unsigned uSuppExact;
|
||||
if ( pResMux->Polarity )
|
||||
Kit_TruthCofactor1New( pTruthCof, pTruthThis, p->nVars, pResMux->Variable );
|
||||
else
|
||||
Kit_TruthCofactor0New( pTruthCof, pTruthThis, p->nVars, pResMux->Variable );
|
||||
uSuppExact = Kit_TruthSupport( pTruthCof, p->nVars ) | ( 1 << pResMux->Variable );
|
||||
if ( Kit_WordCountOnes( uSuppExact ) >= (int)p->nVars )
|
||||
return 0;
|
||||
clk = Abc_Clock();
|
||||
p2 = Lpk_MuxSplit( pMan, p, pResMux->Variable, pResMux->Polarity );
|
||||
pMan->timeEvalMuxSp += Abc_Clock() - clk;
|
||||
|
|
|
|||
Loading…
Reference in New Issue