liveness.c File Reference

#include <stdio.h>
#include "base/main/main.h"
#include "aig/aig/aig.h"
#include "aig/saig/saig.h"
#include <string.h>
#include "base/main/mainInt.h"

Go to the source code of this file.

Macros
#define	PROPAGATE_NAMES
#define	MULTIPLE_LTL_FORMULA
#define	ALLOW_SAFETY_PROPERTIES
#define	FULL_BIERE_MODE   0
#define	IGNORE_LIVENESS_KEEP_SAFETY_MODE   1
#define	IGNORE_SAFETY_KEEP_LIVENESS_MODE   2
#define	IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE   3
#define	FULL_BIERE_ONE_LOOP_MODE   4

Typedefs
typedef struct ltlNode_t	ltlNode

Functions
Aig_Man_t *	Abc_NtkToDar (Abc_Ntk_t *pNtk, int fExors, int fRegisters)
	DECLARATIONS ///. More...
Abc_Ntk_t *	Abc_NtkFromAigPhase (Aig_Man_t *pMan)
ltlNode *	readLtlFormula (char *formula)
void	traverseAbstractSyntaxTree (ltlNode *node)
ltlNode *	parseFormulaCreateAST (char *inputFormula)
int	isWellFormed (ltlNode *topNode)
int	checkSignalNameExistence (Abc_Ntk_t *pNtk, ltlNode *topASTNode)
void	populateBoolWithAigNodePtr (Abc_Ntk_t *pNtk, Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, ltlNode *topASTNode)
int	checkAllBoolHaveAIGPointer (ltlNode *topASTNode)
void	populateAigPointerUnitGF (Aig_Man_t *pAigNew, ltlNode *topASTNode, Vec_Ptr_t *vSignal, Vec_Vec_t *vAigGFMap)
void	setAIGNodePtrOfGloballyNode (ltlNode *astNode, Aig_Obj_t *pObjLo)
Aig_Obj_t *	buildLogicFromLTLNode (Aig_Man_t *pAig, ltlNode *pLtlNode)
Aig_Obj_t *	retriveAIGPointerFromLTLNode (ltlNode *astNode)
void	traverseAbstractSyntaxTree_postFix (ltlNode *node)
static int	nodeName_starts_with (Abc_Obj_t *pNode, const char *prefix)
void	printVecPtrOfString (Vec_Ptr_t *vec)
int	getPoIndex (Aig_Man_t *pAig, Aig_Obj_t *pPivot)
char *	retrieveTruePiName (Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, Aig_Obj_t *pObjPivot)
char *	retrieveLOName (Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, Aig_Obj_t *pObjPivot, Vec_Ptr_t *vLive, Vec_Ptr_t *vFair)
int	Aig_ManCiCleanupBiere (Aig_Man_t *p)
int	Aig_ManCoCleanupBiere (Aig_Man_t *p)
Aig_Man_t *	LivenessToSafetyTransformation (int mode, Abc_Ntk_t *pNtk, Aig_Man_t *p, Vec_Ptr_t *vLive, Vec_Ptr_t *vFair, Vec_Ptr_t *vAssertSafety, Vec_Ptr_t *vAssumeSafety)
Aig_Man_t *	LivenessToSafetyTransformationAbs (int mode, Abc_Ntk_t *pNtk, Aig_Man_t *p, Vec_Int_t *vFlops, Vec_Ptr_t *vLive, Vec_Ptr_t *vFair, Vec_Ptr_t *vAssertSafety, Vec_Ptr_t *vAssumeSafety)
Aig_Man_t *	LivenessToSafetyTransformationOneStepLoop (int mode, Abc_Ntk_t *pNtk, Aig_Man_t *p, Vec_Ptr_t *vLive, Vec_Ptr_t *vFair, Vec_Ptr_t *vAssertSafety, Vec_Ptr_t *vAssumeSafety)
Vec_Ptr_t *	populateLivenessVector (Abc_Ntk_t *pNtk, Aig_Man_t *pAig)
Vec_Ptr_t *	populateFairnessVector (Abc_Ntk_t *pNtk, Aig_Man_t *pAig)
Vec_Ptr_t *	populateSafetyAssertionVector (Abc_Ntk_t *pNtk, Aig_Man_t *pAig)
Vec_Ptr_t *	populateSafetyAssumptionVector (Abc_Ntk_t *pNtk, Aig_Man_t *pAig)
void	updateNewNetworkNameManager (Abc_Ntk_t *pNtk, Aig_Man_t *pAig, Vec_Ptr_t *vPiNames, Vec_Ptr_t *vLoNames)
int	Abc_CommandAbcLivenessToSafety (Abc_Frame_t *pAbc, int argc, char **argv)
Vec_Int_t *	prepareFlopVector (Aig_Man_t *pAig, int vectorLength)
int	Abc_CommandAbcLivenessToSafetyAbstraction (Abc_Frame_t *pAbc, int argc, char **argv)
Aig_Man_t *	LivenessToSafetyTransformationWithLTL (int mode, Abc_Ntk_t *pNtk, Aig_Man_t *p, Vec_Ptr_t *vLive, Vec_Ptr_t *vFair, Vec_Ptr_t *vAssertSafety, Vec_Ptr_t *vAssumeSafety, int *numLtlProcessed, Vec_Ptr_t *ltlBuffer)
int	Abc_CommandAbcLivenessToSafetyWithLTL (Abc_Frame_t *pAbc, int argc, char **argv)

Variables
Vec_Ptr_t *	vecPis
Vec_Ptr_t *	vecPiNames
Vec_Ptr_t *	vecLos
Vec_Ptr_t *	vecLoNames

Macro Definition Documentation

#define ALLOW_SAFETY_PROPERTIES

Definition at line 32 of file liveness.c.

#define FULL_BIERE_MODE   0

Definition at line 34 of file liveness.c.

#define FULL_BIERE_ONE_LOOP_MODE   4

Definition at line 38 of file liveness.c.

#define IGNORE_LIVENESS_KEEP_SAFETY_MODE   1

Definition at line 35 of file liveness.c.

#define IGNORE_SAFETY_KEEP_LIVENESS_MODE   2

Definition at line 36 of file liveness.c.

#define IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE   3

Definition at line 37 of file liveness.c.

#define MULTIPLE_LTL_FORMULA

Definition at line 31 of file liveness.c.

#define PROPAGATE_NAMES

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

FileName [liveness.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Liveness property checking.]

Synopsis [Main implementation module.]

Author [Sayak Ray]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - January 1, 2009.]

Revision [

Id:

liveness.c,v 1.00 2009/01/01 00:00:00 alanmi Exp

]

Definition at line 30 of file liveness.c.

Typedef Documentation

typedef struct ltlNode_t ltlNode

Definition at line 48 of file liveness.c.

Function Documentation

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

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;
}

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

Definition at line 1599 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;
    Vec_Int_t * vFlops;
                
    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 );
    }

    vFlops = prepareFlopVector( pAig, Aig_ManRegNum(pAig)%2 == 0? Aig_ManRegNum(pAig)/2 : (Aig_ManRegNum(pAig)-1)/2);

    //vFlops = prepareFlopVector( pAig, 100 );

    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 = LivenessToSafetyTransformationAbs( FULL_BIERE_MODE, pNtk, pAig, vFlops, 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 = LivenessToSafetyTransformationAbs( IGNORE_LIVENESS_KEEP_SAFETY_MODE, pNtk, pAig, vFlops, 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 = LivenessToSafetyTransformationAbs( IGNORE_SAFETY_KEEP_LIVENESS_MODE, pNtk, pAig, vFlops, 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;
        //}
    }

    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;
}

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

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;
}

Abc_Ntk_t* Abc_NtkFromAigPhase

(

Aig_Man_t *

pMan

)

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 590 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;
}

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

DECLARATIONS ///.

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 233 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;
}

int Aig_ManCiCleanupBiere

(

Aig_Man_t *

p

)

Definition at line 222 of file liveness.c.

{
    int nPisOld = Aig_ManCiNum(p);
    
    p->nObjs[AIG_OBJ_CI] = Vec_PtrSize( p->vCis );
    if ( Aig_ManRegNum(p) )
        p->nTruePis = Aig_ManCiNum(p) - Aig_ManRegNum(p);
    
    return nPisOld - Aig_ManCiNum(p);
}

int Aig_ManCoCleanupBiere

(

Aig_Man_t *

p

)

Definition at line 234 of file liveness.c.

{
    int nPosOld = Aig_ManCoNum(p);

    p->nObjs[AIG_OBJ_CO] = Vec_PtrSize( p->vCos );
    if ( Aig_ManRegNum(p) )
        p->nTruePos = Aig_ManCoNum(p) - Aig_ManRegNum(p);
    return nPosOld - Aig_ManCoNum(p);
}

Aig_Obj_t* buildLogicFromLTLNode	(	Aig_Man_t *	pAig,
		ltlNode *	pLtlNode
	)

Definition at line 601 of file ltl_parser.c.

{
    Aig_Obj_t *leftAigObj, *rightAigObj;

    if( pLtlNode->pObj != NULL )
        return pLtlNode->pObj;
    else
    {
        assert( pLtlNode->type != BOOL );
        switch( pLtlNode->type ){
            case AND:
                assert( pLtlNode->left ); assert( pLtlNode->right );
                leftAigObj = buildLogicFromLTLNode( pAig, pLtlNode->left );
                rightAigObj = buildLogicFromLTLNode( pAig, pLtlNode->right );
                assert( leftAigObj ); assert( rightAigObj );
                pLtlNode->pObj = Aig_And( pAig, leftAigObj, rightAigObj );
                return pLtlNode->pObj;
            case OR:
                assert( pLtlNode->left ); assert( pLtlNode->right );
                leftAigObj = buildLogicFromLTLNode( pAig, pLtlNode->left );
                rightAigObj = buildLogicFromLTLNode( pAig, pLtlNode->right );
                assert( leftAigObj ); assert( rightAigObj );
                pLtlNode->pObj = Aig_Or( pAig, leftAigObj, rightAigObj );
                return pLtlNode->pObj;
            case NOT:
                assert( pLtlNode->left ); assert( pLtlNode->right == NULL ); 
                leftAigObj = buildLogicFromLTLNode( pAig, pLtlNode->left );
                assert( leftAigObj );
                pLtlNode->pObj = Aig_Not( leftAigObj );
                return pLtlNode->pObj;
            case GLOBALLY:
            case EVENTUALLY:
            case NEXT:
            case UNTIL:
                printf("\nAttempting to create circuit with missing AIG pointer in a TEMPORAL node: ABORTING!!\n");
                exit(0);
            default:
                printf("\nSerious ERROR: attempting to create AIG node from a temporal node\n");
                exit(0);
        }
    }
}

int checkAllBoolHaveAIGPointer

(

ltlNode *

topASTNode

)

Definition at line 795 of file ltl_parser.c.

{
    
    switch( topASTNode->type ){
        case BOOL:
            if( topASTNode->pObj != NULL )
                return 1;
            else
            {
                printf("\nfaulting PODMANDYO topASTNode->name = %s\n", topASTNode->name);
                return 0;
            }
        case AND:
        case OR:
        case IMPLY:
        case UNTIL:
            assert( topASTNode->left != NULL );
            assert( topASTNode->right != NULL );
            return checkAllBoolHaveAIGPointer( topASTNode->left ) && checkAllBoolHaveAIGPointer( topASTNode->right );
            
        case NOT:
        case NEXT:
        case GLOBALLY:
        case EVENTUALLY:
            assert( topASTNode->left != NULL );
            assert( topASTNode->right == NULL );
            return checkAllBoolHaveAIGPointer( topASTNode->left );
        default:
            printf("\nUNSUPPORTED LTL NODE TYPE:: Aborting execution\n");
            exit(0);
    }
}

