Skip to content

Commit

Permalink
Updated readme; performance improvements, and added checks for circui…
Browse files Browse the repository at this point in the history
…ts with cycles.
  • Loading branch information
calmofthestorm committed Apr 11, 2013
1 parent c6cc31b commit 7ea0a31
Show file tree
Hide file tree
Showing 4 changed files with 31 additions and 8 deletions.
4 changes: 2 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -62,14 +62,14 @@ action, but this is difficult to implement in a platform-agnostic way.
Note that the primary purpose of writing this was to play with all the cool
new toys in C++11, and so I'm taking the excuse to use them wherever possible.

TODO:
* Infinite loop on non-combinational circuits (-> error)
ISSUES:
* Only supports small subset of BLIF.
(wontfix; it's sufficient for combinational circuits)
* BLIF requires that truth tables be unambiguous insofar as input vectors must
uniquely specify an output. Currently, if an input vector is ambiguous it will
be treated as 1; I would like this to instead be an error. (-> error)
* Test/configure build on Windows/Mac
* Migrate test suite to an actual framework

LEGAL:
This is a hobby project. It is published in the hope of being useful but I make
Expand Down
18 changes: 12 additions & 6 deletions blif.cc
Original file line number Diff line number Diff line change
Expand Up @@ -220,16 +220,14 @@ void BLIF::writeEvaluator(std::ostream& output, const string& fxn_name) const {
for (const auto& gate : mTruthTables) {
if (ordered.find(gate.first) == ordered.end()) {
std::stack<int> todo;
std::unordered_set<int> visited;
todo.push(gate.first);
while (!todo.empty()) {
int top_name = todo.top();
todo.pop();
// This second check is necessary if the same gate occurs twice in a
// given dependency tree. We could either index the stack with a set
// to prevent dupes on it or check here. This is better since a
// duplicate in the dep tree occasionally will waste less ram than
// doubling the storage of the dep stack, and both take the same time.
if (ordered.find(top_name) == ordered.end()) {
// Mark this node as visit started to catch cycles
visited.insert(top_name);
bool ready = true;
const TruthTable& top = mTruthTables.find(top_name)->second;
for (const auto& dependency : top.getInputs()) {
Expand All @@ -238,7 +236,15 @@ void BLIF::writeEvaluator(std::ostream& output, const string& fxn_name) const {
todo.push(top_name);
ready = false;
}
todo.push(dependency);

// If we attempt to visit a node we've already visited, and
// it has not been ordered, then there is a cycle.
if (visited.find(dependency) == visited.end()) {
todo.push(dependency);
} else {
throw CircularDependencyError(mLiteralsReverse.find(top_name)->second,
mLiteralsReverse.find(dependency)->second);
}
}
}
if (ready) {
Expand Down
10 changes: 10 additions & 0 deletions error.cc
Original file line number Diff line number Diff line change
Expand Up @@ -66,4 +66,14 @@ void UndefinedPrimaryOutputError::describe(ostream& os) const {
os << "Primary output " << mOutput << " is never defined." << endl;
}

CircularDependencyError::CircularDependencyError(const string& name1,
const string& name2)
: mName1(name1), mName2(name2) { }

void CircularDependencyError::describe(ostream& os) const {
os << "Circuit has circular dependency between " << mName1 << " and "
<< mName2 << "\n(The verifier only supports combinational circuits)"
<< endl;
}

} // namespace blifverifier
7 changes: 7 additions & 0 deletions error.h
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,13 @@ struct UndefinedPrimaryOutputError : LogicError {
void describe(std::ostream& os) const override;
};

struct CircularDependencyError : LogicError {
explicit CircularDependencyError(const std::string& name1,
const std::string& name2);
void describe(std::ostream& os) const override;
const std::string mName1, mName2;
};

} // namespace blifverifier

#endif

0 comments on commit 7ea0a31

Please sign in to comment.