#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"
#include "proof/pdr/pdr.h"
#include <time.h>

Macros
#define	SIMPLE_kCS 0

#define	kCS_WITH_SAFETY_INVARIANTS 1

#define	kCS_WITH_DISCOVER_MONOTONE_SIGNALS 2

#define	kCS_WITH_SAFETY_AND_DCS_INVARIANTS 3

#define	kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS 4

Functions
ABC_NAMESPACE_IMPL_START Aig_Man_t *	Abc_NtkToDar (Abc_Ntk_t *pNtk, int fExors, int fRegisters)
	DECLARATIONS ///. More...

Abc_Ntk_t *	Abc_NtkFromAigPhase (Aig_Man_t *pMan)

Abc_Ntk_t *	Abc_NtkMakeOnePo (Abc_Ntk_t *pNtk, int Output, int nRange)

void	Aig_ManDumpBlif (Aig_Man_t p, char pFileName, Vec_Ptr_t vPiNames, Vec_Ptr_t vPoNames)

Aig_Man_t *	generateWorkingAig (Aig_Man_t pAig, Abc_Ntk_t pNtk, int *pIndex0Live)

Aig_Man_t *	generateWorkingAigWithDSC (Aig_Man_t pAig, Abc_Ntk_t pNtk, int pIndex0Live, Vec_Ptr_t vMasterBarriers)

Vec_Ptr_t *	findDisjunctiveMonotoneSignals (Abc_Ntk_t *pNtk)

Vec_Int_t *	createSingletonIntVector (int i)

Aig_Man_t *	generateDisjunctiveTester (Abc_Ntk_t pNtk, Aig_Man_t pAig, int combN, int combK)

Aig_Man_t *	generateGeneralDisjunctiveTester (Abc_Ntk_t pNtk, Aig_Man_t pAig, int combK)

Aig_Obj_t *	readLiveSignal_0 (Aig_Man_t *pAig, int liveIndex_0)

Aig_Obj_t *	readLiveSignal_k (Aig_Man_t *pAig, int liveIndex_k)

Aig_Man_t *	introduceAbsorberLogic (Aig_Man_t pAig, int pLiveIndex_0, int *pLiveIndex_k, int nonFirstIteration)

void	modifyAigToApplySafetyInvar (Aig_Man_t *pAig, int csTarget, int safetyInvarPO)

int	flipConePdr (Aig_Man_t *pAig, int directive, int targetCSPropertyIndex, int safetyInvariantPOIndex, int absorberCount)

int	collectSafetyInvariantPOIndex (Abc_Ntk_t *pNtk)

Vec_Ptr_t *	collectUserGivenDisjunctiveMonotoneSignals (Abc_Ntk_t *pNtk)

void	deallocateMasterBarrierDisjunctInt (Vec_Ptr_t *vMasterBarrierDisjunctsArg)

void	deallocateMasterBarrierDisjunctVecPtrVecInt (Vec_Ptr_t *vMasterBarrierDisjunctsArg)

Vec_Ptr_t *	getVecOfVecFairness (FILE *fp)

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

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

Macro Definition Documentation

#define kCS_WITH_DISCOVER_MONOTONE_SIGNALS 2

Definition at line 59 of file kliveness.c.

#define kCS_WITH_SAFETY_AND_DCS_INVARIANTS 3

Definition at line 60 of file kliveness.c.

#define kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS 4

Definition at line 61 of file kliveness.c.

#define kCS_WITH_SAFETY_INVARIANTS 1

Definition at line 58 of file kliveness.c.

#define SIMPLE_kCS 0

Definition at line 57 of file kliveness.c.

Function Documentation

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

Definition at line 525 of file kliveness.c.

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

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

Definition at line 718 of file kliveness.c.

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

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

Abc_Ntk_t* Abc_NtkMakeOnePo	(	Abc_Ntk_t *	pNtkInit,
		int	Output,
		int	nRange
	)

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

Synopsis [Removes all POs, except one.]

Description []

SideEffects []

SeeAlso []

Definition at line 1590 of file abcNtk.c.

 {
     Abc_Ntk_t * pNtk;
     Vec_Ptr_t * vPosLeft;
     Vec_Ptr_t * vCosLeft;
     Abc_Obj_t * pNodePo;
     int i;
     assert( !Abc_NtkIsNetlist(pNtkInit) );
     assert( Abc_NtkHasOnlyLatchBoxes(pNtkInit) );
     if ( Output < 0 || Output >= Abc_NtkPoNum(pNtkInit) )
     {
         printf( "PO index is incorrect.\n" );
         return NULL;
     }
 
     pNtk = Abc_NtkDup( pNtkInit );
     if ( Abc_NtkPoNum(pNtk) == 1 )
         return pNtk;
 
     if ( nRange < 1 )
         nRange = 1;
 
     // filter POs
     vPosLeft = Vec_PtrAlloc( nRange );
     Abc_NtkForEachPo( pNtk, pNodePo, i )
         if ( i < Output || i >= Output + nRange )
             Abc_NtkDeleteObjPo( pNodePo );
         else
             Vec_PtrPush( vPosLeft, pNodePo );
     // filter COs
     vCosLeft = Vec_PtrDup( vPosLeft );
     for ( i = Abc_NtkPoNum(pNtk); i < Abc_NtkCoNum(pNtk); i++ )
         Vec_PtrPush( vCosLeft, Abc_NtkCo(pNtk, i) );
     // update arrays
     Vec_PtrFree( pNtk->vPos );  pNtk->vPos = vPosLeft;
     Vec_PtrFree( pNtk->vCos );  pNtk->vCos = vCosLeft;
 
     // clean the network
     if ( Abc_NtkIsStrash(pNtk) )
     {
         Abc_AigCleanup( (Abc_Aig_t *)pNtk->pManFunc );
         printf( "Run sequential cleanup (\"scl\") to get rid of dangling logic.\n" );
     }
     else
     {
         printf( "Run sequential cleanup (\"st; scl\") to get rid of dangling logic.\n" );
     }
 
     if ( !Abc_NtkCheck( pNtk ) )
         fprintf( stdout, "Abc_NtkMakeComb(): Network check has failed.\n" );
     return pNtk;
 }

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