int checkSignalNameExistence	(	Abc_Ntk_t *	pNtk,
		ltlNode *	topASTNode
	)

Definition at line 699 of file ltl_parser.c.

{
    char *targetName;
    Abc_Obj_t * pNode;
    int i;
        
    switch( topASTNode->type ){
        case BOOL:
            targetName = topASTNode->name;
            //printf("\nTrying to match name %s\n", targetName);
            if( checkBooleanConstant( targetName ) != -1 )
                return 1;
            Abc_NtkForEachPo( pNtk, pNode, i )
            {
                if( strcmp( Abc_ObjName( pNode ), targetName ) == 0 )
                {
                    //printf("\nVariable name \"%s\" MATCHED\n", targetName);
                    return 1;
                }
            }
            printf("\nVariable name \"%s\" not found in the PO name list\n", targetName);
            return 0;
        case AND:
        case OR:
        case IMPLY:
        case UNTIL:
            assert( topASTNode->left != NULL );
            assert( topASTNode->right != NULL );
            return checkSignalNameExistence( pNtk, topASTNode->left ) && checkSignalNameExistence( pNtk, topASTNode->right );
            
        case NOT:
        case NEXT:
        case GLOBALLY:
        case EVENTUALLY:
            assert( topASTNode->left != NULL );
            assert( topASTNode->right == NULL );
            return checkSignalNameExistence( pNtk, topASTNode->left );
        default:
            printf("\nUNSUPPORTED LTL NODE TYPE:: Aborting execution\n");
            exit(0);
    }
}

int getPoIndex	(	Aig_Man_t *	pAig,
		Aig_Obj_t *	pPivot
	)

Definition at line 102 of file liveness.c.

{
    int i;
    Aig_Obj_t *pObj;

    Saig_ManForEachPo( pAig, pObj, i )
    {
        if( pObj == pPivot )
            return i;
    }
    return -1;
}

int isWellFormed

(

ltlNode *

topNode

)

Definition at line 661 of file ltl_parser.c.

{
    ltlNode *nextNode;

    switch( topNode->type ){
        case AND:
        case OR:
        case IMPLY:
            return isWellFormed( topNode->left) && isWellFormed( topNode->right ) ;
        case NOT:
            assert( topNode->right == NULL );
            return isWellFormed( topNode->left );
        case BOOL:
            return 1;
        case GLOBALLY:
            nextNode = topNode->left;
            assert( topNode->right == NULL );
            if( nextNode->type != EVENTUALLY )
                return 0;
            else
            {
                assert( nextNode->right == NULL );
                return isNonTemporalSubformula( nextNode->left );
            }
        default:
            return 0;
    }
}

Aig_Man_t* LivenessToSafetyTransformation	(	int	mode,
		Abc_Ntk_t *	pNtk,
		Aig_Man_t *	p,
		Vec_Ptr_t *	vLive,
		Vec_Ptr_t *	vFair,
		Vec_Ptr_t *	vAssertSafety,
		Vec_Ptr_t *	vAssumeSafety
	)

Definition at line 244 of file liveness.c.

{
    Aig_Man_t * pNew;
    int i, nRegCount;
    Aig_Obj_t * pObjSavePi = NULL;
    Aig_Obj_t *pObjSavedLo = NULL, *pObjSavedLi = NULL;
    Aig_Obj_t *pObj, *pMatch;
    Aig_Obj_t *pObjSaveOrSaved = NULL, *pObjSaveAndNotSaved = NULL, *pObjSavedLoAndEquality;
    Aig_Obj_t *pObjShadowLo, *pObjShadowLi, *pObjShadowLiDriver;
    Aig_Obj_t *pObjXor, *pObjXnor, *pObjAndAcc;
    Aig_Obj_t *pObjLive, *pObjFair, *pObjSafetyGate;
    Aig_Obj_t *pObjSafetyPropertyOutput = NULL;
    Aig_Obj_t *pObjOriginalSafetyPropertyOutput;
    Aig_Obj_t *pDriverImage, *pArgument, *collectiveAssertSafety, *collectiveAssumeSafety;
    char *nodeName;
    int piCopied = 0, liCopied = 0, loCopied = 0, liCreated = 0, loCreated = 0, liveLatch = 0, fairLatch = 0;
    
    vecPis = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
    vecPiNames = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);

    vecLos = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
    vecLoNames = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );

    //****************************************************************
    // Step1: create the new manager
    // Note: The new manager is created with "2 * Aig_ManObjNumMax(p)"
    // nodes, but this selection is arbitrary - need to be justified
    //****************************************************************
    pNew = Aig_ManStart( 2 * Aig_ManObjNumMax(p) );
    pNew->pName = (char *)malloc( strlen( pNtk->pName ) + strlen("_l2s") + 1 );
    sprintf(pNew->pName, "%s_%s", pNtk->pName, "l2s");
    pNew->pSpec = NULL;
    
    //****************************************************************
    // Step 2: map constant nodes
    //****************************************************************
    pObj = Aig_ManConst1( p );
    pObj->pData = Aig_ManConst1( pNew );

    //****************************************************************
    // Step 3: create true PIs
    //****************************************************************
    Saig_ManForEachPi( p, pObj, i )
    {
        piCopied++;
        pObj->pData = Aig_ObjCreateCi(pNew);
        Vec_PtrPush( vecPis, pObj->pData );
        nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) ));
        Vec_PtrPush( vecPiNames, nodeName );
    }

    //****************************************************************
    // Step 4: create the special Pi corresponding to SAVE
    //****************************************************************
    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
    {
        pObjSavePi = Aig_ObjCreateCi( pNew );
        nodeName = "SAVE_BIERE",
        Vec_PtrPush( vecPiNames, nodeName );
    }
        
    //****************************************************************
    // Step 5: create register outputs
    //****************************************************************
    Saig_ManForEachLo( p, pObj, i )
    {
        loCopied++;
        pObj->pData = Aig_ObjCreateCi(pNew);
        Vec_PtrPush( vecLos, pObj->pData );
        nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ));
        Vec_PtrPush( vecLoNames, nodeName );
    }

    //****************************************************************
    // Step 6: create "saved" register output
    //****************************************************************
    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
    {
        loCreated++;
        pObjSavedLo = Aig_ObjCreateCi( pNew );
        Vec_PtrPush( vecLos, pObjSavedLo );
        nodeName = "SAVED_LO";
        Vec_PtrPush( vecLoNames, nodeName );
    }

    //****************************************************************
    // Step 7: create the OR gate and the AND gate directly fed by "SAVE" Pi
    //****************************************************************
    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
    {
        pObjSaveOrSaved = Aig_Or( pNew, pObjSavePi, pObjSavedLo );
        pObjSaveAndNotSaved = Aig_And( pNew, pObjSavePi, Aig_Not(pObjSavedLo) );
    }

    //********************************************************************
    // Step 8: create internal nodes
    //********************************************************************
    Aig_ManForEachNode( p, pObj, i )
    {
        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    }

    
    //********************************************************************
    // Step 8.x : create PO for each safety assertions
    // NOTE : Here the output is purposely inverted as it will be thrown to 
    // dprove
    //********************************************************************
    if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
    {
        if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) == 0 )
        {
            pObjAndAcc = Aig_ManConst1( pNew );
            Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
            {
                pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
                pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
            }
            pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_Not(pObjAndAcc) );
        }
        else if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) != 0 )
        {
            pObjAndAcc = Aig_ManConst1( pNew );
            Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
            {
                pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
                pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
            }
            collectiveAssertSafety = pObjAndAcc;

            pObjAndAcc = Aig_ManConst1( pNew );
            Vec_PtrForEachEntry( Aig_Obj_t *, vAssumeSafety, pObj, i )
            {
                pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
                pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
            }
            collectiveAssumeSafety = pObjAndAcc;
            pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) );
        }
        else
        {
            printf("WARNING!! No safety property is found, a new (negated) constant 1 output is created\n");
            pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_Not( Aig_ManConst1(pNew) ) );
        }
    }

    //********************************************************************
    // Step 9: create the safety property output gate for the liveness properties
    // discuss with Sat/Alan for an alternative implementation
    //********************************************************************
    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
    {
        pObjSafetyPropertyOutput = Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
    }

    // create register inputs for the original registers
    nRegCount = 0;
    
    Saig_ManForEachLo( p, pObj, i )
    {
        pMatch = Saig_ObjLoToLi( p, pObj );
        Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
        nRegCount++;
        liCopied++;
    }

    // create register input corresponding to the register "saved"
    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
    {
        #ifndef DUPLICATE_CKT_DEBUG
            pObjSavedLi = Aig_ObjCreateCo( pNew, pObjSaveOrSaved );
            nRegCount++;
            liCreated++;

            //Changed on October 13, 2009
            //pObjAndAcc = NULL;
            pObjAndAcc = Aig_ManConst1( pNew );

    // create the family of shadow registers, then create the cascade of Xnor and And gates for the comparator 
            Saig_ManForEachLo( p, pObj, i )
            {
                pObjShadowLo = Aig_ObjCreateCi( pNew );

                #ifdef PROPAGATE_NAMES
                    Vec_PtrPush( vecLos, pObjShadowLo );
                    nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ) ) + 10 );
                    sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "SHADOW" );
                    
                    Vec_PtrPush( vecLoNames, nodeName );
                #endif

                pObjShadowLiDriver = Aig_Mux( pNew, pObjSaveAndNotSaved, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
                pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
                nRegCount++;
                loCreated++; liCreated++;
        
                pObjXor = Aig_Exor( pNew, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
                pObjXnor = Aig_Not( pObjXor );
                
                pObjAndAcc = Aig_And( pNew, pObjXnor, pObjAndAcc );
            }

            // create the AND gate whose output will be the signal "looped"
            pObjSavedLoAndEquality = Aig_And( pNew, pObjSavedLo, pObjAndAcc );

            // create the master AND gate and corresponding AND and OR logic for the liveness properties
            pObjAndAcc = Aig_ManConst1( pNew );
            if( vLive == NULL || Vec_PtrSize( vLive ) == 0 )
            {
                printf("Circuit without any liveness property\n");
            }
            else
            {
                Vec_PtrForEachEntry( Aig_Obj_t *, vLive, pObj, i )
                {
                    liveLatch++;
                    pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
                    pObjShadowLo = Aig_ObjCreateCi( pNew );

                    #ifdef PROPAGATE_NAMES
                        Vec_PtrPush( vecLos, pObjShadowLo );
                        nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 );
                        sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "LIVENESS" );
                        Vec_PtrPush( vecLoNames, nodeName );
                    #endif

                    pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
                    pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
                    nRegCount++;
                    loCreated++; liCreated++;
            
                    pObjAndAcc = Aig_And( pNew, pObjShadowLo, pObjAndAcc );
                }
            }

            pObjLive = pObjAndAcc;
                
            pObjAndAcc = Aig_ManConst1( pNew );
            if( vFair == NULL || Vec_PtrSize( vFair ) == 0 )
                printf("Circuit without any fairness property\n");
            else
            {
                Vec_PtrForEachEntry( Aig_Obj_t *, vFair, pObj, i )
                {
                    fairLatch++;
                    pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
                    pObjShadowLo = Aig_ObjCreateCi( pNew );

                    #ifdef PROPAGATE_NAMES
                        Vec_PtrPush( vecLos, pObjShadowLo );
                        nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 );
                        sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "FAIRNESS" );
                        Vec_PtrPush( vecLoNames, nodeName );
                    #endif

                    pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
                    pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
                    nRegCount++;
                    loCreated++; liCreated++;
            
                    pObjAndAcc = Aig_And( pNew, pObjShadowLo, pObjAndAcc );
                }
            }

            pObjFair = pObjAndAcc;
                
            //pObjSafetyGate = Aig_Exor( pNew, Aig_Not(Aig_ManConst1( pNew )), Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) ) );
            //Following is the actual Biere translation
            pObjSafetyGate = Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) );

            Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyGate );
        #endif
    }

    Aig_ManSetRegNum( pNew, nRegCount );

    Aig_ManCiCleanupBiere( pNew );
    Aig_ManCoCleanupBiere( pNew );
    
    Aig_ManCleanup( pNew );
    
    assert( Aig_ManCheck( pNew ) );
    
    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
    {
            assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjCioId(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
            assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) );
            assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch );
    }

    return pNew;
}

