#include "llbInt.h"

Include dependency graph for llb2Dump.c:

Functions
ABC_NAMESPACE_IMPL_START char *	Llb_ManGetDummyName (char *pPrefix, int Num, int nDigits)
	DECLARATIONS ///.

void	Llb_ManDumpReached (DdManager ddG, DdNode bReached, char pModel, char pFileName)

Function Documentation

◆ Llb_ManDumpReached()

void Llb_ManDumpReached	(	DdManager *	ddG,
		DdNode *	bReached,
		char *	pModel,
		char *	pFileName )

Function*************************************************************

Synopsis [Writes reached state BDD into a BLIF file.]

Description []

SideEffects []

SeeAlso []

Definition at line 63 of file llb2Dump.c.

{
    FILE * pFile;
    Vec_Ptr_t * vNamesIn, * vNamesOut;
    char * pName;
    int i, nDigits;
    // reorder the BDD
    Cudd_ReduceHeap( ddG, CUDD_REORDER_SYMM_SIFT, 1 );
 
    // create input names
    nDigits = Abc_Base10Log( Cudd_ReadSize(ddG) );
    vNamesIn = Vec_PtrAlloc( Cudd_ReadSize(ddG) );
    for ( i = 0; i < Cudd_ReadSize(ddG); i++ )
    {
        pName = Llb_ManGetDummyName( "ff", i, nDigits );
        Vec_PtrPush( vNamesIn, Extra_UtilStrsav(pName) );
    }
    // create output names
    vNamesOut = Vec_PtrAlloc( 1 );
    Vec_PtrPush( vNamesOut, Extra_UtilStrsav("Reached") );
 
    // write the file
    pFile = fopen( pFileName, "wb" );
    Cudd_DumpBlif( ddG, 1, &bReached, (char **)Vec_PtrArray(vNamesIn), (char **)Vec_PtrArray(vNamesOut), pModel, pFile, 0 );
    fclose( pFile );
 
    // cleanup
    Vec_PtrForEachEntry( char *, vNamesIn, pName, i )
        ABC_FREE( pName );
    Vec_PtrForEachEntry( char *, vNamesOut, pName, i )
        ABC_FREE( pName );
    Vec_PtrFree( vNamesIn );
    Vec_PtrFree( vNamesOut );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Llb_ManGetDummyName()

ABC_NAMESPACE_IMPL_START char * Llb_ManGetDummyName	(	char *	pPrefix,
		int	Num,
		int	nDigits )

DECLARATIONS ///.

CFile****************************************************************

FileName [llb2Dump.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [BDD based reachability.]

Synopsis [Dumps the BDD of reached states into a file.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id: llb2Dump.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Returns a dummy name.]