DECLARATIONS ///.

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

FileName [kliveness.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Liveness property checking.]

Synopsis [Main implementation module of the algorithm k-Liveness ] [invented by Koen Claessen, Niklas Sorensson. Implements] [the code for 'kcs'. 'kcs' pre-processes based on switch] [and then runs the (absorber circuit >> pdr) loop ]

Author [Sayak Ray]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - October 31, 2012.]

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

void Aig_ManDumpBlif	(	Aig_Man_t *	p,
		char *	pFileName,
		Vec_Ptr_t *	vPiNames,
		Vec_Ptr_t *	vPoNames
	)

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

Synopsis [Writes the AIG into a BLIF file.]

Description []

SideEffects []

SeeAlso []

Definition at line 733 of file aigUtil.c.

 {
     FILE * pFile;
     Vec_Ptr_t * vNodes;
     Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pConst1 = NULL;
     int i, nDigits, Counter = 0;
     if ( Aig_ManCoNum(p) == 0 )
     {
         printf( "Aig_ManDumpBlif(): AIG manager does not have POs.\n" );
         return;
     }
     // check if constant is used
     Aig_ManForEachCo( p, pObj, i )
         if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
             pConst1 = Aig_ManConst1(p);
     // collect nodes in the DFS order
     vNodes = Aig_ManDfs( p, 1 );
     // assign IDs to objects
     Aig_ManConst1(p)->iData = Counter++;
     Aig_ManForEachCi( p, pObj, i )
         pObj->iData = Counter++;
     Aig_ManForEachCo( p, pObj, i )
         pObj->iData = Counter++;
     Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
         pObj->iData = Counter++;
     nDigits = Abc_Base10Log( Counter );
     // write the file 
     pFile = fopen( pFileName, "w" );
     fprintf( pFile, "# BLIF file written by procedure Aig_ManDumpBlif()\n" );
 //    fprintf( pFile, "# http://www.eecs.berkeley.edu/~alanmi/abc/\n" );
     fprintf( pFile, ".model %s\n", p->pName );
     // write PIs
     fprintf( pFile, ".inputs" );
     Aig_ManForEachPiSeq( p, pObj, i )
         if ( vPiNames )
             fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, i) );
         else
             fprintf( pFile, " n%0*d", nDigits, pObj->iData );
     fprintf( pFile, "\n" );
     // write POs
     fprintf( pFile, ".outputs" );
     Aig_ManForEachPoSeq( p, pObj, i )
         if ( vPoNames )
             fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPoNames, i) );
         else
             fprintf( pFile, " n%0*d", nDigits, pObj->iData );
     fprintf( pFile, "\n" );
     // write latches
     if ( Aig_ManRegNum(p) )
     {
         fprintf( pFile, "\n" );
         Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
         {
             fprintf( pFile, ".latch" );
             if ( vPoNames )
                 fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPoNames, Aig_ManCoNum(p)-Aig_ManRegNum(p)+i) );
             else
                 fprintf( pFile, " n%0*d", nDigits, pObjLi->iData );
             if ( vPiNames )
                 fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ManCiNum(p)-Aig_ManRegNum(p)+i) );
             else
                 fprintf( pFile, " n%0*d", nDigits, pObjLo->iData );
             fprintf( pFile, " 0\n" );
         }
         fprintf( pFile, "\n" );
     } 
     // write nodes
     if ( pConst1 )
         fprintf( pFile, ".names n%0*d\n 1\n", nDigits, pConst1->iData );
     Aig_ManSetCioIds( p );
     Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
     {
         fprintf( pFile, ".names" );
         if ( vPiNames && Aig_ObjIsCi(Aig_ObjFanin0(pObj)) )
             fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ObjCioId(Aig_ObjFanin0(pObj))) );
         else
             fprintf( pFile, " n%0*d", nDigits, Aig_ObjFanin0(pObj)->iData );
         if ( vPiNames && Aig_ObjIsCi(Aig_ObjFanin1(pObj)) )
             fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ObjCioId(Aig_ObjFanin1(pObj))) );
         else
             fprintf( pFile, " n%0*d", nDigits, Aig_ObjFanin1(pObj)->iData );
         fprintf( pFile, " n%0*d\n", nDigits, pObj->iData );
         fprintf( pFile, "%d%d 1\n", !Aig_ObjFaninC0(pObj), !Aig_ObjFaninC1(pObj) );
     }
     // write POs
     Aig_ManForEachCo( p, pObj, i )
     {
         fprintf( pFile, ".names" );
         if ( vPiNames && Aig_ObjIsCi(Aig_ObjFanin0(pObj)) )
             fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ObjCioId(Aig_ObjFanin0(pObj))) );
         else
             fprintf( pFile, " n%0*d", nDigits, Aig_ObjFanin0(pObj)->iData );
         if ( vPoNames )
             fprintf( pFile, " %s\n", (char*)Vec_PtrEntry(vPoNames, Aig_ObjCioId(pObj)) );
         else
             fprintf( pFile, " n%0*d\n", nDigits, pObj->iData );
         fprintf( pFile, "%d 1\n", !Aig_ObjFaninC0(pObj) );
     }
     Aig_ManCleanCioIds( p );
     fprintf( pFile, ".end\n\n" );
     fclose( pFile );
     Vec_PtrFree( vNodes );
 }

int collectSafetyInvariantPOIndex ( Abc_Ntk_t * pNtk )

Definition at line 425 of file kliveness.c.

 {
     Abc_Obj_t *pObj;
     int i;
 
     Abc_NtkForEachPo( pNtk, pObj, i )
     {
         if( strstr( Abc_ObjName( pObj ), "csSafetyInvar_" ) != NULL )
             return i;
     }       
 
     return -1;
 }

Vec_Ptr_t* collectUserGivenDisjunctiveMonotoneSignals ( Abc_Ntk_t * pNtk )

Definition at line 439 of file kliveness.c.

 {
     Abc_Obj_t *pObj;
     int i;
     Vec_Ptr_t *monotoneVector;
     Vec_Int_t *newIntVector;
 
     monotoneVector = Vec_PtrAlloc(0);   
     Abc_NtkForEachPo( pNtk, pObj, i )
     {
         if( strstr( Abc_ObjName( pObj ), "csLevel1Stabil_" ) != NULL )
         {
             newIntVector = createSingletonIntVector(i);
             Vec_PtrPush(monotoneVector, newIntVector);
         }
     }
 
     if( Vec_PtrSize(monotoneVector) > 0 )
         return monotoneVector;
     else
         return NULL;
 
 }