Aig_Man_t* LivenessToSafetyTransformationAbs	(	int	mode,
		Abc_Ntk_t *	pNtk,
		Aig_Man_t *	p,
		Vec_Int_t *	vFlops,
		Vec_Ptr_t *	vLive,
		Vec_Ptr_t *	vFair,
		Vec_Ptr_t *	vAssertSafety,
		Vec_Ptr_t *	vAssumeSafety
	)

Definition at line 542 of file liveness.c.

{
    Aig_Man_t * pNew;
    int i, nRegCount, iEntry;
    Aig_Obj_t * pObjSavePi = NULL;
    Aig_Obj_t *pObjSavedLi = NULL, *pObjSavedLo = NULL;
    Aig_Obj_t *pObj, *pMatch;
    Aig_Obj_t *pObjSavedLoAndEquality, *pObjSaveOrSaved = NULL, *pObjSaveAndNotSaved = NULL;
    Aig_Obj_t *pObjShadowLo, *pObjShadowLi, *pObjShadowLiDriver;
    Aig_Obj_t *pObjXor, *pObjXnor, *pObjAndAcc;
    Aig_Obj_t *pObjLive, *pObjFair, *pObjSafetyGate;
    Aig_Obj_t *pObjSafetyPropertyOutput = NULL;
    Aig_Obj_t *pDriverImage, *pArgument, *collectiveAssertSafety, *collectiveAssumeSafety;
    char *nodeName;
    int piCopied = 0, liCopied = 0, loCopied = 0, liCreated = 0, loCreated = 0, liveLatch = 0, fairLatch = 0;//, piVecIndex = 0;
    
    vecPis = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
    vecPiNames = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);

    vecLos = Vec_PtrAlloc( Saig_ManRegNum( p ) + Vec_IntSize( vFlops ) + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
    vecLoNames = Vec_PtrAlloc( Saig_ManRegNum( p ) + Vec_IntSize( vFlops ) + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );

    //****************************************************************
    // Step1: create the new manager
    // Note: The new manager is created with "2 * Aig_ManObjNumMax(p)"
    // nodes, but this selection is arbitrary - need to be justified
    //****************************************************************
    pNew = Aig_ManStart( 2 * Aig_ManObjNumMax(p) );
    pNew->pName = (char *)malloc( strlen( pNtk->pName ) + strlen("_l2s") + 1 );
    sprintf(pNew->pName, "%s_%s", pNtk->pName, "l2s");
    pNew->pSpec = NULL;
    
    //****************************************************************
    // Step 2: map constant nodes
    //****************************************************************
    pObj = Aig_ManConst1( p );
    pObj->pData = Aig_ManConst1( pNew );

    //****************************************************************
    // Step 3: create true PIs
    //****************************************************************
    Saig_ManForEachPi( p, pObj, i )
    {
        piCopied++;
        pObj->pData = Aig_ObjCreateCi(pNew);
        Vec_PtrPush( vecPis, pObj->pData );
        nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) ));
        Vec_PtrPush( vecPiNames, nodeName );
    }

    //****************************************************************
    // Step 4: create the special Pi corresponding to SAVE
    //****************************************************************
    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
    {
        pObjSavePi = Aig_ObjCreateCi( pNew );
        nodeName = "SAVE_BIERE",
        Vec_PtrPush( vecPiNames, nodeName );
    }
        
    //****************************************************************
    // Step 5: create register outputs
    //****************************************************************
    Saig_ManForEachLo( p, pObj, i )
    {
        loCopied++;
        pObj->pData = Aig_ObjCreateCi(pNew);
        Vec_PtrPush( vecLos, pObj->pData );
        nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ));
        Vec_PtrPush( vecLoNames, nodeName );
    }

    //****************************************************************
    // Step 6: create "saved" register output
    //****************************************************************
    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
    {
        loCreated++;
        pObjSavedLo = Aig_ObjCreateCi( pNew );
        Vec_PtrPush( vecLos, pObjSavedLo );
        nodeName = "SAVED_LO";
        Vec_PtrPush( vecLoNames, nodeName );
    }

    //****************************************************************
    // Step 7: create the OR gate and the AND gate directly fed by "SAVE" Pi
    //****************************************************************
    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
    {
        pObjSaveOrSaved = Aig_Or( pNew, pObjSavePi, pObjSavedLo );
        pObjSaveAndNotSaved = Aig_And( pNew, pObjSavePi, Aig_Not(pObjSavedLo) );
    }

    //********************************************************************
    // Step 8: create internal nodes
    //********************************************************************
    Aig_ManForEachNode( p, pObj, i )
    {
        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    }

    
    //********************************************************************
    // Step 8.x : create PO for each safety assertions
    // NOTE : Here the output is purposely inverted as it will be thrown to 
    // dprove
    //********************************************************************
    if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
    {
        if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) == 0 )
        {
            pObjAndAcc = Aig_ManConst1( pNew );
            Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
            {
                pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
                pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
            }
            Aig_ObjCreateCo( pNew, Aig_Not(pObjAndAcc) );
        }
        else if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) != 0 )
        {
            pObjAndAcc = Aig_ManConst1( pNew );
            Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
            {
                pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
                pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
            }
            collectiveAssertSafety = pObjAndAcc;

            pObjAndAcc = Aig_ManConst1( pNew );
            Vec_PtrForEachEntry( Aig_Obj_t *, vAssumeSafety, pObj, i )
            {
                pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
                pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
            }
            collectiveAssumeSafety = pObjAndAcc;
            Aig_ObjCreateCo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) );
        }
        else
        {
            printf("WARNING!! No safety property is found, a new (negated) constant 1 output is created\n");
            Aig_ObjCreateCo( pNew, Aig_Not( Aig_ManConst1(pNew) ) );
        }
    }

    //********************************************************************
    // Step 9: create the safety property output gate for the liveness properties
    // discuss with Sat/Alan for an alternative implementation
    //********************************************************************
    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
    {
        pObjSafetyPropertyOutput = Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
    }

    // create register inputs for the original registers
    nRegCount = 0;
    
    Saig_ManForEachLo( p, pObj, i )
    {
        pMatch = Saig_ObjLoToLi( p, pObj );
        Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
        nRegCount++;
        liCopied++;
    }

    // create register input corresponding to the register "saved"
    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
    {
        #ifndef DUPLICATE_CKT_DEBUG
            pObjSavedLi = Aig_ObjCreateCo( pNew, pObjSaveOrSaved );
            nRegCount++;
            liCreated++;

            //Changed on October 13, 2009
            //pObjAndAcc = NULL;
            pObjAndAcc = Aig_ManConst1( pNew );

    // create the family of shadow registers, then create the cascade of Xnor and And gates for the comparator 
            //Saig_ManForEachLo( p, pObj, i )
            Saig_ManForEachLo( p, pObj, i )
            {
                printf("Flop[%d] = %s\n", i, Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ) );
            }
            Vec_IntForEachEntry( vFlops, iEntry, i )
            {
                pObjShadowLo = Aig_ObjCreateCi( pNew );
                pObj = Aig_ManLo( p, iEntry );

                #ifdef PROPAGATE_NAMES
                    Vec_PtrPush( vecLos, pObjShadowLo );
                    nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + iEntry ) ) ) + 10 );
                    sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + iEntry ) ), "SHADOW" );
                    printf("Flop copied [%d] = %s\n", iEntry, nodeName );
                    Vec_PtrPush( vecLoNames, nodeName );
                #endif

                pObjShadowLiDriver = Aig_Mux( pNew, pObjSaveAndNotSaved, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
                pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
                nRegCount++;
                loCreated++; liCreated++;
        
                pObjXor = Aig_Exor( pNew, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
                pObjXnor = Aig_Not( pObjXor );
                
                pObjAndAcc = Aig_And( pNew, pObjXnor, pObjAndAcc );
            }

            // create the AND gate whose output will be the signal "looped"
            pObjSavedLoAndEquality = Aig_And( pNew, pObjSavedLo, pObjAndAcc );

            // create the master AND gate and corresponding AND and OR logic for the liveness properties
            pObjAndAcc = Aig_ManConst1( pNew );
            if( vLive == NULL || Vec_PtrSize( vLive ) == 0 )
            {
                printf("Circuit without any liveness property\n");
            }
            else
            {
                Vec_PtrForEachEntry( Aig_Obj_t *, vLive, pObj, i )
                {
                    liveLatch++;
                    pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
                    pObjShadowLo = Aig_ObjCreateCi( pNew );

                    #ifdef PROPAGATE_NAMES
                        Vec_PtrPush( vecLos, pObjShadowLo );
                        nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 );
                        sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "LIVENESS" );
                        Vec_PtrPush( vecLoNames, nodeName );
                    #endif

                    pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
                    pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
                    nRegCount++;
                    loCreated++; liCreated++;
            
                    pObjAndAcc = Aig_And( pNew, pObjShadowLo, pObjAndAcc );
                }
            }

            pObjLive = pObjAndAcc;
                
            pObjAndAcc = Aig_ManConst1( pNew );
            if( vFair == NULL || Vec_PtrSize( vFair ) == 0 )
                printf("Circuit without any fairness property\n");
            else
            {
                Vec_PtrForEachEntry( Aig_Obj_t *, vFair, pObj, i )
                {
                    fairLatch++;
                    pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
                    pObjShadowLo = Aig_ObjCreateCi( pNew );

                    #ifdef PROPAGATE_NAMES
                        Vec_PtrPush( vecLos, pObjShadowLo );
                        nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 );
                        sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "FAIRNESS" );
                        Vec_PtrPush( vecLoNames, nodeName );
                    #endif

                    pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
                    pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
                    nRegCount++;
                    loCreated++; liCreated++;
            
                    pObjAndAcc = Aig_And( pNew, pObjShadowLo, pObjAndAcc );
                }
            }

            pObjFair = pObjAndAcc;
                
            //pObjSafetyGate = Aig_Exor( pNew, Aig_Not(Aig_ManConst1( pNew )), Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) ) );
            //Following is the actual Biere translation
            pObjSafetyGate = Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) );

            Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyGate );
        #endif
    }

    Aig_ManSetRegNum( pNew, nRegCount );

    Aig_ManCiCleanupBiere( pNew );
    Aig_ManCoCleanupBiere( pNew );
    
    Aig_ManCleanup( pNew );
    
    assert( Aig_ManCheck( pNew ) );
    
    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
    {
            assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjCioId(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
            assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) );
            assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) + Vec_IntSize( vFlops ) + 1 + liveLatch + fairLatch );
    }

    return pNew;
}

