SPIN verification (PoC)

MODULE.bazel

@@ -150,6 +150,10 @@ use_repo(perfetto_ext, "perfetto_cfg")
 # Perfetto requires this to get through bazel analysis, but seems unused for our use.
 bazel_dep(name = "rules_android", version = "0.6.0")
 
+# SPIN model checker — used by xls/spin to verify Promela models generated from XLS IR.
+spin_ext = use_extension("//dependency_support/spin:extension.bzl", "spin_extension")
+use_repo(spin_ext, "spin")
+
 # Pin this as otherwise we encounter some bazel analysis failure.
 bazel_dep(name = "rules_jvm_external", version = "6.8")
 

dependency_support/spin/BUILD.bazel

@@ -0,0 +1,17 @@
+# Copyright 2026 The XLS Authors
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#      http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+# Support files for the SPIN model-checker dependency.
+
+exports_files(["bundled.BUILD.bazel"])

dependency_support/spin/bundled.BUILD.bazel

@@ -0,0 +1,94 @@
+# Copyright 2026 The XLS Authors
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#      http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+# Build rules for the SPIN model checker.
+# https://spinroot.com / https://github.com/nimble-code/Spin
+
+load("@rules_cc//cc:defs.bzl", "cc_binary")
+
+licenses(["notice"])  # BSD-like, see Src/LICENSE
+
+exports_files(["Src/LICENSE"])
+
+package(default_visibility = ["//visibility:public"])
+
+# Process spin.y with bison; produces y.tab.c and y.tab.h.
+genrule(
+    name = "spin_yacc_gen",
+    srcs = ["Src/spin.y"],
+    outs = [
+        "y.tab.c",
+        "y.tab.h",
+    ],
+    cmd = "M4=$(M4) $(BISON) --yacc --defines=$(location y.tab.h) -o $(location y.tab.c) $(location Src/spin.y) 2>/dev/null",
+    toolchains = [
+        "@rules_bison//bison:current_bison_toolchain",
+        "@rules_m4//m4:current_m4_toolchain",
+    ],
+    visibility = ["//visibility:private"],
+)
+
+cc_binary(
+    name = "spin",
+    srcs = [
+        "Src/dstep.c",
+        "Src/flow.c",
+        "Src/guided.c",
+        "Src/main.c",
+        "Src/mesg.c",
+        "Src/msc_tcl.c",
+        "Src/pangen1.c",
+        "Src/pangen1.h",
+        "Src/pangen2.c",
+        "Src/pangen2.h",
+        "Src/pangen3.c",
+        "Src/pangen3.h",
+        "Src/pangen4.c",
+        "Src/pangen4.h",
+        "Src/pangen5.c",
+        "Src/pangen5.h",
+        "Src/pangen6.c",
+        "Src/pangen6.h",
+        "Src/pangen7.c",
+        "Src/pangen7.h",
+        "Src/reprosrc.c",
+        "Src/run.c",
+        "Src/sched.c",
+        "Src/spin.h",
+        "Src/spinlex.c",
+        "Src/structs.c",
+        "Src/sym.c",
+        "Src/tl.h",
+        "Src/tl_buchi.c",
+        "Src/tl_cache.c",
+        "Src/tl_lex.c",
+        "Src/tl_main.c",
+        "Src/tl_mem.c",
+        "Src/tl_parse.c",
+        "Src/tl_rewrt.c",
+        "Src/tl_trans.c",
+        "Src/vars.c",
+        "Src/version.h",
+        ":spin_yacc_gen",
+    ],
+    copts = [
+        "-O2",
+        "-DNXT",
+        "-w",
+    ],
+    includes = [
+        ".",
+        "Src",
+    ],
+)

dependency_support/spin/extension.bzl

@@ -0,0 +1,35 @@
+# Copyright 2026 The XLS Authors
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#      http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+"""Module extension for the SPIN model checker (https://spinroot.com)."""
+
+load("@bazel_tools//tools/build_defs/repo:http.bzl", "http_archive")
+
+def _spin_extension_impl(_ctx):
+    http_archive(
+        name = "spin",
+        sha256 = "e2ba8cfebf963cb524be2a3caee68821472602f9c4f0e557f2550d8e382eab99",
+        strip_prefix = "Spin-master",
+        urls = ["https://github.com/nimble-code/Spin/archive/refs/heads/master.tar.gz"],
+        build_file = Label("//dependency_support/spin:bundled.BUILD.bazel"),
+        patches = [
+            # Adds -Q <file>: emit one JSON line per channel event during simulation.
+            # Adds -K<dir>: pan writes .trail files into <dir> instead of cwd.
+            # Adds -H: pan exits with code 1 when errors > 0 (default is 0).
+            Label("//dependency_support/spin/patches:spin.patch"),
+        ],
+        patch_args = ["-p1", "--fuzz=3"],
+    )
+
+spin_extension = module_extension(implementation = _spin_extension_impl)

