abc.c File Reference

#include "base/abc/abc.h"
#include "base/main/main.h"
#include "base/main/mainInt.h"
#include "proof/fraig/fraig.h"
#include "opt/fxu/fxu.h"
#include "opt/fxch/Fxch.h"
#include "opt/cut/cut.h"
#include "map/fpga/fpga.h"
#include "map/if/if.h"
#include "opt/sim/sim.h"
#include "opt/res/res.h"
#include "opt/lpk/lpk.h"
#include "aig/gia/giaAig.h"
#include "opt/dar/dar.h"
#include "opt/mfs/mfs.h"
#include "proof/fra/fra.h"
#include "aig/saig/saig.h"
#include "proof/int/int.h"
#include "proof/dch/dch.h"
#include "proof/ssw/ssw.h"
#include "opt/cgt/cgt.h"
#include "bool/kit/kit.h"
#include "map/amap/amap.h"
#include "opt/ret/retInt.h"
#include "sat/xsat/xsat.h"
#include "sat/satoko/satoko.h"
#include "sat/cnf/cnf.h"
#include "proof/cec/cec.h"
#include "proof/acec/acec.h"
#include "proof/pdr/pdr.h"
#include "misc/tim/tim.h"
#include "bdd/llb/llb.h"
#include "bdd/bbr/bbr.h"
#include "map/cov/cov.h"
#include "base/cmd/cmd.h"
#include "proof/abs/abs.h"
#include "sat/bmc/bmc.h"
#include "proof/ssc/ssc.h"
#include "opt/sfm/sfm.h"
#include "opt/sbd/sbd.h"
#include "bool/rpo/rpo.h"
#include "map/mpm/mpm.h"
#include "map/mio/mio.h"
#include "opt/fret/fretime.h"
#include "opt/nwk/nwkMerge.h"
#include "base/acb/acbPar.h"
#include "misc/extra/extra.h"
#include "opt/eslim/eSLIM.h"
#include <unistd.h>
#include "abciUnfold2.c"

Go to the source code of this file.

Functions
int	Abc_CommandAbcLivenessToSafety (Abc_Frame_t *pAbc, int argc, char **argv)
int	Abc_CommandAbcLivenessToSafetySim (Abc_Frame_t *pAbc, int argc, char **argv)
int	Abc_CommandAbcLivenessToSafetyWithLTL (Abc_Frame_t *pAbc, int argc, char **argv)
int	Abc_CommandCS_kLiveness (Abc_Frame_t *pAbc, int argc, char **argv)
int	Abc_CommandNChooseK (Abc_Frame_t *pAbc, int argc, char **argv)
Aig_Man_t *	Abc_NtkToDar (Abc_Ntk_t *pNtk, int fExors, int fRegisters)
Abc_Ntk_t *	Abc_NtkFromAigPhase (Aig_Man_t *pMan)
	DECLARATIONS ///.
Vec_Ptr_t *	Abc_NtkCollectCiNames (Abc_Ntk_t *pNtk)
Vec_Ptr_t *	Abc_NtkCollectCoNames (Abc_Ntk_t *pNtk)
void	Extra_BitMatrixTransposeP (Vec_Wrd_t *vSimsIn, int nWordsIn, Vec_Wrd_t *vSimsOut, int nWordsOut)
	DECLARATIONS ///.
void	Abc_FrameReplaceCex (Abc_Frame_t *pAbc, Abc_Cex_t **ppCex)
	FUNCTION DEFINITIONS ///.
void	Abc_FrameReplaceCexVec (Abc_Frame_t *pAbc, Vec_Ptr_t **pvCexVec)
void	Abc_FrameReplacePoEquivs (Abc_Frame_t *pAbc, Vec_Ptr_t **pvPoEquivs)
void	Abc_FrameReplacePoStatuses (Abc_Frame_t *pAbc, Vec_Int_t **pvStatuses)
Vec_Int_t *	Abc_FrameDeriveStatusArray (Vec_Ptr_t *vCexes)
Vec_Int_t *	Abc_FrameDeriveStatusArray2 (Vec_Ptr_t *vCexes)
void	Abc_FrameClearDesign ()
void	Abc_FrameUpdateGia (Abc_Frame_t *pAbc, Gia_Man_t *pNew)
Gia_Man_t *	Abc_FrameGetGia (Abc_Frame_t *pAbc)
void	Abc_Init (Abc_Frame_t *pAbc)
	DECLARATIONS ///.
void	Abc_End (Abc_Frame_t *pAbc)
Vec_Int_t *	Vec_IntReadList (char *pStr, char Separ)
int	Abc_CommandCexMin (Abc_Frame_t *pAbc, int argc, char **argv)
int	Abc_CommandAbc9PoPart2 (Abc_Frame_t *pAbc, int argc, char **argv)
int	Abc_CommandAbc9CexCut (Abc_Frame_t *pAbc, int argc, char **argv)
int	Abc_CommandAbc9CexMerge (Abc_Frame_t *pAbc, int argc, char **argv)
int	Abc_CommandAbc9CexMin (Abc_Frame_t *pAbc, int argc, char **argv)

Variables
Bnd_Man_t *	pBnd
	DECLARATIONS ///.

Function Documentation

Abc_CommandAbc9CexCut()

int Abc_CommandAbc9CexCut	(	Abc_Frame_t *	pAbc,
		int	argc,
		char **	argv )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 53672 of file abc.c.

{
    return -1;
}

Abc_CommandAbc9CexMerge()

int Abc_CommandAbc9CexMerge	(	Abc_Frame_t *	pAbc,
		int	argc,
		char **	argv )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 53688 of file abc.c.

{
    Abc_Cex_t * pCexNew;
    int c;
    int iFrStart = 0;
    int iFrStop  = ABC_INFINITY;
    int fVerbose = 0;
    Extra_UtilGetoptReset();
    while ( ( c = Extra_UtilGetopt( argc, argv, "FGvh" ) ) != EOF )
    {
        switch ( c )
        {
        case 'F':
            if ( globalUtilOptind >= argc )
            {
                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
                goto usage;
            }
            iFrStart = atoi(argv[globalUtilOptind]);
            globalUtilOptind++;
            if ( iFrStart < 0 )
                goto usage;
            break;
        case 'G':
            if ( globalUtilOptind >= argc )
            {
                Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" );
                goto usage;
            }
            iFrStop = atoi(argv[globalUtilOptind]);
            globalUtilOptind++;
            if ( iFrStop < 0 )
                goto usage;
            break;
        case 'v':
            fVerbose ^= 1;
            break;
        case 'h':
            goto usage;
        default:
            Abc_Print( -2, "Unknown switch.\n");
            goto usage;
        }
    }
 
    if ( pAbc->pCex == NULL )
    {
        Abc_Print( 1, "There is no current cex.\n");
        return 0;
    }
    if ( pAbc->pCex2 == NULL )
    {
        Abc_Print( 1, "There is no saved cex.\n");
        return 0;
    }
    if ( iFrStop - iFrStart < pAbc->pCex->iFrame )
    {
        Abc_Print( 1, "Current CEX does not allow to shorten the saved CEX.\n");
        return 0;
    }
    pCexNew = Abc_CexMerge( pAbc->pCex2, pAbc->pCex, iFrStart, iFrStop );
    if ( pCexNew == NULL )
    {
        Abc_Print( 1, "Merging CEXes has failed.\n");
        return 0;
    }
    // replace the saved CEX
    ABC_FREE( pAbc->pCex2 );
    pAbc->pCex2 = pCexNew;
    return 0;
 
usage:
    Abc_Print( -2, "usage: &cexmerge [-FG num] [-vh]\n" );
    Abc_Print( -2, "\t         merges the current CEX into the saved one\n" );
    Abc_Print( -2, "\t         and sets the resulting CEX as the saved one\n" );
    Abc_Print( -2, "\t-F num : 0-based number of the starting frame [default = %d]\n", iFrStart );
    Abc_Print( -2, "\t-G num : 0-based number of the ending frame [default = %d]\n",   iFrStop );
    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
    Abc_Print( -2, "\t-h     : print the command usage\n");
    return 1;
}

Here is the call graph for this function:

Abc_CommandAbc9CexMin()

int Abc_CommandAbc9CexMin	(	Abc_Frame_t *	pAbc,
		int	argc,
		char **	argv )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 53781 of file abc.c.

{
    extern Abc_Cex_t * Gia_ManCexMin( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int nRealPis, int fJustMax, int fUseAll, int fVerbose );
    Abc_Cex_t * pCexNew;
    int iFrameStart = 0;
    int nRealPis = -1;
    int fJustMax = 1;
    int fUseAll = 0;
    int c, fVerbose = 0;
    Extra_UtilGetoptReset();
    while ( ( c = Extra_UtilGetopt( argc, argv, "FNjavh" ) ) != EOF )
    {
        switch ( c )
        {
        case 'F':
            if ( globalUtilOptind >= argc )
            {
                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
                goto usage;
            }
            iFrameStart = atoi(argv[globalUtilOptind]);
            globalUtilOptind++;
            if ( iFrameStart < 0 )
                goto usage;
            break;
        case 'N':
            if ( globalUtilOptind >= argc )
            {
                Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
                goto usage;
            }
            nRealPis = atoi(argv[globalUtilOptind]);
            globalUtilOptind++;
            if ( nRealPis < 0 )
                goto usage;
            break;
        case 'j':
            fJustMax ^= 1;
            break;
        case 'a':
            fUseAll ^= 1;
            break;
        case 'v':
            fVerbose ^= 1;
            break;
        case 'h':
            goto usage;
        default:
            goto usage;
        }
    }
    if ( pAbc->pGia == NULL )
    {
        Abc_Print( -1, "Abc_CommandAbc9CexMin(): There is no AIG.\n" );
        return 1;
    }
    if ( Gia_ManRegNum(pAbc->pGia) == 0 )
    {
        Abc_Print( -1, "Abc_CommandAbc9CexMin(): The network is combinational.\n" );
        return 0;
    }
    if ( pAbc->pCex == NULL )
    {
        Abc_Print( -1, "Abc_CommandAbc9CexMin(): There is no counter-example.\n" );
        return 1;
    }
    pCexNew = Gia_ManCexMin( pAbc->pGia, pAbc->pCex, iFrameStart, nRealPis, fJustMax, fUseAll, fVerbose );
    if ( pCexNew )
        Abc_FrameReplaceCex( pAbc, &pCexNew );
    return 0;
 
usage:
    Abc_Print( -2, "usage: &cexmin [-FN num] [-javh]\n" );
    Abc_Print( -2, "\t         minimizes a deep counter-example\n" );
    Abc_Print( -2, "\t-F num : starting timeframe for minimization [default = %d]\n", iFrameStart );
    Abc_Print( -2, "\t-N num : the number of real primary inputs [default = %d]\n", nRealPis );
    Abc_Print( -2, "\t-j     : toggle computing all justifying assignments [default = %s]\n", fJustMax? "yes": "no" );
    Abc_Print( -2, "\t-a     : toggle using all terminal objects [default = %s]\n", fUseAll? "yes": "no" );
    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
    Abc_Print( -2, "\t-h     : print the command usage\n");
    return 1;
}

Here is the call graph for this function:

Abc_CommandAbc9PoPart2()

int Abc_CommandAbc9PoPart2	(	Abc_Frame_t *	pAbc,
		int	argc,
		char **	argv )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 49428 of file abc.c.

{
    extern Gia_Man_t * Gia_ManFindPoPartition2( Gia_Man_t * p, int iStartNum, int nDelta, int nOutsMin, int nOutsMax, int fSetLargest, int fVerbose, Vec_Ptr_t ** pvPosEquivs );
    Gia_Man_t * pTemp = NULL;
    Vec_Ptr_t * vPosEquivs = NULL;
    int c, iStartNum = 0, nDelta = 10, nOutsMin = 100, nOutsMax = 1000, fSetLargest = 0, fVerbose = 0;
    Extra_UtilGetoptReset();
    while ( ( c = Extra_UtilGetopt( argc, argv, "SDLUmvh" ) ) != EOF )
    {
        switch ( c )
        {
        case 'S':
            if ( globalUtilOptind >= argc )
            {
                Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
                goto usage;
            }
            iStartNum = atoi(argv[globalUtilOptind]);
            globalUtilOptind++;
            if ( iStartNum < 0 )
                goto usage;
            break;
        case 'D':
            if ( globalUtilOptind >= argc )
            {
                Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" );
                goto usage;
            }
            nDelta = atoi(argv[globalUtilOptind]);
            globalUtilOptind++;
            if ( nDelta < 0 )
                goto usage;
            break;
        case 'L':
            if ( globalUtilOptind >= argc )
            {
                Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
                goto usage;
            }
            nOutsMin = atoi(argv[globalUtilOptind]);
            globalUtilOptind++;
            if ( nOutsMin < 0 )
                goto usage;
            break;
        case 'U':
            if ( globalUtilOptind >= argc )
            {
                Abc_Print( -1, "Command line switch \"-U\" should be followed by an integer.\n" );
                goto usage;
            }
            nOutsMax = atoi(argv[globalUtilOptind]);
            globalUtilOptind++;
            if ( nOutsMax < 0 )
                goto usage;
            break;
        case 'm':
            fSetLargest ^= 1;
            break;
        case 'v':
            fVerbose ^= 1;
            break;
        case 'h':
            goto usage;
        default:
            goto usage;
        }
    }
    if ( pAbc->pGia == NULL )
    {
        Abc_Print( -1, "Abc_CommandAbc9PoPart(): There is no AIG.\n" );
        return 1;
    }
    pTemp = Gia_ManFindPoPartition2( pAbc->pGia, iStartNum, nDelta, nOutsMin, nOutsMax, fSetLargest, fVerbose, &vPosEquivs );
    if ( pTemp )
        Abc_FrameUpdateGia( pAbc, pTemp );
    Abc_FrameReplacePoEquivs( pAbc, &vPosEquivs );
    return 0;
 
usage:
    Abc_Print( -2, "usage: &popart2 [-SDLU num] [-mvh]\n" );
    Abc_Print( -2, "\t         extracting multi-output sequential logic cones\n" );
    Abc_Print( -2, "\t-S num : the index of the PO to start the cluster [default = %d]\n", iStartNum );
    Abc_Print( -2, "\t-D num : the max increase in flop count after adding one PO [default = %d]\n", nDelta );
    Abc_Print( -2, "\t-L num : the minimum number of POs in a cluster [default = %d]\n", nOutsMin );
    Abc_Print( -2, "\t-U num : the maximum number of POs in a cluster [default = %d]\n", nOutsMax );
    Abc_Print( -2, "\t-m     : toggle selecting the largest cluster [default = %s]\n", fSetLargest? "yes": "no" );
    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
    Abc_Print( -2, "\t-h     : print the command usage\n");
    return 1;
}

Here is the call graph for this function:

Abc_CommandAbcLivenessToSafety()

int Abc_CommandAbcLivenessToSafety ( Abc_Frame_t * pAbc, int argc, char ** argv )

extern

Definition at line 1254 of file liveness.c.

