Added $assume cell type

diff --git a/kernel/celltypes.h b/kernel/celltypes.h
index 57bcde47104ffb7770b57a94dd8f9244a9fd8dba..533c370fe24313d3beacf300e47c0cedc4d314e2 100644 (file)
--- 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 c10261b23772524d3736a13749a10509bf5697fd..adf89a24510518464ac34dd8e79ffd6f6cd64f11 100644 (file)
--- 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 093d248d4acfad62c6ec0fce94ccf9846a03766b..719b0a83a18d5334483686be97bfee7fe3ae4e60 100644 (file)
--- 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;

diff --git a/manual/CHAPTER_CellLib.tex b/manual/CHAPTER_CellLib.tex
index 43d40c73fbd2c3e5ebef946bb5e1e15213a00494..c9bf978a9dda15422d3eacbf84a382b5aa7b7aa5 100644 (file)
--- a/manual/CHAPTER_CellLib.tex
+++ b/manual/CHAPTER_CellLib.tex
@@ -417,7 +417,7 @@ pass. The combinatorial logic cells can be mapped to physical cells from a Liber
 using the {\tt abc} pass.
 
 \begin{fixme}
-Add information about {\tt \$assert} and {\tt \$equiv} cells.
+Add information about {\tt \$assert}, {\tt \$assume}, and {\tt \$equiv} cells.
 \end{fixme}
 
 \begin{fixme}

diff --git a/techlibs/common/simlib.v b/techlibs/common/simlib.v
index bc343c62dddf9dc9499b51935100dc4cbc548d61..abd2af521f622588683358f5c23fa558e3e6ba83 100644 (file)
--- a/techlibs/common/simlib.v
+++ b/techlibs/common/simlib.v
@@ -1163,7 +1163,24 @@ input A, EN;
 `ifndef SIMLIB_NOCHECKS
 always @* begin
        if (A !== 1'b1 && EN === 1'b1) begin
-               $display("Assertation failed!");
+               $display("Assertation %m failed!");
+               $stop;
+       end
+end
+`endif
+
+endmodule
+
+// --------------------------------------------------------
+
+module \$assume (A, EN);
+
+input A, EN;
+
+`ifndef SIMLIB_NOCHECKS
+always @* begin
+       if (A !== 1'b1 && EN === 1'b1) begin
+               $display("Assumption %m failed!");
                $stop;
        end
 end