Add $allconst and $allseq cell types

Signed-off-by: Clifford Wolf <clifford@clifford.at>

diff --git a/README.md b/README.md
index 92dc68a6a8431846ab7152a6bd128ae94afaa07c..87b231a5c51df08c65ff924635cc3f58122ec536 100644 (file)
--- a/README.md
+++ b/README.md
@@ -387,15 +387,20 @@ Non-standard or SystemVerilog features for formal verification
 - The system task ``$initstate`` evaluates to 1 in the initial state and
   to 0 otherwise.
 
-- The system task ``$anyconst`` evaluates to any constant value. This is
+- The system function ``$anyconst`` evaluates to any constant value. This is
   equivalent to declaring a reg as ``rand const``, but also works outside
   of checkers. (Yosys also supports ``rand const`` outside checkers.)
 
-- The system task ``$anyseq`` evaluates to any value, possibly a different
+- The system function ``$anyseq`` evaluates to any value, possibly a different
   value in each cycle. This is equivalent to declaring a reg as ``rand``,
   but also works outside of checkers. (Yosys also supports ``rand``
   variables outside checkers.)
 
+- The system functions ``$allconst`` and ``$allseq`` are used to construct formal
+  exist-forall problems. Assertions are only violated if the trace vialoates
+  the assertion for all ``$allconst/$allseq`` values and assumptions only hold
+  if the trace satisfies the assumtion for all ``$allconst/$allseq`` values.
+
 - The SystemVerilog tasks ``$past``, ``$stable``, ``$rose`` and ``$fell`` are
   supported in any clocked block.
 

diff --git a/examples/smtbmc/demo2.v b/examples/smtbmc/demo2.v
index 34745e89844b726bc811d74ee6b79aa473b60216..0cf529a4298b5f0e8928e675c4b8ba92efd7f967 100644 (file)
--- a/examples/smtbmc/demo2.v
+++ b/examples/smtbmc/demo2.v
@@ -9,7 +9,7 @@
 
 module demo2(input clk, input [4:0] addr, output reg [31:0] data);
        reg [31:0] mem [0:31];
-       always @(posedge clk)
+       always @(negedge clk)
                data <= mem[addr];
 
        reg [31:0] used_addr = 0;

diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc
index 3b08fc28db9c620f1add24d97234505ab2f9338f..57ba9668d02c4e78efe536ba37c3f34a74814530 100644 (file)
--- a/frontends/ast/genrtlil.cc
+++ b/frontends/ast/genrtlil.cc
@@ -764,7 +764,7 @@ void AstNode::detectSignWidthWorker(int &width_hint, bool &sign_hint, bool *foun
                break;
 
        case AST_FCALL:
-               if (str == "\\$anyconst" || str == "\\$anyseq") {
+               if (str == "\\$anyconst" || str == "\\$anyseq" || str == "\\$allconst" || str == "\\$allseq") {
                        if (GetSize(children) == 1) {
                                while (children[0]->simplify(true, false, false, 1, -1, false, true) == true) { }
                                if (children[0]->type != AST_CONSTANT)
@@ -1475,7 +1475,7 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
                } break;
 
        case AST_FCALL: {
-                       if (str == "\\$anyconst" || str == "\\$anyseq")
+                       if (str == "\\$anyconst" || str == "\\$anyseq" || str == "\\$allconst" || str == "\\$allseq")
                        {
                                string myid = stringf("%s$%d", str.c_str() + 1, autoidx++);
                                int width = width_hint;

diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index c454fb907ffd4c3752c05382ee0373b2f8d46168..a16fdfeebc81a61de318d1a4d50dc8cd4db3655f 100644 (file)
--- a/frontends/ast/simplify.cc
+++ b/frontends/ast/simplify.cc
@@ -1832,7 +1832,7 @@ skip_dynamic_range_lvalue_expansion:;
                        }
 
                        // $anyconst and $anyseq are mapped in AstNode::genRTLIL()
-                       if (str == "\\$anyconst" || str == "\\$anyseq") {
+                       if (str == "\\$anyconst" || str == "\\$anyseq" || str == "\\$allconst" || str == "\\$allseq") {
                                recursion_counter--;
                                return false;
                        }

diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y
index 9aa01c9f09f8554c9359d5460fb693e2b9ca207a..ba2fc036e638071a0257e911aa192f7ca3023942 100644 (file)
--- a/frontends/verilog/verilog_parser.y
+++ b/frontends/verilog/verilog_parser.y
@@ -1335,7 +1335,9 @@ rvalue:
                $$ = new AstNode(AST_IDENTIFIER, $2);
                $$->str = *$1;
                delete $1;
-               if ($2 == nullptr && ($$->str == "\\$initstate" || $$->str == "\\$anyconst" || $$->str == "\\$anyseq"))
+               if ($2 == nullptr && ($$->str == "\\$initstate" ||
+                               $$->str == "\\$anyconst" || $$->str == "\\$anyseq" ||
+                               $$->str == "\\$allconst" || $$->str == "\\$allseq"))
                        $$->type = AST_FCALL;
        } |
        hierarchical_id non_opt_multirange {

diff --git a/kernel/celltypes.h b/kernel/celltypes.h
index 5218b536369206f1cdf9383661f06f4c227c1c87..fcc4fcc4bca504e0817fddf7b2aeb84674273d9f 100644 (file)
--- a/kernel/celltypes.h
+++ b/kernel/celltypes.h
@@ -122,6 +122,8 @@ struct CellTypes
                setup_type("$initstate", pool<RTLIL::IdString>(), {Y}, true);
                setup_type("$anyconst", pool<RTLIL::IdString>(), {Y}, true);
                setup_type("$anyseq", pool<RTLIL::IdString>(), {Y}, true);
+               setup_type("$allconst", pool<RTLIL::IdString>(), {Y}, true);
+               setup_type("$allseq", pool<RTLIL::IdString>(), {Y}, true);
                setup_type("$equiv", {A, B}, {Y}, true);
        }
 

diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc
index fb3d9dbe9e78aa637521ab6404d772e83290569f..a4fa2cf047224d57a13615a7e723f73b9d210cd7 100644 (file)
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -1101,7 +1101,7 @@ namespace {
                                return;
                        }
 
-                       if (cell->type.in("$anyconst", "$anyseq")) {
+                       if (cell->type.in("$anyconst", "$anyseq", "$allconst", "$allseq")) {
                                port("\\Y", param("\\WIDTH"));
                                check_expected();
                                return;
@@ -2145,6 +2145,26 @@ RTLIL::SigSpec RTLIL::Module::Anyseq(RTLIL::IdString name, int width, const std:
        return sig;
 }
 
+RTLIL::SigSpec RTLIL::Module::Allconst(RTLIL::IdString name, int width, const std::string &src)
+{
+       RTLIL::SigSpec sig = addWire(NEW_ID, width);
+       Cell *cell = addCell(name, "$allconst");
+       cell->setParam("\\WIDTH", width);
+       cell->setPort("\\Y", sig);
+       cell->set_src_attribute(src);
+       return sig;
+}
+
+RTLIL::SigSpec RTLIL::Module::Allseq(RTLIL::IdString name, int width, const std::string &src)
+{
+       RTLIL::SigSpec sig = addWire(NEW_ID, width);
+       Cell *cell = addCell(name, "$allseq");
+       cell->setParam("\\WIDTH", width);
+       cell->setPort("\\Y", sig);
+       cell->set_src_attribute(src);
+       return sig;
+}
+
 RTLIL::SigSpec RTLIL::Module::Initstate(RTLIL::IdString name, const std::string &src)
 {
        RTLIL::SigSpec sig = addWire(NEW_ID);

diff --git a/kernel/rtlil.h b/kernel/rtlil.h
index a251b425273ac07f8f99c5a55336d219beb4923b..54d0b8c2215653e8c25ae65b2acc0feeb539cffc 100644 (file)
--- a/kernel/rtlil.h
+++ b/kernel/rtlil.h
@@ -1127,6 +1127,8 @@ public:
 
        RTLIL::SigSpec Anyconst  (RTLIL::IdString name, int width = 1, const std::string &src = "");
        RTLIL::SigSpec Anyseq    (RTLIL::IdString name, int width = 1, const std::string &src = "");
+       RTLIL::SigSpec Allconst  (RTLIL::IdString name, int width = 1, const std::string &src = "");
+       RTLIL::SigSpec Allseq    (RTLIL::IdString name, int width = 1, const std::string &src = "");
        RTLIL::SigSpec Initstate (RTLIL::IdString name, const std::string &src = "");
 };
 

diff --git a/manual/CHAPTER_CellLib.tex b/manual/CHAPTER_CellLib.tex
index c36e61b05674c1a8a66ad053999c1825d82d7d04..277e893284cd5f54ebe37e54447b15130b6c45ae 100644 (file)
--- a/manual/CHAPTER_CellLib.tex
+++ b/manual/CHAPTER_CellLib.tex
@@ -421,7 +421,8 @@ 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}, {\tt \$assume}, {\tt \$live}, {\tt \$fair}, {\tt \$cover}, {\tt \$equiv}, {\tt \$initstate}, {\tt \$anyconst}, and {\tt \$anyseq} cells.
+Add information about {\tt \$assert}, {\tt \$assume}, {\tt \$live}, {\tt \$fair}, {\tt \$cover}, {\tt \$equiv},
+{\tt \$initstate}, {\tt \$anyconst}, {\tt \$anyseq}, {\tt \$allconst}, {\tt \$allseq} cells.
 \end{fixme}
 
 \begin{fixme}

diff --git a/passes/opt/opt_merge.cc b/passes/opt/opt_merge.cc
index 93d9f012ffb7286c2a626c490772393f874102ed..2aeb514e4c26a8def798b853e9be96e2afe079f2 100644 (file)
--- a/passes/opt/opt_merge.cc
+++ b/passes/opt/opt_merge.cc
@@ -279,6 +279,8 @@ struct OptMergeWorker
                ct.cell_types.erase("$_TBUF_");
                ct.cell_types.erase("$anyseq");
                ct.cell_types.erase("$anyconst");
+               ct.cell_types.erase("$allseq");
+               ct.cell_types.erase("$allconst");
 
                log("Finding identical cells in module `%s'.\n", module->name.c_str());
                assign_map.set(module);

diff --git a/techlibs/common/simlib.v b/techlibs/common/simlib.v
index 276503fe88437a360f4cae7e2bc9a34cd2f34ca8..8e43fe058de6b277206015db87946760b9913a47 100644 (file)
--- a/techlibs/common/simlib.v
+++ b/techlibs/common/simlib.v
@@ -1370,6 +1370,30 @@ endmodule
 
 // --------------------------------------------------------
 
+module \$allconst (Y);
+
+parameter WIDTH = 0;
+
+output [WIDTH-1:0] Y;
+
+assign Y = 'bx;
+
+endmodule
+
+// --------------------------------------------------------
+
+module \$allseq (Y);
+
+parameter WIDTH = 0;
+
+output [WIDTH-1:0] Y;
+
+assign Y = 'bx;
+
+endmodule
+
+// --------------------------------------------------------
+
 module \$equiv (A, B, Y);
 
 input A, B;