Added $assume cell type

3 files changed, 38 insertions, 0 deletions

diff --git a/kernel/celltypes.h b/kernel/celltypes.h
index 57bcde47..533c370f 100644
--- a/kernel/celltypes.h
+++ b/kernel/celltypes.h
@@ -114,6 +114,7 @@ struct CellTypes
 		setup_type("$fa", {A, B, C}, {X, Y}, true);
 
 		setup_type("$assert", {A, EN}, pool<RTLIL::IdString>(), true);
+		setup_type("$assume", {A, EN}, pool<RTLIL::IdString>(), true);
 		setup_type("$equiv", {A, B}, {Y}, true);
 	}
 
diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc
index c10261b2..adf89a24 100644
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -941,6 +941,13 @@ namespace {
 				return;
 			}
 
+			if (cell->type == "$assume") {
+				port("\\A", 1);
+				port("\\EN", 1);
+				check_expected();
+				return;
+			}
+
 			if (cell->type == "$equiv") {
 				port("\\A", 1);
 				port("\\B", 1);
diff --git a/kernel/satgen.h b/kernel/satgen.h
index 093d248d..719b0a83 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -68,6 +68,7 @@ struct SatGen
 	std::string prefix;
 	SigPool initial_state;
 	std::map<std::string, RTLIL::SigSpec> asserts_a, asserts_en;
+	std::map<std::string, RTLIL::SigSpec> assumes_a, assumes_en;
 	std::map<std::string, std::map<RTLIL::SigBit, int>> imported_signals;
 	bool ignore_div_by_zero;
 	bool model_undef;
@@ -161,6 +162,13 @@ struct SatGen
 		sig_en = asserts_en[pf];
 	}
 
+	void getAssumes(RTLIL::SigSpec &sig_a, RTLIL::SigSpec &sig_en, int timestep = -1)
+	{
+		std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
+		sig_a = assumes_a[pf];
+		sig_en = assumes_en[pf];
+	}
+
 	int importAsserts(int timestep = -1)
 	{
 		std::vector<int> check_bits, enable_bits;
@@ -175,6 +183,20 @@ struct SatGen
 		return ez->vec_reduce_and(ez->vec_or(check_bits, ez->vec_not(enable_bits)));
 	}
 
+	int importAssumes(int timestep = -1)
+	{
+		std::vector<int> check_bits, enable_bits;
+		std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
+		if (model_undef) {
+			check_bits = ez->vec_and(ez->vec_not(importUndefSigSpec(assumes_a[pf], timestep)), importDefSigSpec(assumes_a[pf], timestep));
+			enable_bits = ez->vec_and(ez->vec_not(importUndefSigSpec(assumes_en[pf], timestep)), importDefSigSpec(assumes_en[pf], timestep));
+		} else {
+			check_bits = importDefSigSpec(assumes_a[pf], timestep);
+			enable_bits = importDefSigSpec(assumes_en[pf], 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)
@@ -1234,6 +1256,14 @@ struct SatGen
 			return true;
 		}
 
+		if (cell->type == "$assume")
+		{
+			std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
+			assumes_a[pf].append((*sigmap)(cell->getPort("\\A")));
+			assumes_en[pf].append((*sigmap)(cell->getPort("\\EN")));
+			return true;
+		}
+
 		// Unsupported internal cell types: $pow $lut
 		// .. and all sequential cells except $dff and $_DFF_[NP]_
 		return false;