Aig_Man_t* LivenessToSafetyTransformationOneStepLoop	(	int	mode,
		Abc_Ntk_t *	pNtk,
		Aig_Man_t *	p,
		Vec_Ptr_t *	vLive,
		Vec_Ptr_t *	vFair,
		Vec_Ptr_t *	vAssertSafety,
		Vec_Ptr_t *	vAssumeSafety
	)

Definition at line 843 of file liveness.c.

{
    Aig_Man_t * pNew;
    int i, nRegCount;
    Aig_Obj_t * pObjSavePi = NULL;
    Aig_Obj_t *pObj, *pMatch;
    Aig_Obj_t *pObjSavedLoAndEquality;
    Aig_Obj_t *pObjXor, *pObjXnor, *pObjAndAcc, *pObjAndAccDummy;
    Aig_Obj_t *pObjLive, *pObjFair, *pObjSafetyGate;
    Aig_Obj_t *pObjSafetyPropertyOutput = NULL;
    Aig_Obj_t *pDriverImage;
    Aig_Obj_t *pObjCorrespondingLi;
    Aig_Obj_t *pArgument;
    Aig_Obj_t *collectiveAssertSafety, *collectiveAssumeSafety;

    char *nodeName;
    int piCopied = 0, liCopied = 0, loCopied = 0;//, liCreated = 0, loCreated = 0, piVecIndex = 0;

    if( Aig_ManRegNum( p ) == 0 )
    {
        printf("The input AIG contains no register, returning the original AIG as it is\n");
        return p;
    }

    vecPis = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
    vecPiNames = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);

    vecLos = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
    vecLoNames = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );

    //****************************************************************
    // Step1: create the new manager
    // Note: The new manager is created with "2 * Aig_ManObjNumMax(p)"
    // nodes, but this selection is arbitrary - need to be justified
    //****************************************************************
    pNew = Aig_ManStart( 2 * Aig_ManObjNumMax(p) );
    pNew->pName = Abc_UtilStrsav( "live2safe" );
    pNew->pSpec = NULL;
    
    //****************************************************************
    // Step 2: map constant nodes
    //****************************************************************
    pObj = Aig_ManConst1( p );
    pObj->pData = Aig_ManConst1( pNew );

    //****************************************************************
    // Step 3: create true PIs
    //****************************************************************
    Saig_ManForEachPi( p, pObj, i )
    {
        piCopied++;
        pObj->pData = Aig_ObjCreateCi(pNew);
        Vec_PtrPush( vecPis, pObj->pData );
        nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) ));
        Vec_PtrPush( vecPiNames, nodeName );
    }

    //****************************************************************
    // Step 4: create the special Pi corresponding to SAVE
    //****************************************************************
    if( mode == FULL_BIERE_ONE_LOOP_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE )
    {
        pObjSavePi = Aig_ObjCreateCi( pNew );
        nodeName = "SAVE_BIERE",
        Vec_PtrPush( vecPiNames, nodeName );
    }
            
    //****************************************************************
    // Step 5: create register outputs
    //****************************************************************
    Saig_ManForEachLo( p, pObj, i )
    {
        loCopied++;
        pObj->pData = Aig_ObjCreateCi(pNew);
        Vec_PtrPush( vecLos, pObj->pData );
        nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ));
        Vec_PtrPush( vecLoNames, nodeName );
    }

    //****************************************************************
    // Step 6: create "saved" register output
    //****************************************************************

#if 0
    loCreated++;
    pObjSavedLo = Aig_ObjCreateCi( pNew );
    Vec_PtrPush( vecLos, pObjSavedLo );
    nodeName = "SAVED_LO";
    Vec_PtrPush( vecLoNames, nodeName );
#endif

    //****************************************************************
    // Step 7: create the OR gate and the AND gate directly fed by "SAVE" Pi
    //****************************************************************
#if 0
    pObjSaveOrSaved = Aig_Or( pNew, pObjSavePi, pObjSavedLo );
    pObjSaveAndNotSaved = Aig_And( pNew, pObjSavePi, Aig_Not(pObjSavedLo) );
#endif

    //********************************************************************
    // Step 8: create internal nodes
    //********************************************************************
    Aig_ManForEachNode( p, pObj, i )
    {
        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    }

#if 0
    //********************************************************************
    // Step 8.x : create PO for each safety assertions
    //********************************************************************
    Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
    {
        pObj->pData = Aig_ObjCreateCo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) );
    }
#endif

    if( mode == FULL_BIERE_ONE_LOOP_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
    {
        if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) == 0 )
        {
            pObjAndAcc = NULL;
            Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
            {
                //pObj->pData = Aig_ObjCreateCo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) );
                pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
                if( pObjAndAcc == NULL )
                    pObjAndAcc = pArgument;
                else
                {
                    pObjAndAccDummy = pObjAndAcc;
                    pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAccDummy );
                }
            }
            Aig_ObjCreateCo( pNew, Aig_Not(pObjAndAcc) );
        }
        else if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) != 0 )
        {
            pObjAndAcc = NULL;
            Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
            {
                //pObj->pData = Aig_ObjCreateCo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) );
                pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
                if( pObjAndAcc == NULL )
                    pObjAndAcc = pArgument;
                else
                {
                    pObjAndAccDummy = pObjAndAcc;
                    pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAccDummy );
                }
            }
            collectiveAssertSafety = pObjAndAcc;
            pObjAndAcc = NULL;
            Vec_PtrForEachEntry( Aig_Obj_t *, vAssumeSafety, pObj, i )
            {
                //pObj->pData = Aig_ObjCreateCo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) );
                pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
                if( pObjAndAcc == NULL )
                    pObjAndAcc = pArgument;
                else
                {
                    pObjAndAccDummy = pObjAndAcc;
                    pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAccDummy );
                }
            }
            collectiveAssumeSafety = pObjAndAcc;
            Aig_ObjCreateCo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) );
        }
        else
            printf("No safety property is specified, hence no safety gate is created\n");
    }

    //********************************************************************
    // Step 9: create the safety property output gate
    // create the safety property output gate, this will be the sole true PO 
    // of the whole circuit, discuss with Sat/Alan for an alternative implementation
    //********************************************************************

    if( mode == FULL_BIERE_ONE_LOOP_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE )
    {
        pObjSafetyPropertyOutput = Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
    }

    // create register inputs for the original registers
    nRegCount = 0;
    
    Saig_ManForEachLo( p, pObj, i )
    {
        pMatch = Saig_ObjLoToLi( p, pObj );
        //Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pMatch) );
        Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
        nRegCount++;
        liCopied++;
    }

#if 0
    // create register input corresponding to the register "saved"
    pObjSavedLi = Aig_ObjCreateCo( pNew, pObjSaveOrSaved );
    nRegCount++;
    liCreated++;7
#endif

    pObjAndAcc = NULL;

    //****************************************************************************************************
    //For detection of loop of length 1 we do not need any shadow register, we only need equality detector
    //between Lo_j and Li_j and then a cascade of AND gates
    //****************************************************************************************************

    if( mode == FULL_BIERE_ONE_LOOP_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE )
    {
        Saig_ManForEachLo( p, pObj, i )
        {
            pObjCorrespondingLi = Saig_ObjLoToLi( p, pObj );
        
            pObjXor = Aig_Exor( pNew, (Aig_Obj_t *)pObj->pData,  Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0( pObjCorrespondingLi )->pData, Aig_ObjFaninC0( pObjCorrespondingLi ) ) );
            pObjXnor = Aig_Not( pObjXor );
        
            if( pObjAndAcc == NULL )
                pObjAndAcc = pObjXnor;
            else
            {
                pObjAndAccDummy = pObjAndAcc;
                pObjAndAcc = Aig_And( pNew, pObjXnor, pObjAndAccDummy );
            }
        }

        // create the AND gate whose output will be the signal "looped"
        pObjSavedLoAndEquality = Aig_And( pNew, pObjSavePi, pObjAndAcc );
    
        // create the master AND gate and corresponding AND and OR logic for the liveness properties
        pObjAndAcc = NULL;
        if( vLive == NULL || Vec_PtrSize( vLive ) == 0 )
            printf("Circuit without any liveness property\n");
        else
        {
            Vec_PtrForEachEntry( Aig_Obj_t *, vLive, pObj, i )
            {
                pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
                if( pObjAndAcc == NULL )
                    pObjAndAcc = pDriverImage;
                else
                {
                    pObjAndAccDummy = pObjAndAcc;
                    pObjAndAcc = Aig_And( pNew, pDriverImage, pObjAndAccDummy );
                }
            }
        }

        if( pObjAndAcc != NULL )
            pObjLive = pObjAndAcc;
        else
            pObjLive = Aig_ManConst1( pNew );
    
        // create the master AND gate and corresponding AND and OR logic for the fairness properties
        pObjAndAcc = NULL;
        if( vFair == NULL || Vec_PtrSize( vFair ) == 0 )
            printf("Circuit without any fairness property\n");
        else
        {
            Vec_PtrForEachEntry( Aig_Obj_t *, vFair, pObj, i )
            {
                pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
                if( pObjAndAcc == NULL )
                    pObjAndAcc = pDriverImage;
                else
                {
                    pObjAndAccDummy = pObjAndAcc;
                    pObjAndAcc = Aig_And( pNew, pDriverImage, pObjAndAccDummy );
                }
            }
        }

        if( pObjAndAcc != NULL )
            pObjFair = pObjAndAcc;
        else
            pObjFair = Aig_ManConst1( pNew );
    
        pObjSafetyGate = Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) );
    
        Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyGate );
    }

    Aig_ManSetRegNum( pNew, nRegCount );

    //printf("\nSaig_ManPiNum = %d, Reg Num = %d, before everything, before Pi cleanup\n", Vec_PtrSize( pNew->vPis ), pNew->nRegs );

    Aig_ManCiCleanupBiere( pNew );
    Aig_ManCoCleanupBiere( pNew );

    Aig_ManCleanup( pNew );
    
    assert( Aig_ManCheck( pNew ) );
    
    return pNew;
}

Aig_Man_t* LivenessToSafetyTransformationWithLTL	(	int	mode,
		Abc_Ntk_t *	pNtk,
		Aig_Man_t *	p,
		Vec_Ptr_t *	vLive,
		Vec_Ptr_t *	vFair,
		Vec_Ptr_t *	vAssertSafety,
		Vec_Ptr_t *	vAssumeSafety,
		int *	numLtlProcessed,
		Vec_Ptr_t *	ltlBuffer
	)

Definition at line 1798 of file liveness.c.