Vec_Int_t* createSingletonIntVector ( int i )

Definition at line 380 of file disjunctiveMonotone.c.

 {
     Vec_Int_t *myVec = Vec_IntAlloc(1);
     
     Vec_IntPush(myVec, iElem);
     return myVec;
 }

void deallocateMasterBarrierDisjunctInt ( Vec_Ptr_t * vMasterBarrierDisjunctsArg )

Definition at line 463 of file kliveness.c.

 {
     Vec_Int_t *vInt;
     int i;
 
     if(vMasterBarrierDisjunctsArg)
     {
         Vec_PtrForEachEntry(Vec_Int_t *, vMasterBarrierDisjunctsArg, vInt, i)
         {   
             Vec_IntFree(vInt);
         }
         Vec_PtrFree(vMasterBarrierDisjunctsArg);
     }
 }

void deallocateMasterBarrierDisjunctVecPtrVecInt ( Vec_Ptr_t * vMasterBarrierDisjunctsArg )

Definition at line 478 of file kliveness.c.

 {
     Vec_Int_t *vInt;
     Vec_Ptr_t *vPtr;
     int i, j, k, iElem;
 
     if(vMasterBarrierDisjunctsArg)
     {
         Vec_PtrForEachEntry(Vec_Ptr_t *, vMasterBarrierDisjunctsArg, vPtr, i)
         {   
             assert(vPtr);
             Vec_PtrForEachEntry( Vec_Int_t *, vPtr, vInt, j )
             {
                 //Vec_IntFree(vInt);
                 Vec_IntForEachEntry( vInt, iElem, k )
                     printf("%d - ", iElem);
                 //printf("Chung Chang j = %d\n", j);
             }
             Vec_PtrFree(vPtr);
         }
         Vec_PtrFree(vMasterBarrierDisjunctsArg);
     }
 }

Vec_Ptr_t* findDisjunctiveMonotoneSignals ( Abc_Ntk_t * pNtk )

