Skip to content

A
abc
Commit 3c25decf by Alan Mishchenko
Options

Version abc50828

parent 28db025b
Showing with 458 additions and 182 deletions
abc.dsp
......@@ -1036,6 +1036,18 @@ SOURCE=.\src\sat\sim\simUnate.c
SOURCE=.\src\sat\sim\simUtils.c
# End Source File
# End Group
# Begin Group "csat"
# PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\sat\csat\csat_apis.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\csat\csat_apis.h
# End Source File
# End Group
# End Group
# Begin Group "opt"
......
abc.opt
No preview for this file type
src/base/abc/abc.c
......@@ -1065,6 +1065,11 @@ int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( Abc_NtkIsAig(pNtk) )
{
fprintf( pErr, "Cleanup cannot be performed on the AIG.\n" );
return 1;
}
// modify the current network
Abc_NtkCleanup( pNtk, 0 );
......
src/base/abc/abc.h
......@@ -406,6 +406,7 @@ extern Abc_Ntk_t * Abc_NtkStartRead( char * pName );
extern void Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk );
extern Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk );
extern Abc_Ntk_t * Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAllCis );
extern Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * vValues );
extern void Abc_NtkDelete( Abc_Ntk_t * pNtk );
extern void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk );
extern Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj );
......@@ -532,10 +533,13 @@ extern void Abc_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk );
/*=== abcSop.c ==========================================================*/
extern char * Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName );
extern char * Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars );
extern char * Abc_SopCreateConst0( Extra_MmFlex_t * pMan );
extern char * Abc_SopCreateConst1( Extra_MmFlex_t * pMan );
extern char * Abc_SopCreateAnd2( Extra_MmFlex_t * pMan, int fCompl0, int fCompl1 );
extern char * Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars );
extern char * Abc_SopCreateNand( Extra_MmFlex_t * pMan, int nVars );
extern char * Abc_SopCreateOr( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
extern char * Abc_SopCreateOrMultiCube( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
extern char * Abc_SopCreateNor( Extra_MmFlex_t * pMan, int nVars );
extern char * Abc_SopCreateXor( Extra_MmFlex_t * pMan, int nVars );
extern char * Abc_SopCreateNxor( Extra_MmFlex_t * pMan, int nVars );
......@@ -559,6 +563,7 @@ extern void Abc_SopWriteCnf( FILE * pFile, char * pClauses, Vec_In
extern void Abc_SopAddCnfToSolver( solver * pSat, char * pClauses, Vec_Int_t * vVars, Vec_Int_t * vTemp );
/*=== abcStrash.c ==========================================================*/
extern Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes );
extern Abc_Obj_t * Abc_NodeStrash( Abc_Aig_t * pMan, Abc_Obj_t * pNode );
extern Abc_Obj_t * Abc_NodeStrashDec( Abc_Aig_t * pMan, Vec_Ptr_t * vFanins, Vec_Int_t * vForm );
extern int Abc_NodeStrashDecCount( Abc_Aig_t * pMan, Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins, Vec_Int_t * vForm, Vec_Int_t * vLevels, int NodeMax, int LevelMax );
extern int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
......
src/base/abc/abcAig.c
......@@ -172,6 +172,10 @@ Abc_Aig_t * Abc_AigDup( Abc_Aig_t * pMan, Abc_Aig_t * pManNew )
Abc_ObjSetFaninL0( pObj->pCopy, Abc_ObjFaninL0(pObj) );
Abc_ObjSetFaninL1( pObj->pCopy, Abc_ObjFaninL1(pObj) );
}
// relink the choice nodes
Vec_PtrForEachEntry( vNodes, pObj, i )
if ( pObj->pData )
pObj->pCopy->pData = ((Abc_Obj_t *)pObj->pData)->pCopy;
Vec_PtrFree( vNodes );
// relink the CO nodes
Abc_NtkForEachCo( pMan->pNtkAig, pObj, i )
......
src/base/abc/abcCheck.c
......@@ -361,7 +361,8 @@ bool Abc_NtkCheckPos( Abc_Ntk_t * pNtk )
bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
{
Abc_Obj_t * pFanin, * pFanout;
int i, k, Value = 1;
int i, Value = 1;
// int k;
// check the network
if ( pObj->pNtk != pNtk )
......@@ -395,7 +396,7 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
Value = 0;
}
}
/*
// make sure fanins are not duplicated
for ( i = 0; i < pObj->vFanins.nSize; i++ )
for ( k = i + 1; k < pObj->vFanins.nSize; k++ )
......@@ -417,7 +418,7 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
printf( "Warning: Node %s has", Abc_ObjName(pObj) );
printf( " duplicated fanout %s.\n", Abc_ObjName(Abc_ObjFanout(pObj,k)) );
}
*/
return Value;
}
......
src/base/abc/abcCreate.c
......@@ -333,7 +333,64 @@ Abc_Ntk_t * Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAll
Abc_NtkLogicStoreName( pNode->pCopy, Abc_ObjName(pNode) );
if ( !Abc_NtkCheck( pNtkNew ) )
fprintf( stdout, "Abc_NtkDup(): Network check has failed.\n" );
fprintf( stdout, "Abc_NtkSplitOutput(): Network check has failed.\n" );
return pNtkNew;
}
/**Function*************************************************************
Synopsis [Creates the network composed of one output.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * vValues )
{
Vec_Ptr_t * vNodes;
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pObj, * pFinal, * pOther, * pNodePo;
int i;
assert( Abc_NtkIsLogic(pNtk) );
// start the network
Abc_NtkCleanCopy( pNtk );
pNtkNew = Abc_NtkAlloc( ABC_NTK_AIG );
pNtkNew->pName = util_strsav(pNtk->pName);
// collect the nodes in the TFI of the output
vNodes = Abc_NtkDfsNodes( pNtk, (Abc_Obj_t **)vRoots->pArray, vRoots->nSize );
// create the PIs
Abc_NtkForEachCi( pNtk, pObj, i )
{
pObj->pCopy = Abc_NtkCreatePi(pNtkNew);
Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) );
}
// copy the nodes
Vec_PtrForEachEntry( vNodes, pObj, i )
pObj->pCopy = Abc_NodeStrash( pNtkNew->pManFunc, pObj );
Vec_PtrFree( vNodes );
// add the PO
pFinal = Abc_AigConst1( pNtkNew->pManFunc );
Vec_PtrForEachEntry( vRoots, pObj, i )
{
pOther = pObj->pCopy;
if ( Vec_IntEntry(vValues, i) == 0 )
pOther = Abc_ObjNot(pOther);
pFinal = Abc_AigAnd( pNtkNew->pManFunc, pFinal, pOther );
}
// add the PO corresponding to this output
pNodePo = Abc_NtkCreatePo( pNtkNew );
Abc_ObjAddFanin( pNodePo, pFinal );
Abc_NtkLogicStoreName( pNodePo, "miter" );
if ( !Abc_NtkCheck( pNtkNew ) )
fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" );
return pNtkNew;
}
......
src/base/abc/abcFraig.c
......@@ -89,7 +89,7 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA
ProgressBar * pProgress;
Fraig_Node_t * pNodeFraig;
Vec_Ptr_t * vNodes;
Abc_Obj_t * pNode, * pConst1;
Abc_Obj_t * pNode, * pConst1, * pReset;
int i;
assert( Abc_NtkIsAig(pNtk) );
......@@ -102,6 +102,7 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA
Abc_NtkForEachCi( pNtk, pNode, i )
pNode->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, i);
pConst1 = Abc_AigConst1( pNtk->pManFunc );
pReset = Abc_AigReset( pNtk->pManFunc );
// perform strashing
vNodes = Abc_AigDfs( pNtk, fAllNodes, 0 );
......@@ -111,6 +112,8 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA
Extra_ProgressBarUpdate( pProgress, i, NULL );
if ( pNode == pConst1 )
pNodeFraig = Fraig_ManReadConst1(pMan);
else if ( pNode == pReset )
continue;
else
pNodeFraig = Fraig_NodeAnd( pMan,
Fraig_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ),
......
src/base/abc/abcNetlist.c
......@@ -254,22 +254,25 @@ Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk )
if ( !Abc_NodeIsAigChoice(pObj) )
continue;
// create an OR gate
pNodeNew = Abc_NtkCreateNode(pNtk);
pNodeNew = Abc_NtkCreateNode(pNtkNew);
// add fanins
Vec_IntClear( pNtk->vIntTemp );
for ( k = 0, pFanin = pObj; pFanin; pFanin = pFanin->pData, k++ )
for ( pFanin = pObj; pFanin; pFanin = pFanin->pData )
{
Vec_IntPush( pNtk->vIntTemp, (int)(pObj->fPhase != pFanin->fPhase) );
Abc_ObjAddFanin( pNodeNew, pFanin->pCopy );
}
// create the logic function
pNodeNew->pData = Abc_SopCreateOr( pNtk->pManFunc, pNtk->vIntTemp->nSize, pNtk->vIntTemp->pArray );
pNodeNew->pData = Abc_SopCreateOrMultiCube( pNtkNew->pManFunc, pNtk->vIntTemp->nSize, pNtk->vIntTemp->pArray );
// set the new node
pObj->pCopy = pNodeNew;
pObj->pCopy->pCopy = pNodeNew;
}
// connect the internal nodes
Abc_NtkForEachNode( pNtk, pObj, i )
Abc_ObjForEachFanin( pObj, pFanin, k )
if ( pFanin->pCopy->pCopy )
Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy->pCopy );
else
Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
// connect the COs
Abc_NtkFinalize( pNtk, pNtkNew );
......
src/base/abc/abcSop.c
......@@ -92,7 +92,39 @@ char * Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars )
/**Function*************************************************************
Synopsis [Starts the constant 1 cover with the given number of variables and cubes.]
Synopsis [Starts the constant 1 cover with 0 variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Abc_SopCreateConst1( Extra_MmFlex_t * pMan )
{
return Abc_SopRegister( pMan, " 1\n" );
}
/**Function*************************************************************
Synopsis [Starts the constant 1 cover with 0 variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Abc_SopCreateConst0( Extra_MmFlex_t * pMan )
{
return Abc_SopRegister( pMan, " 0\n" );
}
/**Function*************************************************************
Synopsis [Starts the AND2 cover.]
Description []
......@@ -115,7 +147,7 @@ char * Abc_SopCreateAnd2( Extra_MmFlex_t * pMan, int fCompl0, int fCompl1 )
/**Function*************************************************************
Synopsis [Starts the constant 1 cover with the given number of variables and cubes.]
Synopsis [Starts the multi-input AND cover.]
Description []
......@@ -136,7 +168,7 @@ char * Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars )
/**Function*************************************************************
Synopsis [Starts the constant 1 cover with the given number of variables and cubes.]
Synopsis [Starts the multi-input NAND cover.]
Description []
......@@ -158,7 +190,7 @@ char * Abc_SopCreateNand( Extra_MmFlex_t * pMan, int nVars )
/**Function*************************************************************
Synopsis [Starts the constant 1 cover with the given number of variables and cubes.]
Synopsis [Starts the multi-input OR cover.]
Description []
......@@ -180,7 +212,32 @@ char * Abc_SopCreateOr( Extra_MmFlex_t * pMan, int nVars, int * pfCompl )
/**Function*************************************************************
Synopsis [Starts the constant 1 cover with the given number of variables and cubes.]
Synopsis [Starts the multi-input OR cover.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Abc_SopCreateOrMultiCube( Extra_MmFlex_t * pMan, int nVars, int * pfCompl )
{
char * pSop, * pCube;
int i;
pSop = Abc_SopStart( pMan, nVars, nVars );
i = 0;
Abc_SopForEachCube( pSop, nVars, pCube )
{
pCube[i] = '1' - (pfCompl? pfCompl[i] : 0);
i++;
}
return pSop;
}
/**Function*************************************************************
Synopsis [Starts the multi-input NOR cover.]
Description []
......@@ -201,7 +258,7 @@ char * Abc_SopCreateNor( Extra_MmFlex_t * pMan, int nVars )
/**Function*************************************************************
Synopsis [Starts the constant 1 cover with the given number of variables and cubes.]
Synopsis [Starts the multi-input XOR cover.]
Description []
......@@ -218,7 +275,7 @@ char * Abc_SopCreateXor( Extra_MmFlex_t * pMan, int nVars )
/**Function*************************************************************
Synopsis [Starts the constant 1 cover with the given number of variables and cubes.]
Synopsis [Starts the multi-input XNOR cover.]
Description []
......@@ -235,7 +292,7 @@ char * Abc_SopCreateNxor( Extra_MmFlex_t * pMan, int nVars )
/**Function*************************************************************
Synopsis [Starts the constant 1 cover with the given number of variables and cubes.]
Synopsis [Starts the inv cover.]
Description []
......@@ -251,7 +308,7 @@ char * Abc_SopCreateInv( Extra_MmFlex_t * pMan )
/**Function*************************************************************
Synopsis [Starts the constant 1 cover with the given number of variables and cubes.]
Synopsis [Starts the buf cover.]
Description []
......@@ -367,18 +424,11 @@ int Abc_SopGetPhase( char * pSop )
int Abc_SopGetIthCareLit( char * pSop, int i )
{
char * pCube;
int nVars, c;
int nVars;
nVars = Abc_SopGetVarNum( pSop );
for ( c = 0; ; c++ )
{
// get the cube
pCube = pSop + c * (nVars + 3);
if ( *pCube == 0 )
break;
// get the literal
Abc_SopForEachCube( pSop, nVars, pCube )
if ( pCube[i] != '-' )
return pCube[i] - '0';
}
return -1;
}
......@@ -520,6 +570,8 @@ bool Abc_SopIsAndType( char * pSop )
for ( pCur = pSop; *pCur != ' '; pCur++ )
if ( *pCur == '-' )
return 0;
if ( pCur[1] != '1' )
return 0;
return 1;
}
......@@ -537,14 +589,12 @@ bool Abc_SopIsAndType( char * pSop )
bool Abc_SopIsOrType( char * pSop )
{
char * pCube, * pCur;
int nVars, nLits, c;
int nVars, nLits;
nVars = Abc_SopGetVarNum( pSop );
for ( c = 0; ; c++ )
if ( nVars != Abc_SopGetCubeNum(pSop) )
return 0;
Abc_SopForEachCube( pSop, nVars, pCube )
{
// get the cube
pCube = pSop + c * (nVars + 3);
if ( *pCube == 0 )
break;
// count the number of literals in the cube
nLits = 0;
for ( pCur = pCube; *pCur != ' '; pCur++ )
......
src/base/abc/abcStrash.c
......@@ -28,7 +28,6 @@
// static functions
static void Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fAllNodes );
static Abc_Obj_t * Abc_NodeStrash( Abc_Aig_t * pMan, Abc_Obj_t * pNode );
static Abc_Obj_t * Abc_NodeStrashSop( Abc_Aig_t * pMan, Abc_Obj_t * pNode, char * pSop );
static Abc_Obj_t * Abc_NodeStrashFactor( Abc_Aig_t * pMan, Abc_Obj_t * pNode, char * pSop );
......
src/base/cmd/cmd.c
......@@ -335,7 +335,7 @@ int CmdCommandHistory( Abc_Frame_t * pAbc, int argc, char **argv )
int i, num;
int size;
int c;
num = 30;
num = 50;
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
......
src/csat_apis.h deleted 100644 → 0
//These are the APIs, enums and data structures that we use
//and expect from our use of CSAT.
enum GateType
{
// GateType defines the gate type that can be added to circuit by
// CSAT_AddGate();
enum GateType
{
CSAT_CONST = 0, // constant gate
CSAT_BPI, // boolean PI
CSAT_BPPI, // bit level PSEUDO PRIMARY INPUT
CSAT_BAND, // bit level AND
CSAT_BNAND, // bit level NAND
CSAT_BOR, // bit level OR
CSAT_BNOR, // bit level NOR
CSAT_BXOR, // bit level XOR
CSAT_BXNOR, // bit level XNOR
CSAT_BINV, // bit level INVERTER
CSAT_BBUF, // bit level BUFFER
CSAT_BPPO, // bit level PSEUDO PRIMARY OUTPUT
CSAT_BPO, // boolean PO
};
#endif
//CSAT_StatusT defines the return value by CSAT_Solve();
#ifndef _CSAT_STATUS_
#define _CSAT_STATUS_
enum CSAT_StatusT
{
UNDETERMINED = 0,
UNSATISFIABLE,
SATISFIABLE,
TIME_OUT,
FRAME_OUT,
NO_TARGET,
ABORTED,
SEQ_SATISFIABLE
};
#endif
// CSAT_OptionT defines the solver option about learning
// which is used by CSAT_SetSolveOption();
#ifndef _CSAT_OPTION_
#define _CSAT_OPTION_
enum CSAT_OptionT
{
BASE_LINE = 0,
IMPLICT_LEARNING, //default
EXPLICT_LEARNING
};
#endif
#ifndef _CSAT_Target_Result
#define _CSAT_Target_Result
typedef struct _CSAT_Target_ResultT CSAT_Target_ResultT;
/*
struct _CSAT_Target_ResultT
{
enum CSAT_StatusT status; //solve status of the target
int num_dec; //num of decisions to solve the target
int num_imp; //num of implications to solve the target
int num_cftg; //num of conflict gates learned
int num_cfts; //num of conflict signals in conflict gates
double time; //time(in second) used to solver the target
int no_sig; // if "status" is SATISFIABLE, "no_sig" is the number of
// primary inputs, if the "status" is TIME_OUT, "no_sig" is the
// number of constant signals found.
char** names; // if the "status" is SATISFIABLE, "names" is the name array of
// primary inputs, "values" is the value array of primary
// inputs that satisfy the target.
// if the "status" is TIME_OUT, "names" is the name array of
// constant signals found (signals at the root of decision
// tree),"values" is the value array of constant signals found.
int* values;
};
*/
// create a new manager
CSAT_Manager CSAT_InitManager(void);
// set solver options for learning
void CSAT_SetSolveOption(CSAT_Manager mng,enum CSAT_OptionT option);
// add a gate to the circuit
// the meaning of the parameters are:
// type: the type of the gate to be added
// name: the name of the gate to be added, name should be unique in a circuit.
// nofi: number of fanins of the gate to be added;
// fanins: the name array of fanins of the gate to be added
int CSAT_AddGate(CSAT_Manager mng,
enum GateType type,
char* name,
int nofi,
char** fanins,
int dc_attr=0);
// check if there are gates that are not used by any primary ouput.
// if no such gates exist, return 1 else return 0;
int CSAT_Check_Integrity(CSAT_Manager mng);
// set time limit for solving a target.
// runtime: time limit (in second).
void CSAT_SetTimeLimit(CSAT_Manager mng ,int runtime);
void CSAT_SetLearnLimit (CSAT_Manager mng ,int num);
void CSAT_SetSolveBacktrackLimit (CSAT_Manager mng ,int num);
void CSAT_SetLearnBacktrackLimit (CSAT_Manager mng ,int num);
void CSAT_EnableDump(CSAT_Manager mng ,char* dump_file);
// the meaning of the parameters are:
// nog: number of gates that are in the targets
// names: name array of gates
// values: value array of the corresponding gates given in "names" to be
// solved. the relation of them is AND.
int CSAT_AddTarget(CSAT_Manager mng, int nog, char**names, int* values);
// initialize the solver internal data structure.
void CSAT_SolveInit(CSAT_Manager mng);
void CSAT_AnalyzeTargets(CSAT_Manager mng);
// solve the targets added by CSAT_AddTarget()
enum CSAT_StatusT CSAT_Solve(CSAT_Manager mng);
// get the solve status of a target
// TargetID: the target id returned by CSAT_AddTarget().
CSAT_Target_ResultT*
CSAT_Get_Target_Result(CSAT_Manager mng, int TargetID);
void CSAT_Dump_Bench_File(CSAT_Manager mng);
src/opt/rwr/rwr.h
......@@ -125,7 +125,6 @@ extern void Rwr_ManIncTravId( Rwr_Man_t * p );
extern Rwr_Man_t * Rwr_ManStart( bool fPrecompute );
extern void Rwr_ManStop( Rwr_Man_t * p );
extern void Rwr_ManPrintStats( Rwr_Man_t * p );
extern void Rwr_ManPrepareNetwork( Rwr_Man_t * p, Abc_Ntk_t * pNtk );
extern Vec_Ptr_t * Rwr_ManReadFanins( Rwr_Man_t * p );
extern Vec_Int_t * Rwr_ManReadDecs( Rwr_Man_t * p );
extern int Rwr_ManReadCompl( Rwr_Man_t * p );
......
src/opt/rwr/rwrMan.c
......@@ -164,27 +164,6 @@ void Rwr_ManPrintStats( Rwr_Man_t * p )
/**Function*************************************************************
Synopsis [Assigns elementary cuts to the PIs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Rwr_ManPrepareNetwork( Rwr_Man_t * p, Abc_Ntk_t * pNtk )
{
// save the fanout counters for all internal nodes
// p->vFanNums = Rwt_NtkFanoutCounters( pNtk );
// precompute the required times for all internal nodes
// p->vReqTimes = Abc_NtkGetRequiredLevels( pNtk );
// start the cut computation
// Rwr_NtkStartCuts( p, pNtk );
}
/**Function*************************************************************
Synopsis [Stops the resynthesis manager.]
Description []
......
src/sat/csat/csat_apis.h 0 → 100644
/**CFile****************************************************************
FileName [csat_apis.h]
PackageName [Interface to CSAT.]
Synopsis [APIs, enums, and data structures expected from the use of CSAT.]
Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - August 28, 2005]
Revision [$Id: csat_apis.h,v 1.00 2005/08/28 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __CSAT_APIS_H__
#define __CSAT_APIS_H__
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// STRUCTURE DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct CSAT_ManagerStruct_t CSAT_Manager_t;
typedef struct CSAT_ManagerStruct_t * CSAT_Manager;
// GateType defines the gate type that can be added to circuit by
// CSAT_AddGate();
#ifndef _CSAT_GATE_TYPE_
#define _CSAT_GATE_TYPE_
enum GateType
{
CSAT_CONST = 0, // constant gate
CSAT_BPI, // boolean PI
CSAT_BPPI, // bit level PSEUDO PRIMARY INPUT
CSAT_BAND, // bit level AND
CSAT_BNAND, // bit level NAND
CSAT_BOR, // bit level OR
CSAT_BNOR, // bit level NOR
CSAT_BXOR, // bit level XOR
CSAT_BXNOR, // bit level XNOR
CSAT_BINV, // bit level INVERTER
CSAT_BBUF, // bit level BUFFER
CSAT_BPPO, // bit level PSEUDO PRIMARY OUTPUT
CSAT_BPO // boolean PO
};
#endif
//CSAT_StatusT defines the return value by CSAT_Solve();
#ifndef _CSAT_STATUS_
#define _CSAT_STATUS_
enum CSAT_StatusT
{
UNDETERMINED = 0,
UNSATISFIABLE,
SATISFIABLE,
TIME_OUT,
FRAME_OUT,
NO_TARGET,
ABORTED,
SEQ_SATISFIABLE
};
#endif
// CSAT_OptionT defines the solver option about learning
// which is used by CSAT_SetSolveOption();
#ifndef _CSAT_OPTION_
#define _CSAT_OPTION_
enum CSAT_OptionT
{
BASE_LINE = 0,
IMPLICT_LEARNING, //default
EXPLICT_LEARNING
};
#endif
#ifndef _CSAT_Target_Result
#define _CSAT_Target_Result
typedef struct _CSAT_Target_ResultT CSAT_Target_ResultT;
struct _CSAT_Target_ResultT
{
enum CSAT_StatusT status; // solve status of the target
int num_dec; // num of decisions to solve the target
int num_imp; // num of implications to solve the target
int num_cftg; // num of conflict gates learned
int num_cfts; // num of conflict signals in conflict gates
double time; // time(in second) used to solve the target
int no_sig; // if "status" is SATISFIABLE, "no_sig" is the number of
// primary inputs, if the "status" is TIME_OUT, "no_sig" is the
// number of constant signals found.
char** names; // if the "status" is SATISFIABLE, "names" is the name array of
// primary inputs, "values" is the value array of primary
// inputs that satisfy the target.
// if the "status" is TIME_OUT, "names" is the name array of
// constant signals found (signals at the root of decision
// tree), "values" is the value array of constant signals found.
int* values;
};
#endif
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
// create a new manager
extern CSAT_Manager CSAT_InitManager(void);
// set solver options for learning
extern void CSAT_SetSolveOption(CSAT_Manager mng, enum CSAT_OptionT option);
// add a gate to the circuit
// the meaning of the parameters are:
// type: the type of the gate to be added
// name: the name of the gate to be added, name should be unique in a circuit.
// nofi: number of fanins of the gate to be added;
// fanins: the name array of fanins of the gate to be added
extern int CSAT_AddGate(CSAT_Manager mng,
enum GateType type,
char* name,
int nofi,
char** fanins,
int dc_attr);
// check if there are gates that are not used by any primary ouput.
// if no such gates exist, return 1 else return 0;
extern int CSAT_Check_Integrity(CSAT_Manager mng);
// set time limit for solving a target.
// runtime: time limit (in second).
extern void CSAT_SetTimeLimit(CSAT_Manager mng, int runtime);
extern void CSAT_SetLearnLimit(CSAT_Manager mng, int num);
extern void CSAT_SetSolveBacktrackLimit(CSAT_Manager mng, int num);
extern void CSAT_SetLearnBacktrackLimit(CSAT_Manager mng, int num);
extern void CSAT_EnableDump(CSAT_Manager mng, char* dump_file);
// the meaning of the parameters are:
// nog: number of gates that are in the targets
// names: name array of gates
// values: value array of the corresponding gates given in "names" to be
// solved. the relation of them is AND.
extern int CSAT_AddTarget(CSAT_Manager mng, int nog, char**names, int* values);
// initialize the solver internal data structure.
extern void CSAT_SolveInit(CSAT_Manager mng);
extern void CSAT_AnalyzeTargets(CSAT_Manager mng);
// solve the targets added by CSAT_AddTarget()
extern enum CSAT_StatusT CSAT_Solve(CSAT_Manager mng);
// get the solve status of a target
// TargetID: the target id returned by CSAT_AddTarget().
extern CSAT_Target_ResultT * CSAT_Get_Target_Result(CSAT_Manager mng, int TargetID);
extern void CSAT_Dump_Bench_File(CSAT_Manager mng);
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
#endif
src/sat/fraig/fraig.h
......@@ -97,6 +97,7 @@ extern int Fraig_ManReadFeedBack( Fraig_Man_t * p );
extern int Fraig_ManReadDoSparse( Fraig_Man_t * p );
extern int Fraig_ManReadChoicing( Fraig_Man_t * p );
extern int Fraig_ManReadVerbose( Fraig_Man_t * p );
extern int * Fraig_ManReadModel( Fraig_Man_t * p );
extern void Fraig_ManSetFuncRed( Fraig_Man_t * p, int fFuncRed );
extern void Fraig_ManSetFeedBack( Fraig_Man_t * p, int fFeedBack );
......@@ -157,6 +158,7 @@ extern int Fraig_CountLevels( Fraig_Man_t * pMan );
extern int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit );
extern int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit );
extern void Fraig_ManProveMiter( Fraig_Man_t * p );
extern int Fraig_ManCheckMiter( Fraig_Man_t * p );
/*=== fraigVec.c ===============================================================*/
extern Fraig_NodeVec_t * Fraig_NodeVecAlloc( int nCap );
......
src/sat/fraig/fraigApi.c
......@@ -57,6 +57,7 @@ int Fraig_ManReadFeedBack( Fraig_Man_t * p ) {
int Fraig_ManReadDoSparse( Fraig_Man_t * p ) { return p->fDoSparse; }
int Fraig_ManReadChoicing( Fraig_Man_t * p ) { return p->fChoicing; }
int Fraig_ManReadVerbose( Fraig_Man_t * p ) { return p->fVerbose; }
int * Fraig_ManReadModel( Fraig_Man_t * p ) { return p->pModel; }
/**Function*************************************************************
......
src/sat/fraig/fraigFeed.c
......@@ -765,6 +765,47 @@ void Fraig_ReallocateSimulationInfo( Fraig_Man_t * p )
p->pSimsDiff = (unsigned *)Fraig_MemFixedEntryFetch( mmSimsNew );
}
/**Function*************************************************************
Synopsis [Doubles the size of simulation info.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int * Fraig_ManSaveCounterExample( Fraig_Man_t * p, Fraig_Node_t * pNode )
{
int * pModel = NULL;
int iPattern;
int i;
iPattern = Fraig_FindFirstDiff( p->pConst1, pNode, p->nWordsDyna, 0 );
if ( iPattern >= 0 )
{
pModel = ALLOC( int, p->vInputs->nSize );
memset( pModel, 0, sizeof(int) * p->vInputs->nSize );
for ( i = 0; i < p->vInputs->nSize; i++ )
if ( Fraig_BitStringHasBit( p->vInputs->pArray[i]->puSimD, iPattern ) )
pModel[i] = 1;
return pModel;
}
iPattern = Fraig_FindFirstDiff( p->pConst1, pNode, p->nWordsRand, 1 );
if ( iPattern >= 0 )
{
pModel = ALLOC( int, p->vInputs->nSize );
memset( pModel, 0, sizeof(int) * p->vInputs->nSize );
for ( i = 0; i < p->vInputs->nSize; i++ )
if ( Fraig_BitStringHasBit( p->vInputs->pArray[i]->puSimR, iPattern ) )
pModel[i] = 1;
return pModel;
}
return pModel;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/sat/fraig/fraigInt.h
......@@ -178,6 +178,7 @@ struct Fraig_ManStruct_t_
Msat_Solver_t * pSat; // the SAT solver
Msat_IntVec_t * vProj; // the temporary array of projection vars
int nSatNums; // the counter of SAT variables
int * pModel; // the assignment, which satisfies the miter
// these arrays belong to the solver
Msat_IntVec_t * vVarsInt; // the temporary array of variables
Msat_ClauseVec_t * vAdjacents; // the temporary storage for connectivity
......@@ -378,6 +379,7 @@ extern void Fraig_FeedBackInit( Fraig_Man_t * p );
extern void Fraig_FeedBack( Fraig_Man_t * p, int * pModel, Msat_IntVec_t * vVars, Fraig_Node_t * pOld, Fraig_Node_t * pNew );
extern void Fraig_FeedBackTest( Fraig_Man_t * p );
extern int Fraig_FeedBackCompress( Fraig_Man_t * p );
extern int * Fraig_ManSaveCounterExample( Fraig_Man_t * p, Fraig_Node_t * pNode );
/*=== fraigMem.c =============================================================*/
extern Fraig_MemFixed_t * Fraig_MemFixedStart( int nEntrySize );
extern void Fraig_MemFixedStop( Fraig_MemFixed_t * p, int fVerbose );
......@@ -404,6 +406,7 @@ extern Fraig_Node_t * Fraig_HashTableLookupF0( Fraig_Man_t * pMan, Fraig_No
extern void Fraig_HashTableInsertF0( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
extern int Fraig_CompareSimInfo( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand );
extern int Fraig_CompareSimInfoUnderMask( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand, unsigned * puMask );
extern int Fraig_FindFirstDiff( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand );
extern void Fraig_CollectXors( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand, unsigned * puMask );
extern void Fraig_TablePrintStatsS( Fraig_Man_t * pMan );
extern void Fraig_TablePrintStatsF( Fraig_Man_t * pMan );
......
src/sat/fraig/fraigMan.c
......@@ -171,6 +171,7 @@ void Fraig_ManFree( Fraig_Man_t * p )
if ( p->vProj ) Msat_IntVecFree( p->vProj );
if ( p->vCones ) Fraig_NodeVecFree( p->vCones );
if ( p->vPatsReal ) Msat_IntVecFree( p->vPatsReal );
if ( p->pModel ) free( p->pModel );
Fraig_MemFixedStop( p->mmNodes, 0 );
Fraig_MemFixedStop( p->mmSims, 0 );
......
src/sat/fraig/fraigSat.c
......@@ -111,6 +111,31 @@ void Fraig_ManProveMiter( Fraig_Man_t * p )
/**Function*************************************************************
Synopsis [Returns 1 if the miter is unsat; 0 if sat; -1 if undecided.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fraig_ManCheckMiter( Fraig_Man_t * p )
{
if ( p->vOutputs->pArray[0] == Fraig_Not(p->pConst1) )
return 1;
// save the counter example
FREE( p->pModel );
p->pModel = Fraig_ManSaveCounterExample( p, Fraig_Regular(p->vOutputs->pArray[0]) );
// if the model is not found, return undecided
if ( p->pModel == NULL )
return -1;
return 0;
}
/**Function*************************************************************
Synopsis [Checks whether two nodes are functinally equivalent.]
Description [The flag (fComp) tells whether the nodes to be checked
......
src/sat/fraig/fraigTable.c
......@@ -373,6 +373,43 @@ int Fraig_CompareSimInfo( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWor
/**Function*************************************************************
Synopsis [Find the number of the different pattern.]
Description [Returns -1 if there is no such pattern]
SideEffects []
SeeAlso []
***********************************************************************/
int Fraig_FindFirstDiff( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand )
{
int i, v;
assert( !Fraig_IsComplement(pNode1) );
assert( !Fraig_IsComplement(pNode2) );
if ( fUseRand )
{
// check the simulation info
for ( i = 0; i < iWordLast; i++ )
if ( pNode1->puSimR[i] != pNode2->puSimR[i] )
for ( v = 0; v < 32; v++ )
if ( (pNode1->puSimR[i] ^ pNode2->puSimR[i]) & (1 << v) )
return i * 32 + v;
}
else
{
// check the simulation info
for ( i = 0; i < iWordLast; i++ )
if ( pNode1->puSimD[i] != pNode2->puSimD[i] )
for ( v = 0; v < 32; v++ )
if ( (pNode1->puSimD[i] ^ pNode2->puSimD[i]) & (1 << v) )
return i * 32 + v;
}
return -1;
}
/**Function*************************************************************
Synopsis [Compares two pieces of simulation info.]
Description [Returns 1 if they are equal.]
......
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