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; 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);