Definition at line 596 of file disjunctiveMonotone.c.

 {
     Aig_Man_t *pAig;
     Vec_Int_t *vCandidateMonotoneSignals;
     Vec_Int_t *vKnownMonotoneSignals;
     //Vec_Int_t *vKnownMonotoneSignalsRoundTwo;
     //Vec_Int_t *vOldConsequentVector;
     //Vec_Int_t *vRemainingConsecVector;
     int i;
     int iElem;
     int pendingSignalIndex;
     Abc_Ntk_t *pNtkTemp;
     int hintSingalBeginningMarker;
     int hintSingalEndMarker;
     struct aigPoIndices *aigPoIndicesInstance;
     //struct monotoneVectorsStruct *monotoneVectorsInstance;
     struct antecedentConsequentVectorsStruct *anteConsecInstance;
     //Aig_Obj_t *safetyDriverNew;
     Vec_Int_t *newIntVec;
     Vec_Ptr_t *levelOneMonotne, *levelTwoMonotne;
     //Vec_Ptr_t *levelThreeMonotne;
 
     Vec_Ptr_t *vMasterDisjunctions;
 
     extern int findPendingSignal(Abc_Ntk_t *pNtk);
     extern Vec_Int_t *findHintOutputs(Abc_Ntk_t *pNtk); 
     extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
 
     //system("rm monotone.dat");
     
     /*******************************************/   
     //Finding the PO index of the pending signal 
     /*******************************************/   
     pendingSignalIndex = findPendingSignal(pNtk);
     if( pendingSignalIndex == -1 )
     {
         printf("\nNo Pending Signal Found\n");
         return NULL;
     }
     //else
         //printf("Po[%d] = %s\n", pendingSignalIndex, Abc_ObjName( Abc_NtkPo(pNtk, pendingSignalIndex) ) );
 
     /*******************************************/   
     //Finding the PO indices of all hint signals
     /*******************************************/   
     vCandidateMonotoneSignals = findHintOutputs(pNtk);
     if( vCandidateMonotoneSignals == NULL )
         return NULL;
     else
     {
         //Vec_IntForEachEntry( vCandidateMonotoneSignals, iElem, i )
         //  printf("Po[%d] = %s\n", iElem, Abc_ObjName( Abc_NtkPo(pNtk, iElem) ) );
         hintSingalBeginningMarker = Vec_IntEntry( vCandidateMonotoneSignals, 0 );
         hintSingalEndMarker = Vec_IntEntry( vCandidateMonotoneSignals, Vec_IntSize(vCandidateMonotoneSignals) - 1 );
     }
 
     /**********************************************/
     //Allocating "struct" with necessary parameters
     /**********************************************/
     aigPoIndicesInstance = allocAigPoIndices();
     aigPoIndicesInstance->attrPendingSignalIndex = pendingSignalIndex;
     aigPoIndicesInstance->attrHintSingalBeginningMarker = hintSingalBeginningMarker;
     aigPoIndicesInstance->attrHintSingalEndMarker = hintSingalEndMarker;
     aigPoIndicesInstance->attrSafetyInvarIndex = collectSafetyInvariantPOIndex(pNtk);
 
     /****************************************************/
     //Allocating "struct" with necessary monotone vectors
     /****************************************************/
     anteConsecInstance = allocAntecedentConsequentVectorsStruct();
     anteConsecInstance->attrAntecedents = NULL;
     anteConsecInstance->attrConsequentCandidates = vCandidateMonotoneSignals;
 
     /*******************************************/   
     //Generate AIG from Ntk
     /*******************************************/   
     if( !Abc_NtkIsStrash( pNtk ) )
     {
         pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
         pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
     }
     else
     {
         pAig = Abc_NtkToDar( pNtk, 0, 1 );
         pNtkTemp = pNtk;
     }
 
     /*******************************************/   
     //finding LEVEL 1 monotone signals
     /*******************************************/   
     //printf("Calling target function outside loop\n");
     vKnownMonotoneSignals = findNewDisjunctiveMonotone( pAig, aigPoIndicesInstance, anteConsecInstance );
     levelOneMonotne = Vec_PtrAlloc(0);
     Vec_IntForEachEntry( vKnownMonotoneSignals, iElem, i )
     {
         newIntVec = createSingletonIntVector( iElem );
         Vec_PtrPush( levelOneMonotne, newIntVec );
         //printf("Monotone Po[%d] = %s\n", iElem, Abc_ObjName( Abc_NtkPo(pNtk, iElem) ) );
     }
     //printAllIntVectors( levelOneMonotne, pNtk, "monotone.dat" );
 
     vMasterDisjunctions = Vec_PtrAlloc( Vec_PtrSize( levelOneMonotne ));
     appendVecToMasterVecInt(vMasterDisjunctions, levelOneMonotne );
 
     /*******************************************/   
     //finding LEVEL >1 monotone signals
     /*******************************************/   
     #if 0
     if( vKnownMonotoneSignals )
     {
         Vec_IntForEachEntry( vKnownMonotoneSignals, iElem, i )
         {
             printf("\n**************************************************************\n");
             printf("Exploring Second Layer : Reference Po[%d] = %s", iElem, Abc_ObjName( Abc_NtkPo(pNtk, iElem) ));
             printf("\n**************************************************************\n");
             anteConsecInstance->attrAntecedents = createSingletonIntVector( iElem );
             vOldConsequentVector = anteConsecInstance->attrConsequentCandidates;
             vRemainingConsecVector = updateAnteConseVectors(anteConsecInstance);
             if( anteConsecInstance->attrConsequentCandidates != vRemainingConsecVector )
             {
                 anteConsecInstance->attrConsequentCandidates = vRemainingConsecVector;
             }
             vKnownMonotoneSignalsRoundTwo = findNewDisjunctiveMonotone( pAig, aigPoIndicesInstance, anteConsecInstance );
             Vec_IntForEachEntry( vKnownMonotoneSignalsRoundTwo, iElemTwo, iTwo )
             {
                 printf("Monotone Po[%d] = %s, (%d, %d)\n", iElemTwo, Abc_ObjName( Abc_NtkPo(pNtk, iElemTwo) ), iElem, iElemTwo );
             }
             Vec_IntFree(vKnownMonotoneSignalsRoundTwo);
             Vec_IntFree(anteConsecInstance->attrAntecedents);
             if(anteConsecInstance->attrConsequentCandidates != vOldConsequentVector)
             {
                 Vec_IntFree(anteConsecInstance->attrConsequentCandidates);
                 anteConsecInstance->attrConsequentCandidates = vOldConsequentVector;
             }
         }
     }
     #endif 
 
 #if 1
     levelTwoMonotne = findNextLevelDisjunctiveMonotone( pAig, aigPoIndicesInstance, anteConsecInstance, levelOneMonotne );
     //printAllIntVectors( levelTwoMonotne, pNtk, "monotone.dat" );
     appendVecToMasterVecInt(vMasterDisjunctions, levelTwoMonotne );
 #endif
 
     //levelThreeMonotne = findNextLevelDisjunctiveMonotone( pAig, aigPoIndicesInstance, anteConsecInstance, levelTwoMonotne );
     //printAllIntVectors( levelThreeMonotne );
     //printAllIntVectors( levelTwoMonotne, pNtk, "monotone.dat" );
     //appendVecToMasterVecInt(vMasterDisjunctions, levelThreeMonotne );
 
     deallocAigPoIndices(aigPoIndicesInstance);
     deallocAntecedentConsequentVectorsStruct(anteConsecInstance);
     //deallocPointersToMonotoneVectors(monotoneVectorsInstance);
 
     deallocateVecOfIntVec( levelOneMonotne );
     deallocateVecOfIntVec( levelTwoMonotne );
 
     Aig_ManStop(pAig);
     Vec_IntFree(vKnownMonotoneSignals);
 
     return vMasterDisjunctions;
 }

int flipConePdr	(	Aig_Man_t *	pAig,
		int	directive,
		int	targetCSPropertyIndex,
		int	safetyInvariantPOIndex,
		int	absorberCount
	)

Definition at line 341 of file kliveness.c.

 {
     int RetValue, i;
     Aig_Obj_t *pObjTargetPo;
     Aig_Man_t *pAigDupl;
     Pdr_Par_t Pars, * pPars = &Pars;
     Abc_Cex_t * pCex = NULL;
 
     char *fileName;
     
     fileName = (char *)malloc(sizeof(char) * 50);
     sprintf(fileName, "%s_%d.%s", "kLive", absorberCount, "blif" );
 
     if( directive == kCS_WITH_SAFETY_INVARIANTS || directive == kCS_WITH_SAFETY_AND_DCS_INVARIANTS || directive == kCS_WITH_SAFETY_AND_USER_GIVEN_DCS_INVARIANTS )
     {
         assert( safetyInvariantPOIndex != -1 );
         modifyAigToApplySafetyInvar(pAig, targetCSPropertyIndex, safetyInvariantPOIndex);
     }
 
     pAigDupl = pAig;
     pAig = Aig_ManDupSimple( pAigDupl );
 
     for( i=0; i<Saig_ManPoNum(pAig); i++ )
     {
         pObjTargetPo = Aig_ManCo( pAig, i );
         Aig_ObjChild0Flip( pObjTargetPo );
     }
 
     Pdr_ManSetDefaultParams( pPars );
     pPars->fVerbose = 1;
     pPars->fNotVerbose = 1;
     pPars->fSolveAll = 1;
     pAig->vSeqModelVec = NULL;
 
     Aig_ManCleanup( pAig );
     assert( Aig_ManCheck( pAig ) );
 
     Pdr_ManSolve( pAig, pPars );    
 
     if( pAig->vSeqModelVec )
     {
         pCex = (Abc_Cex_t *)Vec_PtrEntry( pAig->vSeqModelVec, targetCSPropertyIndex );
         if( pCex == NULL )
         {
             RetValue = 1;
         }
         else
             RetValue = 0;
     }
     else
     {
         RetValue = -1;
         exit(0);
     }
 
     free(fileName);
 
     for( i=0; i<Saig_ManPoNum(pAig); i++ )
     {
         pObjTargetPo = Aig_ManCo( pAig, i );
         Aig_ObjChild0Flip( pObjTargetPo );
     }
     
     Aig_ManStop( pAig );
     return RetValue;
 }

