diff --git a/README.md b/README.md index 81988786..12944f4c 100644 --- a/README.md +++ b/README.md @@ -155,7 +155,7 @@ or runtime errors are execution failures rather than SEC verdicts. ```bash # Single file per design -build/src/bin/kepler-formal <-verilog/-naja_if/-systemverilog/-sv/-sv2v> [options] \ +build/src/bin/kepler-formal <-verilog/-naja_if/-systemverilog/-sv/-sv2v/-vhdl> [options] \ [...] # Multi-file Verilog @@ -168,6 +168,11 @@ build/src/bin/kepler-formal -sv -v sec \ --sv_design1_flist --sv_design1_top \ --sv_design2_flist --sv_design2_top \ [--liberty ...] + +# VHDL SEC, files in compile order with the top-level unit last +build/src/bin/kepler-formal -vhdl -v sec \ + --design1 --design2 \ + [--vhdl_design1_top ] [--vhdl_design2_top ] ``` | Flag | Meaning | @@ -183,9 +188,11 @@ build/src/bin/kepler-formal -sv -v sec \ | `-naja_if` | Parse both designs as Naja IF. | | `-systemverilog`, `-sv` | Parse both designs as SystemVerilog. Requires SEC. | | `-sv2v` | Parse design 1 as SystemVerilog and design 2 as Verilog for SEC RTL-vs-gate comparison. | +| `-vhdl` | Parse both designs as VHDL. Requires SEC. Experimental; see [VHDL support](docs/vhdl/README.md). | | `--design1 ` | Explicit source list for design 1 in multi-file Verilog mode. | | `--design2 ` | Explicit source list for design 2 in multi-file Verilog mode. | | `--verilog_design1_top `, `--verilog_design2_top ` | Select the top module for each Verilog design. In `sv2v` mode, only design 2 is Verilog. | +| `--vhdl_design1_top `, `--vhdl_design2_top ` | Select the top entity for each VHDL design. | | `-sv`, `-systemverilog` | Use SystemVerilog input mode. | | `--liberty `, `--lib ` | Liberty library files. | | `--verilog_preprocessing` | Enable preprocessing for Verilog inputs. | @@ -206,7 +213,7 @@ build/src/bin/kepler-formal --config | Key | Type | Meaning | | --- | --- | --- | -| `format` | string | `verilog`, `v`, `naja_if`, `systemverilog`, `sv`, or `sv2v`. Defaults to `verilog` if omitted. | +| `format` | string | `verilog`, `v`, `naja_if`, `systemverilog`, `sv`, `sv2v`, `vhdl`, or `vhd`. Defaults to `verilog` if omitted. | | `verification` | string | `lec` or `sec`. Defaults to `lec`. | | `btor2_export` | bool | Enable BTOR2 export before solving; SEC only. Defaults to `false`. | | `btor2_export_path` | string | BTOR2 destination; defaults to `miter.btor2` when enabled. Requires `btor2_export: true`. | @@ -214,6 +221,7 @@ build/src/bin/kepler-formal --config | `allow-boundary-mismatch` | bool | Allow an LEC boundary mismatch. Defaults to `false`; ignored for SEC. | | `input_paths` | list | Required. Either `[design0, design1]` or `[[design0_file...], [design1_file...]]`. The nested form is for multi-file Verilog. | | `verilog_design1_top`, `verilog_design2_top` | string | Select the top module for each Verilog design. In `sv2v` mode, only `verilog_design2_top` is valid. | +| `vhdl_design1_top`, `vhdl_design2_top` | string | Select the top entity for each VHDL design. Only valid with `format: vhdl`. | | `liberty_files` | list[string] | Liberty libraries loaded through `SNLLibertyConstructor`. | | `py_tech_files` | list[string] | Python primitive loaders loaded through `SNLPyLoader`. | | `verilog_preprocessing` | bool | Enable preprocessing for Verilog inputs. | diff --git a/bazel/naja.BUILD.bazel b/bazel/naja.BUILD.bazel index 9555c85c..67936294 100644 --- a/bazel/naja.BUILD.bazel +++ b/bazel/naja.BUILD.bazel @@ -10,6 +10,7 @@ cc_library( "//src/nl/formats/liberty:naja_snl_liberty", "//src/nl/formats/systemverilog:naja_snl_systemverilog", "//src/nl/formats/verilog:naja_snl_verilog", + "//src/nl/formats/vhdl:naja_snl_vhdl", "//src/nl/netlist:naja_nl", "//src/nl/netlist:naja_snl_visual", "//src/nl/netlist/serialization/capnp:naja_nl_dump", diff --git a/docs/flags-spec.md b/docs/flags-spec.md index aa93d07e..dd79acfc 100644 --- a/docs/flags-spec.md +++ b/docs/flags-spec.md @@ -17,6 +17,7 @@ The SEC-specific flag surface is documented separately in | `sec` | Gate-level sequential equivalence checking | Sequential Verilog/SystemVerilog netlists plus Liberty/Python primitive libraries as needed. | | `sec` | RTL-level sequential equivalence checking | RTL Verilog/SystemVerilog sources, including SystemVerilog flists with explicit tops. | | `sec` | SystemVerilog-to-Verilog RTL-vs-gate checking (`sv2v`) | SystemVerilog design 1 and Verilog design 2, plus Liberty/Python primitive libraries as needed. | +| `sec` | VHDL RTL-level sequential equivalence checking (`vhdl`) | VHDL sources for both designs, in compile order. Experimental; see [VHDL support](vhdl/README.md). | LEC is the default. Select SEC with `-v sec`, `--verification sec`, or `verification: sec` in YAML. @@ -41,6 +42,7 @@ LEC is the default. Select SEC with `-v sec`, `--verification sec`, or | `-naja_if` | Use naja-if format. | | `-systemverilog`, `-sv` | Use SystemVerilog format for both designs. Requires SEC verification. | | `-sv2v` | Use mixed SystemVerilog-to-Verilog format for SEC RTL-vs-gate comparison: design 1 is parsed as SystemVerilog, design 2 is parsed as Verilog. | +| `-vhdl` | Use VHDL format for both designs. Requires SEC verification. | | `--help`, `-h` | Print usage and exit. | | `--version`, `-V` | Print the embedded Kepler Formal and Naja versions and Git hashes to stdout and exit successfully. Use as a standalone option. | | `--config `, `-c ` | Load a YAML config file. Config mode cannot be combined with other command-line options. | @@ -51,6 +53,7 @@ LEC is the default. Select SEC with `-v sec`, `--verification sec`, or | `--sv_design1_flist `, `--sv_design2_flist ` | Per-design SystemVerilog file lists. Only design 1 is valid in `sv2v` mode. | | `--sv_design1_top `, `--sv_design2_top ` | Per-design SystemVerilog top modules. Only design 1 is valid in `sv2v` mode. | | `--verilog_design1_top `, `--verilog_design2_top ` | Per-design Verilog top modules. Only design 2 is valid in `sv2v` mode. | +| `--vhdl_design1_top `, `--vhdl_design2_top ` | Per-design VHDL top entities. Only valid in `vhdl` mode. | | `--compact` | Reduce peak memory. In SEC, extract and release design 1 before loading design 2. | | `--report-skipped-pos` | Emit skipped-PO reports in the current working directory. | @@ -58,7 +61,7 @@ LEC is the default. Select SEC with `-v sec`, `--verification sec`, or | Key | Type | Meaning | | --- | --- | --- | -| `format` | string | Input format: `verilog`, `v`, `naja_if`, `systemverilog`, `sv`, or `sv2v`. If omitted, the implementation defaults to `verilog`. | +| `format` | string | Input format: `verilog`, `v`, `naja_if`, `systemverilog`, `sv`, `sv2v`, `vhdl`, or `vhd`. If omitted, the implementation defaults to `verilog`. | | `verification` | string | `lec` or `sec`. Defaults to `lec`. | | `max_k` | integer | SEC proof/search bound. Defaults to `32`. | | `sec_engine` | string | `k_induction`, `imc`, or `pdr`. Defaults to `pdr`. | @@ -88,6 +91,7 @@ LEC is the default. Select SEC with `-v sec`, `--verification sec`, or | `sv_design1_flist`, `sv_design2_flist` | string | Per-design SystemVerilog file lists. Only design 1 is valid in `sv2v` mode. | | `sv_design1_top`, `sv_design2_top` | string | Per-design SystemVerilog top modules. Only design 1 is valid in `sv2v` mode. | | `verilog_design1_top`, `verilog_design2_top` | string | Per-design Verilog top modules. Only design 2 is valid in `sv2v` mode. | +| `vhdl_design1_top`, `vhdl_design2_top` | string | Per-design VHDL top entities. Only valid in `vhdl` mode. | | `solver` | string | SAT solver selection: `kissat`, `glucose`, or `cadical`. Defaults to `kissat`. | Example: diff --git a/docs/vhdl/README.md b/docs/vhdl/README.md new file mode 100644 index 00000000..0f300ca1 --- /dev/null +++ b/docs/vhdl/README.md @@ -0,0 +1,74 @@ +# VHDL Support + +This document tracks the VHDL flow in `kepler-formal`. + +Status: + +- experimental: the VHDL frontend in Naja is in beta and accepts a restricted + RTL subset +- supported for RTL-level SEC, with both designs given as VHDL +- the `vhdl` input mode requires SEC verification + +## Usage + +CLI flag: `-vhdl`. YAML: `format: vhdl` (or `vhd`). + +```bash +# Single file per design +build/src/bin/kepler-formal -vhdl -v sec + +# Multi-file VHDL designs +build/src/bin/kepler-formal -vhdl -v sec \ + --design1 --design2 \ + [--vhdl_design1_top ] [--vhdl_design2_top ] +``` + +```yaml +format: vhdl +verification: sec +vhdl_design1_top: top +vhdl_design2_top: top +input_paths: + - [design1/pkg.vhd, design1/leaf.vhd, design1/top.vhd] + - [design2/top.vhd] +``` + +## File order + +Files are loaded one at a time, in the order given, and each file can use the +units of the files before it. List them in compile order: packages and +instantiated entities first, the top-level unit last. A file that instantiates +an entity from a later file is rejected with a `missing entity` error. + +## Top selection + +`vhdl_design1_top` and `vhdl_design2_top` name the top entity of each design. +The top is elaborated after the last file is loaded, so it may be declared in +any of the files. + +Without a top option, the top is the design built from the last file that +produces one; package-only files produce none. When that file declares several +entities, the top is the one no other entity instantiates. Name the top +explicitly whenever the last file is not the top-level unit. + +## Supported language subset + +Naja lowers VHDL to the same primitives as its SystemVerilog frontend, as +two-state hardware. The subset covers `bit`, `bit_vector` and imported +`std_logic` types, concurrent and conditional assignments, positive-edge +processes with synchronous reset and enable, constrained arrays with static +indexing, and direct entity instantiation. See +`thirdparty/naja/src/vhdl/README.md` for the current limits. + +A construct outside the subset stops the run with an error that names the file +and line. It is never approximated. + +## Notes + +- Warnings from the VHDL frontend are printed on the console. No separate + diagnostics report is written. +- Registers without a reset bootstrap need the default `dual_rail_steady` + encoding. With `sec_encoding: binary`, give a reset bootstrap through + `sec_reset`; see [SEC reset bootstrap](../sec-reset-bootstrap.md). +- Mixed comparisons, such as VHDL against Verilog or SystemVerilog, are not + available. diff --git a/src/bin/CMakeLists.txt b/src/bin/CMakeLists.txt index 485efae1..bd3c6efb 100644 --- a/src/bin/CMakeLists.txt +++ b/src/bin/CMakeLists.txt @@ -38,6 +38,7 @@ set(KEPLER_FORMAL_DRIVER_LIBRARIES naja_snl_liberty naja_snl_systemverilog naja_snl_verilog + naja_snl_vhdl kissat cadical formal_strategies diff --git a/src/bin/KeplerFormal.cpp b/src/bin/KeplerFormal.cpp index 1af7988d..54d58e4e 100644 --- a/src/bin/KeplerFormal.cpp +++ b/src/bin/KeplerFormal.cpp @@ -37,6 +37,7 @@ #include "SNLSVConstructor.h" #include "SNLVRLConstructor.h" #include "SNLVRLDumper.h" +#include "VHDLConstructor.h" #include "SNLBusTerm.h" #include "SNLInstance.h" #include "SNLRTLInfos.h" @@ -64,13 +65,14 @@ static const char* kSkippedOpaqueCellPOReport = static void print_usage(const char* prog) { SPDLOG_INFO( // LCOV_EXCL_STOP - "Usage: {} --version | [--config ] | <-naja_if/-verilog/-systemverilog/-sv/-sv2v> " + "Usage: {} --version | [--config ] | <-naja_if/-verilog/-systemverilog/-sv/-sv2v/-vhdl> " "[-v ] [-k ] [--sec-engine ] [--sec-encoding ] [--learn-internal-relations ] [--allow-x-equality-in-internal-relations ] [--sec-reset-cycles ] [--sec-reset-port ...] " "[--verilog_design1_top ] [--verilog_design2_top ] " + "[--vhdl_design1_top ] [--vhdl_design2_top ] " "[--set-as-boundary ]... " " [...] | " - "<-naja_if/-verilog/-systemverilog/-sv/-sv2v> --design1 --design2 " - " [--verilog_design1_top ] [--verilog_design2_top ] [--liberty ...] [-v ] [-k ] [--sec-engine ] [--sec-encoding ] [--learn-internal-relations ] [--allow-x-equality-in-internal-relations ] [--sec-reset-cycles ] [--sec-reset-port ...] " + "<-naja_if/-verilog/-systemverilog/-sv/-sv2v/-vhdl> --design1 --design2 " + " [--verilog_design1_top ] [--verilog_design2_top ] [--vhdl_design1_top ] [--vhdl_design2_top ] [--liberty ...] [-v ] [-k ] [--sec-engine ] [--sec-encoding ] [--learn-internal-relations ] [--allow-x-equality-in-internal-relations ] [--sec-reset-cycles ] [--sec-reset-port ...] " "[--allow-boundary-mismatch] [--compact] " "[--set-as-boundary ]... " "[--report-skipped-pos] | " @@ -514,6 +516,8 @@ static bool validateConfigKeys(const YAML::Node& cfg) { "verilog_design2_top", "sv_design1_top", "sv_design2_top", + "vhdl_design1_top", + "vhdl_design2_top", }; for (auto it = cfg.begin(); it != cfg.end(); ++it) { @@ -566,6 +570,9 @@ struct VerilogTopOptions { std::optional design1; }; +// VHDL selects its tops the same way: one optional name per design. +using VhdlTopOptions = VerilogTopOptions; + static bool parseConfigInputPaths(const YAML::Node& node, DesignInputs& out, std::string& error) { @@ -771,7 +778,7 @@ static bool sameCompactSecDesignSpec( bool isSystemVerilog, const DesignInputs& designInputs, const SystemVerilogOptions& systemVerilogOptions, - const VerilogTopOptions& verilogTopOptions, + const VerilogTopOptions& topOptions, const KEPLER_FORMAL::BoundaryPairs& boundaryPairs) { if (normalizeInputListForComparison(designInputs.design0) != normalizeInputListForComparison(designInputs.design1)) { @@ -784,7 +791,7 @@ static bool sameCompactSecDesignSpec( } // LCOV_EXCL_START if (!isSystemVerilog) { - return verilogTopOptions.design0 == verilogTopOptions.design1; + return topOptions.design0 == topOptions.design1; // LCOV_EXCL_STOP } // LCOV_EXCL_START @@ -809,6 +816,33 @@ static naja::NL::SNLDesign* selectTopDesign( return top; } +// Naja's VHDL loader reads one file per call and keeps the earlier sources in +// the library, so files are loaded in compile order: packages and instantiated +// entities first, the top-level unit last. The requested top is elaborated +// once every file is known. +static naja::NL::SNLDesign* constructVhdlDesign( + naja::NL::NLLibrary* library, + const std::vector& designPaths, + const std::optional& requestedTop) { + naja::NL::VHDLConstructor::ConstructOptions options; + // Naja's default report file is rewritten by every load, so a multi-file + // design would keep only its last file. Warnings stay on the console. + options.diagnosticsReportPath.reset(); + const naja::NL::VHDLConstructor constructor(library, options); + naja::NL::SNLDesign* top = nullptr; + for (size_t i = 0; i < designPaths.size(); ++i) { + const bool isLast = i + 1 == designPaths.size(); + const std::string_view fileTop = + isLast && requestedTop ? std::string_view(*requestedTop) + : std::string_view(); + // Package-only files and entities awaiting generic values return null. + if (auto* design = constructor.constructFile(designPaths[i], fileTop)) { + top = design; + } + } + return top; +} + static bool applySystemVerilogConfigOption(const YAML::Node& cfg, const char* key, std::optional& target, @@ -1207,7 +1241,7 @@ static int KeplerFormalMainImpl( KEPLER_FORMAL::RunResult* runResult, const KEPLER_FORMAL::PrimitiveLibraryLoader& primitiveLoader) { using namespace std::chrono; - enum class FormatType { VERILOG, SYSTEMVERILOG, SV2V, NAJA_IF }; + enum class FormatType { VERILOG, SYSTEMVERILOG, SV2V, VHDL, NAJA_IF }; constexpr size_t kDefaultSecMaxK = 32; const auto cleanupNajaState = []() { naja::DNL::destroy(); @@ -1230,6 +1264,7 @@ static int KeplerFormalMainImpl( DesignInputs designInputs; SystemVerilogOptions systemVerilogOptions; VerilogTopOptions verilogTopOptions; + VhdlTopOptions vhdlTopOptions; KEPLER_FORMAL::BoundaryPairs boundaryPairs; std::vector libertyFiles; std::vector pythonFiles; @@ -1313,6 +1348,8 @@ static int KeplerFormalMainImpl( inputFormatType = FormatType::SYSTEMVERILOG; } else if (fmt == "sv2v") { inputFormatType = FormatType::SV2V; + } else if (fmt == "vhdl" || fmt == "vhd") { + inputFormatType = FormatType::VHDL; } else { SPDLOG_CRITICAL("Unrecognized format in config: {}", fmt); return EXIT_FAILURE; @@ -1565,7 +1602,11 @@ static int KeplerFormalMainImpl( !applySystemVerilogConfigOption( cfg, "verilog_design1_top", verilogTopOptions.design0, svConfigError) || !applySystemVerilogConfigOption( - cfg, "verilog_design2_top", verilogTopOptions.design1, svConfigError)) { + cfg, "verilog_design2_top", verilogTopOptions.design1, svConfigError) || + !applySystemVerilogConfigOption( + cfg, "vhdl_design1_top", vhdlTopOptions.design0, svConfigError) || + !applySystemVerilogConfigOption( + cfg, "vhdl_design2_top", vhdlTopOptions.design1, svConfigError)) { // LCOV_EXCL_START SPDLOG_CRITICAL("Invalid design config option: {}", svConfigError); return EXIT_FAILURE; @@ -1783,6 +1824,12 @@ static int KeplerFormalMainImpl( formatFound = true; break; } + if (arg == "-vhdl") { + inputFormatType = FormatType::VHDL; + ++parseStart; + formatFound = true; + break; + } // LCOV_EXCL_START SPDLOG_CRITICAL("Unrecognized option before input format type: {}", arg); return EXIT_FAILURE; @@ -1991,6 +2038,7 @@ static int KeplerFormalMainImpl( // LCOV_EXCL_START if (arg == "--sv_design1_flist" || arg == "--sv_design2_flist" || arg == "--verilog_design1_top" || arg == "--verilog_design2_top" || + arg == "--vhdl_design1_top" || arg == "--vhdl_design2_top" || arg == "--sv_design1_top" || arg == "--sv_design2_top") { if (i + 1 >= argc) { SPDLOG_CRITICAL("Missing value after {}", arg); @@ -2015,6 +2063,10 @@ static int KeplerFormalMainImpl( systemVerilogOptions.design1.top = value; } else if (arg == "--verilog_design1_top") { verilogTopOptions.design0 = value; + } else if (arg == "--vhdl_design1_top") { + vhdlTopOptions.design0 = value; + } else if (arg == "--vhdl_design2_top") { + vhdlTopOptions.design1 = value; } else { verilogTopOptions.design1 = value; // LCOV_EXCL_STOP @@ -2094,6 +2146,10 @@ static int KeplerFormalMainImpl( inputFormatName = "SV2V"; inputFormatToken = "sv2v"; } + if (inputFormatType == FormatType::VHDL) { + inputFormatName = "VHDL"; + inputFormatToken = "vhdl"; + } if (runResult != nullptr) { runResult->inputFormat = inputFormatToken; runResult->verification = verificationModeName(verificationMode); @@ -2159,6 +2215,12 @@ static int KeplerFormalMainImpl( "SystemVerilog input formats require SEC verification (-v sec or verification: sec)"); return EXIT_FAILURE; } + if (inputFormatType == FormatType::VHDL && + verificationMode != VerificationMode::SEC) { + SPDLOG_CRITICAL( + "VHDL input format requires SEC verification (-v sec or verification: sec)"); + return EXIT_FAILURE; + } std::string btor2ExportError; if (!btor2ExportConfig.validate( verificationMode == VerificationMode::SEC, btor2ExportError)) { @@ -2254,6 +2316,11 @@ static int KeplerFormalMainImpl( "Verilog top options are only valid with -verilog/-sv2v input"); return EXIT_FAILURE; } + if (inputFormatType != FormatType::VHDL && + (vhdlTopOptions.design0 || vhdlTopOptions.design1)) { + SPDLOG_CRITICAL("VHDL top options are only valid with -vhdl input"); + return EXIT_FAILURE; + } if (inputFormatType == FormatType::SV2V && verilogTopOptions.design0) { SPDLOG_CRITICAL( "sv2v format only accepts a Verilog top option for design 2; " @@ -2545,9 +2612,12 @@ static int KeplerFormalMainImpl( const auto isHdlFormat = [&]() { return inputFormatType == FormatType::VERILOG || inputFormatType == FormatType::SYSTEMVERILOG || - inputFormatType == FormatType::SV2V; + inputFormatType == FormatType::SV2V || + inputFormatType == FormatType::VHDL; }; + const bool useVhdl = inputFormatType == FormatType::VHDL; + const auto designUsesSystemVerilog = [&](int designIndex) { return inputFormatType == FormatType::SYSTEMVERILOG || (inputFormatType == FormatType::SV2V && designIndex == 0); @@ -2580,10 +2650,18 @@ static int KeplerFormalMainImpl( db->setID(dbID); const bool useSystemVerilog = designUsesSystemVerilog(designIndex); SPDLOG_INFO("Parsing {} file(s) for design {}", - useSystemVerilog ? "systemverilog" : "verilog", + useVhdl ? "vhdl" + : useSystemVerilog ? "systemverilog" : "verilog", designIndex + 1); auto designLibrary = NLLibrary::create(db, NLName("DESIGN")); - if (useSystemVerilog) { + naja::NL::SNLDesign* vhdlTop = nullptr; + if (useVhdl) { + vhdlTop = constructVhdlDesign( + designLibrary, + designPaths, + designIndex == 0 ? vhdlTopOptions.design0 + : vhdlTopOptions.design1); + } else if (useSystemVerilog) { // LCOV_EXCL_START SNLSVConstructor constructor(designLibrary); std::vector temporaryFiles; @@ -2636,13 +2714,16 @@ static int KeplerFormalMainImpl( constructor.config_.preprocessEnabled_ = verilogPreprocessing; constructor.construct(toPathVector(designPaths)); } - auto top = useSystemVerilog - ? SNLUtils::findTop(designLibrary) - : selectTopDesign( - designLibrary, - designIndex == 0 ? verilogTopOptions.design0 - : verilogTopOptions.design1, - designIndex); + auto top = useVhdl + ? vhdlTop + : useSystemVerilog + ? SNLUtils::findTop(designLibrary) + : selectTopDesign( + designLibrary, + designIndex == 0 + ? verilogTopOptions.design0 + : verilogTopOptions.design1, + designIndex); if (!top) { // LCOV_EXCL_START // LCOV_DISABLED_START @@ -2854,7 +2935,7 @@ static int KeplerFormalMainImpl( inputFormatType == FormatType::SYSTEMVERILOG, designInputs, systemVerilogOptions, - verilogTopOptions, + useVhdl ? vhdlTopOptions : verilogTopOptions, boundaryPairs)) { // CVA6-style smoke runs often compare a design against itself. In // compact SEC, extracting that identical second side would require @@ -2941,10 +3022,18 @@ static int KeplerFormalMainImpl( const bool design0UsesSystemVerilog = designUsesSystemVerilog(0); SPDLOG_INFO("Parsing {} file(s) for design 1", // LCOV_EXCL_STOP - design0UsesSystemVerilog ? "systemverilog" : "verilog"); + useVhdl ? "vhdl" + : design0UsesSystemVerilog ? "systemverilog" + : "verilog"); // LCOV_EXCL_START auto designLibrary = NLLibrary::create(db0, NLName("DESIGN")); - if (design0UsesSystemVerilog) { + naja::NL::SNLDesign* vhdlTop = nullptr; + // LCOV_EXCL_STOP + if (useVhdl) { + vhdlTop = constructVhdlDesign( + designLibrary, designInputs.design0, vhdlTopOptions.design0); + // LCOV_EXCL_START + } else if (design0UsesSystemVerilog) { SNLSVConstructor constructor(designLibrary); std::vector temporaryFiles; const auto* sv2vPrimitiveLibraries = @@ -2984,9 +3073,12 @@ static int KeplerFormalMainImpl( constructor.config_.preprocessEnabled_ = verilogPreprocessing; constructor.construct(design0Paths); } - auto top = design0UsesSystemVerilog - ? SNLUtils::findTop(designLibrary) - : selectTopDesign(designLibrary, verilogTopOptions.design0, 0); + auto top = useVhdl + ? vhdlTop + : design0UsesSystemVerilog + ? SNLUtils::findTop(designLibrary) + : selectTopDesign( + designLibrary, verilogTopOptions.design0, 0); if (top) { db0->setTopDesign(top); SPDLOG_INFO("Found top design: {}", top->getString()); @@ -3063,10 +3155,18 @@ static int KeplerFormalMainImpl( const bool design1UsesSystemVerilog = designUsesSystemVerilog(1); SPDLOG_INFO("Parsing {} file(s) for design 2", // LCOV_EXCL_STOP - design1UsesSystemVerilog ? "systemverilog" : "verilog"); + useVhdl ? "vhdl" + : design1UsesSystemVerilog ? "systemverilog" + : "verilog"); // LCOV_EXCL_START auto designLibrary = NLLibrary::create(db1, NLName("DESIGN")); - if (design1UsesSystemVerilog) { + naja::NL::SNLDesign* vhdlTop = nullptr; + // LCOV_EXCL_STOP + if (useVhdl) { + vhdlTop = constructVhdlDesign( + designLibrary, designInputs.design1, vhdlTopOptions.design1); + // LCOV_EXCL_START + } else if (design1UsesSystemVerilog) { SNLSVConstructor constructor(designLibrary); std::vector temporaryFiles; const auto svInputPaths = buildSystemVerilogInputPaths( @@ -3095,9 +3195,12 @@ static int KeplerFormalMainImpl( constructor.config_.preprocessEnabled_ = verilogPreprocessing; constructor.construct(design1Paths); } - auto top = design1UsesSystemVerilog - ? SNLUtils::findTop(designLibrary) - : selectTopDesign(designLibrary, verilogTopOptions.design1, 1); + auto top = useVhdl + ? vhdlTop + : design1UsesSystemVerilog + ? SNLUtils::findTop(designLibrary) + : selectTopDesign( + designLibrary, verilogTopOptions.design1, 1); if (top) { db1->setTopDesign(top); SPDLOG_INFO("Found top design: {}", top->getString()); diff --git a/src/clauses/Tree2BoolExpr.cpp b/src/clauses/Tree2BoolExpr.cpp index c27ac7f5..1ccebf77 100644 --- a/src/clauses/Tree2BoolExpr.cpp +++ b/src/clauses/Tree2BoolExpr.cpp @@ -11,6 +11,7 @@ #include #include #include +#include #include #include #include @@ -527,6 +528,74 @@ BoolExpr* buildGenericTruthTableExpr(const SNLTruthTable& tbl, uint32_t k) { tbl, k, nullptr, naja::DNL::DNLID_MAX); } +// A cube is a product term: `first` selects the inputs it tests and `second` +// gives their required values. +using Cube = std::pair; + +// Wider tables keep one term per row: merging is exponential in the inputs. +constexpr uint32_t kMaxPrimeImplicantInputs = 10; + +// Returns the prime implicants of the table over its relevant inputs. A sum of +// all prime implicants agrees with a sum of rows on 0/1 inputs, and unlike it +// stays exact when an input is unknown in ternary (dual-rail) evaluation: a +// known select decides a mux whatever the unselected input is. +static const std::vector& primeImplicants(const SNLTruthTable& tbl, + uint32_t k) { + thread_local std::vector level, next, primes; + thread_local std::vector merged; + uint64_t relevant = 0; + uint32_t relevantCount = 0; + for (uint32_t j = 0; j < k; ++j) { + if (getRelevantETS(j)) { + relevant |= uint64_t{1} << j; + ++relevantCount; + } + } + const auto sortUnique = [](std::vector& cubes) { + std::sort(cubes.begin(), cubes.end()); + cubes.erase(std::unique(cubes.begin(), cubes.end()), cubes.end()); + }; + level.clear(); + primes.clear(); + const uint64_t rows = uint64_t{1} << k; + for (uint64_t m = 0; m < rows; ++m) { + if (tbl.bits().bit(m)) { + level.emplace_back(relevant, m & relevant); + } + } + sortUnique(level); + if (relevantCount > kMaxPrimeImplicantInputs) { + primes = level; + return primes; + } + while (!level.empty()) { + next.clear(); + merged.assign(level.size(), 0); + for (size_t i = 0; i < level.size(); ++i) { + const auto [care, value] = level[i]; + for (uint64_t bits = care; bits != 0; bits &= bits - 1) { + const uint64_t bit = bits & (~bits + 1); + // Two cubes that differ in one tested input merge into one that + // no longer tests it. + if (std::binary_search(level.begin(), level.end(), + Cube{care, value ^ bit})) { + merged[i] = 1; + next.emplace_back(care & ~bit, value & ~bit); + } + } + } + for (size_t i = 0; i < level.size(); ++i) { + if (!merged[i]) { + primes.push_back(level[i]); + } + } + sortUnique(next); + level.swap(next); + } + std::sort(primes.begin(), primes.end()); + return primes; +} + // Frame type used for explicit stack-based post-order traversal. // Each frame holds a pointer to a node and a boolean indicating whether // the node has been visited (post-visit) or not (pre-visit). @@ -725,23 +794,18 @@ BoolExpr* Tree2BoolExpr::convert( // The algorithm expects at least one relevant input for a PI node. assert(numRelIdx > 0 && "No relevant inputs for node"); { - // Build DNF terms by iterating over rows where the table output is 1. - // For each such row, create a conjunction of literals for relevant inputs. + // Build DNF terms from the prime implicants of the table. + // For each one, create a conjunction of literals for the inputs it tests. clearTermsETS(); - for (uint64_t m = 0; m < rows; ++m) { - if (!tbl.bits().bit(m)) { - continue; - } + for (const auto& [care, m] : primeImplicants(tbl, k)) { BoolExpr* term = nullptr; bool firstLit = true; BoolExpr* lit = nullptr; - // For each relevant input, pick the literal (child or its negation) - // according to the bit value in row m. + // For each tested input, pick the literal (child or its negation) + // according to its required value. for (uint32_t j = 0; j < k; ++j) { - if (!getRelevantETS(j)) { - // LCOV_EXCL_START - continue; // LCOV_EXCL_LINE - // LCOV_EXCL_STOP + if (((care >> j) & 1) == 0) { + continue; } bool bit1 = ((m >> j) & 1) != 0; lit = bit1 ? getChildFETS(j) : BoolExpr::Not(getChildFETS(j)); diff --git a/src/sec/kinduction/BaseCaseSolver.cpp b/src/sec/kinduction/BaseCaseSolver.cpp index 6a410fdf..da272dce 100644 --- a/src/sec/kinduction/BaseCaseSolver.cpp +++ b/src/sec/kinduction/BaseCaseSolver.cpp @@ -1399,7 +1399,8 @@ std::optional findBaseCounterexampleImp std::optional exactPublicBadFrame, bool localizeMultiOutputFrontier = true, BaseCaseSolverProfile solverProfile = BaseCaseSolverProfile::SecConeProof, - SATSolverWrapper::SolveStatus* solveStatusOut = nullptr); + SATSolverWrapper::SolveStatus* solveStatusOut = nullptr, + bool assumeResetFrontierProperty = true); // LCOV_EXCL_START KInductionProblem makeSingleObservedOutputProblem( // LCOV_EXCL_LINE @@ -1585,7 +1586,8 @@ std::optional findBaseCounterexampleImp std::optional exactPublicBadFrame, bool localizeMultiOutputFrontier, BaseCaseSolverProfile solverProfile, - SATSolverWrapper::SolveStatus* solveStatusOut) { + SATSolverWrapper::SolveStatus* solveStatusOut, + bool assumeResetFrontierProperty) { if (solveStatusOut != nullptr) { *solveStatusOut = SATSolverWrapper::SolveStatus::Unsat; } @@ -1599,7 +1601,8 @@ std::optional findBaseCounterexampleImp const size_t bootstrapFrames = resetBootstrapFrames(problem); const bool resetBootstrapObservationFrontier = - bootstrapFrames != 0 && problem.usesResetBootstrapObservationFrontier(); + assumeResetFrontierProperty && bootstrapFrames != 0 && + problem.usesResetBootstrapObservationFrontier(); const size_t internalK = k + bootstrapFrames; // Base BMC only needs to assert the requested bad frame(s). For frontier // sweeps, earlier depths are checked by the caller; for cumulative base @@ -2218,6 +2221,31 @@ bool baseCaseValidationUsesLocalQueryProfile( solverType == KEPLER_FORMAL::Config::SolverType::KISSAT; } +std::optional +findResetFrontierMismatch(const KInductionProblem& problem, + KEPLER_FORMAL::Config::SolverType solverType) { + if (resetBootstrapFrames(problem) == 0 || + !problem.usesResetBootstrapObservationFrontier()) { + return std::nullopt; + } + // Ask whether any reset trace lets the outputs agree on the frontier frame. + KInductionProblem agreeing = problem; + agreeing.bad = problem.property; + SATSolverWrapper::SolveStatus status = SATSolverWrapper::SolveStatus::Unknown; + findBaseCounterexampleImpl( + agreeing, solverType, 0, 0, /*localizeMultiOutputFrontier=*/false, + BaseCaseSolverProfile::PdrValidationProofOnly, &status, + /*assumeResetFrontierProperty=*/false); + if (status != SATSolverWrapper::SolveStatus::Unsat) { + return std::nullopt; + } + // None does, so every reset trace is a mismatch on that frame. + return findBaseCounterexampleImpl( + problem, solverType, 0, 0, /*localizeMultiOutputFrontier=*/false, + BaseCaseSolverProfile::SecConeProof, nullptr, + /*assumeResetFrontierProperty=*/false); +} + std::optional findBaseCounterexample( const KInductionProblem& problem, KEPLER_FORMAL::Config::SolverType solverType, diff --git a/src/sec/kinduction/BaseCaseSolver.h b/src/sec/kinduction/BaseCaseSolver.h index 37f25a85..9236115c 100644 --- a/src/sec/kinduction/BaseCaseSolver.h +++ b/src/sec/kinduction/BaseCaseSolver.h @@ -52,6 +52,14 @@ std::optional findBaseCounterexample( KEPLER_FORMAL::Config::SolverType solverType, size_t k); +// With an incomplete reset, binary SEC assumes that the outputs agree on the +// first frame after the reset prefix. Returns a counterexample when no reset +// trace can satisfy that assumption, so that a contradictory assumption is +// reported as a mismatch instead of making every later proof vacuous. +std::optional +findResetFrontierMismatch(const KInductionProblem& problem, + KEPLER_FORMAL::Config::SolverType solverType); + // Resource-bounded base proof for localized recovery paths. A true UNSAT // answer is required before an output may be covered; timeout stays Unknown so // callers can conservatively split or skip the hard residual. diff --git a/src/sec/pdr/PDREngine.cpp b/src/sec/pdr/PDREngine.cpp index 840179bf..0005e88d 100644 --- a/src/sec/pdr/PDREngine.cpp +++ b/src/sec/pdr/PDREngine.cpp @@ -5356,7 +5356,9 @@ class PdrTernaryModelReducer { } for (auto& [symbolMap, dependencies] : memoDependenciesBySymbolMap_) { - (void)symbolMap; + // Roots compiled later add parents to nodes shared with earlier roots, + // and propagation visits those parents in every memo. + dependencies.memo = &supportCache_->ternaryEvaluationMemo(symbolMap); for (auto& [mappedSymbol, localSymbols] : dependencies.localSymbolsByMappedSymbol) { (void)mappedSymbol; diff --git a/src/sec/strategy/SequentialEquivalenceStrategy.cpp b/src/sec/strategy/SequentialEquivalenceStrategy.cpp index 82956fb4..24e24167 100644 --- a/src/sec/strategy/SequentialEquivalenceStrategy.cpp +++ b/src/sec/strategy/SequentialEquivalenceStrategy.cpp @@ -3884,6 +3884,17 @@ SequentialEquivalenceResult SequentialEquivalenceStrategy::runExtractedModels( fflush(stderr); } + if (auto witness = SEC::findResetFrontierMismatch(proofProblem, solverType_)) { + const KInductionResult mismatch{ + KInductionStatus::Different, 0, std::move(witness)}; + return makeSecResult( + SequentialEquivalenceStatus::Different, + 0, + formatCounterexampleWitness(mismatch, model0, model1, top0_, top1_), + aligned.outputCoverage, + extractedBoundaryReports); + } + return runSelectedSecEngine( secEngine_, proofProblem, diff --git a/test/strategies/miter/KeplerFormalCliTests.cpp b/test/strategies/miter/KeplerFormalCliTests.cpp index a5d1dc00..66ae30c2 100644 --- a/test/strategies/miter/KeplerFormalCliTests.cpp +++ b/test/strategies/miter/KeplerFormalCliTests.cpp @@ -1946,6 +1946,319 @@ TEST_F(KeplerFormalCliTests, ConfigSystemVerilogLecRejected) { std::filesystem::remove_all(fixture.tmpDir); } +namespace { + +const char* const kVhdlRegister = + "entity top is\n" + " port (clk, rst, en, d : in bit; q : out bit);\n" + "end;\n" + "architecture rtl of top is\n" + "begin\n" + " process(clk) begin\n" + " if rising_edge(clk) then\n" + " if rst = '1' then\n" + " q <= '0';\n" + " elsif en = '1' then\n" + " q <= d;\n" + " end if;\n" + " end if;\n" + " end process;\n" + "end;\n"; + +const char* const kVhdlInvertedRegister = + "entity top is\n" + " port (clk, rst, en, d : in bit; q : out bit);\n" + "end;\n" + "architecture rtl of top is\n" + "begin\n" + " process(clk) begin\n" + " if rising_edge(clk) then\n" + " if rst = '1' then\n" + " q <= '0';\n" + " elsif en = '1' then\n" + " q <= not d;\n" + " end if;\n" + " end if;\n" + " end process;\n" + "end;\n"; + +std::string vhdlSecConfig(const SimpleCliFixture& fixture) { + // The default dual-rail encoding proves registers without a reset bootstrap. + return "format: vhdl\n" + "verification: sec\n" + "max_k: 4\n" + "input_paths:\n" + " - " + fixture.design0Path.string() + "\n" + " - " + fixture.design1Path.string() + "\n"; +} + +} // namespace + +TEST_F(KeplerFormalCliTests, ConfigVhdlProvesRewrittenLogicEquivalent) { + const auto fixture = createDesignFixture( + "vhd", + "entity top is\n" + " port (a, b, c : in bit; y : out bit);\n" + "end;\n" + "architecture rtl of top is\n" + "begin\n" + " y <= not (a and b) xor c;\n" + "end;\n", + "entity top is\n" + " port (a, b, c : in bit; y : out bit);\n" + "end;\n" + "architecture rtl of top is\n" + "begin\n" + " y <= ((not a) or (not b)) xor c;\n" + "end;\n"); + const auto cfgPath = writeTempConfig(vhdlSecConfig(fixture)); + const auto run = runStructuredWithConfigFile(cfgPath); + EXPECT_EQ(run.exitCode, EXIT_SUCCESS); + EXPECT_EQ(run.result.status, KEPLER_FORMAL::RunStatus::Equivalent); + EXPECT_EQ(run.result.inputFormat, "vhdl"); + std::filesystem::remove(cfgPath); + std::filesystem::remove_all(fixture.tmpDir); +} + +TEST_F(KeplerFormalCliTests, ConfigVhdlProvesRegistersEquivalent) { + const auto fixture = createEquivalentDesignFixture("vhd", kVhdlRegister); + const auto cfgPath = writeTempConfig(vhdlSecConfig(fixture)); + const auto run = runStructuredWithConfigFile(cfgPath); + EXPECT_EQ(run.exitCode, EXIT_SUCCESS); + EXPECT_EQ(run.result.status, KEPLER_FORMAL::RunStatus::Equivalent); + std::filesystem::remove(cfgPath); + std::filesystem::remove_all(fixture.tmpDir); +} + +TEST_F(KeplerFormalCliTests, ConfigVhdlFindsRegisterDifference) { + const auto fixture = + createDesignFixture("vhd", kVhdlRegister, kVhdlInvertedRegister); + const auto cfgPath = writeTempConfig(vhdlSecConfig(fixture)); + const auto run = runStructuredWithConfigFile(cfgPath); + EXPECT_NE(run.exitCode, EXIT_SUCCESS); + EXPECT_EQ(run.result.status, KEPLER_FORMAL::RunStatus::Different); + std::filesystem::remove(cfgPath); + std::filesystem::remove_all(fixture.tmpDir); +} + +TEST_F(KeplerFormalCliTests, ConfigVhdlLecRejected) { + const auto fixture = createEquivalentDesignFixture("vhd", kVhdlRegister); + const auto cfgPath = writeTempConfig( + "format: vhdl\n" + "input_paths:\n" + " - " + fixture.design0Path.string() + "\n" + " - " + fixture.design1Path.string() + "\n"); + int rc = runWithConfigFile(cfgPath); + EXPECT_NE(rc, EXIT_SUCCESS); + std::filesystem::remove(cfgPath); + std::filesystem::remove_all(fixture.tmpDir); +} + +TEST_F(KeplerFormalCliTests, ConfigVhdlTopRejectedForOtherFormats) { + const auto fixture = createEquivalentDesignFixture( + "v", + "module top(input a, output y);\n" + " assign y = a;\n" + "endmodule\n"); + const auto cfgPath = writeTempConfig( + "format: verilog\n" + "vhdl_design1_top: top\n" + "input_paths:\n" + " - " + fixture.design0Path.string() + "\n" + " - " + fixture.design1Path.string() + "\n"); + int rc = runWithConfigFile(cfgPath); + EXPECT_NE(rc, EXIT_SUCCESS); + std::filesystem::remove(cfgPath); + std::filesystem::remove_all(fixture.tmpDir); +} + +TEST_F(KeplerFormalCliTests, CliVhdlMultiFileHierarchyMatchesFlatDesign) { + SimpleCliFixture fixture; + fixture.tmpDir = makeUniqueTempDir("kepler_formal_cli_vhdl_hierarchy"); + const auto leafPath = fixture.tmpDir / "leaf.vhd"; + fixture.design0Path = fixture.tmpDir / "design0_top.vhd"; + fixture.design1Path = fixture.tmpDir / "design1.vhd"; + { + std::ofstream leaf(leafPath); + leaf << "entity inv4 is\n" + " port (a : in bit_vector(3 downto 0);\n" + " y : out bit_vector(3 downto 0));\n" + "end;\n" + "architecture rtl of inv4 is\n" + "begin\n" + " y <= not a;\n" + "end;\n"; + } + { + std::ofstream design0(fixture.design0Path); + design0 << "entity htop is\n" + " port (a : in bit_vector(3 downto 0);\n" + " y : out bit_vector(3 downto 0));\n" + "end;\n" + "architecture structural of htop is\n" + " signal mid : bit_vector(3 downto 0);\n" + "begin\n" + " u0: entity work.inv4 port map(a, mid);\n" + " u1: entity work.inv4 port map(mid, y);\n" + "end;\n"; + } + { + std::ofstream design1(fixture.design1Path); + design1 << "entity htop is\n" + " port (a : in bit_vector(3 downto 0);\n" + " y : out bit_vector(3 downto 0));\n" + "end;\n" + "architecture rtl of htop is\n" + "begin\n" + " y <= a;\n" + "end;\n"; + } + + // Files are loaded in compile order, so the instantiated entity comes first. + const auto run = runStructuredWithArgs( + {"kepler-formal", "-vhdl", "-v", "sec", + "--vhdl_design1_top", "htop", "--vhdl_design2_top", "htop", + "--design1", leafPath.string(), fixture.design0Path.string(), + "--design2", fixture.design1Path.string()}); + EXPECT_EQ(run.exitCode, EXIT_SUCCESS); + EXPECT_EQ(run.result.status, KEPLER_FORMAL::RunStatus::Equivalent); + + const auto wrongOrder = runStructuredWithArgs( + {"kepler-formal", "-vhdl", "-v", "sec", + "--design1", fixture.design0Path.string(), leafPath.string(), + "--design2", fixture.design1Path.string()}); + EXPECT_NE(wrongOrder.exitCode, EXIT_SUCCESS); + EXPECT_NE(wrongOrder.result.status, KEPLER_FORMAL::RunStatus::Equivalent); + + std::filesystem::remove_all(fixture.tmpDir); +} + +TEST_F(KeplerFormalCliTests, CliVhdlCompactModeFindsRegisterDifference) { + const auto fixture = + createDesignFixture("vhd", kVhdlRegister, kVhdlInvertedRegister); + const auto run = runStructuredWithArgs( + {"kepler-formal", "-vhdl", "-v", "sec", + "--compact", + "--design1", fixture.design0Path.string(), + "--design2", fixture.design1Path.string()}); + EXPECT_NE(run.exitCode, EXIT_SUCCESS); + EXPECT_EQ(run.result.status, KEPLER_FORMAL::RunStatus::Different); + std::filesystem::remove_all(fixture.tmpDir); +} + +TEST_F(KeplerFormalCliTests, CliVhdlReportsLoadFailures) { + const auto fixture = createDesignFixture( + "vhd", + "entity top is\n" + " port (a : in bit; y : out bit)\n" + "end;\n", + kVhdlRegister); + const auto syntaxError = runStructuredWithArgs( + {"kepler-formal", "-vhdl", "-v", "sec", + "--design1", fixture.design0Path.string(), + "--design2", fixture.design1Path.string()}); + EXPECT_NE(syntaxError.exitCode, EXIT_SUCCESS); + EXPECT_NE(syntaxError.result.status, KEPLER_FORMAL::RunStatus::Equivalent); + + const auto unknownTop = runStructuredWithArgs( + {"kepler-formal", "-vhdl", "-v", "sec", + "--vhdl_design2_top", "missing_top", + "--design1", fixture.design1Path.string(), + "--design2", fixture.design1Path.string()}); + EXPECT_NE(unknownTop.exitCode, EXIT_SUCCESS); + EXPECT_NE(unknownTop.result.status, KEPLER_FORMAL::RunStatus::Equivalent); + + std::filesystem::remove_all(fixture.tmpDir); +} + +namespace { + +// A 4-bit register that resets through a mux and only depends on itself. +std::string vhdlSelfFeedingRegister(const std::string& resetValue, + const std::string& feedback) { + return "library ieee;\n" + "use ieee.std_logic_1164.all;\n" + "entity top is\n" + " port (clk, rst : in std_logic;\n" + " q : out std_logic_vector(3 downto 0));\n" + "end;\n" + "architecture rtl of top is\n" + " signal t : std_logic_vector(3 downto 0);\n" + "begin\n" + " q <= t;\n" + " process (clk) begin\n" + " if rising_edge(clk) then\n" + " if rst = '1' then\n" + " t <= \"" + resetValue + "\";\n" + " else\n" + " t(3) <= " + feedback + ";\n" + " t(2) <= t(3);\n" + " t(1) <= t(2);\n" + " t(0) <= t(1);\n" + " end if;\n" + " end if;\n" + " end process;\n" + "end;\n"; +} + +KEPLER_FORMAL::RunStatus runVhdlSec(const SimpleCliFixture& fixture, + std::vector options) { + std::vector args = {"kepler-formal", "-vhdl", "-v", "sec"}; + args.insert(args.end(), options.begin(), options.end()); + args.insert(args.end(), {"--design1", fixture.design0Path.string(), + "--design2", fixture.design1Path.string()}); + return runStructuredWithArgs(std::move(args)).result.status; +} + +const std::vector kBinaryResetBootstrap = { + "--sec-encoding", "binary", "--sec-reset-cycles", "1", + "--sec-reset-port", "rst=1"}; + +} // namespace + +TEST_F(KeplerFormalCliTests, CliVhdlFindsDifferenceInSelfFeedingRegister) { + // The state is known only if reset decides the mux over an unknown input. + const auto fixture = createDesignFixture( + "vhd", + vhdlSelfFeedingRegister("1111", "t(0)"), + vhdlSelfFeedingRegister("1111", "not t(0)")); + EXPECT_EQ(runVhdlSec(fixture, {}), KEPLER_FORMAL::RunStatus::Different); + std::filesystem::remove_all(fixture.tmpDir); +} + +TEST_F(KeplerFormalCliTests, CliVhdlBinaryResetBootstrapFindsResetMismatch) { + // The outputs cannot agree on the first frame after reset, so assuming that + // they do must not turn into a proof. + const auto fixture = createDesignFixture( + "vhd", + vhdlSelfFeedingRegister("1111", "t(0)"), + vhdlSelfFeedingRegister("0000", "t(0)")); + for (const std::string engine : {"pdr", "k_induction", "imc"}) { + SCOPED_TRACE(engine); + auto options = kBinaryResetBootstrap; + options.insert(options.end(), {"--sec-engine", engine}); + EXPECT_EQ(runVhdlSec(fixture, options), + KEPLER_FORMAL::RunStatus::Different); + } + std::filesystem::remove_all(fixture.tmpDir); +} + +TEST_F(KeplerFormalCliTests, CliVhdlBinaryResetBootstrapPdrFindsDifference) { + // PDR used to read past a ternary evaluation memo on this pair. + const auto fixture = createDesignFixture( + "vhd", + vhdlSelfFeedingRegister("1111", "t(0)"), + vhdlSelfFeedingRegister("1111", "not t(0)")); + EXPECT_EQ(runVhdlSec(fixture, kBinaryResetBootstrap), + KEPLER_FORMAL::RunStatus::Different); + const auto same = createEquivalentDesignFixture( + "vhd", vhdlSelfFeedingRegister("1111", "t(0)")); + EXPECT_EQ(runVhdlSec(same, kBinaryResetBootstrap), + KEPLER_FORMAL::RunStatus::Equivalent); + std::filesystem::remove_all(fixture.tmpDir); + std::filesystem::remove_all(same.tmpDir); +} + TEST_F(KeplerFormalCliTests, ConfigSv2vGateLevelVerilogTopAccepted) { SimpleCliFixture fixture; fixture.tmpDir = makeUniqueTempDir("kepler_formal_cli_sv2v");