Skip to content

A
abc
Commit aec5d338 by Alan Mishchenko
Options

Backward reachability using circuit cofactoring.

parent 1e20e2cc
Showing with 126 additions and 8 deletions
abclib.dsp
......@@ -4023,6 +4023,10 @@ SOURCE=.\src\aig\gia\giaBidec.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaCCof.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaCof.c
# End Source File
# Begin Source File
......
src/aig/gia/giaAbsVta.c
......@@ -212,7 +212,7 @@ void Vga_ManGrow( Vta_Man_t * p, int fThis )
static int PrevF = -1;
Gia_Obj_t * pObj, * pObj2;
int Beg, End, One, i, c, f, iOutVar, nClauses;
assert( ++PrevF == f );
assert( ++PrevF == fThis );
assert( fThis >= 0 && fThis < p->nFramesMax );
// create variable for the output
......@@ -422,9 +422,9 @@ void Gia_VtaCollect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vOrder, Ve
***********************************************************************/
Vec_Int_t * Gia_VtaCollect( Gia_Man_t * p, Vec_Int_t ** pvFraLims, Vec_Int_t ** pvRoots )
{
Vec_Int_t * vOrder; // resulting ordering of PI/RO/And
Vec_Int_t * vOrder; // resulting ordering of PI/RO/And
Vec_Int_t * vFraLims; // frame limits
Vec_Int_t * vRoots; // CO roots
Vec_Int_t * vRoots; // CO roots
Gia_Obj_t * pObj;
int i, StopPoint;
......@@ -435,10 +435,15 @@ Vec_Int_t * Gia_VtaCollect( Gia_Man_t * p, Vec_Int_t ** pvFraLims, Vec_Int_t **
Gia_ManForEachPo( p, pObj, i )
Vec_IntPush( vRoots, Gia_ObjId(p, pObj) );
// collects nodes/flops
vFraLims = Vec_IntAlloc( 1000 );
// start order
vOrder = Vec_IntAlloc( Gia_ManObjNum(p) );
Vec_IntPush( vOrder, -1 );
// start limits
vFraLims = Vec_IntAlloc( 1000 );
Vec_IntPush( vFraLims, Vec_IntSize(vOrder) );
// collect new nodes
StopPoint = Vec_IntSize(vRoots);
Gia_ManForEachObjVec( vRoots, p, pObj, i )
{
......@@ -487,6 +492,7 @@ Gia_Man_t * Gia_VtaTest( Gia_Man_t * p )
{
Vec_Int_t * vOrder, * vFraLims, * vRoots;
Gia_Man_t * pCopy;
int i, Entry;
// the new AIG orders flops and PIs in the "natural" order
vOrder = Gia_VtaCollect( p, &vFraLims, &vRoots );
......@@ -497,6 +503,10 @@ Gia_Man_t * Gia_VtaTest( Gia_Man_t * p )
Gia_ManObjNum(p) - Gia_ManCoNum(p) - Vec_IntSize(vOrder),
Vec_IntSize(vFraLims) - 1 );
Vec_IntForEachEntry( vFraLims, Entry, i )
printf( "%d=%d ", i, Entry );
printf( "\n" );
pCopy = Gia_VtaDup( p, vOrder );
// Gia_ManStopP( &pCopy );
......
src/aig/gia/module.make
......@@ -4,6 +4,7 @@ SRC += src/aig/gia/gia.c \
src/aig/gia/giaAig.c \
src/aig/gia/giaAiger.c \
src/aig/gia/giaBidec.c \
src/aig/gia/giaCCof.c \
src/aig/gia/giaCof.c \
src/aig/gia/giaCSatOld.c \
src/aig/gia/giaCSat.c \
......
src/base/abci/abc.c
......@@ -383,6 +383,7 @@ static int Abc_CommandAbc9GlaDerive ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9GlaCba ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9GlaPba ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Reparam ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9BackReach ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Posplit ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9ReachM ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9ReachP ( Abc_Frame_t * pAbc, int argc, char ** argv );
......@@ -839,6 +840,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&gla_cba", Abc_CommandAbc9GlaCba, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&gla_pba", Abc_CommandAbc9GlaPba, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&reparam", Abc_CommandAbc9Reparam, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&back_reach", Abc_CommandAbc9BackReach, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&posplit", Abc_CommandAbc9Posplit, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&reachm", Abc_CommandAbc9ReachM, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&reachp", Abc_CommandAbc9ReachP, 0 );
......@@ -26256,13 +26258,16 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Gia_ManFrames2( Gia_Man_t * pAig, Gia_ParFra_t * pPars );
Gia_Man_t * pTemp;
Gia_ParFra_t Pars, * pPars = &Pars;
int c;
int nCofFanLit = 0;
int nNewAlgo = 1;
Gia_ManFraSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FLivh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "FLiavh" ) ) != EOF )
{
switch ( c )
{
......@@ -26291,6 +26296,9 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'i':
pPars->fInit ^= 1;
break;
case 'a':
nNewAlgo ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
......@@ -26312,17 +26320,20 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( nCofFanLit )
pTemp = Gia_ManUnrollAndCofactor( pAbc->pGia, pPars->nFrames, nCofFanLit, pPars->fVerbose );
else
else if ( nNewAlgo )
pTemp = Gia_ManFrames2( pAbc->pGia, pPars );
else
pTemp = Gia_ManFrames( pAbc->pGia, pPars );
Abc_CommandUpdate9( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &frames [-FL <num>] [-ivh]\n" );
Abc_Print( -2, "usage: &frames [-FL <num>] [-aivh]\n" );
Abc_Print( -2, "\t unrolls the design for several timeframes\n" );
Abc_Print( -2, "\t-F num : the number of frames to unroll [default = %d]\n", pPars->nFrames );
Abc_Print( -2, "\t-L num : the limit on fanout count of resets/enables to cofactor [default = %d]\n", nCofFanLit );
Abc_Print( -2, "\t-i : toggle initializing registers [default = %s]\n", pPars->fInit? "yes": "no" );
Abc_Print( -2, "\t-a : toggle using new algorithm [default = %s]\n", nNewAlgo? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
......@@ -29434,6 +29445,98 @@ usage:
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9BackReach( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Gia_ManCofTest( Gia_Man_t * pGia, int nFrameMax, int nConfMax, int nTimeMax, int fVerbose );
Gia_Man_t * pTemp = NULL;
int c, fVerbose = 0;
int nFrameMax = 1000000;
int nConfMax = 1000000;
int nTimeMax = 10;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FCTvh" ) ) != EOF )
{
switch ( c )
{
case 'F':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
nFrameMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nFrameMax < 0 )
goto usage;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
nConfMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nConfMax < 0 )
goto usage;
break;
case 'T':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage;
}
nTimeMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nTimeMax < 0 )
goto usage;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9BackReach(): There is no AIG.\n" );
return 1;
}
if ( Gia_ManPoNum(pAbc->pGia) != 1 )
{
Abc_Print( -1, "Abc_CommandAbc9BackReach(): The number of POs is different from 1.\n" );
return 1;
}
pTemp = Gia_ManCofTest( pAbc->pGia, nFrameMax, nConfMax, nTimeMax, fVerbose );
Abc_CommandUpdate9( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &back_reach [-FCT <num>] [-vh]\n" );
Abc_Print( -2, "\t performs input trimming and reparameterization\n" );
Abc_Print( -2, "\t-F num : the limit on the depth of induction [default = %d]\n", nFrameMax );
Abc_Print( -2, "\t-C num : the conflict limit at a node during induction [default = %d]\n", nConfMax );
Abc_Print( -2, "\t-T num : the timeout for property directed reachability [default = %d]\n", nTimeMax );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9Posplit( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Aig_Man_t * Aig_ManSplit( Aig_Man_t * p, int nVars, int fVerbose );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment