initial commit of public abc

2026-09-08 11:53:16 +02:00 · 2010-11-01 01:35:04 -07:00
parent f0e77f6797
commit 6130e39b18
1119 changed files with 74755 additions and 20648 deletions
@@ -0,0 +1,629 @@
+/**CFile****************************************************************
+
+  FileName    [cmdPlugin.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [Integrating external binary.]
+
+  Author      [Alan Mishchenko, Niklas Een]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 29, 2010.]
+
+  Revision    [$Id: cmdPlugin.c,v 1.00 2010/09/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifdef WIN32
+#include <io.h> 
+#include <process.h> 
+#else
+#include <unistd.h>
+#endif
+
+#include "abc.h"
+#include "mainInt.h"
+#include "cmd.h"
+#include "cmdInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+/*
+
+-------- Original Message --------
+Subject:     ABC/ZZ integration
+Date:     Wed, 29 Sep 2010 00:34:32 -0700
+From:     Niklas Een <[email protected]>
+To:     Alan Mishchenko <[email protected]>
+
+Hi Alan,
+
+Since the interface is file-based, it is important that we generate 
+good, unique filenames (we may run multiple instances of ABC in the 
+same directory), so I have attached some portable code for doing that 
+(tmpFile.c). You can integrate it appropriately.
+
+This is how my interface is meant to work:
+
+(1) As part of your call to Bip, give it first argument "-abc". 
+    This will alter Bip's behavior slightly.
+
+(2) To list the commands, call 'bip -list-commands'. 
+    My commands begin with a comma (so that's my prefix).
+
+(3) All commands expect an input file and an output file. 
+    The input file should be in AIGER format. 
+    The output will be a text file. 
+    Example:
+       bip -input=tmp.aig -output=tmp.out ,pdr -check -prop=5
+
+    So you just auto-generate the two temporary files (output file is 
+    closed and left empty) and stitch the ABC command line at the end. 
+    All you need to check for is if the ABC line begins with a comma.
+
+(4) The result written to the output file will contain a number 
+    of object. Each object is on a separate line of the form:
+
+    <object name>: <object data>
+
+That is: name, colon, space, data, newline. If you see a name you don't 
+recognize, just skip that line (so you will ignore future extensions by me). 
+I currently define the following objects:
+
+    result:
+    counter-example:
+    proof-invariant:
+    bug-free-depth:
+    abstraction:
+  
+"result:" is one of "proved", "failed", "undetermined" (=reached resource limit), "error" 
+(only used by the abstraction command, and only if resource limit was so tight that the 
+abstraction was still empty -- no abstraction is returned in this special case).
+
+"counter-example:" -- same format as before
+
+"proof-invariant:" contains an text-encoded single-output AIG. If you want 
+you can parse it and validate the invariant.
+
+"bug-free-depth:" the depth up to which the procedure has checked for counter-example. 
+Starts at -1 (not even the initial states have been verified).
+
+"abstraction:" -- same format as before
+
+(5) I propose that you add a command "load_plugin <path/binary>". That way Bob can put 
+Bip where ever he likes and just modify his abc_rc file.
+
+The intention is that ABC can read this file and act on it without knowing what 
+particular command was used. If there is an abstraction, you will always apply it. 
+If there is a "bug-free-depth" you will store that data somewhere so that Bob can query 
+it through the Python interface, and so on. If we need different actions for different 
+command, then we add a new object for the new action.
+
+// N.
+
+*/
+
+extern int tmpFile(const char* prefix, const char* suffix, char** out_name);
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_GetBinaryName( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    char * pTemp;
+    int i;
+    Vec_PtrForEachEntry( char *, pAbc->vPlugInComBinPairs, pTemp, i )
+    {
+        i++;
+        if ( strcmp( pTemp, argv[0] ) == 0 )
+            return Vec_PtrEntry( pAbc->vPlugInComBinPairs, i );
+    }
+    assert( 0 );
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Read flop map.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Str_t * Abc_ManReadFile( char * pFileName )
+{
+    FILE * pFile;
+    Vec_Str_t * vStr;
+    int c;
+    pFile = fopen( pFileName, "r" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\".\n", pFileName );
+        return NULL;
+    }
+    vStr = Vec_StrAlloc( 100 );
+    while ( (c = fgetc(pFile)) != EOF )
+        Vec_StrPush( vStr, (char)c );
+    Vec_StrPush( vStr, '\0' );
+    fclose( pFile );
+    return vStr;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Read flop map.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Abc_ManReadBinary( char * pFileName, char * pToken )
+{
+    Vec_Int_t * vMap = NULL;
+    Vec_Str_t * vStr;
+    char * pStr;
+    int i, Length;
+    vStr = Abc_ManReadFile( pFileName );
+    if ( vStr == NULL )
+        return NULL;
+    pStr = Vec_StrArray( vStr );
+    pStr = strstr( pStr, pToken );
+    if ( pStr != NULL )
+    {
+        pStr  += strlen( pToken );
+        vMap   = Vec_IntAlloc( 100 );
+        Length = strlen( pStr );
+        for ( i = 0; i < Length; i++ )
+        {
+            if ( pStr[i] == '0' || pStr[i] == '?' )
+                Vec_IntPush( vMap, 0 );
+            else if ( pStr[i] == '1' )
+                Vec_IntPush( vMap, 1 );
+            if ( ('a' <= pStr[i] && pStr[i] <= 'z') || 
+                 ('A' <= pStr[i] && pStr[i] <= 'Z') )
+                break;
+        }
+    }
+    Vec_StrFree( vStr );
+    return vMap;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Read flop map.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ManReadInteger( char * pFileName, char * pToken )
+{
+    int Result = -1;
+    Vec_Str_t * vStr;
+    char * pStr;
+    vStr = Abc_ManReadFile( pFileName );
+    if ( vStr == NULL )
+        return -1;
+    pStr = Vec_StrArray( vStr );
+    pStr = strstr( pStr, pToken );
+    if ( pStr != NULL )
+        Result = atoi( pStr + strlen(pToken) );
+    Vec_StrFree( vStr );
+    return Result;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Read flop map.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ManReadStatus( char * pFileName, char * pToken )
+{
+    int Result = -1;
+    Vec_Str_t * vStr;
+    char * pStr;
+    vStr = Abc_ManReadFile( pFileName );
+    if ( vStr == NULL )
+        return -1;
+    pStr = Vec_StrArray( vStr );
+    pStr = strstr( pStr, pToken );
+    if ( pStr != NULL )
+    {
+        if ( strncmp(pStr+8, "proved", 6) == 0 )
+            Result = 1; 
+        else if ( strncmp(pStr+8, "failed", 6) == 0 )
+            Result = 0; 
+    }
+    Vec_StrFree( vStr );
+    return Result;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Work-around to insert 0s for PIs without fanout.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Abc_ManExpandCex( Gia_Man_t * pGia, Vec_Int_t * vCex )
+{
+    Vec_Int_t * vCexNew;
+    Gia_Obj_t * pObj;
+    int i, k;
+
+    // start with register outputs
+    vCexNew = Vec_IntAlloc( Vec_IntSize(vCex) );
+    Gia_ManForEachRo( pGia, pObj, i )
+        Vec_IntPush( vCexNew, 0 );
+
+    ABC_FREE( pGia->pRefs );
+    Gia_ManCreateRefs( pGia );
+    k = Gia_ManRegNum( pGia );
+    while ( 1 )
+    {
+        Gia_ManForEachPi( pGia, pObj, i )
+        {
+            if ( Gia_ObjRefs(pGia, pObj) == 0 )
+                Vec_IntPush( vCexNew, 0 );
+            else
+            {
+                if ( k == Vec_IntSize(vCex) )
+                    break;
+                Vec_IntPush( vCexNew, Vec_IntEntry(vCex, k++) );
+            }
+        }
+        if ( k == Vec_IntSize(vCex) )
+            break;
+    }
+    return vCexNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cmd_CommandAbcPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    char * pFileIn, * pFileOut;
+    char * pFileNameBinary;
+    Vec_Str_t * vCommand;
+    Vec_Int_t * vCex;
+    FILE * pFile;
+    int i, fd, clk;
+    int fLeaveFiles;
+/*
+    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+    if ( pNtk == NULL )
+    {
+        Abc_Print( -1, "Current network does not exist\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsStrash( pNtk) )
+    {
+        Abc_Print( -1, "The current network is not an AIG. Cannot continue.\n" );
+        return 1;
+    }
+*/
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Current AIG does not exist (try command &ps).\n" );
+        return 1;
+    }
+
+    // check if there is the binary
+    pFileNameBinary = Abc_GetBinaryName( pAbc, argc, argv );
+    if ( (pFile = fopen( pFileNameBinary, "r" )) == NULL )
+    {
+        Abc_Print( -1, "Cannot run the binary \"%s\".\n\n", pFileNameBinary );
+        return 1;
+    }
+    fclose( pFile );
+
+    // create temp file
+    fd = tmpFile( "__abctmp_", ".aig", &pFileIn );
+    if ( fd == -1 )
+    {
+        Abc_Print( -1, "Cannot create a temporary file.\n" );
+        return 1;
+    }
+#ifdef WIN32
+    _close( fd );
+#else
+    close( fd );
+#endif
+
+    // create temp file
+    fd = tmpFile( "__abctmp_", ".out", &pFileOut );
+    if ( fd == -1 )
+    {
+        ABC_FREE( pFileIn );
+        Abc_Print( -1, "Cannot create a temporary file.\n" );
+        return 1;
+    }
+#ifdef WIN32
+    _close( fd );
+#else
+    close( fd );
+#endif
+
+
+    // write current network into a file
+/*
+    {
+        extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+        Aig_Man_t * pAig;
+        pAig = Abc_NtkToDar( pNtk, 0, 1 );
+        Ioa_WriteAiger( pAig, pFileIn, 0, 0 );
+        Aig_ManStop( pAig );
+    }
+*/ 
+    // check what to do with the files
+    fLeaveFiles = 0;
+    if ( strcmp( argv[argc-1], "!" ) == 0 )
+    {
+        Abc_Print( 0, "Input file \"%s\" and output file \"%s\" are not deleted.\n", pFileIn, pFileOut );
+        fLeaveFiles = 1;
+        argc--;
+    }
+
+    // create input file
+    Gia_WriteAiger( pAbc->pGia, pFileIn, 0, 0 );
+
+    // create command line
+    vCommand = Vec_StrAlloc( 100 );
+    Vec_StrAppend( vCommand, pFileNameBinary );
+    // add input/output file
+    Vec_StrAppend( vCommand, " -abc" );
+//    Vec_StrAppend( vCommand, " -input=C:/_projects/abc/_TEST/hwmcc/139442p0.aig" );
+    Vec_StrAppend( vCommand, " -input=" );
+    Vec_StrAppend( vCommand, pFileIn );
+    Vec_StrAppend( vCommand, " -output=" );
+    Vec_StrAppend( vCommand, pFileOut );
+    // add other arguments
+    for ( i = 0; i < argc; i++ )
+    {
+        Vec_StrAppend( vCommand, " " );
+        Vec_StrAppend( vCommand, argv[i] );
+    }
+    Vec_StrPush( vCommand, 0 );
+
+    // run the command line
+//printf( "Running command line: %s\n", Vec_StrArray(vCommand) ); 
+
+    clk = clock();
+    if ( system( Vec_StrArray(vCommand) ) )
+    {
+        Abc_Print( -1, "The following command has returned non-zero exit status:\n" );
+        Abc_Print( -1, "\"%s\"\n", Vec_StrArray(vCommand) );
+        return 1;
+    }
+    clk = clock() - clk;
+    Vec_StrFree( vCommand );
+
+    // check if the output file exists
+    if ( (pFile = fopen( pFileOut, "r" )) == NULL )
+    {
+        Abc_Print( -1, "There is no output file \"%s\".\n", pFileOut );
+        return 1;
+    }
+    fclose( pFile );
+
+    // process the output
+    if ( Extra_FileSize(pFileOut) > 0 )
+    {
+        // read program arguments
+        pAbc->Status  = Abc_ManReadStatus( pFileOut, "result:" );
+        pAbc->nFrames = Abc_ManReadInteger( pFileOut, "bug-free-depth:" );
+        if ( pAbc->nFrames == -1 )
+            printf( "Gia_ManCexAbstractionStartNew(): Cannot read the number of frames covered by BMC.\n" );
+        pAbc->pGia->vFlopClasses = Abc_ManReadBinary( pFileOut, "abstraction:" );
+        vCex = Abc_ManReadBinary( pFileOut, "counter-example:" );
+        if ( vCex ) 
+        {
+            int nFrames, nRemain;
+
+            nFrames = (Vec_IntSize(vCex) - Gia_ManRegNum(pAbc->pGia)) / Gia_ManPiNum(pAbc->pGia);
+            nRemain = (Vec_IntSize(vCex) - Gia_ManRegNum(pAbc->pGia)) % Gia_ManPiNum(pAbc->pGia);
+            if ( nRemain != 0 )
+            {   
+                Vec_Int_t * vTemp;
+                Abc_Print( 1, "Adjusting counter-example by adding zeros for PIs without fanout.\n" );
+                // expand the counter-example to include PIs without fanout
+                vCex = Abc_ManExpandCex( pAbc->pGia, vTemp = vCex );
+                Vec_IntFree( vTemp );
+            }
+
+            nFrames = (Vec_IntSize(vCex) - Gia_ManRegNum(pAbc->pGia)) / Gia_ManPiNum(pAbc->pGia);
+            nRemain = (Vec_IntSize(vCex) - Gia_ManRegNum(pAbc->pGia)) % Gia_ManPiNum(pAbc->pGia);
+            if ( nRemain != 0 )
+                Abc_Print( 1, "Counter example has a wrong length.\n" );
+            else
+            {
+                extern int Gia_ManVerifyCounterExampleAllOuts( Gia_Man_t * pAig, Abc_Cex_t * p );
+
+                Abc_Print( 1, "Problem is satisfiable. Found counter-example in frame %d.  ", nFrames-1 );
+                Abc_PrintTime( 1, "Time", clk );
+                ABC_FREE( pAbc->pCex );
+                pAbc->pCex = Gia_ManDeriveCexFromArray( pAbc->pGia, vCex, 0, nFrames-1 );
+
+//                Gia_ManPrintCex( pAbc->pCex );
+
+//                if ( !Gia_ManVerifyCounterExample( pAbc->pGia, pAbc->pCex, 0 ) )
+//                    Abc_Print( 1, "Generated counter-example is INVALID.\n" );
+
+                // remporary work-around to detect the output number - October 18, 2010
+                pAbc->pCex->iPo = Gia_ManVerifyCounterExampleAllOuts( pAbc->pGia, pAbc->pCex );
+                if ( pAbc->pCex->iPo == -1 )
+                {
+                    Abc_Print( 1, "Generated counter-example is INVALID.\n" );
+                    ABC_FREE( pAbc->pCex );
+                }
+                else
+                {
+                    Abc_Print( 1, "Returned counter-example successfully verified in ABC.\n" );
+                }
+            }
+            Vec_IntFreeP( &vCex );
+        }
+    }
+
+    
+
+    // clean up
+    if ( !fLeaveFiles )
+    {
+        remove( pFileIn );
+        remove( pFileOut );
+    }
+    ABC_FREE( pFileIn );
+    ABC_FREE( pFileOut );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cmd_CommandAbcLoadPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pFile;
+    char pBuffer[1000];
+    char * pCommandLine;
+    char * pTempFile;
+    char * pStrDirBin, * pStrSection;
+    int fd, RetValue;
+
+    if ( argc != 3 )
+    {
+        Abc_Print( -1, "Wrong number of arguments.\n" );
+        goto usage;
+    }
+    // collect arguments
+    pStrDirBin  = argv[argc-2];
+    pStrSection = argv[argc-1];
+
+    // check if the file exists
+    if ( (pFile = fopen( pStrDirBin, "r" )) == NULL )
+    {
+//        Abc_Print( -1, "Cannot run the binary \"%s\".\n", pStrDirBin );
+//        goto usage;
+        return 0;
+    }
+    fclose( pFile );
+
+    // create temp file
+    fd = tmpFile( "__abctmp_", ".txt", &pTempFile );
+    if ( fd == -1 )
+    {
+        Abc_Print( -1, "Cannot create a temporary file.\n" );
+        goto usage;
+    }
+#ifdef WIN32
+    _close( fd );
+#else
+    close( fd );
+#endif
+
+    // get command list
+    pCommandLine = ABC_ALLOC( char, 100 + strlen(pStrDirBin) + strlen(pTempFile) );
+//    sprintf( pCommandLine, "%s -abc -list-commands > %s", pStrDirBin, pTempFile );
+    sprintf( pCommandLine, "%s -abc -list-commands > %s", pStrDirBin, pTempFile );
+    RetValue = system( pCommandLine );
+    if ( RetValue == -1 )
+    {
+        Abc_Print( -1, "Command \"%s\" did not succeed.\n", pCommandLine );
+        ABC_FREE( pCommandLine );
+        ABC_FREE( pTempFile );
+        goto usage;
+    }
+    ABC_FREE( pCommandLine );
+
+    // create commands
+    pFile = fopen( pTempFile, "r" );
+    if ( pFile == NULL )
+    {
+        Abc_Print( -1, "Cannot open file with the list of commands.\n" );
+        ABC_FREE( pTempFile );
+        goto usage;
+    }
+    while ( fgets( pBuffer, 1000, pFile ) != NULL )
+    {
+        if ( pBuffer[strlen(pBuffer)-1] == '\n' )
+            pBuffer[strlen(pBuffer)-1] = 0;
+        Cmd_CommandAdd( pAbc, pStrSection, pBuffer, Cmd_CommandAbcPlugIn, 1 );
+//        plugin_commands.push(Pair(cmd_name, binary_name));
+        Vec_PtrPush( pAbc->vPlugInComBinPairs, strdup(pBuffer) );
+        Vec_PtrPush( pAbc->vPlugInComBinPairs, strdup(pStrDirBin) );
+        printf( "Creating command %s with binary %s\n", pBuffer, pStrDirBin );
+    }
+    fclose( pFile );
+    remove( pTempFile );
+    ABC_FREE( pTempFile );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: load_plugin <plugin_dir\\binary_name> <section_name>\n" );
+    Abc_Print( -2, "\t        loads external binary as a plugin\n" );
+    Abc_Print( -2, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+