Add proc_constancy_checker_main.

xls/dev_tools/BUILD

@@ -17,7 +17,12 @@ load("@rules_cc//cc:cc_library.bzl", "cc_library")
 load("@rules_cc//cc:cc_test.bzl", "cc_test")
 load("@rules_shell//shell:sh_test.bzl", "sh_test")
 load("//xls/build_rules:py_oss_defs.bzl", "pytype_strict_binary", "pytype_strict_contrib_test", "pytype_strict_library")
-load("//xls/build_rules:xls_build_defs.bzl", "xls_ir_equivalence_test")
+load(
+    "//xls/build_rules:xls_build_defs.bzl",
+    "xls_dslx_ir",
+    "xls_dslx_library",
+    "xls_ir_equivalence_test",
+)
 
 package(
     default_applicable_licenses = ["//:license"],
@@ -999,3 +1004,102 @@ cc_library(
         "@abseil-cpp//absl/strings:str_format",
     ],
 )
+
+cc_library(
+    name = "proc_constancy_checker",
+    srcs = ["proc_constancy_checker.cc"],
+    hdrs = ["proc_constancy_checker.h"],
+    deps = [
+        "//xls/common/status:status_macros",
+        "//xls/ir",
+        "//xls/ir:bits",
+        "//xls/ir:op",
+        "//xls/ir:proc_testutils",
+        "//xls/ir:type",
+        "//xls/ir:value",
+        "//xls/passes:non_synth_removal_pass",
+        "//xls/passes:optimization_pass",
+        "//xls/passes:pass_base",
+        "//xls/solvers:z3_ir_translator",
+        "@abseil-cpp//absl/algorithm:container",
+        "@abseil-cpp//absl/container:flat_hash_map",
+        "@abseil-cpp//absl/container:flat_hash_set",
+        "@abseil-cpp//absl/status",
+        "@abseil-cpp//absl/status:statusor",
+        "@z3//:api",
+    ],
+)
+
+cc_test(
+    name = "proc_constancy_checker_test",
+    srcs = ["proc_constancy_checker_test.cc"],
+    deps = [
+        ":proc_constancy_checker",
+        "//xls/common:xls_gunit_main",
+        "//xls/common/status:matchers",
+        "//xls/common/status:status_macros",
+        "//xls/ir",
+        "//xls/ir:bits",
+        "//xls/ir:channel",
+        "//xls/ir:channel_ops",
+        "//xls/ir:function_builder",
+        "//xls/ir:ir_test_base",
+        "//xls/ir:source_location",
+        "//xls/ir:value",
+        "@abseil-cpp//absl/status:statusor",
+        "@googletest//:gtest",
+    ],
+)
+
+cc_binary(
+    name = "proc_constancy_checker_main",
+    srcs = ["proc_constancy_checker_main.cc"],
+    deps = [
+        ":proc_constancy_checker",
+        "//xls/common:exit_status",
+        "//xls/common:init_xls",
+        "//xls/common/file:filesystem",
+        "//xls/common/status:status_macros",
+        "//xls/ir",
+        "//xls/ir:channel",
+        "//xls/ir:function_builder",
+        "//xls/ir:ir_parser",
+        "//xls/ir:op",
+        "//xls/ir:type",
+        "//xls/solvers:z3_ir_translator",
+        "@abseil-cpp//absl/container:flat_hash_map",
+        "@abseil-cpp//absl/container:flat_hash_set",
+        "@abseil-cpp//absl/flags:flag",
+        "@abseil-cpp//absl/log:check",
+        "@abseil-cpp//absl/status",
+        "@abseil-cpp//absl/status:statusor",
+        "@abseil-cpp//absl/strings",
+        "@abseil-cpp//absl/strings:str_format",
+        "@z3//:api",
+    ],
+)
+
+xls_dslx_library(
+    name = "constancy_test_dslx",
+    srcs = ["testdata/constancy_test.x"],
+)
+
+xls_dslx_ir(
+    name = "constancy_test",
+    dslx_top = "test_proc",
+    ir_file = "testdata/constancy_test.ir",
+    library = ":constancy_test_dslx",
+)
+
+pytype_strict_contrib_test(
+    name = "proc_constancy_checker_main_test",
+    srcs = ["proc_constancy_checker_main_test.py"],
+    data = [
+        ":proc_constancy_checker_main",
+        ":testdata/constancy_test.ir",
+    ],
+    deps = [
+        "//xls/common:runfiles",
+        "@abseil-py//absl/testing:absltest",
+    ],
+)

xls/dev_tools/proc_constancy_checker.cc

