Skip to content

update rrr #405

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
alanminko merged 1 commit into from
Apr 24, 2025
Merged

update rrr #405

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/aig/gia/giaRrr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}

Expand Down
57 changes: 51 additions & 6 deletions src/base/abci/abc.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 )
{
Expand Down Expand Up @@ -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 );
Expand All @@ -45599,10 +45644,10 @@ int Abc_CommandAbc9Rrr( Abc_Frame_t * pAbc, int argc, char ** argv )
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 );
Expand All @@ -45617,7 +45662,7 @@ int Abc_CommandAbc9Rrr( Abc_Frame_t * pAbc, int argc, char ** argv )
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;
Expand Down
16 changes: 11 additions & 5 deletions src/opt/rrr/rrrAbc.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand All @@ -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) {
Expand All @@ -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;
}

Expand All @@ -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);
}

}
Expand Down
49 changes: 44 additions & 5 deletions src/opt/rrr/rrrAnalyzer.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 */
Expand All @@ -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);
}

/* }}} */
Expand All @@ -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;
}
Expand All @@ -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;
}

/* }}} */

}

Expand Down
36 changes: 30 additions & 6 deletions src/opt/rrr/rrrAndNetwork.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,20 +64,21 @@ 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;
int GetNumNodes() const; // number of allocated nodes (max id + 1)
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;
Expand Down Expand Up @@ -272,7 +273,7 @@ namespace rrr {

/* {{{ Initialization APIs */

void AndNetwork::Clear() {
void AndNetwork::Clear(bool fClearCallbacks) {
nNodes = 0;
vPis.clear();
lInts.clear();
Expand All @@ -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();
Expand Down Expand Up @@ -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);
}

/* }}} */
Expand All @@ -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;
}
Expand Down
Loading
Loading