TODO: physical-only cells without a liberty function should not stop loading

test/strategies/miter/MiterTests.cpp

@@ -9,6 +9,7 @@
 #include <filesystem>
 #include <fstream>
 #include <functional>
+#include <regex>
 #include <set>
 #include <sstream>
 #include <string>
@@ -3209,6 +3210,85 @@ static int run_kepler_cli_with_args(const std::vector<std::string>& 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<std::string>& 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);