{
    Aig_Man_t * pNew;
    int i, ii, iii, nRegCount;
    Aig_Obj_t * pObjSavePi = NULL;
    Aig_Obj_t *pObjSavedLo = NULL, *pObjSavedLi = NULL;
    Aig_Obj_t *pObj, *pMatch;
    Aig_Obj_t *pObjSaveOrSaved = NULL, *pObjSaveAndNotSaved = NULL, *pObjSavedLoAndEquality;
    Aig_Obj_t *pObjShadowLo, *pObjShadowLi, *pObjShadowLiDriver;
    Aig_Obj_t *pObjXor, *pObjXnor, *pObjAndAcc;
    Aig_Obj_t *pObjLive, *pObjSafetyGate;
    Aig_Obj_t *pObjSafetyPropertyOutput;
    Aig_Obj_t *pObjOriginalSafetyPropertyOutput;
    Aig_Obj_t *pDriverImage, *pArgument, *collectiveAssertSafety, *collectiveAssumeSafety;
    Aig_Obj_t *pNegatedSafetyConjunction = NULL;
    Aig_Obj_t *pObjSafetyAndLiveToSafety;
    char *nodeName, *pFormula;
    int piCopied = 0, liCopied = 0, loCopied = 0, liCreated = 0, loCreated = 0, liveLatch = 0;//, piVecIndex = 0, fairLatch = 0;
    Vec_Ptr_t *vSignal, *vTopASTNodeArray = NULL;
    ltlNode *pEnrtyGLOBALLY;
    ltlNode *topNodeOfAST, *tempTopASTNode;
    Vec_Vec_t *vAigGFMap;
    Vec_Ptr_t *vSignalMemory, *vGFFlopMemory, *vPoForLtlProps = NULL;
    Vec_Ptr_t *vecInputLtlFormulae;
    
    vecPis = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
    vecPiNames = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);

    vecLos = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
    vecLoNames = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );

    //****************************************************************
    //step0: Parsing the LTL formula
    //****************************************************************
    //Vec_PtrForEachEntry( char *, pNtk->vLtlProperties, pFormula, i )
    //  printf("\ninput LTL formula [%d] = %s\n", i, pFormula );


#ifdef MULTIPLE_LTL_FORMULA


    //***************************************************************************
    //Reading input LTL formulae from Ntk data-structure and creating 
    //AST for them, Steps involved: 
    //      parsing -> AST creation -> well-formedness check -> signal name check
    //***************************************************************************

    //resetting numLtlProcessed
    *numLtlProcessed = 0;
    
    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
    {
        //if( ltlBuffer )
        vecInputLtlFormulae = ltlBuffer;
        //vecInputLtlFormulae = pNtk->vLtlProperties;
        if( vecInputLtlFormulae )
        {
            vTopASTNodeArray = Vec_PtrAlloc( Vec_PtrSize( vecInputLtlFormulae ) );
            printf("\n");
            Vec_PtrForEachEntry( char *, vecInputLtlFormulae, pFormula, i )
            {
                tempTopASTNode = parseFormulaCreateAST( pFormula );
                //traverseAbstractSyntaxTree_postFix( tempTopASTNode );
                if( tempTopASTNode )
                {
                    printf("Formula %d: AST is created, ", i+1);
                    if( isWellFormed( tempTopASTNode ) )
                        printf("Well-formedness check PASSED, ");
                    else
                    {
                        printf("Well-formedness check FAILED!!\n");
                        printf("AST will be ignored for formula %d, no extra logic will be added for this formula\n", i+1 );
                        //do memory management to free the created AST
                        continue;
                    }
                    if( checkSignalNameExistence( pNtk, tempTopASTNode ) )
                        printf("Signal check PASSED\n");
                    else
                    {
                        printf("Signal check FAILED!!");
                        printf("AST will be ignored for formula %d, no extra logic will be added for this formula\n", i+1 );
                        //do memory management to free the created AST
                        continue;
                    }
                    Vec_PtrPush( vTopASTNodeArray, tempTopASTNode );
                    (*numLtlProcessed)++;
                }
                else
                    printf("\nNo AST has been created for formula %d, no extra logic will be added\n", i+1 );
            }
        }
        printf("\n");
        if( Vec_PtrSize( vTopASTNodeArray ) == 0 )
        {
            //printf("\nNo AST has been created for any formula; hence the circuit is left untouched\n");
            printf("\nCurrently aborting, need to take care when Vec_PtrSize( vTopASTNodeArray ) == 0\n");
            exit(0);
        }
    }

        //****************************************************************
        // Step1: create the new manager
        // Note: The new manager is created with "2 * Aig_ManObjNumMax(p)"
        // nodes, but this selection is arbitrary - need to be justified
        //****************************************************************
        pNew = Aig_ManStart( 2 * Aig_ManObjNumMax(p) );
        pNew->pName = (char *)malloc( strlen( pNtk->pName ) + strlen("_l3s") + 1 );
        sprintf(pNew->pName, "%s_%s", pNtk->pName, "l3s");
        pNew->pSpec = NULL;
    
        //****************************************************************
        // Step 2: map constant nodes
        //****************************************************************
        pObj = Aig_ManConst1( p );
        pObj->pData = Aig_ManConst1( pNew );

        //****************************************************************
        // Step 3: create true PIs
        //****************************************************************
        Saig_ManForEachPi( p, pObj, i )
        {
            piCopied++;
            pObj->pData = Aig_ObjCreateCi(pNew);
            Vec_PtrPush( vecPis, pObj->pData );
            nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) ));
            Vec_PtrPush( vecPiNames, nodeName );
        }

        //****************************************************************
        // Step 4: create the special Pi corresponding to SAVE
        //****************************************************************
        if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
        {
            pObjSavePi = Aig_ObjCreateCi( pNew );
            nodeName = "SAVE_BIERE",
            Vec_PtrPush( vecPiNames, nodeName );
        }
        
        //****************************************************************
        // Step 5: create register outputs
        //****************************************************************
        Saig_ManForEachLo( p, pObj, i )
        {
            loCopied++;
            pObj->pData = Aig_ObjCreateCi(pNew);
            Vec_PtrPush( vecLos, pObj->pData );
            nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ));
            Vec_PtrPush( vecLoNames, nodeName );
        }

        //****************************************************************
        // Step 6: create "saved" register output
        //****************************************************************
        if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
        {
            loCreated++;
            pObjSavedLo = Aig_ObjCreateCi( pNew );
            Vec_PtrPush( vecLos, pObjSavedLo );
            nodeName = "SAVED_LO";
            Vec_PtrPush( vecLoNames, nodeName );
        }

        //****************************************************************
        // Step 7: create the OR gate and the AND gate directly fed by "SAVE" Pi
        //****************************************************************
        if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
        {
            pObjSaveOrSaved = Aig_Or( pNew, pObjSavePi, pObjSavedLo );
            pObjSaveAndNotSaved = Aig_And( pNew, pObjSavePi, Aig_Not(pObjSavedLo) );
        }

        //********************************************************************
        // Step 8: create internal nodes
        //********************************************************************
        Aig_ManForEachNode( p, pObj, i )
        {
            pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
        }

        
        //********************************************************************
        // Step 8.x : create PO for each safety assertions
        // NOTE : Here the output is purposely inverted as it will be thrown to 
        // dprove
        //********************************************************************
        assert( pNegatedSafetyConjunction == NULL );
        if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE)
        {
            if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) == 0 )
            {
                pObjAndAcc = Aig_ManConst1( pNew );
                Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
                {
                    pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
                    pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
                }
                pNegatedSafetyConjunction = Aig_Not(pObjAndAcc);
                if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
                    pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_Not(pObjAndAcc) );
            }
            else if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) != 0 )
            {
                pObjAndAcc = Aig_ManConst1( pNew );
                Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
                {
                    pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
                    pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
                }
                collectiveAssertSafety = pObjAndAcc;

                pObjAndAcc = Aig_ManConst1( pNew );
                Vec_PtrForEachEntry( Aig_Obj_t *, vAssumeSafety, pObj, i )
                {
                    pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
                    pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
                }
                collectiveAssumeSafety = pObjAndAcc;
                pNegatedSafetyConjunction =  Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety );
                if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
                    pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) );
            }
            else
            {
                printf("WARNING!! No safety property is found, a new (negated) constant 1 output is created\n");
                pNegatedSafetyConjunction = Aig_Not( Aig_ManConst1(pNew) );
                if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
                    pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_Not( Aig_ManConst1(pNew) ) );
            }
        }
        assert( pNegatedSafetyConjunction != NULL );

        //********************************************************************
        // Step 9: create the safety property output gate for the liveness properties
        // discuss with Sat/Alan for an alternative implementation
        //********************************************************************
        if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
        {
            vPoForLtlProps = Vec_PtrAlloc( Vec_PtrSize( vTopASTNodeArray ) );
            if( Vec_PtrSize( vTopASTNodeArray ) )
            {
                //no effective AST for any input LTL property
                //must do something graceful
            }
            for( i=0; i<Vec_PtrSize( vTopASTNodeArray ); i++ )
            {
                pObjSafetyPropertyOutput = Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
                Vec_PtrPush( vPoForLtlProps, pObjSafetyPropertyOutput );
            }
        }

        //*************************************************************************************
        // Step 10: Placeholder PO's were created for Liveness property outputs in the
        // last step. FYI, # of new liveness property outputs = # of LTL properties in the circuit
        // It is time for creation of loop LI's and other stuff
        // Now creating register inputs for the original flops
        //*************************************************************************************
        nRegCount = 0;
        
        Saig_ManForEachLo( p, pObj, i )
        {
            pMatch = Saig_ObjLoToLi( p, pObj );
            Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
            nRegCount++;
            liCopied++;
        }

        //*************************************************************************************
        // Step 11: create register input corresponding to the register "saved"
        //*************************************************************************************
        if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
        {
            #ifndef DUPLICATE_CKT_DEBUG
                pObjSavedLi = Aig_ObjCreateCo( pNew, pObjSaveOrSaved );
                nRegCount++;
                liCreated++;

                pObjAndAcc = Aig_ManConst1( pNew );

                //*************************************************************************************
                // Step 11: create the family of shadow registers, then create the cascade of Xnor 
                // and And gates for the comparator 
                //*************************************************************************************
                Saig_ManForEachLo( p, pObj, i )
                {
                //printf("\nKEMON RENDY = %s", Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i )) );
                //top|route0_target0_queue_with_credit0_queue0
                //top|route0_master0_queue2
                //  if( strcmp(  Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "top|route0_queue1_num[0]" ) == 0 
                //          || strcmp(  Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "top|route0_queue1_num[1]" ) == 0 || strcmp(  Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "top|route0_queue1_num[2]" ) == 0 )
                    {       
                        pObjShadowLo = Aig_ObjCreateCi( pNew );

                    #ifdef PROPAGATE_NAMES
                        Vec_PtrPush( vecLos, pObjShadowLo );
                        nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ) ) + 10 );
                        sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "SHADOW" );
                        
                        Vec_PtrPush( vecLoNames, nodeName );
                    #endif

                        pObjShadowLiDriver = Aig_Mux( pNew, pObjSaveAndNotSaved, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
                        pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
                        nRegCount++;
                        loCreated++; liCreated++;
            
                        pObjXor = Aig_Exor( pNew, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
                        pObjXnor = Aig_Not( pObjXor );
                    
                        pObjAndAcc = Aig_And( pNew, pObjXnor, pObjAndAcc );
                    }
                }

                // create the AND gate whose output will be the signal "looped"
                pObjSavedLoAndEquality = Aig_And( pNew, pObjSavedLo, pObjAndAcc );

                // create the master AND gate and corresponding AND and OR logic for the liveness properties
                
                //*************************************************************************************
                // Step 11: logic for LTL properties:- (looped & ~theta) where theta is the input ltl 
                // property
                // Description of some data-structure:
                //-------------------------------------------------------------------------------------
                // Name          | Type            | Purpose
                //-------------------------------------------------------------------------------------
                // vSignalMemory | Vec_Ptr_t *     | A vector across all ASTs of the LTL properties
                //               |                 | It remembers if OR+Latch for GF node has already been
                //               |                 | created for a particular signal.
                //               |                 |
                // vGFFlopMemory | Vec_Ptr_t *     | A vector across all ASTs of the LTL properties
                //               |                 | remembers if OR+Latch of a GF node has already been created
                //               |                 |
                // vSignal       | Vec_Ptr_t *     | vector for each AST; contains pointers from GF nodes
                //               |                 | to AIG signals
                //               |                 |
                // vAigGFMap     | Vec_Vec_t *     | vAigGFMap[ index ] = vector of GF nodes pointing to
                //               |                 | the same AIG node; "index" is the index of that
                //               |                 | AIG node in the vector vSignal
                //*************************************************************************************
                
                vSignalMemory = Vec_PtrAlloc(10);
                vGFFlopMemory = Vec_PtrAlloc(10);

                Vec_PtrForEachEntry( ltlNode *, vTopASTNodeArray, topNodeOfAST, iii )
                {
                                    vSignal = Vec_PtrAlloc( 10 );
                                    vAigGFMap = Vec_VecAlloc( 10 );
                                    
                                    //*************************************************************************************
                                    //Step 11a: for the current AST, find out the leaf level Boolean signal pointers from 
                                    // the NEW aig.
                                    //*************************************************************************************
                                    populateBoolWithAigNodePtr( pNtk, p, pNew, topNodeOfAST );
                                    assert( checkAllBoolHaveAIGPointer( topNodeOfAST ) );

                                    //*************************************************************************************
                                    //Step 11b: for each GF node, compute the pointer in AIG that it should point to
                                    // In particular, if the subtree below GF is some Boolean crown (including the case
                                    // of simple negation, create new logic and populate the AIG pointer in GF node
                                    // accordingly
                                    //*************************************************************************************
                                    populateAigPointerUnitGF( pNew, topNodeOfAST, vSignal, vAigGFMap );
                                    
                                    //*************************************************************************************
                                    //Step 11c: everything below GF are computed. Now, it is time to create logic for individual 
                                    // GF nodes (i.e. the OR gate and the latch and the Boolean crown of the AST
                                    //*************************************************************************************
                                    Vec_PtrForEachEntry( Aig_Obj_t *, vSignal, pObj, i )
                                    {
                                        //*********************************************************
                                        // Step 11c.1: if the OR+Latch of the particular signal is
                                        // not already created, create it. It may have already been 
                                        // created from another property, so check it before creation
                                        //*********************************************************
                                        if( Vec_PtrFind( vSignalMemory, pObj ) == -1 )
                                        {
                                            liveLatch++;

                                            pDriverImage = pObj;
                                            pObjShadowLo = Aig_ObjCreateCi( pNew );
                                            pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
                                            pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );

                                            nRegCount++;
                                            loCreated++; liCreated++;

                                            Vec_PtrPush( vSignalMemory, pObj );
                                            Vec_PtrPush( vGFFlopMemory, pObjShadowLo );

                                            #if 1
                                            #ifdef PROPAGATE_NAMES
                                                Vec_PtrPush( vecLos, pObjShadowLo );
                                                //nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 );
                                                //sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "LIVENESS" );
                                                nodeName = (char *)malloc( 20 );
                                                sprintf( nodeName, "n%d__%s", Aig_ObjId(pObjShadowLo), "GF_flop" );
                                                Vec_PtrPush( vecLoNames, nodeName );
                                            #endif
                                            #endif
                                        }
                                        else
                                            pObjShadowLo = (Aig_Obj_t *)Vec_PtrEntry( vGFFlopMemory, Vec_PtrFind( vSignalMemory, pObj ) );
                                                                                
                                        Vec_VecForEachEntryLevel( ltlNode *, vAigGFMap, pEnrtyGLOBALLY, ii, i )
                                            setAIGNodePtrOfGloballyNode( pEnrtyGLOBALLY, pObjShadowLo);
                                            

                                        //#ifdef PROPAGATE_NAMES
                                        //  Vec_PtrPush( vecLos, pObjShadowLo );
                                        //  nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 );
                                        //  sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "LIVENESS" );
                                        //  Vec_PtrPush( vecLoNames, nodeName );
                                        //#endif
                                        
                                    }
                                    
                                    //*********************************************************
                                    //Step 11c.2: creating the Boolean crown
                                    //*********************************************************
                                    buildLogicFromLTLNode( pNew, topNodeOfAST );

                                    //*********************************************************
                                    //Step 11c.3: creating logic for (looped & ~theta) and patching
                                    // it with the proper PO
                                    //Note: if ALLOW_SAFETY_PROPERTIES is defined then the final AND
                                    //gate is a conjunction of safety & liveness, i.e. SAFETY & (looped => theta)
                                    //since ABC convention demands a NOT gate at the end, the property logic 
                                    //becomes !( SAFETY & (looped => theta) ) = !SAFETY + (looped & !theta)
                                    //*********************************************************
                                    pObjLive = retriveAIGPointerFromLTLNode( topNodeOfAST );
                                    pObjSafetyGate = Aig_And( pNew, pObjSavedLoAndEquality, Aig_Not(pObjLive) );
                                    #ifdef ALLOW_SAFETY_PROPERTIES
                                        printf("liveness output is conjoined with safety assertions\n");
                                        pObjSafetyAndLiveToSafety = Aig_Or( pNew, pObjSafetyGate, pNegatedSafetyConjunction );
                                        pObjSafetyPropertyOutput = (Aig_Obj_t *)Vec_PtrEntry( vPoForLtlProps, iii );
                                        Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyAndLiveToSafety );
                                    #else
                                        pObjSafetyPropertyOutput = Vec_PtrEntry( vPoForLtlProps, iii );
                                        Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyGate );
                                    #endif
                                    //refreshing vSignal and vAigGFMap arrays
                                    Vec_PtrFree( vSignal );
                                    Vec_VecFree( vAigGFMap );
                }
                                
            #endif
        }
