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

Add inv_get -f to read flop names from GIA

This commit is contained in:
Tobias Wiersema 2021-08-19 17:23:03 +02:00
parent 4da6cc8904
commit ca710b3dda
2 changed files with 40 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/base/wlc/wlcAbc.c
View File

@ -140,7 +140,7 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vCounts, int fVerbose )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv ) Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Ptr_t * vNamesIn )
{ {
extern Vec_Int_t * Pdr_InvCounts( Vec_Int_t * vInv ); extern Vec_Int_t * Pdr_InvCounts( Vec_Int_t * vInv );
extern Vec_Str_t * Pdr_InvPrintStr( Vec_Int_t * vInv, Vec_Int_t * vCounts ); extern Vec_Str_t * Pdr_InvPrintStr( Vec_Int_t * vInv, Vec_Int_t * vCounts );
@ -166,9 +166,15 @@ Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv )
if ( Entry == 0 ) if ( Entry == 0 )
continue; continue;
pMainObj = Abc_NtkCreatePi( pMainNtk ); pMainObj = Abc_NtkCreatePi( pMainNtk );
if (vNamesIn != NULL && i < Vec_PtrSize(vNamesIn)) {
Abc_ObjAssignName( pMainObj, (char *)Vec_PtrEntry(vNamesIn, i), NULL );
}
else
{
sprintf( Buffer, "pi%d", i ); sprintf( Buffer, "pi%d", i );
Abc_ObjAssignName( pMainObj, Buffer, NULL ); Abc_ObjAssignName( pMainObj, Buffer, NULL );
} }
}
if ( Abc_NtkPiNum(pMainNtk) != nInputs ) if ( Abc_NtkPiNum(pMainNtk) != nInputs )
{ {
printf( "Mismatch between number of inputs and the number of literals in the invariant.\n" ); printf( "Mismatch between number of inputs and the number of literals in the invariant.\n" );

36
src/base/wlc/wlcCom.c
View File

@ -1727,15 +1727,19 @@ usage:
******************************************************************************/ ******************************************************************************/
int Abc_CommandInvGet( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandInvGet( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
extern Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv ); extern Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Ptr_t * vNamesIn );
Abc_Ntk_t * pMainNtk; Abc_Ntk_t * pMainNtk;
Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
int c, fVerbose = 0; int c, i, fVerbose = 0, fFlopNamesFromGia = 0;
Vec_Ptr_t * vNamesIn = NULL;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "fvh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
case 'f':
fFlopNamesFromGia ^= 1;
break;
case 'v': case 'v':
fVerbose ^= 1; fVerbose ^= 1;
break; break;
@ -1750,16 +1754,38 @@ int Abc_CommandInvGet( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "Abc_CommandInvGet(): Invariant is not available.\n" ); Abc_Print( 1, "Abc_CommandInvGet(): Invariant is not available.\n" );
return 0; return 0;
} }
// See if we shall and can copy the PI names from the current GIA
if ( fFlopNamesFromGia )
{
if ( pAbc->pGia == NULL )
{
Abc_Print( 1, "Abc_CommandInvGet(): No network in &-space, cannot copy names.\n" );
fFlopNamesFromGia = 0;
}
else
{
vNamesIn = Vec_PtrStart( Gia_ManRegNum(pAbc->pGia) );
for ( i = 0; i < Gia_ManRegNum(pAbc->pGia); ++i )
{
// Only the registers
Vec_PtrSetEntry( vNamesIn, i, Extra_UtilStrsav( (const char*)Vec_PtrEntry( pAbc->pGia->vNamesIn, Gia_ManPiNum(pAbc->pGia)+i ) ) );
}
}
}
// derive the network // derive the network
pMainNtk = Wlc_NtkGetInv( pNtk, Wlc_AbcGetInv(pAbc) ); pMainNtk = Wlc_NtkGetInv( pNtk, Wlc_AbcGetInv(pAbc), vNamesIn );
// Delete names
if (vNamesIn)
Vec_PtrFree( vNamesIn );
// replace the current network // replace the current network
if ( pMainNtk ) if ( pMainNtk )
Abc_FrameReplaceCurrentNetwork( pAbc, pMainNtk ); Abc_FrameReplaceCurrentNetwork( pAbc, pMainNtk );
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: inv_get [-vh]\n" ); Abc_Print( -2, "usage: inv_get [-fvh]\n" );
Abc_Print( -2, "\t places invariant found by PDR as the current network in the main-space\n" ); Abc_Print( -2, "\t places invariant found by PDR as the current network in the main-space\n" );
Abc_Print( -2, "\t (in the case of \'sat\' or \'undecided\', inifity clauses are used)\n" ); Abc_Print( -2, "\t (in the case of \'sat\' or \'undecided\', inifity clauses are used)\n" );
Abc_Print( -2, "\t-f : toggle reading flop names from the &-space [default = %s]\n", fFlopNamesFromGia? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "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"); Abc_Print( -2, "\t-h : print the command usage\n");
return 1; return 1;