Aig_Man_t* generateDisjunctiveTester	(	Abc_Ntk_t *	pNtk,
		Aig_Man_t *	pAig,
		int	combN,
		int	combK
	)

Definition at line 148 of file combination.c.

 {
     //AIG creation related data structure
     Aig_Man_t *pNewAig;
     int piCopied = 0, loCopied = 0, loCreated = 0, liCopied = 0, liCreated = 0, poCopied = 0;
     //int i, iElem, nRegCount, hintSingalBeginningMarker, hintSingalEndMarker;
     int i, nRegCount, hintSingalBeginningMarker, hintSingalEndMarker;
     int combN_internal, combK_internal; //, targetPoIndex;
     long longI, lCombinationCount;
     //Aig_Obj_t *pObj, *pObjMonoCand, *pObjLO_nCk, *pObjDisj_nCk;
     Aig_Obj_t *pObj, *pObjLO_nCk, *pObjDisj_nCk;
     Vec_Ptr_t *vLO_nCk, *vPODriver_nCk, *vDisj_nCk;
     Vec_Int_t *vCandidateMonotoneSignals;
 
     extern Vec_Int_t *findHintOutputs(Abc_Ntk_t *pNtk);
     
     //Knuth's Data Strcuture
     //Vec_Int_t *vC_KNUTH;
     //int i_KNUTH, j_KNUTH, combCounter_KNUTH = 0;
 
     //Collecting target HINT signals
     vCandidateMonotoneSignals = findHintOutputs(pNtk);
     if( vCandidateMonotoneSignals == NULL )
     {
         printf("\nTraget Signal Set is Empty: Duplicating given AIG\n");
         combN_internal = 0;
     }
     else
     {
         //Vec_IntForEachEntry( vCandidateMonotoneSignals, iElem, i )
         //  printf("Po[%d] = %s\n", iElem, Abc_ObjName( Abc_NtkPo(pNtk, iElem) ) );
         hintSingalBeginningMarker = Vec_IntEntry( vCandidateMonotoneSignals, 0 );
         hintSingalEndMarker = Vec_IntEntry( vCandidateMonotoneSignals, Vec_IntSize(vCandidateMonotoneSignals) - 1 );
         combN_internal = hintSingalEndMarker - hintSingalBeginningMarker + 1;
     }
 
     //combK_internal = combK;
 
     //Knuth's Data Structure Initialization
     //vC_KNUTH = Vec_IntAlloc(combK_internal+3);
     //for(i_KNUTH=-1; i_KNUTH<combK_internal; i_KNUTH++)
     //  Vec_IntPush( vC_KNUTH, i_KNUTH );
     //Vec_IntPush( vC_KNUTH, combN_internal );
     //Vec_IntPush( vC_KNUTH, 0 );
 
     //Standard AIG duplication begins
     //Standard AIG Manager Creation
     pNewAig = Aig_ManStart( Aig_ManObjNumMax(pAig) );
     pNewAig->pName = (char *)malloc( strlen( pAig->pName ) + strlen("_nCk") + 1 );
     sprintf(pNewAig->pName, "%s_%s", pAig->pName, "nCk");
         pNewAig->pSpec = NULL;
 
     //Standard Mapping of Constant Nodes
     pObj = Aig_ManConst1( pAig );
         pObj->pData = Aig_ManConst1( pNewAig );
 
     //Standard AIG PI duplication
     Saig_ManForEachPi( pAig, pObj, i )
     {
         piCopied++;
         pObj->pData = Aig_ObjCreateCi(pNewAig);
     }
 
     //Standard AIG LO duplication
     Saig_ManForEachLo( pAig, pObj, i )
         {
         loCopied++;
         pObj->pData = Aig_ObjCreateCi(pNewAig);
         }
 
     //nCk LO creation
     lCombinationCount = 0;
     for(combK_internal=1; combK_internal<=combK; combK_internal++)
         lCombinationCount += countCombination( combN_internal, combK_internal );
     assert( lCombinationCount > 0 );
     vLO_nCk = Vec_PtrAlloc(lCombinationCount);
     for( longI = 0; longI < lCombinationCount; longI++ )
     {
         loCreated++;
         pObj = Aig_ObjCreateCi(pNewAig);
         Vec_PtrPush( vLO_nCk, pObj );
     }
 
     //Standard Node duplication
     Aig_ManForEachNode( pAig, pObj, i )
     {
         pObj->pData = Aig_And( pNewAig, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
     }
     
     //nCk specific logic creation (i.e. nCk number of OR gates)
     vDisj_nCk = Vec_PtrAlloc(lCombinationCount);
 
     
 
     //while(1)
     //{
     //  //visit combination
     //  //printf("Comb-%3d : ", ++combCounter_KNUTH);
     //  pObjMonoCand = Aig_Not(Aig_ManConst1(pNewAig));
     //  for( i_KNUTH=combK_internal; i_KNUTH>0; i_KNUTH--)
     //  {
     //      //printf("vC[%d] = %d ", i_KNUTH, Vec_IntEntry(vC_KNUTH, i_KNUTH));
     //      targetPoIndex = Vec_IntEntry( vCandidateMonotoneSignals, Vec_IntEntry(vC_KNUTH, i_KNUTH));
     //      pObj = Aig_ObjChild0Copy(Aig_ManCo( pAig, targetPoIndex ));
     //      pObjMonoCand = Aig_Or( pNewAig, pObj, pObjMonoCand );
     //  }
     //  Vec_PtrPush(vDisj_nCk, pObjMonoCand );
     //  //printf("\n");
 
     //  j_KNUTH = 1;
     //  while( Vec_IntEntry( vC_KNUTH, j_KNUTH ) + 1 == Vec_IntEntry( vC_KNUTH, j_KNUTH+1 ) )
     //  {
     //      Vec_IntWriteEntry( vC_KNUTH, j_KNUTH, j_KNUTH-1 );
     //      j_KNUTH = j_KNUTH + 1;
     //  }
     //  if( j_KNUTH > combK_internal ) break;
     //  Vec_IntWriteEntry( vC_KNUTH, j_KNUTH, Vec_IntEntry( vC_KNUTH, j_KNUTH ) + 1 );
     //}
     for( combK_internal=1; combK_internal<=combK; combK_internal++ )
         generateCombinatorialStabil( pNewAig, pAig, vCandidateMonotoneSignals,
                 vDisj_nCk, combN_internal, combK_internal );
 
 
     //creation of implication logic
     vPODriver_nCk = Vec_PtrAlloc(lCombinationCount);
     for( longI = 0; longI < lCombinationCount; longI++ )
     {
         pObjLO_nCk = (Aig_Obj_t *)(Vec_PtrEntry( vLO_nCk, longI ));
         pObjDisj_nCk = (Aig_Obj_t *)(Vec_PtrEntry( vDisj_nCk, longI ));
 
         pObj = Aig_Or( pNewAig, Aig_Not(pObjDisj_nCk), pObjLO_nCk);
         Vec_PtrPush(vPODriver_nCk, pObj);
     }
     
     //Standard PO duplication
     Saig_ManForEachPo( pAig, pObj, i )
     {
         poCopied++;
         pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) ); 
     }
 
     //nCk specific PO creation
     for( longI = 0; longI < lCombinationCount; longI++ )
     {
         Aig_ObjCreateCo( pNewAig, (Aig_Obj_t *)(Vec_PtrEntry( vPODriver_nCk, longI )) );
     }
 
     //Standard LI duplication
     Saig_ManForEachLi( pAig, pObj, i )
     {
         liCopied++;
         Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
     }
 
     //nCk specific LI creation
     for( longI = 0; longI < lCombinationCount; longI++ )
     {
         liCreated++;
         Aig_ObjCreateCo( pNewAig, (Aig_Obj_t *)(Vec_PtrEntry( vPODriver_nCk, longI )) );
     }
 
     //clean-up, book-keeping
     assert( liCopied + liCreated == loCopied + loCreated ); 
     nRegCount = loCopied + loCreated;
 
     Aig_ManSetRegNum( pNewAig, nRegCount );
     Aig_ManCleanup( pNewAig );
     assert( Aig_ManCheck( pNewAig ) );
     
     //Vec_IntFree(vC_KNUTH);    
     return pNewAig;
 }