#endif

    Aig_ManSetRegNum( pNew, nRegCount );

    Aig_ManCiCleanupBiere( pNew );
    Aig_ManCoCleanupBiere( pNew );
    
    Aig_ManCleanup( pNew );
    
    assert( Aig_ManCheck( pNew ) );
    
    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
    {
            assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjCioId(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
            assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) );
            //assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch );
    }


    return pNew;
}

static int nodeName_starts_with ( Abc_Obj_t *  pNode, const char *  prefix  )

static

Definition at line 84 of file liveness.c.

{
    if( strstr( Abc_ObjName( pNode ), prefix ) == Abc_ObjName( pNode ) )
        return 1;
    else
        return 0;
}

ltlNode* parseFormulaCreateAST

(

char *

inputFormula

)

Definition at line 366 of file ltl_parser.c.

{
    ltlNode *temp;

    temp = readLtlFormula( inputFormula );
    //if( temp == NULL )
    //  printf("\nAST creation failed for formula %s", inputFormula );
    resetGlobalVar();
    return temp;
}

void populateAigPointerUnitGF	(	Aig_Man_t *	pAigNew,
		ltlNode *	topASTNode,
		Vec_Ptr_t *	vSignal,
		Vec_Vec_t *	vAigGFMap
	)

Definition at line 505 of file ltl_parser.c.

{
    ltlNode *nextNode, *nextToNextNode;
    int serialNumSignal;

    switch( topASTNode->type ){
        case AND:
        case OR:
        case IMPLY:
            populateAigPointerUnitGF( pAigNew, topASTNode->left, vSignal, vAigGFMap );
            populateAigPointerUnitGF( pAigNew, topASTNode->right, vSignal, vAigGFMap );
            return;
        case NOT:
            populateAigPointerUnitGF( pAigNew, topASTNode->left, vSignal, vAigGFMap );
            return;
        case GLOBALLY:
            nextNode = topASTNode->left;
            assert( nextNode->type = EVENTUALLY );
            nextToNextNode = nextNode->left;
            if( nextToNextNode->type == BOOL )
            {
                assert( nextToNextNode->pObj );
                serialNumSignal = Vec_PtrFind( vSignal, nextToNextNode->pObj );
                if( serialNumSignal == -1 )
                {                   
                    Vec_PtrPush( vSignal, nextToNextNode->pObj );
                    serialNumSignal = Vec_PtrFind( vSignal, nextToNextNode->pObj );
                }
                //Vec_PtrPush( vGLOBALLY, topASTNode );
                Vec_VecPush( vAigGFMap, serialNumSignal, topASTNode );
            }
            else
            {
                assert( nextToNextNode->pObj == NULL );
                buildLogicFromLTLNode_combinationalOnly( pAigNew, nextToNextNode );
                serialNumSignal = Vec_PtrFind( vSignal, nextToNextNode->pObj );
                if( serialNumSignal == -1 )
                {
                    Vec_PtrPush( vSignal, nextToNextNode->pObj );
                    serialNumSignal = Vec_PtrFind( vSignal, nextToNextNode->pObj );
                }
                //Vec_PtrPush( vGLOBALLY, topASTNode );
                Vec_VecPush( vAigGFMap, serialNumSignal, topASTNode );
            }
            return;
        case BOOL:
            return;
        default:
            printf("\nINVALID situation: aborting...\n");
            exit(0);
    }
}

void populateBoolWithAigNodePtr	(	Abc_Ntk_t *	pNtk,
		Aig_Man_t *	pAigOld,
		Aig_Man_t *	pAigNew,
		ltlNode *	topASTNode
	)

Definition at line 742 of file ltl_parser.c.

{
    char *targetName;
    Abc_Obj_t * pNode;
    int i;
    Aig_Obj_t *pObj, *pDriverImage;
    
    switch( topASTNode->type ){
        case BOOL:
            targetName = topASTNode->name;
            if( checkBooleanConstant( targetName ) == 1 )
            {
                topASTNode->pObj = Aig_ManConst1( pAigNew );
                return;
            }
            if( checkBooleanConstant( targetName ) == 0 )
            {
                topASTNode->pObj = Aig_Not(topASTNode->pObj = Aig_ManConst1( pAigNew ));
                return;
            }
            Abc_NtkForEachPo( pNtk, pNode, i )
                if( strcmp( Abc_ObjName( pNode ), targetName ) == 0 )
                {
                    pObj = Aig_ManCo( pAigOld, i );
                    assert( Aig_ObjIsCo( pObj ));
                    pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
                    topASTNode->pObj = pDriverImage;
                    return;
                }
            assert(0);
        case AND:
        case OR:
        case IMPLY:
        case UNTIL:
            assert( topASTNode->left != NULL );
            assert( topASTNode->right != NULL );
            populateBoolWithAigNodePtr( pNtk, pAigOld, pAigNew, topASTNode->left );
            populateBoolWithAigNodePtr( pNtk, pAigOld, pAigNew, topASTNode->right );
            return;
        case NOT:
        case NEXT:
        case GLOBALLY:
        case EVENTUALLY:
            assert( topASTNode->left != NULL );
            assert( topASTNode->right == NULL );
            populateBoolWithAigNodePtr( pNtk, pAigOld, pAigNew, topASTNode->left );
            return;
        default:
            printf("\nUNSUPPORTED LTL NODE TYPE:: Aborting execution\n");
            exit(0);
    }
}

