rrr::BddAnalyzer< Ntk > Class Template Reference

#include <rrrBddAnalyzer.h>

Public Member Functions
	BddAnalyzer ()
	BddAnalyzer (Parameter const *pPar)
	~BddAnalyzer ()
void	AssignNetwork (Ntk *pNtk_, bool fReuse)
bool	CheckRedundancy (int id, int idx)
bool	CheckFeasibility (int id, int fi, bool c)
void	ResetSummary ()
summary< int >	GetStatsSummary () const
summary< double >	GetTimesSummary () const

Detailed Description

template<typename Ntk>
class rrr::BddAnalyzer< Ntk >

Definition at line 12 of file rrrBddAnalyzer.h.

Constructor & Destructor Documentation

BddAnalyzer() [1/2]

template<typename Ntk>

rrr::BddAnalyzer< Ntk >::BddAnalyzer

(

)

Definition at line 602 of file rrrBddAnalyzer.h.

                                :
    pNtk(NULL),
    nVerbose(0),
    fInitialized(false),
    pBdd(NULL),
    target(-1),
    fResim(false) {
    ResetSummary();
  }

Here is the call graph for this function:

BddAnalyzer() [2/2]

template<typename Ntk>

rrr::BddAnalyzer< Ntk >::BddAnalyzer

(

Parameter const *

pPar

)

Definition at line 613 of file rrrBddAnalyzer.h.

                                                     :
    pNtk(NULL),
    nVerbose(pPar->nAnalyzerVerbose),
    fInitialized(false),
    pBdd(NULL),
    target(-1),
    fResim(false) {
    ResetSummary();
  }

Here is the call graph for this function:

~BddAnalyzer()

template<typename Ntk>

rrr::BddAnalyzer< Ntk >::~BddAnalyzer

(

)

Definition at line 624 of file rrrBddAnalyzer.h.

                                 {
    Reset();
  }

Member Function Documentation

AssignNetwork()

template<typename Ntk>

void rrr::BddAnalyzer< Ntk >::AssignNetwork	(	Ntk *	pNtk_,
		bool	fReuse )

Definition at line 629 of file rrrBddAnalyzer.h.

                                                              {
    Reset(fReuse);
    pNtk = pNtk_;
    pNtk->AddCallback(std::bind(&BddAnalyzer<Ntk>::ActionCallback, this, std::placeholders::_1));
  }

CheckFeasibility()

template<typename Ntk>

bool rrr::BddAnalyzer< Ntk >::CheckFeasibility	(	int	id,
		int	fi,
		bool	c )

Definition at line 675 of file rrrBddAnalyzer.h.

                                                                {
    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;
    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]);
      IncRef(x);
      lit y = pBdd->Or(x, pBdd->LitNotCond(vFs[fi], c));
      DecRef(x);
      if(pBdd->IsConst1(y)) {
        fFeasible = true;
      }
      break;
    }
    default:
      assert(0);
    }
    if(nVerbose) {
      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;
      }
    }
    durationCheck += Duration(timeStart, GetCurrentTime());
    return fFeasible;
  }

CheckRedundancy()

template<typename Ntk>

bool rrr::BddAnalyzer< Ntk >::CheckRedundancy	(	int	id,
		int	idx )

Definition at line 640 of file rrrBddAnalyzer.h.

                                                        {
    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)) {
        fRedundant = true;
      }
      break;
    }
    default:
      assert(0);
    }
    if(nVerbose) {
      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;
      }
    }
    durationCheck += Duration(timeStart, GetCurrentTime());
    return fRedundant;
  }

GetStatsSummary()

template<typename Ntk>

summary< int > rrr::BddAnalyzer< Ntk >::GetStatsSummary

(

)

const

Definition at line 732 of file rrrBddAnalyzer.h.

                                                       {
    summary<int> v;
    v.emplace_back("bdd node", pBdd->GetNumTotalCreatedNodes() - nNodesOld + nNodesAccumulated);
    return v;
  }

GetTimesSummary()

template<typename Ntk>

summary< double > rrr::BddAnalyzer< Ntk >::GetTimesSummary

(

)

const

Definition at line 739 of file rrrBddAnalyzer.h.

                                                          {
    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;
  }

ResetSummary()

template<typename Ntk>

void rrr::BddAnalyzer< Ntk >::ResetSummary

(

)

Definition at line 718 of file rrrBddAnalyzer.h.

                                      {
    if(pBdd) {
      nNodesOld = pBdd->GetNumTotalCreatedNodes();
    } else {
      nNodesOld = 0;
    }
    nNodesAccumulated = 0;
    durationSimulation = 0;
    durationPf = 0;
    durationCheck = 0;
    durationReorder = 0;
  }

Here is the caller graph for this function:

---

The documentation for this class was generated from the following file:

• src/opt/rrr/rrrBddAnalyzer.h