{
    FILE * pOut, * pErr;
    Abc_Ntk_t * pNtk, * pNtkTemp, *pNtkNew, *pNtkOld;
    Aig_Man_t * pAig, *pAigNew = NULL;
    int c;
    Vec_Ptr_t * vLive, * vFair, *vAssertSafety, *vAssumeSafety;
    int directive = -1;
                
    pNtk = Abc_FrameReadNtk(pAbc);
    pOut = Abc_FrameReadOut(pAbc);
    pErr = Abc_FrameReadErr(pAbc);
 
    if( argc == 1 )
    {
        assert( directive == -1 );
        directive = FULL_BIERE_MODE;
    }
    else
    {
        Extra_UtilGetoptReset();
        while ( ( c = Extra_UtilGetopt( argc, argv, "1slh" ) ) != EOF )
        {
            switch( c )
            {
            case '1': 
                if( directive == -1 )
                    directive = FULL_BIERE_ONE_LOOP_MODE;
                else
                {
                    assert( directive == IGNORE_LIVENESS_KEEP_SAFETY_MODE || directive == IGNORE_SAFETY_KEEP_LIVENESS_MODE );
                    if( directive == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
                        directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE;
                    else
                        directive = IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE;
                }
                break;
            case 's':
                if( directive == -1 )
                    directive = IGNORE_SAFETY_KEEP_LIVENESS_MODE;
                else
                {
                    if( directive != FULL_BIERE_ONE_LOOP_MODE )
                        goto usage;
                    assert(directive == FULL_BIERE_ONE_LOOP_MODE);
                    directive = IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE;
                }
                break;
            case 'l':
                if( directive == -1 )
                    directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE;
                else
                {
                    if( directive != FULL_BIERE_ONE_LOOP_MODE )
                        goto usage;
                    assert(directive == FULL_BIERE_ONE_LOOP_MODE);
                    directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE;
                }
                break;
            case 'h':
                goto usage;
            default:
                goto usage;
            }
        }
    }
 
    if ( pNtk == NULL )
    {
        fprintf( pErr, "Empty network.\n" );
        return 1;
    }
    if( !Abc_NtkIsStrash( pNtk ) )
    {
        printf("The input network was not strashed, strashing....\n");
        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
        pNtkOld = pNtkTemp;
        pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
        vLive = populateLivenessVector( pNtk, pAig );
        vFair = populateFairnessVector( pNtk, pAig );
        vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
        vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
    }
    else
    {
        pAig = Abc_NtkToDar( pNtk, 0, 1 );
        pNtkOld = pNtk;
        vLive = populateLivenessVector( pNtk, pAig );
        vFair = populateFairnessVector( pNtk, pAig );
        vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
        vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
    }
 
    switch( directive )
    {
    case FULL_BIERE_MODE:
        //if( Vec_PtrSize(vLive) == 0 && Vec_PtrSize(vAssertSafety) == 0 )
        //{
        //    printf("Input circuit has NO safety and NO liveness property, original network is not disturbed\n");
        //    return 1;
        //}
        //else
        //{
            pAigNew = LivenessToSafetyTransformation( FULL_BIERE_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
            if( Aig_ManRegNum(pAigNew) != 0 )
                printf("A new circuit is produced with\n\t2 POs - one for safety and one for liveness.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created if the original circuit is combinational\n\tnon-property POs are suppressed\n");
            break;
        //}
    case FULL_BIERE_ONE_LOOP_MODE:
        //if( Vec_PtrSize(vLive) == 0 && Vec_PtrSize(vAssertSafety) == 0 )
        //{
        //    printf("Input circuit has NO safety and NO liveness property, original network is not disturbed\n");
        //    return 1;
        //}
        //else
        //{
            pAigNew = LivenessToSafetyTransformationOneStepLoop( FULL_BIERE_ONE_LOOP_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
            if( Aig_ManRegNum(pAigNew) != 0 )
                printf("A new circuit is produced with\n\t2 POs - one for safety and one for liveness.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created\n\tnon-property POs are suppressed\n");
            break;
        //}
    case IGNORE_LIVENESS_KEEP_SAFETY_MODE:
        //if( Vec_PtrSize(vAssertSafety) == 0 )
        //{    
        //    printf("Input circuit has NO safety property, original network is not disturbed\n");
        //    return 1;
        //}
        //else
        //{
            pAigNew = LivenessToSafetyTransformation( IGNORE_LIVENESS_KEEP_SAFETY_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
            if( Aig_ManRegNum(pAigNew) != 0 )
                printf("A new circuit is produced with\n\t1 PO - only for safety property; liveness properties are ignored, if any.\n\tno additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created\n\tnon-property POs are suppressed\n");
            break;
        //}
    case IGNORE_SAFETY_KEEP_LIVENESS_MODE:
        //if( Vec_PtrSize(vLive) == 0 )
        //{    
        //    printf("Input circuit has NO liveness property, original network is not disturbed\n");
        //    return 1;
        //}
        //else
        //{
            pAigNew = LivenessToSafetyTransformation( IGNORE_SAFETY_KEEP_LIVENESS_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
            if( Aig_ManRegNum(pAigNew) != 0 )
                printf("A new circuit is produced with\n\t1 PO - only for liveness property; safety properties are ignored, if any.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created if the original circuit is combinational\n\tnon-property POs are suppressed\n");
            break;
        //}
    case IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE:
        //if( Vec_PtrSize(vLive) == 0 )
        //{
        //    printf("Input circuit has NO liveness property, original network is not disturbed\n");
        //    return 1;
        //}
        //else
        //{
            pAigNew = LivenessToSafetyTransformationOneStepLoop( IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
            if( Aig_ManRegNum(pAigNew) != 0 )
                printf("New circuit is produced ignoring safety outputs!\nOnly liveness and fairness outputs are considered.\nShadow registers are not created\n");
            break;
        //}
    }
 
#if 0
    if( argc == 1 )
    {
        pAigNew = LivenessToSafetyTransformation( FULL_BIERE_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
        if( Aig_ManRegNum(pAigNew) != 0 )
            printf("New circuit is produced considering all safety, liveness and fairness outputs.\nBiere's logic is created\n");
    }
    else 
    {
        Extra_UtilGetoptReset();
        c = Extra_UtilGetopt( argc, argv, "1lsh" );
        if( c == '1' )
        {
            if ( pNtk == NULL )
            {
                fprintf( pErr, "Empty network.\n" );
                return 1;
            }
            if( !Abc_NtkIsStrash( pNtk ) )
            {
                printf("The input network was not strashed, strashing....\n");
                pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
                pNtkOld = pNtkTemp;
                pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
                vLive = populateLivenessVector( pNtk, pAig );
                vFair = populateFairnessVector( pNtk, pAig );
                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
            }
            else
            {
                pAig = Abc_NtkToDar( pNtk, 0, 1 );
                pNtkOld = pNtk;
                vLive = populateLivenessVector( pNtk, pAig );
                vFair = populateFairnessVector( pNtk, pAig );
                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
            }
            pAigNew = LivenessToSafetyTransformationOneStepLoop( pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
        }
        else if( c == 'l' )
        {
            if ( pNtk == NULL )
            {
                fprintf( pErr, "Empty network.\n" );
                return 1;
            }
            if( !Abc_NtkIsStrash( pNtk ) )
            {
                printf("The input network was not strashed, strashing....\n");
                pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
                pNtkOld = pNtkTemp;
                pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
                vLive = populateLivenessVector( pNtk, pAig );
                vFair = populateFairnessVector( pNtk, pAig );
                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
            }
            else
            {
                pAig = Abc_NtkToDar( pNtk, 0, 1 );
                pNtkOld = pNtk;
                vLive = populateLivenessVector( pNtk, pAig );
                vFair = populateFairnessVector( pNtk, pAig );
                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
            }
            pAigNew = LivenessToSafetyTransformation( IGNORE_LIVENESS_KEEP_SAFETY_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
            if( Aig_ManRegNum(pAigNew) != 0 )
                printf("New circuit is produced ignoring liveness outputs!\nOnly safety outputs are kept.\nBiere's logic is not created\n");
        }
        else if( c == 's' )
        {
            if ( pNtk == NULL )
            {
                fprintf( pErr, "Empty network.\n" );
                return 1;
            }
            
            if( !Abc_NtkIsStrash( pNtk ) )
            {
                printf("The input network was not strashed, strashing....\n");
                pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
                pNtkOld = pNtkTemp;
                pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
                vLive = populateLivenessVector( pNtk, pAig );
                vFair = populateFairnessVector( pNtk, pAig );
                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
            }
            else
            {
                pAig = Abc_NtkToDar( pNtk, 0, 1 );
                pNtkOld = pNtk;
                vLive = populateLivenessVector( pNtk, pAig );
                vFair = populateFairnessVector( pNtk, pAig );
                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
            }
            pAigNew = LivenessToSafetyTransformation( IGNORE_SAFETY_KEEP_LIVENESS_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
            if( Aig_ManRegNum(pAigNew) != 0 )
                printf("New circuit is produced ignoring safety outputs!\nOnly liveness and fairness outputs are considered.\nBiere's logic is created\n");
        }
        else if( c == 'h' )
            goto usage;
        else
            goto usage;
    }
#endif
    
#if 0
    Aig_ManPrintStats( pAigNew );
    printf("\nDetail statistics*************************************\n");
    printf("Number of true primary inputs = %d\n", Saig_ManPiNum( pAigNew ));
    printf("Number of true primary outputs = %d\n", Saig_ManPoNum( pAigNew ));
    printf("Number of true latch outputs = %d\n", Saig_ManCiNum( pAigNew ) - Saig_ManPiNum( pAigNew ));
    printf("Number of true latch inputs = %d\n", Saig_ManCoNum( pAigNew ) - Saig_ManPoNum( pAigNew ));
    printf("Numer of registers = %d\n", Saig_ManRegNum( pAigNew ) );
    printf("\n*******************************************************\n");
#endif
 
    pNtkNew = Abc_NtkFromAigPhase( pAigNew );
    pNtkNew->pName = Abc_UtilStrsav( pAigNew->pName );
    
    if ( !Abc_NtkCheck( pNtkNew ) )
        fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" );
    
    updateNewNetworkNameManager( pNtkNew, pAigNew, vecPiNames, vecLoNames );
    Abc_FrameSetCurrentNetwork( pAbc, pNtkNew );
 
#if 0
#ifndef DUPLICATE_CKT_DEBUG
    Saig_ManForEachPi( pAigNew, pObj, i )
        assert( strcmp( (char *)Vec_PtrEntry(vecPiNames, i), retrieveTruePiName( pNtk, pAig, pAigNew, pObj ) ) == 0 );
        //printf("Name of %d-th Pi = %s, %s\n", i, retrieveTruePiName( pNtk, pAig, pAigNew, pObj ), (char *)Vec_PtrEntry(vecPiNames, i) );
 
    Saig_ManForEachLo( pAigNew, pObj, i )
        assert( strcmp( (char *)Vec_PtrEntry(vecLoNames, i), retrieveLOName( pNtk, pAig, pAigNew, pObj, vLive, vFair ) ) == 0 );
#endif    
#endif
        
    return 0;
 
usage:
    fprintf( stdout, "usage: l2s [-1lsh]\n" );
    fprintf( stdout, "\t         performs Armin Biere's live-to-safe transformation\n" );
    fprintf( stdout, "\t-1 : no shadow logic, presume all loops are self loops\n");
    fprintf( stdout, "\t-l : ignore liveness and fairness outputs\n");
    fprintf( stdout, "\t-s : ignore safety assertions and assumptions\n");
    fprintf( stdout, "\t-h : print command usage\n");
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_CommandAbcLivenessToSafetySim()

int Abc_CommandAbcLivenessToSafetySim ( Abc_Frame_t * pAbc, int argc, char ** argv )

extern

Definition at line 754 of file liveness_sim.c.

{
    FILE * pOut, * pErr;
    Abc_Ntk_t * pNtk, * pNtkTemp, *pNtkNew, *pNtkOld;
    Aig_Man_t * pAig, *pAigNew;
    int c;
    Vec_Ptr_t * vLive, * vFair;
                
    pNtk = Abc_FrameReadNtk(pAbc);
    pOut = Abc_FrameReadOut(pAbc);
    pErr = Abc_FrameReadErr(pAbc);
 
    if ( pNtk == NULL )
    {
        fprintf( pErr, "Empty network.\n" );
        return 1;
    }
 
    if( !Abc_NtkIsStrash( pNtk ) )
    {
        printf("\nThe input network was not strashed, strashing....\n");
        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
        pNtkOld = pNtkTemp;
        pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
        vLive = populateLivenessVector( pNtk, pAig );
        vFair = populateFairnessVector( pNtk, pAig );
    }
    else
    {
        pAig = Abc_NtkToDar( pNtk, 0, 1 );
        pNtkOld = pNtk;
        vLive = populateLivenessVector( pNtk, pAig );
        vFair = populateFairnessVector( pNtk, pAig );
    }
 
#if 0
    Aig_ManPrintStats( pAig );
    printf("\nDetail statistics*************************************\n");
    printf("Number of true primary inputs = %d\n", Saig_ManPiNum( pAig ));
    printf("Number of true primary outputs = %d\n", Saig_ManPoNum( pAig ));
    printf("Number of true latch outputs = %d\n", Saig_ManCiNum( pAig ) - Saig_ManPiNum( pAig ));
    printf("Number of true latch inputs = %d\n", Saig_ManCoNum( pAig ) - Saig_ManPoNum( pAig ));
    printf("Numer of registers = %d\n", Saig_ManRegNum( pAig ) );
    printf("\n*******************************************************\n");
#endif
 
    c = Extra_UtilGetopt( argc, argv, "1" );
    if( c == '1' )
        pAigNew = LivenessToSafetyTransformationOneStepLoopSim( pNtk, pAig, vLive, vFair );
    else
        pAigNew = LivenessToSafetyTransformationSim( pNtk, pAig, vLive, vFair );
    
#if 0
    Aig_ManPrintStats( pAigNew );
    printf("\nDetail statistics*************************************\n");
    printf("Number of true primary inputs = %d\n", Saig_ManPiNum( pAigNew ));
    printf("Number of true primary outputs = %d\n", Saig_ManPoNum( pAigNew ));
    printf("Number of true latch outputs = %d\n", Saig_ManCiNum( pAigNew ) - Saig_ManPiNum( pAigNew ));
    printf("Number of true latch inputs = %d\n", Saig_ManCoNum( pAigNew ) - Saig_ManPoNum( pAigNew ));
    printf("Numer of registers = %d\n", Saig_ManRegNum( pAigNew ) );
    printf("\n*******************************************************\n");
#endif
 
    pNtkNew = Abc_NtkFromAigPhase( pAigNew );
 
    if ( !Abc_NtkCheck( pNtkNew ) )
        fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" );
    
    updateNewNetworkNameManager( pNtkNew, pAigNew, vecPiNames,vecLoNames );
    Abc_FrameSetCurrentNetwork( pAbc, pNtkNew );
 
    //Saig_ManForEachPi( pAigNew, pObj, i )
    //    printf("Name of %d-th Pi = %s\n", i, retrieveTruePiName( pNtk, pAig, pAigNew, pObj ) );
 
    //Saig_ManForEachLo( pAigNew, pObj, i )
    //    printf("Name of %d-th Lo = %s\n", i, retrieveLOName( pNtk, pAig, pAigNew, pObj, vLive, vFair ) );
 
    //printVecPtrOfString( vecPiNames );
    //printVecPtrOfString( vecLoNames );
 
#if 0
#ifndef DUPLICATE_CKT_DEBUG
    Saig_ManForEachPi( pAigNew, pObj, i )
        assert( strcmp( (char *)Vec_PtrEntry(vecPiNames, i), retrieveTruePiName( pNtk, pAig, pAigNew, pObj ) ) == 0 );
        //printf("Name of %d-th Pi = %s, %s\n", i, retrieveTruePiName( pNtk, pAig, pAigNew, pObj ), (char *)Vec_PtrEntry(vecPiNames, i) );
 
    Saig_ManForEachLo( pAigNew, pObj, i )
        assert( strcmp( (char *)Vec_PtrEntry(vecLoNames, i), retrieveLOName( pNtk, pAig, pAigNew, pObj, vLive, vFair ) ) == 0 );
#endif    
#endif
        
    return 0;
 
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_CommandAbcLivenessToSafetyWithLTL()

int Abc_CommandAbcLivenessToSafetyWithLTL ( Abc_Frame_t * pAbc, int argc, char ** argv )

extern

Definition at line 2268 of file liveness.c.

{
    FILE * pOut, * pErr;
    Abc_Ntk_t * pNtk, * pNtkTemp, *pNtkNew, *pNtkOld;
    Aig_Man_t * pAig, *pAigNew = NULL;
    int c;
    Vec_Ptr_t * vLive, * vFair, *vAssertSafety, *vAssumeSafety;
    int directive = -1;
//    char *ltfFormulaString = NULL;
    int numOfLtlPropOutput;//, LTL_FLAG = 0;
    Vec_Ptr_t *ltlBuffer;
                
    pNtk = Abc_FrameReadNtk(pAbc);
    pOut = Abc_FrameReadOut(pAbc);
    pErr = Abc_FrameReadErr(pAbc);
 
    if( argc == 1 )
    {
        assert( directive == -1 );
        directive = FULL_BIERE_MODE;
    }
    else
    {
        Extra_UtilGetoptReset();
        while ( ( c = Extra_UtilGetopt( argc, argv, "1slhf" ) ) != EOF )
        {
            switch( c )
            {
            case '1': 
                if( directive == -1 )
                    directive = FULL_BIERE_ONE_LOOP_MODE;
                else
                {
                    assert( directive == IGNORE_LIVENESS_KEEP_SAFETY_MODE || directive == IGNORE_SAFETY_KEEP_LIVENESS_MODE );
                    if( directive == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
                        directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE;
                    else
                        directive = IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE;
                }
                break;
            case 's':
                if( directive == -1 )
                    directive = IGNORE_SAFETY_KEEP_LIVENESS_MODE;
                else
                {
                    if( directive != FULL_BIERE_ONE_LOOP_MODE )
                        goto usage;
                    assert(directive == FULL_BIERE_ONE_LOOP_MODE);
                    directive = IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE;
                }
                break;
            case 'l':
                if( directive == -1 )
                    directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE;
                else
                {
                    if( directive != FULL_BIERE_ONE_LOOP_MODE )
                        goto usage;
                    assert(directive == FULL_BIERE_ONE_LOOP_MODE);
                    directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE;
                }
                break;
            case 'f':
                //assert( argc >= 3 );
                //vecLtlFormula = Vec_PtrAlloc( argc - 2 );
                //if( argc >= 3 )
                //{
                //    for( t=3; t<=argc; t++ )
                //    {
                //        printf("argv[%d] = %s\n", t-1, argv[t-1]);
                //        Vec_PtrPush( vecLtlFormula, argv[t-1] );
                //    }
                //}
                //printf("argv[argc] = %s\n", argv[argc-1]);
                //ltfFormulaString = argv[2];
                
                //LTL_FLAG = 1;
                printf("\nILLEGAL FLAG: aborting....\n");
                exit(0);
                break;
            case 'h':
                goto usage;
            default:
                goto usage;
            }
        }
    }
 
    if ( pNtk == NULL )
    {
        fprintf( pErr, "Empty network.\n" );
        return 1;
    }
    if( !Abc_NtkIsStrash( pNtk ) )
    {
        printf("The input network was not strashed, strashing....\n");
        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
        pNtkOld = pNtkTemp;
        pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
        vLive = populateLivenessVector( pNtk, pAig );
        vFair = populateFairnessVector( pNtk, pAig );
        vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
        vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
    }
    else
    {
        pAig = Abc_NtkToDar( pNtk, 0, 1 );
        pNtkOld = pNtk;
        vLive = populateLivenessVector( pNtk, pAig );
        vFair = populateFairnessVector( pNtk, pAig );
        vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
        vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
    }
 
    if( pAbc->vLTLProperties_global != NULL )
        ltlBuffer = pAbc->vLTLProperties_global;
    else
        ltlBuffer = NULL;
 
    switch( directive )
    {
    case FULL_BIERE_MODE:
            pAigNew = LivenessToSafetyTransformationWithLTL( FULL_BIERE_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety, &numOfLtlPropOutput, ltlBuffer );
            if( Aig_ManRegNum(pAigNew) != 0 )
                printf("A new circuit is produced with\n\t%d POs - one for safety and %d for liveness.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created if the original circuit is combinational\n\tnon-property POs are suppressed\n", numOfLtlPropOutput+1, numOfLtlPropOutput);
            break;
        
    case FULL_BIERE_ONE_LOOP_MODE:
            pAigNew = LivenessToSafetyTransformationOneStepLoop( FULL_BIERE_ONE_LOOP_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
            if( Aig_ManRegNum(pAigNew) != 0 )
                printf("A new circuit is produced with\n\t2 POs - one for safety and one for liveness.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created\n\tnon-property POs are suppressed\n");
            break;
        
    case IGNORE_LIVENESS_KEEP_SAFETY_MODE:
            pAigNew = LivenessToSafetyTransformationWithLTL( IGNORE_LIVENESS_KEEP_SAFETY_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety, &numOfLtlPropOutput, ltlBuffer );
            assert( numOfLtlPropOutput == 0 );
            if( Aig_ManRegNum(pAigNew) != 0 )
                printf("A new circuit is produced with\n\t1 PO - only for safety property; liveness properties are ignored, if any.\n\tno additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created\n\tnon-property POs are suppressed\n");
            break;
        
    case IGNORE_SAFETY_KEEP_LIVENESS_MODE:
            pAigNew = LivenessToSafetyTransformationWithLTL( IGNORE_SAFETY_KEEP_LIVENESS_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety, &numOfLtlPropOutput, ltlBuffer );
            if( Aig_ManRegNum(pAigNew) != 0 )
                printf("A new circuit is produced with\n\t%d PO - only for liveness property; safety properties are ignored, if any.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created if the original circuit is combinational\n\tnon-property POs are suppressed\n", numOfLtlPropOutput);
            break;
        
    case IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE:
            pAigNew = LivenessToSafetyTransformationOneStepLoop( IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
            if( Aig_ManRegNum(pAigNew) != 0 )
                printf("New circuit is produced ignoring safety outputs!\nOnly liveness and fairness outputs are considered.\nShadow registers are not created\n");
            break;
    }
 
#if 0
    if( argc == 1 )
    {
        pAigNew = LivenessToSafetyTransformation( FULL_BIERE_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
        if( Aig_ManRegNum(pAigNew) != 0 )
            printf("New circuit is produced considering all safety, liveness and fairness outputs.\nBiere's logic is created\n");
    }
    else 
    {
        Extra_UtilGetoptReset();
        c = Extra_UtilGetopt( argc, argv, "1lsh" );
        if( c == '1' )
        {
            if ( pNtk == NULL )
            {
                fprintf( pErr, "Empty network.\n" );
                return 1;
            }
            if( !Abc_NtkIsStrash( pNtk ) )
            {
                printf("The input network was not strashed, strashing....\n");
                pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
                pNtkOld = pNtkTemp;
                pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
                vLive = populateLivenessVector( pNtk, pAig );
                vFair = populateFairnessVector( pNtk, pAig );
                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
            }
            else
            {
                pAig = Abc_NtkToDar( pNtk, 0, 1 );
                pNtkOld = pNtk;
                vLive = populateLivenessVector( pNtk, pAig );
                vFair = populateFairnessVector( pNtk, pAig );
                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
            }
            pAigNew = LivenessToSafetyTransformationOneStepLoop( pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
        }
        else if( c == 'l' )
        {
            if ( pNtk == NULL )
            {
                fprintf( pErr, "Empty network.\n" );
                return 1;
            }
            if( !Abc_NtkIsStrash( pNtk ) )
            {
                printf("The input network was not strashed, strashing....\n");
                pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
                pNtkOld = pNtkTemp;
                pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
                vLive = populateLivenessVector( pNtk, pAig );
                vFair = populateFairnessVector( pNtk, pAig );
                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
            }
            else
            {
                pAig = Abc_NtkToDar( pNtk, 0, 1 );
                pNtkOld = pNtk;
                vLive = populateLivenessVector( pNtk, pAig );
                vFair = populateFairnessVector( pNtk, pAig );
                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
            }
            pAigNew = LivenessToSafetyTransformation( IGNORE_LIVENESS_KEEP_SAFETY_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
            if( Aig_ManRegNum(pAigNew) != 0 )
                printf("New circuit is produced ignoring liveness outputs!\nOnly safety outputs are kept.\nBiere's logic is not created\n");
        }
        else if( c == 's' )
        {
            if ( pNtk == NULL )
            {
                fprintf( pErr, "Empty network.\n" );
                return 1;
            }
            
            if( !Abc_NtkIsStrash( pNtk ) )
            {
                printf("The input network was not strashed, strashing....\n");
                pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
                pNtkOld = pNtkTemp;
                pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
                vLive = populateLivenessVector( pNtk, pAig );
                vFair = populateFairnessVector( pNtk, pAig );
                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
            }
            else
            {
                pAig = Abc_NtkToDar( pNtk, 0, 1 );
                pNtkOld = pNtk;
                vLive = populateLivenessVector( pNtk, pAig );
                vFair = populateFairnessVector( pNtk, pAig );
                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
            }
            pAigNew = LivenessToSafetyTransformation( IGNORE_SAFETY_KEEP_LIVENESS_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
            if( Aig_ManRegNum(pAigNew) != 0 )
                printf("New circuit is produced ignoring safety outputs!\nOnly liveness and fairness outputs are considered.\nBiere's logic is created\n");
        }
        else if( c == 'h' )
            goto usage;
        else
            goto usage;
    }
#endif
    
#if 0
    Aig_ManPrintStats( pAigNew );
    printf("\nDetail statistics*************************************\n");
    printf("Number of true primary inputs = %d\n", Saig_ManPiNum( pAigNew ));
    printf("Number of true primary outputs = %d\n", Saig_ManPoNum( pAigNew ));
    printf("Number of true latch outputs = %d\n", Saig_ManCiNum( pAigNew ) - Saig_ManPiNum( pAigNew ));
    printf("Number of true latch inputs = %d\n", Saig_ManCoNum( pAigNew ) - Saig_ManPoNum( pAigNew ));
    printf("Numer of registers = %d\n", Saig_ManRegNum( pAigNew ) );
    printf("\n*******************************************************\n");
#endif
 
    pNtkNew = Abc_NtkFromAigPhase( pAigNew );
    pNtkNew->pName = Abc_UtilStrsav( pAigNew->pName );
    
    if ( !Abc_NtkCheck( pNtkNew ) )
        fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" );
    
    updateNewNetworkNameManager( pNtkNew, pAigNew, vecPiNames, vecLoNames );
    Abc_FrameSetCurrentNetwork( pAbc, pNtkNew );
 
#if 0
#ifndef DUPLICATE_CKT_DEBUG
    Saig_ManForEachPi( pAigNew, pObj, i )
        assert( strcmp( (char *)Vec_PtrEntry(vecPiNames, i), retrieveTruePiName( pNtk, pAig, pAigNew, pObj ) ) == 0 );
        //printf("Name of %d-th Pi = %s, %s\n", i, retrieveTruePiName( pNtk, pAig, pAigNew, pObj ), (char *)Vec_PtrEntry(vecPiNames, i) );
 
    Saig_ManForEachLo( pAigNew, pObj, i )
        assert( strcmp( (char *)Vec_PtrEntry(vecLoNames, i), retrieveLOName( pNtk, pAig, pAigNew, pObj, vLive, vFair ) ) == 0 );
#endif    
#endif
        
    return 0;
 
usage:
    fprintf( stdout, "usage: l3s [-1lsh]\n" );
    fprintf( stdout, "\t         performs Armin Biere's live-to-safe transformation\n" );
    fprintf( stdout, "\t-1 : no shadow logic, presume all loops are self loops\n");
    fprintf( stdout, "\t-l : ignore liveness and fairness outputs\n");
    fprintf( stdout, "\t-s : ignore safety assertions and assumptions\n");
    fprintf( stdout, "\t-h : print command usage\n");
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_CommandCexMin()

int Abc_CommandCexMin	(	Abc_Frame_t *	pAbc,
		int	argc,
		char **	argv )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 32479 of file abc.c.

{
    Abc_Ntk_t * pNtk;
    Abc_Cex_t * vCexNew = NULL;
    int c;
    int nConfLimit = 1000;
    int nRounds    =    1;
    int fVerbose   =    0;
    Extra_UtilGetoptReset();
    while ( ( c = Extra_UtilGetopt( argc, argv, "CRvh" ) ) != EOF )
    {
        switch ( c )
        {
        case 'C':
            if ( globalUtilOptind >= argc )
            {
                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
                goto usage;
            }
            nConfLimit = atoi(argv[globalUtilOptind]);
            globalUtilOptind++;
            if ( nConfLimit < 0 )
                goto usage;
            break;
        case 'R':
            if ( globalUtilOptind >= argc )
            {
                Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
                goto usage;
            }
            nRounds = atoi(argv[globalUtilOptind]);
            globalUtilOptind++;
            if ( nRounds < 0 )
                goto usage;
            break;
        case 'v':
            fVerbose ^= 1;
            break;
        case 'h':
            goto usage;
        default:
            Abc_Print( -2, "Unknown switch.\n");
            goto usage;
        }
    }
 
    if ( pAbc->pCex == NULL )
    {
        Abc_Print( 1, "There is no current cex.\n");
        return 0;
    }
 
    // check the main AIG
    pNtk = Abc_FrameReadNtk(pAbc);
    if ( pNtk == NULL )
        Abc_Print( 1, "Main AIG: There is no current network.\n");
    else if ( !Abc_NtkIsStrash(pNtk) )
        Abc_Print( 1, "Main AIG: The current network is not an AIG.\n");
    else if ( Abc_NtkPiNum(pNtk) != pAbc->pCex->nPis )
        Abc_Print( 1, "Main AIG: The number of PIs (%d) is different from cex (%d).\n", Abc_NtkPiNum(pNtk), pAbc->pCex->nPis );
//      else if ( Abc_NtkLatchNum(pNtk) != pAbc->pCex->nRegs )
//          Abc_Print( 1, "Main AIG: The number of registers (%d) is different from cex (%d).\n", Abc_NtkLatchNum(pNtk), pAbc->pCex->nRegs );
//      else if ( Abc_NtkPoNum(pNtk) <= pAbc->pCex->iPo )
//          Abc_Print( 1, "Main AIG: The number of POs (%d) is less than the PO index in cex (%d).\n", Abc_NtkPoNum(pNtk), pAbc->pCex->iPo );
    else
    {
        Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
        Gia_Man_t * pGia = Gia_ManFromAigSimple( pAig );
//        if ( !Gia_ManVerifyCex( pGia, pAbc->pCex, 0 ) )
        int iPoOld = pAbc->pCex->iPo;
        pAbc->pCex->iPo = Gia_ManFindFailedPoCex( pGia, pAbc->pCex, 0 );
        Gia_ManStop( pGia );
        if ( pAbc->pCex->iPo == -1 )
        {
            pAbc->pCex->iPo = iPoOld;
            Abc_Print( -1, "Main AIG: The cex does not fail any outputs.\n" );
            return 0;
        }
        else if ( iPoOld != pAbc->pCex->iPo )
            Abc_Print( 0, "Main AIG: The cex refined PO %d instead of PO %d.\n", pAbc->pCex->iPo, iPoOld );
        // perform minimization
        vCexNew = Saig_ManCexMinPerform( pAig, pAbc->pCex );
        Aig_ManStop( pAig );
        Abc_CexFree( vCexNew );
//        Abc_FrameReplaceCex( pAbc, &vCexNew );
 
//        Abc_Print( 1,"Implementation of this command is not finished.\n" );
    }
    return 0;
 
usage:
    Abc_Print( -2, "usage: cexmin [-CR num] [-vh]\n" );
    Abc_Print( -2, "\t         reduces the length of the counter-example\n" );
    Abc_Print( -2, "\t-C num : the maximum number of conflicts [default = %d]\n", nConfLimit );
    Abc_Print( -2, "\t-R num : the number of minimization rounds [default = %d]\n", nRounds );
    Abc_Print( -2, "\t-v     : toggle printing optimization summary [default = %s]\n", fVerbose? "yes": "no" );
    Abc_Print( -2, "\t-h     : print the command usage\n");
    return 1;
}

Here is the call graph for this function:

Abc_CommandCS_kLiveness()

int Abc_CommandCS_kLiveness ( Abc_Frame_t * pAbc, int argc, char ** argv )

extern

Definition at line 525 of file kliveness.c.

{
        Abc_Ntk_t * pNtk, * pNtkTemp;
    Aig_Man_t * pAig, *pAigCS, *pAigCSNew;
    int absorberCount;
    int absorberLimit = 500;
    int RetValue;
    int liveIndex_0 = -1, liveIndex_k = -1;
    int fVerbose = 1;
    int directive = -1;
    int c;
    int safetyInvariantPO = -1;
    abctime beginTime, endTime;
    double time_spent;
    Vec_Ptr_t *vMasterBarrierDisjuncts = NULL;
    Aig_Man_t *pWorkingAig;
    //FILE *fp;
 
    pNtk = Abc_FrameReadNtk(pAbc);
 
    //fp = fopen("propFile.txt", "r");
    //if( fp )
    //    getVecOfVecFairness(fp);
    //exit(0);
 
    /*************************************************
    Extraction of Command Line Argument    
    *************************************************/
    if( argc == 1 )
    {
        assert( directive == -1 );
        directive = SIMPLE_kCS;
    }
    else
    {
        Extra_UtilGetoptReset();
        while ( ( c = Extra_UtilGetopt( argc, argv, "cmCgh" ) ) != EOF )
        {
            switch( c )
            {
            case 'c':
                directive = kCS_WITH_SAFETY_INVARIANTS; 
                break;
            case 'm':
                directive = kCS_WITH_DISCOVER_MONOTONE_SIGNALS; 
                break;
            case 'C':
                directive = kCS_WITH_SAFETY_AND_DCS_INVARIANTS;
                break;
            case 'g':
                directive = kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS;
                break;
            case 'h':
                goto usage;
                break;
            default:
                goto usage;
            }
        }
    }
    /*************************************************
    Extraction of Command Line Argument Ends    
    *************************************************/
 
    if( !Abc_NtkIsStrash( pNtk ) )
    {
        printf("The input network was not strashed, strashing....\n");
        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
        pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
    }
    else
    {
        pAig = Abc_NtkToDar( pNtk, 0, 1 );
        pNtkTemp = pNtk;
    }
 
    if( directive == kCS_WITH_SAFETY_INVARIANTS )
    {
        safetyInvariantPO = collectSafetyInvariantPOIndex(pNtkTemp);            
        assert( safetyInvariantPO != -1 );
    }
 
    if(directive == kCS_WITH_DISCOVER_MONOTONE_SIGNALS)
    {
        beginTime = Abc_Clock();
        vMasterBarrierDisjuncts = findDisjunctiveMonotoneSignals( pNtk );
        endTime = Abc_Clock();
        time_spent = (double)(endTime - beginTime)/CLOCKS_PER_SEC;
        printf("pre-processing time = %f\n",time_spent); 
        return 0;
    }
 
    if(directive == kCS_WITH_SAFETY_AND_DCS_INVARIANTS)
    {
        safetyInvariantPO = collectSafetyInvariantPOIndex(pNtkTemp);            
        assert( safetyInvariantPO != -1 );
 
        beginTime = Abc_Clock();
        vMasterBarrierDisjuncts = findDisjunctiveMonotoneSignals( pNtk );
        endTime = Abc_Clock();
        time_spent = (double)(endTime - beginTime)/CLOCKS_PER_SEC;
        printf("pre-processing time = %f\n",time_spent); 
 
        assert( vMasterBarrierDisjuncts != NULL );
        assert( Vec_PtrSize(vMasterBarrierDisjuncts) > 0 );
    }
 
    if(directive == kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS)
    {
        safetyInvariantPO = collectSafetyInvariantPOIndex(pNtkTemp);            
        assert( safetyInvariantPO != -1 );
 
        beginTime = Abc_Clock();
        vMasterBarrierDisjuncts = collectUserGivenDisjunctiveMonotoneSignals( pNtk );
        endTime = Abc_Clock();
        time_spent = (double)(endTime - beginTime)/CLOCKS_PER_SEC;
        printf("pre-processing time = %f\n",time_spent); 
 
        assert( vMasterBarrierDisjuncts != NULL );
        assert( Vec_PtrSize(vMasterBarrierDisjuncts) > 0 );
    }
 
    if(directive == kCS_WITH_SAFETY_AND_DCS_INVARIANTS || directive == kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS)
    {
        assert( vMasterBarrierDisjuncts != NULL );
        pWorkingAig = generateWorkingAigWithDSC( pAig, pNtk, &liveIndex_0, vMasterBarrierDisjuncts );
        pAigCS = introduceAbsorberLogic(pWorkingAig, &liveIndex_0, &liveIndex_k, 0);
    }
    else
    {
        pWorkingAig = generateWorkingAig( pAig, pNtk, &liveIndex_0 );
        pAigCS = introduceAbsorberLogic(pWorkingAig, &liveIndex_0, &liveIndex_k, 0);
    }
 
    Aig_ManStop(pWorkingAig);
 
    for( absorberCount=1; absorberCount<absorberLimit; absorberCount++ )
    {
        //printf( "\nindex of the liveness output = %d\n", liveIndex_k );
        RetValue = flipConePdr( pAigCS, directive, liveIndex_k, safetyInvariantPO, absorberCount );
 
        if ( RetValue == 1 )
        {
                Abc_Print( 1, "k = %d, Property proved\n", absorberCount );
            break;
        }
            else if ( RetValue == 0 )
        {
            if( fVerbose )
            {
                Abc_Print( 1, "k = %d, Property DISPROVED\n", absorberCount );
            }
        }
            else if ( RetValue == -1 )
        {
                Abc_Print( 1, "Property UNDECIDED with k = %d.\n", absorberCount );
        }
            else
                assert( 0 );
 
        pAigCSNew = introduceAbsorberLogic(pAigCS, &liveIndex_0, &liveIndex_k, absorberCount);
        Aig_ManStop(pAigCS);
        pAigCS = pAigCSNew;
    }
 
    Aig_ManStop(pAigCS);
    Aig_ManStop(pAig);
 
    if(directive == kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS)
    {
        deallocateMasterBarrierDisjunctInt(vMasterBarrierDisjuncts);
    }
    else
    {
        //if(vMasterBarrierDisjuncts)
        //    Vec_PtrFree(vMasterBarrierDisjuncts);
        //deallocateMasterBarrierDisjunctVecPtrVecInt(vMasterBarrierDisjuncts);
        deallocateMasterBarrierDisjunctInt(vMasterBarrierDisjuncts);
    }
    return 0;
 
    usage:
        fprintf( stdout, "usage: kcs [-cmgCh]\n" );
            fprintf( stdout, "\timplements Claessen-Sorensson's k-Liveness algorithm\n" );
        fprintf( stdout, "\t-c : verification with constraints, looks for POs prefixed with csSafetyInvar_\n");
        fprintf( stdout, "\t-m : discovers monotone signals\n");
            fprintf( stdout, "\t-g : verification with user-supplied barriers, looks for POs prefixed with csLevel1Stabil_\n");
        fprintf( stdout, "\t-C : verification with discovered monotone signals\n");
        fprintf( stdout, "\t-h : print usage\n");
            return 1;
 
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_CommandNChooseK()

int Abc_CommandNChooseK ( Abc_Frame_t * pAbc, int argc, char ** argv )

extern

Definition at line 718 of file kliveness.c.

{
    Abc_Ntk_t * pNtk, * pNtkTemp, *pNtkCombStabil;
    Aig_Man_t * pAig, *pAigCombStabil;
    int directive = -1;
    int c;
    int parameterizedCombK;
 
    pNtk = Abc_FrameReadNtk(pAbc);
 
 
    /*************************************************
    Extraction of Command Line Argument    
    *************************************************/
    if( argc == 1 )
    {
        assert( directive == -1 );
        directive = SIMPLE_kCS;
    }
    else
    {
        Extra_UtilGetoptReset();
        while ( ( c = Extra_UtilGetopt( argc, argv, "cmCgh" ) ) != EOF )
        {
            switch( c )
            {
            case 'c':
                directive = kCS_WITH_SAFETY_INVARIANTS; 
                break;
            case 'm':
                directive = kCS_WITH_DISCOVER_MONOTONE_SIGNALS; 
                break;
            case 'C':
                directive = kCS_WITH_SAFETY_AND_DCS_INVARIANTS;
                break;
            case 'g':
                directive = kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS;
                break;
            case 'h':
                goto usage;
                break;
            default:
                goto usage;
            }
        }
    }
    /*************************************************
    Extraction of Command Line Argument Ends    
    *************************************************/
 
    if( !Abc_NtkIsStrash( pNtk ) )
    {
        printf("The input network was not strashed, strashing....\n");
        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
        pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
    }
    else
    {
        pAig = Abc_NtkToDar( pNtk, 0, 1 );
        pNtkTemp = pNtk;
    }
 
/**********************Code for generation of nCk outputs**/
    //combCount = countCombination(1000, 3);
    //pAigCombStabil = generateDisjunctiveTester( pNtk, pAig, 7, 2 );
    printf("Enter parameterizedCombK = " );
    if( scanf("%d", &parameterizedCombK) != 1 )
    {
        printf("\nFailed to read integer!\n");
        return 0;
    }
    printf("\n");
 
    pAigCombStabil = generateGeneralDisjunctiveTester( pNtk, pAig, parameterizedCombK );
    Aig_ManPrintStats(pAigCombStabil);
    pNtkCombStabil = Abc_NtkFromAigPhase( pAigCombStabil );
    pNtkCombStabil->pName = Abc_UtilStrsav( pAigCombStabil->pName );
    if ( !Abc_NtkCheck( pNtkCombStabil ) )
            fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" );
    Abc_FrameSetCurrentNetwork( pAbc, pNtkCombStabil );
 
    Aig_ManStop( pAigCombStabil );
    Aig_ManStop( pAig );
 
    return 1;
    //printf("\ncombCount = %d\n", combCount);
    //exit(0);
/**********************************************************/
 
    usage:
        fprintf( stdout, "usage: nck [-cmgCh]\n" );
            fprintf( stdout, "\tgenerates combinatorial signals for stabilization\n" );
        fprintf( stdout, "\t-h : print usage\n");
            return 1;
 
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_End()

void Abc_End

(

Abc_Frame_t *

pAbc

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1504 of file abc.c.

{
    extern Abc_Frame_t * Abc_FrameGetGlobalFrame();
    Abc_FrameClearDesign();
    Cnf_ManFree();
    {
        extern int Abc_NtkCompareAndSaveBest( Abc_Ntk_t * pNtk );
        Abc_NtkCompareAndSaveBest( NULL );
    }
    {
        extern void Dar_LibStop();
        Dar_LibStop();
    }
    {
        extern void Aig_RManQuit();
        Aig_RManQuit();
    }
    {
        extern void Npn_ManClean();
        Npn_ManClean();
    }
    {
        extern void Sdm_ManQuit();
        Sdm_ManQuit();
    }
    Abc_NtkFraigStoreClean();
    Gia_ManStopP( &pAbc->pGia );
    Gia_ManStopP( &pAbc->pGia2 );
    Gia_ManStopP( &pAbc->pGiaBest );
    Gia_ManStopP( &pAbc->pGiaBest2 );
    Gia_ManStopP( &pAbc->pGiaSaved );
    if ( Abc_NtkRecIsRunning3() )
        Abc_NtkRecStop3();
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_FrameClearDesign()

void Abc_FrameClearDesign

(

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 809 of file abc.c.

{
}

Here is the caller graph for this function:

Abc_FrameDeriveStatusArray()

Vec_Int_t * Abc_FrameDeriveStatusArray

(

Vec_Ptr_t *

vCexes

)

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

Synopsis [Derives array of statuses from the array of CEXes.]

Description []

SideEffects []

SeeAlso []

Definition at line 764 of file abc.c.

{
    Vec_Int_t * vStatuses;
    Abc_Cex_t * pCex;
    int i;
    if ( vCexes == NULL )
        return NULL;
    vStatuses = Vec_IntAlloc( Vec_PtrSize(vCexes) );
    Vec_IntFill( vStatuses, Vec_PtrSize(vCexes), -1 ); // assume UNDEC
    Vec_PtrForEachEntry( Abc_Cex_t *, vCexes, pCex, i )
        if ( pCex != NULL )
            Vec_IntWriteEntry( vStatuses, i, 0 ); // set this output as SAT
    return vStatuses;
}

Abc_FrameDeriveStatusArray2()

Vec_Int_t * Abc_FrameDeriveStatusArray2

(

Vec_Ptr_t *

vCexes

)

Definition at line 778 of file abc.c.

{
    Vec_Int_t * vStatuses;
    Abc_Cex_t * pCex;
    int i;
    if ( vCexes == NULL )
        return NULL;
    vStatuses = Vec_IntAlloc( Vec_PtrSize(vCexes) );
    Vec_IntFill( vStatuses, Vec_PtrSize(vCexes), -1 ); // assume UNDEC
    Vec_PtrForEachEntry( Abc_Cex_t *, vCexes, pCex, i )
        if ( pCex == (Abc_Cex_t *)(ABC_PTRINT_T)1 )
        {
            Vec_IntWriteEntry( vStatuses, i, 1 ); // set this output as UNSAT
            Vec_PtrWriteEntry( vCexes, i, NULL );
        }
        else if ( pCex != NULL )
            Vec_IntWriteEntry( vStatuses, i, 0 ); // set this output as SAT
    return vStatuses;
}

Abc_FrameGetGia()

Gia_Man_t * Abc_FrameGetGia

(

Abc_Frame_t *

pAbc

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 869 of file abc.c.

{
    Gia_Man_t * pGia;
    if ( pAbc->pGia2 )
        Gia_ManStop( pAbc->pGia2 );
    pAbc->pGia2 = NULL;
    pGia = pAbc->pGia;
    pAbc->pGia = NULL;
    return pGia;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_FrameReplaceCex()

void Abc_FrameReplaceCex	(	Abc_Frame_t *	pAbc,
		Abc_Cex_t **	ppCex )

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 679 of file abc.c.

{
    // update CEX
    ABC_FREE( pAbc->pCex );
    pAbc->pCex = *ppCex;
    *ppCex = NULL;
    // remove CEX vector
    if ( pAbc->vCexVec )
    {
        Vec_PtrFreeFree( pAbc->vCexVec );
        pAbc->vCexVec = NULL;
    }
}

Here is the caller graph for this function:

Abc_FrameReplaceCexVec()

void Abc_FrameReplaceCexVec	(	Abc_Frame_t *	pAbc,
		Vec_Ptr_t **	pvCexVec )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 704 of file abc.c.

{
    // update CEX vector
    if ( pAbc->vCexVec )
        Vec_PtrFreeFree( pAbc->vCexVec );
    pAbc->vCexVec = *pvCexVec;
    *pvCexVec = NULL;
    // remove CEX
    ABC_FREE( pAbc->pCex );
}

Here is the caller graph for this function:

Abc_FrameReplacePoEquivs()

void Abc_FrameReplacePoEquivs	(	Abc_Frame_t *	pAbc,
		Vec_Ptr_t **	pvPoEquivs )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 726 of file abc.c.

{
    if ( pAbc->vPoEquivs )
        Vec_VecFree( (Vec_Vec_t *)pAbc->vPoEquivs );
    pAbc->vPoEquivs = *pvPoEquivs;
    *pvPoEquivs = NULL;
}

Here is the caller graph for this function:

Abc_FrameReplacePoStatuses()

void Abc_FrameReplacePoStatuses	(	Abc_Frame_t *	pAbc,
		Vec_Int_t **	pvStatuses )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 745 of file abc.c.

{
    if ( pAbc->vStatuses )
        Vec_IntFree( pAbc->vStatuses );
    pAbc->vStatuses = *pvStatuses;
    *pvStatuses = NULL;
}

Abc_FrameUpdateGia()

void Abc_FrameUpdateGia	(	Abc_Frame_t *	pAbc,
		Gia_Man_t *	pNew )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 824 of file abc.c.

{
    if ( pNew == NULL )
    {
        Abc_Print( -1, "Abc_FrameUpdateGia(): Transformation has failed.\n" );
        return;
    }
    if ( Gia_ManPoNum(pNew) == 0 )
        Abc_Print( 0, "The current GIA has no primary outputs. Some commands may not work correctly.\n" );
    if ( pNew == pAbc->pGia )
        return;
    // transfer names
    if (!pNew->vNamesIn && pAbc->pGia && pAbc->pGia->vNamesIn && Gia_ManCiNum(pNew) == Vec_PtrSize(pAbc->pGia->vNamesIn))
    {
        pNew->vNamesIn = pAbc->pGia->vNamesIn;
        pAbc->pGia->vNamesIn = NULL;
    }
    if (!pNew->vNamesOut && pAbc->pGia && pAbc->pGia->vNamesOut && Gia_ManCoNum(pNew) == Vec_PtrSize(pAbc->pGia->vNamesOut))
    {
        pNew->vNamesOut = pAbc->pGia->vNamesOut;
        pAbc->pGia->vNamesOut = NULL;
    }
    if (!pNew->vNamesNode && pAbc->pGia && pAbc->pGia->vNamesNode && Gia_ManObjNum(pNew) == Vec_PtrSize(pAbc->pGia->vNamesNode))
    {
        pNew->vNamesNode = pAbc->pGia->vNamesNode;
        pAbc->pGia->vNamesNode = NULL;
    }
    // update
    if ( pAbc->pGia2 )
        Gia_ManStop( pAbc->pGia2 );
    pAbc->pGia2 = pAbc->pGia;
    pAbc->pGia  = pNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_Init()

void Abc_Init

(

Abc_Frame_t *

pAbc

)

DECLARATIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 892 of file abc.c.

{
    Cmd_CommandAdd( pAbc, "Printing",     "ps",            Abc_CommandPrintStats,       0 );
    Cmd_CommandAdd( pAbc, "Printing",     "print_stats",   Abc_CommandPrintStats,       0 );
    Cmd_CommandAdd( pAbc, "Printing",     "print_exdc",    Abc_CommandPrintExdc,        0 );
    Cmd_CommandAdd( pAbc, "Printing",     "print_io",      Abc_CommandPrintIo,          0 );
    Cmd_CommandAdd( pAbc, "Printing",     "print_latch",   Abc_CommandPrintLatch,       0 );
    Cmd_CommandAdd( pAbc, "Printing",     "pfan",          Abc_CommandPrintFanio,       0 );
    Cmd_CommandAdd( pAbc, "Printing",     "print_fanio",   Abc_CommandPrintFanio,       0 );
    Cmd_CommandAdd( pAbc, "Printing",     "print_mffc",    Abc_CommandPrintMffc,        0 );
    Cmd_CommandAdd( pAbc, "Printing",     "pf",            Abc_CommandPrintFactor,      0 );
    Cmd_CommandAdd( pAbc, "Printing",     "print_factor",  Abc_CommandPrintFactor,      0 );
    Cmd_CommandAdd( pAbc, "Printing",     "print_level",   Abc_CommandPrintLevel,       0 );
    Cmd_CommandAdd( pAbc, "Printing",     "psu",           Abc_CommandPrintSupport,     0 );
    Cmd_CommandAdd( pAbc, "Printing",     "print_supp",    Abc_CommandPrintSupport,     0 );
#ifdef ABC_USE_CUDD
    Cmd_CommandAdd( pAbc, "Printing",     "print_mint",    Abc_CommandPrintMint,        0 );
#endif
    Cmd_CommandAdd( pAbc, "Printing",     "print_symm",    Abc_CommandPrintSymms,       0 );
    Cmd_CommandAdd( pAbc, "Printing",     "print_unate",   Abc_CommandPrintUnate,       0 );
    Cmd_CommandAdd( pAbc, "Printing",     "print_auto",    Abc_CommandPrintAuto,        0 );
    Cmd_CommandAdd( pAbc, "Printing",     "print_kmap",    Abc_CommandPrintKMap,        0 );
    Cmd_CommandAdd( pAbc, "Printing",     "pg",            Abc_CommandPrintGates,       0 );
    Cmd_CommandAdd( pAbc, "Printing",     "print_gates",   Abc_CommandPrintGates,       0 );
    Cmd_CommandAdd( pAbc, "Printing",     "print_sharing", Abc_CommandPrintSharing,     0 );
    Cmd_CommandAdd( pAbc, "Printing",     "print_xcut",    Abc_CommandPrintXCut,        0 );
    Cmd_CommandAdd( pAbc, "Printing",     "print_dsd",     Abc_CommandPrintDsd,         0 );
    Cmd_CommandAdd( pAbc, "Printing",     "print_cone",    Abc_CommandPrintCone,        0 );
    Cmd_CommandAdd( pAbc, "Printing",     "print_miter",   Abc_CommandPrintMiter,       0 );
    Cmd_CommandAdd( pAbc, "Printing",     "print_status",  Abc_CommandPrintStatus,      0 );
    Cmd_CommandAdd( pAbc, "Printing",     "print_delay",   Abc_CommandPrintDelay,       0 );
 
    Cmd_CommandAdd( pAbc, "Printing",     "show",          Abc_CommandShow,             0 );
    Cmd_CommandAdd( pAbc, "Printing",     "show_bdd",      Abc_CommandShowBdd,          0 );
    Cmd_CommandAdd( pAbc, "Printing",     "show_cut",      Abc_CommandShowCut,          0 );
 
    Cmd_CommandAdd( pAbc, "Synthesis",    "clp",           Abc_CommandCollapse,         1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "collapse",      Abc_CommandCollapse,         1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "satclp",        Abc_CommandSatClp,           1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "st",            Abc_CommandStrash,           1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "strash",        Abc_CommandStrash,           1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "b",             Abc_CommandBalance,          1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "balance",       Abc_CommandBalance,          1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "mux_struct",    Abc_CommandMuxStruct,        1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "multi",         Abc_CommandMulti,            1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "renode",        Abc_CommandRenode,           1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "cleanup",       Abc_CommandCleanup,          1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "sweep",         Abc_CommandSweep,            1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "fx",            Abc_CommandFastExtract,      1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "fxch",          Abc_CommandFxch,             1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "eliminate",     Abc_CommandEliminate,        1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "dsd",           Abc_CommandDisjoint,         1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "sparsify",      Abc_CommandSparsify,         1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "lutpack",       Abc_CommandLutpack,          1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "lutmin",        Abc_CommandLutmin,           1 );
//    Cmd_CommandAdd( pAbc, "Synthesis",    "imfs",          Abc_CommandImfs,             1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "mfs",           Abc_CommandMfs,              1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "mfs2",          Abc_CommandMfs2,             1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "mfs3",          Abc_CommandMfs3,             1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "mfse",          Abc_CommandMfse,              1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "logicpush",     Abc_CommandLogicPush,        1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "trace",         Abc_CommandTrace,            0 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "glitch",        Abc_CommandGlitch,           0 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "speedup",       Abc_CommandSpeedup,          1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "powerdown",     Abc_CommandPowerdown,        1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "addbuffs",      Abc_CommandAddBuffs,         1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "merge",         Abc_CommandMerge,            1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "testdec",       Abc_CommandTestDec,          0 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "testnpn",       Abc_CommandTestNpn,          0 );
    Cmd_CommandAdd( pAbc, "LogiCS",       "testrpo",       Abc_CommandTestRPO,          0 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "testtruth",     Abc_CommandTestTruth,        0 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "testsupp",      Abc_CommandTestSupp,         0 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "testrand",      Abc_CommandTestRand,         0 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "runsat",        Abc_CommandRunSat,           0 );    
    Cmd_CommandAdd( pAbc, "Synthesis",    "runeco",        Abc_CommandRunEco,           0 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "rungen",        Abc_CommandRunGen,           0 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "runscript",     Abc_CommandRunScript,        0 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "xec",           Abc_CommandRunTest,          0 );
 
    Cmd_CommandAdd( pAbc, "Synthesis",    "rewrite",       Abc_CommandRewrite,          1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "refactor",      Abc_CommandRefactor,         1 );
//    Cmd_CommandAdd( pAbc, "Synthesis",    "restructure",   Abc_CommandRestructure,      1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "resub",         Abc_CommandResubstitute,     1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "resub_unate",   Abc_CommandResubUnate,       1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "resub_core",    Abc_CommandResubCore,        1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "resub_check",   Abc_CommandResubCheck,       0 );
//    Cmd_CommandAdd( pAbc, "Synthesis",    "rr",            Abc_CommandRr,               1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "cascade",       Abc_CommandCascade,          1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "lutcasdec",     Abc_CommandLutCasDec,        1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "lutcas",        Abc_CommandLutCas,           1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "bseval",        Abc_CommandBsEval,           0 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "extract",       Abc_CommandExtract,          1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "varmin",        Abc_CommandVarMin,           0 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "faultclasses",  Abc_CommandFaultClasses,     0 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "exact",         Abc_CommandExact,            1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "orchestrate",  Abc_CommandOrchestrate,     1 );
    Cmd_CommandAdd( pAbc, "Synthesis",    "aigaug",       Abc_CommandAIGAugmentation,     1 );
 
    Cmd_CommandAdd( pAbc, "Exact synthesis", "bms_start",  Abc_CommandBmsStart,         0 );
    Cmd_CommandAdd( pAbc, "Exact synthesis", "bms_stop",   Abc_CommandBmsStop,          0 );
    Cmd_CommandAdd( pAbc, "Exact synthesis", "bms_ps",     Abc_CommandBmsPs,            0 );
    Cmd_CommandAdd( pAbc, "Exact synthesis", "majexact",   Abc_CommandMajExact,         0 );
    Cmd_CommandAdd( pAbc, "Exact synthesis", "twoexact",   Abc_CommandTwoExact,         0 );
    Cmd_CommandAdd( pAbc, "Exact synthesis", "lutexact",   Abc_CommandLutExact,         0 );
    Cmd_CommandAdd( pAbc, "Exact synthesis", "allexact",   Abc_CommandAllExact,         0 );
    Cmd_CommandAdd( pAbc, "Exact synthesis", "testexact",  Abc_CommandTestExact,        0 );
    Cmd_CommandAdd( pAbc, "Exact synthesis", "majgen",     Abc_CommandMajGen,           0 );
 
    Cmd_CommandAdd( pAbc, "Various",      "logic",         Abc_CommandLogic,            1 );
    Cmd_CommandAdd( pAbc, "Various",      "comb",          Abc_CommandComb,             1 );
    Cmd_CommandAdd( pAbc, "Various",      "miter",         Abc_CommandMiter,            1 );
    Cmd_CommandAdd( pAbc, "Various",      "miter2",        Abc_CommandMiter2,           1 );
    Cmd_CommandAdd( pAbc, "Various",      "demiter",       Abc_CommandDemiter,          1 );
    Cmd_CommandAdd( pAbc, "Various",      "orpos",         Abc_CommandOrPos,            1 );
    Cmd_CommandAdd( pAbc, "Various",      "andpos",        Abc_CommandAndPos,           1 );
    Cmd_CommandAdd( pAbc, "Various",      "zeropo",        Abc_CommandZeroPo,           1 );
    Cmd_CommandAdd( pAbc, "Various",      "swappos",       Abc_CommandSwapPos,          1 );
    Cmd_CommandAdd( pAbc, "Various",      "removepo",      Abc_CommandRemovePo,         1 );
    Cmd_CommandAdd( pAbc, "Various",      "dropsat",       Abc_CommandDropSat,          1 );
    Cmd_CommandAdd( pAbc, "Various",      "addpi",         Abc_CommandAddPi,            1 );
    Cmd_CommandAdd( pAbc, "Various",      "addflop",       Abc_CommandAddFlop,          1 );
    Cmd_CommandAdd( pAbc, "Various",      "append",        Abc_CommandAppend,           1 );
    Cmd_CommandAdd( pAbc, "Various",      "putontop",      Abc_CommandPutOnTop,         1 );
    Cmd_CommandAdd( pAbc, "Various",      "frames",        Abc_CommandFrames,           1 );
    Cmd_CommandAdd( pAbc, "Various",      "dframes",       Abc_CommandDFrames,          1 );
    Cmd_CommandAdd( pAbc, "Various",      "sop",           Abc_CommandSop,              0 );
    Cmd_CommandAdd( pAbc, "Various",      "bdd",           Abc_CommandBdd,              0 );
    Cmd_CommandAdd( pAbc, "Various",      "aig",           Abc_CommandAig,              0 );
    Cmd_CommandAdd( pAbc, "Various",      "reorder",       Abc_CommandReorder,          0 );
    Cmd_CommandAdd( pAbc, "Various",      "bidec",         Abc_CommandBidec,            1 );
    Cmd_CommandAdd( pAbc, "Various",      "order",         Abc_CommandOrder,            0 );
    Cmd_CommandAdd( pAbc, "Various",      "muxes",         Abc_CommandMuxes,            1 );
    Cmd_CommandAdd( pAbc, "Various",      "cubes",         Abc_CommandCubes,            1 );
    Cmd_CommandAdd( pAbc, "Various",      "expand",        Abc_CommandExpand,           1 );
    Cmd_CommandAdd( pAbc, "Various",      "splitsop",      Abc_CommandSplitSop,         1 );
    Cmd_CommandAdd( pAbc, "Various",      "ext_seq_dcs",   Abc_CommandExtSeqDcs,        0 );
    Cmd_CommandAdd( pAbc, "Various",      "reach",         Abc_CommandReach,            0 );
    Cmd_CommandAdd( pAbc, "Various",      "cone",          Abc_CommandCone,             1 );
    Cmd_CommandAdd( pAbc, "Various",      "node",          Abc_CommandNode,             1 );
    Cmd_CommandAdd( pAbc, "Various",      "range",         Abc_CommandRange,            1 );
    Cmd_CommandAdd( pAbc, "Various",      "cof",           Abc_CommandCof,              1 );
    Cmd_CommandAdd( pAbc, "Various",      "topmost",       Abc_CommandTopmost,          1 );
    Cmd_CommandAdd( pAbc, "Various",      "bottommost",    Abc_CommandBottommost,       1 );
    Cmd_CommandAdd( pAbc, "Various",      "topand",        Abc_CommandTopAnd,           1 );
    Cmd_CommandAdd( pAbc, "Various",      "trim",          Abc_CommandTrim,             1 );
    Cmd_CommandAdd( pAbc, "Various",      "short_names",   Abc_CommandShortNames,       0 );
    Cmd_CommandAdd( pAbc, "Various",      "move_names",    Abc_CommandMoveNames,        0 );
    Cmd_CommandAdd( pAbc, "Various",      "exdc_free",     Abc_CommandExdcFree,         1 );
    Cmd_CommandAdd( pAbc, "Various",      "exdc_get",      Abc_CommandExdcGet,          1 );
    Cmd_CommandAdd( pAbc, "Various",      "exdc_set",      Abc_CommandExdcSet,          1 );
    Cmd_CommandAdd( pAbc, "Various",      "care_set",      Abc_CommandCareSet,          1 );
    Cmd_CommandAdd( pAbc, "Various",      "cut",           Abc_CommandCut,              0 );
    Cmd_CommandAdd( pAbc, "Various",      "espresso",      Abc_CommandEspresso,         1 );
    Cmd_CommandAdd( pAbc, "Various",      "gen",           Abc_CommandGen,              0 );
    Cmd_CommandAdd( pAbc, "Various",      "gentf",         Abc_CommandGenTF,            0 );
    Cmd_CommandAdd( pAbc, "Various",      "genat",         Abc_CommandGenAT,            0 );
    Cmd_CommandAdd( pAbc, "Various",      "genfsm",        Abc_CommandGenFsm,           0 );
    Cmd_CommandAdd( pAbc, "Various",      "cover",         Abc_CommandCover,            1 );
    Cmd_CommandAdd( pAbc, "Various",      "double",        Abc_CommandDouble,           1 );
    Cmd_CommandAdd( pAbc, "Various",      "inter",         Abc_CommandInter,            1 );
    Cmd_CommandAdd( pAbc, "Various",      "bb2wb",         Abc_CommandBb2Wb,            0 );
    Cmd_CommandAdd( pAbc, "Various",      "outdec",        Abc_CommandOutdec,           1 );
    Cmd_CommandAdd( pAbc, "Various",      "nodedup",       Abc_CommandNodeDup,          1 );
    Cmd_CommandAdd( pAbc, "Various",      "wrap",          Abc_CommandWrap,             0 );
    Cmd_CommandAdd( pAbc, "Various",      "testcolor",     Abc_CommandTestColor,        0 );
    Cmd_CommandAdd( pAbc, "Various",      "test",          Abc_CommandTest,             0 );
//    Cmd_CommandAdd( pAbc, "Various",      "qbf_solve",     Abc_CommandTest,               0 );
 
    Cmd_CommandAdd( pAbc, "Various",      "qvar",          Abc_CommandQuaVar,           1 );
    Cmd_CommandAdd( pAbc, "Various",      "qrel",          Abc_CommandQuaRel,           1 );
    Cmd_CommandAdd( pAbc, "Various",      "qreach",        Abc_CommandQuaReach,         1 );
    Cmd_CommandAdd( pAbc, "Various",      "senseinput",    Abc_CommandSenseInput,       1 );
    Cmd_CommandAdd( pAbc, "Various",      "npnload",       Abc_CommandNpnLoad,          0 );
    Cmd_CommandAdd( pAbc, "Various",      "npnsave",       Abc_CommandNpnSave,          0 );
 
    Cmd_CommandAdd( pAbc, "Various",      "send_aig",      Abc_CommandSendAig,          0 );
    Cmd_CommandAdd( pAbc, "Various",      "send_status",   Abc_CommandSendStatus,       0 );
 
    Cmd_CommandAdd( pAbc, "Various",      "backup",        Abc_CommandBackup,           0 );
    Cmd_CommandAdd( pAbc, "Various",      "restore",       Abc_CommandRestore,          0 );
 
    Cmd_CommandAdd( pAbc, "Various",      "minisat",       Abc_CommandMinisat,          0 );
    Cmd_CommandAdd( pAbc, "Various",      "minisimp",      Abc_CommandMinisimp,         0 );
 
    Cmd_CommandAdd( pAbc, "New AIG",      "istrash",       Abc_CommandIStrash,          1 );
    Cmd_CommandAdd( pAbc, "New AIG",      "icut",          Abc_CommandICut,             0 );
    Cmd_CommandAdd( pAbc, "New AIG",      "irw",           Abc_CommandIRewrite,         1 );
    Cmd_CommandAdd( pAbc, "New AIG",      "drw",           Abc_CommandDRewrite,         1 );
    Cmd_CommandAdd( pAbc, "New AIG",      "drf",           Abc_CommandDRefactor,        1 );
    Cmd_CommandAdd( pAbc, "New AIG",      "dc2",           Abc_CommandDc2,              1 );
    Cmd_CommandAdd( pAbc, "New AIG",      "dchoice",       Abc_CommandDChoice,          1 );
    Cmd_CommandAdd( pAbc, "New AIG",      "dch",           Abc_CommandDch,              1 );
    Cmd_CommandAdd( pAbc, "New AIG",      "drwsat",        Abc_CommandDrwsat,           1 );
    Cmd_CommandAdd( pAbc, "New AIG",      "irws",          Abc_CommandIRewriteSeq,      1 );
    Cmd_CommandAdd( pAbc, "New AIG",      "iresyn",        Abc_CommandIResyn,           1 );
    Cmd_CommandAdd( pAbc, "New AIG",      "isat",          Abc_CommandISat,             1 );
    Cmd_CommandAdd( pAbc, "New AIG",      "ifraig",        Abc_CommandIFraig,           1 );
    Cmd_CommandAdd( pAbc, "New AIG",      "dfraig",        Abc_CommandDFraig,           1 );
    Cmd_CommandAdd( pAbc, "New AIG",      "csweep",        Abc_CommandCSweep,           1 );
//    Cmd_CommandAdd( pAbc, "New AIG",      "haig",          Abc_CommandHaig,             1 );
    Cmd_CommandAdd( pAbc, "New AIG",      "qbf",           Abc_CommandQbf,              0 );
 
    Cmd_CommandAdd( pAbc, "Fraiging",     "fraig",         Abc_CommandFraig,            1 );
    Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_trust",   Abc_CommandFraigTrust,       1 );
    Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_store",   Abc_CommandFraigStore,       0 );
    Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_restore", Abc_CommandFraigRestore,     1 );
    Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_clean",   Abc_CommandFraigClean,       0 );
    Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_sweep",   Abc_CommandFraigSweep,       1 );
    Cmd_CommandAdd( pAbc, "Fraiging",     "dress",         Abc_CommandFraigDress,       1 );
    Cmd_CommandAdd( pAbc, "Fraiging",     "dump_equiv",    Abc_CommandDumpEquiv,        0 );
 
    Cmd_CommandAdd( pAbc, "Choicing",     "rec_start3",    Abc_CommandRecStart3,        0 );
    Cmd_CommandAdd( pAbc, "Choicing",     "rec_stop3",     Abc_CommandRecStop3,         0 );
    Cmd_CommandAdd( pAbc, "Choicing",     "rec_ps3",       Abc_CommandRecPs3,           0 );
    Cmd_CommandAdd( pAbc, "Choicing",     "rec_add3",      Abc_CommandRecAdd3,          0 );
    Cmd_CommandAdd( pAbc, "Choicing",     "rec_dump3",     Abc_CommandRecDump3,         0 );
    Cmd_CommandAdd( pAbc, "Choicing",     "rec_merge3",    Abc_CommandRecMerge3,        0 );
 
    Cmd_CommandAdd( pAbc, "SC mapping",   "map",           Abc_CommandMap,              1 );
    Cmd_CommandAdd( pAbc, "SC mapping",   "amap",          Abc_CommandAmap,             1 );
    Cmd_CommandAdd( pAbc, "SC mapping",   "phase_map",     Abc_CommandPhaseMap,         1 );
    Cmd_CommandAdd( pAbc, "SC mapping",   "stochmap",      Abc_CommandStochMap,         1 );
    Cmd_CommandAdd( pAbc, "SC mapping",   "unmap",         Abc_CommandUnmap,            1 );
    Cmd_CommandAdd( pAbc, "SC mapping",   "attach",        Abc_CommandAttach,           1 );
    Cmd_CommandAdd( pAbc, "SC mapping",   "superc",        Abc_CommandSuperChoice,      1 );
    Cmd_CommandAdd( pAbc, "SC mapping",   "supercl",       Abc_CommandSuperChoiceLut,   1 );
    Cmd_CommandAdd( pAbc, "SC mapping",   "timescale",     Abc_CommandTimeScale,        0 );
    Cmd_CommandAdd( pAbc, "SC mapping",   "rewire",        Abc_CommandRewire,           1 );
 
//    Cmd_CommandAdd( pAbc, "FPGA mapping", "fpga",          Abc_CommandFpga,             1 );
//    Cmd_CommandAdd( pAbc, "FPGA mapping", "ffpga",         Abc_CommandFpgaFast,         1 );
    Cmd_CommandAdd( pAbc, "FPGA mapping", "if",            Abc_CommandIf,               1 );
    Cmd_CommandAdd( pAbc, "FPGA mapping", "ifif",          Abc_CommandIfif,             1 );
 
    Cmd_CommandAdd( pAbc, "DSD manager",  "dsd_save",      Abc_CommandDsdSave,          0 );
    Cmd_CommandAdd( pAbc, "DSD manager",  "dsd_load",      Abc_CommandDsdLoad,          0 );
    Cmd_CommandAdd( pAbc, "DSD manager",  "dsd_free",      Abc_CommandDsdFree,          0 );
    Cmd_CommandAdd( pAbc, "DSD manager",  "dsd_ps",        Abc_CommandDsdPs,            0 );
    Cmd_CommandAdd( pAbc, "DSD manager",  "dsd_match",     Abc_CommandDsdMatch,         0 );
    Cmd_CommandAdd( pAbc, "DSD manager",  "dsd_merge",     Abc_CommandDsdMerge,         0 );
    Cmd_CommandAdd( pAbc, "DSD manager",  "dsd_filter",    Abc_CommandDsdFilter,        0 );
 
//    Cmd_CommandAdd( pAbc, "Sequential",   "scut",          Abc_CommandScut,             0 );
    Cmd_CommandAdd( pAbc, "Sequential",   "init",          Abc_CommandInit,             1 );
    Cmd_CommandAdd( pAbc, "Sequential",   "zero",          Abc_CommandZero,             1 );
    Cmd_CommandAdd( pAbc, "Sequential",   "undc",          Abc_CommandUndc,             1 );
    Cmd_CommandAdd( pAbc, "Sequential",   "onehot",        Abc_CommandOneHot,           1 );
    Cmd_CommandAdd( pAbc, "Sequential",   "pipe",          Abc_CommandPipe,             1 );
    Cmd_CommandAdd( pAbc, "Sequential",   "retime",        Abc_CommandRetime,           1 );
    Cmd_CommandAdd( pAbc, "Sequential",   "dretime",       Abc_CommandDRetime,          1 );
    Cmd_CommandAdd( pAbc, "Sequential",   "fretime",       Abc_CommandFlowRetime,       1 );
    Cmd_CommandAdd( pAbc, "Sequential",   "cretime",       Abc_CommandCRetime,          1 );
//    Cmd_CommandAdd( pAbc, "Sequential",   "sfpga",         Abc_CommandSeqFpga,          1 );
//    Cmd_CommandAdd( pAbc, "Sequential",   "smap",          Abc_CommandSeqMap,           1 );
    Cmd_CommandAdd( pAbc, "Sequential",   "ssweep",        Abc_CommandSeqSweep,         1 );
    Cmd_CommandAdd( pAbc, "Sequential",   "scorr",         Abc_CommandSeqSweep2,        1 );
    Cmd_CommandAdd( pAbc, "Sequential",   "testssw",       Abc_CommandTestSeqSweep,     0 );
    Cmd_CommandAdd( pAbc, "Sequential",   "testscorr",     Abc_CommandTestScorr,        0 );
    Cmd_CommandAdd( pAbc, "Sequential",   "lcorr",         Abc_CommandLcorr,            1 );
    Cmd_CommandAdd( pAbc, "Sequential",   "scleanup",      Abc_CommandSeqCleanup,       1 );
    Cmd_CommandAdd( pAbc, "Sequential",   "cycle",         Abc_CommandCycle,            1 );
    Cmd_CommandAdd( pAbc, "Sequential",   "xsim",          Abc_CommandXsim,             0 );
    Cmd_CommandAdd( pAbc, "Sequential",   "sim",           Abc_CommandSim,              0 );
    Cmd_CommandAdd( pAbc, "Sequential",   "sim3",          Abc_CommandSim3,             0 );
    Cmd_CommandAdd( pAbc, "Sequential",   "phase",         Abc_CommandDarPhase,         1 );
    Cmd_CommandAdd( pAbc, "Sequential",   "synch",         Abc_CommandSynch,            1 );
    Cmd_CommandAdd( pAbc, "Sequential",   "clockgate",     Abc_CommandClockGate,        1 );
    Cmd_CommandAdd( pAbc, "Sequential",   "extwin",        Abc_CommandExtWin,           1 );
    Cmd_CommandAdd( pAbc, "Sequential",   "inswin",        Abc_CommandInsWin,           1 );
    Cmd_CommandAdd( pAbc, "Sequential",   "symfun",        Abc_CommandSymFun,           0 );
    Cmd_CommandAdd( pAbc, "Sequential",   "atmap",         Abc_CommandATMap,            0 );
    Cmd_CommandAdd( pAbc, "Sequential",   "permute",       Abc_CommandPermute,          1 );
    Cmd_CommandAdd( pAbc, "Sequential",   "unpermute",     Abc_CommandUnpermute,        1 );
    Cmd_CommandAdd( pAbc, "Sequential",   "cubeenum",      Abc_CommandCubeEnum,         0 );
    Cmd_CommandAdd( pAbc, "Sequential",   "pathenum",      Abc_CommandPathEnum,         0 );
    Cmd_CommandAdd( pAbc, "Sequential",   "funenum",       Abc_CommandFunEnum,          0 );
 
    Cmd_CommandAdd( pAbc, "Verification", "cec",           Abc_CommandCec,              0 );
    Cmd_CommandAdd( pAbc, "Verification", "dcec",          Abc_CommandDCec,             0 );
    Cmd_CommandAdd( pAbc, "Verification", "dsec",          Abc_CommandDSec,             0 );
    Cmd_CommandAdd( pAbc, "Verification", "dprove",        Abc_CommandDProve,           0 );
    Cmd_CommandAdd( pAbc, "Verification", "absec",         Abc_CommandAbSec,            0 );
    Cmd_CommandAdd( pAbc, "Verification", "simsec",        Abc_CommandSimSec,           0 );
    Cmd_CommandAdd( pAbc, "Verification", "match",         Abc_CommandMatch,            0 );
    Cmd_CommandAdd( pAbc, "Verification", "sat",           Abc_CommandSat,              0 );
    Cmd_CommandAdd( pAbc, "Verification", "dsat",          Abc_CommandDSat,             0 );
    Cmd_CommandAdd( pAbc, "Verification", "xsat",          Abc_CommandXSat,             0 );
    Cmd_CommandAdd( pAbc, "Verification", "satoko",        Abc_CommandSatoko,           0 );
    Cmd_CommandAdd( pAbc, "Verification", "&satoko",       Abc_CommandAbc9Satoko,       0 );
    Cmd_CommandAdd( pAbc, "Verification", "&sat3",         Abc_CommandAbc9Sat3,         0 );
    Cmd_CommandAdd( pAbc, "Verification", "&kissat",       Abc_CommandAbc9Kissat,       0 );
    Cmd_CommandAdd( pAbc, "Verification", "psat",          Abc_CommandPSat,             0 );
    Cmd_CommandAdd( pAbc, "Verification", "prove",         Abc_CommandProve,            1 );
    Cmd_CommandAdd( pAbc, "Verification", "iprove",        Abc_CommandIProve,           1 );
    Cmd_CommandAdd( pAbc, "Verification", "debug",         Abc_CommandDebug,            0 );
    Cmd_CommandAdd( pAbc, "Verification", "eco",           Abc_CommandEco,              0 );
    Cmd_CommandAdd( pAbc, "Verification", "bmc",           Abc_CommandBmc,              0 );
    Cmd_CommandAdd( pAbc, "Verification", "bmc2",          Abc_CommandBmc2,             0 );
    Cmd_CommandAdd( pAbc, "Verification", "bmc3",          Abc_CommandBmc3,             1 );
    Cmd_CommandAdd( pAbc, "Verification", "int",           Abc_CommandBmcInter,         1 );
    Cmd_CommandAdd( pAbc, "Verification", "indcut",        Abc_CommandIndcut,           0 );
    Cmd_CommandAdd( pAbc, "Verification", "enlarge",       Abc_CommandEnlarge,          1 );
    Cmd_CommandAdd( pAbc, "Verification", "tempor",        Abc_CommandTempor,           1 );
    Cmd_CommandAdd( pAbc, "Verification", "ind",           Abc_CommandInduction,        0 );
    Cmd_CommandAdd( pAbc, "Verification", "constr",        Abc_CommandConstr,           0 );
    Cmd_CommandAdd( pAbc, "Verification", "unfold",        Abc_CommandUnfold,           1 );
    Cmd_CommandAdd( pAbc, "Verification", "fold",          Abc_CommandFold,             1 );
    Cmd_CommandAdd( pAbc, "Verification", "unfold2",       Abc_CommandUnfold2,          1 );    // jlong
    Cmd_CommandAdd( pAbc, "Verification", "fold2",         Abc_CommandFold2,            1 );    // jlong
    Cmd_CommandAdd( pAbc, "Verification", "bm",            Abc_CommandBm,               1 );
    Cmd_CommandAdd( pAbc, "Verification", "bm2",           Abc_CommandBm2,              1 );
    Cmd_CommandAdd( pAbc, "Verification", "saucy3",        Abc_CommandSaucy,            1 );
    Cmd_CommandAdd( pAbc, "Verification", "testcex",       Abc_CommandTestCex,          0 );
    Cmd_CommandAdd( pAbc, "Verification", "pdr",           Abc_CommandPdr,              0 );
#ifdef ABC_USE_CUDD
    Cmd_CommandAdd( pAbc, "Verification", "reconcile",     Abc_CommandReconcile,        1 );
#endif
    Cmd_CommandAdd( pAbc, "Verification", "cexsave",       Abc_CommandCexSave,          0 );
    Cmd_CommandAdd( pAbc, "Verification", "cexload",       Abc_CommandCexLoad,          0 );
    Cmd_CommandAdd( pAbc, "Verification", "cexcut",        Abc_CommandCexCut,           0 );
    Cmd_CommandAdd( pAbc, "Verification", "cexmerge",      Abc_CommandCexMerge,         0 );
//    Cmd_CommandAdd( pAbc, "Verification", "cexmin",        Abc_CommandCexMin,           0 );
    Cmd_CommandAdd( pAbc, "Verification", "dualrail",      Abc_CommandDualRail,         1 );
    Cmd_CommandAdd( pAbc, "Verification", "blockpo",       Abc_CommandBlockPo,          1 );
    Cmd_CommandAdd( pAbc, "Verification", "iso",           Abc_CommandIso,              1 );
 
    Cmd_CommandAdd( pAbc, "Various",      "save",          Abc_CommandAbcSave,          0 );
    Cmd_CommandAdd( pAbc, "Various",      "load",          Abc_CommandAbcLoad,          0 );
 
    Cmd_CommandAdd( pAbc, "ABC9",         "&get",          Abc_CommandAbc9Get,          0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&put",          Abc_CommandAbc9Put,          0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&move_names",   Abc_CommandAbc9MoveNames,    0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&save",         Abc_CommandAbc9Save,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&save2",        Abc_CommandAbc9Save2,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&saveaig",      Abc_CommandAbc9SaveAig,      0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&load",         Abc_CommandAbc9Load,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&load2",        Abc_CommandAbc9Load2,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&loadaig",      Abc_CommandAbc9LoadAig,      0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&r",            Abc_CommandAbc9Read,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&read",         Abc_CommandAbc9Read,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&read_blif",    Abc_CommandAbc9ReadBlif,     0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&read_cblif",   Abc_CommandAbc9ReadCBlif,    0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&read_stg",     Abc_CommandAbc9ReadStg,      0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&read_ver",     Abc_CommandAbc9ReadVer,      0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&write_ver",    Abc_CommandAbc9WriteVer,     0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&w",            Abc_CommandAbc9Write,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&write",        Abc_CommandAbc9Write,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&wlut",         Abc_CommandAbc9WriteLut,     0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&ps",           Abc_CommandAbc9Ps,           0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&pfan",         Abc_CommandAbc9PFan,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&pms",          Abc_CommandAbc9Pms,          0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&psig",         Abc_CommandAbc9PSig,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&status",       Abc_CommandAbc9Status,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&profile",      Abc_CommandAbc9MuxProfile,   0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&muxpos",       Abc_CommandAbc9MuxPos,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&muxstr",       Abc_CommandAbc9MuxStr,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&muxdec",       Abc_CommandAbc9MuxDec,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&print_truth",  Abc_CommandAbc9PrintTruth,   0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&unate",        Abc_CommandAbc9Unate,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&rex2gia",      Abc_CommandAbc9Rex2Gia,      0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&rexwalk",      Abc_CommandAbc9RexWalk,      0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&show",         Abc_CommandAbc9Show,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&setregnum",    Abc_CommandAbc9SetRegNum,    0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&st",           Abc_CommandAbc9Strash,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&topand",       Abc_CommandAbc9Topand,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&add1hot",      Abc_CommandAbc9Add1Hot,      0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&cof",          Abc_CommandAbc9Cof,          0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&cofs",         Abc_CommandAbc9Cofs,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&trim",         Abc_CommandAbc9Trim,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&dfs",          Abc_CommandAbc9Dfs,          0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&sim",          Abc_CommandAbc9Sim,          0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&sim2",         Abc_CommandAbc9Sim2,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&sim3",         Abc_CommandAbc9Sim3,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&mlgen",        Abc_CommandAbc9MLGen,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&mltest",       Abc_CommandAbc9MLTest,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&iwls21test",   Abc_CommandAbc9Iwls21Test,   0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&sim_read",     Abc_CommandAbc9ReadSim,      0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&sim_write",    Abc_CommandAbc9WriteSim,     0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&sim_print",    Abc_CommandAbc9PrintSim,     0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&sim_gen",      Abc_CommandAbc9GenSim,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&simrsb",       Abc_CommandAbc9SimRsb,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&resim",        Abc_CommandAbc9Resim,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&speci",        Abc_CommandAbc9SpecI,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&equiv",        Abc_CommandAbc9Equiv,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&equiv2",       Abc_CommandAbc9Equiv2,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&equiv3",       Abc_CommandAbc9Equiv3,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&semi",         Abc_CommandAbc9Semi,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&times",        Abc_CommandAbc9Times,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&frames",       Abc_CommandAbc9Frames,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&retime",       Abc_CommandAbc9Retime,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&enable",       Abc_CommandAbc9Enable,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&dc2",          Abc_CommandAbc9Dc2,          0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&dsd",          Abc_CommandAbc9Dsd,          0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&bidec",        Abc_CommandAbc9Bidec,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&shrink",       Abc_CommandAbc9Shrink,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&fx",           Abc_CommandAbc9Fx,           0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&extract",      Abc_CommandAbc9Extract,      0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&b",            Abc_CommandAbc9Balance,      0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&blut",         Abc_CommandAbc9BalanceLut,   0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&resub",        Abc_CommandAbc9Resub,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&reshape",      Abc_CommandAbc9Reshape,      0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&syn2",         Abc_CommandAbc9Syn2,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&syn3",         Abc_CommandAbc9Syn3,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&syn4",         Abc_CommandAbc9Syn4,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&synch2",       Abc_CommandAbc9Synch2,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&false",        Abc_CommandAbc9False,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&miter",        Abc_CommandAbc9Miter,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&miter2",       Abc_CommandAbc9Miter2,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&append",       Abc_CommandAbc9Append,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&scl",          Abc_CommandAbc9Scl,          0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&lcorr",        Abc_CommandAbc9Lcorr,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&scorr",        Abc_CommandAbc9Scorr,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&choice",       Abc_CommandAbc9Choice,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&sat",          Abc_CommandAbc9Sat,          0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&satenum",      Abc_CommandAbc9SatEnum,      0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&adv_sim_gen",      Abc_CommandAbc9AdvGenSim,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&fraig",        Abc_CommandAbc9Fraig,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&cfraig",       Abc_CommandAbc9CFraig,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&srm",          Abc_CommandAbc9Srm,          0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&srm2",         Abc_CommandAbc9Srm2,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&filter",       Abc_CommandAbc9Filter,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&reduce",       Abc_CommandAbc9Reduce,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&equiv_mark",   Abc_CommandAbc9EquivMark,    0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&equiv_filter", Abc_CommandAbc9EquivFilter,  0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&cec",          Abc_CommandAbc9Cec,          0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&icec",         Abc_CommandAbc9ICec,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&verify",       Abc_CommandAbc9Verify,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&sweep",        Abc_CommandAbc9Sweep,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&force",        Abc_CommandAbc9Force,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&embed",        Abc_CommandAbc9Embed,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&sopb",         Abc_CommandAbc9Sopb,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&dsdb",         Abc_CommandAbc9Dsdb,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&flow",         Abc_CommandAbc9Flow,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&flow2",        Abc_CommandAbc9Flow2,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&flow3",        Abc_CommandAbc9Flow3,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&if",           Abc_CommandAbc9If,           0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&iff",          Abc_CommandAbc9Iff,          0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&iiff",         Abc_CommandAbc9Iiff,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&if2",          Abc_CommandAbc9If2,          0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&sif",          Abc_CommandAbc9Sif,          0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&jf",           Abc_CommandAbc9Jf,           0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&kf",           Abc_CommandAbc9Kf,           0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&lf",           Abc_CommandAbc9Lf,           0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&mf",           Abc_CommandAbc9Mf,           0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&nf",           Abc_CommandAbc9Nf,           0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&of",           Abc_CommandAbc9Of,           0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&simap",        Abc_CommandAbc9Simap,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&exmap",        Abc_CommandAbc9Exmap,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&pack",         Abc_CommandAbc9Pack,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&edge",         Abc_CommandAbc9Edge,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&satlut",       Abc_CommandAbc9SatLut,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&lnetread",     Abc_CommandAbc9LNetRead,     0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&lnetsim",      Abc_CommandAbc9LNetSim,      0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&lneteval",     Abc_CommandAbc9LNetEval,     0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&lnetopt",      Abc_CommandAbc9LNetOpt,      0 );
//#ifndef _WIN32
    Cmd_CommandAdd( pAbc, "ABC9",         "&ttopt",        Abc_CommandAbc9Ttopt,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&transduction", Abc_CommandAbc9Transduction, 0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&transtoch"   , Abc_CommandAbc9TranStoch,    0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&rrr",          Abc_CommandAbc9Rrr,          0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&rewire"      , Abc_CommandAbc9Rewire,       0 );
//#endif
    Cmd_CommandAdd( pAbc, "ABC9",         "&lnetmap",      Abc_CommandAbc9LNetMap,      0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&unmap",        Abc_CommandAbc9Unmap,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&struct",       Abc_CommandAbc9Struct,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&trace",        Abc_CommandAbc9Trace,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&speedup",      Abc_CommandAbc9Speedup,      0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&era",          Abc_CommandAbc9Era,          0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&dch",          Abc_CommandAbc9Dch,          0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&rpm",          Abc_CommandAbc9Rpm,          0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&back_reach",   Abc_CommandAbc9BackReach,    0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&posplit",      Abc_CommandAbc9Posplit,      0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&permute",      Abc_CommandAbc9Permute,      0 );
#ifdef ABC_USE_CUDD
    Cmd_CommandAdd( pAbc, "ABC9",         "&reachm",       Abc_CommandAbc9ReachM,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&reachp",       Abc_CommandAbc9ReachP,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&reachn",       Abc_CommandAbc9ReachN,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&reachy",       Abc_CommandAbc9ReachY,       0 );
#endif
    Cmd_CommandAdd( pAbc, "ABC9",         "&undo",         Abc_CommandAbc9Undo,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&mesh",         Abc_CommandAbc9Mesh,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&iso",          Abc_CommandAbc9Iso,          0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&isonpn",       Abc_CommandAbc9IsoNpn,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&isost",        Abc_CommandAbc9IsoSt,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&store",        Abc_CommandAbc9Store,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&compare",      Abc_CommandAbc9Compare,      0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&reveng",       Abc_CommandAbc9RevEng,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&uif",          Abc_CommandAbc9Uif,          0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&cexinfo",      Abc_CommandAbc9CexInfo,      0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&cycle",        Abc_CommandAbc9Cycle,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&cone",         Abc_CommandAbc9Cone,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&slice",        Abc_CommandAbc9Slice,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&popart",       Abc_CommandAbc9PoPart,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&gprove",       Abc_CommandAbc9GroupProve,   0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&mprove",       Abc_CommandAbc9MultiProve,   0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&splitprove",   Abc_CommandAbc9SplitProve,   0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&sprove",       Abc_CommandAbc9SProve,       0 );    
    Cmd_CommandAdd( pAbc, "ABC9",         "&splitsat",     Abc_CommandAbc9SplitSat,     0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&bmc",          Abc_CommandAbc9Bmc,          0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&bmcs",         Abc_CommandAbc9SBmc,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&chainbmc",     Abc_CommandAbc9ChainBmc,     0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&bcore",        Abc_CommandAbc9BCore,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&icheck",       Abc_CommandAbc9ICheck,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&sattest",      Abc_CommandAbc9SatTest,      0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&fftest",       Abc_CommandAbc9FFTest,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&qbf",          Abc_CommandAbc9Qbf,          0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&qvar",         Abc_CommandAbc9QVar,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&genqbf",       Abc_CommandAbc9GenQbf,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&homoqbf",      Abc_CommandAbc9HomoQbf,      0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&satfx",        Abc_CommandAbc9SatFx,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&satclp",       Abc_CommandAbc9SatClp,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&inse",         Abc_CommandAbc9Inse,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&maxi",         Abc_CommandAbc9Maxi,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&bmci",         Abc_CommandAbc9Bmci,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&poxsim",       Abc_CommandAbc9PoXsim,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&demiter",      Abc_CommandAbc9Demiter,      0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&fadds",        Abc_CommandAbc9Fadds,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&atree",        Abc_CommandAbc9ATree,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&polyn",        Abc_CommandAbc9Polyn,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&acec",         Abc_CommandAbc9Acec,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&anorm",        Abc_CommandAbc9Anorm,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&decla",        Abc_CommandAbc9Decla,        0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&esop",         Abc_CommandAbc9Esop,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&exorcism",     Abc_CommandAbc9Exorcism,     0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&mfs",          Abc_CommandAbc9Mfs,          0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&mfsd",         Abc_CommandAbc9Mfsd,         0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&deepsyn",      Abc_CommandAbc9DeepSyn,      0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&randsyn",      Abc_CommandAbc9RandSyn,      0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&satsyn",       Abc_CommandAbc9SatSyn,       0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&stochsyn",     Abc_CommandAbc9StochSyn,     0 );
//    Cmd_CommandAdd( pAbc, "ABC9",         "&popart2",      Abc_CommandAbc9PoPart2,      0 );
//    Cmd_CommandAdd( pAbc, "ABC9",         "&cexcut",       Abc_CommandAbc9CexCut,       0 );
//    Cmd_CommandAdd( pAbc, "ABC9",         "&cexmerge",     Abc_CommandAbc9CexMerge,     0 );
//    Cmd_CommandAdd( pAbc, "ABC9",         "&cexmin",       Abc_CommandAbc9CexMin,       0 );
 
    Cmd_CommandAdd( pAbc, "Abstraction",  "&abs_create",   Abc_CommandAbc9AbsCreate,    0 );
    Cmd_CommandAdd( pAbc, "Abstraction",  "&abs_derive",   Abc_CommandAbc9AbsDerive,    0 );
    Cmd_CommandAdd( pAbc, "Abstraction",  "&abs_refine",   Abc_CommandAbc9AbsRefine,    0 );
    Cmd_CommandAdd( pAbc, "Abstraction",  "&gla_derive",   Abc_CommandAbc9GlaDerive,    0 );
    Cmd_CommandAdd( pAbc, "Abstraction",  "&gla_refine",   Abc_CommandAbc9GlaRefine,    0 );
    Cmd_CommandAdd( pAbc, "Abstraction",  "&gla_shrink",   Abc_CommandAbc9GlaShrink,    0 );
    Cmd_CommandAdd( pAbc, "Abstraction",  "&gla",          Abc_CommandAbc9Gla,          0 );
    Cmd_CommandAdd( pAbc, "Abstraction",  "&vta",          Abc_CommandAbc9Vta,          0 );
    Cmd_CommandAdd( pAbc, "Abstraction",  "&vta_gla",      Abc_CommandAbc9Vta2Gla,      0 );
    Cmd_CommandAdd( pAbc, "Abstraction",  "&gla_vta",      Abc_CommandAbc9Gla2Vta,      0 );
    Cmd_CommandAdd( pAbc, "Abstraction",  "&fla_gla",      Abc_CommandAbc9Fla2Gla,      0 );
    Cmd_CommandAdd( pAbc, "Abstraction",  "&gla_fla",      Abc_CommandAbc9Gla2Fla,      0 );
 
    Cmd_CommandAdd( pAbc, "Liveness",     "l2s",           Abc_CommandAbcLivenessToSafety,        0 );
    Cmd_CommandAdd( pAbc, "Liveness",     "l2ssim",        Abc_CommandAbcLivenessToSafetySim,     0 );
    Cmd_CommandAdd( pAbc, "Liveness",     "l3s",           Abc_CommandAbcLivenessToSafetyWithLTL, 0 );
    Cmd_CommandAdd( pAbc, "Liveness",     "kcs",           Abc_CommandCS_kLiveness,               0 );
    Cmd_CommandAdd( pAbc, "Liveness",     "nck",           Abc_CommandNChooseK,                   0 );
 
    Cmd_CommandAdd( pAbc, "ABC9",         "&gen",          Abc_CommandAbc9Gen,                    0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&cfs",          Abc_CommandAbc9Cfs,                    0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&prodadd",      Abc_CommandAbc9ProdAdd,                0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&addflop",      Abc_CommandAbc9AddFlop,                0 );    
    Cmd_CommandAdd( pAbc, "ABC9",         "&bmiter",       Abc_CommandAbc9BMiter,                 0 );    
    Cmd_CommandAdd( pAbc, "ABC9",         "&gen_hie",      Abc_CommandAbc9GenHie,                 0 );    
    Cmd_CommandAdd( pAbc, "ABC9",         "&putontop",     Abc_CommandAbc9PutOnTop,               0 );    
    Cmd_CommandAdd( pAbc, "ABC9",         "&brecover",     Abc_CommandAbc9BRecover,               0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&str_eco",      Abc_CommandAbc9StrEco,                 0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&gencex",       Abc_CommandAbc9GenCex,                 0 );    
    Cmd_CommandAdd( pAbc, "ABC9",         "&odc",          Abc_CommandAbc9Odc,                    0 );    
    Cmd_CommandAdd( pAbc, "ABC9",         "&genrel",       Abc_CommandAbc9GenRel,                 0 );    
    Cmd_CommandAdd( pAbc, "ABC9",         "&genmux",       Abc_CommandAbc9GenMux,                 0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&gencomp",      Abc_CommandAbc9GenComp,                0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&gensorter",    Abc_CommandAbc9GenSorter,              0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&genneuron",    Abc_CommandAbc9GenNeuron,              0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&genadder",     Abc_CommandAbc9GenAdder,               0 );
    Cmd_CommandAdd( pAbc, "ABC9",         "&window",       Abc_CommandAbc9Window,                 0 );    
    Cmd_CommandAdd( pAbc, "ABC9",         "&funabs",       Abc_CommandAbc9FunAbs,                 0 );    
    Cmd_CommandAdd( pAbc, "ABC9",         "&dsdinfo",      Abc_CommandAbc9DsdInfo,                0 );    
    Cmd_CommandAdd( pAbc, "ABC9",         "&funtrace",     Abc_CommandAbc9FunTrace,               0 );    
    Cmd_CommandAdd( pAbc, "ABC9",         "&mulfind",      Abc_CommandAbc9MulFind,                0 );    
    Cmd_CommandAdd( pAbc, "ABC9",         "&andcare",      Abc_CommandAbc9AndCare,                0 );    
    
    Cmd_CommandAdd( pAbc, "ABC9",         "&test",         Abc_CommandAbc9Test,                   0 );
 
    Cmd_CommandAdd( pAbc, "ABC9",         "&eslim",        Abc_CommandAbc9eSLIM,                  0 );
    {
//        extern Mf_ManTruthCount();
//        Mf_ManTruthCount();
    }
 
    {
        extern void Dar_LibStart();
        Dar_LibStart();
    }
    {
//        extern void Dau_DsdTest();
//        Dau_DsdTest();
//        extern void If_ManSatTest();
//        If_ManSatTest();
    }
 
//    if ( Sdm_ManCanRead() )
//        Sdm_ManRead();
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkCollectCiNames()

Vec_Ptr_t * Abc_NtkCollectCiNames ( Abc_Ntk_t * pNtk )

extern

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

Synopsis [Collects CI of the network.]

Description []

SideEffects []

SeeAlso []

Definition at line 1348 of file abcDar.c.

{
    Abc_Obj_t * pObj;
    int i;
    Vec_Ptr_t * vNames;
    vNames = Vec_PtrAlloc( 100 );
    Abc_NtkForEachCi( pNtk, pObj, i )
        Vec_PtrPush( vNames, Extra_UtilStrsav(Abc_ObjName(pObj)) );
    return vNames;
}

Here is the call graph for this function:

Abc_NtkCollectCoNames()

Vec_Ptr_t * Abc_NtkCollectCoNames ( Abc_Ntk_t * pNtk )

extern

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

Synopsis [Collects CO of the network.]

Description []

SideEffects []

SeeAlso []

Definition at line 1370 of file abcDar.c.

{
    Abc_Obj_t * pObj;
    int i;
    Vec_Ptr_t * vNames;
    vNames = Vec_PtrAlloc( 100 );
    Abc_NtkForEachCo( pNtk, pObj, i )
        Vec_PtrPush( vNames, Extra_UtilStrsav(Abc_ObjName(pObj)) );
    return vNames;
}

Here is the call graph for this function:

Abc_NtkFromAigPhase()

Abc_Ntk_t * Abc_NtkFromAigPhase ( Aig_Man_t * pMan )

extern

DECLARATIONS ///.

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

Synopsis [Converts the network from the AIG manager into ABC.]

Description [This procedure should be called after seq sweeping, which changes the number of registers.]

SideEffects []

SeeAlso []

Definition at line 595 of file abcDar.c.

{
    Vec_Ptr_t * vNodes; 
    Abc_Ntk_t * pNtkNew;
    Abc_Obj_t * pObjNew;
    Aig_Obj_t * pObj, * pObjLo, * pObjLi;
    int i; 
    assert( pMan->nAsserts == 0 );
    // perform strashing
    pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
    pNtkNew->nConstrs = pMan->nConstrs;
    pNtkNew->nBarBufs = pMan->nBarBufs;
    // duplicate the name and the spec
//    pNtkNew->pName = Extra_UtilStrsav(pMan->pName);
//    pNtkNew->pSpec = Extra_UtilStrsav(pMan->pSpec);
    Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
    // create PIs
    Aig_ManForEachPiSeq( pMan, pObj, i )
    {
        pObjNew = Abc_NtkCreatePi( pNtkNew );
//        Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjNew), NULL );
        pObj->pData = pObjNew;
    }
    // create POs
    Aig_ManForEachPoSeq( pMan, pObj, i )
    {
        pObjNew = Abc_NtkCreatePo( pNtkNew );
//        Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjNew), NULL );
        pObj->pData = pObjNew;
    }
    assert( Abc_NtkCiNum(pNtkNew) == Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan) );
    assert( Abc_NtkCoNum(pNtkNew) == Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) );
    // create as many latches as there are registers in the manager
    Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i )
    {
        pObjNew = Abc_NtkCreateLatch( pNtkNew );
        pObjLi->pData = Abc_NtkCreateBi( pNtkNew );
        pObjLo->pData = Abc_NtkCreateBo( pNtkNew );
        Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)pObjLi->pData );
        Abc_ObjAddFanin( (Abc_Obj_t *)pObjLo->pData, pObjNew );
        Abc_LatchSetInit0( pObjNew );
//        Abc_ObjAssignName( (Abc_Obj_t *)pObjLi->pData, Abc_ObjName((Abc_Obj_t *)pObjLi->pData), NULL );
//        Abc_ObjAssignName( (Abc_Obj_t *)pObjLo->pData, Abc_ObjName((Abc_Obj_t *)pObjLo->pData), NULL );
    }
    // rebuild the AIG
    vNodes = Aig_ManDfs( pMan, 1 );
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
        if ( Aig_ObjIsBuf(pObj) )
            pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
        else
            pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
    Vec_PtrFree( vNodes );
    // connect the PO nodes
    Aig_ManForEachCo( pMan, pObj, i )
    {
        pObjNew = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
        Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjNew );
    }
 
    Abc_NtkAddDummyPiNames( pNtkNew );
    Abc_NtkAddDummyPoNames( pNtkNew );
    Abc_NtkAddDummyBoxNames( pNtkNew );
 
    // check the resulting AIG
    if ( !Abc_NtkCheck( pNtkNew ) )
        Abc_Print( 1, "Abc_NtkFromAigPhase(): Network check has failed.\n" );
    return pNtkNew;
}

Abc_NtkToDar()

Aig_Man_t * Abc_NtkToDar ( Abc_Ntk_t * pNtk, int fExors, int fRegisters )

extern

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

Synopsis [Converts the network from the AIG manager into ABC.]

Description [Assumes that registers are ordered after PIs/POs.]

SideEffects []

SeeAlso []

Definition at line 237 of file abcDar.c.

{
    Vec_Ptr_t * vNodes;
    Aig_Man_t * pMan;
    Aig_Obj_t * pObjNew;
    Abc_Obj_t * pObj;
    int i, nNodes, nDontCares;
    // make sure the latches follow PIs/POs
    if ( fRegisters ) 
    { 
        assert( Abc_NtkBoxNum(pNtk) == Abc_NtkLatchNum(pNtk) );
        Abc_NtkForEachCi( pNtk, pObj, i )
            if ( i < Abc_NtkPiNum(pNtk) )
            {
                assert( Abc_ObjIsPi(pObj) );
                if ( !Abc_ObjIsPi(pObj) )
                    Abc_Print( 1, "Abc_NtkToDar(): Temporary bug: The PI ordering is wrong!\n" );
            }
            else
                assert( Abc_ObjIsBo(pObj) );
        Abc_NtkForEachCo( pNtk, pObj, i )
            if ( i < Abc_NtkPoNum(pNtk) )
            {
                assert( Abc_ObjIsPo(pObj) );
                if ( !Abc_ObjIsPo(pObj) )
                    Abc_Print( 1, "Abc_NtkToDar(): Temporary bug: The PO ordering is wrong!\n" );
            }
            else
                assert( Abc_ObjIsBi(pObj) );
        // print warning about initial values
        nDontCares = 0;
        Abc_NtkForEachLatch( pNtk, pObj, i )
            if ( Abc_LatchIsInitDc(pObj) )
            {
                Abc_LatchSetInit0(pObj);
                nDontCares++;
            }
        if ( nDontCares )
        {
            Abc_Print( 1, "Warning: %d registers in this network have don't-care init values.\n", nDontCares );
            Abc_Print( 1, "The don't-care are assumed to be 0. The result may not verify.\n" );
            Abc_Print( 1, "Use command \"print_latch\" to see the init values of registers.\n" );
            Abc_Print( 1, "Use command \"zero\" to convert or \"init\" to change the values.\n" );
        }
    }
    // create the manager
    pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
    pMan->fCatchExor = fExors;
    pMan->nConstrs = pNtk->nConstrs;
    pMan->nBarBufs = pNtk->nBarBufs;
    pMan->pName = Extra_UtilStrsav( pNtk->pName );
    pMan->pSpec = Extra_UtilStrsav( pNtk->pSpec );
    // transfer the pointers to the basic nodes
    Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
    Abc_NtkForEachCi( pNtk, pObj, i )
    {
        pObj->pCopy = (Abc_Obj_t *)Aig_ObjCreateCi(pMan);
        // initialize logic level of the CIs
        ((Aig_Obj_t *)pObj->pCopy)->Level = pObj->Level;
    }
 
    // complement the 1-values registers
    if ( fRegisters ) {
        Abc_NtkForEachLatch( pNtk, pObj, i )
            if ( Abc_LatchIsInit1(pObj) )
                Abc_ObjFanout0(pObj)->pCopy = Abc_ObjNot(Abc_ObjFanout0(pObj)->pCopy);
    }
    // perform the conversion of the internal nodes (assumes DFS ordering)
//    pMan->fAddStrash = 1;
    vNodes = Abc_NtkDfs( pNtk, 0 );
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
//    Abc_NtkForEachNode( pNtk, pObj, i )
    {
        pObj->pCopy = (Abc_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj), (Aig_Obj_t *)Abc_ObjChild1Copy(pObj) );
//        Abc_Print( 1, "%d->%d ", pObj->Id, ((Aig_Obj_t *)pObj->pCopy)->Id );
    }
    Vec_PtrFree( vNodes );
    pMan->fAddStrash = 0;
    // create the POs
    Abc_NtkForEachCo( pNtk, pObj, i )
        Aig_ObjCreateCo( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj) );
    // complement the 1-valued registers
    Aig_ManSetRegNum( pMan, Abc_NtkLatchNum(pNtk) );
    if ( fRegisters )
        Aig_ManForEachLiSeq( pMan, pObjNew, i )
            if ( Abc_LatchIsInit1(Abc_ObjFanout0(Abc_NtkCo(pNtk,i))) )
                pObjNew->pFanin0 = Aig_Not(pObjNew->pFanin0);
    // remove dangling nodes
    nNodes = (Abc_NtkGetChoiceNum(pNtk) == 0)? Aig_ManCleanup( pMan ) : 0;
    if ( !fExors && nNodes )
        Abc_Print( 1, "Abc_NtkToDar(): Unexpected %d dangling nodes when converting to AIG!\n", nNodes );
//Aig_ManDumpVerilog( pMan, "test.v" );
    // save the number of registers
    if ( fRegisters )
    {
        Aig_ManSetRegNum( pMan, Abc_NtkLatchNum(pNtk) );
        pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs );
//        pMan->vFlopNums = NULL;
//        pMan->vOnehots = Abc_NtkConverLatchNamesIntoNumbers( pNtk );
        if ( pNtk->vOnehots )
            pMan->vOnehots = (Vec_Ptr_t *)Vec_VecDupInt( (Vec_Vec_t *)pNtk->vOnehots );
    }
    if ( !Aig_ManCheck( pMan ) )
    {
        Abc_Print( 1, "Abc_NtkToDar: AIG check has failed.\n" );
        Aig_ManStop( pMan );
        return NULL;
    }
    return pMan;
}

Here is the caller graph for this function:

Extra_BitMatrixTransposeP()

void Extra_BitMatrixTransposeP ( Vec_Wrd_t * vSimsIn, int nWordsIn, Vec_Wrd_t * vSimsOut, int nWordsOut )

extern

DECLARATIONS ///.

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

FileName [giaDecs.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Scalable AIG package.]

Synopsis [Calling various decomposition engines.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

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

]

Definition at line 2652 of file extraUtilMisc.c.

{    
    word * pM[64];  int i, y, x;
    assert( Vec_WrdSize(vSimsIn) == Vec_WrdSize(vSimsOut) );
    assert( Vec_WrdSize(vSimsIn) == 64 * nWordsIn * nWordsOut );
    for ( x = 0; x < nWordsOut; x++ )
    for ( y = 0; y < nWordsIn;  y++ )
    {
        for ( i = 0; i < 64; i++ )
        {
            pM[i]    = Vec_WrdEntryP( vSimsOut, (64*y+63-i)*nWordsOut + x );
            pM[i][0] = Vec_WrdEntry ( vSimsIn,  (64*x+63-i)*nWordsIn  + y );
        }
        Extra_Transpose64p( pM );
    }
}

Vec_IntReadList()

Vec_Int_t * Vec_IntReadList	(	char *	pStr,
		char	Separ )

Definition at line 13445 of file abc.c.

{
    Vec_Int_t * vRes = Vec_IntAlloc( 10 );
    Vec_IntPush( vRes, atoi(pStr) );
    for ( int c = 0; c < strlen(pStr); c++ )
        if ( pStr[c] == Separ )
            Vec_IntPush( vRes, atoi(pStr+c+1) );
    return vRes;
}

Here is the call graph for this function:

Variable Documentation

pBnd

Bnd_Man_t* pBnd

extern

DECLARATIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

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

FileName [giaDup.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Scalable AIG package.]

Synopsis [Duplication procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

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

]

Definition at line 61 of file giaBound.c.