summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2008-10-25 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2008-10-25 08:01:00 -0700
commitd2b735f794575ce0f10f01bba1255cf1dc3b8aaf (patch)
treebaac975efb3057f03506f165acbd36d2e67341b6 /src/aig
parent2418d9b08d0b49c675f02dc2351e2230079174af (diff)
downloadabc-d2b735f794575ce0f10f01bba1255cf1dc3b8aaf.tar.gz
abc-d2b735f794575ce0f10f01bba1255cf1dc3b8aaf.tar.bz2
abc-d2b735f794575ce0f10f01bba1255cf1dc3b8aaf.zip
Version abc81025
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/fra/fraCec.c4
-rw-r--r--src/aig/ntl/ntl.h4
-rw-r--r--src/aig/ntl/ntlEc.c1
-rw-r--r--src/aig/ntl/ntlReadBlif.c2
-rw-r--r--src/aig/ntl/ntlReadBlif_old.c1261
-rw-r--r--src/aig/ntl/ntlTable.c77
-rw-r--r--src/aig/nwk/nwkCheck.c2
-rw-r--r--src/aig/saig/module.make1
-rw-r--r--src/aig/saig/saig.h1
-rw-r--r--src/aig/saig/saigBmc.c550
-rw-r--r--src/aig/saig/saigBmc2.c314
-rw-r--r--src/aig/saig/saigMiter.c159
-rw-r--r--src/aig/saig/saigSynch.c1
-rw-r--r--src/aig/ssw/module.make1
-rw-r--r--src/aig/ssw/ssw.h1
-rw-r--r--src/aig/ssw/sswClass.c52
-rw-r--r--src/aig/ssw/sswInt.h1
-rw-r--r--src/aig/ssw/sswIslands.c382
-rw-r--r--src/aig/ssw/sswPairs.c2
19 files changed, 1330 insertions, 1486 deletions
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
@@ -180,6 +180,27 @@ Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName )
/**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).]
Description []
@@ -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;
@@ -243,6 +264,60 @@ int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * pNam
/**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.]
Description []
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 );
@@ -793,6 +793,48 @@ Ssw_Cla_t * Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses )
/**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.]
Description [Returns the number of refinements performed.]
@@ -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