@@ -0,0 +1,163 @@
+// 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.
+
+#include "xls/dev_tools/proc_constancy_checker.h"
+
+#include <cstdint>
+#include <utility>
+#include <vector>
+
+#include "absl/algorithm/container.h"
+#include "absl/container/flat_hash_map.h"
+#include "absl/container/flat_hash_set.h"
+#include "absl/status/status.h"
+#include "absl/status/statusor.h"
+#include "xls/common/status/status_macros.h"
+#include "xls/ir/bits.h"
+#include "xls/ir/function.h"
+#include "xls/ir/node.h"
+#include "xls/ir/nodes.h"
+#include "xls/ir/op.h"
+#include "xls/ir/package.h"
+#include "xls/ir/proc.h"
+#include "xls/ir/proc_testutils.h"
+#include "xls/ir/topo_sort.h"
+#include "xls/ir/type.h"
+#include "xls/ir/value.h"
+#include "xls/passes/non_synth_removal_pass.h"
+#include "xls/passes/optimization_pass.h"
+#include "xls/passes/pass_base.h"
+#include "xls/solvers/z3_ir_translator.h"
+#include "z3/src/api/z3_api.h"
+
+namespace xls {
+namespace {
+
+// Returns true if `n` is trivially constant by construction (i.e. a Literal or
+// a tree of operations whose inputs are exclusively Literals, with no path from
+// dynamic inputs like Receive or StateRead).
+//
+// Aggregate types that are literal are often constructed from their literal
+// elements rather than making a single aggregate-typed literal. We want to
+// avoid spurious "non-constant" detections in these cases.
+//
+// Note that `non_constant_nodes` must contain every one of `n`'s operands for
+// which `IsConstantByConstruction(op)` is true in order to evaluate
+// `IsConstantByConstruction(n)` correctly. This can be achieved by calling
+// `IsConstantByConstruction` on the nodes in topological order, inserting
+// constant nodes into the set as we go.
+bool IsConstantByConstruction(
+    Node* n, const absl::flat_hash_set<Node*>& constant_nodes) {
+  if (n->Is<Literal>()) {
+    return true;
+  }
+  if (n->OpIn({Op::kReceive, Op::kStateRead, Op::kParam, Op::kSend, Op::kNext,
+               Op::kAssert, Op::kTrace, Op::kCover})) {
+    return false;
+  }
+  return absl::c_all_of(n->operands(), [&](Node* operand) {
+    return constant_nodes.contains(operand);
+  });
+}
+
+}  // namespace
+
+absl::Status StripNonSynthNodes(Package* package, Proc* proc) {
+  OptimizationContext context;
+  PassResults pass_results;
+  NonSynthRemovalPass pass;
+  XLS_RETURN_IF_ERROR(pass.Run(package, {}, &pass_results, context).status());
+
+  return absl::OkStatus();
+}
+
+absl::StatusOr<std::vector<Node*>> GetNodesFilteringNonSynthAndTrivialConstants(
+    Proc* proc) {
+  XLS_ASSIGN_OR_RETURN(std::vector<Node*> sorted_nodes, TopoSort(proc));
+  absl::flat_hash_set<Node*> constant_nodes;
+  std::vector<Node*> target_nodes;
+  for (Node* n : sorted_nodes) {
+    if (IsConstantByConstruction(n, constant_nodes)) {
+      constant_nodes.insert(n);
+      continue;
+    }
+    if (n->GetType()->IsToken() || n->GetType()->GetFlatBitCount() == 0) {
+      continue;
+    }
+    if (n->OpIn({Op::kParam, Op::kStateRead, Op::kReceive, Op::kSend, Op::kNext,
+                 Op::kAssert, Op::kTrace, Op::kCover})) {
+      continue;
+    }
+    target_nodes.push_back(n);
+  }
+  return target_nodes;
+}
+
+absl::StatusOr<std::pair<Function*, NodeActivationMap>> UnrollProcForConstancy(
+    Proc* proc, int64_t activation_count) {
+  XLS_ASSIGN_OR_RETURN(
+      UnrolledProc unrolled,
+      UnrollProc(proc, activation_count, /*include_state=*/true,
+                 Value::Tuple({Value(UBits(0xdeadbeef, 32))}),
+                 /*cleanup=*/false));
+
+  NodeActivationMap node_activations;
+  for (const ActivationAction& act : unrolled.activations) {
+    for (const auto& [orig_node, val] : act.node_values) {
+      if (val.node() != nullptr) {
+        node_activations[orig_node].push_back(val.node());
+      }
+    }
+  }
+  return std::make_pair(unrolled.function, node_activations);
+}
+
+std::vector<Z3_ast> FlattenBitsOnly(Z3_context ctx,
+                                    solvers::z3::IrTranslator* translator,
+                                    Type* type, Z3_ast value) {
+  if (type->IsBits()) {
+    return translator->FlattenValue(type, value);
+  }
+  if (type->IsTuple()) {
+    TupleType* tuple_type = type->AsTupleOrDie();
+    Z3_sort tuple_sort = Z3_get_sort(ctx, value);
+    std::vector<Z3_ast> all_bits;
+    for (int64_t i = 0; i < tuple_type->size(); ++i) {
+      Type* elem_type = tuple_type->element_type(i);
+      Z3_func_decl proj_fn = Z3_get_tuple_sort_field_decl(ctx, tuple_sort, i);
+      Z3_ast elem_ast = Z3_mk_app(ctx, proj_fn, 1, &value);
+      std::vector<Z3_ast> elem_bits =
+          FlattenBitsOnly(ctx, translator, elem_type, elem_ast);
+      all_bits.insert(all_bits.end(), elem_bits.begin(), elem_bits.end());
+    }
+    return all_bits;
+  }
+  if (type->IsArray()) {
+    ArrayType* array_type = type->AsArrayOrDie();
+    Z3_sort array_sort = Z3_get_sort(ctx, value);
+    Z3_sort domain_sort = Z3_get_array_sort_domain(ctx, array_sort);
+    std::vector<Z3_ast> all_bits;
+    for (int64_t i = 0; i < array_type->size(); ++i) {
+      Z3_ast idx_ast = Z3_mk_unsigned_int64(ctx, i, domain_sort);
+      Z3_ast elem_ast = Z3_mk_select(ctx, value, idx_ast);
+      std::vector<Z3_ast> elem_bits = FlattenBitsOnly(
+          ctx, translator, array_type->element_type(), elem_ast);
+      all_bits.insert(all_bits.end(), elem_bits.begin(), elem_bits.end());
+    }
+    return all_bits;
+  }
+  return {};
+}
+
+}  // namespace xls

