From 59fe3268a788722dcae9615e014270fe8be3599b Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 19 Feb 2013 23:07:29 -0800 Subject: Adding STG generation (&era -d) and STG encoding (&read_stg ). --- src/aig/gia/gia.h | 3 + src/aig/gia/giaEra.c | 56 +++++++++-- src/aig/gia/giaStg.c | 247 ++++++++++++++++++++++++++++++++++++++++++++++++ src/aig/gia/module.make | 1 + 4 files changed, 299 insertions(+), 8 deletions(-) create mode 100644 src/aig/gia/giaStg.c (limited to 'src/aig/gia') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 62c97051..07a839ae 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -966,6 +966,9 @@ extern int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * extern float Gia_ManDelayTraceLut( Gia_Man_t * p ); extern float Gia_ManDelayTraceLutPrint( Gia_Man_t * p, int fVerbose ); extern Gia_Man_t * Gia_ManSpeedup( Gia_Man_t * p, int Percentage, int Degree, int fVerbose, int fVeryVerbose ); +/*=== giaStg.c ============================================================*/ +extern void Gia_ManStgPrint( FILE * pFile, Vec_Int_t * vLines, int nIns, int nOuts, int nStates ); +extern Gia_Man_t * Gia_ManStgRead( char * pFileName, int fOneHot, int fLogar ); /*=== giaSweep.c ============================================================*/ extern Gia_Man_t * Gia_ManFraigSweep( Gia_Man_t * p, void * pPars ); /*=== giaSwitch.c ============================================================*/ diff --git a/src/aig/gia/giaEra.c b/src/aig/gia/giaEra.c index 21a693da..8f0e2b07 100644 --- a/src/aig/gia/giaEra.c +++ b/src/aig/gia/giaEra.c @@ -52,6 +52,7 @@ struct Gia_ManEra_t_ Gia_ObjEra_t * pStateNew; // temporary state int iCurState; // the current state Vec_Int_t * vBugTrace; // the sequence of transitions + Vec_Int_t * vStgDump; // STG written into a file // hash table for states int nBins; unsigned * pBins; @@ -102,6 +103,7 @@ Gia_ManEra_t * Gia_ManEraCreate( Gia_Man_t * pAig ) // assign constant zero node pSimInfo = Gia_ManEraData( p, 0 ); memset( pSimInfo, 0, sizeof(unsigned) * p->nWordsSim ); + p->vStgDump = Vec_IntAlloc( 1000 ); return p; } @@ -119,6 +121,7 @@ Gia_ManEra_t * Gia_ManEraCreate( Gia_Man_t * pAig ) void Gia_ManEraFree( Gia_ManEra_t * p ) { Mem_FixedStop( p->pMemory, 0 ); + Vec_IntFree( p->vStgDump ); Vec_PtrFree( p->vStates ); if ( p->vBugTrace ) Vec_IntFree( p->vBugTrace ); ABC_FREE( p->pDataSim ); @@ -195,14 +198,20 @@ int Gia_ManEraStateHash( unsigned * pState, int nWordsSim, int nTableSize ) SeeAlso [] ***********************************************************************/ -static inline unsigned * Gia_ManEraHashFind( Gia_ManEra_t * p, Gia_ObjEra_t * pState ) +static inline unsigned * Gia_ManEraHashFind( Gia_ManEra_t * p, Gia_ObjEra_t * pState, int * pStateNum ) { Gia_ObjEra_t * pThis; unsigned * pPlace = p->pBins + Gia_ManEraStateHash( pState->pData, p->nWordsDat, p->nBins ); for ( pThis = (*pPlace)? Gia_ManEraState(p, *pPlace) : NULL; pThis; pPlace = (unsigned *)&pThis->iNext, pThis = (*pPlace)? Gia_ManEraState(p, *pPlace) : NULL ) if ( !memcmp( pState->pData, pThis->pData, sizeof(unsigned) * p->nWordsDat ) ) + { + if ( pStateNum ) + *pStateNum = pThis->Num; return NULL; + } + if ( pStateNum ) + *pStateNum = -1; return pPlace; } @@ -238,7 +247,7 @@ void Gia_ManEraHashResize( Gia_ManEra_t * p ) { assert( pThis->Num ); pThis->iNext = 0; - piPlace = Gia_ManEraHashFind( p, pThis ); + piPlace = Gia_ManEraHashFind( p, pThis, NULL ); assert( *piPlace == 0 ); // should not be there *piPlace = pThis->Num; Counter++; @@ -437,11 +446,11 @@ int Gia_ManCountDepth( Gia_ManEra_t * p ) SeeAlso [] ***********************************************************************/ -int Gia_ManAnalyzeResult( Gia_ManEra_t * p, Gia_ObjEra_t * pState, int fMiter ) +int Gia_ManAnalyzeResult( Gia_ManEra_t * p, Gia_ObjEra_t * pState, int fMiter, int fStgDump ) { Gia_Obj_t * pObj; - unsigned * pSimInfo, * piPlace; - int i, k, iCond, nMints; + unsigned * pSimInfo, * piPlace, uOutput = 0; + int i, k, iCond, nMints, iNextState; // check if the miter is asserted if ( fMiter ) { @@ -468,9 +477,27 @@ int Gia_ManAnalyzeResult( Gia_ManEra_t * p, Gia_ObjEra_t * pState, int fMiter ) if ( Abc_InfoHasBit(p->pStateNew->pData, i) != Abc_InfoHasBit(pSimInfo, k) ) Abc_InfoXorBit( p->pStateNew->pData, i ); } - piPlace = Gia_ManEraHashFind( p, p->pStateNew ); + if ( fStgDump ) + { + uOutput = 0; + Gia_ManForEachPo( p->pAig, pObj, i ) + { + pSimInfo = Gia_ManEraData( p, Gia_ObjId(p->pAig, pObj) ); + if ( Abc_InfoHasBit(pSimInfo, k) && i < 32 ) + Abc_InfoXorBit( &uOutput, i ); + } + } + piPlace = Gia_ManEraHashFind( p, p->pStateNew, &iNextState ); + if ( fStgDump ) Vec_IntPush( p->vStgDump, k ); + if ( fStgDump ) Vec_IntPush( p->vStgDump, pState->Num ); if ( piPlace == NULL ) + { + if ( fStgDump ) Vec_IntPush( p->vStgDump, iNextState ); + if ( fStgDump ) Vec_IntPush( p->vStgDump, uOutput ); continue; + } + if ( fStgDump ) Vec_IntPush( p->vStgDump, p->pStateNew->Num ); + if ( fStgDump ) Vec_IntPush( p->vStgDump, uOutput ); //printf( "Inserting %d ", Vec_PtrSize(p->vStates) ); //Extra_PrintBinary( stdout, p->pStateNew->pData, Gia_ManRegNum(p->pAig) ); printf( "\n" ); assert( *piPlace == 0 ); @@ -497,7 +524,7 @@ int Gia_ManAnalyzeResult( Gia_ManEra_t * p, Gia_ObjEra_t * pState, int fMiter ) SeeAlso [] ***********************************************************************/ -int Gia_ManCollectReachable( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbose ) +int Gia_ManCollectReachable( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fDumpFile, int fVerbose ) { Gia_ManEra_t * p; Gia_ObjEra_t * pState; @@ -531,7 +558,7 @@ int Gia_ManCollectReachable( Gia_Man_t * pAig, int nStatesMax, int fMiter, int f //Extra_PrintBinary( stdout, p->pStateNew->pData, Gia_ManRegNum(p->pAig) ); printf( "\n" ); Gia_ManInsertState( p, pState ); Gia_ManPerformOneIter( p ); - if ( Gia_ManAnalyzeResult( p, pState, fMiter ) && fMiter ) + if ( Gia_ManAnalyzeResult( p, pState, fMiter, fDumpFile ) && fMiter ) { RetValue = 0; printf( "Miter failed in state %d after %d transitions. ", @@ -549,6 +576,19 @@ int Gia_ManCollectReachable( Gia_Man_t * pAig, int nStatesMax, int fMiter, int f } printf( "Reachability analysis traversed %d states with depth %d. ", p->iCurState-1, Gia_ManCountDepth(p) ); ABC_PRT( "Time", clock() - clk ); + if ( fDumpFile ) + { + char * pFileName = "test.stg"; + FILE * pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + printf( "Cannot open file \"%s\" for writing.\n", pFileName ); + else + { + Gia_ManStgPrint( pFile, p->vStgDump, Gia_ManPiNum(pAig), Gia_ManPoNum(pAig), p->iCurState-1 ); + fclose( pFile ); + printf( "Extracted STG was written into file \"%s\".\n", pFileName ); + } + } Gia_ManEraFree( p ); return RetValue; } diff --git a/src/aig/gia/giaStg.c b/src/aig/gia/giaStg.c new file mode 100644 index 00000000..80f12530 --- /dev/null +++ b/src/aig/gia/giaStg.c @@ -0,0 +1,247 @@ +/**CFile**************************************************************** + + FileName [gia.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: gia.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" +#include "misc/extra/extra.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManStgOneHot( Vec_Int_t * vLines, int nIns, int nOuts, int nStates ) +{ + Gia_Man_t * p; + Vec_Int_t * vInMints, * vCurs, * vOuts, * vNexts; + int i, b, LitC, Lit; + assert( Vec_IntSize(vLines) % 4 == 0 ); + + // start manager + p = Gia_ManStart( 10000 ); + p->pName = Abc_UtilStrsav( "stg" ); + for ( i = 0; i < nIns + nStates; i++ ) + Gia_ManAppendCi(p); + + // create input minterms + Gia_ManHashAlloc( p ); + vInMints = Vec_IntAlloc( 1 << nIns ); + for ( i = 0; i < (1 << nIns); i++ ) + { + for ( Lit = 1, b = 0; b < nIns; b++ ) + Lit = Gia_ManHashAnd( p, Lit, Abc_Var2Lit( b+1, !((i >> b) & 1) ) ); + Vec_IntPush( vInMints, Lit ); + } + + // create current states + vCurs = Vec_IntAlloc( nStates ); + for ( i = 0; i < nStates; i++ ) + Vec_IntPush( vCurs, Abc_Var2Lit( 1+nIns+i, !i ) ); + + // start outputs and current states + vOuts = Vec_IntStart( nOuts ); + vNexts = Vec_IntStart( nStates ); + + // go through the lines + for ( i = 0; i < Vec_IntSize(vLines); ) + { + int iMint = Vec_IntEntry(vLines, i++); + int iCur = Vec_IntEntry(vLines, i++) - 1; + int iNext = Vec_IntEntry(vLines, i++) - 1; + int iOut = Vec_IntEntry(vLines, i++); + assert( iMint >= 0 && iMint < (1<= 0 && iCur < nStates ); + assert( iNext >= 0 && iNext < nStates ); + assert( iOut >= 0 && iOut < (1<> b) & 1 ) + { + Lit = Gia_ManHashOr( p, LitC, Vec_IntEntry(vOuts, b) ); + Vec_IntWriteEntry( vOuts, b, Lit ); + } + } + + // create POs + Vec_IntForEachEntry( vOuts, Lit, i ) + Gia_ManAppendCo( p, Lit ); + + // create next states + Vec_IntForEachEntry( vNexts, Lit, i ) + Gia_ManAppendCo( p, Abc_LitNotCond(Lit, !i) ); + + Gia_ManSetRegNum( p, nStates ); + Gia_ManHashStop( p ); + + Vec_IntFree( vInMints ); + Vec_IntFree( vCurs ); + Vec_IntFree( vOuts ); + Vec_IntFree( vNexts ); + + assert( !Gia_ManHasDangling(p) ); + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManStgPrint( FILE * pFile, Vec_Int_t * vLines, int nIns, int nOuts, int nStates ) +{ + int i, nDigits = Abc_Base10Log( nStates ); + assert( Vec_IntSize(vLines) % 4 == 0 ); + for ( i = 0; i < Vec_IntSize(vLines); i += 4 ) + { + int iMint = Vec_IntEntry(vLines, i ); + int iCur = Vec_IntEntry(vLines, i+1) - 1; + int iNext = Vec_IntEntry(vLines, i+2) - 1; + int iOut = Vec_IntEntry(vLines, i+3); + assert( iMint >= 0 && iMint < (1<= 0 && iCur < nStates ); + assert( iNext >= 0 && iNext < nStates ); + assert( iOut >= 0 && iOut < (1<