From d2b735f794575ce0f10f01bba1255cf1dc3b8aaf Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 25 Oct 2008 08:01:00 -0700 Subject: Version abc81025 --- src/aig/fra/fraCec.c | 4 + src/aig/ntl/ntl.h | 4 +- src/aig/ntl/ntlEc.c | 1 + src/aig/ntl/ntlReadBlif.c | 2 + src/aig/ntl/ntlReadBlif_old.c | 1261 ----------------------------------------- src/aig/ntl/ntlTable.c | 77 ++- src/aig/nwk/nwkCheck.c | 2 +- src/aig/saig/module.make | 1 + src/aig/saig/saig.h | 1 + src/aig/saig/saigBmc.c | 550 +++++++++++------- src/aig/saig/saigBmc2.c | 314 ++++++++++ src/aig/saig/saigMiter.c | 159 +++++- src/aig/saig/saigSynch.c | 1 + src/aig/ssw/module.make | 1 + src/aig/ssw/ssw.h | 1 + src/aig/ssw/sswClass.c | 52 +- src/aig/ssw/sswInt.h | 1 + src/aig/ssw/sswIslands.c | 382 +++++++++++++ src/aig/ssw/sswPairs.c | 2 + src/base/abci/abc.c | 6 +- src/base/abci/abcMap.c | 2 +- src/map/pcm/module.make | 0 src/map/ply/module.make | 0 23 files changed, 1334 insertions(+), 1490 deletions(-) delete mode 100644 src/aig/ntl/ntlReadBlif_old.c create mode 100644 src/aig/saig/saigBmc2.c create mode 100644 src/aig/ssw/sswIslands.c create mode 100644 src/map/pcm/module.make create mode 100644 src/map/ply/module.make (limited to 'src') diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c index fdf87ccd..190281c9 100644 --- a/src/aig/fra/fraCec.c +++ b/src/aig/fra/fraCec.c @@ -175,7 +175,11 @@ int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose ) RetValue = Fra_FraigMiterStatus( pAig ); // assert( RetValue == -1 ); if ( RetValue >= 0 ) + { + pAig->pData = ALLOC( int, Aig_ManPiNum(pAig) ); + memset( pAig->pData, 0, sizeof(int) * Aig_ManPiNum(pAig) ); return RetValue; + } // if SAT only, solve without iteration clk = clock(); diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h index 5f1f724f..a82157c0 100644 --- a/src/aig/ntl/ntl.h +++ b/src/aig/ntl/ntl.h @@ -139,6 +139,7 @@ struct Ntl_Obj_t_ union { // clock / other data Ntl_Net_t * pClock; // clock (for registers) void * pTemp; // other data + int iTemp; // other data }; Ntl_Net_t * pFanio[0]; // fanins/fanouts }; @@ -149,8 +150,8 @@ struct Ntl_Net_t_ void * pCopy; // the copy of this object union { void * pCopy2; // the copy of this object - int iTemp; // other data float dTemp; // other data + int iTemp; // other data }; Ntl_Obj_t * pDriver; // driver of the net char nVisits; // the number of times the net is visited @@ -352,6 +353,7 @@ extern ABC_DLL int Ntl_ManSweep( Ntl_Man_t * p, int fVerbose ); /*=== ntlTable.c ==========================================================*/ extern ABC_DLL Ntl_Net_t * Ntl_ModelFindNet( Ntl_Mod_t * p, char * pName ); extern ABC_DLL Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName ); +extern ABC_DLL void Ntl_ModelSetPioNumbers( Ntl_Mod_t * p ); extern ABC_DLL int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * pName, int * pNumber ); extern ABC_DLL int Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet ); extern ABC_DLL int Ntl_ModelClearNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet ); diff --git a/src/aig/ntl/ntlEc.c b/src/aig/ntl/ntlEc.c index 4850f647..0d41006e 100644 --- a/src/aig/ntl/ntlEc.c +++ b/src/aig/ntl/ntlEc.c @@ -351,6 +351,7 @@ Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 ) pAig1 = Ntl_ManCollapse( pMan1, 1 ); pAig2 = Ntl_ManCollapse( pMan2, 1 ); pAig = Saig_ManCreateMiter( pAig1, pAig2, 0 ); + Aig_ManCleanup( pAig ); Aig_ManStop( pAig1 ); Aig_ManStop( pAig2 ); // cleanup diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c index 30f972c8..800b711c 100644 --- a/src/aig/ntl/ntlReadBlif.c +++ b/src/aig/ntl/ntlReadBlif.c @@ -745,6 +745,7 @@ static int Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p ) if ( !Ioa_ReadParseLineOutputs( pMod, pLine ) ) return 0; // parse the delay info + Ntl_ModelSetPioNumbers( pMod->pNtk ); Vec_PtrForEachEntry( pMod->vDelays, pLine, k ) if ( !Ioa_ReadParseLineDelay( pMod, pLine ) ) return 0; @@ -954,6 +955,7 @@ static int Ioa_ReadParseLineOutputs( Ioa_ReadMod_t * p, char * pLine ) { pNet = Ntl_ModelFindOrCreateNet( p->pNtk, pToken ); pObj = Ntl_ModelCreatePo( p->pNtk, pNet ); + pNet->pCopy = pObj; } return 1; } diff --git a/src/aig/ntl/ntlReadBlif_old.c b/src/aig/ntl/ntlReadBlif_old.c deleted file mode 100644 index ebfb2a80..00000000 --- a/src/aig/ntl/ntlReadBlif_old.c +++ /dev/null @@ -1,1261 +0,0 @@ -/**CFile**************************************************************** - - FileName [ntlReadBlif.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Command processing package.] - - Synopsis [Procedures to read BLIF file.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 8, 2007.] - - Revision [$Id: ntlReadBlif.c,v 1.00 2007/01/08 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "ntl.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Ioa_ReadMod_t_ Ioa_ReadMod_t; // parsing model -typedef struct Ioa_ReadMan_t_ Ioa_ReadMan_t; // parsing manager - -struct Ioa_ReadMod_t_ -{ - // file lines - char * pFirst; // .model line - char * pAttrib; // .attrib line - Vec_Ptr_t * vInputs; // .inputs lines - Vec_Ptr_t * vOutputs; // .outputs lines - Vec_Ptr_t * vLatches; // .latch lines - Vec_Ptr_t * vNames; // .names lines - Vec_Ptr_t * vSubckts; // .subckt lines - Vec_Ptr_t * vDelays; // .delay lines - Vec_Ptr_t * vTimeInputs; // .input_arrival/required lines - Vec_Ptr_t * vTimeOutputs; // .output_required/arrival lines - int fBlackBox; // indicates blackbox model - // the resulting network - Ntl_Mod_t * pNtk; - // the parent manager - Ioa_ReadMan_t * pMan; -}; - -struct Ioa_ReadMan_t_ -{ - // general info about file - char * pFileName; // the name of the file - char * pBuffer; // the contents of the file - Vec_Ptr_t * vLines; // the line beginnings - // the results of reading - Ntl_Man_t * pDesign; // the design under construction - // intermediate storage for models - Vec_Ptr_t * vModels; // vector of models - Ioa_ReadMod_t * pLatest; // the current model - // current processing info - Vec_Ptr_t * vTokens; // the current tokens - Vec_Ptr_t * vTokens2; // the current tokens - Vec_Str_t * vFunc; // the local function - // error reporting - char sError[512]; // the error string generated during parsing - // statistics - int nTablesRead; // the number of processed tables - int nTablesLeft; // the number of dangling tables -}; - -// static functions -static Ioa_ReadMan_t * Ioa_ReadAlloc(); -static void Ioa_ReadFree( Ioa_ReadMan_t * p ); -static Ioa_ReadMod_t * Ioa_ReadModAlloc(); -static void Ioa_ReadModFree( Ioa_ReadMod_t * p ); -static char * Ioa_ReadLoadFile( char * pFileName ); -static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p ); -static int Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p ); -static Ntl_Man_t * Ioa_ReadParse( Ioa_ReadMan_t * p ); -static int Ioa_ReadParseLineModel( Ioa_ReadMod_t * p, char * pLine ); -static int Ioa_ReadParseLineAttrib( Ioa_ReadMod_t * p, char * pLine ); -static int Ioa_ReadParseLineInputs( Ioa_ReadMod_t * p, char * pLine ); -static int Ioa_ReadParseLineOutputs( Ioa_ReadMod_t * p, char * pLine ); -static int Ioa_ReadParseLineLatch( Ioa_ReadMod_t * p, char * pLine ); -static int Ioa_ReadParseLineSubckt( Ioa_ReadMod_t * p, char * pLine ); -static int Ioa_ReadParseLineDelay( Ioa_ReadMod_t * p, char * pLine ); -static int Ioa_ReadParseLineTimes( Ioa_ReadMod_t * p, char * pLine, int fOutput ); -static int Ioa_ReadParseLineNamesBlif( Ioa_ReadMod_t * p, char * pLine ); - -static int Ioa_ReadCharIsSpace( char s ) { return s == ' ' || s == '\t' || s == '\r' || s == '\n'; } -static int Ioa_ReadCharIsSopSymb( char s ) { return s == '0' || s == '1' || s == '-' || s == '\r' || s == '\n'; } - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Reads the network from the BLIF file.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck ) -{ - FILE * pFile; - Ioa_ReadMan_t * p; - Ntl_Man_t * pDesign; -// int nNodes; - - // check that the file is available - pFile = fopen( pFileName, "rb" ); - if ( pFile == NULL ) - { - printf( "Ioa_ReadBlif(): The file is unavailable (absent or open).\n" ); - return 0; - } - fclose( pFile ); - - // start the file reader - p = Ioa_ReadAlloc(); - p->pFileName = pFileName; - p->pBuffer = Ioa_ReadLoadFile( pFileName ); - if ( p->pBuffer == NULL ) - { - Ioa_ReadFree( p ); - return NULL; - } - // set the design name - p->pDesign = Ntl_ManAlloc( pFileName ); - p->pDesign->pName = Ntl_ManStoreFileName( p->pDesign, pFileName ); - p->pDesign->pSpec = Ntl_ManStoreName( p->pDesign, pFileName ); - // prepare the file for parsing - Ioa_ReadReadPreparse( p ); - // parse interfaces of each network - if ( !Ioa_ReadReadInterfaces( p ) ) - { - if ( p->sError[0] ) - fprintf( stdout, "%s\n", p->sError ); - Ioa_ReadFree( p ); - return NULL; - } - // construct the network - pDesign = Ioa_ReadParse( p ); - if ( p->sError[0] ) - fprintf( stdout, "%s\n", p->sError ); - if ( pDesign == NULL ) - { - Ioa_ReadFree( p ); - return NULL; - } - p->pDesign = NULL; - Ioa_ReadFree( p ); -// pDesign should be linked to all models of the design - - // make sure that everything is okay with the network structure - if ( fCheck ) - { - if ( !Ntl_ManCheck( pDesign ) ) - { - printf( "Ioa_ReadBlif: The check has failed for design %s.\n", pDesign->pName ); - Ntl_ManFree( pDesign ); - return NULL; - } - - } - // transform the design by removing the CO drivers -// if ( (nNodes = Ntl_ManReconnectCoDrivers(pDesign)) ) -// printf( "The design was transformed by removing %d buf/inv CO drivers.\n", nNodes ); -//Ioa_WriteBlif( pDesign, "_temp_.blif" ); - return pDesign; -} - -/**Function************************************************************* - - Synopsis [Allocates the BLIF parsing structure.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static Ioa_ReadMan_t * Ioa_ReadAlloc() -{ - Ioa_ReadMan_t * p; - p = ALLOC( Ioa_ReadMan_t, 1 ); - memset( p, 0, sizeof(Ioa_ReadMan_t) ); - p->vLines = Vec_PtrAlloc( 512 ); - p->vModels = Vec_PtrAlloc( 512 ); - p->vTokens = Vec_PtrAlloc( 512 ); - p->vTokens2 = Vec_PtrAlloc( 512 ); - p->vFunc = Vec_StrAlloc( 512 ); - return p; -} - -/**Function************************************************************* - - Synopsis [Frees the BLIF parsing structure.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static void Ioa_ReadFree( Ioa_ReadMan_t * p ) -{ - Ioa_ReadMod_t * pMod; - int i; - if ( p->pDesign ) - Ntl_ManFree( p->pDesign ); - if ( p->pBuffer ) - free( p->pBuffer ); - if ( p->vLines ) - Vec_PtrFree( p->vLines ); - if ( p->vModels ) - { - Vec_PtrForEachEntry( p->vModels, pMod, i ) - Ioa_ReadModFree( pMod ); - Vec_PtrFree( p->vModels ); - } - Vec_PtrFree( p->vTokens ); - Vec_PtrFree( p->vTokens2 ); - Vec_StrFree( p->vFunc ); - free( p ); -} - -/**Function************************************************************* - - Synopsis [Allocates the BLIF parsing structure for one model.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static Ioa_ReadMod_t * Ioa_ReadModAlloc() -{ - Ioa_ReadMod_t * p; - p = ALLOC( Ioa_ReadMod_t, 1 ); - memset( p, 0, sizeof(Ioa_ReadMod_t) ); - p->vInputs = Vec_PtrAlloc( 8 ); - p->vOutputs = Vec_PtrAlloc( 8 ); - p->vLatches = Vec_PtrAlloc( 8 ); - p->vNames = Vec_PtrAlloc( 8 ); - p->vSubckts = Vec_PtrAlloc( 8 ); - p->vDelays = Vec_PtrAlloc( 8 ); - p->vTimeInputs = Vec_PtrAlloc( 8 ); - p->vTimeOutputs = Vec_PtrAlloc( 8 ); - return p; -} - -/**Function************************************************************* - - Synopsis [Deallocates the BLIF parsing structure for one model.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static void Ioa_ReadModFree( Ioa_ReadMod_t * p ) -{ - Vec_PtrFree( p->vInputs ); - Vec_PtrFree( p->vOutputs ); - Vec_PtrFree( p->vLatches ); - Vec_PtrFree( p->vNames ); - Vec_PtrFree( p->vSubckts ); - Vec_PtrFree( p->vDelays ); - Vec_PtrFree( p->vTimeInputs ); - Vec_PtrFree( p->vTimeOutputs ); - free( p ); -} - - - -/**Function************************************************************* - - Synopsis [Counts the number of given chars.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static int Ioa_ReadCountChars( char * pLine, char Char ) -{ - char * pCur; - int Counter = 0; - for ( pCur = pLine; *pCur; pCur++ ) - if ( *pCur == Char ) - Counter++; - return Counter; -} - -/**Function************************************************************* - - Synopsis [Collects the already split tokens.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static void Ioa_ReadCollectTokens( Vec_Ptr_t * vTokens, char * pInput, char * pOutput ) -{ - char * pCur; - Vec_PtrClear( vTokens ); - for ( pCur = pInput; pCur < pOutput; pCur++ ) - { - if ( *pCur == 0 ) - continue; - Vec_PtrPush( vTokens, pCur ); - while ( *++pCur ); - } -} - -/**Function************************************************************* - - Synopsis [Splits the line into tokens.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static void Ioa_ReadSplitIntoTokens( Vec_Ptr_t * vTokens, char * pLine, char Stop ) -{ - char * pCur; - // clear spaces - for ( pCur = pLine; *pCur != Stop; pCur++ ) - if ( Ioa_ReadCharIsSpace(*pCur) ) - *pCur = 0; - // collect tokens - Ioa_ReadCollectTokens( vTokens, pLine, pCur ); -} - -/**Function************************************************************* - - Synopsis [Splits the line into tokens.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static void Ioa_ReadSplitIntoTokensAndClear( Vec_Ptr_t * vTokens, char * pLine, char Stop, char Char ) -{ - char * pCur; - // clear spaces - for ( pCur = pLine; *pCur != Stop; pCur++ ) - if ( Ioa_ReadCharIsSpace(*pCur) || *pCur == Char ) - *pCur = 0; - // collect tokens - Ioa_ReadCollectTokens( vTokens, pLine, pCur ); -} - -/**Function************************************************************* - - Synopsis [Returns the 1-based number of the line in which the token occurs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static int Ioa_ReadGetLine( Ioa_ReadMan_t * p, char * pToken ) -{ - char * pLine; - int i; - Vec_PtrForEachEntry( p->vLines, pLine, i ) - if ( pToken < pLine ) - return i; - return -1; -} - -/**Function************************************************************* - - Synopsis [Reads the file into a character buffer.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static char * Ioa_ReadLoadFile( char * pFileName ) -{ - FILE * pFile; - int nFileSize; - char * pContents; - pFile = fopen( pFileName, "rb" ); - if ( pFile == NULL ) - { - printf( "Ioa_ReadLoadFile(): The file is unavailable (absent or open).\n" ); - return NULL; - } - fseek( pFile, 0, SEEK_END ); - nFileSize = ftell( pFile ); - if ( nFileSize == 0 ) - { - printf( "Ioa_ReadLoadFile(): The file is empty.\n" ); - return NULL; - } - pContents = ALLOC( char, nFileSize + 10 ); - rewind( pFile ); - fread( pContents, nFileSize, 1, pFile ); - fclose( pFile ); - // finish off the file with the spare .end line - // some benchmarks suddenly break off without this line - strcpy( pContents + nFileSize, "\n.end\n" ); - return pContents; -} - -/**Function************************************************************* - - Synopsis [Prepares the parsing.] - - Description [Performs several preliminary operations: - - Cuts the file buffer into separate lines. - - Removes comments and line extenders. - - Sorts lines by directives. - - Estimates the number of objects. - - Allocates room for the objects. - - Allocates room for the hash table.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p ) -{ - char * pCur, * pPrev; - int i, fComment = 0; - // parse the buffer into lines and remove comments - Vec_PtrPush( p->vLines, p->pBuffer ); - for ( pCur = p->pBuffer; *pCur; pCur++ ) - { - if ( *pCur == '\n' ) - { - *pCur = 0; -// if ( *(pCur-1) == '\r' ) -// *(pCur-1) = 0; - fComment = 0; - Vec_PtrPush( p->vLines, pCur + 1 ); - } - else if ( *pCur == '#' ) - fComment = 1; - // remove comments - if ( fComment ) - *pCur = 0; - } - - // unfold the line extensions and sort lines by directive - Vec_PtrForEachEntry( p->vLines, pCur, i ) - { - if ( *pCur == 0 ) - continue; - // find previous non-space character - for ( pPrev = pCur - 2; pPrev >= p->pBuffer; pPrev-- ) - if ( !Ioa_ReadCharIsSpace(*pPrev) ) - break; - // if it is the line extender, overwrite it with spaces - if ( *pPrev == '\\' ) - { - for ( ; *pPrev; pPrev++ ) - *pPrev = ' '; - *pPrev = ' '; - continue; - } - // skip spaces at the beginning of the line - while ( Ioa_ReadCharIsSpace(*pCur++) ); - // parse directives - if ( *(pCur-1) != '.' ) - continue; - if ( !strncmp(pCur, "names", 5) ) - Vec_PtrPush( p->pLatest->vNames, pCur ); - else if ( !strncmp(pCur, "latch", 5) ) - Vec_PtrPush( p->pLatest->vLatches, pCur ); - else if ( !strncmp(pCur, "inputs", 6) ) - Vec_PtrPush( p->pLatest->vInputs, pCur ); - else if ( !strncmp(pCur, "outputs", 7) ) - Vec_PtrPush( p->pLatest->vOutputs, pCur ); - else if ( !strncmp(pCur, "subckt", 6) ) - Vec_PtrPush( p->pLatest->vSubckts, pCur ); - else if ( !strncmp(pCur, "delay", 5) ) - Vec_PtrPush( p->pLatest->vDelays, pCur ); - else if ( !strncmp(pCur, "input_arrival", 13) || - !strncmp(pCur, "input_required", 14) ) - Vec_PtrPush( p->pLatest->vTimeInputs, pCur ); - else if ( !strncmp(pCur, "output_required", 14) || - !strncmp(pCur, "output_arrival", 13) ) - Vec_PtrPush( p->pLatest->vTimeOutputs, pCur ); - else if ( !strncmp(pCur, "blackbox", 8) ) - p->pLatest->fBlackBox = 1; - else if ( !strncmp(pCur, "model", 5) ) - { - p->pLatest = Ioa_ReadModAlloc(); - p->pLatest->pFirst = pCur; - p->pLatest->pMan = p; - } - else if ( !strncmp(pCur, "attrib", 6) ) - { - if ( p->pLatest->pAttrib != NULL ) - fprintf( stdout, "Line %d: Skipping second .attrib line for this model.\n", Ioa_ReadGetLine(p, pCur) ); - else - p->pLatest->pAttrib = pCur; - } - else if ( !strncmp(pCur, "end", 3) ) - { - if ( p->pLatest ) - Vec_PtrPush( p->vModels, p->pLatest ); - p->pLatest = NULL; - } - else if ( !strncmp(pCur, "exdc", 4) ) - { - fprintf( stdout, "Line %d: Skipping EXDC network.\n", Ioa_ReadGetLine(p, pCur) ); - break; - } - else if ( !strncmp(pCur, "no_merge", 8) ) - { - } - else - { - pCur--; - if ( pCur[strlen(pCur)-1] == '\r' ) - pCur[strlen(pCur)-1] = 0; - fprintf( stdout, "Line %d: Skipping line \"%s\".\n", Ioa_ReadGetLine(p, pCur), pCur ); - } - } -} - -/**Function************************************************************* - - Synopsis [Parses interfaces of the models.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static int Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p ) -{ - Ioa_ReadMod_t * pMod; - char * pLine; - int i, k; - // iterate through the models - Vec_PtrForEachEntry( p->vModels, pMod, i ) - { - // parse the model - if ( !Ioa_ReadParseLineModel( pMod, pMod->pFirst ) ) - return 0; - // parse the model attributes - if ( pMod->pAttrib && !Ioa_ReadParseLineAttrib( pMod, pMod->pAttrib ) ) - return 0; - // parse the inputs - Vec_PtrForEachEntry( pMod->vInputs, pLine, k ) - if ( !Ioa_ReadParseLineInputs( pMod, pLine ) ) - return 0; - // parse the outputs - Vec_PtrForEachEntry( pMod->vOutputs, pLine, k ) - if ( !Ioa_ReadParseLineOutputs( pMod, pLine ) ) - return 0; - // parse the delay info - Vec_PtrForEachEntry( pMod->vDelays, pLine, k ) - if ( !Ioa_ReadParseLineDelay( pMod, pLine ) ) - return 0; - Vec_PtrForEachEntry( pMod->vTimeInputs, pLine, k ) - if ( !Ioa_ReadParseLineTimes( pMod, pLine, 0 ) ) - return 0; - Vec_PtrForEachEntry( pMod->vTimeOutputs, pLine, k ) - if ( !Ioa_ReadParseLineTimes( pMod, pLine, 1 ) ) - return 0; - } - return 1; -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static Ntl_Man_t * Ioa_ReadParse( Ioa_ReadMan_t * p ) -{ - Ntl_Man_t * pDesign; - Ioa_ReadMod_t * pMod; - char * pLine; - int i, k; - // iterate through the models - Vec_PtrForEachEntry( p->vModels, pMod, i ) - { - // parse the latches - Vec_PtrForEachEntry( pMod->vLatches, pLine, k ) - if ( !Ioa_ReadParseLineLatch( pMod, pLine ) ) - return NULL; - // parse the nodes - Vec_PtrForEachEntry( pMod->vNames, pLine, k ) - if ( !Ioa_ReadParseLineNamesBlif( pMod, pLine ) ) - return NULL; - // parse the subcircuits - Vec_PtrForEachEntry( pMod->vSubckts, pLine, k ) - if ( !Ioa_ReadParseLineSubckt( pMod, pLine ) ) - return NULL; - // finalize the network - Ntl_ModelFixNonDrivenNets( pMod->pNtk ); - } - if ( i == 0 ) - return NULL; - // update the design name - pMod = Vec_PtrEntry( p->vModels, 0 ); - if ( Ntl_ModelLatchNum(pMod->pNtk) > 0 ) - Ntl_ModelTransformLatches( pMod->pNtk ); - p->pDesign->pName = Ntl_ManStoreName( p->pDesign, pMod->pNtk->pName ); - // return the network - pDesign = p->pDesign; - p->pDesign = NULL; - return pDesign; -} - -/**Function************************************************************* - - Synopsis [Parses the model line.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static int Ioa_ReadParseLineModel( Ioa_ReadMod_t * p, char * pLine ) -{ - Vec_Ptr_t * vTokens = p->pMan->vTokens; - char * pToken; - Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' ); - pToken = Vec_PtrEntry( vTokens, 0 ); - assert( !strcmp(pToken, "model") ); - if ( Vec_PtrSize(vTokens) != 2 ) - { - sprintf( p->pMan->sError, "Line %d: The number of entries (%d) in .model line is different from two.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) ); - return 0; - } - p->pNtk = Ntl_ModelAlloc( p->pMan->pDesign, Vec_PtrEntry(vTokens, 1) ); - if ( p->pNtk == NULL ) - { - sprintf( p->pMan->sError, "Line %d: Model %s already exists.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) ); - return 0; - } - return 1; -} - -/**Function************************************************************* - - Synopsis [Parses the model line.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static int Ioa_ReadParseLineAttrib( Ioa_ReadMod_t * p, char * pLine ) -{ - Vec_Ptr_t * vTokens = p->pMan->vTokens; - char * pToken; - int i; - Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' ); - pToken = Vec_PtrEntry( vTokens, 0 ); - assert( !strncmp(pToken, "attrib", 6) ); - Vec_PtrForEachEntryStart( vTokens, pToken, i, 1 ) - { - pToken = Vec_PtrEntry( vTokens, i ); - if ( strcmp( pToken, "white" ) == 0 ) - p->pNtk->attrWhite = 1; - else if ( strcmp( pToken, "black" ) == 0 ) - p->pNtk->attrWhite = 0; - else if ( strcmp( pToken, "box" ) == 0 ) - p->pNtk->attrBox = 1; - else if ( strcmp( pToken, "white" ) == 0 ) - p->pNtk->attrWhite = 1; - else if ( strcmp( pToken, "comb" ) == 0 ) - p->pNtk->attrComb = 1; - else if ( strcmp( pToken, "seq" ) == 0 ) - p->pNtk->attrComb = 0; - else if ( strcmp( pToken, "keep" ) == 0 ) - p->pNtk->attrKeep = 1; - else - { - sprintf( p->pMan->sError, "Line %d: Unknown attribute (%s) in the .attrib line of model %s.", Ioa_ReadGetLine(p->pMan, pToken), pToken, p->pNtk->pName ); - return 0; - } - } - return 1; -} - -/**Function************************************************************* - - Synopsis [Parses the inputs line.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static int Ioa_ReadParseLineInputs( Ioa_ReadMod_t * p, char * pLine ) -{ - Ntl_Net_t * pNet; - Ntl_Obj_t * pObj; - Vec_Ptr_t * vTokens = p->pMan->vTokens; - char * pToken; - int i; - Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' ); - pToken = Vec_PtrEntry(vTokens, 0); - assert( !strcmp(pToken, "inputs") ); - Vec_PtrForEachEntryStart( vTokens, pToken, i, 1 ) - { - pObj = Ntl_ModelCreatePi( p->pNtk ); - pNet = Ntl_ModelFindOrCreateNet( p->pNtk, pToken ); - if ( !Ntl_ModelSetNetDriver( pObj, pNet ) ) - { - sprintf( p->pMan->sError, "Line %d: Net %s already has a driver.", Ioa_ReadGetLine(p->pMan, pToken), pNet->pName ); - return 0; - } - } - return 1; -} - -/**Function************************************************************* - - Synopsis [Parses the outputs line.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static int Ioa_ReadParseLineOutputs( Ioa_ReadMod_t * p, char * pLine ) -{ - Ntl_Net_t * pNet; - Ntl_Obj_t * pObj; - Vec_Ptr_t * vTokens = p->pMan->vTokens; - char * pToken; - int i; - Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' ); - pToken = Vec_PtrEntry(vTokens, 0); - assert( !strcmp(pToken, "outputs") ); - Vec_PtrForEachEntryStart( vTokens, pToken, i, 1 ) - { - pNet = Ntl_ModelFindOrCreateNet( p->pNtk, pToken ); - pObj = Ntl_ModelCreatePo( p->pNtk, pNet ); - } - return 1; -} - -/**Function************************************************************* - - Synopsis [Parses the latches line.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static int Ioa_ReadParseLineLatch( Ioa_ReadMod_t * p, char * pLine ) -{ - Vec_Ptr_t * vTokens = p->pMan->vTokens; - Ntl_Net_t * pNetLi, * pNetLo; - Ntl_Obj_t * pObj; - char * pToken, * pNameLi, * pNameLo; - Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' ); - pToken = Vec_PtrEntry(vTokens,0); - assert( !strcmp(pToken, "latch") ); - if ( Vec_PtrSize(vTokens) < 3 ) - { - sprintf( p->pMan->sError, "Line %d: Latch does not have input name and output name.", Ioa_ReadGetLine(p->pMan, pToken) ); - return 0; - } - // create latch - pNameLi = Vec_PtrEntry( vTokens, 1 ); - pNameLo = Vec_PtrEntry( vTokens, 2 ); - pNetLi = Ntl_ModelFindOrCreateNet( p->pNtk, pNameLi ); - pNetLo = Ntl_ModelFindOrCreateNet( p->pNtk, pNameLo ); - pObj = Ntl_ModelCreateLatch( p->pNtk ); - pObj->pFanio[0] = pNetLi; - if ( !Ntl_ModelSetNetDriver( pObj, pNetLo ) ) - { - sprintf( p->pMan->sError, "Line %d: Net %s already has a driver.", Ioa_ReadGetLine(p->pMan, pToken), pNetLo->pName ); - return 0; - } - // get initial value - if ( Vec_PtrSize(vTokens) > 3 ) - pObj->LatchId.regInit = atoi( Vec_PtrEntry(vTokens,Vec_PtrSize(vTokens)-1) ); - else - pObj->LatchId.regInit = 2; - if ( pObj->LatchId.regInit < 0 || pObj->LatchId.regInit > 2 ) - { - sprintf( p->pMan->sError, "Line %d: Initial state of the latch is incorrect \"%s\".", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens,3) ); - return 0; - } - // get the register class - if ( Vec_PtrSize(vTokens) == 6 ) - { - pToken = Vec_PtrEntry(vTokens,3); - if ( strcmp( pToken, "fe" ) == 0 ) - pObj->LatchId.regType = 1; - else if ( strcmp( pToken, "re" ) == 0 ) - pObj->LatchId.regType = 2; - else if ( strcmp( pToken, "ah" ) == 0 ) - pObj->LatchId.regType = 3; - else if ( strcmp( pToken, "al" ) == 0 ) - pObj->LatchId.regType = 4; - else if ( strcmp( pToken, "as" ) == 0 ) - pObj->LatchId.regType = 5; - else if ( pToken[0] >= '0' && pToken[0] <= '9' ) - pObj->LatchId.regClass = atoi(pToken); - else - { - sprintf( p->pMan->sError, "Line %d: Type/class of the latch is incorrect \"%s\".", Ioa_ReadGetLine(p->pMan, pToken), pToken ); - return 0; - } - } - if ( pObj->LatchId.regClass < 0 || pObj->LatchId.regClass > (1<<24) ) - { - sprintf( p->pMan->sError, "Line %d: Class of the latch is incorrect \"%s\".", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens,3) ); - return 0; - } - // get the clock - if ( Vec_PtrSize(vTokens) == 5 || Vec_PtrSize(vTokens) == 6 ) - { - pToken = Vec_PtrEntry(vTokens,Vec_PtrSize(vTokens)-2); - pNetLi = Ntl_ModelFindOrCreateNet( p->pNtk, pToken ); - pObj->pClock = pNetLi; - } - return 1; -} - -/**Function************************************************************* - - Synopsis [Parses the subckt line.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static int Ioa_ReadParseLineSubckt( Ioa_ReadMod_t * p, char * pLine ) -{ - Vec_Ptr_t * vTokens = p->pMan->vTokens; - Ntl_Mod_t * pModel; - Ntl_Obj_t * pBox, * pTerm; - Ntl_Net_t * pNet; - char * pToken, * pName, ** ppNames; - int nEquals, i, k; - - // split the line into tokens - nEquals = Ioa_ReadCountChars( pLine, '=' ); - Ioa_ReadSplitIntoTokensAndClear( vTokens, pLine, '\0', '=' ); - pToken = Vec_PtrEntry(vTokens,0); - assert( !strcmp(pToken, "subckt") ); - - // get the model for this box - pName = Vec_PtrEntry(vTokens,1); - pModel = Ntl_ManFindModel( p->pMan->pDesign, pName ); - if ( pModel == NULL ) - { - sprintf( p->pMan->sError, "Line %d: Cannot find the model for subcircuit %s.", Ioa_ReadGetLine(p->pMan, pToken), pName ); - return 0; - } -/* - // temporary fix for splitting the .subckt line - if ( nEquals < Ntl_ModelPiNum(pModel) + Ntl_ModelPoNum(pModel) ) - { - Vec_Ptr_t * vTokens2 = Vec_PtrAlloc( 10 ); - // get one additional token - pToken = Vec_PtrEntry( vTokens, Vec_PtrSize(vTokens) - 1 ); - for ( ; *pToken; pToken++ ); - for ( ; *pToken == 0; pToken++ ); - Ioa_ReadSplitIntoTokensAndClear( vTokens2, pToken, '\0', '=' ); -// assert( Vec_PtrSize( vTokens2 ) == 2 ); - Vec_PtrForEachEntry( vTokens2, pToken, i ) - Vec_PtrPush( vTokens, pToken ); - nEquals += Vec_PtrSize(vTokens2)/2; - Vec_PtrFree( vTokens2 ); - } -*/ - // check if the number of tokens is correct - if ( nEquals != Ntl_ModelPiNum(pModel) + Ntl_ModelPoNum(pModel) ) - { - sprintf( p->pMan->sError, "Line %d: The number of ports (%d) in .subckt %s differs from the sum of PIs and POs of the model (%d).", - Ioa_ReadGetLine(p->pMan, pToken), nEquals, pName, Ntl_ModelPiNum(pModel) + Ntl_ModelPoNum(pModel) ); - return 0; - } - - // get the names - ppNames = (char **)Vec_PtrArray(vTokens) + 2; - - // create the box with these terminals - pBox = Ntl_ModelCreateBox( p->pNtk, Ntl_ModelPiNum(pModel), Ntl_ModelPoNum(pModel) ); - pBox->pImplem = pModel; - Ntl_ModelForEachPi( pModel, pTerm, i ) - { - // find this terminal among the formal inputs of the subcircuit - pName = Ntl_ObjFanout0(pTerm)->pName; - for ( k = 0; k < nEquals; k++ ) - if ( !strcmp( ppNames[2*k], pName ) ) - break; - if ( k == nEquals ) - { - sprintf( p->pMan->sError, "Line %d: Cannot find PI \"%s\" of the model \"%s\" as a formal input of the subcircuit.", - Ioa_ReadGetLine(p->pMan, pToken), pName, pModel->pName ); - return 0; - } - // create the BI with the actual name - pNet = Ntl_ModelFindOrCreateNet( p->pNtk, ppNames[2*k+1] ); - Ntl_ObjSetFanin( pBox, pNet, i ); - } - Ntl_ModelForEachPo( pModel, pTerm, i ) - { - // find this terminal among the formal outputs of the subcircuit - pName = Ntl_ObjFanin0(pTerm)->pName; - for ( k = 0; k < nEquals; k++ ) - if ( !strcmp( ppNames[2*k], pName ) ) - break; - if ( k == nEquals ) - { - sprintf( p->pMan->sError, "Line %d: Cannot find PO \"%s\" of the model \"%s\" as a formal output of the subcircuit.", - Ioa_ReadGetLine(p->pMan, pToken), pName, pModel->pName ); - return 0; - } - // create the BI with the actual name - pNet = Ntl_ModelFindOrCreateNet( p->pNtk, ppNames[2*k+1] ); - Ntl_ObjSetFanout( pBox, pNet, i ); - } - return 1; -} - -/**Function************************************************************* - - Synopsis [Parses the subckt line.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static int Ioa_ReadParseLineDelay( Ioa_ReadMod_t * p, char * pLine ) -{ - Vec_Ptr_t * vTokens = p->pMan->vTokens; - int RetValue1, RetValue2, Number1, Number2, Temp; - char * pToken, * pTokenNum; - float Delay; - assert( sizeof(float) == sizeof(int) ); - Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' ); - pToken = Vec_PtrEntry(vTokens,0); - assert( !strcmp(pToken, "delay") ); - if ( Vec_PtrSize(vTokens) < 2 && Vec_PtrSize(vTokens) > 4 ) - { - sprintf( p->pMan->sError, "Line %d: Delay line does not have a valid number of parameters (1, 2, or 3).", Ioa_ReadGetLine(p->pMan, pToken) ); - return 0; - } - // find the delay number - pTokenNum = Vec_PtrEntryLast(vTokens); - Delay = atof( pTokenNum ); - if ( Delay == 0.0 && pTokenNum[0] != '0' ) - { - sprintf( p->pMan->sError, "Line %d: Delay value (%s) appears to be invalid.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntryLast(vTokens) ); - return 0; - } - // find the PI/PO numbers - RetValue1 = 0; Number1 = -1; - if ( Vec_PtrSize(vTokens) > 2 ) - { - RetValue1 = Ntl_ModelFindPioNumber( p->pNtk, 0, 0, Vec_PtrEntry(vTokens, 1), &Number1 ); - if ( RetValue1 == 0 ) - { - sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among PIs/POs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) ); - return 0; - } - } - RetValue2 = 0; Number2 = -1; - if ( Vec_PtrSize(vTokens) > 3 ) - { - RetValue2 = Ntl_ModelFindPioNumber( p->pNtk, 0, 0, Vec_PtrEntry(vTokens, 2), &Number2 ); - if ( RetValue2 == 0 ) - { - sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among PIs/POs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 2) ); - return 0; - } - } - if ( RetValue1 == RetValue2 && RetValue1 ) - { - sprintf( p->pMan->sError, "Line %d: Both signals \"%s\" and \"%s\" listed appear to be PIs or POs.", - Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1), Vec_PtrEntry(vTokens, 2) ); - return 0; - } - if ( RetValue2 < RetValue1 ) - { - Temp = RetValue2; RetValue2 = RetValue1; RetValue1 = Temp; - Temp = Number2; Number2 = Number1; Number1 = Temp; - } - assert( RetValue1 == 0 || RetValue1 == -1 ); - assert( RetValue2 == 0 || RetValue2 == 1 ); - // store the values - if ( p->pNtk->vDelays == NULL ) - p->pNtk->vDelays = Vec_IntAlloc( 100 ); - Vec_IntPush( p->pNtk->vDelays, Number1 ); - Vec_IntPush( p->pNtk->vDelays, Number2 ); - Vec_IntPush( p->pNtk->vDelays, Aig_Float2Int(Delay) ); - return 1; -} - -/**Function************************************************************* - - Synopsis [Parses the subckt line.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static int Ioa_ReadParseLineTimes( Ioa_ReadMod_t * p, char * pLine, int fOutput ) -{ - Vec_Ptr_t * vTokens = p->pMan->vTokens; - int RetValue, Number = -1; - char * pToken, * pTokenNum; - float Delay; - assert( sizeof(float) == sizeof(int) ); - Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' ); - pToken = Vec_PtrEntry(vTokens,0); - if ( fOutput ) - assert( !strncmp(pToken, "output_", 7) ); - else - assert( !strncmp(pToken, "input_", 6) ); - if ( Vec_PtrSize(vTokens) != 2 && Vec_PtrSize(vTokens) != 3 ) - { - sprintf( p->pMan->sError, "Line %d: Delay line does not have a valid number of parameters (2 or 3).", Ioa_ReadGetLine(p->pMan, pToken) ); - return 0; - } - // find the delay number - pTokenNum = Vec_PtrEntryLast(vTokens); - if ( !strcmp( pTokenNum, "-inf" ) ) - Delay = -TIM_ETERNITY; - else if ( !strcmp( pTokenNum, "inf" ) ) - Delay = TIM_ETERNITY; - else - Delay = atof( pTokenNum ); - if ( Delay == 0.0 && pTokenNum[0] != '0' ) - { - sprintf( p->pMan->sError, "Line %d: Delay value (%s) appears to be invalid.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntryLast(vTokens) ); - return 0; - } - // find the PI/PO numbers - if ( fOutput ) - { - if ( Vec_PtrSize(vTokens) == 3 ) - { - RetValue = Ntl_ModelFindPioNumber( p->pNtk, 0, 1, Vec_PtrEntry(vTokens, 1), &Number ); - if ( RetValue == 0 ) - { - sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among POs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) ); - return 0; - } - } - // store the values - if ( p->pNtk->vTimeOutputs == NULL ) - p->pNtk->vTimeOutputs = Vec_IntAlloc( 100 ); - Vec_IntPush( p->pNtk->vTimeOutputs, Number ); - Vec_IntPush( p->pNtk->vTimeOutputs, Aig_Float2Int(Delay) ); - } - else - { - if ( Vec_PtrSize(vTokens) == 3 ) - { - RetValue = Ntl_ModelFindPioNumber( p->pNtk, 1, 0, Vec_PtrEntry(vTokens, 1), &Number ); - if ( RetValue == 0 ) - { - sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among PIs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) ); - return 0; - } - } - // store the values - if ( p->pNtk->vTimeInputs == NULL ) - p->pNtk->vTimeInputs = Vec_IntAlloc( 100 ); - Vec_IntPush( p->pNtk->vTimeInputs, Number ); - Vec_IntPush( p->pNtk->vTimeInputs, Aig_Float2Int(Delay) ); - } - return 1; -} - - -/**Function************************************************************* - - Synopsis [Constructs the SOP cover from the file parsing info.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static char * Ioa_ReadParseTableBlif( Ioa_ReadMod_t * p, char * pTable, int nFanins ) -{ - Vec_Ptr_t * vTokens = p->pMan->vTokens; - Vec_Str_t * vFunc = p->pMan->vFunc; - char * pProduct, * pOutput; - int i, Polarity = -1; - - p->pMan->nTablesRead++; - // get the tokens - Ioa_ReadSplitIntoTokens( vTokens, pTable, '.' ); - if ( Vec_PtrSize(vTokens) == 0 ) - return Ntl_ManStoreSop( p->pMan->pDesign->pMemSops, " 0\n" ); - if ( Vec_PtrSize(vTokens) == 1 ) - { - pOutput = Vec_PtrEntry( vTokens, 0 ); - if ( ((pOutput[0] - '0') & 0x8E) || pOutput[1] ) - { - sprintf( p->pMan->sError, "Line %d: Constant table has wrong output value \"%s\".", Ioa_ReadGetLine(p->pMan, pOutput), pOutput ); - return NULL; - } - return Ntl_ManStoreSop( p->pMan->pDesign->pMemSops, (pOutput[0] == '0') ? " 0\n" : " 1\n" ); - } - pProduct = Vec_PtrEntry( vTokens, 0 ); - if ( Vec_PtrSize(vTokens) % 2 == 1 ) - { - sprintf( p->pMan->sError, "Line %d: Table has odd number of tokens (%d).", Ioa_ReadGetLine(p->pMan, pProduct), Vec_PtrSize(vTokens) ); - return NULL; - } - // parse the table - Vec_StrClear( vFunc ); - for ( i = 0; i < Vec_PtrSize(vTokens)/2; i++ ) - { - pProduct = Vec_PtrEntry( vTokens, 2*i + 0 ); - pOutput = Vec_PtrEntry( vTokens, 2*i + 1 ); - if ( strlen(pProduct) != (unsigned)nFanins ) - { - sprintf( p->pMan->sError, "Line %d: Cube \"%s\" has size different from the fanin count (%d).", Ioa_ReadGetLine(p->pMan, pProduct), pProduct, nFanins ); - return NULL; - } - if ( ((pOutput[0] - '0') & 0x8E) || pOutput[1] ) - { - sprintf( p->pMan->sError, "Line %d: Output value \"%s\" is incorrect.", Ioa_ReadGetLine(p->pMan, pProduct), pOutput ); - return NULL; - } - if ( Polarity == -1 ) - Polarity = pOutput[0] - '0'; - else if ( Polarity != pOutput[0] - '0' ) - { - sprintf( p->pMan->sError, "Line %d: Output value \"%s\" differs from the value in the first line of the table (%d).", Ioa_ReadGetLine(p->pMan, pProduct), pOutput, Polarity ); - return NULL; - } - // parse one product - Vec_StrAppend( vFunc, pProduct ); - Vec_StrPush( vFunc, ' ' ); - Vec_StrPush( vFunc, pOutput[0] ); - Vec_StrPush( vFunc, '\n' ); - } - Vec_StrPush( vFunc, '\0' ); - return Vec_StrArray( vFunc ); -} - -/**Function************************************************************* - - Synopsis [Parses the nodes line.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static int Ioa_ReadParseLineNamesBlif( Ioa_ReadMod_t * p, char * pLine ) -{ - Vec_Ptr_t * vTokens = p->pMan->vTokens; - Ntl_Obj_t * pNode; - Ntl_Net_t * pNetOut, * pNetIn; - char * pNameOut, * pNameIn; - int i; - Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' ); - // parse the mapped node -// if ( !strcmp(Vec_PtrEntry(vTokens,0), "gate") ) -// return Ioa_ReadParseLineGateBlif( p, vTokens ); - // parse the regular name line - assert( !strcmp(Vec_PtrEntry(vTokens,0), "names") ); - pNameOut = Vec_PtrEntryLast( vTokens ); - pNetOut = Ntl_ModelFindOrCreateNet( p->pNtk, pNameOut ); - // create fanins - pNode = Ntl_ModelCreateNode( p->pNtk, Vec_PtrSize(vTokens) - 2 ); - for ( i = 0; i < Vec_PtrSize(vTokens) - 2; i++ ) - { - pNameIn = Vec_PtrEntry(vTokens, i+1); - pNetIn = Ntl_ModelFindOrCreateNet( p->pNtk, pNameIn ); - Ntl_ObjSetFanin( pNode, pNetIn, i ); - } - if ( !Ntl_ModelSetNetDriver( pNode, pNetOut ) ) - { - sprintf( p->pMan->sError, "Line %d: Signal \"%s\" is defined more than once.", Ioa_ReadGetLine(p->pMan, pNameOut), pNameOut ); - return 0; - } - // parse the table of this node - pNode->pSop = Ioa_ReadParseTableBlif( p, pNameOut + strlen(pNameOut), pNode->nFanins ); - if ( pNode->pSop == NULL ) - return 0; - pNode->pSop = Ntl_ManStoreSop( p->pNtk->pMan->pMemSops, pNode->pSop ); - return 1; -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/aig/ntl/ntlTable.c b/src/aig/ntl/ntlTable.c index fe58e2f8..208b4491 100644 --- a/src/aig/ntl/ntlTable.c +++ b/src/aig/ntl/ntlTable.c @@ -178,6 +178,27 @@ Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName ) return pEnt; } +/**Function************************************************************* + + Synopsis [Assigns numbers to PIs and POs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntl_ModelSetPioNumbers( Ntl_Mod_t * p ) +{ + Ntl_Obj_t * pObj; + int i; + Ntl_ModelForEachPi( p, pObj, i ) + pObj->iTemp = i; + Ntl_ModelForEachPo( p, pObj, i ) + pObj->iTemp = i; +} + /**Function************************************************************* Synopsis [Returns -1, 0, +1 (when it is PI, not found, or PO).] @@ -189,7 +210,7 @@ Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName ) SeeAlso [] ***********************************************************************/ -int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * pName, int * pNumber ) +int Ntl_ModelFindPioNumber_old( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * pName, int * pNumber ) { Ntl_Net_t * pNet; Ntl_Obj_t * pObj; @@ -241,6 +262,60 @@ int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * pNam return 0; } +/**Function************************************************************* + + Synopsis [Returns -1, 0, +1 (when it is PI, not found, or PO).] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * pName, int * pNumber ) +{ + Ntl_Net_t * pNet; + Ntl_Obj_t * pTerm; + *pNumber = -1; + pNet = Ntl_ModelFindNet( p, pName ); + if ( pNet == NULL ) + return 0; + if ( fPiOnly ) + { + pTerm = pNet->pDriver; + if ( pTerm && Ntl_ObjIsPi(pTerm) ) + { + *pNumber = pTerm->iTemp; + return -1; + } + return 0; + } + if ( fPoOnly ) + { + pTerm = pNet->pCopy; + if ( pTerm && Ntl_ObjIsPo(pTerm) ) + { + *pNumber = pTerm->iTemp; + return 1; + } + return 0; + } + pTerm = pNet->pCopy; + if ( pTerm && Ntl_ObjIsPo(pTerm) ) + { + *pNumber = pTerm->iTemp; + return 1; + } + pTerm = pNet->pDriver; + if ( pTerm && Ntl_ObjIsPi(pTerm) ) + { + *pNumber = pTerm->iTemp; + return -1; + } + return 0; +} + /**Function************************************************************* Synopsis [Sets the driver of the net.] diff --git a/src/aig/nwk/nwkCheck.c b/src/aig/nwk/nwkCheck.c index 0890ced8..f20d61f2 100644 --- a/src/aig/nwk/nwkCheck.c +++ b/src/aig/nwk/nwkCheck.c @@ -55,7 +55,7 @@ int Nwk_ManCheck( Nwk_Man_t * p ) Nwk_ManForEachObj( p, pObj, i ) { Nwk_ObjForEachFanin( pObj, pNext, k ) - if ( Nwk_ObjFindFanout( pNext, pObj ) == -1 ) + if ( Nwk_ObjFanoutNum(pNext) < 100 && Nwk_ObjFindFanout( pNext, pObj ) == -1 ) printf( "Nwk_ManCheck(): Object %d has fanin %d which does not have a corresponding fanout.\n", pObj->Id, pNext->Id ); Nwk_ObjForEachFanout( pObj, pNext, k ) if ( Nwk_ObjFindFanin( pNext, pObj ) == -1 ) diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make index 48d91438..7063bd2a 100644 --- a/src/aig/saig/module.make +++ b/src/aig/saig/module.make @@ -1,5 +1,6 @@ SRC += src/aig/saig/saigAbs.c \ src/aig/saig/saigBmc.c \ + src/aig/saig/saigBmc2.c \ src/aig/saig/saigCone.c \ src/aig/saig/saigDup.c \ src/aig/saig/saigHaig.c \ diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index f0c8fb54..a6f5631b 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -99,6 +99,7 @@ extern Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, in extern Aig_Man_t * Saig_ManCreateMiterComb( Aig_Man_t * p1, Aig_Man_t * p2, int Oper ); extern Aig_Man_t * Saig_ManCreateMiterTwo( Aig_Man_t * pOld, Aig_Man_t * pNew, int nFrames ); extern int Saig_ManDemiterSimple( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 ); +extern int Saig_ManDemiterSimpleDiff( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 ); /*=== saigPhase.c ==========================================================*/ extern Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int fIgnore, int fPrint, int fVerbose ); /*=== saigRetFwd.c ==========================================================*/ diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c index 5776cd4a..0bbf63f9 100644 --- a/src/aig/saig/saigBmc.c +++ b/src/aig/saig/saigBmc.c @@ -26,62 +26,172 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +#define AIG_VISITED ((Aig_Obj_t *)(PORT_PTRUINT_T)1) + +typedef struct Saig_Bmc_t_ Saig_Bmc_t; +struct Saig_Bmc_t_ +{ + // parameters + int nFramesMax; // the max number of timeframes to consider + int nConfMaxOne; // the max number of conflicts at a target + int nConfMaxAll; // the max number of conflicts for all targets + int nNodesMax; // the max number of nodes to add + int fVerbose; // enables verbose output + // AIG managers + Aig_Man_t * pAig; // the user's AIG manager + Aig_Man_t * pFrm; // Frames manager + Vec_Ptr_t * vVisited; // nodes visited in Frames + // node mapping + int nObjs; // the largest number of an AIG object + Vec_Ptr_t * vAig2Frm; // mapping of AIG nodees into Frames nodes + // SAT solver + sat_solver * pSat; // SAT solver + Vec_Int_t * vObj2Var; // mapping of frames objects in CNF variables + int nSatVars; // the number of used SAT variables + Vec_Ptr_t * vTargets; // targets to be solved in this interval + int iFramelast; // last frame + int iOutputLast; // last output +}; + +static inline int Saig_BmcSatNum( Saig_Bmc_t * p, Aig_Obj_t * pObj ) { return Vec_IntGetEntry( p->vObj2Var, pObj->Id ); } +static inline void Saig_BmcSetSatNum( Saig_Bmc_t * p, Aig_Obj_t * pObj, int Num ) { Vec_IntSetEntry(p->vObj2Var, pObj->Id, Num); } + +static inline Aig_Obj_t * Saig_BmcObjFrame( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i ) { return Vec_PtrGetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id ); } +static inline void Saig_BmcObjSetFrame( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { Vec_PtrSetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id, pNode ); } + +static inline Aig_Obj_t * Saig_BmcObjChild0( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_NotCond(Saig_BmcObjFrame(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)); } +static inline Aig_Obj_t * Saig_BmcObjChild1( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_NotCond(Saig_BmcObjFrame(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)); } + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* - Synopsis [Create timeframes of the manager for BMC.] + Synopsis [Create manager.] - Description [The resulting manager is combinational. POs correspond to \ - the property outputs in each time-frame.] + Description [] SideEffects [] SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManFramesBmc( Aig_Man_t * pAig, int nFrames ) +Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nConfMaxOne, int nConfMaxAll, int nNodesMax, int fVerbose ) { - Aig_Man_t * pFrames; - Aig_Obj_t * pObj, * pObjLi, * pObjLo; - int i, f; - assert( Saig_ManRegNum(pAig) > 0 ); - pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames ); - // map the constant node - Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames ); - // create variables for register outputs + Saig_Bmc_t * p; + Aig_Obj_t * pObj; + int i, Lit; + assert( Aig_ManRegNum(pAig) > 0 ); + p = (Saig_Bmc_t *)malloc( sizeof(Saig_Bmc_t) ); + memset( p, 0, sizeof(Saig_Bmc_t) ); + // set parameters + p->nFramesMax = 1000000; + p->nConfMaxOne = nConfMaxOne; + p->nConfMaxAll = nConfMaxAll; + p->nNodesMax = nNodesMax; + p->fVerbose = fVerbose; + p->pAig = pAig; + p->nObjs = Aig_ManObjNumMax(pAig); + // create node and variable mappings + p->vAig2Frm = Vec_PtrAlloc( 0 ); + Vec_PtrFill( p->vAig2Frm, 5 * p->nObjs, NULL ); + p->vObj2Var = Vec_IntAlloc( 0 ); + Vec_IntFill( p->vObj2Var, 5 * p->nObjs, 0 ); + // start the AIG manager and map primary inputs + p->pFrm = Aig_ManStart( 5 * p->nObjs ); Saig_ManForEachLo( pAig, pObj, i ) - pObj->pData = Aig_ManConst0( pFrames ); - // add timeframes - for ( f = 0; f < nFrames; f++ ) + Saig_BmcObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrm) ); + // create SAT solver + p->pSat = sat_solver_new(); + sat_solver_setnvars( p->pSat, 2000 ); + p->nSatVars = 1; + Lit = toLit( p->nSatVars ); + sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); + Saig_BmcSetSatNum( p, Aig_ManConst1(p->pFrm), p->nSatVars++ ); + // other data structures + p->vTargets = Vec_PtrAlloc( 0 ); + p->vVisited = Vec_PtrAlloc( 0 ); + return p; +} + +/**Function************************************************************* + + Synopsis [Delete manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_BmcManStop( Saig_Bmc_t * p ) +{ + Aig_ManStop( p->pFrm ); + Vec_PtrFree( p->vAig2Frm ); + Vec_IntFree( p->vObj2Var ); + sat_solver_delete( p->pSat ); + Vec_PtrFree( p->vTargets ); + Vec_PtrFree( p->vVisited ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Explores the possibility of constructing the output.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Saig_BmcIntervalExplore_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i ) +{ + Aig_Obj_t * pRes, * p0, * p1, * pConst1 = Aig_ManConst1(p->pAig); + pRes = Saig_BmcObjFrame( p, pObj, i ); + if ( pRes != NULL ) + return pRes; + if ( Saig_ObjIsPi( p->pAig, pObj ) ) + pRes = AIG_VISITED; + else if ( Saig_ObjIsLo( p->pAig, pObj ) ) + pRes = Saig_BmcIntervalExplore_rec( p, Saig_ObjLoToLi(p->pAig, pObj), i-1 ); + else if ( Aig_ObjIsPo( pObj ) ) { - // create PI nodes for this frame - Saig_ManForEachPi( pAig, pObj, i ) - pObj->pData = Aig_ObjCreatePi( pFrames ); - // add internal nodes of this frame - Aig_ManForEachNode( pAig, pObj, i ) - pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - // create POs for this frame - Saig_ManForEachPo( pAig, pObj, i ) - Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) ); - if ( f == nFrames - 1 ) - break; - // save register inputs - Saig_ManForEachLi( pAig, pObj, i ) - pObj->pData = Aig_ObjChild0Copy(pObj); - // transfer to register outputs - Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) - pObjLo->pData = pObjLi->pData; + pRes = Saig_BmcIntervalExplore_rec( p, Aig_ObjFanin0(pObj), i ); + if ( pRes != AIG_VISITED ) + pRes = Saig_BmcObjChild0( p, pObj, i ); + } + else + { + p0 = Saig_BmcIntervalExplore_rec( p, Aig_ObjFanin0(pObj), i ); + if ( p0 != AIG_VISITED ) + p0 = Saig_BmcObjChild0( p, pObj, i ); + p1 = Saig_BmcIntervalExplore_rec( p, Aig_ObjFanin1(pObj), i ); + if ( p1 != AIG_VISITED ) + p1 = Saig_BmcObjChild1( p, pObj, i ); + + if ( p0 == Aig_Not(p1) ) + pRes = Aig_Not(pConst1); + else if ( Aig_Regular(p0) == pConst1 ) + pRes = (p0 == pConst1) ? p1 : Aig_Not(pConst1); + else if ( Aig_Regular(p1) == pConst1 ) + pRes = (p1 == pConst1) ? p0 : Aig_Not(pConst1); + else + pRes = AIG_VISITED; + + if ( pRes != pConst1 && pRes != Aig_Not(pConst1) ) + pRes = AIG_VISITED; } - Aig_ManCleanup( pFrames ); - return pFrames; + Saig_BmcObjSetFrame( p, pObj, i, pRes ); + return pRes; } /**Function************************************************************* - Synopsis [Returns the number of internal nodes that are not counted yet.] + Synopsis [Performs the actual construction of the output.] Description [] @@ -90,81 +200,70 @@ Aig_Man_t * Saig_ManFramesBmc( Aig_Man_t * pAig, int nFrames ) SeeAlso [] ***********************************************************************/ -int Saig_ManFramesCount_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) +Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i ) { - if ( !Aig_ObjIsNode(pObj) ) - return 0; - if ( Aig_ObjIsTravIdCurrent(p, pObj) ) - return 0; - Aig_ObjSetTravIdCurrent(p, pObj); - return 1 + Saig_ManFramesCount_rec( p, Aig_ObjFanin0(pObj) ) + - Saig_ManFramesCount_rec( p, Aig_ObjFanin1(pObj) ); + Aig_Obj_t * pRes; + pRes = Saig_BmcObjFrame( p, pObj, i ); + assert( pRes != NULL ); + if ( pRes != AIG_VISITED ) + return pRes; + if ( Saig_ObjIsPi( p->pAig, pObj ) ) + pRes = Aig_ObjCreatePi(p->pFrm); + else if ( Saig_ObjIsLo( p->pAig, pObj ) ) + pRes = Saig_BmcIntervalConstruct_rec( p, Saig_ObjLoToLi(p->pAig, pObj), i-1 ); + else if ( Aig_ObjIsPo( pObj ) ) + { + Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin0(pObj), i ); + pRes = Saig_BmcObjChild0( p, pObj, i ); + } + else + { + Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin0(pObj), i ); + Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin1(pObj), i ); + pRes = Aig_And( p->pFrm, Saig_BmcObjChild0(p, pObj, i), Saig_BmcObjChild1(p, pObj, i) ); + } + Saig_BmcObjSetFrame( p, pObj, i, pRes ); + return pRes; } /**Function************************************************************* - Synopsis [Create timeframes of the manager for BMC.] + Synopsis [Adds new AIG nodes to the frames.] - Description [The resulting manager is combinational. POs correspond to - the property outputs in each time-frame. - The unrolling is stopped as soon as the number of nodes in the frames - exceeds the given maximum size.] + Description [] SideEffects [] SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax ) +void Saig_BmcInterval( Saig_Bmc_t * p ) { - Aig_Man_t * pFrames; - Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjPo; - int i, f, Counter = 0; - assert( Saig_ManRegNum(pAig) > 0 ); - pFrames = Aig_ManStart( nSizeMax ); - Aig_ManIncrementTravId( pFrames ); - // map the constant node - Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames ); - // create variables for register outputs - Saig_ManForEachLo( pAig, pObj, i ) - pObj->pData = Aig_ManConst0( pFrames ); - // add timeframes - Counter = 0; - for ( f = 0; f < nFrames; f++ ) + Aig_Obj_t * pTarget, * pObj; + int i, nNodes = Aig_ManNodeNum( p->pFrm ); + Vec_PtrClear( p->vTargets ); + for ( ; p->iFramelast < p->nFramesMax; p->iFramelast++, p->iOutputLast = 0 ) { - // create PI nodes for this frame - Saig_ManForEachPi( pAig, pObj, i ) - pObj->pData = Aig_ObjCreatePi( pFrames ); - // add internal nodes of this frame - Aig_ManForEachNode( pAig, pObj, i ) - pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - // create POs for this frame - Saig_ManForEachPo( pAig, pObj, i ) + if ( p->iOutputLast == 0 ) { - pObjPo = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) ); - Counter += Saig_ManFramesCount_rec( pFrames, Aig_ObjFanin0(pObjPo) ); + Saig_BmcObjSetFrame( p, Aig_ManConst1(p->pAig), p->iFramelast, Aig_ManConst1(p->pFrm) ); + Saig_ManForEachPi( p->pAig, pObj, i ) + Saig_BmcObjSetFrame( p, pObj, p->iFramelast, Aig_ObjCreatePi(p->pFrm) ); } - if ( Counter >= nSizeMax ) + for ( ; p->iOutputLast < Saig_ManPoNum(p->pAig); p->iOutputLast++ ) { - Aig_ManCleanup( pFrames ); - return pFrames; + if ( Aig_ManNodeNum(p->pFrm) >= nNodes + p->nNodesMax ) + return; + Saig_BmcIntervalExplore_rec( p, Aig_ManPo(p->pAig, p->iOutputLast), p->nFramesMax ); + pTarget = Saig_BmcIntervalConstruct_rec( p, Aig_ManPo(p->pAig, p->iOutputLast), p->nFramesMax ); + Vec_PtrPush( p->vTargets, pTarget ); } - if ( f == nFrames - 1 ) - break; - // save register inputs - Saig_ManForEachLi( pAig, pObj, i ) - pObj->pData = Aig_ObjChild0Copy(pObj); - // transfer to register outputs - Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) - pObjLo->pData = pObjLi->pData; } - Aig_ManCleanup( pFrames ); - return pFrames; } /**Function************************************************************* - Synopsis [Performs BMC for the given AIG.] + Synopsis [Performs the actual construction of the output.] Description [] @@ -173,140 +272,179 @@ Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax SeeAlso [] ***********************************************************************/ -int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLimit, int fRewrite, int fVerbose, int * piFrame ) +Aig_Obj_t * Saig_BmcIntervalToAig_rec( Saig_Bmc_t * p, Aig_Man_t * pNew, Aig_Obj_t * pObj ) { - sat_solver * pSat; - Cnf_Dat_t * pCnf; - Aig_Man_t * pFrames, * pAigTemp; - Aig_Obj_t * pObj; - int status, clk, Lit, i, RetValue = 1; - // derive the timeframes - clk = clock(); - if ( nSizeMax > 0 ) - { - pFrames = Saig_ManFramesBmcLimit( pAig, nFrames, nSizeMax ); - nFrames = Aig_ManPoNum(pFrames) / Saig_ManPoNum(pAig) + ((Aig_ManPoNum(pFrames) % Saig_ManPoNum(pAig)) > 0); - } - else - pFrames = Saig_ManFramesBmc( pAig, nFrames ); - if ( piFrame ) - *piFrame = nFrames; - if ( fVerbose ) + if ( pObj->pData ) + return pObj->pData; + Vec_PtrPush( p->vVisited, pObj ); + if ( Saig_BmcSatNum(p, pObj) || Aig_ObjIsPi(pObj) ) + return pObj->pData = Aig_ObjCreatePi(pNew); + Saig_BmcIntervalToAig_rec( p, pNew, Aig_ObjFanin0(pObj) ); + Saig_BmcIntervalToAig_rec( p, pNew, Aig_ObjFanin1(pObj) ); + return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Creates AIG of the newly added nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_BmcIntervalToAig( Saig_Bmc_t * p ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj, * pObjNew; + int i; + pNew = Aig_ManStart( p->nNodesMax ); + Aig_ManConst1(p->pFrm)->pData = Aig_ManConst1(pNew); + Vec_PtrClear( p->vVisited ); + Vec_PtrPush( p->vVisited, Aig_ManConst1(p->pFrm) ); + Vec_PtrForEachEntry( p->vTargets, pObj, i ) { - printf( "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n", - Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig), - Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) ); - printf( "Time-frames (%d): PI/PO = %d/%d. Node = %6d. Lev = %5d. ", - nFrames, Aig_ManPiNum(pFrames), Aig_ManPoNum(pFrames), - Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) ); - PRT( "Time", clock() - clk ); - fflush( stdout ); + pObjNew = Saig_BmcIntervalToAig_rec( p, pNew, Aig_Regular(pObj) ); + Aig_ObjCreatePo( pNew, pObjNew ); } - // rewrite the timeframes - if ( fRewrite ) + return pNew; +} + +/**Function************************************************************* + + Synopsis [Derives CNF for the newly added nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_BmcLoadCnf( Saig_Bmc_t * p, Cnf_Dat_t * pCnf ) +{ + Aig_Obj_t * pObj, * pObjNew; + int i, Lits[2], VarNumOld, VarNumNew; + Vec_PtrForEachEntry( p->vVisited, pObj, i ) { - clk = clock(); -// pFrames = Dar_ManBalance( pAigTemp = pFrames, 0 ); - pFrames = Dar_ManRwsat( pAigTemp = pFrames, 1, 0 ); - Aig_ManStop( pAigTemp ); - if ( fVerbose ) + pObjNew = pObj->pData; + pObj->pData = NULL; + VarNumNew = pCnf->pVarNums[ pObjNew->Id ]; + if ( VarNumNew == -1 ) + continue; + VarNumOld = Saig_BmcSatNum( p, pObj ); + if ( VarNumOld == 0 ) { - printf( "Time-frames after rewriting: Node = %6d. Lev = %5d. ", - Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) ); - PRT( "Time", clock() - clk ); - fflush( stdout ); + Saig_BmcSetSatNum( p, pObj, VarNumNew ); + continue; } - } - // create the SAT solver - clk = clock(); - pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) ); - pSat = sat_solver_new(); - sat_solver_setnvars( pSat, pCnf->nVars ); - for ( i = 0; i < pCnf->nClauses; i++ ) - { - if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) + // add clauses connecting existing variables + Lits[0] = toLitCond( VarNumOld, 0 ); + Lits[1] = toLitCond( VarNumNew, 1 ); + if ( !sat_solver_addclause( p->pSat, Lits, Lits+2 ) ) + assert( 0 ); + Lits[0] = toLitCond( VarNumOld, 1 ); + Lits[1] = toLitCond( VarNumNew, 0 ); + if ( !sat_solver_addclause( p->pSat, Lits, Lits+2 ) ) assert( 0 ); } - if ( fVerbose ) + // add CNF to the SAT solver + for ( i = 0; i < pCnf->nClauses; i++ ) + if ( !sat_solver_addclause( p->pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) + break; + if ( i < pCnf->nClauses ) + printf( "SAT solver became UNSAT after adding clauses.\n" ); +} + +/**Function************************************************************* + + Synopsis [Solves targets with the given resource limit.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_BmcSolveTargets( Saig_Bmc_t * p ) +{ + Aig_Obj_t * pObj; + int i, VarNum, Lit, RetValue; + assert( Vec_PtrSize(p->vTargets) > 0 ); + Vec_PtrForEachEntry( p->vTargets, pObj, i ) { - printf( "CNF: Variables = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals ); - PRT( "Time", clock() - clk ); - fflush( stdout ); + if ( p->pSat->stats.conflicts > p->nConfMaxAll ) + return l_Undef; + VarNum = Saig_BmcSatNum( p, Aig_Regular(pObj) ); + Lit = toLitCond( VarNum, Aig_IsComplement(pObj) ); + RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (sint64)p->nConfMaxOne, (sint64)0, (sint64)0, (sint64)0 ); + if ( RetValue == l_False ) // unsat + continue; + if ( RetValue == l_Undef ) // undecided + return l_Undef; + // generate counter-example + return l_True; } - status = sat_solver_simplify(pSat); - if ( status == 0 ) + return l_False; +} + +/**Function************************************************************* + + Synopsis [Performs BMC with the given parameters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_BmcPerform( Aig_Man_t * pAig, int nConfMaxOne, int nConfMaxAll, int nNodesMax, int fVerbose ) +{ + Saig_Bmc_t * p; + Aig_Man_t * pNew; + Cnf_Dat_t * pCnf; + int RetValue, clk = clock(); + p = Saig_BmcManStart( pAig, nConfMaxOne, nConfMaxAll, nNodesMax, fVerbose ); + while ( 1 ) { - if ( fVerbose ) - { - printf( "The BMC problem is trivially UNSAT\n" ); - fflush( stdout ); - } + // add new logic slice to frames + Saig_BmcInterval( p ); + if ( Vec_PtrSize(p->vTargets) == 0 ) + break; + // convert logic slice into new AIG + pNew = Saig_BmcIntervalToAig( p ); + // derive CNF for the new AIG + pCnf = Cnf_Derive( pNew, Aig_ManPoNum(pNew) ); + Cnf_DataLift( pCnf, p->nSatVars ); + p->nSatVars += pCnf->nVars; + // add this CNF to the solver + Saig_BmcLoadCnf( p, pCnf ); + Cnf_DataFree( pCnf ); + Aig_ManStop( pNew ); + // solve the targets + RetValue = Saig_BmcSolveTargets( p ); + if ( RetValue != l_False ) + break; } + if ( RetValue == l_True ) + printf( "BMC failed for output %d in frame %d. ", p->iOutputLast, p->iFramelast ); + else // if ( RetValue == l_False || RetValue == l_Undef ) + printf( "BMC completed for %d timeframes. ", p->iFramelast ); + PRT( "Time", clock() - clk ); + if ( p->iFramelast >= p->nFramesMax ) + printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax ); + else if ( p->pSat->stats.conflicts > p->nConfMaxAll ) + printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll ); else - { - int clkPart = clock(); - Aig_ManForEachPo( pFrames, pObj, i ) - { - Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 ); - if ( fVerbose ) - { - printf( "Solving output %2d of frame %3d ... \r", - i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) ); - } - clk = clock(); - status = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 ); - if ( fVerbose && (i % Saig_ManPoNum(pAig) == Saig_ManPoNum(pAig) - 1) ) - { - printf( "Solved %2d outputs of frame %3d. ", - Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) ); - printf( "Conf =%8.0f. Imp =%11.0f. ", (double)pSat->stats.conflicts, (double)pSat->stats.propagations ); - PRT( "T", clock() - clkPart ); - clkPart = clock(); - fflush( stdout ); - } - if ( status == l_False ) - { -/* - Lit = lit_neg( Lit ); - RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 ); - assert( RetValue ); - if ( pSat->qtail != pSat->qhead ) - { - RetValue = sat_solver_simplify(pSat); - assert( RetValue ); - } -*/ - } - else if ( status == l_True ) - { - extern void * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel ); - Vec_Int_t * vCiIds = Cnf_DataCollectPiSatNums( pCnf, pFrames ); - int * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize ); - pModel[Aig_ManPiNum(pFrames)] = pObj->Id; - pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pFrames, pModel ); - free( pModel ); - Vec_IntFree( vCiIds ); - -// if ( piFrame ) -// *piFrame = i / Saig_ManPoNum(pAig); - RetValue = 0; - break; - } - else - { - if ( piFrame ) - *piFrame = i / Saig_ManPoNum(pAig); - RetValue = -1; - break; - } - } - } - sat_solver_delete( pSat ); - Cnf_DataFree( pCnf ); - Aig_ManStop( pFrames ); - return RetValue; + printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne ); + Saig_BmcManStop( p ); } + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c new file mode 100644 index 00000000..5776cd4a --- /dev/null +++ b/src/aig/saig/saigBmc2.c @@ -0,0 +1,314 @@ +/**CFile**************************************************************** + + FileName [saigBmc.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Sequential AIG package.] + + Synopsis [Simple BMC package.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: saigBmc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "saig.h" +#include "cnf.h" +#include "satStore.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Create timeframes of the manager for BMC.] + + Description [The resulting manager is combinational. POs correspond to \ + the property outputs in each time-frame.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManFramesBmc( Aig_Man_t * pAig, int nFrames ) +{ + Aig_Man_t * pFrames; + Aig_Obj_t * pObj, * pObjLi, * pObjLo; + int i, f; + assert( Saig_ManRegNum(pAig) > 0 ); + pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames ); + // map the constant node + Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames ); + // create variables for register outputs + Saig_ManForEachLo( pAig, pObj, i ) + pObj->pData = Aig_ManConst0( pFrames ); + // add timeframes + for ( f = 0; f < nFrames; f++ ) + { + // create PI nodes for this frame + Saig_ManForEachPi( pAig, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pFrames ); + // add internal nodes of this frame + Aig_ManForEachNode( pAig, pObj, i ) + pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + // create POs for this frame + Saig_ManForEachPo( pAig, pObj, i ) + Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) ); + if ( f == nFrames - 1 ) + break; + // save register inputs + Saig_ManForEachLi( pAig, pObj, i ) + pObj->pData = Aig_ObjChild0Copy(pObj); + // transfer to register outputs + Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) + pObjLo->pData = pObjLi->pData; + } + Aig_ManCleanup( pFrames ); + return pFrames; +} + +/**Function************************************************************* + + Synopsis [Returns the number of internal nodes that are not counted yet.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManFramesCount_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + if ( !Aig_ObjIsNode(pObj) ) + return 0; + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return 0; + Aig_ObjSetTravIdCurrent(p, pObj); + return 1 + Saig_ManFramesCount_rec( p, Aig_ObjFanin0(pObj) ) + + Saig_ManFramesCount_rec( p, Aig_ObjFanin1(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Create timeframes of the manager for BMC.] + + Description [The resulting manager is combinational. POs correspond to + the property outputs in each time-frame. + The unrolling is stopped as soon as the number of nodes in the frames + exceeds the given maximum size.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax ) +{ + Aig_Man_t * pFrames; + Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjPo; + int i, f, Counter = 0; + assert( Saig_ManRegNum(pAig) > 0 ); + pFrames = Aig_ManStart( nSizeMax ); + Aig_ManIncrementTravId( pFrames ); + // map the constant node + Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames ); + // create variables for register outputs + Saig_ManForEachLo( pAig, pObj, i ) + pObj->pData = Aig_ManConst0( pFrames ); + // add timeframes + Counter = 0; + for ( f = 0; f < nFrames; f++ ) + { + // create PI nodes for this frame + Saig_ManForEachPi( pAig, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pFrames ); + // add internal nodes of this frame + Aig_ManForEachNode( pAig, pObj, i ) + pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + // create POs for this frame + Saig_ManForEachPo( pAig, pObj, i ) + { + pObjPo = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) ); + Counter += Saig_ManFramesCount_rec( pFrames, Aig_ObjFanin0(pObjPo) ); + } + if ( Counter >= nSizeMax ) + { + Aig_ManCleanup( pFrames ); + return pFrames; + } + if ( f == nFrames - 1 ) + break; + // save register inputs + Saig_ManForEachLi( pAig, pObj, i ) + pObj->pData = Aig_ObjChild0Copy(pObj); + // transfer to register outputs + Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) + pObjLo->pData = pObjLi->pData; + } + Aig_ManCleanup( pFrames ); + return pFrames; +} + +/**Function************************************************************* + + Synopsis [Performs BMC for the given AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLimit, int fRewrite, int fVerbose, int * piFrame ) +{ + sat_solver * pSat; + Cnf_Dat_t * pCnf; + Aig_Man_t * pFrames, * pAigTemp; + Aig_Obj_t * pObj; + int status, clk, Lit, i, RetValue = 1; + // derive the timeframes + clk = clock(); + if ( nSizeMax > 0 ) + { + pFrames = Saig_ManFramesBmcLimit( pAig, nFrames, nSizeMax ); + nFrames = Aig_ManPoNum(pFrames) / Saig_ManPoNum(pAig) + ((Aig_ManPoNum(pFrames) % Saig_ManPoNum(pAig)) > 0); + } + else + pFrames = Saig_ManFramesBmc( pAig, nFrames ); + if ( piFrame ) + *piFrame = nFrames; + if ( fVerbose ) + { + printf( "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n", + Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig), + Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) ); + printf( "Time-frames (%d): PI/PO = %d/%d. Node = %6d. Lev = %5d. ", + nFrames, Aig_ManPiNum(pFrames), Aig_ManPoNum(pFrames), + Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) ); + PRT( "Time", clock() - clk ); + fflush( stdout ); + } + // rewrite the timeframes + if ( fRewrite ) + { + clk = clock(); +// pFrames = Dar_ManBalance( pAigTemp = pFrames, 0 ); + pFrames = Dar_ManRwsat( pAigTemp = pFrames, 1, 0 ); + Aig_ManStop( pAigTemp ); + if ( fVerbose ) + { + printf( "Time-frames after rewriting: Node = %6d. Lev = %5d. ", + Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) ); + PRT( "Time", clock() - clk ); + fflush( stdout ); + } + } + // create the SAT solver + clk = clock(); + pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) ); + pSat = sat_solver_new(); + sat_solver_setnvars( pSat, pCnf->nVars ); + for ( i = 0; i < pCnf->nClauses; i++ ) + { + if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) + assert( 0 ); + } + if ( fVerbose ) + { + printf( "CNF: Variables = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals ); + PRT( "Time", clock() - clk ); + fflush( stdout ); + } + status = sat_solver_simplify(pSat); + if ( status == 0 ) + { + if ( fVerbose ) + { + printf( "The BMC problem is trivially UNSAT\n" ); + fflush( stdout ); + } + } + else + { + int clkPart = clock(); + Aig_ManForEachPo( pFrames, pObj, i ) + { + Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 ); + if ( fVerbose ) + { + printf( "Solving output %2d of frame %3d ... \r", + i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) ); + } + clk = clock(); + status = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 ); + if ( fVerbose && (i % Saig_ManPoNum(pAig) == Saig_ManPoNum(pAig) - 1) ) + { + printf( "Solved %2d outputs of frame %3d. ", + Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) ); + printf( "Conf =%8.0f. Imp =%11.0f. ", (double)pSat->stats.conflicts, (double)pSat->stats.propagations ); + PRT( "T", clock() - clkPart ); + clkPart = clock(); + fflush( stdout ); + } + if ( status == l_False ) + { +/* + Lit = lit_neg( Lit ); + RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 ); + assert( RetValue ); + if ( pSat->qtail != pSat->qhead ) + { + RetValue = sat_solver_simplify(pSat); + assert( RetValue ); + } +*/ + } + else if ( status == l_True ) + { + extern void * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel ); + Vec_Int_t * vCiIds = Cnf_DataCollectPiSatNums( pCnf, pFrames ); + int * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize ); + pModel[Aig_ManPiNum(pFrames)] = pObj->Id; + pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pFrames, pModel ); + free( pModel ); + Vec_IntFree( vCiIds ); + +// if ( piFrame ) +// *piFrame = i / Saig_ManPoNum(pAig); + RetValue = 0; + break; + } + else + { + if ( piFrame ) + *piFrame = i / Saig_ManPoNum(pAig); + RetValue = -1; + break; + } + } + } + sat_solver_delete( pSat ); + Cnf_DataFree( pCnf ); + Aig_ManStop( pFrames ); + return RetValue; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c index 5efcd24d..cc71f371 100644 --- a/src/aig/saig/saigMiter.c +++ b/src/aig/saig/saigMiter.c @@ -49,6 +49,8 @@ Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p0, Aig_Man_t * p1, int Oper ) assert( Saig_ManPoNum(p0) == Saig_ManPoNum(p1) ); pNew = Aig_ManStart( Aig_ManObjNumMax(p0) + Aig_ManObjNumMax(p1) ); pNew->pName = Aig_UtilStrsav( "miter" ); + Aig_ManCleanData( p0 ); + Aig_ManCleanData( p1 ); // map constant nodes Aig_ManConst1(p0)->pData = Aig_ManConst1(pNew); Aig_ManConst1(p1)->pData = Aig_ManConst1(pNew); @@ -85,7 +87,7 @@ Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p0, Aig_Man_t * p1, int Oper ) pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); // cleanup Aig_ManSetRegNum( pNew, Saig_ManRegNum(p0) + Saig_ManRegNum(p1) ); - Aig_ManCleanup( pNew ); +// Aig_ManCleanup( pNew ); return pNew; } @@ -184,6 +186,9 @@ Aig_Man_t * Saig_ManUnrollTwo( Aig_Man_t * pBot, Aig_Man_t * pTop, int nFrames ) Aig_ObjCreatePo( p, Aig_ObjChild0Copy(pObj) ); break; } + // create POs for this frame + Saig_ManForEachPo( pAig, pObj, i ) + Aig_ObjCreatePo( p, Aig_ObjChild0Copy(pObj) ); // save register inputs Saig_ManForEachLi( pAig, pObj, i ) pObj->pData = Aig_ObjChild0Copy(pObj); @@ -213,7 +218,7 @@ Aig_Man_t * Saig_ManUnrollTwo( Aig_Man_t * pBot, Aig_Man_t * pTop, int nFrames ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Aig_ManDupNodes_old( Aig_Man_t * p, Vec_Ptr_t * vSet ) +Aig_Man_t * Aig_ManDupNodesAll( Aig_Man_t * p, Vec_Ptr_t * vSet ) { Aig_Man_t * pNew, * pCopy; Aig_Obj_t * pObj; @@ -250,7 +255,7 @@ Aig_Man_t * Aig_ManDupNodes_old( Aig_Man_t * p, Vec_Ptr_t * vSet ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Aig_ManDupNodes( Aig_Man_t * p, Vec_Ptr_t * vSet, int iPart ) +Aig_Man_t * Aig_ManDupNodesHalf( Aig_Man_t * p, Vec_Ptr_t * vSet, int iPart ) { Aig_Man_t * pNew, * pCopy; Aig_Obj_t * pObj; @@ -337,6 +342,79 @@ int Saig_ManDemiterSimple( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAi Vec_PtrFree( vSet1 ); return 0; } + if ( Aig_ObjFaninC0(pObj) ) + pObj0 = Aig_Not(pObj0); + +// printf( "%d %d ", Aig_Regular(pObj0)->Id, Aig_Regular(pObj1)->Id ); + if ( Aig_Regular(pObj0)->Id < Aig_Regular(pObj1)->Id ) + { + Vec_PtrPush( vSet0, pObj0 ); + Vec_PtrPush( vSet1, pObj1 ); + } + else + { + Vec_PtrPush( vSet0, pObj1 ); + Vec_PtrPush( vSet1, pObj0 ); + } + } +// printf( "Miter has %d constant outputs.\n", Counter ); +// printf( "\n" ); + if ( ppAig0 ) + { + *ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 ); + FREE( (*ppAig0)->pName ); + (*ppAig0)->pName = Aig_UtilStrsav( "part0" ); + } + if ( ppAig1 ) + { + *ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 ); + FREE( (*ppAig1)->pName ); + (*ppAig1)->pName = Aig_UtilStrsav( "part1" ); + } + Vec_PtrFree( vSet0 ); + Vec_PtrFree( vSet1 ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Duplicates the AIG to have constant-0 initial state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManDemiterSimpleDiff( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 ) +{ + Vec_Ptr_t * vSet0, * vSet1; + Aig_Obj_t * pObj, * pFanin, * pObj0, * pObj1; + int i, Counter = 0; + assert( Saig_ManRegNum(p) % 2 == 0 ); + vSet0 = Vec_PtrAlloc( Saig_ManPoNum(p) ); + vSet1 = Vec_PtrAlloc( Saig_ManPoNum(p) ); + Saig_ManForEachPo( p, pObj, i ) + { + pFanin = Aig_ObjFanin0(pObj); + if ( Aig_ObjIsConst1( pFanin ) ) + { + if ( !Aig_ObjFaninC0(pObj) ) + printf( "The output number %d of the miter is constant 1.\n", i ); + Counter++; + continue; + } + if ( !Aig_ObjIsNode(pFanin) || !Aig_ObjRecognizeExor( pFanin, &pObj0, &pObj1 ) ) + { + printf( "The miter cannot be demitered.\n" ); + Vec_PtrFree( vSet0 ); + Vec_PtrFree( vSet1 ); + return 0; + } + if ( Aig_ObjFaninC0(pObj) ) + pObj0 = Aig_Not(pObj0); + // printf( "%d %d ", Aig_Regular(pObj0)->Id, Aig_Regular(pObj1)->Id ); if ( Aig_Regular(pObj0)->Id < Aig_Regular(pObj1)->Id ) { @@ -353,13 +431,13 @@ int Saig_ManDemiterSimple( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAi // printf( "\n" ); if ( ppAig0 ) { - *ppAig0 = Aig_ManDupNodes( p, vSet0, 0 ); + *ppAig0 = Aig_ManDupNodesAll( p, vSet0 ); FREE( (*ppAig0)->pName ); (*ppAig0)->pName = Aig_UtilStrsav( "part0" ); } if ( ppAig1 ) { - *ppAig1 = Aig_ManDupNodes( p, vSet1, 1 ); + *ppAig1 = Aig_ManDupNodesAll( p, vSet1 ); FREE( (*ppAig1)->pName ); (*ppAig1)->pName = Aig_UtilStrsav( "part1" ); } @@ -525,14 +603,14 @@ int Saig_ManDemiter( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 ) if ( ppAig0 ) { assert( 0 ); - *ppAig0 = Aig_ManDupNodes( p, vSet0, 0 ); // not ready + *ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 ); // not ready FREE( (*ppAig0)->pName ); (*ppAig0)->pName = Aig_UtilStrsav( "part0" ); } if ( ppAig1 ) { assert( 0 ); - *ppAig1 = Aig_ManDupNodes( p, vSet1, 1 ); // not ready + *ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 ); // not ready FREE( (*ppAig1)->pName ); (*ppAig1)->pName = Aig_UtilStrsav( "part1" ); } @@ -566,6 +644,42 @@ Aig_Man_t * Saig_ManCreateMiterTwo( Aig_Man_t * pOld, Aig_Man_t * pNew, int nFra return pMiter; } + +/**Function************************************************************* + + Synopsis [Resimulates counter-example and returns the failed output number.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_SecCexResimulate( Aig_Man_t * p, int * pModel, int * pnOutputs ) +{ + Aig_Obj_t * pObj; + int i, RetValue = -1; + *pnOutputs = 0; + Aig_ManConst1(p)->fMarkA = 1; + Aig_ManForEachPi( p, pObj, i ) + pObj->fMarkA = pModel[i]; + Aig_ManForEachNode( p, pObj, i ) + pObj->fMarkA = ( Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj) ) & + ( Aig_ObjFanin1(pObj)->fMarkA ^ Aig_ObjFaninC1(pObj) ); + Aig_ManForEachPo( p, pObj, i ) + pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj); + Aig_ManForEachPo( p, pObj, i ) + if ( pObj->fMarkA ) + { + if ( RetValue == -1 ) + RetValue = i; + (*pnOutputs)++; + } + Aig_ManCleanMarkA(p); + return RetValue; +} + /**Function************************************************************* Synopsis [Reduces SEC to CEC for the special case of seq synthesis.] @@ -578,12 +692,16 @@ Aig_Man_t * Saig_ManCreateMiterTwo( Aig_Man_t * pOld, Aig_Man_t * pNew, int nFra SeeAlso [] ***********************************************************************/ -int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int fVerbose ) +int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int nFrames, int fVerbose ) { extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose ); - int nFrames = 2; // modify to enable comparison over any number of frames + int iOut, nOuts; Aig_Man_t * pMiterCec; int RetValue, clkTotal = clock(); + Aig_ManPrintStats( pPart0 ); + Aig_ManPrintStats( pPart1 ); +// Aig_ManDumpBlif( pPart0, "file0.blif", NULL, NULL ); +// Aig_ManDumpBlif( pPart1, "file1.blif", NULL, NULL ); // assert( Aig_ManNodeNum(pPart0) <= Aig_ManNodeNum(pPart1) ); if ( Aig_ManNodeNum(pPart0) >= Aig_ManNodeNum(pPart1) ) { @@ -605,7 +723,6 @@ int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int fVerbose ) // transfer model if given // if ( pNtk2 == NULL ) // pNtk1->pModel = pMiterCec->pData, pMiterCec->pData = NULL; - Aig_ManStop( pMiterCec ); // report the miter if ( RetValue == 1 ) { @@ -616,6 +733,24 @@ PRT( "Time", clock() - clkTotal ); { printf( "Networks are NOT EQUIVALENT. " ); PRT( "Time", clock() - clkTotal ); + if ( pMiterCec->pData == NULL ) + printf( "Counter-example is not available.\n" ); + else + { + iOut = Ssw_SecCexResimulate( pMiterCec, pMiterCec->pData, &nOuts ); + if ( iOut == -1 ) + printf( "Counter-example verification has failed.\n" ); + else + { + if ( iOut < Saig_ManPoNum(pPart0) * nFrames ) + printf( "Primary output %d has failed in frame %d.\n", + iOut%Saig_ManPoNum(pPart0), iOut/Saig_ManPoNum(pPart0) ); + else + printf( "Flop input %d has failed in the last frame.\n", + iOut - Saig_ManPoNum(pPart0) * nFrames ); + printf( "The counter-example detected %d incorrect POs or flop inputs.\n", nOuts ); + } + } } else { @@ -623,6 +758,7 @@ PRT( "Time", clock() - clkTotal ); PRT( "Time", clock() - clkTotal ); } fflush( stdout ); + Aig_ManStop( pMiterCec ); return RetValue; } @@ -639,6 +775,7 @@ PRT( "Time", clock() - clkTotal ); ***********************************************************************/ int Ssw_SecSpecialMiter( Aig_Man_t * pMiter, int fVerbose ) { + int nFrames = 2; // modify to enable comparison over any number of frames Aig_Man_t * pPart0, * pPart1; int RetValue; if ( fVerbose ) @@ -657,7 +794,7 @@ int Ssw_SecSpecialMiter( Aig_Man_t * pMiter, int fVerbose ) // Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL ); // printf( "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" ); } - RetValue = Ssw_SecSpecial( pPart0, pPart1, fVerbose ); + RetValue = Ssw_SecSpecial( pPart0, pPart1, nFrames, fVerbose ); Aig_ManStop( pPart0 ); Aig_ManStop( pPart1 ); return RetValue; diff --git a/src/aig/saig/saigSynch.c b/src/aig/saig/saigSynch.c index eb0fefc9..c52f2f48 100644 --- a/src/aig/saig/saigSynch.c +++ b/src/aig/saig/saigSynch.c @@ -632,6 +632,7 @@ Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords, pAig1z = Saig_ManDupInitZero( pAig1 ); pAig2z = Saig_ManDupInitZero( pAig2 ); pMiter = Saig_ManCreateMiter( pAig1z, pAig2z, 0 ); + Aig_ManCleanup( pMiter ); Aig_ManStop( pAig1z ); Aig_ManStop( pAig2z ); diff --git a/src/aig/ssw/module.make b/src/aig/ssw/module.make index a7d940b4..1e79c955 100644 --- a/src/aig/ssw/module.make +++ b/src/aig/ssw/module.make @@ -4,6 +4,7 @@ SRC += src/aig/ssw/sswAig.c \ src/aig/ssw/sswCnf.c \ src/aig/ssw/sswCore.c \ src/aig/ssw/sswDyn.c \ + src/aig/ssw/sswIslands.c \ src/aig/ssw/sswLcorr.c \ src/aig/ssw/sswMan.c \ src/aig/ssw/sswPart.c \ diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h index 73226dbe..4bb2356a 100644 --- a/src/aig/ssw/ssw.h +++ b/src/aig/ssw/ssw.h @@ -104,6 +104,7 @@ extern int Ssw_SecSpecialMiter( Aig_Man_t * pMiter, int fVerbose ); /*=== sswPart.c ==========================================================*/ extern Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars ); /*=== sswPairs.c ===================================================*/ +extern int Ssw_MiterStatus( Aig_Man_t * p, int fVerbose ); extern int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars ); extern int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars ); extern int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars ); diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c index f234a58f..3dfee28b 100644 --- a/src/aig/ssw/sswClass.c +++ b/src/aig/ssw/sswClass.c @@ -446,7 +446,7 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj ) assert( p->pId2Class[pObj->Id] == NULL ); pRepr = Aig_ObjRepr( p->pAig, pObj ); assert( pRepr != NULL ); - Vec_PtrPush( p->vRefined, pObj ); +// Vec_PtrPush( p->vRefined, pObj ); if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) ) { assert( p->pClassSizes[pRepr->Id] == 0 ); @@ -455,7 +455,7 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj ) p->nCands1--; return; } - Vec_PtrPush( p->vRefined, pRepr ); +// Vec_PtrPush( p->vRefined, pRepr ); Aig_ObjSetRepr( p->pAig, pObj, NULL ); assert( p->pId2Class[pRepr->Id][0] == pRepr ); assert( p->pClassSizes[pRepr->Id] >= 2 ); @@ -791,6 +791,48 @@ Ssw_Cla_t * Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses ) return p; } +/**Function************************************************************* + + Synopsis [Creates classes from the temporary representation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ssw_Cla_t * Ssw_ClassesFromIslands( Aig_Man_t * pMiter, Vec_Int_t * vPairs ) +{ + Ssw_Cla_t * p; + Aig_Obj_t ** ppClassNew; + Aig_Obj_t * pObj, * pRepr; + int i; + // start the classes + p = Ssw_ClassesStart( pMiter ); + // allocate memory for classes + p->pMemClasses = ALLOC( Aig_Obj_t *, Vec_IntSize(vPairs) ); + // create classes + for ( i = 0; i < Vec_IntSize(vPairs); i += 2 ) + { + pRepr = Aig_ManObj( pMiter, Vec_IntEntry(vPairs, i) ); + pObj = Aig_ManObj( pMiter, Vec_IntEntry(vPairs, i+1) ); + assert( Aig_ObjId(pRepr) < Aig_ObjId(pObj) ); + Aig_ObjSetRepr( pMiter, pObj, pRepr ); + // get room for storing the class + ppClassNew = p->pMemClasses + i; + ppClassNew[0] = pRepr; + ppClassNew[1] = pObj; + // create new class + Ssw_ObjAddClass( p, pRepr, ppClassNew, 2 ); + } + // prepare room for new classes + p->pMemClassesFree = NULL; + Ssw_ClassesCheck( p ); +// Ssw_ClassesPrint( p, 0 ); + return p; +} + /**Function************************************************************* Synopsis [Iteratively refines the classes after simulation.] @@ -820,8 +862,8 @@ int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursi if ( Vec_PtrSize(p->vClassNew) == 0 ) return 0; // remember that this class is refined - Ssw_ClassForEachNode( p, pReprOld, pObj, i ) - Vec_PtrPush( p->vRefined, pObj ); +// Ssw_ClassForEachNode( p, pReprOld, pObj, i ) +// Vec_PtrPush( p->vRefined, pObj ); // get the new representative pReprNew = Vec_PtrEntry( p->vClassNew, 0 ); @@ -944,7 +986,7 @@ int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive ) if ( !p->pFuncNodeIsConst( p->pManData, pObj ) ) { Vec_PtrPush( p->vClassNew, pObj ); - Vec_PtrPush( p->vRefined, pObj ); +// Vec_PtrPush( p->vRefined, pObj ); } } // check if there is a new class diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h index 8d8d3265..90c1367f 100644 --- a/src/aig/ssw/sswInt.h +++ b/src/aig/ssw/sswInt.h @@ -205,6 +205,7 @@ extern Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int n extern Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs ); extern Ssw_Cla_t * Ssw_ClassesPrepareTargets( Aig_Man_t * pAig ); extern Ssw_Cla_t * Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses ); +extern Ssw_Cla_t * Ssw_ClassesFromIslands( Aig_Man_t * pMiter, Vec_Int_t * vPairs ); extern int Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive ); extern int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive ); extern int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive ); diff --git a/src/aig/ssw/sswIslands.c b/src/aig/ssw/sswIslands.c new file mode 100644 index 00000000..5a5783f7 --- /dev/null +++ b/src/aig/ssw/sswIslands.c @@ -0,0 +1,382 @@ +/**CFile**************************************************************** + + FileName [sswIslands.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Inductive prover with constraints.] + + Synopsis [Detection of islands of difference.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - September 1, 2008.] + + Revision [$Id: sswIslands.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "sswInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline Aig_Obj_t * Aig_ObjChild0Copy2( Aig_Obj_t * pObj ) { return Aig_ObjFanin0(pObj)->pData? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj)) : NULL; } +static inline Aig_Obj_t * Aig_ObjChild1Copy2( Aig_Obj_t * pObj ) { return Aig_ObjFanin1(pObj)->pData? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj)) : NULL; } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates pair of structurally equivalent nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_CreatePair( Vec_Int_t * vPairs, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) +{ + pObj0->pData = pObj1; + pObj1->pData = pObj0; + Vec_IntPush( vPairs, pObj0->Id ); + Vec_IntPush( vPairs, pObj1->Id ); +} + +/**Function************************************************************* + + Synopsis [Detects islands of common logic and returns them as pairs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Ssw_DetectIslands( Aig_Man_t * p0, Aig_Man_t * p1, int nCommonFlops, int fVerbose ) +{ + Vec_Int_t * vPairs; + Aig_Obj_t * pObj0, * pObj1, * pFanin0, * pFanin1; + int i; + assert( Aig_ManRegNum(p0) > 0 ); + assert( Aig_ManRegNum(p1) > 0 ); + assert( Aig_ManRegNum(p0) >= nCommonFlops ); + assert( Aig_ManRegNum(p1) >= nCommonFlops ); + assert( Saig_ManPiNum(p0) == Saig_ManPiNum(p1) ); + assert( Saig_ManPoNum(p0) == Saig_ManPoNum(p1) ); + Aig_ManCleanData( p0 ); + Aig_ManCleanData( p1 ); + // start structural equivalence + vPairs = Vec_IntAlloc( 1000 ); + Ssw_CreatePair( vPairs, Aig_ManConst1(p0), Aig_ManConst1(p1) ); + Saig_ManForEachPi( p0, pObj0, i ) + Ssw_CreatePair( vPairs, pObj0, Aig_ManPi(p1, i) ); + Saig_ManForEachLo( p0, pObj0, i ) + { + if ( i == nCommonFlops ) + break; + Ssw_CreatePair( vPairs, pObj0, Saig_ManLo(p1, i) ); + } + // find structurally equivalent nodes + Aig_ManForEachNode( p0, pObj0, i ) + { + pFanin0 = Aig_ObjChild0Copy2( pObj0 ); + pFanin1 = Aig_ObjChild1Copy2( pObj0 ); + if ( pFanin0 == NULL || pFanin1 == NULL ) + continue; + pObj1 = Aig_TableLookupTwo( p1, pFanin0, pFanin1 ); + if ( pObj1 == NULL ) + continue; + Ssw_CreatePair( vPairs, pObj0, pObj1 ); + } + return vPairs; +} + +/**Function************************************************************* + + Synopsis [Collects additional Lis and Los.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_CollectExtraLiLo( Aig_Man_t * p, int nCommonFlops, Vec_Ptr_t * vLis, Vec_Ptr_t * vLos ) +{ + Aig_Obj_t * pObjLo, * pObjLi; + int i; + Saig_ManForEachLiLo( p, pObjLo, pObjLi, i ) + { + if ( i < nCommonFlops ) + continue; + Vec_PtrPush( vLis, pObjLi ); + Vec_PtrPush( vLos, pObjLo ); + } +} + +/**Function************************************************************* + + Synopsis [Overlays and extends the pairs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_OverlayIslands( Aig_Man_t * pTo, Aig_Man_t * pFrom, Vec_Ptr_t * vLisFrom, Vec_Ptr_t * vLosFrom, Vec_Int_t * vPairs, int nCommonFlops, int fToGoesFirst ) +{ + Aig_Obj_t * pObjFrom, * pObjTo, * pFanin0To, * pFanin1To; + int i; + // create additional register outputs of From in To + Vec_PtrForEachEntry( vLosFrom, pObjFrom, i ) + { + pObjTo = Aig_ObjCreatePi( pTo ); + if( fToGoesFirst ) + Ssw_CreatePair( vPairs, pObjTo, pObjFrom ); + else + Ssw_CreatePair( vPairs, pObjFrom, pObjTo ); + } + // create additional nodes of From in To + Aig_ManForEachNode( pFrom, pObjFrom, i ) + { + if ( pObjFrom->pData != NULL ) + continue; + pFanin0To = Aig_ObjChild0Copy2( pObjFrom ); + pFanin1To = Aig_ObjChild1Copy2( pObjFrom ); + assert( pFanin0To != NULL && pFanin1To != NULL ); + pObjTo = Aig_And( pTo, pFanin0To, pFanin1To ); + if( fToGoesFirst ) + Ssw_CreatePair( vPairs, pObjTo, pObjFrom ); + else + Ssw_CreatePair( vPairs, pObjFrom, pObjTo ); + } + // finally recreate additional register inputs + Vec_PtrForEachEntry( vLisFrom, pObjFrom, i ) + { + pFanin0To = Aig_ObjChild0Copy2( pObjFrom ); + Aig_ObjCreatePo( pTo, pFanin0To ); + } + // update the number of registers + Aig_ManSetRegNum( pTo, Aig_ManRegNum(pTo) + Vec_PtrSize(vLisFrom) ); +} + +/**Function************************************************************* + + Synopsis [Overlays and extends the pairs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Saig_ManMiterWithIslands( Aig_Man_t * p0, Aig_Man_t * p1, Aig_Man_t ** ppMiter, Vec_Int_t * vPairs ) +{ + Aig_Man_t * pMiter; + Vec_Int_t * vPairsNew; + Aig_Obj_t * pObj0, * pObj1; + int i; + vPairsNew = Vec_IntAlloc( 1000 ); + pMiter = Saig_ManCreateMiter( p0, p1, 0 ); + for ( i = 0; i < Vec_IntSize(vPairs); i += 2 ) + { + pObj0 = Aig_ManObj( p0, Vec_IntEntry(vPairs, i) ); + pObj1 = Aig_ManObj( p1, Vec_IntEntry(vPairs, i+1) ); + pObj0 = pObj0->pData; + pObj1 = pObj1->pData; + assert( !Aig_IsComplement(pObj0) ); + assert( !Aig_IsComplement(pObj1) ); + if ( pObj0 == pObj1 ) + continue; + assert( pObj0->Id < pObj1->Id ); + Vec_IntPush( vPairsNew, pObj0->Id ); + Vec_IntPush( vPairsNew, pObj1->Id ); + } + *ppMiter = pMiter; + return vPairsNew; +} + +/**Function************************************************************* + + Synopsis [Solves SEC using structural similarity.] + + Description [Modifies both p0 and p1 by adding extra logic.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Ssw_SecWithIslandsInternal( Aig_Man_t * p0, Aig_Man_t * p1, int nCommonFlops, int fVerbose, Ssw_Pars_t * pPars ) +{ + Ssw_Man_t * p; + Ssw_Pars_t Pars; + Vec_Int_t * vPairs, * vPairsMiter; + Aig_Man_t * pMiter, * pAigNew; + Vec_Ptr_t * vLis0, * vLos0, * vLis1, * vLos1; + int nNodes, nRegs; + assert( Aig_ManRegNum(p0) > 0 ); + assert( Aig_ManRegNum(p1) > 0 ); + assert( Aig_ManRegNum(p0) >= nCommonFlops ); + assert( Aig_ManRegNum(p1) >= nCommonFlops ); + assert( Saig_ManPiNum(p0) == Saig_ManPiNum(p1) ); + assert( Saig_ManPoNum(p0) == Saig_ManPoNum(p1) ); + // derive pairs + vPairs = Ssw_DetectIslands( p0, p1, nCommonFlops, fVerbose ); + if ( fVerbose ) + { + printf( "Original managers:\n" ); + Aig_ManPrintStats( p0 ); + Aig_ManPrintStats( p1 ); + printf( "Detected %d PI pairs, %d LO pairs, and %d node pairs.\n", + Saig_ManPiNum(p0), nCommonFlops, Vec_IntSize(vPairs)/2 - Saig_ManPiNum(p0) - nCommonFlops - 1 ); + } + // complete the manager with islands + vLis0 = Vec_PtrAlloc( 100 ); + vLos0 = Vec_PtrAlloc( 100 ); + vLis1 = Vec_PtrAlloc( 100 ); + vLos1 = Vec_PtrAlloc( 100 ); + Ssw_CollectExtraLiLo( p0, nCommonFlops, vLis0, vLos0 ); + Ssw_CollectExtraLiLo( p1, nCommonFlops, vLis1, vLos1 ); + + nRegs = Saig_ManRegNum(p0); + nNodes = Aig_ManNodeNum(p0); + Ssw_OverlayIslands( p0, p1, vLis1, vLos1, vPairs, nCommonFlops, 1 ); + if ( fVerbose ) + printf( "Completed p0 with %d registers and %d nodes.\n", + Saig_ManRegNum(p0) - nRegs, Aig_ManNodeNum(p0) - nNodes ); + + nRegs = Saig_ManRegNum(p1); + nNodes = Aig_ManNodeNum(p1); + Ssw_OverlayIslands( p1, p0, vLis0, vLos0, vPairs, nCommonFlops, 0 ); + if ( fVerbose ) + printf( "Completed p1 with %d registers and %d nodes.\n", + Saig_ManRegNum(p1) - nRegs, Aig_ManNodeNum(p1) - nNodes ); + if ( fVerbose ) + { + printf( "Modified managers:\n" ); + Aig_ManPrintStats( p0 ); + Aig_ManPrintStats( p1 ); + } + + Vec_PtrFree( vLis0 ); + Vec_PtrFree( vLos0 ); + Vec_PtrFree( vLis1 ); + Vec_PtrFree( vLos1 ); + // create sequential miter + vPairsMiter = Saig_ManMiterWithIslands( p0, p1, &pMiter, vPairs ); + Vec_IntFree( vPairs ); + // if parameters are not given, create them + if ( pPars == NULL ) + Ssw_ManSetDefaultParams( pPars = &Pars ); + // start the induction manager + p = Ssw_ManCreate( pMiter, pPars ); + // create equivalence classes using these IDs + p->ppClasses = Ssw_ClassesFromIslands( pMiter, vPairsMiter ); + p->pSml = Ssw_SmlStart( pMiter, 0, 1 + p->pPars->nFramesAddSim, 1 ); + Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord ); + // perform refinement of classes + pAigNew = Ssw_SignalCorrespondenceRefine( p ); + // cleanup + Ssw_ManStop( p ); + Aig_ManStop( pMiter ); + Vec_IntFree( vPairsMiter ); + return pAigNew; +} + +/**Function************************************************************* + + Synopsis [Solves SEC using structural similarity.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_SecWithIslands( Aig_Man_t * p0, Aig_Man_t * p1, int nCommonFlops, int fVerbose, Ssw_Pars_t * pPars ) +{ + Aig_Man_t * pAigRes; + Aig_Man_t * p0New, * p1New; + int RetValue, clk = clock(); + // try the new AIGs +// printf( "Performing verification using structural similarity.\n" ); + p0New = Aig_ManDupSimple( p0 ); + p1New = Aig_ManDupSimple( p1 ); + pAigRes = Ssw_SecWithIslandsInternal( p0New, p1New, nCommonFlops, fVerbose, pPars ); + Aig_ManStop( p0New ); + Aig_ManStop( p1New ); + // report the results + RetValue = Ssw_MiterStatus( pAigRes, 1 ); + if ( RetValue == 1 ) + printf( "Verification successful. " ); + else if ( RetValue == 0 ) + printf( "Verification failed with a counter-example. " ); + else + printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ", + Aig_ManRegNum(pAigRes), Aig_ManRegNum(p0New)+Aig_ManRegNum(p1New) ); + PRT( "Time", clock() - clk ); + // cleanup + Aig_ManStop( pAigRes ); + return RetValue; +} + + +/**Function************************************************************* + + Synopsis [Solves SEC using structural similarity for the miter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_SecWithIslandsMiter( Aig_Man_t * pMiter, int nCommonFlops, int fVerbose ) +{ + Aig_Man_t * pPart0, * pPart1; + int RetValue; + if ( fVerbose ) + Aig_ManPrintStats( pMiter ); + // demiter the miter + if ( !Saig_ManDemiterSimpleDiff( pMiter, &pPart0, &pPart1 ) ) + { + printf( "Demitering has failed.\n" ); + return -1; + } + if ( fVerbose ) + { +// Aig_ManPrintStats( pPart0 ); +// Aig_ManPrintStats( pPart1 ); +// Aig_ManDumpBlif( pPart0, "part0.blif", NULL, NULL ); +// Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL ); +// printf( "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" ); + } + RetValue = Ssw_SecWithIslands( pPart0, pPart1, nCommonFlops, fVerbose, NULL ); + Aig_ManStop( pPart0 ); + Aig_ManStop( pPart1 ); + return RetValue; +} + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/ssw/sswPairs.c b/src/aig/ssw/sswPairs.c index c77ad30d..1af357f9 100644 --- a/src/aig/ssw/sswPairs.c +++ b/src/aig/ssw/sswPairs.c @@ -276,6 +276,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pA assert( Vec_IntSize(vIds1) == Vec_IntSize(vIds2) ); // create sequential miter pMiter = Saig_ManCreateMiter( pAig1, pAig2, 0 ); + Aig_ManCleanup( pMiter ); // transfer information to the miter vPairs = Ssw_TransferSignalPairs( pMiter, pAig1, pAig2, vIds1, vIds2 ); // create representation of the classes @@ -413,6 +414,7 @@ int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars ) // try the new AIGs printf( "Performing general verification without node pairs.\n" ); pMiter = Saig_ManCreateMiter( pAig1, pAig2, 0 ); + Aig_ManCleanup( pMiter ); pAigRes = Ssw_SignalCorrespondence( pMiter, pPars ); Aig_ManStop( pMiter ); // report the results diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index b5d751b2..f12e94e1 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -7936,7 +7936,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); */ - +/* pNtkRes = Abc_NtkDarTestNtk( pNtk ); if ( pNtkRes == NULL ) { @@ -7945,9 +7945,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) } // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); +*/ - -// Abc_NtkDarTest( pNtk ); + Abc_NtkDarTest( pNtk ); return 0; usage: diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c index f6a1bb4e..d0bce990 100644 --- a/src/base/abci/abcMap.c +++ b/src/base/abci/abcMap.c @@ -109,9 +109,9 @@ clk = clock(); // reconstruct the network after mapping pNtkNew = Abc_NtkFromMap( pMan, pNtk ); + Map_ManFree( pMan ); if ( pNtkNew == NULL ) return NULL; - Map_ManFree( pMan ); if ( pNtk->pExdc ) pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc ); diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make new file mode 100644 index 00000000..e69de29b diff --git a/src/map/ply/module.make b/src/map/ply/module.make new file mode 100644 index 00000000..e69de29b -- cgit v1.2.3