Vec_Ptr_t* populateFairnessVector	(	Abc_Ntk_t *	pNtk,
		Aig_Man_t *	pAig
	)

Definition at line 1161 of file liveness.c.

{
    Abc_Obj_t * pNode;
    int i, fairCounter = 0;
    Vec_Ptr_t * vFair;

    vFair = Vec_PtrAlloc( 100 );
    Abc_NtkForEachPo( pNtk, pNode, i )
        //if( strstr( Abc_ObjName( pNode ), "assume_fair") != NULL )
        if( nodeName_starts_with( pNode, "assume_fair" ) )
        {
            Vec_PtrPush( vFair, Aig_ManCo( pAig, i ) );
            fairCounter++;
        }
    printf("Number of fairness property found = %d\n", fairCounter);
    return vFair;
}

Vec_Ptr_t* populateLivenessVector	(	Abc_Ntk_t *	pNtk,
		Aig_Man_t *	pAig
	)

Definition at line 1143 of file liveness.c.

{
    Abc_Obj_t * pNode;
    int i, liveCounter = 0;
    Vec_Ptr_t * vLive;

    vLive = Vec_PtrAlloc( 100 );
    Abc_NtkForEachPo( pNtk, pNode, i )
        //if( strstr( Abc_ObjName( pNode ), "assert_fair") != NULL )
        if( nodeName_starts_with( pNode, "assert_fair" ) )
        {
            Vec_PtrPush( vLive, Aig_ManCo( pAig, i ) );
            liveCounter++;
        }
    printf("Number of liveness property found = %d\n", liveCounter);
    return vLive;
}

Vec_Ptr_t* populateSafetyAssertionVector	(	Abc_Ntk_t *	pNtk,
		Aig_Man_t *	pAig
	)

Definition at line 1179 of file liveness.c.

{
    Abc_Obj_t * pNode;
    int i, assertSafetyCounter = 0;
    Vec_Ptr_t * vAssertSafety;

    vAssertSafety = Vec_PtrAlloc( 100 );
    Abc_NtkForEachPo( pNtk, pNode, i )
        //if( strstr( Abc_ObjName( pNode ), "Assert") != NULL )
        if( nodeName_starts_with( pNode, "assert_safety" ) || nodeName_starts_with( pNode, "Assert" ))
        {
            Vec_PtrPush( vAssertSafety, Aig_ManCo( pAig, i ) );
            assertSafetyCounter++;
        }
    printf("Number of safety property found = %d\n", assertSafetyCounter);
    return vAssertSafety;
}

Vec_Ptr_t* populateSafetyAssumptionVector	(	Abc_Ntk_t *	pNtk,
		Aig_Man_t *	pAig
	)

Definition at line 1197 of file liveness.c.

{
    Abc_Obj_t * pNode;
    int i, assumeSafetyCounter = 0;
    Vec_Ptr_t * vAssumeSafety;

    vAssumeSafety = Vec_PtrAlloc( 100 );
    Abc_NtkForEachPo( pNtk, pNode, i )
        //if( strstr( Abc_ObjName( pNode ), "Assert") != NULL )
        if( nodeName_starts_with( pNode, "assume_safety" ) || nodeName_starts_with( pNode, "Assume" ))
        {
            Vec_PtrPush( vAssumeSafety, Aig_ManCo( pAig, i ) );
            assumeSafetyCounter++;
        }
    printf("Number of assume_safety property found = %d\n", assumeSafetyCounter);
    return vAssumeSafety;
}

Vec_Int_t* prepareFlopVector	(	Aig_Man_t *	pAig,
		int	vectorLength
	)

Definition at line 1569 of file liveness.c.

{
    Vec_Int_t *vFlops;
    int i;

    vFlops = Vec_IntAlloc( vectorLength );

    for( i=0; i<vectorLength; i++ )
        Vec_IntPush( vFlops, i );

#if 0
    Vec_IntPush( vFlops, 19 );
    Vec_IntPush( vFlops, 20 );
    Vec_IntPush( vFlops, 23 );
    Vec_IntPush( vFlops, 24 );
    //Vec_IntPush( vFlops, 2 );
    //Vec_IntPush( vFlops, 3 );
    //Vec_IntPush( vFlops, 4 );
    //Vec_IntPush( vFlops, 5 );
    //Vec_IntPush( vFlops, 8 );
    //Vec_IntPush( vFlops, 9 );
    //Vec_IntPush( vFlops, 10 );
    //Vec_IntPush( vFlops, 11 );
    //Vec_IntPush( vFlops, 0 );
    //Vec_IntPush( vFlops, 0 );
#endif

    return vFlops;
}

void printVecPtrOfString

(

Vec_Ptr_t *

vec

)

Definition at line 92 of file liveness.c.

{
    int i;

    for( i=0; i< Vec_PtrSize( vec ); i++ )
    {
        printf("vec[%d] = %s\n", i, (char *)Vec_PtrEntry(vec, i) );
    }
}

ltlNode* readLtlFormula

(

char *

formula

)

Definition at line 137 of file ltl_parser.c.

{
    char ch;
    char *varName;
    int formulaLength, rememberEnd;
    int i = startOfSuffixString;
    ltlNode *curr_node, *temp_node_left, *temp_node_right;
    char prevChar;
    
    formulaLength = strlen( formula );
    if( isUnexpectedEOS( formula, startOfSuffixString ) )
    {
        printf("\nFAULTING POINT: formula = %s\nstartOfSuffixString = %d, formula[%d] = %c\n\n", formula, startOfSuffixString, startOfSuffixString - 1, formula[startOfSuffixString-1]);
        return NULL;
    }
            
    while( i < formulaLength )
    {
        ch = formula[i];

        switch(ch){
            case ' ':
            case '\n':
            case '\r':
            case '\t':
            case '\v':
            case '\f':
                        i++;
                        startOfSuffixString = i;
                        break;
            case ':':
                        i++;
                        if( !isTemporalOperator( formula, i ) )
                            return NULL;
                        startOfSuffixString = i;
                        break;
            case 'G':
                        prevChar = formula[i-1];
                        if( prevChar == ':' ) //i.e. 'G' is a temporal operator
                        {
                            i++;
                            startOfSuffixString = i;
                            temp_node_left = readLtlFormula( formula );
                            if( temp_node_left == NULL )
                                return NULL;
                            else
                            {
                                curr_node = generateTypedNode(GLOBALLY);
                                curr_node->left = temp_node_left;
                                return curr_node;
                            }
                        }
                        else    //i.e. 'G' must be starting a variable name
                        {
                            varName = getVarName( formula, i, &rememberEnd );
                            if( !varName )
                            {
                                printf("\nInvalid LTL formula: expecting valid variable name token...aborting" );
                                return NULL;
                            }
                            curr_node = generateTypedNode(BOOL);
                            curr_node->name = varName;
                            i = rememberEnd;
                            startOfSuffixString = i;
                            return curr_node;
                        }
            case 'F':
                        prevChar = formula[i-1];
                        if( prevChar == ':' ) //i.e. 'F' is a temporal operator
                        {
                            i++;
                            startOfSuffixString = i;
                            temp_node_left = readLtlFormula( formula );
                            if( temp_node_left == NULL )
                                return NULL;
                            else
                            {
                                curr_node = generateTypedNode(EVENTUALLY);
                                curr_node->left = temp_node_left;
                                return curr_node;
                            }
                        }
                        else //i.e. 'F' must be starting a variable name
                        {
                            varName = getVarName( formula, i, &rememberEnd );
                            if( !varName )
                            {
                                printf("\nInvalid LTL formula: expecting valid variable name token...aborting" );
                                return NULL;
                            }
                            curr_node = generateTypedNode(BOOL);
                            curr_node->name = varName;
                            i = rememberEnd;
                            startOfSuffixString = i;
                            return curr_node;
                        }   
            case 'X':
                        prevChar = formula[i-1];
                        if( prevChar == ':' ) //i.e. 'X' is a temporal operator
                        {
                            i++;
                            startOfSuffixString = i;
                            temp_node_left = readLtlFormula( formula );
                            if( temp_node_left == NULL )
                                return NULL;
                            else
                            {
                                curr_node = generateTypedNode(NEXT);
                                curr_node->left = temp_node_left;
                                return curr_node;
                            }
                        }
                        else //i.e. 'X' must be starting a variable name
                        {
                            varName = getVarName( formula, i, &rememberEnd );
                            if( !varName )
                            {
                                printf("\nInvalid LTL formula: expecting valid variable name token...aborting" );
                                return NULL;
                            }
                            curr_node = generateTypedNode(BOOL);
                            curr_node->name = varName;
                            i = rememberEnd;
                            startOfSuffixString = i;
                            return curr_node;
                        }   
            case 'U':
                        prevChar = formula[i-1];
                        if( prevChar == ':' ) //i.e. 'X' is a temporal operator
                        {
                            i++;
                            startOfSuffixString = i;
                            temp_node_left = readLtlFormula( formula );
                            if( temp_node_left == NULL )
                                return NULL;
                            temp_node_right = readLtlFormula( formula );
                            if( temp_node_right == NULL )
                            {
                                //need to do memory management: if right subtree is NULL then left
                                //subtree must be freed.
                                return NULL;
                            }
                            curr_node = generateTypedNode(UNTIL);
                            curr_node->left = temp_node_left;
                            curr_node->right = temp_node_right;
                            return curr_node;
                        }
                        else //i.e. 'U' must be starting a variable name
                        {
                            varName = getVarName( formula, i, &rememberEnd );
                            if( !varName )
                            {
                                printf("\nInvalid LTL formula: expecting valid variable name token...aborting" );
                                return NULL;
                            }
                            curr_node = generateTypedNode(BOOL);
                            curr_node->name = varName;
                            i = rememberEnd;
                            startOfSuffixString = i;
                            return curr_node;
                        }   
            case '+':
                        i++;
                        startOfSuffixString = i;
                        temp_node_left = readLtlFormula( formula );
                        if( temp_node_left == NULL )
                            return NULL;
                        temp_node_right = readLtlFormula( formula );
                        if( temp_node_right == NULL )
                        {
                            //need to do memory management: if right subtree is NULL then left
                            //subtree must be freed.
                            return NULL;
                        }
                        curr_node = generateTypedNode(OR);
                        curr_node->left = temp_node_left;
                        curr_node->right = temp_node_right;
                        return curr_node;
            case '&':
                        i++;
                        startOfSuffixString = i;
                        temp_node_left = readLtlFormula( formula );
                        if( temp_node_left == NULL )
                            return NULL;
                        temp_node_right = readLtlFormula( formula );
                        if( temp_node_right == NULL )
                        {
                            //need to do memory management: if right subtree is NULL then left
                            //subtree must be freed.
                            return NULL;
                        }
                        curr_node = generateTypedNode(AND);
                        curr_node->left = temp_node_left;
                        curr_node->right = temp_node_right;
                        return curr_node;
            case '!':
                        i++;
                        startOfSuffixString = i;
                        temp_node_left = readLtlFormula( formula );
                        if( temp_node_left == NULL )
                            return NULL;
                        else
                        {
                            curr_node = generateTypedNode(NOT);
                            curr_node->left = temp_node_left;
                            return curr_node;
                        }
            default:
                varName = getVarName( formula, i, &rememberEnd );
                if( !varName )
                {
                    printf("\nInvalid LTL formula: expecting valid variable name token...aborting" );
                    return NULL;
                }
                curr_node = generateTypedNode(BOOL);
                curr_node->name = varName;
                i = rememberEnd;
                startOfSuffixString = i;
                return curr_node;
        }
    }
    return NULL;
}

