summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/abci/abc.c36
1 files changed, 10 insertions, 26 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 3eb4d5e7..0fa6f86c 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -400,6 +400,9 @@ extern int Abc_CommandAbcLivenessToSafety ( Abc_Frame_t * pAbc, int argc, cha
extern int Abc_CommandAbcLivenessToSafetySim ( Abc_Frame_t * pAbc, int argc, char ** argv );
extern int Abc_CommandAbcLivenessToSafetyWithLTL( Abc_Frame_t * pAbc, int argc, char ** argv );
+extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -6214,8 +6217,6 @@ int Abc_CommandOrPos( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( fReverse )
{
extern Aig_Man_t * Abc_NtkToDarBmc( Abc_Ntk_t * pNtk, Vec_Int_t ** pvMap );
- extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
-
Aig_Man_t * pMan = Abc_NtkToDarBmc( pNtk, NULL );
Abc_Ntk_t * pNtkRes = Abc_NtkFromAigPhase( pMan );
Aig_ManStop( pMan );
@@ -8062,7 +8063,6 @@ usage:
***********************************************************************/
int Abc_CommandTrim( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
Abc_Ntk_t * pNtk, * pNtkRes;
Gia_Man_t * pGia, * pNew;
Aig_Man_t * pAig;
@@ -11847,7 +11847,6 @@ int Abc_CommandSendAig( Abc_Frame_t * pAbc, int argc, char ** argv )
}
else
{
- extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
Aig_Man_t * pAig;
Gia_Man_t * pGia;
if ( pAbc->pNtkCur == NULL )
@@ -21358,7 +21357,6 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
pAbc->Status = Abc_NtkDarBmcInter( pNtkNew, pPars, NULL );
if ( pAbc->Status == 0 )
{
- extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
Aig_Man_t * pMan = Abc_NtkToDar( pNtk, 0, 1 );
pNtkNew->pSeqModel->iPo = Saig_ManFindFailedPoCex( pMan, pNtkNew->pSeqModel );
Aig_ManStop( pMan );
@@ -22487,7 +22485,6 @@ int Abc_CommandTestCex( Abc_Frame_t * pAbc, int argc, char ** argv )
// Abc_Print( 1, "Main AIG: The number of POs (%d) is less than the PO index in cex (%d).\n", Abc_NtkPoNum(pNtk), pAbc->pCex->iPo );
else
{
- extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
Gia_Man_t * pGia = Gia_ManFromAigSimple( pAig );
// if ( !Gia_ManVerifyCex( pGia, pAbc->pCex, 0 ) )
@@ -22728,7 +22725,6 @@ usage:
***********************************************************************/
int Abc_CommandReconcile( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
extern Abc_Cex_t * Llb4_Nonlin4NormalizeCex( Aig_Man_t * pAigOrg, Aig_Man_t * pAigRpm, Abc_Cex_t * pCexRpm );
Abc_Cex_t * pCex;
Abc_Ntk_t * pNtk1 = NULL, * pNtk2 = NULL;
@@ -22927,13 +22923,13 @@ usage:
***********************************************************************/
int Abc_CommandCexCut( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- int c;
- int iFrStart = 0;
- int iFrStop = ABC_INFINITY;
- int fCombOnly = 0;
- int fUseOne = 0;
- int fAllFrames = 0;
- int fVerbose = 0;
+ Abc_Ntk_t * pNtkNew;
+ int c, iFrStart = 0;
+ int iFrStop = ABC_INFINITY;
+ int fCombOnly = 0;
+ int fUseOne = 0;
+ int fAllFrames = 0;
+ int fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FGcnmvh" ) ) != EOF )
{
@@ -23000,9 +22996,6 @@ int Abc_CommandCexCut( Abc_Frame_t * pAbc, int argc, char ** argv )
iFrStop = pAbc->pCex->iFrame;
{
- extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
- extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
- Abc_Ntk_t * pNtkNew;
Aig_Man_t * pAig = Abc_NtkToDar( pAbc->pNtkCur, 0, 1 );
Aig_Man_t * pAigNew = Bmc_AigTargetStates( pAig, pAbc->pCex, iFrStart, iFrStop, fCombOnly, fUseOne, fAllFrames, fVerbose );
Aig_ManStop( pAig );
@@ -23211,7 +23204,6 @@ int Abc_CommandCexMin( Abc_Frame_t * pAbc, int argc, char ** argv )
// Abc_Print( 1, "Main AIG: The number of POs (%d) is less than the PO index in cex (%d).\n", Abc_NtkPoNum(pNtk), pAbc->pCex->iPo );
else
{
- extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
Gia_Man_t * pGia = Gia_ManFromAigSimple( pAig );
// if ( !Gia_ManVerifyCex( pGia, pAbc->pCex, 0 ) )
@@ -23260,8 +23252,6 @@ usage:
int Abc_CommandDualRail( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Vec_Int_t * Abc_NtkFindDcLatches( Abc_Ntk_t * pNtk );
- extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
- extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
Abc_Ntk_t * pNtk, * pNtkNew = NULL;
Aig_Man_t * pAig, * pAigNew;
Vec_Int_t * vDcFlops = NULL;
@@ -23378,8 +23368,6 @@ usage:
***********************************************************************/
int Abc_CommandBlockPo( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
- extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
Abc_Ntk_t * pNtk, * pNtkNew = NULL;
Aig_Man_t * pAig;
int c;
@@ -23462,8 +23450,6 @@ usage:
***********************************************************************/
int Abc_CommandIso( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
- extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
Abc_Ntk_t * pNtk, * pNtkNew = NULL;
Aig_Man_t * pAig, * pTemp;
Vec_Ptr_t * vPosEquivs = NULL;
@@ -23946,7 +23932,6 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
extern Aig_Man_t * Abc_NtkToDarChoices( Abc_Ntk_t * pNtk );
extern Vec_Ptr_t * Abc_NtkCollectCiNames( Abc_Ntk_t * pNtk );
extern Vec_Ptr_t * Abc_NtkCollectCoNames( Abc_Ntk_t * pNtk );
@@ -24032,7 +24017,6 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
extern Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan );
Aig_Man_t * pMan;
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-05 00:56:41 +0000