summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abc/abc.h2
-rw-r--r--src/base/abc/abcNtk.c103
-rw-r--r--src/base/abci/abc.c141
-rw-r--r--src/base/abci/abcDar.c39
-rw-r--r--src/base/io/ioUtil.c2
5 files changed, 265 insertions, 22 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 7dce5154..10bab783 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -703,7 +703,7 @@ extern Abc_Ntk_t * Abc_NtkCreateFromNode( Abc_Ntk_t * pNtk, Abc_Obj_t * p
extern Abc_Ntk_t * Abc_NtkCreateWithNode( char * pSop );
extern void Abc_NtkDelete( Abc_Ntk_t * pNtk );
extern void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk );
-extern void Abc_NtkMakeComb( Abc_Ntk_t * pNtk );
+extern void Abc_NtkMakeComb( Abc_Ntk_t * pNtk, int fRemoveLatches );
/*=== abcObj.c ==========================================================*/
extern Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
extern void Abc_ObjRecycle( Abc_Obj_t * pObj );
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 6f34fa0b..b66c3f32 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -1104,7 +1104,7 @@ void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
-void Abc_NtkMakeComb( Abc_Ntk_t * pNtk )
+void Abc_NtkMakeComb( Abc_Ntk_t * pNtk, int fRemoveLatches )
{
Abc_Obj_t * pObj;
int i;
@@ -1136,17 +1136,48 @@ void Abc_NtkMakeComb( Abc_Ntk_t * pNtk )
}
assert( Abc_NtkBoNum(pNtk) == 0 );
- // move COs to become POs
- Vec_PtrClear( pNtk->vPos );
- Abc_NtkForEachCo( pNtk, pObj, i )
+ if ( fRemoveLatches )
+ {
+ // remove registers
+ Vec_Ptr_t * vBos;
+ vBos = Vec_PtrAlloc( 100 );
+ Vec_PtrClear( pNtk->vPos );
+ Abc_NtkForEachCo( pNtk, pObj, i )
+ if ( Abc_ObjIsBi(pObj) )
+ Vec_PtrPush( vBos, pObj );
+ else
+ Vec_PtrPush( pNtk->vPos, pObj );
+ // remove COs
+ Vec_PtrFree( pNtk->vCos );
+ pNtk->vCos = NULL;
+ // remove the BOs
+ Vec_PtrForEachEntry( vBos, pObj, i )
+ Abc_NtkDeleteObj( pObj );
+ Vec_PtrFree( vBos );
+ // create COs
+ pNtk->vCos = Vec_PtrDup( pNtk->vPos );
+ // cleanup
+ if ( Abc_NtkIsLogic(pNtk) )
+ Abc_NtkCleanup( pNtk, 0 );
+ else if ( Abc_NtkIsStrash(pNtk) )
+ Abc_AigCleanup( pNtk->pManFunc );
+ else
+ assert( 0 );
+ }
+ else
{
- if ( Abc_ObjIsBi(pObj) )
+ // move COs to become POs
+ Vec_PtrClear( pNtk->vPos );
+ Abc_NtkForEachCo( pNtk, pObj, i )
{
- pObj->Type = ABC_OBJ_PO;
- pNtk->nObjCounts[ABC_OBJ_PO]++;
- pNtk->nObjCounts[ABC_OBJ_BI]--;
+ if ( Abc_ObjIsBi(pObj) )
+ {
+ pObj->Type = ABC_OBJ_PO;
+ pNtk->nObjCounts[ABC_OBJ_PO]++;
+ pNtk->nObjCounts[ABC_OBJ_BI]--;
+ }
+ Vec_PtrPush( pNtk->vPos, pObj );
}
- Vec_PtrPush( pNtk->vPos, pObj );
}
assert( Abc_NtkBiNum(pNtk) == 0 );
@@ -1157,6 +1188,60 @@ void Abc_NtkMakeComb( Abc_Ntk_t * pNtk )
/**Function*************************************************************
+ Synopsis [Removes all POs, except one.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkMakeOnePo( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodePo )
+{
+ Vec_Ptr_t * vPosToRemove;
+ Abc_Obj_t * pObj;
+ int i;
+
+ assert( !Abc_NtkIsNetlist(pNtk) );
+ assert( Abc_NtkHasOnlyLatchBoxes(pNtk) );
+
+ if ( Abc_NtkPoNum(pNtk) == 1 )
+ return;
+
+ // make sure the node exists
+ Abc_NtkForEachPo( pNtk, pObj, i )
+ if ( pObj == pNodePo )
+ break;
+ assert( i < Abc_NtkPoNum(pNtk) );
+
+ // collect POs to remove
+ vPosToRemove = Vec_PtrAlloc( 100 );
+ Abc_NtkForEachPo( pNtk, pObj, i )
+ if ( pObj != pNodePo )
+ Vec_PtrPush( vPosToRemove, pObj );
+
+ // remove the POs
+ Vec_PtrForEachEntry( vPosToRemove, pObj, i )
+ Abc_NtkDeleteObj( pObj );
+ Vec_PtrFree( vPosToRemove );
+
+ if ( Abc_NtkIsStrash(pNtk) )
+ {
+ Abc_AigCleanup( 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" );
+}
+
+/**Function*************************************************************
+
Synopsis [Removes POs with suppsize less than 2 and PIs without fanout.]
Description []
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d3ac7669..8c9a9609 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -197,6 +197,7 @@ static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandIProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDebug ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBmc ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandBmcInter ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIndcut ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandEnlarge ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -447,6 +448,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Verification", "iprove", Abc_CommandIProve, 1 );
Cmd_CommandAdd( pAbc, "Verification", "debug", Abc_CommandDebug, 0 );
Cmd_CommandAdd( pAbc, "Verification", "bmc", Abc_CommandBmc, 0 );
+ Cmd_CommandAdd( pAbc, "Verification", "int", Abc_CommandBmcInter, 0 );
Cmd_CommandAdd( pAbc, "Verification", "indcut", Abc_CommandIndcut, 0 );
Cmd_CommandAdd( pAbc, "Verification", "enlarge", Abc_CommandEnlarge, 1 );
@@ -4531,17 +4533,22 @@ int Abc_CommandComb( Abc_Frame_t * pAbc, int argc, char ** argv )
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
int c;
+ int fRemoveLatches;
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
+ fRemoveLatches = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "lh" ) ) != EOF )
{
switch ( c )
{
+ case 'l':
+ fRemoveLatches ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -4562,14 +4569,15 @@ int Abc_CommandComb( Abc_Frame_t * pAbc, int argc, char ** argv )
// get the new network
pNtkRes = Abc_NtkDup( pNtk );
- Abc_NtkMakeComb( pNtkRes );
+ Abc_NtkMakeComb( pNtkRes, fRemoveLatches );
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
- fprintf( pErr, "usage: comb [-h]\n" );
+ fprintf( pErr, "usage: comb [-lh]\n" );
fprintf( pErr, "\t makes the current network combinational by replacing latches by PI/PO pairs\n" );
+ fprintf( pErr, "\t-l : toggle removing latches [default = %s]\n", fRemoveLatches? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
@@ -5741,8 +5749,11 @@ int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
int fUseAllCis;
int fUseMffc;
+ int fSeq;
int Output;
+ extern void Abc_NtkMakeOnePo( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodePo );
+
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -5750,9 +5761,10 @@ int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
fUseAllCis = 0;
fUseMffc = 0;
+ fSeq = 0;
Output = -1;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Omah" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Omash" ) ) != EOF )
{
switch ( c )
{
@@ -5769,9 +5781,13 @@ int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv )
break;
case 'm':
fUseMffc ^= 1;
+ break;
case 'a':
fUseAllCis ^= 1;
break;
+ case 's':
+ fSeq ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -5824,12 +5840,18 @@ int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
pNodeCo = Abc_NtkCo( pNtk, Output );
- if ( fUseMffc )
+ if ( fSeq )
+ {
+ pNtkRes = Abc_NtkDup( pNtk );
+ pNodeCo = Abc_NtkPo( pNtkRes, Output );
+ Abc_NtkMakeOnePo( pNtkRes, pNodeCo );
+ }
+ else if ( fUseMffc )
pNtkRes = Abc_NtkCreateMffc( pNtk, Abc_ObjFanin0(pNodeCo), Abc_ObjName(pNodeCo) );
- else
+ else
pNtkRes = Abc_NtkCreateCone( pNtk, Abc_ObjFanin0(pNodeCo), Abc_ObjName(pNodeCo), fUseAllCis );
}
- if ( pNodeCo && Abc_ObjFaninC0(pNodeCo) )
+ if ( pNodeCo && Abc_ObjFaninC0(pNodeCo) && !fSeq )
printf( "The extracted cone represents the complement function of the CO.\n" );
if ( pNtkRes == NULL )
{
@@ -5841,10 +5863,11 @@ int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: cone [-O num] [-amh] <name>\n" );
+ fprintf( pErr, "usage: cone [-O num] [-amsh] <name>\n" );
fprintf( pErr, "\t replaces the current network by one logic cone\n" );
- fprintf( pErr, "\t-a : toggle writing all CIs or structral support only [default = %s]\n", fUseAllCis? "all": "structural" );
- fprintf( pErr, "\t-m : toggle writing only MFFC or complete TFI cone [default = %s]\n", fUseMffc? "MFFC": "TFI cone" );
+ fprintf( pErr, "\t-a : toggle keeping all CIs or structral support only [default = %s]\n", fUseAllCis? "all": "structural" );
+ fprintf( pErr, "\t-m : toggle keeping only MFFC or complete TFI cone [default = %s]\n", fUseMffc? "MFFC": "TFI cone" );
+ fprintf( pErr, "\t-s : toggle comb or sequential cone (works with \"-O num\") [default = %s]\n", fSeq? "seq": "comb" );
fprintf( pErr, "\t-h : print the command usage\n");
fprintf( pErr, "\t-O num : (optional) the 0-based number of the CO to extract\n");
fprintf( pErr, "\tname : (optional) the name of the node to extract\n");
@@ -14601,6 +14624,11 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
return 0;
}
+ if ( Abc_NtkLatchNum(pNtk) == 0 )
+ {
+ fprintf( stdout, "Does not work for combinational networks.\n" );
+ return 0;
+ }
Abc_NtkDarBmc( pNtk, nFrames, nBTLimit, fRewrite, fVerbose );
return 0;
@@ -14614,7 +14642,98 @@ usage:
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
-
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk;
+ int c;
+ int nBTLimit;
+ int fRewrite;
+ int fVerbose;
+
+ extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ nBTLimit = 20000;
+ fRewrite = 0;
+ fVerbose = 1;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Crvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nBTLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nBTLimit < 0 )
+ goto usage;
+ break;
+ case 'r':
+ fRewrite ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
+ return 0;
+ }
+ if ( Abc_NtkLatchNum(pNtk) == 0 )
+ {
+ fprintf( stdout, "Does not work for combinational networks.\n" );
+ return 0;
+ }
+ if ( Abc_NtkPoNum(pNtk) != 1 )
+ {
+ fprintf( stdout, "Currently only works for single-output miters (run \"orpos\").\n" );
+ return 0;
+ }
+ Abc_NtkDarBmcInter( pNtk, nBTLimit, fVerbose );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: int [-C num] [-vh]\n" );
+ fprintf( pErr, "\t uses interpolation to prove the property\n" );
+ fprintf( pErr, "\t-C num : the limit on conflicts for one SAT run [default = %d]\n", nBTLimit );
+// fprintf( pErr, "\t-r : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" );
+ fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
/**Function*************************************************************
Synopsis []
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 329bccf8..d2022e37 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1240,6 +1240,45 @@ PRT( "Time", clock() - clk );
SeeAlso []
***********************************************************************/
+int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose )
+{
+ Aig_Man_t * pMan;
+ int RetValue, Depth, clk = clock();
+ // derive the AIG manager
+ pMan = Abc_NtkToDar( pNtk, 0, 1 );
+ if ( pMan == NULL )
+ {
+ printf( "Converting miter into AIG has failed.\n" );
+ return -1;
+ }
+ assert( pMan->nRegs > 0 );
+ pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan);
+ pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan);
+ RetValue = Saig_Interpolate( pMan, nConfLimit, fVerbose, &Depth );
+ if ( RetValue == 1 )
+ printf( "Property proved. " );
+ else if ( RetValue == 0 )
+ printf( "Property DISPROVED with counter-example at depth %d. ", Depth );
+ else if ( RetValue == -1 )
+ printf( "Property UNDECIDED. " );
+ else
+ assert( 0 );
+PRT( "Time", clock() - clk );
+ Aig_ManStop( pMan );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Gives the current ABC network to AIG manager for processing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose )
{
Aig_Man_t * pMan;
diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c
index 37d57f30..a5d32e39 100644
--- a/src/base/io/ioUtil.c
+++ b/src/base/io/ioUtil.c
@@ -299,7 +299,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
{
fprintf( stdout, "Latches are writen into the PLA file at PI/PO pairs.\n" );
pNtkCopy = Abc_NtkDup( pNtk );
- Abc_NtkMakeComb( pNtkCopy );
+ Abc_NtkMakeComb( pNtkCopy, 0 );
pNtkTemp = Abc_NtkToNetlist( pNtk );
Abc_NtkDelete( pNtkCopy );
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-10 00:39:22 +0000