char* retrieveLOName	(	Abc_Ntk_t *	pNtkOld,
		Aig_Man_t *	pAigOld,
		Aig_Man_t *	pAigNew,
		Aig_Obj_t *	pObjPivot,
		Vec_Ptr_t *	vLive,
		Vec_Ptr_t *	vFair
	)

Definition at line 137 of file liveness.c.

{
    Aig_Obj_t *pObjOld, *pObj;
    Abc_Obj_t *pNode;
    int index, oldIndex, originalLatchNum = Saig_ManRegNum(pAigOld), strMatch, i;
    char *dummyStr = (char *)malloc( sizeof(char) * 50 );

    assert( Saig_ObjIsLo( pAigNew, pObjPivot ) );
    Saig_ManForEachLo( pAigNew, pObj, index )
        if( pObj == pObjPivot )
            break;
    if( index < originalLatchNum )
    {
        oldIndex = Saig_ManPiNum( pAigOld ) + index;
        pObjOld = Aig_ManCi( pAigOld, oldIndex );
        pNode = Abc_NtkCi( pNtkOld, oldIndex );
        assert( pObjOld->pData == pObjPivot );
        return Abc_ObjName( pNode );
    }
    else if( index == originalLatchNum )
        return "SAVED_LO";
    else if( index > originalLatchNum && index < 2 * originalLatchNum + 1 )
    {
        oldIndex = Saig_ManPiNum( pAigOld ) + index - originalLatchNum - 1;
        pObjOld = Aig_ManCi( pAigOld, oldIndex );
        pNode = Abc_NtkCi( pNtkOld, oldIndex );
        sprintf( dummyStr, "%s__%s", Abc_ObjName( pNode ), "SHADOW");
        return dummyStr;
    }
    else if( index >= 2 * originalLatchNum + 1 && index < 2 * originalLatchNum + 1 + Vec_PtrSize( vLive ) )
    {
        oldIndex = index - 2 * originalLatchNum - 1;
        strMatch = 0;
        dummyStr[0] = '\0';
        Saig_ManForEachPo( pAigOld, pObj, i )
        {
            pNode = Abc_NtkPo( pNtkOld, i );
            //if( strstr( Abc_ObjName( pNode ), "assert_fair" ) != NULL )
            if( nodeName_starts_with( pNode, "assert_fair" ) )
            {
                if( strMatch == oldIndex )
                {
                    sprintf( dummyStr, "%s__%s", Abc_ObjName( pNode ), "LIVENESS");
                    //return dummyStr;
                    break;
                }
                else
                    strMatch++;
            }
        }
        assert( dummyStr[0] != '\0' );
        return dummyStr;
    }
    else if( index >= 2 * originalLatchNum + 1 + Vec_PtrSize( vLive ) && index < 2 * originalLatchNum + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) )
    {
        oldIndex = index - 2 * originalLatchNum - 1 - Vec_PtrSize( vLive );
        strMatch = 0;
        dummyStr[0] = '\0';
        Saig_ManForEachPo( pAigOld, pObj, i )
        {
            pNode = Abc_NtkPo( pNtkOld, i );
            //if( strstr( Abc_ObjName( pNode ), "assume_fair" ) != NULL )
            if( nodeName_starts_with( pNode, "assume_fair" ) )
            {
                if( strMatch == oldIndex )
                {
                    sprintf( dummyStr, "%s__%s", Abc_ObjName( pNode ), "FAIRNESS");
                    //return dummyStr;
                    break;
                }
                else
                    strMatch++;
            }
        }
        assert( dummyStr[0] != '\0' );
        return dummyStr;
    }
    else
        return "UNKNOWN";
}

char* retrieveTruePiName	(	Abc_Ntk_t *	pNtkOld,
		Aig_Man_t *	pAigOld,
		Aig_Man_t *	pAigNew,
		Aig_Obj_t *	pObjPivot
	)

Definition at line 115 of file liveness.c.

{
    Aig_Obj_t *pObjOld, *pObj;
    Abc_Obj_t *pNode;
    int index;

    assert( Saig_ObjIsPi( pAigNew, pObjPivot ) );
    Aig_ManForEachCi( pAigNew, pObj, index )
        if( pObj == pObjPivot )
            break;
    assert( index < Aig_ManCiNum( pAigNew ) - Aig_ManRegNum( pAigNew ) );
    if( index == Saig_ManPiNum( pAigNew ) - 1 )
        return "SAVE_BIERE";
    else
    {
        pObjOld = Aig_ManCi( pAigOld, index );
        pNode = Abc_NtkPi( pNtkOld, index );
        assert( pObjOld->pData == pObjPivot );
        return Abc_ObjName( pNode );
    }
}

Aig_Obj_t* retriveAIGPointerFromLTLNode

(

ltlNode *

astNode

)

Definition at line 833 of file ltl_parser.c.

{
    return astNode->pObj;
}

void setAIGNodePtrOfGloballyNode	(	ltlNode *	astNode,
		Aig_Obj_t *	pObjLo
	)

Definition at line 828 of file ltl_parser.c.

{
    astNode->pObj = pObjLo;
}

void traverseAbstractSyntaxTree

(

ltlNode *

node

)

Definition at line 377 of file ltl_parser.c.

{
    switch(node->type){
        case( AND ):
            printf("& ");
            assert( node->left != NULL );
            assert( node->right != NULL );
            traverseAbstractSyntaxTree( node->left );
            traverseAbstractSyntaxTree( node->right );
            return;
        case( OR ):
            printf("+ ");
            assert( node->left != NULL );
            assert( node->right != NULL );
            traverseAbstractSyntaxTree( node->left );
            traverseAbstractSyntaxTree( node->right );
            return;
        case( NOT ):
            printf("~ ");
            assert( node->left != NULL );
            traverseAbstractSyntaxTree( node->left );
            assert( node->right == NULL );
            return;
        case( GLOBALLY ):
            printf("G ");
            assert( node->left != NULL );
            traverseAbstractSyntaxTree( node->left );
            assert( node->right == NULL );
            return;
        case( EVENTUALLY ):
            printf("F ");
            assert( node->left != NULL );
            traverseAbstractSyntaxTree( node->left );
            assert( node->right == NULL );
            return;
        case( NEXT ):
            printf("X ");
            assert( node->left != NULL );
            traverseAbstractSyntaxTree( node->left );
            assert( node->right == NULL );
            return;
        case( UNTIL ):
            printf("U ");
            assert( node->left != NULL );
            assert( node->right != NULL );
            traverseAbstractSyntaxTree( node->left );
            traverseAbstractSyntaxTree( node->right );
            return;
        case( BOOL ):
            printf("%s ", node->name);
            assert( node->left == NULL );
            assert( node->right == NULL );
            return;
        default:
            printf("\nUnsupported token type: Exiting execution\n");
            exit(0);
    }
}

void traverseAbstractSyntaxTree_postFix

(

ltlNode *

node

)

Definition at line 436 of file ltl_parser.c.

{
    switch(node->type){
        case( AND ):
            printf("( ");
            assert( node->left != NULL );
            assert( node->right != NULL );
            traverseAbstractSyntaxTree_postFix( node->left );
            printf("& ");
            traverseAbstractSyntaxTree_postFix( node->right );
            printf(") ");
            return;
        case( OR ):
            printf("( ");
            assert( node->left != NULL );
            assert( node->right != NULL );
            traverseAbstractSyntaxTree_postFix( node->left );
            printf("+ ");
            traverseAbstractSyntaxTree_postFix( node->right );
            printf(") ");
            return;
        case( NOT ):
            printf("~ ");
            assert( node->left != NULL );
            traverseAbstractSyntaxTree_postFix( node->left );
            assert( node->right == NULL );
            return;
        case( GLOBALLY ):
            printf("G ");
            //printf("( ");
            assert( node->left != NULL );
            traverseAbstractSyntaxTree_postFix( node->left );
            assert( node->right == NULL );
            //printf(") ");
            return;
        case( EVENTUALLY ):
            printf("F ");
            //printf("( ");
            assert( node->left != NULL );
            traverseAbstractSyntaxTree_postFix( node->left );
            assert( node->right == NULL );
            //printf(") ");
            return;
        case( NEXT ):
            printf("X ");
            assert( node->left != NULL );
            traverseAbstractSyntaxTree_postFix( node->left );
            assert( node->right == NULL );
            return;
        case( UNTIL ):
            printf("( ");
            assert( node->left != NULL );
            assert( node->right != NULL );
            traverseAbstractSyntaxTree_postFix( node->left );
            printf("U ");
            traverseAbstractSyntaxTree_postFix( node->right );
            printf(") ");
            return;
        case( BOOL ):
            printf("%s ", node->name);
            assert( node->left == NULL );
            assert( node->right == NULL );
            return;
        default:
            printf("\nUnsupported token type: Exiting execution\n");
            exit(0);
    }
}

void updateNewNetworkNameManager	(	Abc_Ntk_t *	pNtk,
		Aig_Man_t *	pAig,
		Vec_Ptr_t *	vPiNames,
		Vec_Ptr_t *	vLoNames
	)

Definition at line 1215 of file liveness.c.

{
    Aig_Obj_t *pObj;
    Abc_Obj_t *pNode;
    int i, ntkObjId;

    pNtk->pManName = Nm_ManCreate( Abc_NtkCiNum( pNtk ) );

    if( vPiNames )
    {
        Saig_ManForEachPi( pAig, pObj, i )
        {
            ntkObjId = Abc_NtkCi( pNtk, i )->Id;
            //printf("Pi %d, Saved Name = %s, id = %d\n", i, Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), Vec_PtrEntry(vPiNames, i), NULL ), ntkObjId);  
            Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), (char *)Vec_PtrEntry(vPiNames, i), NULL );
        }
    }
    if( vLoNames )
    {
        Saig_ManForEachLo( pAig, pObj, i )
        {
            ntkObjId = Abc_NtkCi( pNtk, Saig_ManPiNum( pAig ) + i )->Id;
            //printf("Lo %d, Saved name = %s, id = %d\n", i, Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), Vec_PtrEntry(vLoNames, i), NULL ), ntkObjId);  
            Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), (char *)Vec_PtrEntry(vLoNames, i), NULL );
        }
    }

    Abc_NtkForEachPo(pNtk, pNode, i)
    {
        Abc_ObjAssignName(pNode, "assert_safety_", Abc_ObjName(pNode) );
    }

    // assign latch input names
    Abc_NtkForEachLatch(pNtk, pNode, i)
        if ( Nm_ManFindNameById(pNtk->pManName, Abc_ObjFanin0(pNode)->Id) == NULL )
            Abc_ObjAssignName( Abc_ObjFanin0(pNode), Abc_ObjName(Abc_ObjFanin0(pNode)), NULL );
}

Variable Documentation

Vec_Ptr_t * vecLoNames

Definition at line 219 of file liveness.c.

Vec_Ptr_t* vecLos

Definition at line 219 of file liveness.c.

Vec_Ptr_t * vecPiNames

Definition at line 218 of file liveness.c.

Vec_Ptr_t* vecPis

Definition at line 218 of file liveness.c.