Aig_Man_t* generateGeneralDisjunctiveTester	(	Abc_Ntk_t *	pNtk,
		Aig_Man_t *	pAig,
		int	combK
	)

Definition at line 321 of file combination.c.

 {
     //AIG creation related data structure
     Aig_Man_t *pNewAig;
     int piCopied = 0, loCopied = 0, loCreated = 0, liCopied = 0, liCreated = 0, poCopied = 0;
     //int i, iElem, nRegCount, hintSingalBeginningMarker, hintSingalEndMarker;
     int i, nRegCount;
     int combN_internal, combK_internal; //, targetPoIndex;
     long longI, lCombinationCount;
     //Aig_Obj_t *pObj, *pObjMonoCand, *pObjLO_nCk, *pObjDisj_nCk;
     Aig_Obj_t *pObj, *pObjLO_nCk, *pObjDisj_nCk;
     Vec_Ptr_t *vLO_nCk, *vPODriver_nCk, *vDisj_nCk;
 
     extern Vec_Int_t *findHintOutputs(Abc_Ntk_t *pNtk);
     
     //Knuth's Data Strcuture
     //Vec_Int_t *vC_KNUTH;
     //int i_KNUTH, j_KNUTH, combCounter_KNUTH = 0;
 
     //Collecting target HINT signals
     //vCandidateMonotoneSignals = findHintOutputs(pNtk);
     //if( vCandidateMonotoneSignals == NULL )
     //{
     //  printf("\nTraget Signal Set is Empty: Duplicating given AIG\n");
     //  combN_internal = 0;
     //}
     //else
     //{
         //Vec_IntForEachEntry( vCandidateMonotoneSignals, iElem, i )
         //  printf("Po[%d] = %s\n", iElem, Abc_ObjName( Abc_NtkPo(pNtk, iElem) ) );
     //  hintSingalBeginningMarker = Vec_IntEntry( vCandidateMonotoneSignals, 0 );
     //  hintSingalEndMarker = Vec_IntEntry( vCandidateMonotoneSignals, Vec_IntSize(vCandidateMonotoneSignals) - 1 );
     //  combN_internal = hintSingalEndMarker - hintSingalBeginningMarker + 1;
     //}
 
     combN_internal = Aig_ManRegNum(pAig);
 
     pNewAig = Aig_ManStart( Aig_ManObjNumMax(pAig) );
     pNewAig->pName = (char *)malloc( strlen( pAig->pName ) + strlen("_nCk") + 1 );
     sprintf(pNewAig->pName, "%s_%s", pAig->pName, "nCk");
         pNewAig->pSpec = NULL;
 
     //Standard Mapping of Constant Nodes
     pObj = Aig_ManConst1( pAig );
         pObj->pData = Aig_ManConst1( pNewAig );
 
     //Standard AIG PI duplication
     Saig_ManForEachPi( pAig, pObj, i )
     {
         piCopied++;
         pObj->pData = Aig_ObjCreateCi(pNewAig);
     }
 
     //Standard AIG LO duplication
     Saig_ManForEachLo( pAig, pObj, i )
         {
         loCopied++;
         pObj->pData = Aig_ObjCreateCi(pNewAig);
         }
 
     //nCk LO creation
     lCombinationCount = 0;
     for(combK_internal=1; combK_internal<=combK; combK_internal++)
         lCombinationCount += countCombination( combN_internal, combK_internal );
     assert( lCombinationCount > 0 );
     vLO_nCk = Vec_PtrAlloc(lCombinationCount);
     for( longI = 0; longI < lCombinationCount; longI++ )
     {
         loCreated++;
         pObj = Aig_ObjCreateCi(pNewAig);
         Vec_PtrPush( vLO_nCk, pObj );
     }
 
     //Standard Node duplication
     Aig_ManForEachNode( pAig, pObj, i )
     {
         pObj->pData = Aig_And( pNewAig, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
     }
     
     //nCk specific logic creation (i.e. nCk number of OR gates)
     vDisj_nCk = Vec_PtrAlloc(lCombinationCount);
 
     for( combK_internal=1; combK_internal<=combK; combK_internal++ )
     {
         generateCombinatorialStabilExhaust( pNewAig, pAig,
                 vDisj_nCk, combN_internal, combK_internal );
     }
 
 
     //creation of implication logic
     vPODriver_nCk = Vec_PtrAlloc(lCombinationCount);
     for( longI = 0; longI < lCombinationCount; longI++ )
     {
         pObjLO_nCk = (Aig_Obj_t *)(Vec_PtrEntry( vLO_nCk, longI ));
         pObjDisj_nCk = (Aig_Obj_t *)(Vec_PtrEntry( vDisj_nCk, longI ));
 
         pObj = Aig_Or( pNewAig, Aig_Not(pObjDisj_nCk), pObjLO_nCk);
         Vec_PtrPush(vPODriver_nCk, pObj);
     }
     
     //Standard PO duplication
     Saig_ManForEachPo( pAig, pObj, i )
     {
         poCopied++;
         pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) ); 
     }
 
     //nCk specific PO creation
     for( longI = 0; longI < lCombinationCount; longI++ )
     {
         Aig_ObjCreateCo( pNewAig, (Aig_Obj_t *)(Vec_PtrEntry( vPODriver_nCk, longI )) );
     }
 
     //Standard LI duplication
     Saig_ManForEachLi( pAig, pObj, i )
     {
         liCopied++;
         Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
     }
 
     //nCk specific LI creation
     for( longI = 0; longI < lCombinationCount; longI++ )
     {
         liCreated++;
         Aig_ObjCreateCo( pNewAig, (Aig_Obj_t *)(Vec_PtrEntry( vPODriver_nCk, longI )) );
     }
 
     //clean-up, book-keeping
     assert( liCopied + liCreated == loCopied + loCreated ); 
     nRegCount = loCopied + loCreated;
 
     Aig_ManSetRegNum( pNewAig, nRegCount );
     Aig_ManCleanup( pNewAig );
     assert( Aig_ManCheck( pNewAig ) );
     
     Vec_PtrFree(vLO_nCk);
     Vec_PtrFree(vPODriver_nCk);
     Vec_PtrFree(vDisj_nCk);
     //Vec_IntFree(vC_KNUTH);    
     return pNewAig;
 }

