summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-01-19 15:37:56 +0100
committerClifford Wolf <clifford@clifford.at>2014-01-19 15:37:56 +0100
commitc36bac0e109b2a7192247cd3df9319f6f10a3e84 (patch)
tree1ff8677820b9cf1fe11601e1f1c7ddc1f33b9428
parent1e67099b77904802880ad7c53d2cac33c6df456f (diff)
Added $assert support to satgen
-rw-r--r--kernel/satgen.h21
1 files changed, 21 insertions, 0 deletions
diff --git a/kernel/satgen.h b/kernel/satgen.h
index a668c73a..0909e58e 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -38,6 +38,7 @@ struct SatGen
SigMap *sigmap;
std::string prefix;
SigPool initial_state;
+ RTLIL::SigSpec asserts_a, asserts_en;
bool ignore_div_by_zero;
bool model_undef;
@@ -96,6 +97,19 @@ struct SatGen
return importSigSpecWorker(sig, pf, true, false);
}
+ int importAsserts(int timestep = -1)
+ {
+ std::vector<int> check_bits, enable_bits;
+ if (model_undef) {
+ check_bits = ez->vec_and(ez->vec_not(importUndefSigSpec(asserts_a, timestep)), importDefSigSpec(asserts_a, timestep));
+ enable_bits = ez->vec_and(ez->vec_not(importUndefSigSpec(asserts_en, timestep)), importDefSigSpec(asserts_en, timestep));
+ } else {
+ check_bits = importDefSigSpec(asserts_a, timestep);
+ enable_bits = importDefSigSpec(asserts_en, timestep);
+ }
+ return ez->vec_reduce_and(ez->vec_or(check_bits, ez->vec_not(enable_bits)));
+ }
+
int signals_eq(RTLIL::SigSpec lhs, RTLIL::SigSpec rhs, int timestep_lhs = -1, int timestep_rhs = -1)
{
if (timestep_rhs < 0)
@@ -765,6 +779,13 @@ struct SatGen
return true;
}
+ if (cell->type == "$assert")
+ {
+ asserts_a.append((*sigmap)(cell->connections.at("\\A")));
+ asserts_en.append((*sigmap)(cell->connections.at("\\EN")));
+ return true;
+ }
+
// Unsupported internal cell types: $pow $lut
// .. and all sequential cells except $dff and $_DFF_[NP]_
return false;