From cabd6d302cb67a00dd8edd404db8b397750c1b33 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C3=98yvind=20Harboe?= Date: Tue, 6 Oct 2026 09:36:01 +0200 Subject: [PATCH 1/2] LEC: name the problem the solver is given, and the time it takes "Starting solver" said nothing about what it started on. On a 256-word, 21-port register file the miter built in four minutes and the solver then ran for over half an hour with nothing more logged: no way to tell a hard problem from a hang, or to compare it with a smaller run. The two existing lines now carry it, without adding a line: Starting solver: variables, clauses, outputs compared SAT solver finished: UNSAT in s SATSolverWrapper counts the clauses it is handed and the largest variable they use. LecLogNamesTheSolverProblemAndItsTime runs an equivalent pair the miter cannot hash away (a & b against ~(~a | ~b)) and reads both lines from the log. Co-Authored-By: Claude Opus 5.5 --- src/sat/SATSolverWrapper.h | 12 ++++++ src/strategies/miter/MiterStrategy.cpp | 15 +++++-- .../strategies/miter/KeplerFormalCliTests.cpp | 41 +++++++++++++++++++ 3 files changed, 64 insertions(+), 4 deletions(-) diff --git a/src/sat/SATSolverWrapper.h b/src/sat/SATSolverWrapper.h index a024dec1..52748ef1 100644 --- a/src/sat/SATSolverWrapper.h +++ b/src/sat/SATSolverWrapper.h @@ -340,9 +340,19 @@ class SATSolverWrapper { addClauseRange(lits); } + // The problem as handed to the solver, for the log line that starts it: + // clauses added and the largest variable any of them uses. + size_t numClauses() const { return numClauses_; } + size_t numVariables() const { return numVariables_; } + private: template void addClauseRange(const ClauseRange& lits) { + ++numClauses_; + for (int lit : lits) { + // external +-(var+2): a literal of magnitude v is variable v-1 counted from 1 + numVariables_ = std::max(numVariables_, static_cast(std::abs(lit)) - 1); + } if (solverType_ == KEPLER_FORMAL::Config::SolverType::GLUCOSE) { Glucose::vec clause; for (int lit : lits) { @@ -1115,6 +1125,8 @@ class SATSolverWrapper { // LCOV_EXCL_STOP private: + size_t numClauses_ = 0; + size_t numVariables_ = 0; static CaDiCraig::CraigVarType cadicalCraigVariableType( // LCOV_EXCL_LINE CraigVariablePartition partition) { switch (partition) { // LCOV_EXCL_LINE diff --git a/src/strategies/miter/MiterStrategy.cpp b/src/strategies/miter/MiterStrategy.cpp index 4ca2cbd8..8e91fab1 100644 --- a/src/strategies/miter/MiterStrategy.cpp +++ b/src/strategies/miter/MiterStrategy.cpp @@ -1,6 +1,7 @@ // Copyright 2024-2026 keplertech.io // SPDX-License-Identifier: Apache-2.0 +#include #include "MiterStrategy.h" #include "BoolExpr.h" #include "BuildPrimaryOutputClauses.h" @@ -1053,9 +1054,12 @@ bool MiterStrategy::run(bool compact) { solver.addClause({rootVar}); // solve with no assumptions - logger->info("Starting solver"); + logger->info("Starting solver: {} variables, {} clauses, {} outputs compared", + solver.numVariables(), solver.numClauses(), POs0.size()); + const auto solveStart = std::chrono::steady_clock::now(); bool sat = solver.solve(); - logger->info("SAT solver finished: {}", sat ? "SAT" : "UNSAT"); + logger->info("SAT solver finished: {} in {:.1f} s", sat ? "SAT" : "UNSAT", + std::chrono::duration(std::chrono::steady_clock::now() - solveStart).count()); if (sat) { logger->info("Miter found a difference -> moving to analyze individual POs"); @@ -1362,9 +1366,12 @@ bool MiterStrategy::runCompactPOs(const tbb::concurrent_vector& POs0, int rootVar = tseitinEncode(solver, miter, node2var, varName2idx); solver.addClause({rootVar}); - logger->info("Starting solver"); + logger->info("Starting solver: {} variables, {} clauses, {} outputs compared", + solver.numVariables(), solver.numClauses(), POs0.size()); + const auto solveStart = std::chrono::steady_clock::now(); const bool sat = solver.solve(); - logger->info("SAT solver finished: {}", sat ? "SAT" : "UNSAT"); + logger->info("SAT solver finished: {} in {:.1f} s", sat ? "SAT" : "UNSAT", + std::chrono::duration(std::chrono::steady_clock::now() - solveStart).count()); logger->info("Circuits are {}", sat ? "DIFFERENT" : "IDENTICAL"); if (sat) { logger->warn("Due to compact mode, per PO analysis is skipped."); diff --git a/test/strategies/miter/KeplerFormalCliTests.cpp b/test/strategies/miter/KeplerFormalCliTests.cpp index 30b58ba8..2e50b6df 100644 --- a/test/strategies/miter/KeplerFormalCliTests.cpp +++ b/test/strategies/miter/KeplerFormalCliTests.cpp @@ -12,6 +12,7 @@ #include #include #include +#include #include #include #include @@ -1029,6 +1030,46 @@ TEST_F(KeplerFormalCliTests, InProcessDriverRejectsAnActiveNajaUniverse) { EXPECT_EQ(help.result.status, KEPLER_FORMAL::RunStatus::NoResult); } +TEST_F(KeplerFormalCliTests, LecLogNamesTheSolverProblemAndItsTime) { + // An equivalent pair the miter cannot hash away, so the solver runs. Its + // start line names the problem it was given and its finish line the time: + // a long solve can then be told from a hang and compared with a smaller. + NamedLoggerGuard loggerGuard("kepler_formal_main_logger"); + const auto fixture = createDesignFixture( + "v", + "module top(input a, input b, output y);\n" + " assign y = a & b;\n" + "endmodule\n", + "module top(input a, input b, output y);\n" + " assign y = ~(~a | ~b);\n" + "endmodule\n"); + const auto log = fixture.tmpDir / "problem_size.log"; + const auto cfg = writeTempConfig( + "format: verilog\n" + "verification: lec\n" + "input_paths:\n" + " - " + fixture.design0Path.string() + "\n" + " - " + fixture.design1Path.string() + "\n" + "log_file: " + log.string() + "\n"); + const auto run = runStructuredWithConfigFile(cfg); + EXPECT_EQ(run.exitCode, EXIT_SUCCESS); + EXPECT_EQ(run.result.status, KEPLER_FORMAL::RunStatus::Equivalent); + std::ifstream in(log); + std::stringstream text; + text << in.rdbuf(); + EXPECT_TRUE(std::regex_search( + text.str(), + std::regex("Starting solver: [0-9]+ variables, [0-9]+ clauses, " + "[0-9]+ outputs compared"))) + << text.str(); + EXPECT_TRUE(std::regex_search( + text.str(), + std::regex("SAT solver finished: (SAT|UNSAT) in [0-9]+\\.[0-9] s"))) + << text.str(); + std::filesystem::remove(cfg); + std::filesystem::remove_all(fixture.tmpDir); +} + TEST_F(KeplerFormalCliTests, InProcessDriverReturnsStructuredLecResults) { SolverGuard solverGuard; ReportSkippedPOsGuard reportGuard; From cf650378a42220ed36ebfe602ba501c6ed2e6263 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C3=98yvind=20Harboe?= Date: Tue, 6 Oct 2026 09:59:59 +0200 Subject: [PATCH 2/2] Solver problem size: a test the Bazel build runs KeplerFormalCliTests.cpp is built by CMake only. MiterTests' LecLogNamesTheSolverProblemAndItsTime runs the binary on AND2 against NAND2 into INV (a tiny inline liberty), an equivalent pair the miter cannot hash away, and reads both solver lines from the log. Co-Authored-By: Claude Opus 5.5 --- test/strategies/miter/MiterTests.cpp | 91 ++++++++++++++++++++++++++++ 1 file changed, 91 insertions(+) diff --git a/test/strategies/miter/MiterTests.cpp b/test/strategies/miter/MiterTests.cpp index 628c2266..e520c8ca 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,96 @@ 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, LecLogNamesTheSolverProblemAndItsTime) { + // An equivalent pair the miter cannot hash away, so the solver runs: its + // start line names the problem it was given, its finish line the time. + const auto dir = cliScratchDir("lec_problem_size"); + writeText(dir / "tiny.lib", kTinyLiberty); + writeText(dir / "and.v", + "module top(input a, input b, output y);\n" + " AND2 u (.A(a), .B(b), .Y(y));\n" + "endmodule\n"); + writeText(dir / "nand_inv.v", + "module top(input a, input b, output y);\n" + " wire n;\n" + " NAND2 u0 (.A(a), .B(b), .Y(n));\n" + " INV u1 (.A(n), .Y(y));\n" + "endmodule\n"); + writeText(dir / "cfg.yaml", + "format: verilog\n" + "verification: lec\n" + "input_paths:\n - and.v\n - nand_inv.v\n" + "liberty_files:\n - tiny.lib\n" + "log_file: miter.log\n"); + ASSERT_EQ(runKeplerIn(dir, {"--config", "cfg.yaml"}), 0) + << readText(dir / "kepler.out"); + const auto log = readText(dir / "miter.log"); + EXPECT_TRUE(std::regex_search( + log, std::regex("Starting solver: [0-9]+ variables, [0-9]+ clauses, " + "[0-9]+ outputs compared"))) + << log; + EXPECT_TRUE(std::regex_search( + log, std::regex("SAT solver finished: UNSAT in [0-9]+\\.[0-9] s"))) + << log; + std::filesystem::remove_all(dir); +} + TEST(KeplerCliSubprocessTests, BinaryExists) { std::filesystem::path p(KEPLER_BIN); bool exists = std::filesystem::exists(p);