summaryrefslogtreecommitdiffstats
path: root/src/base/abci/abcDar.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/abci/abcDar.c')
-rw-r--r--src/base/abci/abcDar.c726
1 files changed, 684 insertions, 42 deletions
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index dcc7f4c1..9dc10d84 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -29,6 +29,8 @@
#include "dch.h"
#include "ssw.h"
#include "cgt.h"
+#include "cec.h"
+#include "fsim.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -126,7 +128,7 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters )
if ( Abc_LatchIsInit1(Abc_ObjFanout0(Abc_NtkCo(pNtk,i))) )
pObjNew->pFanin0 = Aig_Not(pObjNew->pFanin0);
// remove dangling nodes
- nNodes = Aig_ManCleanup( pMan );
+ nNodes = (Abc_NtkGetChoiceNum(pNtk) == 0)? Aig_ManCleanup( pMan ) : 0;
if ( !fExors && nNodes )
printf( "Abc_NtkToDar(): Unexpected %d dangling nodes when converting to AIG!\n", nNodes );
//Aig_ManDumpVerilog( pMan, "test.v" );
@@ -153,6 +155,63 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters )
Synopsis [Converts the network from the AIG manager into ABC.]
+ Description [Assumes that registers are ordered after PIs/POs.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Abc_NtkToDarChoices( Abc_Ntk_t * pNtk )
+{
+ Aig_Man_t * pMan;
+ Abc_Obj_t * pObj, * pPrev, * pFanin;
+ Vec_Ptr_t * vNodes;
+ int i;
+ vNodes = Abc_AigDfs( pNtk, 0, 0 );
+ // create the manager
+ pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
+ pMan->pName = Extra_UtilStrsav( pNtk->pName );
+ if ( Abc_NtkGetChoiceNum(pNtk) )
+ {
+ pMan->pEquivs = ALLOC( Aig_Obj_t *, Abc_NtkObjNum(pNtk) );
+ memset( pMan->pEquivs, 0, sizeof(Aig_Obj_t *) * Abc_NtkObjNum(pNtk) );
+ }
+ // 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_ObjCreatePi(pMan);
+ // perform the conversion of the internal nodes (assumes DFS ordering)
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ {
+ pObj->pCopy = (Abc_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj), (Aig_Obj_t *)Abc_ObjChild1Copy(pObj) );
+// printf( "%d->%d ", pObj->Id, ((Aig_Obj_t *)pObj->pCopy)->Id );
+ if ( Abc_AigNodeIsChoice( pObj ) )
+ {
+ for ( pPrev = pObj, pFanin = pObj->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
+ Aig_ObjSetEquiv( pMan, (Aig_Obj_t *)pPrev->pCopy, (Aig_Obj_t *)pFanin->pCopy );
+// Aig_ManCreateChoice( pIfMan, (Aig_Obj_t *)pNode->pCopy );
+ }
+ }
+ Vec_PtrFree( vNodes );
+ // create the POs
+ Abc_NtkForEachCo( pNtk, pObj, i )
+ Aig_ObjCreatePo( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj) );
+ // complement the 1-valued registers
+ Aig_ManSetRegNum( pMan, 0 );
+ if ( !Aig_ManCheck( pMan ) )
+ {
+ printf( "Abc_NtkToDar: AIG check has failed.\n" );
+ Aig_ManStop( pMan );
+ return NULL;
+ }
+ return pMan;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Converts the network from the AIG manager into ABC.]
+
Description []
SideEffects []
@@ -351,6 +410,9 @@ Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan )
assert( pMan->nAsserts == 0 );
// perform strashing
pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
+ // 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 )
@@ -771,7 +833,7 @@ clk = clock();
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fFanout, int fVerbose )
+Abc_Ntk_t * Abc_NtkDC2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose )
{
Aig_Man_t * pMan, * pTemp;
Abc_Ntk_t * pNtkAig;
@@ -783,7 +845,7 @@ Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel,
// Aig_ManPrintStats( pMan );
clk = clock();
- pMan = Dar_ManCompress2( pTemp = pMan, fBalance, fUpdateLevel, fFanout, fVerbose );
+ pMan = Dar_ManCompress2( pTemp = pMan, fBalance, fUpdateLevel, fFanout, fPower, fVerbose );
Aig_ManStop( pTemp );
//PRT( "time", clock() - clk );
@@ -832,7 +894,7 @@ Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, in
***********************************************************************/
Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars )
{
- extern Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
+ extern Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose );
Vec_Ptr_t * vAigs;
Aig_Man_t * pMan, * pTemp;
@@ -845,8 +907,8 @@ Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars )
clk = clock();
if ( pPars->fSynthesis )
{
-// vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, pPars->fVerbose );
- vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, 0 );
+// vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, pPars->fPower, pPars->fVerbose );
+ vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, pPars->fPower, 0 );
Aig_ManStop( pMan );
}
else
@@ -1191,6 +1253,81 @@ PRT( "Time", clock() - clkTotal );
SeeAlso []
***********************************************************************/
+int Abc_NtkDarCec2( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Cec_ParCec_t * pPars )
+{
+ Aig_Man_t * pMan1, * pMan2 = NULL;
+ int RetValue, clkTotal = clock();
+ if ( pNtk2 )
+ {
+ if ( Abc_NtkPiNum(pNtk1) != Abc_NtkPiNum(pNtk2) )
+ {
+ printf( "Networks have different number of PIs.\n" );
+ return -1;
+ }
+ if ( Abc_NtkPoNum(pNtk1) != Abc_NtkPoNum(pNtk2) )
+ {
+ printf( "Networks have different number of POs.\n" );
+ return -1;
+ }
+ }
+ if ( pNtk1 )
+ {
+ pMan1 = Abc_NtkToDar( pNtk1, 0, 0 );
+ if ( pMan1 == NULL )
+ {
+ printf( "Converting into AIG has failed.\n" );
+ return -1;
+ }
+ }
+ if ( pNtk2 )
+ {
+ pMan2 = Abc_NtkToDar( pNtk2, 0, 0 );
+ if ( pMan2 == NULL )
+ {
+ Aig_ManStop( pMan1 );
+ printf( "Converting into AIG has failed.\n" );
+ return -1;
+ }
+ }
+ // perform verification
+ RetValue = Cec_Solve( pMan1, pMan2, pPars );
+ // transfer model if given
+ pNtk1->pModel = pMan1->pData, pMan1->pData = NULL;
+ Aig_ManStop( pMan1 );
+ if ( pMan2 )
+ Aig_ManStop( pMan2 );
+
+ // report the miter
+ if ( RetValue == 1 )
+ {
+ printf( "Networks are equivalent. " );
+PRT( "Time", clock() - clkTotal );
+ }
+ else if ( RetValue == 0 )
+ {
+ printf( "Networks are NOT EQUIVALENT. " );
+PRT( "Time", clock() - clkTotal );
+ }
+ else
+ {
+ printf( "Networks are UNDECIDED. " );
+PRT( "Time", clock() - clkTotal );
+ }
+ fflush( stdout );
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Gives the current ABC network to AIG manager for processing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, Fra_Ssw_t * pPars )
{
Fraig_Params_t Params;
@@ -1282,7 +1419,7 @@ void Abc_NtkPrintLatchEquivClasses( Abc_Ntk_t * pNtk, Aig_Man_t * pAig )
if ( pRepr == NULL )
{
// printf("Nothing equivalent to flop %s\n", pFlopName);
- p_irrelevant[i] = true;
+// p_irrelevant[i] = true;
continue;
}
@@ -1600,7 +1737,7 @@ PRT( "Time", clock() - clk );
***********************************************************************/
int Abc_NtkDarDemiter( Abc_Ntk_t * pNtk )
{
- Aig_Man_t * pMan, * pPart0, * pPart1, * pMiter;
+ Aig_Man_t * pMan, * pPart0, * pPart1;//, * pMiter;
// derive the AIG manager
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
@@ -1608,7 +1745,8 @@ int Abc_NtkDarDemiter( Abc_Ntk_t * pNtk )
printf( "Converting network into AIG has failed.\n" );
return 0;
}
- if ( !Saig_ManDemiterSimple( pMan, &pPart0, &pPart1 ) )
+// if ( !Saig_ManDemiterSimple( pMan, &pPart0, &pPart1 ) )
+ if ( !Saig_ManDemiterSimpleDiff( pMan, &pPart0, &pPart1 ) )
{
printf( "Demitering has failed.\n" );
return 0;
@@ -1617,10 +1755,10 @@ int Abc_NtkDarDemiter( Abc_Ntk_t * pNtk )
Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL );
printf( "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" );
// create two-level miter
- pMiter = Saig_ManCreateMiterTwo( pPart0, pPart1, 2 );
- Aig_ManDumpBlif( pMiter, "miter01.blif", NULL, NULL );
- Aig_ManStop( pMiter );
- printf( "The new miter is written into file \"%s\".\n", "miter01.blif" );
+// pMiter = Saig_ManCreateMiterTwo( pPart0, pPart1, 2 );
+// Aig_ManDumpBlif( pMiter, "miter01.blif", NULL, NULL );
+// Aig_ManStop( pMiter );
+// printf( "The new miter is written into file \"%s\".\n", "miter01.blif" );
Aig_ManStop( pPart0 );
Aig_ManStop( pPart1 );
@@ -1761,7 +1899,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Fra_Sec_t * pSecPar )
return 1;
}
- // commented out because something became non-inductive
+ // commented out because sometimes the problem became non-inductive
/*
// preprocess the miter by fraiging it
// (note that for each functional class, fraiging leaves one representative;
@@ -1805,6 +1943,146 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Fra_Sec_t * pSecPar )
return RetValue;
}
+
+/**Function*************************************************************
+
+ Synopsis [Performs BDD-based reachability analysis.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkDarAbSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbose )
+{
+ Aig_Man_t * pMan1, * pMan2 = NULL;
+ int RetValue;
+ // derive AIG manager
+ pMan1 = Abc_NtkToDar( pNtk1, 0, 1 );
+ if ( pMan1 == NULL )
+ {
+ printf( "Converting miter into AIG has failed.\n" );
+ return -1;
+ }
+ assert( Aig_ManRegNum(pMan1) > 0 );
+ // derive AIG manager
+ if ( pNtk2 )
+ {
+ pMan2 = Abc_NtkToDar( pNtk2, 0, 1 );
+ if ( pMan2 == NULL )
+ {
+ printf( "Converting miter into AIG has failed.\n" );
+ return -1;
+ }
+ assert( Aig_ManRegNum(pMan2) > 0 );
+ }
+
+ // perform verification
+ RetValue = Ssw_SecSpecialMiter( pMan1, pMan2, nFrames, fVerbose );
+ Aig_ManStop( pMan1 );
+ if ( pMan2 )
+ Aig_ManStop( pMan2 );
+ return RetValue;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Gives the current ABC network to AIG manager for processing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkDarSimSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Ssw_Pars_t * pPars )
+{
+ Aig_Man_t * pMan1, * pMan2 = NULL;
+ int RetValue;
+ // derive AIG manager
+ pMan1 = Abc_NtkToDar( pNtk1, 0, 1 );
+ if ( pMan1 == NULL )
+ {
+ printf( "Converting miter into AIG has failed.\n" );
+ return -1;
+ }
+ assert( Aig_ManRegNum(pMan1) > 0 );
+ // derive AIG manager
+ if ( pNtk2 )
+ {
+ pMan2 = Abc_NtkToDar( pNtk2, 0, 1 );
+ if ( pMan2 == NULL )
+ {
+ printf( "Converting miter into AIG has failed.\n" );
+ return -1;
+ }
+ assert( Aig_ManRegNum(pMan2) > 0 );
+ }
+
+ // perform verification
+ RetValue = Ssw_SecWithSimilarity( pMan1, pMan2, pPars );
+ Aig_ManStop( pMan1 );
+ if ( pMan2 )
+ Aig_ManStop( pMan2 );
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarMatch( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nDist, int fVerbose )
+{
+ extern Vec_Int_t * Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose, Aig_Man_t ** ppMiter );
+ Abc_Ntk_t * pNtkAig;
+ Aig_Man_t * pMan1, * pMan2 = NULL, * pManRes;
+ Vec_Int_t * vPairs;
+ assert( Abc_NtkIsStrash(pNtk1) );
+ // derive AIG manager
+ pMan1 = Abc_NtkToDar( pNtk1, 0, 1 );
+ if ( pMan1 == NULL )
+ {
+ printf( "Converting miter into AIG has failed.\n" );
+ return NULL;
+ }
+ assert( Aig_ManRegNum(pMan1) > 0 );
+ // derive AIG manager
+ if ( pNtk2 )
+ {
+ pMan2 = Abc_NtkToDar( pNtk2, 0, 1 );
+ if ( pMan2 == NULL )
+ {
+ printf( "Converting miter into AIG has failed.\n" );
+ return NULL;
+ }
+ assert( Aig_ManRegNum(pMan2) > 0 );
+ }
+
+ // perform verification
+ vPairs = Saig_StrSimPerformMatching( pMan1, pMan2, nDist, 1, &pManRes );
+ pNtkAig = Abc_NtkFromAigPhase( pManRes );
+ if ( vPairs )
+ Vec_IntFree( vPairs );
+ if ( pManRes )
+ Aig_ManStop( pManRes );
+ Aig_ManStop( pMan1 );
+ if ( pMan2 )
+ Aig_ManStop( pMan2 );
+ return pNtkAig;
+}
+
+
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
@@ -2049,33 +2327,140 @@ Abc_Ntk_t * Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk, int nIters, int nSteps, int
SeeAlso []
***********************************************************************/
-int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int fVerbose )
+int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, int fNew, int fComb, int fMiter, int fVerbose )
{
+ extern int Cec_ManSimulate( Aig_Man_t * pAig, int nWords, int nIters, int TimeLimit, int fMiter, int fVerbose );
+ extern int Raig_ManSimulate( Aig_Man_t * pAig, int nWords, int nIters, int TimeLimit, int fMiter, int fVerbose );
Aig_Man_t * pMan;
- Fra_Sml_t * pSml;
Fra_Cex_t * pCex;
- int RetValue, clk = clock();
+ int status, RetValue, clk = clock();
pMan = Abc_NtkToDar( pNtk, 0, 1 );
- pSml = Fra_SmlSimulateSeq( pMan, 0, nFrames, nWords );
- if ( pSml->fNonConstOut )
+ if ( fComb || Abc_NtkLatchNum(pNtk) == 0 )
{
- pCex = Fra_SmlGetCounterExample( pSml );
- if ( pCex )
- printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
+ if ( Cec_ManSimulate( pMan, nWords, nFrames, TimeOut, fMiter, fVerbose ) )
+ {
+ pCex = pMan->pSeqModel;
+ if ( pCex )
+ {
+ printf( "Simulation iterated %d times with %d words asserted output %d in frame %d. ",
nFrames, nWords, pCex->iPo, pCex->iFrame );
- FREE( pNtk->pModel );
- FREE( pNtk->pSeqModel );
- pNtk->pSeqModel = pCex;
- RetValue = 1;
+ status = Ssw_SmlRunCounterExample( pMan, (Ssw_Cex_t *)pCex );
+ if ( status == 0 )
+ printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
+ }
+ FREE( pNtk->pModel );
+ FREE( pNtk->pSeqModel );
+ pNtk->pSeqModel = pCex;
+ RetValue = 1;
+ }
+ else
+ {
+ RetValue = 0;
+ printf( "Simulation iterated %d times with %d words did not assert the outputs. ",
+ nFrames, nWords );
+ }
+ }
+ else if ( fNew )
+ {
+/*
+ if ( Raig_ManSimulate( pMan, nWords, nFrames, TimeOut, fVerbose ) )
+ {
+ if ( (pCex = pMan->pSeqModel) )
+ {
+ printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
+ nFrames, nWords, pCex->iPo, pCex->iFrame );
+ status = Ssw_SmlRunCounterExample( pMan, (Ssw_Cex_t *)pCex );
+ if ( status == 0 )
+ printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
+ }
+ FREE( pNtk->pModel );
+ FREE( pNtk->pSeqModel );
+ pNtk->pSeqModel = pCex; pMan->pSeqModel = NULL;
+ RetValue = 1;
+ }
+ else
+ {
+ RetValue = 0;
+ printf( "Simulation of %d frames with %d words did not assert the outputs. ",
+ nFrames, nWords );
+ }
+*/
+ Fsim_ParSim_t Pars, * pPars = &Pars;
+ Fsim_ManSetDefaultParamsSim( pPars );
+ pPars->nWords = nWords;
+ pPars->nIters = nFrames;
+ pPars->TimeLimit = TimeOut;
+ pPars->fCheckMiter = fMiter;
+ pPars->fVerbose = fVerbose;
+ if ( Fsim_ManSimulate( pMan, pPars ) )
+ {
+ if ( (pCex = pMan->pSeqModel) )
+ {
+ printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
+ nFrames, nWords, pCex->iPo, pCex->iFrame );
+ status = Ssw_SmlRunCounterExample( pMan, (Ssw_Cex_t *)pCex );
+ if ( status == 0 )
+ printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
+ }
+ FREE( pNtk->pModel );
+ FREE( pNtk->pSeqModel );
+ pNtk->pSeqModel = pCex; pMan->pSeqModel = NULL;
+ RetValue = 1;
+ }
+ else
+ {
+ RetValue = 0;
+ printf( "Simulation of %d frames with %d words did not assert the outputs. ",
+ nFrames, nWords );
+ }
}
else
{
- RetValue = 0;
- printf( "Simulation of %d frames with %d words did not assert the outputs. ",
- nFrames, nWords );
+/*
+ Fra_Sml_t * pSml;
+ pSml = Fra_SmlSimulateSeq( pMan, 0, nFrames, nWords );
+ if ( pSml->fNonConstOut )
+ {
+ pCex = Fra_SmlGetCounterExample( pSml );
+ if ( pCex )
+ printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
+ nFrames, nWords, pCex->iPo, pCex->iFrame );
+ FREE( pNtk->pModel );
+ FREE( pNtk->pSeqModel );
+ pNtk->pSeqModel = pCex;
+ RetValue = 1;
+ }
+ else
+ {
+ RetValue = 0;
+ printf( "Simulation of %d frames with %d words did not assert the outputs. ",
+ nFrames, nWords );
+ }
+ Fra_SmlStop( pSml );
+*/
+ if ( Raig_ManSimulate( pMan, nWords, nFrames, TimeOut, fMiter, fVerbose ) )
+ {
+ if ( (pCex = pMan->pSeqModel) )
+ {
+ printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
+ nFrames, nWords, pCex->iPo, pCex->iFrame );
+ status = Ssw_SmlRunCounterExample( pMan, (Ssw_Cex_t *)pCex );
+ if ( status == 0 )
+ printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
+ }
+ FREE( pNtk->pModel );
+ FREE( pNtk->pSeqModel );
+ pNtk->pSeqModel = pCex; pMan->pSeqModel = NULL;
+ RetValue = 1;
+ }
+ else
+ {
+ RetValue = 0;
+ printf( "Simulation of %d frames with %d words did not assert the outputs. ",
+ nFrames, nWords );
+ }
}
PRT( "Time", clock() - clk );
- Fra_SmlStop( pSml );
Aig_ManStop( pMan );
return RetValue;
}
@@ -2200,14 +2585,20 @@ Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConf
return NULL;
Aig_ManSetRegNum( pMan, pMan->nRegs );
- pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fDynamic, fExtend, fVerbose );
+ pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fDynamic, fExtend, 0, fVerbose );
+ if ( pTemp->pSeqModel )
+ {
+ FREE( pNtk->pModel );
+ FREE( pNtk->pSeqModel );
+ pNtk->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
+ }
Aig_ManStop( pTemp );
if ( pMan == NULL )
return NULL;
pNtkAig = Abc_NtkFromAigPhase( pMan );
- pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
- pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
+// pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
+// pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
Aig_ManStop( pMan );
return pNtkAig;
}
@@ -2480,8 +2871,8 @@ Abc_Ntk_t * Abc_NtkPhaseAbstract( Abc_Ntk_t * pNtk, int nFrames, int fIgnore, in
if ( pMan == NULL )
return NULL;
pNtkAig = Abc_NtkFromAigPhase( pMan );
- pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
- pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
+// pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
+// pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
Aig_ManStop( pMan );
return pNtkAig;
}
@@ -2545,8 +2936,8 @@ Abc_Ntk_t * Abc_NtkDarSynch( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nWords, i
if ( pMan == NULL )
return NULL;
pNtkAig = Abc_NtkFromAigPhase( pMan );
- pNtkAig->pName = Extra_UtilStrsav("miter");
- pNtkAig->pSpec = NULL;
+// pNtkAig->pName = Extra_UtilStrsav("miter");
+// pNtkAig->pSpec = NULL;
Aig_ManStop( pMan );
return pNtkAig;
}
@@ -2600,6 +2991,129 @@ Abc_Ntk_t * Abc_NtkDarClockGate( Abc_Ntk_t * pNtk, Abc_Ntk_t * pCare, Cgt_Par_t
SeeAlso []
***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarExtWin( Abc_Ntk_t * pNtk, int nObjId, int nDist, int fVerbose )
+{
+ Abc_Ntk_t * pNtkAig;
+ Aig_Man_t * pMan1, * pMan;
+ Aig_Obj_t * pObj;
+ pMan1 = Abc_NtkToDar( pNtk, 0, 1 );
+ if ( pMan1 == NULL )
+ return NULL;
+ if ( nObjId == -1 )
+ {
+ pObj = Saig_ManFindPivot( pMan1 );
+ printf( "Selected object %d as a window pivot.\n", pObj->Id );
+ }
+ else
+ {
+ if ( nObjId >= Aig_ManObjNumMax(pMan1) )
+ {
+ Aig_ManStop( pMan1 );
+ printf( "The ID is too large.\n" );
+ return NULL;
+ }
+ pObj = Aig_ManObj( pMan1, nObjId );
+ if ( pObj == NULL )
+ {
+ Aig_ManStop( pMan1 );
+ printf( "Object with ID %d does not exist.\n", nObjId );
+ return NULL;
+ }
+ if ( !Saig_ObjIsLo(pMan1, pObj) && !Aig_ObjIsNode(pObj) )
+ {
+ Aig_ManStop( pMan1 );
+ printf( "Object with ID %d is not a node or reg output.\n", nObjId );
+ return NULL;
+ }
+ }
+ pMan = Saig_ManWindowExtract( pMan1, pObj, nDist );
+ Aig_ManStop( pMan1 );
+ if ( pMan == NULL )
+ return NULL;
+ pNtkAig = Abc_NtkFromAigPhase( pMan );
+ pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
+ pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
+ Aig_ManStop( pMan );
+ return pNtkAig;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs phase abstraction.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarInsWin( Abc_Ntk_t * pNtk, Abc_Ntk_t * pCare, int nObjId, int nDist, int fVerbose )
+{
+ Abc_Ntk_t * pNtkAig;
+ Aig_Man_t * pMan1, * pMan2 = NULL, * pMan;
+ Aig_Obj_t * pObj;
+ pMan1 = Abc_NtkToDar( pNtk, 0, 1 );
+ if ( pMan1 == NULL )
+ return NULL;
+ if ( nObjId == -1 )
+ {
+ pObj = Saig_ManFindPivot( pMan1 );
+ printf( "Selected object %d as a window pivot.\n", pObj->Id );
+ }
+ else
+ {
+ if ( nObjId >= Aig_ManObjNumMax(pMan1) )
+ {
+ Aig_ManStop( pMan1 );
+ printf( "The ID is too large.\n" );
+ return NULL;
+ }
+ pObj = Aig_ManObj( pMan1, nObjId );
+ if ( pObj == NULL )
+ {
+ Aig_ManStop( pMan1 );
+ printf( "Object with ID %d does not exist.\n", nObjId );
+ return NULL;
+ }
+ if ( !Saig_ObjIsLo(pMan1, pObj) && !Aig_ObjIsNode(pObj) )
+ {
+ Aig_ManStop( pMan1 );
+ printf( "Object with ID %d is not a node or reg output.\n", nObjId );
+ return NULL;
+ }
+ }
+ if ( pCare )
+ {
+ pMan2 = Abc_NtkToDar( pCare, 0, 0 );
+ if ( pMan2 == NULL )
+ {
+ Aig_ManStop( pMan1 );
+ return NULL;
+ }
+ }
+ pMan = Saig_ManWindowInsert( pMan1, pObj, nDist, pMan2 );
+ Aig_ManStop( pMan1 );
+ if ( pMan2 )
+ Aig_ManStop( pMan2 );
+ if ( pMan == NULL )
+ return NULL;
+ pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
+ Aig_ManStop( pMan );
+ return pNtkAig;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs phase abstraction.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
Abc_Ntk_t * Abc_NtkDarFrames( Abc_Ntk_t * pNtk, int nPrefix, int nFrames, int fInit, int fVerbose )
{
Abc_Ntk_t * pNtkAig;
@@ -2680,6 +3194,112 @@ void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartitio
Aig_ManStop( pMan );
}
+#include "amap.h"
+#include "mio.h"
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Amap_ManProduceNetwork( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMapping )
+{
+ extern void * Abc_FrameReadLibGen();
+ Mio_Library_t * pLib = Abc_FrameReadLibGen();
+ Amap_Out_t * pRes;
+ Vec_Ptr_t * vNodesNew;
+ Abc_Ntk_t * pNtkNew;
+ Abc_Obj_t * pNodeNew, * pFaninNew;
+ int i, k, iPis, iPos, nDupGates;
+ // make sure gates exist in the current library
+ Vec_PtrForEachEntry( vMapping, pRes, i )
+ if ( pRes->pName && Mio_LibraryReadGateByName( pLib, pRes->pName ) == NULL )
+ {
+ printf( "Current library does not contain gate \"%s\".\n", pRes->pName );
+ return NULL;
+ }
+ // create the network
+ pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_MAP );
+ pNtkNew->pManFunc = pLib;
+ iPis = iPos = 0;
+ vNodesNew = Vec_PtrAlloc( Vec_PtrSize(vMapping) );
+ Vec_PtrForEachEntry( vMapping, pRes, i )
+ {
+ if ( pRes->Type == -1 )
+ pNodeNew = Abc_NtkCi( pNtkNew, iPis++ );
+ else if ( pRes->Type == 1 )
+ pNodeNew = Abc_NtkCo( pNtkNew, iPos++ );
+ else
+ {
+ pNodeNew = Abc_NtkCreateNode( pNtkNew );
+ pNodeNew->pData = Mio_LibraryReadGateByName( pLib, pRes->pName );
+ }
+ for ( k = 0; k < pRes->nFans; k++ )
+ {
+ pFaninNew = Vec_PtrEntry( vNodesNew, pRes->pFans[k] );
+ Abc_ObjAddFanin( pNodeNew, pFaninNew );
+ }
+ Vec_PtrPush( vNodesNew, pNodeNew );
+ }
+ Vec_PtrFree( vNodesNew );
+ assert( iPis == Abc_NtkCiNum(pNtkNew) );
+ assert( iPos == Abc_NtkCoNum(pNtkNew) );
+ // decouple the PO driver nodes to reduce the number of levels
+ nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
+// if ( nDupGates && Map_ManReadVerbose(pMan) )
+// printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
+ return pNtkNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Gives the current ABC network to AIG manager for processing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarAmap( Abc_Ntk_t * pNtk, Amap_Par_t * pPars )
+{
+ Vec_Ptr_t * vMapping;
+ Abc_Ntk_t * pNtkAig = NULL;
+ Aig_Man_t * pMan;
+ Aig_MmFlex_t * pMem;
+
+ assert( Abc_NtkIsStrash(pNtk) );
+ // convert to the AIG manager
+ pMan = Abc_NtkToDarChoices( pNtk );
+ if ( pMan == NULL )
+ return NULL;
+
+ // perform computation
+ vMapping = Amap_ManTest( pMan, pPars );
+ Aig_ManStop( pMan );
+ if ( vMapping == NULL )
+ return NULL;
+ pMem = Vec_PtrPop( vMapping );
+ pNtkAig = Amap_ManProduceNetwork( pNtk, vMapping );
+ Aig_MmFlexStop( pMem, 0 );
+ Vec_PtrFree( vMapping );
+
+ // make sure everything is okay
+ if ( pNtkAig && !Abc_NtkCheck( pNtkAig ) )
+ {
+ printf( "Abc_NtkDar: The network check has failed.\n" );
+ Abc_NtkDelete( pNtkAig );
+ return NULL;
+ }
+ return pNtkAig;
+}
/**Function*************************************************************
@@ -2694,9 +3314,10 @@ void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartitio
***********************************************************************/
void Abc_NtkDarTest( Abc_Ntk_t * pNtk )
{
-// extern Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig );
-
- Aig_Man_t * pMan;//, * pTemp;
+ extern void Fsim_ManTest( Aig_Man_t * pAig );
+ extern Vec_Int_t * Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose, Aig_Man_t ** ppMiter );
+// Vec_Int_t * vPairs;
+ Aig_Man_t * pMan;//, * pMan2;//, * pTemp;
assert( Abc_NtkIsStrash(pNtk) );
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
@@ -2714,9 +3335,21 @@ Aig_ManPrintStats( pMan );
pTemp = Ssw_SignalCorrespondeceTestPairs( pMan );
Aig_ManStop( pTemp );
*/
- Ssw_SecSpecialMiter( pMan, 1 );
+/*
+// Ssw_SecSpecialMiter( pMan, NULL, 2, 1 );
+ pMan2 = Aig_ManDupSimple(pMan);
+ vPairs = Saig_StrSimPerformMatching( pMan, pMan2, 0, 1, NULL );
+ Vec_IntFree( vPairs );
Aig_ManStop( pMan );
+ Aig_ManStop( pMan2 );
+*/
+
+// Saig_MvManSimulate( pMan, 1 );
+
+ Fsim_ManTest( pMan );
+ Aig_ManStop( pMan );
+
}
/**Function*************************************************************
@@ -2732,6 +3365,8 @@ Aig_ManPrintStats( pMan );
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
{
+ extern Aig_Man_t * Saig_ManDualRail( Aig_Man_t * p, int fMiter );
+
/*
extern Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig );
@@ -2760,9 +3395,16 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
return NULL;
+/*
+ Aig_ManSetRegNum( pMan, pMan->nRegs );
+ pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 0, 0, 0, 1 );
+ Aig_ManStop( pTemp );
+ if ( pMan == NULL )
+ return NULL;
+*/
Aig_ManSetRegNum( pMan, pMan->nRegs );
- pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 0, 0, 1 );
+ pMan = Saig_ManDualRail( pTemp = pMan, 1 );
Aig_ManStop( pTemp );
if ( pMan == NULL )
return NULL;
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-06 16:40:15 +0000