Merge branch 'master' of https://github.com/cliffordwolf/yosys into btor

3 files changed, 29 insertions, 0 deletions

diff --git a/kernel/celltypes.h b/kernel/celltypes.h
index 2f311c82..9e63e9d1 100644
--- a/kernel/celltypes.h
+++ b/kernel/celltypes.h
@@ -96,6 +96,7 @@ struct CellTypes
 		cell_types.insert("$pmux");
 		cell_types.insert("$safe_pmux");
 		cell_types.insert("$lut");
+		cell_types.insert("$assert");
 	}
 
 	void setup_internals_mem()
diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc
index 66152573..7638d468 100644
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -595,6 +595,13 @@ namespace {
 				return;
 			}
 
+			if (cell->type == "$assert") {
+				port("\\A", 1);
+				port("\\EN", 1);
+				check_expected();
+				return;
+			}
+
 			if (cell->type == "$_INV_") { check_gate("AY"); return; }
 			if (cell->type == "$_AND_") { check_gate("ABY"); return; }
 			if (cell->type == "$_OR_")  { check_gate("ABY"); return; }
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;