From f4d50061fe4b859d3954f685f1a833ff772e27d2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C3=98yvind=20Harboe?= Date: Tue, 6 Oct 2026 10:00:46 +0200 Subject: [PATCH] Test: physical-only cells without a liberty function do not stop LEC A placed netlist carries physical-only cells -- well taps, fillers, decaps -- with no pins, no logic, and often no liberty entry. Loading stops on one: "TAPCELL cannot be found in SNL while constructing instance u_tap". LecIgnoresPhysicalOnlyCellsWithoutAFunction compares a netlist with one against the same netlist without it and expects them equivalent. It fails today; this is the request, not the fix. Co-Authored-By: Claude Opus 5.5 --- test/strategies/miter/MiterTests.cpp | 80 ++++++++++++++++++++++++++++ 1 file changed, 80 insertions(+) diff --git a/test/strategies/miter/MiterTests.cpp b/test/strategies/miter/MiterTests.cpp index 628c2266..e12a3864 100644 --- a/test/strategies/miter/MiterTests.cpp +++ b/test/strategies/miter/MiterTests.cpp @@ -9,6 +9,7 @@ #include #include #include +#include #include #include #include @@ -3209,6 +3210,85 @@ static int run_kepler_cli_with_args(const std::vector& args) { #endif } +// A scratch directory per test, and a shell run of kepler-formal in it with +// stdout and stderr kept: the subprocess form of a CLI test. +static std::filesystem::path cliScratchDir(const std::string& name) { + const auto dir = std::filesystem::temp_directory_path() / + ("kepler_cli_" + name + "_" + + std::to_string(std::chrono::steady_clock::now() + .time_since_epoch() + .count())); + std::filesystem::create_directories(dir); + return dir; +} + +static void writeText(const std::filesystem::path& path, const std::string& text) { + std::ofstream out(path); + out << text; +} + +static std::string readText(const std::filesystem::path& path) { + std::ifstream in(path); + std::stringstream text; + text << in.rdbuf(); + return text.str(); +} + +// AND2, NAND2 and INV, enough for an equivalent pair the miter cannot hash +// away: AND2 against NAND2 into INV. +static const char* kTinyLiberty = + "library(tiny) {\n" + " cell(AND2) {\n" + " pin(A) { direction : input; }\n" + " pin(B) { direction : input; }\n" + " pin(Y) { direction : output; function : \"(A&B)\"; }\n" + " }\n" + " cell(NAND2) {\n" + " pin(A) { direction : input; }\n" + " pin(B) { direction : input; }\n" + " pin(Y) { direction : output; function : \"!(A&B)\"; }\n" + " }\n" + " cell(INV) {\n" + " pin(A) { direction : input; }\n" + " pin(Y) { direction : output; function : \"!A\"; }\n" + " }\n" + "}\n"; + +// Runs kepler-formal in `dir`; its output goes to `dir`/kepler.out. +static int runKeplerIn(const std::filesystem::path& dir, + const std::vector& args) { + std::string cmd = "cd '" + dir.string() + "' && '" + std::string(KEPLER_BIN) + "'"; + for (const auto& a : args) { + cmd += " '" + a + "'"; + } + cmd += " > kepler.out 2>&1"; + const int rc = std::system(cmd.c_str()); + return (rc != -1 && WIFEXITED(rc)) ? WEXITSTATUS(rc) : EXIT_FAILURE; +} + +TEST(KeplerCliSubprocessTests, LecIgnoresPhysicalOnlyCellsWithoutAFunction) { + // A placed netlist carries physical-only cells -- well taps, fillers, + // decaps -- with no pins and no logic, and often no liberty entry. The + // netlist with one is equivalent to the same netlist without it; today + // loading stops ("TAPCELL cannot be found in SNL"). + const auto dir = cliScratchDir("physical_only_cells"); + writeText(dir / "tiny.lib", kTinyLiberty); + writeText(dir / "plain.v", + "module top(input a, input b, output y);\n" + " AND2 u (.A(a), .B(b), .Y(y));\n" + "endmodule\n"); + writeText(dir / "tapped.v", + "module top(input a, input b, output y);\n" + " AND2 u (.A(a), .B(b), .Y(y));\n" + " TAPCELL u_tap ();\n" + "endmodule\n"); + EXPECT_EQ(runKeplerIn(dir, {"-verilog", "plain.v", "tapped.v", "tiny.lib"}), 0) + << readText(dir / "kepler.out"); + EXPECT_NE(readText(dir / "kepler.out").find("No difference was found"), + std::string::npos); + std::filesystem::remove_all(dir); +} + TEST(KeplerCliSubprocessTests, BinaryExists) { std::filesystem::path p(KEPLER_BIN); bool exists = std::filesystem::exists(p);