diff --git a/xls/dev_tools/BUILD b/xls/dev_tools/BUILD index b9672859d2..34c6b5c744 100644 --- a/xls/dev_tools/BUILD +++ b/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", + ], +) diff --git a/xls/dev_tools/proc_constancy_checker.cc b/xls/dev_tools/proc_constancy_checker.cc new file mode 100644 index 0000000000..6448b00dc1 --- /dev/null +++ b/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 +#include +#include + +#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& constant_nodes) { + if (n->Is()) { + 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> GetNodesFilteringNonSynthAndTrivialConstants( + Proc* proc) { + XLS_ASSIGN_OR_RETURN(std::vector sorted_nodes, TopoSort(proc)); + absl::flat_hash_set constant_nodes; + std::vector 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> 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 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 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 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 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 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 diff --git a/xls/dev_tools/proc_constancy_checker.h b/xls/dev_tools/proc_constancy_checker.h new file mode 100644 index 0000000000..23963a0483 --- /dev/null +++ b/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 +#include +#include + +#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>; + +// 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> 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> UnrollProcForConstancy( + Proc* proc, int64_t activation_count); + +// Flattens a Z3 AST representing a Bits or Tuple/Array type into individual bit +// ASTs. +std::vector FlattenBitsOnly(Z3_context ctx, + solvers::z3::IrTranslator* translator, + Type* type, Z3_ast value); + +} // namespace xls + +#endif // XLS_DEV_TOOLS_PROC_CONSTANCY_CHECKER_H_ diff --git a/xls/dev_tools/proc_constancy_checker_main.cc b/xls/dev_tools/proc_constancy_checker_main.cc new file mode 100644 index 0000000000..294e3bf525 --- /dev/null +++ b/xls/dev_tools/proc_constancy_checker_main.cc @@ -0,0 +1,453 @@ +// 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 + +#include +#include +#include +#include +#include +#include +#include +#include + +#include "absl/container/flat_hash_map.h" +#include "absl/container/flat_hash_set.h" +#include "absl/flags/flag.h" +#include "absl/log/check.h" +#include "absl/status/status.h" +#include "absl/status/statusor.h" +#include "absl/strings/match.h" +#include "absl/strings/str_format.h" +#include "absl/strings/str_split.h" +#include "xls/common/exit_status.h" +#include "xls/common/file/filesystem.h" +#include "xls/common/init_xls.h" +#include "xls/common/status/status_macros.h" +#include "xls/dev_tools/proc_constancy_checker.h" +#include "xls/ir/channel.h" +#include "xls/ir/function_builder.h" +#include "xls/ir/ir_parser.h" +#include "xls/ir/op.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" + +enum class CheckMode { kNode, kBit }; + +bool AbslParseFlag(std::string_view text, CheckMode* mode, std::string* error) { + if (text == "node") { + *mode = CheckMode::kNode; + return true; + } + if (text == "bit") { + *mode = CheckMode::kBit; + return true; + } + *error = "unknown check mode, specify 'node' or 'bit'"; + return false; +} + +std::string AbslUnparseFlag(CheckMode mode) { + return mode == CheckMode::kNode ? "node" : "bit"; +} + +ABSL_FLAG(std::string, ir_path, "", "Path to the XLS IR file."); +ABSL_FLAG(std::string, top_proc, "", + "Name of the top proc. Uses top proc if empty."); +ABSL_FLAG(int64_t, unroll_count, 4, + "Number of activations to unroll the proc."); +ABSL_FLAG(CheckMode, mode, CheckMode::kNode, + "Constancy check mode: 'node' or 'bit'."); +ABSL_FLAG(int64_t, z3_rlimit, 0, + "Z3 resource limit per check (0 for no limit)."); +ABSL_FLAG(int64_t, z3_timeout_ms, 0, + "Z3 timeout in milliseconds per check (0 for no timeout)."); +ABSL_FLAG( + std::string, node_filter, "", + "Comma-separated substrings to filter target node names to check (e.g. " + "'nor.195914,nor.195923'). If empty, checks all target nodes."); +ABSL_FLAG( + bool, fail_on_constants, false, + "If true, returns a non-zero exit code when any constant nodes or bits " + "are detected."); + +namespace xls { +namespace { + +// Map from original proc node to its cloned Node* instances across activations. +using NodeActivationMap = absl::flat_hash_map>; + +std::vector FilterCandidatesByName( + const std::vector& candidates, + const std::vector& filter_tokens) { + if (filter_tokens.empty()) { + return candidates; + } + std::vector filtered; + for (Node* n : candidates) { + bool match = false; + for (std::string_view tok : filter_tokens) { + if (absl::StrContains(n->GetName(), tok)) { + match = true; + break; + } + } + if (match) { + filtered.push_back(n); + } + } + return filtered; +} + +absl::StatusOr> FilterTargetsForChecking( + const std::vector& candidates, + const NodeActivationMap& node_activations, int64_t unroll_count) { + std::vector target_nodes; + for (Node* n : candidates) { + auto it = node_activations.find(n); + if (it == node_activations.end()) { + continue; + } + if (it->second.size() != unroll_count) { + continue; + } + target_nodes.push_back(n); + } + return target_nodes; +} + +bool IsInteractiveTty(const std::ostream& os) { + if (os.rdbuf() == std::cout.rdbuf()) { + return isatty(fileno(stdout)); + } + if (os.rdbuf() == std::cerr.rdbuf()) { + return isatty(fileno(stderr)); + } + return false; +} + +// TODO: google/xls#4734 - move to gloop +class ProgressTracker { + public: + ProgressTracker(std::ostream& os, int64_t total_targets) + : os_(os), + total_targets_(total_targets), + interactive_(IsInteractiveTty(os)) {} + + void RenderProgress(int64_t current) { + if (!interactive_) { + return; + } + float progress = total_targets_ > 0 + ? static_cast(current) / total_targets_ + : 1.0f; + int64_t percent = static_cast(progress * 100); + int64_t bar_width = 30; + int64_t pos = static_cast(bar_width * progress); + + os_ << "\r[" << std::setw(3) << percent << "%] ["; + for (int64_t i = 0; i < bar_width; ++i) { + if (i < 10) { + os_ << "\033[1;32m"; // Green + } else if (i < 20) { + os_ << "\033[1;97m"; // White + } else { + os_ << "\033[1;31m"; // Red + } + + if (i < pos) { + os_ << "="; + } else if (i == pos) { + os_ << ">"; + } else { + os_ << " "; + } + } + os_ << "\033[0m] " << current << "/" << total_targets_ + << " nodes (Constant: " << constant_checks_; + if (timeout_checks_ > 0) { + os_ << ", Timeout: " << timeout_checks_; + } + os_ << ")" << std::flush; + } + + void RecordNonConstantCheck() { non_constant_checks_++; } + void RecordConstantNode(Node* n) { + constant_checks_++; + if (interactive_) { + os_ << "\r\033[K"; + } + os_ << "UNSAT *** ALERT: CONSTANT NODE DETECTED ***: '" << n->GetName() + << "' (" << OpToString(n->op()) << ", " << n->GetType()->ToString() + << ")\n"; + } + void RecordConstantBit(Node* n, int64_t b) { + constant_checks_++; + if (interactive_) { + os_ << "\r\033[K"; + } + os_ << "UNSAT *** ALERT: CONSTANT BIT DETECTED ***: '" << n->GetName() + << "' bit [" << b << "]\n"; + } + void RecordTimeoutNode(Node* n, std::string_view reason) { + timeout_checks_++; + if (interactive_) { + os_ << "\r\033[K"; + } + os_ << "UNKNOWN (" << (!reason.empty() ? reason : "unknown") << "): '" + << n->GetName() << "' (" << OpToString(n->op()) << ")\n"; + } + void RecordTimeoutBit(Node* n, int64_t b, std::string_view reason) { + timeout_checks_++; + if (interactive_) { + os_ << "\r\033[K"; + } + os_ << "UNKNOWN (" << (!reason.empty() ? reason : "unknown") << "): '" + << n->GetName() << "' bit [" << b << "]\n"; + } + + int64_t non_constant_checks() const { return non_constant_checks_; } + int64_t constant_checks() const { return constant_checks_; } + int64_t timeout_checks() const { return timeout_checks_; } + + private: + std::ostream& os_; + int64_t total_targets_; + bool interactive_; + int64_t non_constant_checks_ = 0; + int64_t constant_checks_ = 0; + int64_t timeout_checks_ = 0; +}; + +absl::Status RealMain(std::ostream& os, std::string_view ir_path, + std::string_view top_proc_name, int64_t unroll_count, + CheckMode mode, int64_t rlimit, int64_t timeout_ms, + std::string_view node_filter_str, + bool fail_on_constants) { + XLS_ASSIGN_OR_RETURN(std::string ir_text, GetFileContents(ir_path)); + XLS_ASSIGN_OR_RETURN(std::unique_ptr package, + Parser::ParsePackage(ir_text)); + + Proc* proc = nullptr; + if (top_proc_name.empty()) { + XLS_ASSIGN_OR_RETURN(proc, package->GetTopAsProc()); + } else { + XLS_ASSIGN_OR_RETURN(proc, package->GetProc(top_proc_name)); + } + + os << "Loaded Proc '" << proc->name() << "' with " << proc->node_count() + << " nodes.\n"; + + // Strip non-synthesizable nodes before unrolling or checking. + XLS_RETURN_IF_ERROR(StripNonSynthNodes(package.get(), proc)); + + // Get candidate target nodes early so we can skip unrolling if none exist. + XLS_ASSIGN_OR_RETURN(std::vector candidates, + GetNodesFilteringNonSynthAndTrivialConstants(proc)); + + std::vector filter_tokens; + if (!node_filter_str.empty()) { + filter_tokens = absl::StrSplit(node_filter_str, ',', absl::SkipEmpty()); + } + candidates = FilterCandidatesByName(candidates, filter_tokens); + + if (candidates.empty()) { + os << "Constant Checks: 0\n"; + return absl::OkStatus(); + } + + // Unroll the proc. + os << "Unrolling proc " << unroll_count << " times...\n"; + XLS_ASSIGN_OR_RETURN((auto [unrolled_func, node_activations]), + UnrollProcForConstancy(proc, unroll_count)); + + // Translate Unrolled Function to Z3 + os << "Translating unrolled function to Z3 SMT AST...\n"; + XLS_ASSIGN_OR_RETURN(std::unique_ptr translator, + solvers::z3::IrTranslator::CreateAndTranslate( + unrolled_func, /*allow_unsupported=*/true)); + + Z3_context ctx = translator->ctx(); + Z3_solver solver = Z3_mk_solver(ctx); + Z3_solver_inc_ref(ctx, solver); + Z3_params params = Z3_mk_params(ctx); + Z3_params_inc_ref(ctx, params); + + if (rlimit > 0) { + translator->SetRlimit(rlimit); + Z3_params_set_uint(ctx, params, Z3_mk_string_symbol(ctx, "rlimit"), + static_cast(rlimit)); + } + if (timeout_ms > 0) { + Z3_params_set_uint(ctx, params, Z3_mk_string_symbol(ctx, "timeout"), + static_cast(timeout_ms)); + } + // Z3 swallows ctrl+c, interpreting it as a sign to cancel the current solve + // rather than the whole binary. + Z3_params_set_bool(ctx, params, Z3_mk_string_symbol(ctx, "ctrl_c"), false); + + Z3_solver_set_params(ctx, solver, params); + + XLS_ASSIGN_OR_RETURN( + std::vector target_nodes, + FilterTargetsForChecking(candidates, node_activations, unroll_count)); + + os << "Verifying " << target_nodes.size() + << " non-literal, synthesizable nodes in mode '" << AbslUnparseFlag(mode) + << "'...\n\n"; + + ProgressTracker progress_tracker(os, target_nodes.size()); + progress_tracker.RenderProgress(0); + + for (int64_t idx = 0; idx < target_nodes.size(); ++idx) { + Node* n = target_nodes[idx]; + const std::vector& act_nodes = node_activations[n]; + + if (mode == CheckMode::kNode) { + std::vector disequalities; + disequalities.reserve(act_nodes.size() - 1); + Z3_ast ast_0 = translator->GetTranslation(act_nodes[0]); + for (int64_t i = 1; i < act_nodes.size(); ++i) { + Z3_ast ast_i = translator->GetTranslation(act_nodes[i]); + Z3_ast eq = Z3_mk_eq(ctx, ast_0, ast_i); + disequalities.push_back(Z3_mk_not(ctx, eq)); + } + + Z3_ast can_change = + Z3_mk_or(ctx, disequalities.size(), disequalities.data()); + + Z3_lbool check_res = Z3_solver_check_assumptions( + ctx, solver, /*num_assumptions=*/1, /*assumptions=*/&can_change); + + if (check_res == Z3_L_TRUE) { + progress_tracker.RecordNonConstantCheck(); + } else if (check_res == Z3_L_FALSE) { + progress_tracker.RecordConstantNode(n); + // Performance optimization: permanently assert proven constants into + // the shared solver at decision level 0. Because target nodes are + // checked in topological order, Z3's congruence-closure and bit-vector + // engines instantly merge constant operand ASTs across activations into + // the same equivalence class, allowing downstream checks to simplify + // without re-exploring the proof trees of their operands. + Z3_solver_assert(ctx, solver, Z3_mk_not(ctx, can_change)); + } else { + const char* reason = Z3_solver_get_reason_unknown(ctx, solver); + progress_tracker.RecordTimeoutNode( + n, reason != nullptr ? reason : "unknown"); + } + } else { + // Bit mode: check each bit index b independently + int64_t width = n->GetType()->GetFlatBitCount(); + + // Collect flat bit ASTs for each activation + std::vector> act_flat_bits; + act_flat_bits.reserve(act_nodes.size()); + for (Node* act_node : act_nodes) { + Z3_ast ast = translator->GetTranslation(act_node); + act_flat_bits.push_back( + FlattenBitsOnly(ctx, translator.get(), n->GetType(), ast)); + } + + for (int64_t b = 0; b < width; ++b) { + bool skip = false; + for (int64_t i = 0; i < act_flat_bits.size(); ++i) { + if (b >= act_flat_bits[i].size()) { + skip = true; + break; + } + } + if (skip) { + continue; + } + + std::vector disequalities; + disequalities.reserve(act_flat_bits.size() - 1); + for (int64_t i = 1; i < act_flat_bits.size(); ++i) { + Z3_ast eq = Z3_mk_eq(ctx, act_flat_bits[0][b], act_flat_bits[i][b]); + disequalities.push_back(Z3_mk_not(ctx, eq)); + } + + Z3_ast can_change = + Z3_mk_or(ctx, disequalities.size(), disequalities.data()); + + Z3_lbool check_res = Z3_solver_check_assumptions( + ctx, solver, /*num_assumptions=*/1, /*assumptions=*/&can_change); + + if (check_res == Z3_L_TRUE) { + progress_tracker.RecordNonConstantCheck(); + } else if (check_res == Z3_L_FALSE) { + progress_tracker.RecordConstantBit(n, b); + // Performance optimization: permanently assert proven constant bits + // into the shared solver at decision level 0. Downstream bit-vector + // operations can immediately exploit these constant bit assignments + // without re-exploring the proof trees of their operands. + Z3_solver_assert(ctx, solver, Z3_mk_not(ctx, can_change)); + } else { + const char* reason = Z3_solver_get_reason_unknown(ctx, solver); + progress_tracker.RecordTimeoutBit( + n, b, reason != nullptr ? reason : "unknown"); + } + } + } + progress_tracker.RenderProgress(idx + 1); + } + + os << "\r\033[K"; // Clear progress bar before printing summary + + os << "\n=== Verification Summary ===\n" + << "Check Mode: " << AbslUnparseFlag(mode) << "\n" + << "Non-Constant Checks: " << progress_tracker.non_constant_checks() + << "\n" + << "Constant Checks: " << progress_tracker.constant_checks() + << " (Potential Static Flops)\n" + << "Timeout Checks: " << progress_tracker.timeout_checks() << "\n"; + + Z3_params_dec_ref(ctx, params); + Z3_solver_dec_ref(ctx, solver); + + if (fail_on_constants && progress_tracker.constant_checks() > 0) { + return absl::FailedPreconditionError(absl::StrFormat( + "Found %d constant nodes/bits.", progress_tracker.constant_checks())); + } + + return absl::OkStatus(); +} + +} // namespace +} // namespace xls + +int main(int argc, char** argv) { + xls::InitXls(argv[0], argc, argv); + std::string ir_path = absl::GetFlag(FLAGS_ir_path); + QCHECK(!ir_path.empty()) << "--ir_path must be specified."; + + int64_t unroll_count = absl::GetFlag(FLAGS_unroll_count); + QCHECK_GT(unroll_count, 1) + << "--unroll_count must be > 1 as there must be at least two activations " + "to check for constancy."; + + std::string top_proc_name = absl::GetFlag(FLAGS_top_proc); + CheckMode mode = absl::GetFlag(FLAGS_mode); + int64_t rlimit = absl::GetFlag(FLAGS_z3_rlimit); + int64_t timeout_ms = absl::GetFlag(FLAGS_z3_timeout_ms); + std::string node_filter_str = absl::GetFlag(FLAGS_node_filter); + bool fail_on_constants = absl::GetFlag(FLAGS_fail_on_constants); + return xls::ExitStatus(xls::RealMain(std::cout, ir_path, top_proc_name, + unroll_count, mode, rlimit, timeout_ms, + node_filter_str, fail_on_constants)); +} diff --git a/xls/dev_tools/proc_constancy_checker_main_test.py b/xls/dev_tools/proc_constancy_checker_main_test.py new file mode 100644 index 0000000000..02bbc7f48a --- /dev/null +++ b/xls/dev_tools/proc_constancy_checker_main_test.py @@ -0,0 +1,129 @@ +# 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. + +import subprocess + +from absl.testing import absltest +from xls.common import runfiles + +PROC_CONSTANCY_CHECKER_MAIN_PATH = runfiles.get_path( + 'xls/dev_tools/proc_constancy_checker_main' +) + +TEST_IR_PATH = runfiles.get_path('xls/dev_tools/testdata/constancy_test.ir') + + +class ProcConstancyCheckerMainTest(absltest.TestCase): + + def test_constancy_detection_node_mode(self): + cmd = [ + PROC_CONSTANCY_CHECKER_MAIN_PATH, + f'--ir_path={TEST_IR_PATH}', + '--unroll_count=3', + '--mode=node', + ] + p = subprocess.run( + cmd, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + encoding='utf-8', + check=False, + ) + self.assertEqual(p.returncode, 0, msg=p.stderr) + self.assertIn('CONSTANT NODE DETECTED', p.stdout) + self.assertIn("'const_zero'", p.stdout) + self.assertNotIn("CONSTANT NODE DETECTED: 'trailing_zero'", p.stdout) + + def test_constancy_detection_bit_mode(self): + cmd = [ + PROC_CONSTANCY_CHECKER_MAIN_PATH, + f'--ir_path={TEST_IR_PATH}', + '--unroll_count=3', + '--mode=bit', + '--node_filter=trailing_zero', + ] + p = subprocess.run( + cmd, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + encoding='utf-8', + check=False, + ) + self.assertEqual(p.returncode, 0, msg=p.stderr) + self.assertIn('CONSTANT BIT DETECTED', p.stdout) + self.assertIn("'trailing_zero' bit [0]", p.stdout) + self.assertIn("'trailing_zero' bit [1]", p.stdout) + + def test_fail_on_constants_flag(self): + cmd = [ + PROC_CONSTANCY_CHECKER_MAIN_PATH, + f'--ir_path={TEST_IR_PATH}', + '--unroll_count=3', + '--mode=node', + '--fail_on_constants', + ] + p = subprocess.run( + cmd, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + encoding='utf-8', + check=False, + ) + self.assertNotEqual(p.returncode, 0) + self.assertIn('CONSTANT NODE DETECTED', p.stdout) + self.assertIn("'const_zero'", p.stdout) + + def test_fail_on_constants_flag_bit_mode(self): + cmd = [ + PROC_CONSTANCY_CHECKER_MAIN_PATH, + f'--ir_path={TEST_IR_PATH}', + '--unroll_count=3', + '--mode=bit', + '--node_filter=trailing_zero', + '--fail_on_constants', + ] + p = subprocess.run( + cmd, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + encoding='utf-8', + check=False, + ) + self.assertNotEqual(p.returncode, 0) + self.assertIn('CONSTANT BIT DETECTED', p.stdout) + self.assertIn("'trailing_zero' bit [0]", p.stdout) + self.assertIn("'trailing_zero' bit [1]", p.stdout) + + def test_node_filter(self): + cmd = [ + PROC_CONSTANCY_CHECKER_MAIN_PATH, + f'--ir_path={TEST_IR_PATH}', + '--unroll_count=3', + '--mode=node', + '--node_filter=add1', + ] + p = subprocess.run( + cmd, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + encoding='utf-8', + check=False, + ) + self.assertEqual(p.returncode, 0, msg=p.stderr) + self.assertIn('Constant Checks: 0', p.stdout) + self.assertNotIn("'const_zero'", p.stdout) + + +if __name__ == '__main__': + absltest.main() diff --git a/xls/dev_tools/proc_constancy_checker_test.cc b/xls/dev_tools/proc_constancy_checker_test.cc new file mode 100644 index 0000000000..b09b4f0605 --- /dev/null +++ b/xls/dev_tools/proc_constancy_checker_test.cc @@ -0,0 +1,87 @@ +// 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 +#include +#include +#include + +#include "gmock/gmock.h" +#include "gtest/gtest.h" +#include "absl/status/statusor.h" +#include "xls/common/status/matchers.h" +#include "xls/common/status/status_macros.h" +#include "xls/ir/bits.h" +#include "xls/ir/channel.h" +#include "xls/ir/channel_ops.h" +#include "xls/ir/function_builder.h" +#include "xls/ir/ir_test_base.h" +#include "xls/ir/node.h" +#include "xls/ir/package.h" +#include "xls/ir/proc.h" +#include "xls/ir/source_location.h" +#include "xls/ir/value.h" + +namespace xls { +namespace { + +using ::testing::UnorderedElementsAre; + +class ProcConstancyCheckerTest : public IrTestBase { + protected: + absl::StatusOr BuildTestProc(Package* p) { + ProcBuilder pb(TestName(), p); + XLS_ASSIGN_OR_RETURN( + auto out_ch, p->CreateStreamingChannel("out_ch", ChannelOps::kSendOnly, + p->GetBitsType(32))); + auto tok = pb.ReadStateElement("tok", Value::Token()); + auto state = pb.ReadStateElement("st", Value(UBits(0, 32))); + auto lit1 = pb.Literal(UBits(1, 32)); + auto add1 = pb.Add(state, lit1, SourceInfo(), "add1"); + auto cond = pb.Literal(UBits(1, 1)); + pb.Assert(tok, cond, "test assert"); + auto snd_tok = pb.Send(out_ch, tok, add1); + pb.Next(state, add1); + pb.Next(tok, snd_tok); + XLS_ASSIGN_OR_RETURN(Proc * proc, pb.Build()); + XLS_RETURN_IF_ERROR(p->SetTop(proc)); + return proc; + } +}; + +TEST_F(ProcConstancyCheckerTest, GetNonConstantNodes) { + auto p = CreatePackage(); + XLS_ASSERT_OK_AND_ASSIGN(Proc * proc, BuildTestProc(p.get())); + XLS_ASSERT_OK(StripNonSynthNodes(p.get(), proc)); + XLS_ASSERT_OK_AND_ASSIGN(std::vector targets, + GetNodesFilteringNonSynthAndTrivialConstants(proc)); + std::vector names; + for (Node* n : targets) { + names.push_back(n->GetName()); + } + EXPECT_THAT(names, UnorderedElementsAre("add1")); +} + +TEST_F(ProcConstancyCheckerTest, UnrollProcForConstancyTest) { + auto p = CreatePackage(); + XLS_ASSERT_OK_AND_ASSIGN(Proc * proc, BuildTestProc(p.get())); + XLS_ASSERT_OK_AND_ASSIGN((auto [func, map]), UnrollProcForConstancy(proc, 3)); + EXPECT_NE(func, nullptr); + EXPECT_FALSE(map.empty()); +} + +} // namespace +} // namespace xls diff --git a/xls/dev_tools/testdata/constancy_test.x b/xls/dev_tools/testdata/constancy_test.x new file mode 100644 index 0000000000..d5aea383dd --- /dev/null +++ b/xls/dev_tools/testdata/constancy_test.x @@ -0,0 +1,30 @@ +// 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. + +proc test_proc { + out_ch: chan out; + + config(out_ch: chan out) { (out_ch,) } + + init { u32:0 } + + next(st: u32) { + let const_zero = st & u32:0; + let trailing_zero = st << u32:2; + let add1 = st + u32:1 + const_zero + (trailing_zero & u32:0); + assert!(st == st, "test assert"); + let tok = send(join(), out_ch, add1); + add1 + } +} diff --git a/xls/ir/proc_testutils.cc b/xls/ir/proc_testutils.cc index a2baf003a6..928f79ed1d 100644 --- a/xls/ir/proc_testutils.cc +++ b/xls/ir/proc_testutils.cc @@ -59,49 +59,6 @@ namespace xls { namespace { -// A struct which represents a single IO action, either a send or a receive. -struct IOAction { - // Whether this action is a send or a receive. - bool is_send; - // The data that was sent or received. - BValue data; - // A boolean value which is whether the action is attempted (eg for a - // send_if). - BValue executed; - // A boolean value which is whether the action completes, whether or not a - // value is actually returned/sent. If false then the action is blocked due to - // fifo full/empty. - BValue completes; - - // Additional optional BValue that the input/output gen can fill in for use - // wherever it is required. - std::optional context; -}; - -struct ActivationAction { - // What activation we are on. The first activation is index 0. - int64_t activation_index; - // State vector after this activation. Values are only valid if - // 'activation_complete' is true. - absl::flat_hash_map end_state; - // Values which are sent out from this activation. - absl::flat_hash_map sent_values; - // Map from a receive node to the IO action describing the receive. - absl::flat_hash_map receives_finished; - // Boolean value which is true if the activation completed and false if it - // blocked on a send/recv. - // - // This is the and of all the IOAction.completes values. - BValue activation_complete; -}; - -// A struct which represents the unrolled proc. -struct UnrolledProc { - // State at the end of each activation. - std::vector activations; - // Initial state of the proc. - absl::flat_hash_map initial_state; -}; // A concept for a function that can generate inputs for a given receive. // @@ -177,6 +134,7 @@ class UnrollProcVisitor final : public DfsVisitorWithDefault { ? ios_complete.front() : fb_.And(ios_complete, SourceInfo(), /*name=*/absl::StrCat("act_complete_", activation_)), + .node_values = std::move(values_), }; } @@ -520,10 +478,10 @@ absl::Status CleanupFunction(Function* f) { } // namespace -absl::StatusOr UnrollProcToFunction(Proc* p, - int64_t activation_count, - bool include_state, - const Value& token_value) { +absl::StatusOr UnrollProc(Proc* p, int64_t activation_count, + bool include_state, + const Value& token_value, + bool cleanup) { XLS_RET_CHECK_GT(activation_count, 0) << "At least one activation is required."; if (include_state) { @@ -639,9 +597,23 @@ absl::StatusOr UnrollProcToFunction(Proc* p, } XLS_ASSIGN_OR_RETURN(Function * result, fb.BuildWithReturnValue(fb.Tuple(return_values))); - XLS_RETURN_IF_ERROR(CleanupFunction(result)); + if (cleanup) { + XLS_RETURN_IF_ERROR(CleanupFunction(result)); + } + unrolled.function = result; VLOG(2) << "Proc: \n" << p->DumpIr() << "To Func: \n" << result->DumpIr(); - return result; + return unrolled; +} + +absl::StatusOr UnrollProcToFunction(Proc* p, + int64_t activation_count, + bool include_state, + const Value& token_value) { + XLS_ASSIGN_OR_RETURN( + UnrolledProc unrolled, + UnrollProc(p, activation_count, include_state, token_value, + /*cleanup=*/true)); + return unrolled.function; } namespace { diff --git a/xls/ir/proc_testutils.h b/xls/ir/proc_testutils.h index c743f90eb7..1b9dec5d13 100644 --- a/xls/ir/proc_testutils.h +++ b/xls/ir/proc_testutils.h @@ -16,15 +16,70 @@ #define XLS_IR_PROC_TESTUTILS_H_ #include +#include +#include +#include "absl/container/flat_hash_map.h" #include "absl/status/statusor.h" #include "xls/ir/bits.h" +#include "xls/ir/channel.h" +#include "xls/ir/function.h" +#include "xls/ir/function_builder.h" #include "xls/ir/nodes.h" #include "xls/ir/proc.h" #include "xls/ir/value.h" namespace xls { +// A struct which represents a single IO action, either a send or a receive. +struct IOAction { + // Whether this action is a send or a receive. + bool is_send; + // The data that was sent or received. + BValue data; + // A boolean value which is whether the action is attempted (eg for a + // send_if). + BValue executed; + // A boolean value which is whether the action completes, whether or not a + // value is actually returned/sent. If false then the action is blocked due to + // fifo full/empty. + BValue completes; + + // Additional optional BValue that the input/output gen can fill in for use + // wherever it is required. + std::optional context; +}; + +struct ActivationAction { + // What activation we are on. The first activation is index 0. + int64_t activation_index; + // State vector after this activation. Values are only valid if + // 'activation_complete' is true. + absl::flat_hash_map end_state; + // Values which are sent out from this activation. + absl::flat_hash_map sent_values; + // Map from a receive node to the IO action describing the receive. + absl::flat_hash_map receives_finished; + // Boolean value which is true if the activation completed and false if it + // blocked on a send/recv. + // + // This is the and of all the IOAction.completes values. + BValue activation_complete; + + // Mapping from original proc Node* to its unrolled BValue in this activation. + absl::flat_hash_map node_values; +}; + +// A struct which represents the unrolled proc. +struct UnrolledProc { + // The unrolled function created in the proc's package. + Function* function = nullptr; + // State at the end of each activation. + std::vector activations; + // Initial state of the proc. + absl::flat_hash_map initial_state; +}; + // Helper to convert a proc into a function which performs 'activation_count' // activations. Input and output channels never block (though if non-blocking // may skip the send/recv). @@ -52,10 +107,24 @@ namespace xls { // channels so this should not be messed with. // // This is only intended for use with testing tools such as z3. +// Helper to unroll a proc 'activation_count' times and return the complete +// UnrolledProc data structure, including the unrolled Function* as well as the +// intermediate node_values for every activation. +// +// If 'cleanup' is true, runs DCE and inlining on the unrolled function. When +// checking intermediate non-IO node constancy, set 'cleanup' to false so +// intermediate nodes are not eliminated by DCE. absl::StatusOr UnrollProcToFunction( Proc* p, int64_t activation_count, bool include_state, const Value& token_value = Value::Tuple({Value(UBits(0xdeadbeef, 32))})); +// Version of `UnrollProcToFunction` that also returns the intermediate +// node_values for every activation. +absl::StatusOr UnrollProc( + Proc* p, int64_t activation_count, bool include_state, + const Value& token_value = Value::Tuple({Value(UBits(0xdeadbeef, 32))}), + bool cleanup = true); + // Helper to convert a proc into a function which performs 'activation_count' // activations consuming up to 'output_value_count' values and producing up to // 'output_value_count' values. diff --git a/xls/passes/BUILD b/xls/passes/BUILD index 599c5783ae..2a2a023274 100644 --- a/xls/passes/BUILD +++ b/xls/passes/BUILD @@ -4403,6 +4403,44 @@ xls_pass( ], ) +xls_pass( + name = "non_synth_removal_pass", + srcs = ["non_synth_removal_pass.cc"], + hdrs = ["non_synth_removal_pass.h"], + pass_class = "NonSynthRemovalPass", + deps = [ + ":dce_pass", + ":dfe_pass", + ":non_synth_separation_pass", + ":optimization_pass", + ":optimization_pass_registry", + ":pass_base", + "//xls/common/status:status_macros", + "//xls/ir", + "@abseil-cpp//absl/status:statusor", + ], +) + +cc_test( + name = "non_synth_removal_pass_test", + srcs = ["non_synth_removal_pass_test.cc"], + deps = [ + ":non_synth_removal_pass", + ":optimization_pass", + ":pass_base", + "//xls/common:xls_gunit_main", + "//xls/common/status:matchers", + "//xls/ir", + "//xls/ir:bits", + "//xls/ir:function_builder", + "//xls/ir:ir_test_base", + "//xls/ir:value", + "@abseil-cpp//absl/status:status_matchers", + "@abseil-cpp//absl/status:statusor", + "@googletest//:gtest", + ], +) + cc_test( name = "non_synth_separation_pass_test", srcs = ["non_synth_separation_pass_test.cc"], diff --git a/xls/passes/non_synth_removal_pass.cc b/xls/passes/non_synth_removal_pass.cc new file mode 100644 index 0000000000..d53db8b8b9 --- /dev/null +++ b/xls/passes/non_synth_removal_pass.cc @@ -0,0 +1,75 @@ +// 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/passes/non_synth_removal_pass.h" + +#include + +#include "absl/status/statusor.h" +#include "xls/common/status/status_macros.h" +#include "xls/ir/function_base.h" +#include "xls/ir/node.h" +#include "xls/ir/nodes.h" +#include "xls/passes/dce_pass.h" +#include "xls/passes/dfe_pass.h" +#include "xls/passes/non_synth_separation_pass.h" +#include "xls/passes/optimization_pass.h" +#include "xls/passes/optimization_pass_registry.h" +#include "xls/passes/pass_base.h" + +namespace xls { +namespace { + +class NonSynthInvokeRemovalPass : public OptimizationFunctionBasePass { + public: + NonSynthInvokeRemovalPass() + : OptimizationFunctionBasePass("non_synth_invoke_removal", + "Remove non-synthesizable invokes") {} + + protected: + absl::StatusOr RunOnFunctionBaseInternal( + FunctionBase* f, const OptimizationPassOptions& options, + PassResults* results, OptimizationContext& context) const override { + bool changed = false; + auto node_it = f->nodes().begin(); + while (node_it != f->nodes().end()) { + auto next_it = std::next(node_it); + Node* n = *node_it; + if (n->Is()) { + Invoke* invoke = n->As(); + if (invoke->to_apply()->non_synth()) { + XLS_RETURN_IF_ERROR(f->RemoveNode(n)); + changed = true; + } + } + node_it = next_it; + } + return changed; + } +}; + +} // namespace + +NonSynthRemovalPass::NonSynthRemovalPass() + : OptimizationCompoundPass(kName, + "Strip non-synthesizable nodes and functions") { + Add(); + Add(); + Add(); + Add(); +} + +REGISTER_OPT_PASS(NonSynthRemovalPass); + +} // namespace xls diff --git a/xls/passes/non_synth_removal_pass.h b/xls/passes/non_synth_removal_pass.h new file mode 100644 index 0000000000..cf453e8971 --- /dev/null +++ b/xls/passes/non_synth_removal_pass.h @@ -0,0 +1,46 @@ +// 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_PASSES_NON_SYNTH_REMOVAL_PASS_H_ +#define XLS_PASSES_NON_SYNTH_REMOVAL_PASS_H_ + +#include + +#include "xls/passes/optimization_pass.h" + +namespace xls { + +// A compound optimization pass that removes non-synthesizable operations +// (assert, cover, trace) and their exclusive intermediate dependencies. +// +// Internally runs: +// 1. NonSynthSeparationPass (clones non-synthesizable operations into a +// non-synth function invoked from the original function). +// 2. NonSynthInvokeRemovalPass (deletes invoke nodes calling non-synth +// functions). +// 3. DeadCodeEliminationPass (DCE) to delete intermediate operations consumed +// only by the removed non-synth invokes. +// 4. DeadFunctionEliminationPass (DFE) to remove the cloned non-synth +// functions. +class NonSynthRemovalPass : public OptimizationCompoundPass { + public: + static constexpr std::string_view kName = "non_synth_removal"; + + explicit NonSynthRemovalPass(); + ~NonSynthRemovalPass() override = default; +}; + +} // namespace xls + +#endif // XLS_PASSES_NON_SYNTH_REMOVAL_PASS_H_ diff --git a/xls/passes/non_synth_removal_pass_test.cc b/xls/passes/non_synth_removal_pass_test.cc new file mode 100644 index 0000000000..f2f1ca1a45 --- /dev/null +++ b/xls/passes/non_synth_removal_pass_test.cc @@ -0,0 +1,107 @@ +// 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/passes/non_synth_removal_pass.h" + +#include +#include + +#include "gmock/gmock.h" +#include "gtest/gtest.h" +#include "absl/status/status_matchers.h" +#include "absl/status/statusor.h" +#include "xls/common/status/matchers.h" +#include "xls/ir/bits.h" +#include "xls/ir/function_builder.h" +#include "xls/ir/ir_test_base.h" +#include "xls/ir/node.h" +#include "xls/ir/nodes.h" +#include "xls/ir/package.h" +#include "xls/ir/value.h" +#include "xls/passes/optimization_pass.h" +#include "xls/passes/pass_base.h" + +namespace xls { +namespace { + +using ::absl_testing::IsOkAndHolds; + +class NonSynthRemovalPassTest : public IrTestBase { + protected: + NonSynthRemovalPassTest() = default; + + absl::StatusOr Run(Package* p) { + PassResults results; + OptimizationContext context; + NonSynthRemovalPass pass; + return pass.Run(p, OptimizationPassOptions(), &results, context); + } +}; + +TEST_F(NonSynthRemovalPassTest, RemovesAssertAndDependencies) { + auto p = CreatePackage(); + FunctionBuilder fb("f", p.get()); + auto tok = fb.Literal(Value::Token()); + auto x = fb.Param("x", p->GetBitsType(32)); + auto zero = fb.Literal(UBits(0, 32)); + auto eq = fb.Eq(x, zero); + fb.Assert(tok, eq, "x is zero"); + fb.Add(x, fb.Literal(UBits(1, 32))); + XLS_ASSERT_OK_AND_ASSIGN(Function * f, fb.Build()); + XLS_ASSERT_OK(p->SetTop(f)); + + ASSERT_THAT(Run(p.get()), IsOkAndHolds(true)); + EXPECT_EQ(p->GetFunctionBases().size(), 1); + for (Node* n : p->GetFunctionBases().front()->nodes()) { + EXPECT_FALSE(n->Is()); + EXPECT_FALSE(n->Is()); + EXPECT_NE(n->GetName(), "eq"); + } +} + +TEST_F(NonSynthRemovalPassTest, RemovesTraceAndCoverAndDependencies) { + auto p = CreatePackage(); + FunctionBuilder fb("f", p.get()); + auto tok = fb.Literal(Value::Token()); + auto x = fb.Param("x", p->GetBitsType(32)); + auto cond = fb.Eq(x, fb.Literal(UBits(10, 32))); + fb.Trace(tok, cond, {}, "x is 10"); + fb.Cover(cond, "cover label"); + fb.Add(x, fb.Literal(UBits(1, 32))); + XLS_ASSERT_OK_AND_ASSIGN(Function * f, fb.Build()); + XLS_ASSERT_OK(p->SetTop(f)); + + ASSERT_THAT(Run(p.get()), IsOkAndHolds(true)); + EXPECT_EQ(p->GetFunctionBases().size(), 1); + for (Node* n : p->GetFunctionBases().front()->nodes()) { + EXPECT_FALSE(n->Is()); + EXPECT_FALSE(n->Is()); + EXPECT_FALSE(n->Is()); + EXPECT_NE(n->GetName(), "cond"); + } +} + +TEST_F(NonSynthRemovalPassTest, FunctionWithNoNonSynthNodesUnchanged) { + auto p = CreatePackage(); + FunctionBuilder fb("f", p.get()); + auto x = fb.Param("x", p->GetBitsType(32)); + fb.Add(x, fb.Literal(UBits(1, 32))); + XLS_ASSERT_OK_AND_ASSIGN(Function * f, fb.Build()); + XLS_ASSERT_OK(p->SetTop(f)); + + ASSERT_THAT(Run(p.get()), IsOkAndHolds(false)); +} + +} // namespace +} // namespace xls