Added $anyseq cell type

backends/smt2/smt2.cc

@@ -417,7 +417,7 @@ struct Smt2Worker
 				return;
 			}
 
-			if (cell->type == "$anyconst")
+			if (cell->type.in("$anyconst", "$anyseq"))
 			{
 				registers.insert(cell);
 				decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, get_id(module), idcounter,

examples/smtbmc/demo7.v

@@ -1,6 +1,7 @@
 // Demo for memory initialization
 
-module demo7 (input [2:0] addr);
+module demo7;
+	wire [2:0] addr = $anyseq;
 	reg [15:0] memory [0:7];
 
 	initial begin

frontends/ast/genrtlil.cc

@@ -762,7 +762,7 @@ void AstNode::detectSignWidthWorker(int &width_hint, bool &sign_hint, bool *foun
 		break;
 
 	case AST_FCALL:
-		if (str == "\\$anyconst") {
+		if (str == "\\$anyconst" || str == "\\$anyseq") {
 			if (GetSize(children) == 1) {
 				while (children[0]->simplify(true, false, false, 1, -1, false, true) == true) { }
 				if (children[0]->type != AST_CONSTANT)
@@ -1465,7 +1465,7 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
 		} break;
 
 	case AST_FCALL: {
-			if (str == "\\$anyconst")
+			if (str == "\\$anyconst" || str == "\\$anyseq")
 			{
 				string myid = stringf("%s$%d", str.c_str() + 1, autoidx++);
 				int width = width_hint;

frontends/ast/simplify.cc

@@ -1807,8 +1807,8 @@ skip_dynamic_range_lvalue_expansion:;
 				goto apply_newNode;
 			}
 
-			// $anyconst is mapped in AstNode::genRTLIL()
-			if (str == "\\$anyconst") {
+			// $anyconst and $anyseq are mapped in AstNode::genRTLIL()
+			if (str == "\\$anyconst" || str == "\\$anyseq") {
 				recursion_counter--;
 				return false;
 			}

frontends/verilog/verilog_parser.y

@@ -1229,7 +1229,7 @@ rvalue:
 		$$ = new AstNode(AST_IDENTIFIER, $2);
 		$$->str = *$1;
 		delete $1;
-		if ($2 == nullptr && formal_mode && ($$->str == "\\$initstate" || $$->str == "\\$anyconst"))
+		if ($2 == nullptr && formal_mode && ($$->str == "\\$initstate" || $$->str == "\\$anyconst" || $$->str == "\\$anyseq"))
 			$$->type = AST_FCALL;
 	} |
 	hierarchical_id non_opt_multirange {

kernel/celltypes.h

@@ -118,6 +118,7 @@ struct CellTypes
 		setup_type("$assume", {A, EN}, pool<RTLIL::IdString>(), true);
 		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("$equiv", {A, B}, {Y}, true);
 	}
 

kernel/rtlil.cc

@@ -1037,7 +1037,7 @@ namespace {
 				return;
 			}
 
-			if (cell->type == "$anyconst") {
+			if (cell->type.in("$anyconst", "$anyseq")) {
 				port("\\Y", param("\\WIDTH"));
 				check_expected();
 				return;
@@ -2009,6 +2009,15 @@ RTLIL::SigSpec RTLIL::Module::Anyconst(RTLIL::IdString name, int width)
 	return sig;
 }
 
+RTLIL::SigSpec RTLIL::Module::Anyseq(RTLIL::IdString name, int width)
+{
+	RTLIL::SigSpec sig = addWire(NEW_ID, width);
+	Cell *cell = addCell(name, "$anyseq");
+	cell->setParam("\\WIDTH", width);
+	cell->setPort("\\Y", sig);
+	return sig;
+}
+
 RTLIL::SigSpec RTLIL::Module::Initstate(RTLIL::IdString name)
 {
 	RTLIL::SigSpec sig = addWire(NEW_ID);

kernel/rtlil.h

@@ -1108,6 +1108,7 @@ public:
 	RTLIL::SigBit Oai4Gate (RTLIL::IdString name, RTLIL::SigBit sig_a, RTLIL::SigBit sig_b, RTLIL::SigBit sig_c, RTLIL::SigBit sig_d);
 
 	RTLIL::SigSpec Anyconst  (RTLIL::IdString name, int width = 1);
+	RTLIL::SigSpec Anyseq    (RTLIL::IdString name, int width = 1);
 	RTLIL::SigSpec Initstate (RTLIL::IdString name);
 };
 

kernel/satgen.h

@@ -1332,8 +1332,8 @@ struct SatGen
 
 			if (model_undef)
 			{
-				std::vector<int> undef_d = importUndefSigSpec(cell->getPort("\\D"), timestep-1);
-				std::vector<int> undef_q = importUndefSigSpec(cell->getPort("\\Q"), timestep);
+				std::vector<int> undef_d = importUndefSigSpec(cell->getPort("\\Y"), timestep-1);
+				std::vector<int> undef_q = importUndefSigSpec(cell->getPort("\\Y"), timestep);
 
 				ez->assume(ez->vec_eq(undef_d, undef_q));
 				undefGating(q, qq, undef_q);
@@ -1341,6 +1341,11 @@ struct SatGen
 			return true;
 		}
 
+		if (cell->type == "$anyseq")
+		{
+			return true;
+		}
+
 		if (cell->type == "$_BUF_" || cell->type == "$equiv")
 		{
 			std::vector<int> a = importDefSigSpec(cell->getPort("\\A"), timestep);

manual/CHAPTER_CellLib.tex

@@ -421,7 +421,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}, {\tt \$assume}, {\tt \$equiv}, {\tt \$initstate}, and {\tt \$anyconst} cells.
+Add information about {\tt \$assert}, {\tt \$assume}, {\tt \$equiv}, {\tt \$initstate}, {\tt \$anyconst}, and {\tt \$anyseq} cells.
 \end{fixme}
 
 \begin{fixme}

techlibs/common/simlib.v

@@ -1334,6 +1334,18 @@ endmodule
 
 // --------------------------------------------------------
 
+module \$anyseq (Y);
+
+parameter WIDTH = 0;
+
+output [WIDTH-1:0] Y;
+
+assign Y = 'bx;
+
+endmodule
+
+// --------------------------------------------------------
+
 module \$equiv (A, B, Y);
 
 input A, B;