luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

update rrr

This commit is contained in:
MyskYko 2025-04-17 11:01:39 -07:00
parent 27f2429d76
commit b1b1023285
17 changed files with 1548 additions and 679 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/aig/gia/giaRrr.cpp
View File

@ -35,7 +35,7 @@ Gia_Man_t *Gia_ManRrr(Gia_Man_t *pGia, int iSeed, int nWords, int nTimeout, int
Par.fOptOnInsert = fOptOnInsert;
Par.fGreedy = fGreedy;
rrr::Perform(&ntk, &Par);
Gia_Man_t *pNew = rrr::CreateGia(&ntk);
Gia_Man_t *pNew = rrr::CreateGia(&ntk, false);
return pNew;
}

57
src/base/abci/abc.c
View File

@ -45457,7 +45457,7 @@ int Abc_CommandAbc9Rrr( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t *pNew;
int c;
int iSeed = 0, nWords = 10, nTimeout = 0, nSchedulerVerbose = 1, nPartitionerVerbose = 0, nOptimizerVerbose = 0, nAnalyzerVerbose = 0, nSimulatorVerbose = 0, nSatSolverVerbose = 0, fUseBddCspf = 0, fUseBddMspf = 0, nConflictLimit = 0, nSortType = -1, nOptimizerFlow = 0, nSchedulerFlow = 0, nPartitionType = 0, nDistance = 0, nJobs = 1, nThreads = 1, nPartitionSize = 0, nPartitionSizeMin = 0, fDeterministic = 1, nParallelPartitions = 1, fOptOnInsert = 0, fGreedy = 1;
int iSeed = 0, nWords = 10, nTimeout = 0, nSchedulerVerbose = 0, nPartitionerVerbose = 0, nOptimizerVerbose = 0, nAnalyzerVerbose = 0, nSimulatorVerbose = 0, nSatSolverVerbose = 0, fUseBddCspf = 0, fUseBddMspf = 0, nConflictLimit = 0, nSortType = -1, nOptimizerFlow = 0, nSchedulerFlow = 0, nPartitionType = 0, nDistance = 0, nJobs = 1, nThreads = 1, nPartitionSize = 0, nPartitionSizeMin = 0, fDeterministic = 1, nParallelPartitions = 1, fOptOnInsert = 0, fGreedy = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "XYZNJKLBDRWTCGVPOAQSabdegh" ) ) != EOF )
{
@ -45576,6 +45576,51 @@ int Abc_CommandAbc9Rrr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
if ( nSchedulerVerbose )
{
Abc_Print( 2, "Using the following parameters :\n" );
Abc_Print( 2, "\t-X %3d : method ", nOptimizerFlow );
switch( nOptimizerFlow )
{
case 0:
Abc_Print( 2, "(0 = single-add resub)" );
break;
case 1:
Abc_Print( 2, "(1 = multi-add resub)" );
break;
case 2:
Abc_Print( 2, "(2 = repeat single-add and multi-add resubs)" );
break;
case 3:
Abc_Print( 2, "(3 = random one meaningful resub)" );
break;
}
Abc_Print( 2, "\n" );
Abc_Print( 2, "\t-Y %3d : flow ", nSchedulerFlow );
switch ( nSchedulerFlow )
{
case 0:
Abc_Print( 2, "(0 = apply method once)" );
break;
case 1:
Abc_Print( 2, "(1 = iterate like transtoch)" );
break;
case 2:
Abc_Print( 2, "(2 = iterate like deepsyn)" );
break;
}
Abc_Print( 2, "\n" );
Abc_Print( 2, "\t-N %3d : number of jobs to create by restarting or partitioning\n", nJobs );
Abc_Print( 2, "\t-J %3d : number of threads\n", nThreads );
Abc_Print( 2, "\t-K %3d : maximum partition size (0 = no partitioning)\n", nPartitionSize );
Abc_Print( 2, "\t-L %3d : minimum partition size\n", nPartitionSizeMin );
Abc_Print( 2, "\t-B %3d : maximum number of partitions to optimize in parallel\n", nParallelPartitions );
Abc_Print( 2, "\t-R %3d : random number generator seed\n", iSeed );
Abc_Print( 2, "\t-T %3d : timeout in seconds (0 = no timeout)\n", nTimeout );
Abc_Print( 2, "\t-C %3d : conflict limit (0 = no limit)\n", nConflictLimit );
Abc_Print( 2, "Use command line switch \"-h\" to see more options\n\n" );
}
pNew = Gia_ManRrr( pAbc->pGia, iSeed, nWords, nTimeout, nSchedulerVerbose, nPartitionerVerbose, nOptimizerVerbose, nAnalyzerVerbose, nSimulatorVerbose, nSatSolverVerbose, fUseBddCspf, fUseBddMspf, nConflictLimit, nSortType, nOptimizerFlow, nSchedulerFlow, nPartitionType, nDistance, nJobs, nThreads, nPartitionSize, nPartitionSizeMin, fDeterministic, nParallelPartitions, fOptOnInsert, fGreedy );
Abc_FrameUpdateGia( pAbc, pNew );
@ -45599,10 +45644,10 @@ usage:
Abc_Print( -2, "\t 1: level base\n" );
Abc_Print( -2, "\t-N num : number of jobs to create by restarting or partitioning [default = %d]\n", nJobs );
Abc_Print( -2, "\t-J num : number of threads [default = %d]\n", nThreads );
Abc_Print( -2, "\t-K num : partition size (0 = no partitioning) [default = %d]\n", nPartitionSize );
Abc_Print( -2, "\t-K num : minimum partition size [default = %d]\n", nPartitionSizeMin );
Abc_Print( -2, "\t-B num : max number of partitions in parallel [default = %d]\n", nParallelPartitions );
Abc_Print( -2, "\t-D num : distance between nodes (0 = no limit) [default = %d]\n", nDistance );
Abc_Print( -2, "\t-K num : maximum partition size (0 = no partitioning) [default = %d]\n", nPartitionSize );
Abc_Print( -2, "\t-L num : minimum partition size [default = %d]\n", nPartitionSizeMin );
Abc_Print( -2, "\t-B num : maximum number of partitions in parallel [default = %d]\n", nParallelPartitions );
Abc_Print( -2, "\t-D num : maximum distance between node and new fanin (0 = no limit) [default = %d]\n", nDistance );
Abc_Print( -2, "\t-R num : random number generator seed [default = %d]\n", iSeed );
Abc_Print( -2, "\t-W num : number of simulation words [default = %d]\n", nWords );
Abc_Print( -2, "\t-T num : timeout in seconds (0 = no timeout) [default = %d]\n", nTimeout );
@ -45617,7 +45662,7 @@ usage:
Abc_Print( -2, "\t-a : use BDD-based analyzer (CSPF) [default = %s]\n", fUseBddCspf? "yes": "no" );
Abc_Print( -2, "\t-b : use BDD-based analyzer (MSPF) [default = %s]\n", fUseBddMspf? "yes": "no" );
Abc_Print( -2, "\t-d : ensure deterministic execution [default = %s]\n", fDeterministic? "yes": "no" );
Abc_Print( -2, "\t-e : apply c2rs; dc2 after importing changes of partitions [default = %s]\n", fOptOnInsert? "yes": "no" );
Abc_Print( -2, "\t-e : apply \"c2rs; dc2\" after importing changes of partitions [default = %s]\n", fOptOnInsert? "yes": "no" );
Abc_Print( -2, "\t-g : discard changes that increased the cost [default = %s]\n", fGreedy? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;

16
src/opt/rrr/rrrAbc.h
View File

@ -29,9 +29,11 @@ namespace rrr {
}
template <typename Ntk>
Gia_Man_t *CreateGia(Ntk *pNtk) {
Gia_Man_t *CreateGia(Ntk *pNtk, bool fHash = true) {
Gia_Man_t *pGia = Gia_ManStart(pNtk->GetNumNodes());
Gia_ManHashStart(pGia);
if(fHash) {
Gia_ManHashStart(pGia);
}
std::vector<int> v(pNtk->GetNumNodes());
v[0] = Gia_ManConst0Lit();
pNtk->ForEachPi([&](int id) {
@ -43,8 +45,10 @@ namespace rrr {
pNtk->ForEachFanin(id, [&](int fi, bool c) {
if(x == -1) {
x = Abc_LitNotCond(v[fi], c);
} else {
} else if(fHash) {
x = Gia_ManHashAnd(pGia, x, Abc_LitNotCond(v[fi], c));
} else {
x = Gia_ManAppendAnd(pGia, x, Abc_LitNotCond(v[fi], c));
}
});
if(x == -1) {
@ -55,7 +59,9 @@ namespace rrr {
pNtk->ForEachPoDriver([&](int fi, bool c) {
Gia_ManAppendCo(pGia, Abc_LitNotCond(v[fi], c));
});
Gia_ManHashStop(pGia);
if(fHash) {
Gia_ManHashStop(pGia);
}
return pGia;
}
@ -72,7 +78,7 @@ namespace rrr {
assert(r == 0);
Abc_FrameSetBatchMode(0);
}
pNtk->Read(Abc_FrameReadGia(pAbc), GiaReader<Ntk>);
pNtk->Read(Abc_FrameReadGia(pAbc), GiaReader<Ntk>, false);
}
}

49
src/opt/rrr/rrrAnalyzer.h
View File

@ -23,11 +23,16 @@ namespace rrr {
public:
// constructors
Analyzer(Parameter const *pPar);
void UpdateNetwork(Ntk *pNtk_, bool fSame);
void AssignNetwork(Ntk *pNtk_, bool fReuse);
// checks
bool CheckRedundancy(int id, int idx);
bool CheckFeasibility(int id, int fi, bool c);
// summary
void ResetSummary();
summary<int> GetStatsSummary() const;
summary<double> GetTimesSummary() const;
};
/* {{{ Constructors */
@ -39,12 +44,12 @@ namespace rrr {
sim(pPar),
sol(pPar) {
}
template <typename Ntk, typename Sim, typename Sol>
void Analyzer<Ntk, Sim, Sol>::UpdateNetwork(Ntk *pNtk_, bool fSame) {
void Analyzer<Ntk, Sim, Sol>::AssignNetwork(Ntk *pNtk_, bool fReuse) {
pNtk = pNtk_;
sim.UpdateNetwork(pNtk, fSame);
sol.UpdateNetwork(pNtk, fSame);
sim.AssignNetwork(pNtk, fReuse);
sol.AssignNetwork(pNtk, fReuse);
}
/* }}} */
@ -70,6 +75,10 @@ namespace rrr {
}
sim.AddCex(sol.GetCex());
}
} else {
// if(nVerbose) {
// std::cout << "node " << id << " fanin " << (pNtk->GetCompl(id, idx)? "!": "") << pNtk->GetFanin(id, idx) << " index " << idx << " is not redundant" << std::endl;
// }
}
return false;
}
@ -93,11 +102,41 @@ namespace rrr {
}
sim.AddCex(sol.GetCex());
}
} else {
// if(nVerbose) {
// std::cout << "node " << id << " fanin " << (c? "!": "") << fi << " is not feasible" << std::endl;
// }
}
return false;
}
/* }}} */
/* {{{ Summary */
template <typename Ntk, typename Sim, typename Sol>
void Analyzer<Ntk, Sim, Sol>::ResetSummary() {
sim.ResetSummary();
sol.ResetSummary();
}
template <typename Ntk, typename Sim, typename Sol>
summary<int> Analyzer<Ntk, Sim, Sol>::GetStatsSummary() const {
summary<int> v = sim.GetStatsSummary();
summary<int> v2 = sol.GetStatsSummary();
v.insert(v.end(), v2.begin(), v2.end());
return v;
}
template <typename Ntk, typename Sim, typename Sol>
summary<double> Analyzer<Ntk, Sim, Sol>::GetTimesSummary() const {
summary<double> v = sim.GetTimesSummary();
summary<double> v2 = sol.GetTimesSummary();
v.insert(v.end(), v2.begin(), v2.end());
return v;
}
/* }}} */
}

36
src/opt/rrr/rrrAndNetwork.h
View File

@ -64,13 +64,13 @@ namespace rrr {
AndNetwork &operator=(AndNetwork const &x);
// initialization APIs (should not be called after optimization has started)
void Clear();
void Clear(bool fClearCallbacks = true);
void Reserve(int nReserve);
int AddPi();
int AddAnd(int id0, int id1, bool c0, bool c1);
int AddPo(int id, bool c);
template <typename Ntk, typename Reader>
void Read(Ntk *pFrom, Reader &reader);
void Read(Ntk *pFrom, Reader &reader, bool fNew = true);
// network properties
bool UseComplementedEdges() const;
@ -78,6 +78,7 @@ namespace rrr {
int GetNumPis() const;
int GetNumInts() const;
int GetNumPos() const;
int GetNumLevels() const;
int GetConst0() const;
int GetPi(int idx) const;
int GetPo(int idx) const;
@ -272,7 +273,7 @@ namespace rrr {
/* {{{ Initialization APIs */
void AndNetwork::Clear() {
void AndNetwork::Clear(bool fClearCallbacks) {
nNodes = 0;
vPis.clear();
lInts.clear();
@ -284,7 +285,9 @@ namespace rrr {
iTrav = 0;
vTrav.clear();
fPropagating = false;
vCallbacks.clear();
if(fClearCallbacks) {
vCallbacks.clear();
}
vBackups.clear();
// add constant node
vvFaninEdges.emplace_back();
@ -330,9 +333,13 @@ namespace rrr {
}
template <typename Ntk, typename Reader>
void AndNetwork::Read(Ntk *pFrom, Reader &reader) {
Clear();
void AndNetwork::Read(Ntk *pFrom, Reader &reader, bool fNew) {
Clear(false);
reader(pFrom, this);
Action action;
action.type = READ;
action.fNew = fNew;
TakenAction(action);
}
/* }}} */
@ -359,6 +366,23 @@ namespace rrr {
return int_size(vPos);
}
int AndNetwork::GetNumLevels() const {
int nMaxLevel = 0;
std::vector<int> vLevels(nNodes);
ForEachInt([&](int id) {
ForEachFanin(id, [&](int fi) {
if(vLevels[id] < vLevels[fi]) {
vLevels[id] = vLevels[fi];
}
});
vLevels[id] += 1;
if(nMaxLevel < vLevels[id]) {
nMaxLevel = vLevels[id];
}
});
return nMaxLevel;
}
inline int AndNetwork::GetConst0() const {
return 0;
}

448
src/opt/rrr/rrrBddAnalyzer.h
View File

@ -22,6 +22,7 @@ namespace rrr {
int nVerbose;
// data
bool fInitialized;
NewBdd::Man *pBdd;
int target;
std::vector<lit> vFs;
@ -35,6 +36,14 @@ namespace rrr {
// backups
std::vector<BddAnalyzer> vBackups;
// stats
uint64_t nNodesOld;
uint64_t nNodesAccumulated;
double durationSimulation;
double durationPf;
double durationCheck;
double durationReorder;
// BDD utils
void IncRef(lit x) const;
void DecRef(lit x) const;
@ -61,6 +70,10 @@ namespace rrr {
void CspfNode(int id);
void Cspf(int id = -1, bool fC = true);
// preparation
void Reset(bool fReuse = false);
void Initialize();
// save & load
void Save(int slot);
void Load(int slot);
@ -71,11 +84,16 @@ namespace rrr {
BddAnalyzer();
BddAnalyzer(Parameter const *pPar);
~BddAnalyzer();
void UpdateNetwork(Ntk *pNtk_, bool fSame);
void AssignNetwork(Ntk *pNtk_, bool fReuse);
// checks
bool CheckRedundancy(int id, int idx);
bool CheckFeasibility(int id, int fi, bool c);
// summary
void ResetSummary();
summary<int> GetStatsSummary() const;
summary<double> GetTimesSummary() const;
};
/* {{{ BDD utils */
@ -163,103 +181,136 @@ namespace rrr {
void BddAnalyzer<Ntk>::ActionCallback(Action const &action) {
switch(action.type) {
case REMOVE_FANIN:
assert(fInitialized);
vUpdates[action.id] = true;
vGUpdates[action.fi] = true;
DecRef(vvCs[action.id][action.idx]);
vvCs[action.id].erase(vvCs[action.id].begin() + action.idx);
if(target != action.id) {
// require resimulate before next fesibility check
// (this is not mandatory if no pending updates are in TFI of new fanin, but we would rather update than checking every time)
target = -1;
}
break;
case REMOVE_UNUSED:
if(vGUpdates[action.id] || vCUpdates[action.id]) {
if(fInitialized) {
if(vGUpdates[action.id] || vCUpdates[action.id]) {
for(int fi: action.vFanins) {
vGUpdates[fi] = true;
}
}
Assign(vFs[action.id], LitMax);
Assign(vGs[action.id], LitMax);
DelVec(vvCs[action.id]);
}
break;
case REMOVE_BUFFER:
if(fInitialized) {
if(vUpdates[action.id]) {
for(int fo: action.vFanouts) {
vUpdates[fo] = true;
vCUpdates[fo] = true;
}
}
if(vGUpdates[action.id] || vCUpdates[action.id]) {
vGUpdates[action.fi] = true;
}
Assign(vFs[action.id], LitMax);
Assign(vGs[action.id], LitMax);
DelVec(vvCs[action.id]);
}
break;
case REMOVE_CONST:
if(fInitialized) {
if(vUpdates[action.id]) {
for(int fo: action.vFanouts) {
vUpdates[fo] = true;
vCUpdates[fo] = true;
}
}
for(int fi: action.vFanins) {
vGUpdates[fi] = true;
}
Assign(vFs[action.id], LitMax);
Assign(vGs[action.id], LitMax);
DelVec(vvCs[action.id]);
}
Assign(vFs[action.id], LitMax);
Assign(vGs[action.id], LitMax);
DelVec(vvCs[action.id]);
break;
case REMOVE_BUFFER:
if(vUpdates[action.id]) {
for(int fo: action.vFanouts) {
vUpdates[fo] = true;
vCUpdates[fo] = true;
}
}
if(vGUpdates[action.id] || vCUpdates[action.id]) {
vGUpdates[action.fi] = true;
}
Assign(vFs[action.id], LitMax);
Assign(vGs[action.id], LitMax);
DelVec(vvCs[action.id]);
break;
case REMOVE_CONST:
if(vUpdates[action.id]) {
for(int fo: action.vFanouts) {
vUpdates[fo] = true;
vCUpdates[fo] = true;
}
}
for(int fi: action.vFanins) {
vGUpdates[fi] = true;
}
Assign(vFs[action.id], LitMax);
Assign(vGs[action.id], LitMax);
DelVec(vvCs[action.id]);
break;
case ADD_FANIN:
assert(action.id == target);
assert(fInitialized);
vUpdates[action.id] = true;
vCUpdates[action.id] = true;
vvCs[action.id].insert(vvCs[action.id].begin() + action.idx, LitMax);
break;
case TRIVIAL_COLLAPSE: {
if(vGUpdates[action.fi] || vCUpdates[action.fi]) {
case TRIVIAL_COLLAPSE:
if(fInitialized) {
if(vGUpdates[action.fi] || vCUpdates[action.fi]) {
vCUpdates[action.id] = true;
}
std::vector<lit>::iterator it = vvCs[action.id].begin() + action.idx;
DecRef(*it);
it = vvCs[action.id].erase(it);
vvCs[action.id].insert(it, vvCs[action.fi].begin(), vvCs[action.fi].end());
vvCs[action.fi].clear();
Assign(vFs[action.fi], LitMax);
Assign(vGs[action.fi], LitMax);
}
break;
case TRIVIAL_DECOMPOSE:
if(fInitialized) {
Allocate();
SimulateNode(action.fi, vFs);
// time of this simulation is not measured for simplicity sake
assert(vGs[action.fi] == LitMax);
Assign(vGs[action.fi], vGs[action.id]);
std::vector<lit>::iterator it = vvCs[action.id].begin() + action.idx;
assert(vvCs[action.fi].empty());
vvCs[action.fi].insert(vvCs[action.fi].begin(), it, vvCs[action.id].end());
vvCs[action.id].erase(it, vvCs[action.id].end());
assert(vvCs[action.id].size() == action.idx);
vvCs[action.id].resize(action.idx + 1, LitMax);
Assign(vvCs[action.id][action.idx], vGs[action.fi]);
vUpdates[action.fi] = false;
vGUpdates[action.fi] = false;
vCUpdates[action.fi] = vCUpdates[action.id];
}
break;
case SORT_FANINS:
if(fInitialized) {
std::vector<lit> vCs = vvCs[action.id];
vvCs[action.id].clear();
for(int index: action.vIndices) {
vvCs[action.id].push_back(vCs[index]);
}
if(!fResim) {
fResim = true;
/* commenting out the following because it might not be worth checking
// if sorted node is in TFO of functionally updated nodes, resimulation is required
std::vector<int> vFanouts;
pNtk->ForEachInt([&](int id) {
if(vUpdates[id]) {
pNtk->ForEachFanout(id, false, [&](int fo) {
vFanouts.push_back(fo);
});
}
});
pNtk->ForEachTfos(vFanouts, false, [&](int fo) {
if(fResim) {
return;
}
if(fo == action.id) {
fResim = true;
}
});
*/
}
vCUpdates[action.id] = true;
}
std::vector<lit>::iterator it = vvCs[action.id].begin() + action.idx;
DecRef(*it);
it = vvCs[action.id].erase(it);
vvCs[action.id].insert(it, vvCs[action.fi].begin(), vvCs[action.fi].end());
vvCs[action.fi].clear();
Assign(vFs[action.fi], LitMax);
Assign(vGs[action.fi], LitMax);
break;
}
case TRIVIAL_DECOMPOSE: {
Allocate();
SimulateNode(action.fi, vFs);
assert(vGs[action.fi] == LitMax);
Assign(vGs[action.fi], vGs[action.id]);
std::vector<lit>::iterator it = vvCs[action.id].begin() + action.idx;
assert(vvCs[action.fi].empty());
vvCs[action.fi].insert(vvCs[action.fi].begin(), it, vvCs[action.id].end());
vvCs[action.id].erase(it, vvCs[action.id].end());
assert(vvCs[action.id].size() == action.idx);
vvCs[action.id].resize(action.idx + 1, LitMax);
Assign(vvCs[action.id][action.idx], vGs[action.fi]);
vUpdates[action.fi] = false;
vGUpdates[action.fi] = false;
vCUpdates[action.fi] = vCUpdates[action.id];
case READ:
Reset(!action.fNew);
break;
}
case SORT_FANINS: {
std::vector<lit> vCs = vvCs[action.id];
vvCs[action.id].clear();
for(int index: action.vIndices) {
vvCs[action.id].push_back(vCs[index]);
}
if(!fResim && target != -1 && target != action.id) {
pNtk->ForEachTfo(target, false, [&](int fo) {
if(fResim) {
return;
}
if(fo == action.id) {
fResim = true;
}
});
}
vCUpdates[action.id] = true;
break;
}
case SAVE:
Save(action.idx);
break;
@ -306,6 +357,7 @@ namespace rrr {
template <typename Ntk>
void BddAnalyzer<Ntk>::Simulate() {
time_point timeStart = GetCurrentTime();
if(nVerbose) {
std::cout << "symbolic simulation with BDD" << std::endl;
}
@ -324,6 +376,7 @@ namespace rrr {
vUpdates[id] = false;
}
});
durationSimulation += Duration(timeStart, GetCurrentTime());
}
/* }}} */
@ -410,6 +463,7 @@ namespace rrr {
template <typename Ntk>
void BddAnalyzer<Ntk>::Cspf(int id, bool fC) {
time_point timeStart = GetCurrentTime();
if(id != -1) {
pNtk->ForEachTfoReverse(id, false, [&](int fo) {
CspfNode(fo);
@ -427,10 +481,82 @@ namespace rrr {
CspfNode(id);
});
}
durationPf += Duration(timeStart, GetCurrentTime());
}
/* }}} */
/* {{{ Preparation */
template <typename Ntk>
void BddAnalyzer<Ntk>::Reset(bool fReuse) {
while(!vBackups.empty()) {
PopBack();
}
DelVec(vFs);
DelVec(vGs);
DelVecVec(vvCs);
fInitialized = false;
target = -1;
fResim = false;
vUpdates.clear();
vGUpdates.clear();
vCUpdates.clear();
if(!fReuse) {
nNodesOld = 0;
if(pBdd) {
nNodesAccumulated += pBdd->GetNumTotalCreatedNodes();
}
delete pBdd;
pBdd = NULL;
}
}
template <typename Ntk>
void BddAnalyzer<Ntk>::Initialize() {
bool fUseReo = false;
if(!pBdd) {
NewBdd::Param Par;
Par.nObjsMaxLog = 25;
Par.nCacheMaxLog = 20;
Par.fCountOnes = false;
Par.nGbc = 1;
Par.nReo = 4000;
pBdd = new NewBdd::Man(pNtk->GetNumPis(), Par);
fUseReo = true;
}
assert(pBdd->GetNumVars() == pNtk->GetNumPis());
Allocate();
Assign(vFs[0], pBdd->Const0());
int idx = 0;
pNtk->ForEachPi([&](int id) {
Assign(vFs[id], pBdd->IthVar(idx));
idx++;
});
pNtk->ForEachInt([&](int id) {
vUpdates[id] = true;
});
Simulate();
if(fUseReo) {
time_point timeStart = GetCurrentTime();
pBdd->Reorder();
pBdd->TurnOffReo();
durationReorder += Duration(timeStart, GetCurrentTime());
}
pNtk->ForEachInt([&](int id) {
vvCs[id].resize(pNtk->GetNumFanins(id), LitMax);
});
pNtk->ForEachPo([&](int id) {
vvCs[id].resize(1, LitMax);
Assign(vvCs[id][0], pBdd->Const0());
int fi = pNtk->GetFanin(id, 0);
vGUpdates[fi] = true;
});
fInitialized = true;
}
/* }}} */
/* {{{ Save & load */
template <typename Ntk>
@ -468,7 +594,7 @@ namespace rrr {
vBackups.pop_back();
}
/* }}} Save & load end */
/* }}} */
/* {{{ Constructors */
@ -476,93 +602,34 @@ namespace rrr {
BddAnalyzer<Ntk>::BddAnalyzer() :
pNtk(NULL),
nVerbose(0),
fInitialized(false),
pBdd(NULL),
target(-1),
fResim(false) {
ResetSummary();
}
template <typename Ntk>
BddAnalyzer<Ntk>::BddAnalyzer(Parameter const *pPar) :
pNtk(NULL),
nVerbose(pPar->nAnalyzerVerbose),
fInitialized(false),
pBdd(NULL),
target(-1),
fResim(false) {
}
template <typename Ntk>
void BddAnalyzer<Ntk>::UpdateNetwork(Ntk *pNtk_, bool fSame) {
// clear
while(!vBackups.empty()) {
PopBack();
}
DelVec(vFs);
DelVec(vGs);
DelVecVec(vvCs);
pNtk = pNtk_;
target = -1;
fResim = false;
vUpdates.clear();
vGUpdates.clear();
vCUpdates.clear();
// alloc
bool fUseReo = false;
if(!pBdd || pBdd->GetNumVars() != pNtk->GetNumPis()) {
// need to reset manager
delete pBdd;
NewBdd::Param Par;
Par.nObjsMaxLog = 25;
Par.nCacheMaxLog = 20;
Par.fCountOnes = true;
Par.nGbc = 1;
Par.nReo = 4000;
pBdd = new NewBdd::Man(pNtk->GetNumPis(), Par);
fUseReo = true;
} else if(!fSame) {
// turning on reordering if network function changed
pBdd->TurnOnReo();
fUseReo = true;
}
Allocate();
// prepare
Assign(vFs[0], pBdd->Const0());
int idx = 0;
pNtk->ForEachPi([&](int id) {
Assign(vFs[id], pBdd->IthVar(idx));
idx++;
});
pNtk->ForEachInt([&](int id) {
vUpdates[id] = true;
});
Simulate();
if(fUseReo) {
pBdd->Reorder();
pBdd->TurnOffReo();
}
pNtk->ForEachInt([&](int id) {
vvCs[id].resize(pNtk->GetNumFanins(id), LitMax);
});
pNtk->ForEachPo([&](int id) {
vvCs[id].resize(1, LitMax);
Assign(vvCs[id][0], pBdd->Const0());
int fi = pNtk->GetFanin(id, 0);
vGUpdates[fi] = true;
});
pNtk->AddCallback(std::bind(&BddAnalyzer<Ntk>::ActionCallback, this, std::placeholders::_1));
ResetSummary();
}
template <typename Ntk>
BddAnalyzer<Ntk>::~BddAnalyzer() {
while(!vBackups.empty()) {
PopBack();
}
DelVec(vFs);
DelVec(vGs);
DelVecVec(vvCs);
if(pBdd) {
pBdd->PrintStats();
}
delete pBdd;
Reset();
}
template <typename Ntk>
void BddAnalyzer<Ntk>::AssignNetwork(Ntk *pNtk_, bool fReuse) {
Reset(fReuse);
pNtk = pNtk_;
pNtk->AddCallback(std::bind(&BddAnalyzer<Ntk>::ActionCallback, this, std::placeholders::_1));
}
/* }}} */
@ -571,20 +638,22 @@ namespace rrr {
template <typename Ntk>
bool BddAnalyzer<Ntk>::CheckRedundancy(int id, int idx) {
if(fResim) {
if(!fInitialized) {
Initialize();
} else if(fResim) {
Simulate();
fResim = false;
}
Cspf(id);
time_point timeStart = GetCurrentTime();
bool fRedundant = false;
switch(pNtk->GetNodeType(id)) {
case AND: {
int fi = pNtk->GetFanin(id, idx);
bool c = pNtk->GetCompl(id, idx);
lit x = pBdd->Or(pBdd->LitNotCond(vFs[fi], c), vvCs[id][idx]);
if(pBdd->IsConst1(x)) {
if(nVerbose) {
std::cout << "node " << id << " fanin " << (pNtk->GetCompl(id, idx)? "!": "") << pNtk->GetFanin(id, idx) << " index " << idx << " is redundant" << std::endl;
}
return true;
fRedundant = true;
}
break;
}
@ -592,18 +661,30 @@ namespace rrr {
assert(0);
}
if(nVerbose) {
std::cout << "node " << id << " fanin " << (pNtk->GetCompl(id, idx)? "!": "") << pNtk->GetFanin(id, idx) << " index " << idx << " is NOT redundant" << std::endl;
if(fRedundant) {
std::cout << "node " << id << " fanin " << (pNtk->GetCompl(id, idx)? "!": "") << pNtk->GetFanin(id, idx) << " index " << idx << " is redundant" << std::endl;
} else {
std::cout << "node " << id << " fanin " << (pNtk->GetCompl(id, idx)? "!": "") << pNtk->GetFanin(id, idx) << " index " << idx << " is NOT redundant" << std::endl;
}
}
return false;
durationCheck += Duration(timeStart, GetCurrentTime());
return fRedundant;
}
template <typename Ntk>
bool BddAnalyzer<Ntk>::CheckFeasibility(int id, int fi, bool c) {
if(target != id) { // simualte if there has been update in non-tfo of this node
if(!fInitialized) {
Initialize();
} else if(target != id && (target == -1 || vUpdates[target])) {
// resimulation is required if there are pending updates in TFI of new fanin
// but it seems not worthwhile to check that condition every time
// so we update if pending updates are not only at current target
Simulate();
target = id;
}
target = id;
Cspf(id, false);
time_point timeStart = GetCurrentTime();
bool fFeasible = false;
switch(pNtk->GetNodeType(id)) {
case AND: {
lit x = pBdd->Or(pBdd->LitNot(vFs[id]), vGs[id]);
@ -611,10 +692,7 @@ namespace rrr {
lit y = pBdd->Or(x, pBdd->LitNotCond(vFs[fi], c));
DecRef(x);
if(pBdd->IsConst1(y)) {
if(nVerbose) {
std::cout << "node " << id << " fanin " << (c? "!": "") << fi << " is feasible" << std::endl;
}
return true;
fFeasible = true;
}
break;
}
@ -622,9 +700,49 @@ namespace rrr {
assert(0);
}
if(nVerbose) {
std::cout << "node " << id << " fanin " << (c? "!": "") << fi << " is NOT feasible" << std::endl;
if(fFeasible) {
std::cout << "node " << id << " fanin " << (c? "!": "") << fi << " is feasible" << std::endl;
} else {
std::cout << "node " << id << " fanin " << (c? "!": "") << fi << " is NOT feasible" << std::endl;
}
}
return false;
durationCheck += Duration(timeStart, GetCurrentTime());
return fFeasible;
}
/* }}} */
/* {{{ Summary */
template <typename Ntk>
void BddAnalyzer<Ntk>::ResetSummary() {
if(pBdd) {
nNodesOld = pBdd->GetNumTotalCreatedNodes();
} else {
nNodesOld = 0;
}
nNodesAccumulated = 0;
durationSimulation = 0;
durationPf = 0;
durationCheck = 0;
durationReorder = 0;
}
template <typename Ntk>
summary<int> BddAnalyzer<Ntk>::GetStatsSummary() const {
summary<int> v;
v.emplace_back("bdd node", pBdd->GetNumTotalCreatedNodes() - nNodesOld + nNodesAccumulated);
return v;
}
template <typename Ntk>
summary<double> BddAnalyzer<Ntk>::GetTimesSummary() const {
summary<double> v;
v.emplace_back("bdd symbolic simulation", durationSimulation);
v.emplace_back("bdd care computation", durationPf);
v.emplace_back("bdd check", durationCheck);
v.emplace_back("bdd reorder", durationReorder);
return v;
}
/* }}} */

6
src/opt/rrr/rrrBddManager.h
View File

@ -181,6 +181,7 @@ namespace NewBdd {
bvar nObjs;
bvar nObjsAlloc;
bvar nObjsMax;
unsigned long long nCreatedTotal;
bvar RemovedHead;
int nGbc;
bvar nReo;
@ -396,6 +397,7 @@ namespace NewBdd {
for(; *q; q = vNexts.begin() + *q)
if(VarOfBvar(*q) == v && ThenOfBvar(*q) == x1 && ElseOfBvar(*q) == x0)
return Bvar2Lit(*q);
nCreatedTotal++;
bvar next = *p;
if(nObjs < nObjsAlloc)
*p = nObjs++;
@ -642,6 +644,7 @@ namespace NewBdd {
public:
Man(int nVars_, Param p) {
nCreatedTotal = 0;
nVerbose = p.nVerbose;
// parameter sanity check
if(p.nObjsMaxLog < p.nObjsAllocLog)
@ -840,6 +843,9 @@ namespace NewBdd {
<< "alloc: " << std::setw(10) << nObjsAlloc
<< std::endl;
}
unsigned long long GetNumTotalCreatedNodes() {
return nCreatedTotal;
}
};
}

432
src/opt/rrr/rrrBddMspfAnalyzer.h
View File

@ -22,6 +22,7 @@ namespace rrr {
int nVerbose;
// data
bool fInitialized;
NewBdd::Man *pBdd;
std::vector<lit> vFs;
std::vector<lit> vGs;
@ -35,6 +36,14 @@ namespace rrr {
// backups
std::vector<BddMspfAnalyzer> vBackups;
// stats
uint64_t nNodesOld;
uint64_t nNodesAccumulated;
double durationSimulation;
double durationPf;
double durationCheck;
double durationReorder;
// BDD utils
void IncRef(lit x) const;
void DecRef(lit x) const;
@ -63,6 +72,10 @@ namespace rrr {
void MspfNode(int id);
void Mspf(int id = -1, bool fC = true);
// preparation
void Reset(bool fReuse = false);
void Initialize();
// save & load
void Save(int slot);
void Load(int slot);
@ -73,11 +86,16 @@ namespace rrr {
BddMspfAnalyzer();
BddMspfAnalyzer(Parameter const *pPar);
~BddMspfAnalyzer();
void UpdateNetwork(Ntk *pNtk_, bool fSame);
void AssignNetwork(Ntk *pNtk_, bool fReuse);
// checks
bool CheckRedundancy(int id, int idx);
bool CheckFeasibility(int id, int fi, bool c);
// summary
void ResetSummary();
summary<int> GetStatsSummary() const;
summary<double> GetTimesSummary() const;
};
/* {{{ BDD utils */
@ -165,6 +183,7 @@ namespace rrr {
void BddMspfAnalyzer<Ntk>::ActionCallback(Action const &action) {
switch(action.type) {
case REMOVE_FANIN:
assert(fInitialized);
fUpdate = true;
std::fill(vVisits.begin(), vVisits.end(), false);
vUpdates[action.id] = true;
@ -174,103 +193,117 @@ namespace rrr {
vvCs[action.id].erase(vvCs[action.id].begin() + action.idx);
break;
case REMOVE_UNUSED:
if(vGUpdates[action.id] || vCUpdates[action.id]) {
if(fInitialized) {
if(vGUpdates[action.id] || vCUpdates[action.id]) {
for(int fi: action.vFanins) {
vGUpdates[fi] = true;
}
}
Assign(vGs[action.id], LitMax);
DelVec(vvCs[action.id]);
}
break;
case REMOVE_BUFFER:
if(fInitialized) {
if(vUpdates[action.id]) {
fUpdate = true;
for(int fo: action.vFanouts) {
vUpdates[fo] = true;
vCUpdates[fo] = true;
}
}
if(vGUpdates[action.id] || vCUpdates[action.id]) {
vGUpdates[action.fi] = true;
}
Assign(vGs[action.id], LitMax);
DelVec(vvCs[action.id]);
}
break;
case REMOVE_CONST:
if(fInitialized) {
if(vUpdates[action.id]) {
fUpdate = true;
for(int fo: action.vFanouts) {
vUpdates[fo] = true;
vCUpdates[fo] = true;
}
}
for(int fi: action.vFanins) {
vGUpdates[fi] = true;
}
}
Assign(vGs[action.id], LitMax);
DelVec(vvCs[action.id]);
break;
case REMOVE_BUFFER:
if(vUpdates[action.id]) {
fUpdate = true;
for(int fo: action.vFanouts) {
vUpdates[fo] = true;
vCUpdates[fo] = true;
}
}
if(vGUpdates[action.id] || vCUpdates[action.id]) {
vGUpdates[action.fi] = true;
}
Assign(vGs[action.id], LitMax);
DelVec(vvCs[action.id]);
break;
case REMOVE_CONST:
if(vUpdates[action.id]) {
fUpdate = true;
for(int fo: action.vFanouts) {
vUpdates[fo] = true;
vCUpdates[fo] = true;
}
}
for(int fi: action.vFanins) {
vGUpdates[fi] = true;
}
break;
case ADD_FANIN:
assert(fInitialized);
fUpdate = true;
std::fill(vVisits.begin(), vVisits.end(), false);
vUpdates[action.id] = true;
vCUpdates[action.id] = true;
vvCs[action.id].insert(vvCs[action.id].begin() + action.idx, LitMax);
break;
case TRIVIAL_COLLAPSE: {
if(vGUpdates[action.fi] || vCUpdates[action.fi]) {
vCUpdates[action.id] = true;
}
std::vector<lit>::iterator it = vvCs[action.id].begin() + action.idx;
DecRef(*it);
it = vvCs[action.id].erase(it);
vvCs[action.id].insert(it, vvCs[action.fi].begin(), vvCs[action.fi].end());
vvCs[action.fi].clear();
Assign(vFs[action.fi], LitMax);
Assign(vGs[action.fi], LitMax);
break;
}
case TRIVIAL_DECOMPOSE: {
Allocate();
SimulateNode(action.fi, vFs);
assert(vGs[action.fi] == LitMax);
std::vector<lit>::iterator it = vvCs[action.id].begin() + action.idx;
assert(vvCs[action.fi].empty());
vvCs[action.fi].insert(vvCs[action.fi].begin(), it, vvCs[action.id].end());
vvCs[action.id].erase(it, vvCs[action.id].end());
assert(vvCs[action.id].size() == action.idx);
if(!vGUpdates[action.id] && !vCUpdates[action.id]) {
// recompute here only when updates are unlikely to happen
if(pBdd->IsConst1(vGs[action.id])) {
Assign(vGs[action.fi], pBdd->Const1());
} else {
lit x = pBdd->Const1();
IncRef(x);
for(int idx2 = 0; idx2 < action.idx; idx2++) {
int fi = pNtk->GetFanin(action.id, idx2);
bool c = pNtk->GetCompl(action.id, idx2);
Assign(x, pBdd->And(x, pBdd->LitNotCond(vFs[fi], c)));
}
Assign(vGs[action.fi], pBdd->Or(pBdd->LitNot(x), vGs[action.id]));
DecRef(x);
case TRIVIAL_COLLAPSE:
if(fInitialized) {
if(vGUpdates[action.fi] || vCUpdates[action.fi]) {
vCUpdates[action.id] = true;
}
} else {
// otherwise mark the node for future update
vCUpdates[action.id] = true;
}
vvCs[action.id].resize(action.idx + 1, LitMax);
Assign(vvCs[action.id][action.idx], vGs[action.fi]);
vUpdates[action.fi] = false;
vGUpdates[action.fi] = false;
vCUpdates[action.fi] = false;
break;
}
case SORT_FANINS: {
std::vector<lit> vCs = vvCs[action.id];
vvCs[action.id].clear();
for(int index: action.vIndices) {
vvCs[action.id].push_back(vCs[index]);
std::vector<lit>::iterator it = vvCs[action.id].begin() + action.idx;
DecRef(*it);
it = vvCs[action.id].erase(it);
vvCs[action.id].insert(it, vvCs[action.fi].begin(), vvCs[action.fi].end());
vvCs[action.fi].clear();
Assign(vFs[action.fi], LitMax);
Assign(vGs[action.fi], LitMax);
}
break;
}
case TRIVIAL_DECOMPOSE:
if(fInitialized) {
Allocate();
SimulateNode(action.fi, vFs);
// time of this simulation is not measured for simplicity sake
assert(vGs[action.fi] == LitMax);
std::vector<lit>::iterator it = vvCs[action.id].begin() + action.idx;
assert(vvCs[action.fi].empty());
vvCs[action.fi].insert(vvCs[action.fi].begin(), it, vvCs[action.id].end());
vvCs[action.id].erase(it, vvCs[action.id].end());
assert(vvCs[action.id].size() == action.idx);
if(!vGUpdates[action.id] && !vCUpdates[action.id]) {
// recompute here only when updates are unlikely to happen
if(pBdd->IsConst1(vGs[action.id])) {
Assign(vGs[action.fi], pBdd->Const1());
} else {
lit x = pBdd->Const1();
IncRef(x);
for(int idx2 = 0; idx2 < action.idx; idx2++) {
int fi = pNtk->GetFanin(action.id, idx2);
bool c = pNtk->GetCompl(action.id, idx2);
Assign(x, pBdd->And(x, pBdd->LitNotCond(vFs[fi], c)));
}
Assign(vGs[action.fi], pBdd->Or(pBdd->LitNot(x), vGs[action.id]));
DecRef(x);
}
} else {
// otherwise mark the node for future update
vCUpdates[action.id] = true;
}
vvCs[action.id].resize(action.idx + 1, LitMax);
Assign(vvCs[action.id][action.idx], vGs[action.fi]);
vUpdates[action.fi] = false;
vGUpdates[action.fi] = false;
vCUpdates[action.fi] = false;
}
break;
case SORT_FANINS:
if(fInitialized) {
std::vector<lit> vCs = vvCs[action.id];
vvCs[action.id].clear();
for(int index: action.vIndices) {
vvCs[action.id].push_back(vCs[index]);
}
}
break;
case READ:
Reset(!action.fNew);
break;
case SAVE:
Save(action.idx);
break;
@ -326,6 +359,7 @@ namespace rrr {
template <typename Ntk>
void BddMspfAnalyzer<Ntk>::Simulate() {
time_point timeStart = GetCurrentTime();
if(nVerbose) {
std::cout << "symbolic simulation with BDD" << std::endl;
}
@ -340,6 +374,7 @@ namespace rrr {
vUpdates[id] = false;
}
});
durationSimulation += Duration(timeStart, GetCurrentTime());
}
/* }}} */
@ -507,6 +542,7 @@ namespace rrr {
template <typename pNtk>
void BddMspfAnalyzer<pNtk>::Mspf(int id, bool fC) {
time_point timeStart = GetCurrentTime();
if(id != -1) {
pNtk->ForEachTfoReverse(id, false, [&](int fo) {
MspfNode(fo);
@ -524,10 +560,82 @@ namespace rrr {
MspfNode(id);
});
}
durationPf += Duration(timeStart, GetCurrentTime());
}
/* }}} */
/* {{{ Preparation */
template <typename Ntk>
void BddMspfAnalyzer<Ntk>::Reset(bool fReuse) {
while(!vBackups.empty()) {
PopBack();
}
DelVec(vFs);
DelVec(vGs);
DelVecVec(vvCs);
fInitialized = false;
fUpdate = false;
vUpdates.clear();
vGUpdates.clear();
vCUpdates.clear();
vVisits.clear();
if(!fReuse) {
nNodesOld = 0;
if(pBdd) {
nNodesAccumulated += pBdd->GetNumTotalCreatedNodes();
}
delete pBdd;
pBdd = NULL;
}
}
template <typename Ntk>
void BddMspfAnalyzer<Ntk>::Initialize() {
bool fUseReo = false;
if(!pBdd) {
NewBdd::Param Par;
Par.nObjsMaxLog = 25;
Par.nCacheMaxLog = 20;
Par.fCountOnes = false;
Par.nGbc = 1;
Par.nReo = 4000;
pBdd = new NewBdd::Man(pNtk->GetNumPis(), Par);
fUseReo = true;
}
assert(pBdd->GetNumVars() == pNtk->GetNumPis());
Allocate();
Assign(vFs[0], pBdd->Const0());
int idx = 0;
pNtk->ForEachPi([&](int id) {
Assign(vFs[id], pBdd->IthVar(idx));
idx++;
});
pNtk->ForEachInt([&](int id) {
vUpdates[id] = true;
});
Simulate();
if(fUseReo) {
time_point timeStart = GetCurrentTime();
pBdd->Reorder();
pBdd->TurnOffReo();
durationReorder += Duration(timeStart, GetCurrentTime());
}
pNtk->ForEachInt([&](int id) {
vvCs[id].resize(pNtk->GetNumFanins(id), LitMax);
});
pNtk->ForEachPo([&](int id) {
vvCs[id].resize(1, LitMax);
Assign(vvCs[id][0], pBdd->Const0());
int fi = pNtk->GetFanin(id, 0);
vGUpdates[fi] = true;
});
fInitialized = true;
}
/* }}} */
/* {{{ Save & load */
template <typename Ntk>
@ -575,113 +683,56 @@ namespace rrr {
BddMspfAnalyzer<Ntk>::BddMspfAnalyzer() :
pNtk(NULL),
nVerbose(0),
pBdd(NULL) {
fInitialized(false),
pBdd(NULL),
fUpdate(false) {
ResetSummary();
}
template <typename Ntk>
BddMspfAnalyzer<Ntk>::BddMspfAnalyzer(Parameter const *pPar) :
pNtk(NULL),
nVerbose(pPar->nAnalyzerVerbose),
fInitialized(false),
pBdd(NULL),
fUpdate(false) {
ResetSummary();
}
template <typename Ntk>
void BddMspfAnalyzer<Ntk>::UpdateNetwork(Ntk *pNtk_, bool fSame) {
// clear
while(!vBackups.empty()) {
PopBack();
}
DelVec(vFs);
DelVec(vGs);
DelVecVec(vvCs);
BddMspfAnalyzer<Ntk>::~BddMspfAnalyzer() {
Reset();
}
template <typename Ntk>
void BddMspfAnalyzer<Ntk>::AssignNetwork(Ntk *pNtk_, bool fReuse) {
Reset(fReuse);
pNtk = pNtk_;
fUpdate = false;
vUpdates.clear();
vGUpdates.clear();
vCUpdates.clear();
vVisits.clear();
// alloc
bool fUseReo = false;
if(!pBdd || pBdd->GetNumVars() != pNtk->GetNumPis()) {
// need to reset manager
delete pBdd;
NewBdd::Param Par;
Par.nObjsMaxLog = 25;
Par.nCacheMaxLog = 20;
Par.fCountOnes = false;
Par.nGbc = 1;
Par.nReo = 4000;
pBdd = new NewBdd::Man(pNtk->GetNumPis(), Par);
fUseReo = true;
} else if(!fSame) {
// turning on reordering if network function changed
pBdd->TurnOnReo();
fUseReo = true;
}
Allocate();
// prepare
Assign(vFs[0], pBdd->Const0());
int idx = 0;
pNtk->ForEachPi([&](int id) {
Assign(vFs[id], pBdd->IthVar(idx));
idx++;
});
pNtk->ForEachInt([&](int id) {
vUpdates[id] = true;
});
Simulate();
if(fUseReo) {
pBdd->Reorder();
pBdd->TurnOffReo();
}
pNtk->ForEachInt([&](int id) {
vvCs[id].resize(pNtk->GetNumFanins(id), LitMax);
});
pNtk->ForEachPo([&](int id) {
vvCs[id].resize(1, LitMax);
Assign(vvCs[id][0], pBdd->Const0());
int fi = pNtk->GetFanin(id, 0);
vGUpdates[fi] = true;
});
pNtk->AddCallback(std::bind(&BddMspfAnalyzer<Ntk>::ActionCallback, this, std::placeholders::_1));
}
template <typename Ntk>
BddMspfAnalyzer<Ntk>::~BddMspfAnalyzer() {
while(!vBackups.empty()) {
PopBack();
}
DelVec(vFs);
DelVec(vGs);
DelVecVec(vvCs);
if(pBdd) {
pBdd->PrintStats();
}
delete pBdd;
}
/* }}} */
/* {{{ Checks */
template <typename Ntk>
bool BddMspfAnalyzer<Ntk>::CheckRedundancy(int id, int idx) {
if(fUpdate) {
if(!fInitialized) {
Initialize();
} else if(fUpdate) {
Simulate();
fUpdate = false;
}
Mspf(id);
time_point timeStart = GetCurrentTime();
bool fRedundant = false;
switch(pNtk->GetNodeType(id)) {
case AND: {
int fi = pNtk->GetFanin(id, idx);
bool c = pNtk->GetCompl(id, idx);
lit x = pBdd->Or(pBdd->LitNotCond(vFs[fi], c), vvCs[id][idx]);
if(pBdd->IsConst1(x)) {
if(nVerbose) {
std::cout << "node " << id << " fanin " << (pNtk->GetCompl(id, idx)? "!": "") << pNtk->GetFanin(id, idx) << " index " << idx << " is redundant" << std::endl;
}
return true;
fRedundant = true;
}
break;
}
@ -689,18 +740,27 @@ namespace rrr {
assert(0);
}
if(nVerbose) {
std::cout << "node " << id << " fanin " << (pNtk->GetCompl(id, idx)? "!": "") << pNtk->GetFanin(id, idx) << " index " << idx << " is NOT redundant" << std::endl;
if(fRedundant) {
std::cout << "node " << id << " fanin " << (pNtk->GetCompl(id, idx)? "!": "") << pNtk->GetFanin(id, idx) << " index " << idx << " is redundant" << std::endl;
} else {
std::cout << "node " << id << " fanin " << (pNtk->GetCompl(id, idx)? "!": "") << pNtk->GetFanin(id, idx) << " index " << idx << " is NOT redundant" << std::endl;
}
}
return false;
durationCheck += Duration(timeStart, GetCurrentTime());
return fRedundant;
}
template <typename Ntk>
bool BddMspfAnalyzer<Ntk>::CheckFeasibility(int id, int fi, bool c) {
if(fUpdate) {
if(!fInitialized) {
Initialize();
} else if(fUpdate) {
Simulate();
fUpdate = false;
}
Mspf(id, false);
time_point timeStart = GetCurrentTime();
bool fFeasible = false;
switch(pNtk->GetNodeType(id)) {
case AND: {
lit x = pBdd->Or(pBdd->LitNot(vFs[id]), vGs[id]);
@ -708,9 +768,7 @@ namespace rrr {
lit y = pBdd->Or(x, pBdd->LitNotCond(vFs[fi], c));
DecRef(x);
if(pBdd->IsConst1(y)) {
if(nVerbose) {
std::cout << "node " << id << " fanin " << (c? "!": "") << fi << " is feasible" << std::endl;
}
fFeasible = true;
return true;
}
break;
@ -719,9 +777,49 @@ namespace rrr {
assert(0);
}
if(nVerbose) {
std::cout << "node " << id << " fanin " << (c? "!": "") << fi << " is NOT feasible" << std::endl;
if(fFeasible) {
std::cout << "node " << id << " fanin " << (c? "!": "") << fi << " is feasible" << std::endl;
} else {
std::cout << "node " << id << " fanin " << (c? "!": "") << fi << " is NOT feasible" << std::endl;
}
}
return false;
durationCheck += Duration(timeStart, GetCurrentTime());
return fFeasible;
}
/* }}} */
/* {{{ Summary */
template <typename Ntk>
void BddMspfAnalyzer<Ntk>::ResetSummary() {
if(pBdd) {
nNodesOld = pBdd->GetNumTotalCreatedNodes();
} else {
nNodesOld = 0;
}
nNodesAccumulated = 0;
durationSimulation = 0;
durationPf = 0;
durationCheck = 0;
durationReorder = 0;
}
template <typename Ntk>
summary<int> BddMspfAnalyzer<Ntk>::GetStatsSummary() const {
summary<int> v;
v.emplace_back("bdd node", pBdd->GetNumTotalCreatedNodes() - nNodesOld + nNodesAccumulated);
return v;
}
template <typename Ntk>
summary<double> BddMspfAnalyzer<Ntk>::GetTimesSummary() const {
summary<double> v;
v.emplace_back("bdd symbolic simulation", durationSimulation);
v.emplace_back("bdd care computation", durationPf);
v.emplace_back("bdd check", durationCheck);
v.emplace_back("bdd reorder", durationReorder);
return v;
}
/* }}} */

4
src/opt/rrr/rrrLevelBasePartitioner.h
View File

@ -43,7 +43,7 @@ namespace rrr {
public:
// constructors
LevelBasePartitioner(Parameter const *pPar);
void UpdateNetwork(Ntk *pNtk);
void AssignNetwork(Ntk *pNtk);
// APIs
Ntk *Extract(int iSeed);
@ -214,7 +214,7 @@ namespace rrr {
}
template <typename Ntk>
void LevelBasePartitioner<Ntk>::UpdateNetwork(Ntk *pNtk_) {
void LevelBasePartitioner<Ntk>::AssignNetwork(Ntk *pNtk_) {
pNtk = pNtk_;
assert(mSubNtk2Io.empty());
assert(sBlocked.empty());

533
src/opt/rrr/rrrOptimizer.h
View File

@ -21,7 +21,7 @@ namespace rrr {
using citr = std::vector<int>::const_iterator;
using ritr = std::vector<int>::reverse_iterator;
using critr = std::vector<int>::const_reverse_iterator;
// pointer to network
Ntk *pNtk;
@ -35,7 +35,7 @@ namespace rrr {
bool fCompatible;
bool fGreedy;
seconds nTimeout; // assigned upon Run
std::string strVerbosePrefix;
std::function<void(std::string)> PrintLine;
// data
Ana ana;
@ -52,6 +52,11 @@ namespace rrr {
int target;
std::vector<bool> vTfoMarks;
// statistics
struct Stats;
std::map<std::string, Stats> stats;
Stats statsLocal;
// print
template<typename... Args>
void Print(int nVerboseLevel, Args... args);
@ -76,17 +81,18 @@ namespace rrr {
bool ReduceFaninsOneRandom(int id, bool fRemoveUnused = false);
// reduce
bool Reduce();
bool Reduce(bool fSubRoutine = false);
void ReduceRandom();
// remove redundancy
void RemoveRedundancy();
bool RemoveRedundancy();
void RemoveRedundancyRandom();
// addition
template <typename T>
T SingleAdd(int id, T begin, T end);
int MultiAdd(int id, std::vector<int> const &vCands, int nMax = 0);
void Undo();
// resub
void SingleResub(int id, std::vector<int> const &vCands);
@ -108,25 +114,81 @@ namespace rrr {
public:
// constructors
Optimizer(Parameter const *pPar, std::function<double(Ntk *)> CostFunction);
void UpdateNetwork(Ntk *pNtk_, bool fSame = false);
void AssignNetwork(Ntk *pNtk_, bool fReuse = false);
void SetPrintLine(std::function<void(std::string)> const &PrintLine_);
// run
void Run(int iSeed = 0, seconds nTimeout_ = 0);
// summary
void ResetSummary();
summary<int> GetStatsSummary() const;
summary<double> GetTimesSummary() const;
};
/* {{{ Print */
/* {{{ Stats */
template <typename Ntk, typename Ana>
struct Optimizer<Ntk, Ana>::Stats {
int nTriedFis = 0;
int nAddedFis = 0;
int nTried = 0;
int nAdded = 0;
int nChanged = 0;
int nUps = 0;
int nEqs = 0;
int nDowns = 0;
double durationAdd = 0;
double durationReduce = 0;
void Reset() {
nTriedFis = 0;
nAddedFis = 0;
nTried = 0;
nAdded = 0;
nChanged = 0;
nUps = 0;
nEqs = 0;
nDowns = 0;
durationAdd = 0;
durationReduce = 0;
}
Stats& operator+=(Stats const &other) {
this->nTriedFis += other.nTriedFis;
this->nAddedFis += other.nAddedFis;
this->nTried += other.nTried;
this->nAdded += other.nAdded;
this->nChanged += other.nChanged;
this->nUps += other.nUps;
this->nEqs += other.nEqs;
this->nDowns += other.nDowns;
this->durationAdd += other.durationAdd;
this->durationReduce += other.durationReduce;
return *this;
}
std::string GetString() const {
std::stringstream ss;
PrintNext(ss, "tried node/fanin", "=", nTried, "/", nTriedFis, ",", "added node/fanin", "=", nAdded, "/", nAddedFis, ",", "changed", "=", nChanged, ",", "up/eq/dn", "=", nUps, "/", nEqs, "/", nDowns);
return ss.str();
}
};
/* }}} */
/* {{{ Print */
template <typename Ntk, typename Ana>
template <typename... Args>
inline void Optimizer<Ntk, Ana>::Print(int nVerboseLevel, Args... args) {
if(nVerbose > nVerboseLevel) {
std::cout << strVerbosePrefix;
std::stringstream ss;
for(int i = 0; i < nVerboseLevel; i++) {
std::cout << "\t";
ss << "\t";
}
PrintNext(std::cout, args...);
std::cout << std::endl;
PrintNext(ss, args...);
PrintLine(ss.str());
}
}
@ -136,13 +198,13 @@ namespace rrr {
template <typename Ntk, typename Ana>
void Optimizer<Ntk, Ana>::ActionCallback(Action const &action) {
if(nVerbose > 2) {
if(nVerbose > 4) {
std::stringstream ss = GetActionDescription(action);
std::string str;
std::getline(ss, str);
Print(2, str);
Print(4, str);
while(std::getline(ss, str)) {
Print(3, str);
Print(5, str);
}
}
switch(action.type) {
@ -171,6 +233,9 @@ namespace rrr {
break;
case SORT_FANINS:
break;
case READ:
target = -1;
break;
case SAVE:
break;
case LOAD:
@ -482,7 +547,7 @@ namespace rrr {
template <typename Ntk, typename Ana>
inline bool Optimizer<Ntk, Ana>::ReduceFanins(int id, bool fRemoveUnused) {
assert(pNtk->GetNumFanouts(id) > 0);
bool fRemoved = false;
bool fReduced = false;
for(int idx = 0; idx < pNtk->GetNumFanins(id); idx++) {
// skip fanins that were just added
if(mapNewFanins.count(id)) {
@ -495,14 +560,14 @@ namespace rrr {
if(ana.CheckRedundancy(id, idx)) {
int fi = pNtk->GetFanin(id, idx);
pNtk->RemoveFanin(id, idx);
fRemoved = true;
fReduced = true;
idx--;
if(fRemoveUnused && pNtk->GetNumFanouts(fi) == 0) {
pNtk->RemoveUnused(fi, true);
}
}
}
return fRemoved;
return fReduced;
}
/*
@ -542,7 +607,8 @@ namespace rrr {
/* {{{ Reduce */
template <typename Ntk, typename Ana>
bool Optimizer<Ntk, Ana>::Reduce() {
bool Optimizer<Ntk, Ana>::Reduce(bool fSubRoutine) {
time_point timeStart = GetCurrentTime();
bool fReduced = false;
std::vector<int> vInts = pNtk->GetInts();
for(critr it = vInts.rbegin(); it != vInts.rend(); it++) {
@ -558,6 +624,10 @@ namespace rrr {
pNtk->Propagate(*it);
}
}
if(!fSubRoutine) {
time_point timeEnd = GetCurrentTime();
statsLocal.durationReduce += Duration(timeStart, timeEnd);
}
return fReduced;
}
@ -588,35 +658,42 @@ namespace rrr {
/* {{{ Redundancy removal */
template <typename Ntk, typename Ana>
void Optimizer<Ntk, Ana>::RemoveRedundancy() {
bool Optimizer<Ntk, Ana>::RemoveRedundancy() {
time_point timeStart = GetCurrentTime();
bool fReduced = false;
if(fCompatible) {
while(Reduce()) {
while(Reduce(true)) {
fReduced = true;
SortFanins();
}
return;
}
std::vector<int> vInts = pNtk->GetInts();
for(critr it = vInts.rbegin(); it != vInts.rend();) {
if(!pNtk->IsInt(*it)) {
it++;
continue;
}
if(pNtk->GetNumFanouts(*it) == 0) {
pNtk->RemoveUnused(*it);
it++;
continue;
}
SortFanins(*it);
bool fReduced = ReduceFanins(*it);
if(pNtk->GetNumFanins(*it) <= 1) {
pNtk->Propagate(*it);
}
if(fReduced) {
it = vInts.rbegin();
} else {
it++;
} else {
std::vector<int> vInts = pNtk->GetInts();
for(critr it = vInts.rbegin(); it != vInts.rend();) {
if(!pNtk->IsInt(*it)) {
it++;
continue;
}
if(pNtk->GetNumFanouts(*it) == 0) {
pNtk->RemoveUnused(*it);
it++;
continue;
}
SortFanins(*it);
bool fReduced_ = ReduceFanins(*it);
fReduced |= fReduced_;
if(pNtk->GetNumFanins(*it) <= 1) {
pNtk->Propagate(*it);
}
if(fReduced_) {
it = vInts.rbegin();
} else {
it++;
}
}
}
time_point timeEnd = GetCurrentTime();
statsLocal.durationReduce += Duration(timeStart, timeEnd);
return fReduced;
}
/*
@ -656,6 +733,7 @@ namespace rrr {
template <typename Ntk, typename Ana>
template <typename T>
T Optimizer<Ntk, Ana>::SingleAdd(int id, T begin, T end) {
time_point timeStart = GetCurrentTime();
MarkTfo(id);
pNtk->ForEachFanin(id, [&](int fi) {
vTfoMarks[fi] = true;
@ -668,10 +746,13 @@ namespace rrr {
if(vTfoMarks[*it]) {
continue;
}
statsLocal.nTriedFis++;
if(ana.CheckFeasibility(id, *it, false)) {
pNtk->AddFanin(id, *it, false);
statsLocal.nAddedFis++;
} else if(pNtk->UseComplementedEdges() && ana.CheckFeasibility(id, *it, true)) {
pNtk->AddFanin(id, *it, true);
statsLocal.nAddedFis++;
} else {
continue;
}
@ -681,16 +762,19 @@ namespace rrr {
pNtk->ForEachFanin(id, [&](int fi) {
vTfoMarks[fi] = false;
});
time_point timeEnd = GetCurrentTime();
statsLocal.durationAdd += Duration(timeStart, timeEnd);
return it;
}
template <typename Ntk, typename Ana>
int Optimizer<Ntk, Ana>::MultiAdd(int id, std::vector<int> const &vCands, int nMax) {
time_point timeStart = GetCurrentTime();
MarkTfo(id);
pNtk->ForEachFanin(id, [&](int fi) {
vTfoMarks[fi] = true;
});
int nAdded = 0;
int nAddedFis_ = 0;
for(int cand: vCands) {
if(!pNtk->IsInt(cand) && !pNtk->IsPi(cand)) {
continue;
@ -698,23 +782,39 @@ namespace rrr {
if(vTfoMarks[cand]) {
continue;
}
statsLocal.nTriedFis++;
if(ana.CheckFeasibility(id, cand, false)) {
pNtk->AddFanin(id, cand, false);
statsLocal.nAddedFis++;
} else if(pNtk->UseComplementedEdges() && ana.CheckFeasibility(id, cand, true)) {
pNtk->AddFanin(id, cand, true);
statsLocal.nAddedFis++;
} else {
continue;
}
mapNewFanins[id].insert(cand);
nAdded++;
if(nAdded == nMax) {
nAddedFis_++;
if(nAddedFis_ == nMax) {
break;
}
}
pNtk->ForEachFanin(id, [&](int fi) {
vTfoMarks[fi] = false;
});
return nAdded;
time_point timeEnd = GetCurrentTime();
statsLocal.durationAdd += Duration(timeStart, timeEnd);
return nAddedFis_;
}
template <typename Ntk, typename Ana>
void Optimizer<Ntk, Ana>::Undo() {
for(auto const &entry: mapNewFanins) {
int id = entry.first;
for(int fi: entry.second) {
int idx = pNtk->FindFanin(id, fi);
pNtk->RemoveFanin(id, idx);
}
}
}
/* }}} */
@ -731,11 +831,12 @@ namespace rrr {
pNtk->TrivialCollapse(id);
// save if wanted
int slot = -2;
if(fGreedy) {
if(fGreedy || fCompatible) {
slot = pNtk->Save();
}
double dCost = CostFunction(pNtk);
// main loop
double cost = CostFunction(pNtk);
bool fTried = false, fAdded = false;
for(citr it = vCands.begin(); it != vCands.end(); it++) {
if(Timeout()) {
break;
@ -743,25 +844,44 @@ namespace rrr {
if(!pNtk->IsInt(id)) {
break;
}
fTried = true;
it = SingleAdd<citr>(id, it, vCands.end());
if(it == vCands.end()) {
break;
}
Print(1, "cand", *it, "(", int_distance(vCands.begin(), it) + 1, "/", int_size(vCands), "):", "cost", "=", dCost);
RemoveRedundancy();
mapNewFanins.clear();
double dNewCost = CostFunction(pNtk);
Print(2, "cost:", dCost, "->", dNewCost);
if(fGreedy) {
if(dNewCost <= dCost) {
pNtk->Save(slot);
dCost = dNewCost;
fAdded = true;
Print(2, "cand", *it, "(", int_distance(vCands.begin(), it) + 1, "/", int_size(vCands), ")", ":", "cost", "=", cost);
if(RemoveRedundancy()) {
double costNew = CostFunction(pNtk);
// stats
statsLocal.nChanged++;
if(costNew < cost) {
statsLocal.nDowns++;
} else if (costNew == cost) {
statsLocal.nEqs++;
} else {
pNtk->Load(slot);
statsLocal.nUps++;
}
// greedy
if(fGreedy) {
if(costNew <= cost) {
pNtk->Save(slot);
cost = costNew;
} else {
pNtk->Load(slot);
}
} else {
cost = costNew;
}
} else {
dCost = dNewCost;
// assuming addition only always increases cost
if(fCompatible) {
pNtk->Load(slot);
} else {
Undo();
}
}
mapNewFanins.clear();
}
if(pNtk->IsInt(id)) {
pNtk->TrivialDecompose(id);
@ -770,9 +890,15 @@ namespace rrr {
RemoveRedundancy();
}
}
if(fGreedy) {
if(fGreedy || fCompatible) {
pNtk->PopBack();
}
if(fTried) {
statsLocal.nTried++;
}
if(fAdded) {
statsLocal.nAdded++;
}
}
template <typename Ntk, typename Ana>
@ -781,24 +907,43 @@ namespace rrr {
// let us assume the node is not trivially redundant for now
assert(pNtk->GetNumFanouts(id) != 0);
assert(pNtk->GetNumFanins(id) > 1);
statsLocal.nTried++;
// save if wanted
int slot = -2;
if(fGreedy) {
if(fGreedy || fCompatible) {
slot = pNtk->Save();
}
double dCost = CostFunction(pNtk);
// collapse
pNtk->TrivialCollapse(id);
// resub
MultiAdd(id, vCands, nMax);
RemoveRedundancy();
mapNewFanins.clear();
// TODO: we could quit here if nothing has been removed
RemoveRedundancy();
double dNewCost = CostFunction(pNtk);
Print(1, "cost:", dCost, "->", dNewCost);
if(fGreedy && dNewCost > dCost) {
pNtk->Load(slot);
double cost = CostFunction(pNtk);
if(MultiAdd(id, vCands, nMax)) {
statsLocal.nAdded++;
if(RemoveRedundancy()) {
mapNewFanins.clear();
RemoveRedundancy();
double costNew = CostFunction(pNtk);
// stats
statsLocal.nChanged++;
if(costNew < cost) {
statsLocal.nDowns++;
} else if (costNew == cost) {
statsLocal.nEqs++;
} else {
statsLocal.nUps++;
}
// greedy
if(fGreedy && costNew > cost) {
pNtk->Load(slot);
}
} else {
if(fCompatible) {
pNtk->Load(slot);
} else {
Undo();
}
mapNewFanins.clear();
}
}
if(pNtk->IsInt(id)) {
pNtk->TrivialDecompose(id);
@ -807,7 +952,7 @@ namespace rrr {
RemoveRedundancy();
}
}
if(fGreedy) {
if(fGreedy || fCompatible) {
pNtk->PopBack();
}
}
@ -824,57 +969,77 @@ namespace rrr {
// let us assume the node is not trivially redundant for now
assert(pNtk->GetNumFanouts(id) != 0);
assert(pNtk->GetNumFanins(id) > 1);
// save before trivial collapse
int slot0 = pNtk->Save();
Print(2, "method", "=", "single");
// collapse
pNtk->TrivialCollapse(id);
// save after trivial collapse
// save
int slot = pNtk->Save();
double dCost = CostFunction(pNtk);
// remember fanins
std::set<int> sFanins = pNtk->GetExtendedFanins(id);
Print(2, "extended fanins:", sFanins);
Print(3, "extended fanins", ":", sFanins);
// main loop
bool fChanged = false;
double cost = CostFunction(pNtk);
bool fTried = false, fAdded = false;
for(citr it = vCands.begin(); it != vCands.end(); it++) {
if(Timeout()) {
break;
}
assert(pNtk->IsInt(id));
fTried = true;
it = SingleAdd<citr>(id, it, vCands.end());
if(it == vCands.end()) {
break;
}
Print(1, "cand", *it, "(", int_distance(vCands.begin(), it) + 1, "/", int_size(vCands), "):", "cost", "=", dCost);
RemoveRedundancy();
mapNewFanins.clear();
double dNewCost = CostFunction(pNtk);
Print(2, "cost:", dCost, "->", dNewCost);
if(dNewCost <= dCost) {
bool fChanged = false;
if(dNewCost < dCost || !pNtk->IsInt(id)) {
fChanged = true;
} else {
std::set<int> sNewFanins = pNtk->GetExtendedFanins(id);
Print(2, "new extended fanins:", sNewFanins);
if(sFanins != sNewFanins) {
fAdded = true;
Print(3, "cand", *it, "(", int_distance(vCands.begin(), it) + 1, "/", int_size(vCands), ")", ":", "cost", "=", cost);
if(RemoveRedundancy()) {
mapNewFanins.clear();
double costNew = CostFunction(pNtk);
if(costNew <= cost) {
fChanged = false;
if(costNew < cost || !pNtk->IsInt(id)) {
fChanged = true;
} else {
std::set<int> sNewFanins = pNtk->GetExtendedFanins(id);
Print(3, "new extended fanins", ":", sNewFanins);
if(sFanins != sNewFanins) {
fChanged = true;
}
}
if(fChanged) {
statsLocal.nChanged++;
if(costNew < cost) {
statsLocal.nDowns++;
} else if (costNew == cost) {
statsLocal.nEqs++;
} else {
statsLocal.nUps++;
}
break;
}
}
if(fChanged) {
if(pNtk->IsInt(id)) {
pNtk->TrivialDecompose(id);
}
pNtk->PopBack(); // slot
pNtk->PopBack(); // slot0
return true;
pNtk->Load(slot);
} else {
if(fCompatible) {
pNtk->Load(slot);
} else {
Undo();
}
mapNewFanins.clear();
}
pNtk->Load(slot);
}
pNtk->PopBack(); // slot
pNtk->Load(slot0);
pNtk->PopBack(); // slot0
return false;
if(pNtk->IsInt(id)) {
pNtk->TrivialDecompose(id);
}
pNtk->PopBack();
if(fTried) {
statsLocal.nTried++;
}
if(fAdded) {
statsLocal.nAdded++;
}
return fChanged;
}
template <typename Ntk, typename Ana>
@ -885,44 +1050,59 @@ namespace rrr {
// let us assume the node is not trivially redundant for now
assert(pNtk->GetNumFanouts(id) != 0);
assert(pNtk->GetNumFanins(id) > 1);
Print(2, "method", "=", "multi");
statsLocal.nTried++;
// save
int slot = pNtk->Save();
double dCost = CostFunction(pNtk);
// remember fanins
std::set<int> sFanins = pNtk->GetExtendedFanins(id);
Print(2, "extended fanins:", sFanins);
Print(3, "extended fanins", ":", sFanins);
// collapse
pNtk->TrivialCollapse(id);
// resub
MultiAdd(id, vCands, nMax);
RemoveRedundancy();
mapNewFanins.clear();
// TODO: we could quit here if nothing has been removed
RemoveRedundancy();
double dNewCost = CostFunction(pNtk);
Print(1, "cost:", dCost, "->", dNewCost);
if(!fGreedy || dNewCost <= dCost) {
bool fChanged = false;
if(dNewCost < dCost || !pNtk->IsInt(id)) {
fChanged = true;
bool fChanged = false;
double cost = CostFunction(pNtk);
if(MultiAdd(id, vCands, nMax)) {
statsLocal.nAdded++;
if(RemoveRedundancy()) {
mapNewFanins.clear();
RemoveRedundancy();
double costNew = CostFunction(pNtk);
if(!fGreedy || costNew <= cost) {
fChanged = false;
if(costNew < cost || !pNtk->IsInt(id)) {
fChanged = true;
} else {
std::set<int> sNewFanins = pNtk->GetExtendedFanins(id);
Print(3, "new extended fanins", ":", sNewFanins);
if(sFanins != sNewFanins) {
fChanged = true;
}
}
if(fChanged) {
statsLocal.nChanged++;
if(costNew < cost) {
statsLocal.nDowns++;
} else if (costNew == cost) {
statsLocal.nEqs++;
} else {
statsLocal.nUps++;
}
}
}
} else {
std::set<int> sNewFanins = pNtk->GetExtendedFanins(id);
Print(2, "new extended fanins:", sNewFanins);
if(sFanins != sNewFanins) {
fChanged = true;
}
}
if(fChanged) {
if(pNtk->IsInt(id)) {
pNtk->TrivialDecompose(id);
}
pNtk->PopBack();
return true;
mapNewFanins.clear();
}
}
pNtk->Load(slot);
if(fChanged) {
if(pNtk->IsInt(id)) {
pNtk->TrivialDecompose(id);
}
} else {
pNtk->Load(slot);
}
pNtk->PopBack();
return false;
return fChanged;
}
/* }}} */
@ -948,7 +1128,7 @@ namespace rrr {
}
}
// add while remembering extended fanins
Print(1, "targets:", vTargets);
Print(2, "targets", ":", vTargets);
std::vector<std::set<int>> vsFanins;
for(int id: vTargets) {
// get candidates
@ -961,7 +1141,7 @@ namespace rrr {
std::shuffle(vCands.begin(), vCands.end(), rng);
// remember fanins
std::set<int> sFanins = pNtk->GetExtendedFanins(id);
Print(2, "extended fanins:", sFanins);
Print(3, "extended fanins", ":", sFanins);
vsFanins.push_back(std::move(sFanins));
// add
MultiAdd(id, vCands, nMax);
@ -972,7 +1152,7 @@ namespace rrr {
// TODO: we could quit here if nothing has been removed
RemoveRedundancy();
double dNewCost = CostFunction(pNtk);
Print(1, "cost:", dCost, "->", dNewCost);
Print(2, "cost =", dCost, "->", dNewCost);
if(!fGreedy || dNewCost <= dCost) {
bool fChanged = false;
if(dNewCost < dCost) {
@ -986,7 +1166,7 @@ namespace rrr {
}
for(int i = 0; !fChanged && i < int_size(vTargets); i++) {
std::set<int> sNewFanins = pNtk->GetExtendedFanins(vTargets[i]);
Print(2, "new extended fanins:", sNewFanins);
Print(3, "new extended fanins", ":", sNewFanins);
if(vsFanins[i] != sNewFanins) {
fChanged = true;
}
@ -1021,7 +1201,7 @@ namespace rrr {
if(!pNtk->IsInt(*it)) {
continue;
}
Print(0, "node", *it, "(", int_distance(vInts.crbegin(), it) + 1, "/", int_size(vInts), "):", "cost", "=", CostFunction(pNtk));
Print(1, "node", *it, "(", int_distance(vInts.crbegin(), it) + 1, "/", int_size(vInts), ")", ":", "cost", "=", CostFunction(pNtk));
func(*it);
}
}
@ -1037,7 +1217,7 @@ namespace rrr {
if(!pNtk->IsInt(*it)) {
continue;
}
Print(0, "node", *it, "(", int_distance(vInts.cbegin(), it) + 1, "/", int_size(vInts), "):", "cost", "=", CostFunction(pNtk));
Print(1, "node", *it, "(", int_distance(vInts.cbegin(), it) + 1, "/", int_size(vInts), ")", ":", "cost", "=", CostFunction(pNtk));
if(func(*it)) {
break;
}
@ -1048,10 +1228,10 @@ namespace rrr {
void Optimizer<Ntk, Ana>::ApplyCombinationRandomlyStop(int k, std::function<bool(std::vector<int> const &)> const &func) {
std::vector<int> vInts = pNtk->GetInts();
std::shuffle(vInts.begin(), vInts.end(), rng); // order is decided here, so it's not truely exhaustive
int nTried = 0;
int nTried_ = 0;
int nCombs = k * (k - 1) / 2;
ForEachCombinationStop(int_size(vInts), k, [&](std::vector<int> const &vIdxs) {
Print(0, "comb", vIdxs, "(", ++nTried, "/", nCombs, ")");
Print(1, "comb", vIdxs, "(", ++nTried_, "/", nCombs, ")");
assert(int_size(vIdxs) == k);
if(Timeout()) {
return true;
@ -1078,7 +1258,7 @@ namespace rrr {
}
std::vector<int> vIdxs(sIdxs.begin(), sIdxs.end());
std::shuffle(vIdxs.begin(), vIdxs.end(), rng);
Print(0, "comb", vIdxs, "(", i + 1, "/", nSamples, ")");
Print(1, "comb", vIdxs, "(", i + 1, "/", nSamples, ")");
std::vector<int> vTargets(k);
for(int i = 0; i < k; i++) {
vTargets[i] = vInts[vIdxs[i]];
@ -1109,11 +1289,16 @@ namespace rrr {
}
template <typename Ntk, typename Ana>
void Optimizer<Ntk, Ana>::UpdateNetwork(Ntk *pNtk_, bool fSame) {
void Optimizer<Ntk, Ana>::AssignNetwork(Ntk *pNtk_, bool fReuse) {
pNtk = pNtk_;
target = -1;
pNtk->AddCallback(std::bind(&Optimizer<Ntk, Ana>::ActionCallback, this, std::placeholders::_1));
ana.UpdateNetwork(pNtk, fSame);
ana.AssignNetwork(pNtk, fReuse);
}
template <typename Ntk, typename Ana>
void Optimizer<Ntk, Ana>::SetPrintLine(std::function<void(std::string)> const &PrintLine_) {
PrintLine = PrintLine_;
}
/* }}} */
@ -1127,13 +1312,14 @@ namespace rrr {
vRandCosts.clear();
if(nSortTypeOriginal < 0) {
nSortType = rng() % 18;
Print(0, "sorttype =", nSortType);
Print(0, "fanin cost function =", nSortType);
}
nTimeout = nTimeout_;
start = GetCurrentTime();
switch(nFlow) {
case 0:
RemoveRedundancy();
statsLocal.Reset();
ApplyReverseTopologically([&](int id) {
std::vector<int> vCands;
if(nDistance) {
@ -1143,9 +1329,12 @@ namespace rrr {
}
SingleResub(id, vCands);
});
stats["single"] += statsLocal;
Print(0, statsLocal.GetString());
break;
case 1:
RemoveRedundancy();
statsLocal.Reset();
ApplyReverseTopologically([&](int id) {
std::vector<int> vCands;
if(nDistance) {
@ -1155,11 +1344,14 @@ namespace rrr {
}
MultiResub(id, vCands);
});
stats["multi"] += statsLocal;
Print(0, statsLocal.GetString());
break;
case 2: {
RemoveRedundancy();
double dCost = CostFunction(pNtk);
while(true) {
statsLocal.Reset();
ApplyReverseTopologically([&](int id) {
std::vector<int> vCands;
if(nDistance) {
@ -1169,6 +1361,9 @@ namespace rrr {
}
SingleResub(id, vCands);
});
stats["single"] += statsLocal;
Print(0, "single", ":", "cost", "=", CostFunction(pNtk), ",", statsLocal.GetString());
statsLocal.Reset();
ApplyReverseTopologically([&](int id) {
std::vector<int> vCands;
if(nDistance) {
@ -1179,6 +1374,8 @@ namespace rrr {
}
MultiResub(id, vCands);
});
stats["multi"] += statsLocal;
Print(0, "multi ", ":", "cost", "=", CostFunction(pNtk), ",", statsLocal.GetString());
double dNewCost = CostFunction(pNtk);
if(dNewCost < dCost) {
dCost = dNewCost;
@ -1195,17 +1392,27 @@ namespace rrr {
vCands = pNtk->GetPisInts();
std::shuffle(vCands.begin(), vCands.end(), rng);
}
Stats statsSingle, statsMulti;
ApplyRandomlyStop([&](int id) {
statsLocal.Reset();
if(nDistance) {
vCands = pNtk->GetNeighbors(id, true, nDistance);
std::shuffle(vCands.begin(), vCands.end(), rng);
}
bool fChanged;
if(rng() & 1) {
return SingleResubStop(id, vCands);
fChanged = SingleResubStop(id, vCands);
statsSingle += statsLocal;
} else {
return MultiResubStop(id, vCands);
fChanged = MultiResubStop(id, vCands);
statsMulti += statsLocal;
}
return fChanged;
});
stats["single"] += statsSingle;
stats["multi"] += statsMulti;
Print(0, "single", ":", statsSingle.GetString());
Print(0, "multi ", ":", statsMulti.GetString());
break;
}
case 4: {
@ -1221,6 +1428,46 @@ namespace rrr {
}
/* }}} */
/* {{{ Summary */
template <typename Ntk, typename Ana>
void Optimizer<Ntk, Ana>::ResetSummary() {
stats.clear();
ana.ResetSummary();
}
template <typename Ntk, typename Ana>
summary<int> Optimizer<Ntk, Ana>::GetStatsSummary() const {
summary<int> v;
for(auto const &entry: stats) {
v.emplace_back("opt " + entry.first + " tried node", entry.second.nTried);
v.emplace_back("opt " + entry.first + " tried fanin", entry.second.nTriedFis);
v.emplace_back("opt " + entry.first + " added node", entry.second.nAdded);
v.emplace_back("opt " + entry.first + " added fanin", entry.second.nAddedFis);
v.emplace_back("opt " + entry.first + " changed", entry.second.nChanged);
v.emplace_back("opt " + entry.first + " up", entry.second.nUps);
v.emplace_back("opt " + entry.first + " eq", entry.second.nEqs);
v.emplace_back("opt " + entry.first + " dn", entry.second.nDowns);
}
summary<int> v2 = ana.GetStatsSummary();
v.insert(v.end(), v2.begin(), v2.end());
return v;
}
template <typename Ntk, typename Ana>
summary<double> Optimizer<Ntk, Ana>::GetTimesSummary() const {
summary<double> v;
for(auto const &entry: stats) {
v.emplace_back("opt " + entry.first + " add", entry.second.durationAdd);
v.emplace_back("opt " + entry.first + " reduce", entry.second.durationReduce);
}
summary<double> v2 = ana.GetTimesSummary();
v.insert(v.end(), v2.begin(), v2.end());
return v;
}
/* }}} */
}

2
src/opt/rrr/rrrParameter.h
View File

@ -8,7 +8,7 @@ namespace rrr {
int iSeed = 0;
int nWords = 10;
int nTimeout = 0;
int nSchedulerVerbose = 1;
int nSchedulerVerbose = 0;
int nPartitionerVerbose = 0;
int nOptimizerVerbose = 0;
int nAnalyzerVerbose = 0;

4
src/opt/rrr/rrrPartitioner.h
View File

@ -42,7 +42,7 @@ namespace rrr {
public:
// constructors
Partitioner(Parameter const *pPar);
void UpdateNetwork(Ntk *pNtk);
void AssignNetwork(Ntk *pNtk);
// APIs
Ntk *Extract(int iSeed);
@ -270,7 +270,7 @@ namespace rrr {
}
template <typename Ntk>
void Partitioner<Ntk>::UpdateNetwork(Ntk *pNtk_) {
void Partitioner<Ntk>::AssignNetwork(Ntk *pNtk_) {
pNtk = pNtk_;
assert(mSubNtk2Io.empty());
assert(sBlocked.empty());

70
src/opt/rrr/rrrSatSolver.h
View File

@ -28,10 +28,12 @@ namespace rrr {
std::vector<VarValue> vValues; // values in satisfied problem
bool fUpdate;
// statistics
// stats
int nCalls;
int nSats;
int nUnsats;
double durationRedundancy;
double durationFeasibility;
// callback
void ActionCallback(Action const &action);
@ -45,7 +47,7 @@ namespace rrr {
// constructors
SatSolver(Parameter const *pPar);
~SatSolver();
void UpdateNetwork(Ntk *pNtk_, bool fSame);
void AssignNetwork(Ntk *pNtk_, bool fReuse);
// checks
SatResult CheckRedundancy(int id, int idx);
@ -53,6 +55,11 @@ namespace rrr {
// cex
std::vector<VarValue> GetCex();
// stats
void ResetSummary();
summary<int> GetStatsSummary() const;
summary<double> GetTimesSummary() const;
};
/* {{{ Callback */
@ -88,6 +95,11 @@ namespace rrr {
break;
case SORT_FANINS:
break;
case READ:
status = false;
target = -1;
fUpdate = false;
break;
case SAVE:
break;
case LOAD:
@ -259,25 +271,23 @@ namespace rrr {
pSat(sat_solver_new()),
status(false),
target(-1),
fUpdate(false),
nCalls(0),
nSats(0),
nUnsats(0) {
fUpdate(false) {
ResetSummary();
}
template <typename Ntk>
SatSolver<Ntk>::~SatSolver() {
sat_solver_delete(pSat);
std::cout << "SAT solver stats: calls = " << nCalls << " (SAT = " << nSats << ", UNSAT = " << nUnsats << ", UNDET = " << nCalls - nSats - nUnsats << ")" << std::endl;
//std::cout << "SAT solver stats: calls = " << nCalls << " (SAT = " << nSats << ", UNSAT = " << nUnsats << ", UNDET = " << nCalls - nSats - nUnsats << ")" << std::endl;
}
template <typename Ntk>
void SatSolver<Ntk>::UpdateNetwork(Ntk *pNtk_, bool fSame) {
(void)fSame;
pNtk = pNtk_;
void SatSolver<Ntk>::AssignNetwork(Ntk *pNtk_, bool fReuse) {
(void)fReuse;
status = false;
target = -1;
fUpdate = false;
pNtk = pNtk_;
pNtk->AddCallback(std::bind(&SatSolver<Ntk>::ActionCallback, this, std::placeholders::_1));
}
@ -287,11 +297,13 @@ namespace rrr {
template <typename Ntk>
SatResult SatSolver<Ntk>::CheckRedundancy(int id, int idx) {
time_point timeStart = GetCurrentTime();
SetTarget(id);
if(!status) {
if(nVerbose) {
std::cout << "trivially UNSATISFIABLE" << std::endl;
}
durationRedundancy += Duration(timeStart, GetCurrentTime());
return UNSAT;
}
vLits.clear();
@ -319,12 +331,14 @@ namespace rrr {
std::cout << "UNSATISFIABLE" << std::endl;
}
nUnsats++;
durationRedundancy += Duration(timeStart, GetCurrentTime());
return UNSAT;
}
if(res == l_Undef) {
if(nVerbose) {
std::cout << "UNDETERMINED" << std::endl;
}
durationRedundancy += Duration(timeStart, GetCurrentTime());
return UNDET;
}
assert(res == l_True);
@ -353,16 +367,19 @@ namespace rrr {
assert((vValues[fi] == TEMP_TRUE) ^ (idx == idx2) ^ c);
vValues[fi] = DecideVarValue(vValues[fi]);
});
durationRedundancy += Duration(timeStart, GetCurrentTime());
return SAT;
}
template <typename Ntk>
SatResult SatSolver<Ntk>::CheckFeasibility(int id, int fi, bool c) {
time_point timeStart = GetCurrentTime();
SetTarget(id);
if(!status) {
if(nVerbose) {
std::cout << "trivially UNSATISFIABLE" << std::endl;
}
durationFeasibility += Duration(timeStart, GetCurrentTime());
return UNSAT;
}
vLits.clear();
@ -385,12 +402,14 @@ namespace rrr {
std::cout << "UNSATISFIABLE" << std::endl;
}
nUnsats++;
durationFeasibility += Duration(timeStart, GetCurrentTime());
return UNSAT;
}
if(res == l_Undef) {
if(nVerbose) {
std::cout << "UNDETERMINED" << std::endl;
}
durationFeasibility += Duration(timeStart, GetCurrentTime());
return UNDET;
}
assert(res == l_True);
@ -419,6 +438,7 @@ namespace rrr {
vValues[id] = DecideVarValue(vValues[id]);
assert((vValues[fi] == TEMP_TRUE) ^ !c);
vValues[fi] = DecideVarValue(vValues[fi]);
durationFeasibility += Duration(timeStart, GetCurrentTime());
return SAT;
}
@ -537,6 +557,36 @@ namespace rrr {
/* }}} */
/* {{{ Stats */
template <typename Ntk>
void SatSolver<Ntk>::ResetSummary() {
nCalls = 0;
nSats = 0;
nUnsats = 0;
durationRedundancy = 0;
durationFeasibility = 0;
}
template <typename Ntk>
summary<int> SatSolver<Ntk>::GetStatsSummary() const {
summary<int> v;
v.emplace_back("sat call", nCalls);
v.emplace_back("sat satisfiable", nSats);
v.emplace_back("sat unsatisfiable", nUnsats);
return v;
}
template <typename Ntk>
summary<double> SatSolver<Ntk>::GetTimesSummary() const {
summary<double> v;
v.emplace_back("sat redundancy", durationRedundancy);
v.emplace_back("sat feasibility", durationFeasibility);
return v;
}
/* }}} */
}
ABC_NAMESPACE_CXX_HEADER_END

234
src/opt/rrr/rrrScheduler.h
View File

@ -46,10 +46,14 @@ namespace rrr {
// data
int nCreatedJobs;
int nFinishedJobs;
time_point start;
time_point timeStart;
Par par;
std::queue<Job *> qPendingJobs;
Opt *pOpt; // used only in case of single thread execution
std::vector<std::string> vStatsSummaryKeys;
std::map<std::string, int> mStatsSummary;
std::vector<std::string> vTimesSummaryKeys;
std::map<std::string, double> mTimesSummary;
#ifdef ABC_USE_PTHREADS
bool fTerminate;
std::vector<std::thread> vThreads;
@ -57,21 +61,27 @@ namespace rrr {
std::mutex mutexAbc;
std::mutex mutexPendingJobs;
std::mutex mutexFinishedJobs;
std::mutex mutexPrint;
std::condition_variable condPendingJobs;
std::condition_variable condFinishedJobs;
#endif
// print
template <typename... Args>
void Print(int nVerboseLevel, std::string prefix, Args... args);
// time
seconds GetRemainingTime() const;
double GetElapsedTime() const;
// abc
void CallAbc(Ntk *pNtk_, std::string Command);
// run jobs
void RunJob(Opt &opt, Job const *pJob);
void RunJob(Opt &opt, Job *pJob);
// manage jobs
void CreateJob(Ntk *pNtk_, int iSeed_);
Job *CreateJob(Ntk *pNtk_, int iSeed_, double cost);
void OnJobEnd(std::function<void(Job *pJob)> const &func);
// thread
@ -79,6 +89,10 @@ namespace rrr {
void Thread(Parameter const *pPar);
#endif
// summary
template <typename T>
void AddToSummary(std::vector<std::string> &keys, std::map<std::string, T> &m, summary<T> const &result) const;
public:
// constructors
Scheduler(Ntk *pNtk, Parameter const *pPar);
@ -96,12 +110,21 @@ namespace rrr {
int id;
Ntk *pNtk;
int iSeed;
double costInitial;
std::string prefix;
double duration;
summary<int> stats;
summary<double> times;
// constructor
Job(int id, Ntk *pNtk, int iSeed) :
Job(int id, Ntk *pNtk, int iSeed, double cost) :
id(id),
pNtk(pNtk),
iSeed(iSeed) {
iSeed(iSeed),
costInitial(cost) {
std::stringstream ss;
PrintNext(ss, "job", id, ":");
prefix = ss.str() + " ";
}
};
@ -115,21 +138,53 @@ namespace rrr {
/* }}} */
/* {{{ Print */
template <typename Ntk, typename Opt, typename Par>
template<typename... Args>
inline void Scheduler<Ntk, Opt, Par>::Print(int nVerboseLevel, std::string prefix, Args... args) {
if(nVerbose <= nVerboseLevel) {
return;
}
#ifdef ABC_USE_PTHREADS
if(fMultiThreading) {
{
std::unique_lock<std::mutex> l(mutexPrint);
std::cout << prefix;
PrintNext(std::cout, args...);
std::cout << std::endl;
}
return;
}
#endif
std::cout << prefix;
PrintNext(std::cout, args...);
std::cout << std::endl;
}
/* }}} */
/* {{{ Time */
template <typename Ntk, typename Opt, typename Par>
seconds Scheduler<Ntk, Opt, Par>::GetRemainingTime() const {
inline seconds Scheduler<Ntk, Opt, Par>::GetRemainingTime() const {
if(nTimeout == 0) {
return 0;
}
time_point current = GetCurrentTime();
seconds nRemainingTime = nTimeout - DurationInSeconds(start, current);
time_point timeCurrent = GetCurrentTime();
seconds nRemainingTime = nTimeout - DurationInSeconds(timeStart, timeCurrent);
if(nRemainingTime == 0) { // avoid glitch
return -1;
}
return nRemainingTime;
}
template <typename Ntk, typename Opt, typename Par>
inline double Scheduler<Ntk, Opt, Par>::GetElapsedTime() const {
time_point timeCurrent = GetCurrentTime();
return Duration(timeStart, timeCurrent);
}
/* }}} */
/* {{{ Abc */
@ -153,8 +208,12 @@ namespace rrr {
/* {{{ Run jobs */
template <typename Ntk, typename Opt, typename Par>
void Scheduler<Ntk, Opt, Par>::RunJob(Opt &opt, Job const *pJob) {
opt.UpdateNetwork(pJob->pNtk);
void Scheduler<Ntk, Opt, Par>::RunJob(Opt &opt, Job *pJob) {
time_point timeStartLocal = GetCurrentTime();
opt.AssignNetwork(pJob->pNtk, !fPartitioning); // reuse backend if restarting
opt.SetPrintLine([&](std::string str) {
Print(-1, pJob->prefix, str);
});
// start flow
switch(nFlow) {
case 0:
@ -162,23 +221,17 @@ namespace rrr {
break;
case 1: { // transtoch
std::mt19937 rng(pJob->iSeed);
double dCost = CostFunction(pJob->pNtk);
double dBestCost = dCost;
double cost = pJob->costInitial;
double costBest = cost;
Ntk best(*(pJob->pNtk));
if(nVerbose) {
std::cout << "start: cost = " << dCost << std::endl;
}
for(int i = 0; i < 10; i++) {
if(GetRemainingTime() < 0) {
break;
}
if(i != 0) {
CallAbc(pJob->pNtk, "&if -K 6; &mfs; &st");
dCost = CostFunction(pJob->pNtk);
opt.UpdateNetwork(pJob->pNtk, true);
if(nVerbose) {
std::cout << "hop " << std::setw(3) << i << ": cost = " << dCost << std::endl;
}
cost = CostFunction(pJob->pNtk);
Print(1, pJob->prefix, "hop", i, ":", "cost", "=", cost);
}
for(int j = 0; true; j++) {
if(GetRemainingTime() < 0) {
@ -186,37 +239,28 @@ namespace rrr {
}
opt.Run(rng(), GetRemainingTime());
CallAbc(pJob->pNtk, "&dc2");
double dNewCost = CostFunction(pJob->pNtk);
if(nVerbose) {
std::cout << "\tite " << std::setw(3) << j << ": cost = " << dNewCost << std::endl;
}
if(dNewCost < dCost) {
dCost = dNewCost;
opt.UpdateNetwork(pJob->pNtk, true);
double costNew = CostFunction(pJob->pNtk);
Print(1, pJob->prefix, "ite", j, ":", "cost", "=", costNew);
if(costNew < cost) {
cost = costNew;
} else {
break;
}
}
if(dCost < dBestCost) {
dBestCost = dCost;
if(cost < costBest) {
costBest = cost;
best = *(pJob->pNtk);
i = 0;
}
}
*(pJob->pNtk) = best;
if(nVerbose) {
std::cout << "end: cost = " << dBestCost << std::endl;
}
break;
}
case 2: { // deep
std::mt19937 rng(pJob->iSeed);
int n = 0;
double dCost = CostFunction(pJob->pNtk);
double cost = pJob->costInitial;
Ntk best(*(pJob->pNtk));
if(nVerbose) {
std::cout << "start: cost = " << dCost << std::endl;
}
for(int i = 0; i < 1000000; i++) {
if(GetRemainingTime() < 0) {
break;
@ -246,38 +290,30 @@ namespace rrr {
Command += "; &fx; &st";
Command += pComp;
CallAbc(pJob->pNtk, Command);
if(nVerbose) {
std::cout << "ite " << std::setw(6) << i << ": cost = " << CostFunction(pJob->pNtk) << std::endl;
}
Print(1, pJob->prefix, "ite", i, ":", "cost", "=", CostFunction(pJob->pNtk));
// rrr
for(int j = 0; j < n; j++) {
if(GetRemainingTime() < 0) {
break;
}
opt.UpdateNetwork(pJob->pNtk, true);
opt.Run(rng(), GetRemainingTime());
if(rng() & 1) {
CallAbc(pJob->pNtk, "&dc2");
} else {
CallAbc(pJob->pNtk, std::string("&put; ") + pCompress2rs + "; &get");
}
if(nVerbose) {
std::cout << "\trrr " << std::setw(6) << j << ": cost = " << CostFunction(pJob->pNtk) << std::endl;
}
Print(1, pJob->prefix, "rrr", j, ":", "cost", "=", CostFunction(pJob->pNtk));
}
// eval
double dNewCost = CostFunction(pJob->pNtk);
if(dNewCost < dCost) {
dCost = dNewCost;
double costNew = CostFunction(pJob->pNtk);
if(costNew < cost) {
cost = costNew;
best = *(pJob->pNtk);
} else {
n++;
}
}
*(pJob->pNtk) = best;
if(nVerbose) {
std::cout << "end: cost = " << dCost << std::endl;
}
break;
}
case 3:
@ -287,6 +323,11 @@ namespace rrr {
default:
assert(0);
}
time_point timeEndLocal = GetCurrentTime();
pJob->duration = Duration(timeStartLocal, timeEndLocal);
pJob->stats = opt.GetStatsSummary();
pJob->times = opt.GetTimesSummary();
opt.ResetSummary();
}
/* }}} */
@ -294,8 +335,8 @@ namespace rrr {
/* {{{ Manage jobs */
template <typename Ntk, typename Opt, typename Par>
void Scheduler<Ntk, Opt, Par>::CreateJob(Ntk *pNtk_, int iSeed_) {
Job *pJob = new Job(nCreatedJobs++, pNtk_, iSeed_);
typename Scheduler<Ntk, Opt, Par>::Job *Scheduler<Ntk, Opt, Par>::CreateJob(Ntk *pNtk_, int iSeed_, double cost) {
Job *pJob = new Job(nCreatedJobs++, pNtk_, iSeed_, cost);
#ifdef ABC_USE_PTHREADS
if(fMultiThreading) {
{
@ -303,10 +344,11 @@ namespace rrr {
qPendingJobs.push(pJob);
condPendingJobs.notify_one();
}
return;
return pJob;
}
#endif
qPendingJobs.push(pJob);
return pJob;
}
template <typename Ntk, typename Opt, typename Par>
@ -324,6 +366,8 @@ namespace rrr {
}
assert(pJob != NULL);
func(pJob);
AddToSummary(vStatsSummaryKeys, mStatsSummary, pJob->stats);
AddToSummary(vTimesSummaryKeys, mTimesSummary, pJob->times);
delete pJob;
nFinishedJobs++;
return;
@ -335,6 +379,8 @@ namespace rrr {
qPendingJobs.pop();
RunJob(*pOpt, pJob);
func(pJob);
AddToSummary(vStatsSummaryKeys, mStatsSummary, pJob->stats);
AddToSummary(vTimesSummaryKeys, mTimesSummary, pJob->times);
delete pJob;
nFinishedJobs++;
}
@ -374,6 +420,28 @@ namespace rrr {
/* }}} */
/* {{{ Summary */
template <typename Ntk, typename Opt, typename Par>
template <typename T>
void Scheduler<Ntk, Opt, Par>::AddToSummary(std::vector<std::string> &keys, std::map<std::string, T> &m, summary<T> const &result) const {
std::vector<std::string>::iterator it = keys.begin();
for(auto const &entry: result) {
if(m.count(entry.first)) {
m[entry.first] += entry.second;
it = std::find(it, keys.end(), entry.first);
assert(it != keys.end());
it++;
} else {
m[entry.first] = entry.second;
it = keys.insert(it, entry.first);
it++;
}
}
}
/* }}} */
/* {{{ Constructors */
template <typename Ntk, typename Opt, typename Par>
@ -439,74 +507,90 @@ namespace rrr {
template <typename Ntk, typename Opt, typename Par>
void Scheduler<Ntk, Opt, Par>::Run() {
start = GetCurrentTime();
timeStart = GetCurrentTime();
double costStart = CostFunction(pNtk);
if(fPartitioning) {
fDeterministic = false; // it is deterministic anyways as we wait until all jobs finish each round
pNtk->Sweep();
par.UpdateNetwork(pNtk);
par.AssignNetwork(pNtk);
while(nCreatedJobs < nJobs) {
assert(nParallelPartitions > 0);
if(nCreatedJobs < nFinishedJobs + nParallelPartitions) {
Ntk *pSubNtk = par.Extract(iSeed + nCreatedJobs);
if(pSubNtk) {
CreateJob(pSubNtk, iSeed + nCreatedJobs);
std::cout << "job " << nCreatedJobs - 1 << " created (size = " << pSubNtk->GetNumInts() << ")" << std::endl;
Job *pJob = CreateJob(pSubNtk, iSeed + nCreatedJobs, CostFunction(pSubNtk));
Print(1, pJob->prefix, "created ", ":", "i/o", "=", pJob->pNtk->GetNumPis(), "/", pJob->pNtk->GetNumPos(), ",", "node", "=", pJob->pNtk->GetNumInts(), ",", "level", "=", pJob->pNtk->GetNumLevels(), ",", "cost", "=", pJob->costInitial);
continue;
}
}
if(nCreatedJobs == nFinishedJobs) {
std::cout << "failed to partition" << std::endl;
PrintWarning("failed to partition");
break;
}
while(nFinishedJobs < nCreatedJobs) {
OnJobEnd([&](Job *pJob) {
std::cout << "job " << pJob->id << " finished (size = " << pJob->pNtk->GetNumInts() << ")" << std::endl;
double cost = CostFunction(pJob->pNtk);
Print(1, pJob->prefix, "finished", ":", "i/o", "=", pJob->pNtk->GetNumPis(), "/", pJob->pNtk->GetNumPos(), ",", "node", "=", pJob->pNtk->GetNumInts(), ",", "level", "=", pJob->pNtk->GetNumLevels(), ",", "cost", "=", cost);
Print(0, "", "job", pJob->id, "(", nFinishedJobs + 1, "/", nJobs, ")", ":", "i/o", "=", pJob->pNtk->GetNumPis(), "/", pJob->pNtk->GetNumPos(), ",", "node", "=", pJob->pNtk->GetNumInts(), ",", "level", "=", pJob->pNtk->GetNumLevels(), ",", "cost", "=", cost, "(", 100 * (cost - pJob->costInitial) / pJob->costInitial, "%", ")", ",", "duration", "=", pJob->duration, "s", ",", "elapsed", "=", GetElapsedTime(), "s");
par.Insert(pJob->pNtk);
});
}
if(fOptOnInsert) {
time_point timeStartLocal = GetCurrentTime();
CallAbc(pNtk, std::string("&put; ") + pCompress2rs + "; dc2; &get");
par.UpdateNetwork(pNtk);
time_point timeEndLocal = GetCurrentTime();
par.AssignNetwork(pNtk);
double cost = CostFunction(pNtk);
Print(0, "", "c2rs; dc2", ":", std::string(34, ' '), "node", "=", pNtk->GetNumInts(), ",", "level", "=", pNtk->GetNumLevels(), ",", "cost", "=", cost, "(", 100 * (cost - costStart) / costStart, "%", ")", ",", "duration", "=", Duration(timeStartLocal, timeEndLocal), "s", ",", "elapsed", "=", GetElapsedTime(), "s");
}
}
while(nFinishedJobs < nCreatedJobs) {
OnJobEnd([&](Job *pJob) {
std::cout << "job " << pJob->id << " finished (size = " << pJob->pNtk->GetNumInts() << ")" << std::endl;
double cost = CostFunction(pJob->pNtk);
Print(1, pJob->prefix, "finished", ":", "i/o", "=", pJob->pNtk->GetNumPis(), "/", pJob->pNtk->GetNumPos(), ",", "node", "=", pJob->pNtk->GetNumInts(), ",", "level", "=", pJob->pNtk->GetNumLevels(), ",", "cost", "=", CostFunction(pJob->pNtk));
Print(0, "", "job", pJob->id, "(", nFinishedJobs + 1, "/", nJobs, ")", ":", "i/o", "=", pJob->pNtk->GetNumPis(), "/", pJob->pNtk->GetNumPos(), ",", "node", "=", pJob->pNtk->GetNumInts(), ",", "level", "=", pJob->pNtk->GetNumLevels(), ",", "cost", "=", cost, "(", 100 * (cost - pJob->costInitial) / pJob->costInitial, "%", ")", ",", "duration", "=", pJob->duration, "s", ",", "elapsed", "=", GetElapsedTime(), "s");
par.Insert(pJob->pNtk);
});
}
if(fOptOnInsert) {
CallAbc(pNtk, std::string("&put; ") + pCompress2rs + "; dc2; &get");
par.UpdateNetwork(pNtk);
par.AssignNetwork(pNtk);
}
} else if(nJobs > 1) {
double dCost = CostFunction(pNtk);
double costBest = costStart;
for(int i = 0; i < nJobs; i++) {
Ntk *pCopy = new Ntk(*pNtk);
CreateJob(pCopy, iSeed + i);
CreateJob(pCopy, iSeed + i, costBest);
}
for(int i = 0; i < nJobs; i++) {
OnJobEnd([&](Job *pJob) {
double dNewCost = CostFunction(pJob->pNtk);
if(nVerbose) {
std::cout << "run " << pJob->id << ": cost = " << dNewCost << std::endl;
}
if(dNewCost < dCost) {
dCost = dNewCost;
double cost = CostFunction(pJob->pNtk);
Print(0, "", "job", pJob->id, "(", nFinishedJobs + 1, "/", nJobs, ")", ":", "node", "=", pJob->pNtk->GetNumInts(), ",", "level", "=", pJob->pNtk->GetNumLevels(), ",", "cost", "=", cost, "(", 100 * (cost - pJob->costInitial) / pJob->costInitial, "%", ")", ",", "duration", "=", pJob->duration, "s", ",", "elapsed", "=", GetElapsedTime(), "s");
if(cost < costBest) {
costBest = cost;
*pNtk = *(pJob->pNtk);
}
delete pJob->pNtk;
});
}
} else {
CreateJob(pNtk, iSeed);
OnJobEnd([&](Job *pJob) { (void)pJob; });
CreateJob(pNtk, iSeed, costStart);
OnJobEnd([&](Job *pJob) {
double cost = CostFunction(pJob->pNtk);
Print(0, "", "job", pJob->id, "(", nFinishedJobs + 1, "/", nJobs, ")", ":", "node", "=", pJob->pNtk->GetNumInts(), ",", "level", "=", pJob->pNtk->GetNumLevels(), ",", "cost", "=", cost, "(", 100 * (cost - pJob->costInitial) / pJob->costInitial, "%", ")", ",", "duration", "=", pJob->duration, "s", ",", "elapsed", "=", GetElapsedTime(), "s");
});
}
time_point end = GetCurrentTime();
double elapsed_seconds = Duration(start, end);
if(nVerbose) {
std::cout << "elapsed: " << std::fixed << std::setprecision(3) << elapsed_seconds << "s" << std::endl;
double cost = CostFunction(pNtk);
double duration = GetElapsedTime();
Print(0, "\n", "stats summary", ":");
for(std::string key: vStatsSummaryKeys) {
Print(0, "\t", SW{30, true}, key, ":", SW{10}, mStatsSummary[key]);
}
Print(0, "", "runtime summary", ":");
for(std::string key: vTimesSummaryKeys) {
Print(0, "\t", SW{30, true}, key, ":", mTimesSummary[key], "s", "(", 100 * mTimesSummary[key] / duration, "%", ")");
}
Print(0, "", "end", ":", "cost", "=", cost, "(", 100 * (cost - costStart) / costStart, "%", ")", ",", "time", "=", duration, "s");
}
/* }}} */

245
src/opt/rrr/rrrSimulator.h
View File

@ -29,6 +29,8 @@ namespace rrr {
int nWords;
// data
bool fGenerated;
bool fInitialized;
int target; // node for which the careset has been computed
std::vector<word> vValues;
std::vector<word> vValues2; // simulation with an inverter
@ -46,9 +48,14 @@ namespace rrr {
// backups
std::vector<Simulator> vBackups;
// statistics
int nAdds;
int nResets;
// stats
int nCex;
int nDiscarded;
int nPackedCountOld;
std::vector<int> vPackedCount;
std::vector<int> vPackedCountEvicted;
double durationSimulation;
double durationCare;
// vector computations
void Clear(int n, itr x) const;
@ -77,6 +84,9 @@ namespace rrr {
// careset computation
void ComputeCare(int id);
// preparation
void Initialize();
// save & load
void Save(int slot);
void Load(int slot);
@ -85,8 +95,7 @@ namespace rrr {
// constructors
Simulator();
Simulator(Parameter const *pPar);
~Simulator();
void UpdateNetwork(Ntk *pNtk_, bool fSame);
void AssignNetwork(Ntk *pNtk_, bool fReuse);
// checks
bool CheckRedundancy(int id, int idx);
@ -94,6 +103,11 @@ namespace rrr {
// cex
void AddCex(std::vector<VarValue> const &vCex);
// summary
void ResetSummary();
summary<int> GetStatsSummary() const;
summary<double> GetTimesSummary() const;
};
@ -195,53 +209,71 @@ namespace rrr {
template <typename Ntk>
void Simulator<Ntk>::ActionCallback(Action const &action) {
if(target == -1) {
return;
}
switch(action.type) {
case REMOVE_FANIN:
if(action.id == target) {
fUpdate = true;
} else {
sUpdates.insert(action.id);
assert(fInitialized);
if(target != -1) {
if(action.id == target) {
fUpdate = true;
} else {
sUpdates.insert(action.id);
}
}
break;
case REMOVE_UNUSED:
break;
case REMOVE_BUFFER:
case REMOVE_CONST:
if(action.id == target) {
if(fUpdate) {
for(int fo: action.vFanouts) {
sUpdates.insert(fo);
}
fUpdate = false;
}
target = -1;
} else {
if(sUpdates.count(action.id)) {
sUpdates.erase(action.id);
for(int fo: action.vFanouts) {
sUpdates.insert(fo);
if(fInitialized) {
if(target != -1) {
if(action.id == target) {
if(fUpdate) {
for(int fo: action.vFanouts) {
sUpdates.insert(fo);
}
fUpdate = false;
}
target = -1;
} else {
if(sUpdates.count(action.id)) {
sUpdates.erase(action.id);
for(int fo: action.vFanouts) {
sUpdates.insert(fo);
}
}
}
}
}
break;
case ADD_FANIN:
if(action.id == target) {
fUpdate = true;
} else {
sUpdates.insert(action.id);
assert(fInitialized);
if(target != -1) {
if(action.id == target) {
fUpdate = true;
} else {
sUpdates.insert(action.id);
}
}
break;
case TRIVIAL_COLLAPSE:
break;
case TRIVIAL_DECOMPOSE:
vValues.resize(nWords * pNtk->GetNumNodes());
SimulateNode(vValues, action.fi);
if(fInitialized) {
if(target != -1) {
vValues.resize(nWords * pNtk->GetNumNodes());
SimulateNode(vValues, action.fi);
// time of this simulation is not measured for simplicity sake
}
}
break;
case SORT_FANINS:
break;
case READ:
fInitialized = false;
if(action.fNew) {
fGenerated = false;
}
break;
case SAVE:
Save(action.idx);
break;
@ -345,6 +377,7 @@ namespace rrr {
template <typename Ntk>
void Simulator<Ntk>::Simulate() {
time_point timeStart = GetCurrentTime();
if(nVerbose) {
std::cout << "simulating" << std::endl;
}
@ -356,10 +389,12 @@ namespace rrr {
std::cout << std::endl;
}
});
durationSimulation += Duration(timeStart, GetCurrentTime());
}
template <typename Ntk>
void Simulator<Ntk>::Resimulate() {
time_point timeStart = GetCurrentTime();
if(nVerbose) {
std::cout << "resimulating" << std::endl;
}
@ -382,10 +417,12 @@ namespace rrr {
}
});
*/
durationSimulation += Duration(timeStart, GetCurrentTime());
}
template <typename Ntk>
void Simulator<Ntk>::SimulateOneWord(int offset) {
time_point timeStart = GetCurrentTime();
if(nVerbose) {
std::cout << "simulating word " << offset << std::endl;
}
@ -397,6 +434,7 @@ namespace rrr {
std::cout << std::endl;
}
});
durationSimulation += Duration(timeStart, GetCurrentTime());
}
/* }}} */
@ -440,6 +478,7 @@ namespace rrr {
sUpdates.clear();
}
target = id;
time_point timeStart = GetCurrentTime();
if(nVerbose) {
std::cout << "computing careset of " << target << std::endl;
}
@ -450,6 +489,7 @@ namespace rrr {
Print(nWords, care.begin());
std::cout << std::endl;
}
durationCare += Duration(timeStart, GetCurrentTime());
return;
}
vValues2 = vValues;
@ -484,10 +524,40 @@ namespace rrr {
Print(nWords, care.begin());
std::cout << std::endl;
}
durationCare += Duration(timeStart, GetCurrentTime());
}
/* }}} */
/* {{{ Preparation */
template <typename Ntk>
void Simulator<Ntk>::Initialize() {
if(!fGenerated) {
// TODO: reset nWords to default here maybe, if such a mechanism that changes nWords has been implemneted
vValues.resize(nWords * pNtk->GetNumNodes());
iPivot = 0;
vAssignedStimuli.clear();
vAssignedStimuli.resize(nWords * pNtk->GetNumPis());
for(int count: vPackedCount) {
if(count) {
vPackedCountEvicted.push_back(count);
}
}
vPackedCount.clear();
vPackedCount.resize(nWords * 64);
GenerateRandomStimuli();
fGenerated = true;
} else {
// use same nWords as we are reusing patterns even if nWords has changed
vValues.resize(nWords * pNtk->GetNumNodes());
}
Simulate();
fInitialized = true;
}
/* }}} */
/* {{{ Save & load */
template <typename Ntk>
@ -517,6 +587,12 @@ namespace rrr {
vBackups[slot].iPivot = iPivot;
vBackups[slot].vAssignedStimuli = vAssignedStimuli;
target = vBackups[slot].target; // assigned to -1 when careset needs updating
if(!fKeepStimula) {
vBackups[slot].nCex = nCex;
vBackups[slot].nPackedCountOld = nPackedCountOld;
vBackups[slot].vPackedCount = vPackedCount;
vBackups[slot].vPackedCountEvicted = vPackedCountEvicted;
}
}
template <typename Ntk>
@ -532,6 +608,11 @@ namespace rrr {
care = vBackups[slot].care;
iPivot = vBackups[slot].iPivot;
vAssignedStimuli = vBackups[slot].vAssignedStimuli;
nDiscarded += nCex - vBackups[slot].nCex;
nCex = vBackups[slot].nCex;
nPackedCountOld = vBackups[slot].nPackedCountOld;
vPackedCount = vBackups[slot].vPackedCount;
vPackedCountEvicted = vBackups[slot].vPackedCountEvicted;
tmp.resize(nWords);
} else {
std::vector<int> vOffsets;
@ -567,7 +648,7 @@ namespace rrr {
}
}
} else {
// when nWords has changed
// TODO: when nWords has changed
assert(0);
}
}
@ -582,11 +663,12 @@ namespace rrr {
pNtk(NULL),
nVerbose(0),
nWords(0),
fGenerated(false),
fInitialized(false),
target(-1),
iPivot(0),
fUpdate(false),
nAdds(0),
nResets(0) {
fUpdate(false) {
ResetSummary();
}
template <typename Ntk>
@ -594,38 +676,27 @@ namespace rrr {
pNtk(NULL),
nVerbose(pPar->nSimulatorVerbose),
nWords(pPar->nWords),
fGenerated(false),
fInitialized(false),
target(-1),
iPivot(0),
fUpdate(false),
nAdds(0),
nResets(0) {
fUpdate(false) {
care.resize(nWords);
tmp.resize(nWords);
ResetSummary();
}
template <typename Ntk>
Simulator<Ntk>::~Simulator() {
if(pNtk) {
std::cout << "simulator stats: added CEXs = " << nAdds << ", resets = " << nResets << std::endl;
void Simulator<Ntk>::AssignNetwork(Ntk *pNtk_, bool fReuse) {
if(!fReuse) {
fGenerated = false;
}
}
template <typename Ntk>
void Simulator<Ntk>::UpdateNetwork(Ntk *pNtk_, bool fSame) {
pNtk = pNtk_;
pNtk->AddCallback(std::bind(&Simulator<Ntk>::ActionCallback, this, std::placeholders::_1));
// TODO: what if nWords has changed? shall we reset it to default?
vValues.resize(nWords * pNtk->GetNumNodes());
fInitialized = false;
target = -1;
fUpdate = false;
sUpdates.clear();
if(!fSame) { // reset stimuli if network function changed
iPivot = 0;
vAssignedStimuli.clear();
vAssignedStimuli.resize(nWords * pNtk->GetNumPis());
GenerateRandomStimuli();
}
Simulate();
pNtk = pNtk_;
pNtk->AddCallback(std::bind(&Simulator<Ntk>::ActionCallback, this, std::placeholders::_1));
}
/* }}} */
@ -634,6 +705,9 @@ namespace rrr {
template <typename Ntk>
bool Simulator<Ntk>::CheckRedundancy(int id, int idx) {
if(!fInitialized) {
Initialize();
}
ComputeCare(id);
switch(pNtk->GetNodeType(id)) {
case AND: {
@ -671,6 +745,9 @@ namespace rrr {
template <typename Ntk>
bool Simulator<Ntk>::CheckFeasibility(int id, int fi, bool c) {
if(!fInitialized) {
Initialize();
}
ComputeCare(id);
switch(pNtk->GetNodeType(id)) {
case AND: {
@ -768,6 +845,7 @@ namespace rrr {
if(nVerbose) {
std::cout << "fusing into stimulus word " << iWord << " bit " << iBit << std::endl;
}
vPackedCount[iWord * 64 + iBit]++;
} else {
// no bits are compatible, so reset at pivot
iWord = iPivot / 64;
@ -775,6 +853,11 @@ namespace rrr {
if(nVerbose) {
std::cout << "resetting stimulus word " << iWord << " bit " << iBit << std::endl;
}
if(vPackedCount[iWord * 64 + iBit]) {
// this can be zero only when stats has been reset
vPackedCountEvicted.push_back(vPackedCount[iWord * 64 + iBit]);
}
vPackedCount[iWord * 64 + iBit] = 1;
word mask = 1ull << iBit;
for(int idx = 0; idx < pNtk->GetNumPis(); idx++) {
vAssignedStimuli[idx * nWords + iWord] &= ~mask;
@ -783,7 +866,6 @@ namespace rrr {
if(iPivot == 64 * nWords) {
iPivot = 0;
}
nResets++;
}
// update stimulus
for(int idx: vCarePiIdxs) {
@ -808,6 +890,7 @@ namespace rrr {
// simulate
SimulateOneWord(iWord);
// recompute care with new stimulus
time_point timeStart = GetCurrentTime();
if(target != -1 && !pNtk->IsPoDriver(target)) {
if(nVerbose) {
std::cout << "recomputing careset of " << target << std::endl;
@ -838,10 +921,56 @@ namespace rrr {
std::cout << std::endl;
}
}
nAdds++;
durationCare += Duration(timeStart, GetCurrentTime());
nCex++;
}
/* }}} */
/* {{{ Summary */
template <typename Ntk>
void Simulator<Ntk>::ResetSummary() {
nCex = 0;
nDiscarded = 0;
nPackedCountOld = 0;
for(int count: vPackedCount) {
if(count) {
nPackedCountOld++;
}
}
vPackedCountEvicted.clear();
durationSimulation = 0;
durationCare = 0;
};
template <typename Ntk>
summary<int> Simulator<Ntk>::GetStatsSummary() const {
summary<int> v;
v.emplace_back("sim cex", nCex);
if(!fKeepStimula) {
v.emplace_back("sim discarded cex", nDiscarded);
}
int nPackedCount = vPackedCountEvicted.size() - nPackedCountOld;
for(int count: vPackedCount) {
if(count) {
nPackedCount++;
}
}
v.emplace_back("sim packed pattern", nPackedCount);
v.emplace_back("sim evicted pattern", vPackedCountEvicted.size());
return v;
};
template <typename Ntk>
summary<double> Simulator<Ntk>::GetTimesSummary() const {
summary<double> v;
v.emplace_back("sim simulation", durationSimulation);
v.emplace_back("sim care computation", durationCare);
return v;
};
/* }}} */
}

5
src/opt/rrr/rrrTypes.h
View File

@ -39,6 +39,7 @@ namespace rrr {
TRIVIAL_COLLAPSE,
TRIVIAL_DECOMPOSE,
SORT_FANINS,
READ,
SAVE,
LOAD,
POP_BACK,
@ -51,6 +52,7 @@ namespace rrr {
int idx = -1;
int fi = -1;
bool c = false;
bool fNew = false;
std::vector<int> vFanins;
std::vector<int> vIndices;
std::vector<int> vFanouts;
@ -60,6 +62,9 @@ namespace rrr {
using clock_type = std::chrono::steady_clock;
using time_point = std::chrono::time_point<clock_type>;
template <typename T>
using summary = std::vector<std::pair<std::string, T>>;
}
ABC_NAMESPACE_CXX_HEADER_END

84
src/opt/rrr/rrrUtils.h
View File

@ -97,7 +97,8 @@ namespace rrr {
/* {{{ Print next */
struct SW {
int width;
int width = 0;
bool left = false;
};
struct NS {}; // no space
@ -107,6 +108,16 @@ namespace rrr {
template <typename T, typename... Args>
void PrintNext(std::ostream &os, T t, Args... args);
static inline void PrintNext(std::ostream &os, int t) {
os << std::setw(4) << t;
}
template <typename... Args>
static inline void PrintNext(std::ostream &os, int t, Args... args) {
os << std::setw(4) << t << " ";
PrintNext(os, args...);
}
static inline void PrintNext(std::ostream &os, bool arg) {
os << arg;
}
@ -121,16 +132,6 @@ namespace rrr {
PrintNext(os, args...);
}
static inline void PrintNext(std::ostream &os, int t) {
os << std::setw(4) << t;
}
template <typename... Args>
static inline void PrintNext(std::ostream &os, int t, Args... args) {
os << std::setw(4) << t << " ";
PrintNext(os, args...);
}
static inline void PrintNext(std::ostream &os, double t) {
os << std::fixed << std::setprecision(2) << std::setw(8) << t;
}
@ -143,12 +144,24 @@ namespace rrr {
template <typename T>
static inline void PrintNext(std::ostream &os, SW sw, T arg) {
if(sw.left) {
os << std::left;
}
os << std::setw(sw.width) << arg;
if(sw.left) {
os << std::right;
}
}
template <typename T, typename... Args>
static inline void PrintNext(std::ostream &os, SW sw, T arg, Args... args) {
if(sw.left) {
os << std::left;
}
os << std::setw(sw.width) << arg << " ";
if(sw.left) {
os << std::right;
}
PrintNext(os, args...);
}
@ -161,24 +174,20 @@ namespace rrr {
template <typename T>
static inline void PrintNext(std::ostream& os, std::vector<T> const &arg) {
std::string delim;
os << "[";
os << "[ ";
for(T const &e: arg) {
os << delim;
PrintNext(os, e);
delim = ", ";
os << " ";
}
os << "]";
}
template <typename T, typename... Args>
static inline void PrintNext(std::ostream& os, std::vector<T> const &arg, Args... args) {
std::string delim;
os << "[";
os << "[ ";
for(T const &e: arg) {
os << delim;
PrintNext(os, e);
delim = ", ";
os << " ";
}
os << "] ";
PrintNext(os, args...);
@ -186,24 +195,20 @@ namespace rrr {
template <typename T>
static inline void PrintNext(std::ostream& os, std::set<T> const &arg) {
std::string delim;
os << "{";
os << "{ ";
for(T const &e: arg) {
os << delim;
PrintNext(os, e);
delim = ", ";
os << " ";
}
os << "}";
}
template <typename T, typename... Args>
static inline void PrintNext(std::ostream& os, std::set<T> const &arg, Args... args) {
std::string delim;
os << "{";
os << "{ ";
for(T const &e: arg) {
os << delim;
PrintNext(os, e);
delim = ", ";
os << " ";
}
os << "} ";
PrintNext(os, args...);
@ -222,6 +227,14 @@ namespace rrr {
/* }}} */
/* {{{ Print others */
static inline void PrintWarning(std::string message) {
std::cerr << "[w] " << message << std::endl;
}
/* }}} */
/* {{{ Combination */
bool ForEachCombinationStopRec(std::vector<int> &v, int n, int k, std::function<bool(std::vector<int> const &)> const &func) {
@ -306,6 +319,8 @@ namespace rrr {
return "trivial decompose";
case SORT_FANINS:
return "sort fanins";
case READ:
return "read";
case SAVE:
return "save";
case LOAD:
@ -323,32 +338,35 @@ namespace rrr {
static inline std::stringstream GetActionDescription(Action const &action) {
std::stringstream ss;
ss << GetActionTypeCstr(action);
std::string delim = ": ";
std::string delim = " : ";
if(action.id != -1) {
ss << delim;
PrintNext(ss, "node", action.id);
delim = ", ";
delim = " , ";
}
if(action.fi != -1) {
ss << delim;
PrintNext(ss, "fanin", (bool)action.c, action.fi);
delim = ", ";
delim = " , ";
}
if(action.idx != -1) {
ss << delim;
PrintNext(ss, "index", action.idx);
}
if(action.fNew) {
ss << " new";
}
ss << std::endl;
if(!action.vFanins.empty()) {
ss << "fanins: ";
ss << "fanins : ";
PrintNext(ss, action.vFanins);
}
if(!action.vIndices.empty()) {
ss << "indices: ";
ss << "indices : ";
PrintNext(ss, action.vIndices);
}
if(!action.vFanouts.empty()) {
ss << "fanouts: ";
ss << "fanouts : ";
PrintNext(ss, action.vFanouts);
}
return ss;