xls/dev_tools/proc_constancy_checker.h

@@ -0,0 +1,72 @@
+// 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.
+
+#ifndef XLS_DEV_TOOLS_PROC_CONSTANCY_CHECKER_H_
+#define XLS_DEV_TOOLS_PROC_CONSTANCY_CHECKER_H_
+
+#include <cstdint>
+#include <utility>
+#include <vector>
+
+#include "absl/container/flat_hash_map.h"
+#include "absl/status/status.h"
+#include "absl/status/statusor.h"
+#include "xls/ir/function.h"
+#include "xls/ir/node.h"
+#include "xls/ir/package.h"
+#include "xls/ir/proc.h"
+#include "xls/ir/type.h"
+#include "xls/solvers/z3_ir_translator.h"
+#include "z3/src/api/z3_api.h"
+
+namespace xls {
+
+// Map from original proc node to its cloned Node* instances across activations.
+using NodeActivationMap = absl::flat_hash_map<Node*, std::vector<Node*>>;
+
+// Strips non-synthesizable nodes (assert, trace, cover) and any intermediate
+// nodes only consumed by them from the given proc/package using
+// NonSynthRemovalPass.
+absl::Status StripNonSynthNodes(Package* package, Proc* proc);
+
+// Returns the list of non-constant, synthesizable candidate nodes in the proc
+// to check for constancy.
+//
+// This name is a mouthful, but the idea is that when we test nodes for
+// constancy, we don't want to waste time or spuriously report nodes we don't
+// care about. Thus, this function enumerates nodes in the proc and filters out:
+// 1. Non-synthesizable nodes (assert, trace, cover): it's OK and even expected
+//    for these to be constant.
+// 2. Trivial constant nodes (literals, or ops only consuming trivial constants-
+//    typically aggregates of literals): these are the nodes that are supposed
+//    to be constant.
+// 3. Token nodes: tokens carry no value and are purely for sequencing.
+absl::StatusOr<std::vector<Node*>> GetNodesFilteringNonSynthAndTrivialConstants(
+    Proc* proc);
+
+// Unrolls the proc `activation_count` times into a function using
+// `proc_testutils::UnrollProc` and returns the unrolled function along with
+// the mapping from original nodes to unrolled clones across activations.
+absl::StatusOr<std::pair<Function*, NodeActivationMap>> UnrollProcForConstancy(
+    Proc* proc, int64_t activation_count);
+
+// Flattens a Z3 AST representing a Bits or Tuple/Array type into individual bit
+// ASTs.
+std::vector<Z3_ast> FlattenBitsOnly(Z3_context ctx,
+                                    solvers::z3::IrTranslator* translator,
+                                    Type* type, Z3_ast value);
+
+}  // namespace xls
+
+#endif  // XLS_DEV_TOOLS_PROC_CONSTANCY_CHECKER_H_