Aig_Man_t* generateWorkingAig	(	Aig_Man_t *	pAig,
		Abc_Ntk_t *	pNtk,
		int *	pIndex0Live
	)

Definition at line 163 of file kLiveConstraints.c.

 {
     Vec_Ptr_t *vSignalVector;
     Aig_Man_t *pAigNew;
 
     vSignalVector = collectCSSignals( pNtk, pAig ); 
     assert(vSignalVector);
     pAigNew = createNewAigWith0LivePo( pAig, vSignalVector, pIndex0Live );
     Vec_PtrFree(vSignalVector);
 
     return pAigNew;
 }

Aig_Man_t* generateWorkingAigWithDSC	(	Aig_Man_t *	pAig,
		Abc_Ntk_t *	pNtk,
		int *	pIndex0Live,
		Vec_Ptr_t *	vMasterBarriers
	)

Definition at line 529 of file arenaViolation.c.

 {
     Vec_Ptr_t *vSignalVector;
     Aig_Man_t *pAigNew;
     int pObjWithinWindow;
     int pObjWindowBegin;
     int pObjPendingSignal;
 
     vSignalVector = collectCSSignalsWithDSC( pNtk, pAig );  
 
     pObjWindowBegin = collectWindowBeginSignalWithDSC( pNtk, pAig );
     pObjWithinWindow = collectWithinWindowSignalWithDSC( pNtk, pAig );
     pObjPendingSignal = collectPendingSignalWithDSC( pNtk, pAig );
 
     pAigNew = createNewAigWith0LivePoWithDSC( pAig, vSignalVector, pIndex0Live, pObjWindowBegin, pObjWithinWindow, pObjPendingSignal, vMasterBarriers );
     Vec_PtrFree(vSignalVector);
 
     return pAigNew;
 }

Vec_Ptr_t* getVecOfVecFairness ( FILE * fp )

Definition at line 502 of file kliveness.c.

 {
     Vec_Ptr_t *masterVector = Vec_PtrAlloc(0);
     //Vec_Ptr_t *currSignalVector;
     char stringBuffer[100];
     //int i;
     
     while(fgets(stringBuffer, 50, fp))
     {
         if(strstr(stringBuffer, ":"))
         {
 
         }
         else
         {
                 
         }
     }
 
     return masterVector;
 }

Aig_Man_t* introduceAbsorberLogic	(	Aig_Man_t *	pAig,
		int *	pLiveIndex_0,
		int *	pLiveIndex_k,
		int	nonFirstIteration
	)

