abc-master
|
Go to the source code of this file.
Functions | |
ABC_NAMESPACE_IMPL_START int | Bmc_GiaGenerateJust_rec (Gia_Man_t *p, int iFrame, int iObj, Vec_Bit_t *vValues, Vec_Bit_t *vJustis) |
DECLARATIONS ///. More... | |
void | Bmc_GiaGenerateJustNonRec (Gia_Man_t *p, int iFrame, Vec_Bit_t *vValues, Vec_Bit_t *vJustis) |
void | Bmc_GiaGenerateJust (Gia_Man_t *p, Abc_Cex_t *pCex, Vec_Bit_t **pvValues, Vec_Bit_t **pvJustis) |
Gia_Man_t * | Bmc_GiaGenerateGiaOne (Gia_Man_t *p, Abc_Cex_t *pCex, Vec_Bit_t **pvInits, int iFrBeg, int iFrEnd) |
Gia_Man_t * | Bmc_GiaGenerateGiaAllFrames (Gia_Man_t *p, Abc_Cex_t *pCex, Vec_Bit_t **pvInits, int iFrBeg, int iFrEnd) |
Gia_Man_t * | Bmc_GiaGenerateGiaAllOne (Gia_Man_t *p, Abc_Cex_t *pCex, Vec_Bit_t **pvInits, int iFrBeg, int iFrEnd) |
Gia_Man_t * | Bmc_GiaTargetStates (Gia_Man_t *p, Abc_Cex_t *pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fUseOne, int fAllFrames, int fVerbose) |
Aig_Man_t * | Bmc_AigTargetStates (Aig_Man_t *p, Abc_Cex_t *pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fUseOne, int fAllFrames, int fVerbose) |
Aig_Man_t* Bmc_AigTargetStates | ( | Aig_Man_t * | p, |
Abc_Cex_t * | pCex, | ||
int | iFrBeg, | ||
int | iFrEnd, | ||
int | fCombOnly, | ||
int | fUseOne, | ||
int | fAllFrames, | ||
int | fVerbose | ||
) |
Function*************************************************************
Synopsis [Generate AIG for target bad states.]
Description []
SideEffects []
SeeAlso []
Definition at line 513 of file bmcCexCut.c.
Gia_Man_t* Bmc_GiaGenerateGiaAllFrames | ( | Gia_Man_t * | p, |
Abc_Cex_t * | pCex, | ||
Vec_Bit_t ** | pvInits, | ||
int | iFrBeg, | ||
int | iFrEnd | ||
) |
Function*************************************************************
Synopsis [Generates all frames from G to the last one.]
Description []
SideEffects []
SeeAlso []
Definition at line 237 of file bmcCexCut.c.
Gia_Man_t* Bmc_GiaGenerateGiaAllOne | ( | Gia_Man_t * | p, |
Abc_Cex_t * | pCex, | ||
Vec_Bit_t ** | pvInits, | ||
int | iFrBeg, | ||
int | iFrEnd | ||
) |
Function*************************************************************
Synopsis [Generates one frame.]
Description []
SideEffects []
SeeAlso []
Definition at line 365 of file bmcCexCut.c.
Gia_Man_t* Bmc_GiaGenerateGiaOne | ( | Gia_Man_t * | p, |
Abc_Cex_t * | pCex, | ||
Vec_Bit_t ** | pvInits, | ||
int | iFrBeg, | ||
int | iFrEnd | ||
) |
Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
Definition at line 192 of file bmcCexCut.c.
void Bmc_GiaGenerateJust | ( | Gia_Man_t * | p, |
Abc_Cex_t * | pCex, | ||
Vec_Bit_t ** | pvValues, | ||
Vec_Bit_t ** | pvJustis | ||
) |
Definition at line 106 of file bmcCexCut.c.
ABC_NAMESPACE_IMPL_START int Bmc_GiaGenerateJust_rec | ( | Gia_Man_t * | p, |
int | iFrame, | ||
int | iObj, | ||
Vec_Bit_t * | vValues, | ||
Vec_Bit_t * | vJustis | ||
) |
DECLARATIONS ///.
CFile****************************************************************
FileName [bmcCexCut.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT-based bounded model checking.]
Synopsis [Derives characterization of bad states.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [
]FUNCTION DEFINITIONS /// Function*************************************************************
Synopsis [Generate justifying assignments.]
Description []
SideEffects []
SeeAlso []
Definition at line 46 of file bmcCexCut.c.
void Bmc_GiaGenerateJustNonRec | ( | Gia_Man_t * | p, |
int | iFrame, | ||
Vec_Bit_t * | vValues, | ||
Vec_Bit_t * | vJustis | ||
) |
Definition at line 74 of file bmcCexCut.c.
Gia_Man_t* Bmc_GiaTargetStates | ( | Gia_Man_t * | p, |
Abc_Cex_t * | pCex, | ||
int | iFrBeg, | ||
int | iFrEnd, | ||
int | fCombOnly, | ||
int | fUseOne, | ||
int | fAllFrames, | ||
int | fVerbose | ||
) |
Function*************************************************************
Synopsis [Generate GIA for target bad states.]
Description []
SideEffects []
SeeAlso []
Definition at line 461 of file bmcCexCut.c.