dependency_support/spin/patches/BUILD.bazel

@@ -0,0 +1,15 @@
+# Copyright 2026 The XLS Authors
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#      http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+exports_files(["spin.patch"])

dependency_support/spin/patches/spin.patch

@@ -0,0 +1,137 @@
+--- a/Src/main.c
++++ b/Src/main.c
+@@ -50,6 +50,7 @@
+ int	old_scope_rules;	/* use pre 5.3.0 rules */
+ int	old_priority_rules;	/* use pre 6.2.0 rules */
+ int	product, Strict;
++FILE	*json_trace_fp = NULL;	/* output file for -Q JSON channel trace */
+ short	replay;
+
+ int	merger = 1, deadvar = 1, implied_semis = 1;
+@@ -267,6 +268,10 @@
+ #else
+ 	struct stat x;
+ #endif
++	if (json_trace_fp)
++	{	fclose(json_trace_fp);
++		json_trace_fp = NULL;
++	}
+ 	if (preprocessonly == 0 &&  strlen(out1) > 0)
+ 	{	(void) unlink((const char *) out1);
+ 	}
+@@ -657,6 +662,7 @@
+ 	printf("\t-p print all statements\n");
+ 	printf("\t-pp pretty-print (reformat) stdin, write stdout\n");
+ 	printf("\t-qN suppress io for queue N in printouts\n");
++	printf("\t-Q file  write per-channel JSON trace (SEND/RECV events) to file\n");
+ 	printf("\t-r print receive events\n");
+ 	printf("\t-replay  replay an error trail-file found earlier\n");
+ 	printf("\t	if the model contains embedded c-code, the ./pan executable is used\n");
+@@ -941,6 +947,18 @@
+ 				alldone(0);
+ 			  }
+ 			  verbose +=  4; break;
++		case 'Q': if (argc < 3)
++			  {	fprintf(stderr,
++				    "spin: -Q requires an output filename\n");
++					alldone(1);
++				  }
++				  json_trace_fp = fopen(argv[2], "w");
++				  if (!json_trace_fp)
++				  {	fprintf(stderr,
++					    "spin: cannot open '%s'\n", argv[2]);
++						alldone(1);
++					  }
++					  argc--; argv++; break;
+ 		case 'q': if (isdigit((int) argv[1][2]))
+ 				qhide(atoi(&argv[1][2]));
+ 			  break;
+--- a/Src/spin.h
++++ b/Src/spin.h
+@@ -102,6 +102,7 @@
+ 	int	*contents;	/* the values stored */
+ 	int	*stepnr;	/* depth when each msg was sent */
+ 	char	**mtp;		/* if mtype, name of list, else 0 */
++	char	*cname;		/* physical channel name, set in qmake */
+ 	struct Queue	*nxt;	/* linked list */
+ } Queue;
+
+--- a/Src/mesg.c
++++ b/Src/mesg.c
+@@ -20,6 +20,7 @@
+ extern int	verbose, TstOnly, s_trail, analyze, columns;
+ extern int	lineno, depth, xspin, m_loss, jumpsteps;
+ extern int	nproc, nstop;
++extern FILE	*json_trace_fp;	/* set by -Q flag; emit JSON channel trace */
+ extern short	Have_claim;
+
+ QH	*qh_lst;
+@@ -78,6 +79,7 @@
+ 	q->nslots = s->ini->val;
+ 	q->nflds  = cnt_mpars(s->ini->rgt);
+ 	q->setat  = depth;
++	q->cname  = s->name;
+
+ 	i = max(1, q->nslots);	/* 0-slot qs get 1 slot minimum */
+ 	j = q->nflds * i;
+@@ -337,6 +339,17 @@
+ 		/* may 30, 2023: the field types are 0..nflds, not i+0..nflds */
+ 		typ_ck(q->fld_width[j], Sym_typ(m->lft), "send");
+ 	}
++	if (json_trace_fp && q->nflds == 1)
++	{	fprintf(json_trace_fp,
++			"{\"channel_name\":\"%s\","
++			"\"direction\":\"SEND\",\"value\":%d,"
++			"\"proctype\":\"%s\",\"pid\":%d}\n",
++			q->cname ? q->cname : "",
++			q->contents[i],
++			(X_lst && X_lst->n) ? X_lst->n->name : "",
++			X_lst ? X_lst->pid : -1);
++		fflush(json_trace_fp);
++	}
+
+ 	if ((verbose&16) && depth >= jumpsteps)
+ 	{	for (i = j; i < q->nflds; i++)
+@@ -429,6 +442,17 @@
+ 	}
+
+ 	oi = q->stepnr[i];
++	if (json_trace_fp && full && n->val < 2 && q->nflds == 1 && !Rvous)
++	{	fprintf(json_trace_fp,
++			"{\"channel_name\":\"%s\","
++			"\"direction\":\"RECV\",\"value\":%d,"
++			"\"proctype\":\"%s\",\"pid\":%d}\n",
++			q->cname ? q->cname : "",
++			q->contents[i],
++			(X_lst && X_lst->n) ? X_lst->n->name : "",
++			X_lst ? X_lst->pid : -1);
++		fflush(json_trace_fp);
++	}
+ 	for (m = n->rgt, j = 0; m && j < q->nflds; m = m->rgt, j++)
+ 	{	if (columns && !full)	/* was columns == 1 */
+ 			continue;
+--- a/Src/pangen2.c
++++ b/Src/pangen2.c
+@@ -474,6 +474,8 @@
+ 	if (separate != 2)
+ 	{	fprintf(fd_tc, "char *TrailFile = PanSource; /* default */\n");
+ 		fprintf(fd_tc, "char *trailfilename;\n");
++		fprintf(fd_tc, "char *trail_output_dir = NULL;\n");
++		fprintf(fd_tc, "int   halt_on_error = 0;\n");
+ 	}
+
+ 	fprintf(fd_tc, "#ifdef LOOPSTATE\n");
+--- a/Src/pangen1.h
++++ b/Src/pangen1.h
+@@ -6030,9 +6030,11 @@
+ 	"	fprintf(fd, \"\t-hN use different hash-seed N:0..499 (defaults to -h0)\\n\");",
+ 	"	fprintf(fd, \"\t-hash generate a random hash-polynomial for -h0 (see also -rhash)\\n\");",
+ 	"	fprintf(fd, \"\t      using a seed set with -RSn (default %%u)\\n\", s_rand);",
++	"\tfprintf(fd, \"\t-H    exit pan with code 1 when errors found (default exits 0)\\n\");",
+ 	"	fprintf(fd, \"\t-i  search for shortest path to error\\n\");",
+ 	"	fprintf(fd, \"\t-I  like -i, but approximate and faster\\n\");",
+ 	"	fprintf(fd, \"\t-J  reverse eval order of nested unlesses\\n\");",
++	"\tfprintf(fd, \"\t-K<dir>  write .trail files into <dir> instead of current directory\\n\");",
+ 	"#ifdef BITSTATE",
+ 	"	fprintf(fd, \"\t-kN set N bits per state (defaults to 3)\\n\");",
+ 	"#endif",

xls/build_rules/xls_dslx_test.bzl

@@ -76,10 +76,15 @@ def get_dslx_test_cmd(ctx, src_files_to_test):
     dslx_interpreter_tool_runfiles = (
         ctx.attr._xls_dslx_interpreter_tool[DefaultInfo].default_runfiles
     )
+    extra_runfiles = [dslx_interpreter_tool_runfiles]
+    needs_spin = (ctx.attr.dslx_test_args.get("guided_model_check") == "True" or
+                  ctx.attr.dslx_test_args.get("exhaustive_model_check") == "True")
+    if needs_spin:
+        extra_runfiles.append(ctx.attr._spin[DefaultInfo].default_runfiles)
     runfiles = get_runfiles_for_xls(
         ctx,
-        [dslx_interpreter_tool_runfiles],
-        src_files_to_test,
+        extra_runfiles,
+        src_files_to_test + ([ctx.executable._spin] if needs_spin else []),
     )
 
     cmds = []
@@ -120,6 +125,9 @@ def _get_dslx_test_cmdline(ctx, src, all_srcs, append_cmd_line_args = True):
         "lower_to_proc_scoped_channels",
         "lower_to_ir",
         "convert_tests",
+        "guided_model_check",
+        "exhaustive_model_check",
+        "trace_channels",
     )
 
     dslx_test_args = dict(_dslx_test_args)
@@ -203,6 +211,13 @@ xls_dslx_test = rule(
         xls_dslx_library_as_input_attrs,
         xls_dslx_test_common_attrs,
         dicts.pick(xls_toolchain_attrs, ["_xls_dslx_interpreter_tool"]),
+        {
+            "_spin": attr.label(
+                default = Label("@spin//:spin"),
+                executable = True,
+                cfg = "target",
+            ),
+        },
     ),
     test = True,
 )