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

Procedure to dump ZDD representing a set of cubes into a PLA file.

This commit is contained in:
Alan Mishchenko 2015-04-10 21:30:53 +09:00
parent b6b9d284c4
commit dff6e2ab31
2 changed files with 40 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/misc/extra/extraBdd.h
View File

@ -196,6 +196,7 @@ extern DdNode * extraBddChangePolarity( DdManager * dd, DdNode * bFunc, DdNo
extern int Extra_bddVarIsInCube( DdNode * bCube, int iVar );
extern DdNode * Extra_bddAndPermute( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute );
extern int Extra_bddCountCubes( DdManager * dd, DdNode ** pFuncs, int nFuncs, int fMode, int nLimit, int * pGuide );
extern void Extra_zddDumpPla( DdManager * dd, DdNode * zCover, int nVars, char * pFileName );
#ifndef ABC_PRB
#define ABC_PRB(dd,f) printf("%s = ", #f); Extra_bddPrint(dd,f); printf("\n")

39
src/misc/extra/extraBddMisc.c
View File

@ -2293,6 +2293,45 @@ printf( "|F| =%6d |G| =%6d |H| =%6d |F|*|G| =%9d ",
Cudd_AutodynEnable( ddF, CUDD_REORDER_SYMM_SIFT );
}
/**Function*************************************************************
Synopsis [Writes ZDD into a PLA file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Extra_zddDumpPla( DdManager * dd, DdNode * F, int nVars, char * pFileName )
{
DdGen *gen;
char * pCube;
int * pPath, i;
FILE * pFile = fopen( pFileName, "wb" );
if ( pFile == NULL )
{
printf( "Cannot open file \"%s\" for writing.\n", pFileName );
return;
}
fprintf( pFile, "# PLA file dumped by Extra_zddDumpPla() in ABC\n" );
fprintf( pFile, ".i %d\n", nVars );
fprintf( pFile, ".o 1\n" );
pCube = ABC_CALLOC( char, dd->sizeZ );
Cudd_zddForeachPath( dd, F, gen, pPath )
{
for ( i = 0; i < nVars; i++ )
pCube[i] = '-';
for ( i = 0; i < nVars; i++ )
if ( pPath[2*i] == 1 || pPath[2*i+1] == 1 )
pCube[i] = '0' + (pPath[2*i] == 1);
fprintf( pFile, "%s 1\n", pCube );
}
fprintf( pFile, ".e\n\n" );
fclose( pFile );
ABC_FREE( pCube );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///