From c36bac0e109b2a7192247cd3df9319f6f10a3e84 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sun, 19 Jan 2014 15:37:56 +0100
Subject: [PATCH] Added $assert support to satgen
---
kernel/satgen.h | 21 +++++++++++++++++++++
1 file changed, 21 insertions(+)
diff --git a/kernel/satgen.h b/kernel/satgen.h
index a668c73a4..0909e58ef 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;