Definition at line 175 of file kliveness.c.

 {
     Aig_Man_t *pNewAig;
     Aig_Obj_t *pObj, *pObjAbsorberLo, *pPInNewArg, *pPOutNewArg;
     Aig_Obj_t *pPIn = NULL, *pPOut = NULL, *pPOutCo = NULL;
     Aig_Obj_t *pFirstAbsorberOr, *pSecondAbsorberOr;
     int i;
     int piCopied = 0, loCreated = 0, loCopied = 0, liCreated = 0, liCopied = 0; 
     int nRegCount;
 
     assert(*pLiveIndex_0 != -1);
     if(nonFirstIteration == 0)
         assert( *pLiveIndex_k == -1 );
     else
         assert( *pLiveIndex_k != -1  );
 
     //****************************************************************
     // 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
     //****************************************************************
     pNewAig = Aig_ManStart( Aig_ManObjNumMax(pAig) );
     pNewAig->pName = (char *)malloc( strlen( pAig->pName ) + strlen("_kCS") + 1 );
     sprintf(pNewAig->pName, "%s_%s", pAig->pName, "kCS");
         pNewAig->pSpec = NULL;
 
     //****************************************************************
     // reading the signal pIn, and pOut
     //****************************************************************
 
     pPIn = readLiveSignal_0( pAig, *pLiveIndex_0 );
     if( *pLiveIndex_k == -1 )
         pPOut = NULL;
     else
         pPOut = readLiveSignal_k( pAig, *pLiveIndex_k );
     
     //****************************************************************
     // Step 2: map constant nodes
     //****************************************************************
         pObj = Aig_ManConst1( pAig );
         pObj->pData = Aig_ManConst1( pNewAig );
 
     //****************************************************************
         // Step 3: create true PIs
     //****************************************************************
         Saig_ManForEachPi( pAig, pObj, i )
     {
         piCopied++;
         pObj->pData = Aig_ObjCreateCi(pNewAig);
     }
 
     //****************************************************************
     // Step 5: create register outputs
     //****************************************************************
         Saig_ManForEachLo( pAig, pObj, i )
         {
         loCopied++;
         pObj->pData = Aig_ObjCreateCi(pNewAig);
         }
 
     //****************************************************************
     // Step 6: create "D" register output for the ABSORBER logic
     //****************************************************************
     loCreated++;
     pObjAbsorberLo = Aig_ObjCreateCi( pNewAig );
 
     nRegCount = loCreated + loCopied;
 
     //********************************************************************
     // Step 7: create internal nodes
     //********************************************************************
         Aig_ManForEachNode( pAig, pObj, i )
     {
         pObj->pData = Aig_And( pNewAig, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
     }
 
     //****************************************************************
     // Step 8: create the two OR gates of the OBSERVER logic
     //****************************************************************
     if( nonFirstIteration == 0 )
     {
         assert(pPIn);
         
         pPInNewArg = !Aig_IsComplement(pPIn)? 
                 (Aig_Obj_t *)((Aig_Regular(pPIn))->pData) : 
                 Aig_Not((Aig_Obj_t *)((Aig_Regular(pPIn))->pData));
 
         pFirstAbsorberOr = Aig_Or( pNewAig, Aig_Not(pPInNewArg), pObjAbsorberLo );
         pSecondAbsorberOr = Aig_Or( pNewAig, pPInNewArg, Aig_Not(pObjAbsorberLo) );
     }
     else
     {
         assert( pPOut );
 
         pPInNewArg = !Aig_IsComplement(pPIn)? 
                 (Aig_Obj_t *)((Aig_Regular(pPIn))->pData) : 
                 Aig_Not((Aig_Obj_t *)((Aig_Regular(pPIn))->pData));
         pPOutNewArg = !Aig_IsComplement(pPOut)? 
                 (Aig_Obj_t *)((Aig_Regular(pPOut))->pData) : 
                 Aig_Not((Aig_Obj_t *)((Aig_Regular(pPOut))->pData));
         
         pFirstAbsorberOr = Aig_Or( pNewAig, Aig_Not(pPOutNewArg), pObjAbsorberLo );
         pSecondAbsorberOr = Aig_Or( pNewAig, pPInNewArg, Aig_Not(pObjAbsorberLo) );
     }   
     
     //********************************************************************
     // Step 9: create primary outputs 
     //********************************************************************
     Saig_ManForEachPo( pAig, pObj, i )
     {
         pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) ); 
         if( i == *pLiveIndex_k )
             pPOutCo = (Aig_Obj_t *)(pObj->pData);
     }
 
     //create new po
     if( nonFirstIteration == 0 )
     {
         assert(pPOutCo == NULL);
         pPOutCo = Aig_ObjCreateCo( pNewAig, pSecondAbsorberOr );    
 
         *pLiveIndex_k = i;
     }   
     else
     {
         assert( pPOutCo != NULL );
         //pPOutCo = Aig_ObjCreateCo( pNewAig, pSecondAbsorberOr );  
         //*pLiveIndex_k = Saig_ManPoNum(pAig);
 
         Aig_ObjPatchFanin0( pNewAig, pPOutCo, pSecondAbsorberOr );
     }
 
     Saig_ManForEachLi( pAig, pObj, i )
     {
         liCopied++;
         Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
     }
 
     //create new li
     liCreated++;
     Aig_ObjCreateCo( pNewAig, pFirstAbsorberOr );
 
     Aig_ManSetRegNum( pNewAig, nRegCount );
     Aig_ManCleanup( pNewAig );
     
     assert( Aig_ManCheck( pNewAig ) );
 
     assert( *pLiveIndex_k != - 1);
     return pNewAig;
 }

void modifyAigToApplySafetyInvar	(	Aig_Man_t *	pAig,
		int	csTarget,
		int	safetyInvarPO
	)

Definition at line 326 of file kliveness.c.

 {
     Aig_Obj_t *pObjPOSafetyInvar, *pObjSafetyInvar;
     Aig_Obj_t *pObjPOCSTarget, *pObjCSTarget;
     Aig_Obj_t *pObjCSTargetNew;
 
     pObjPOSafetyInvar = Aig_ManCo( pAig, safetyInvarPO );
     pObjSafetyInvar =  Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPOSafetyInvar), Aig_ObjFaninC0(pObjPOSafetyInvar));   
     pObjPOCSTarget = Aig_ManCo( pAig, csTarget );
     pObjCSTarget = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPOCSTarget), Aig_ObjFaninC0(pObjPOCSTarget)); 
 
     pObjCSTargetNew = Aig_And( pAig, pObjSafetyInvar, pObjCSTarget );
     Aig_ObjPatchFanin0( pAig, pObjPOCSTarget, pObjCSTargetNew );
 }

Aig_Obj_t* readLiveSignal_0	(	Aig_Man_t *	pAig,
		int	liveIndex_0
	)

Definition at line 83 of file kliveness.c.

 {
     Aig_Obj_t *pObj;
 
     pObj = Aig_ManCo( pAig, liveIndex_0 );
     return Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj));
 }

Aig_Obj_t* readLiveSignal_k	(	Aig_Man_t *	pAig,
		int	liveIndex_k
	)

Definition at line 91 of file kliveness.c.

 {
     Aig_Obj_t *pObj;
 
     pObj = Aig_ManCo( pAig, liveIndex_k );
     return Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj));
 }

Macros

Functions

Macro Definition Documentation

Function Documentation