Add $allconst and $allseq cell types

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

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.
 

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;

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;

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;
 			}

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 {

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);
 	}
 

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);

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 = "");
 };
 

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}

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);

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;