From 570b593e6593e41502ae5b0357cc14c7345fa1ba Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Thu, 8 Jan 2026 14:42:24 +0100 Subject: [PATCH 1/9] added capability of verifying the invariants using 1-induction --- .../include/experimental/Analysis/Passes.td | 7 +- .../HandshakeAnnotateProperties.cpp | 10 ++- .../tools/rigidification/rigidification.sh | 2 + .../verify_invariant_annotation.sh | 87 +++++++++++++++++++ tools/export-rtl/export-rtl.cpp | 23 +++-- 5 files changed, 118 insertions(+), 11 deletions(-) create mode 100644 experimental/tools/rigidification/verify_invariant_annotation.sh diff --git a/experimental/include/experimental/Analysis/Passes.td b/experimental/include/experimental/Analysis/Passes.td index c49af6cc2b..4997ede72a 100644 --- a/experimental/include/experimental/Analysis/Passes.td +++ b/experimental/include/experimental/Analysis/Passes.td @@ -26,8 +26,11 @@ def HandshakeAnnotateProperties : DynamaticPass< "handshake-annotate-properties" let constructor = "dynamatic::experimental::formalprop::createAnnotateProperties()"; let options = [ Option<"jsonPath", "json-path", "std::string", "", "Path to JSON-formatted file where the properties' information is stored.">, - Option<"annotateInvariants", "annotate-invariants", "bool", "true", - "Annotate invariants to assist k-inductive proofs">]; + Option<"annotateInvariants", "annotate-invariants", "bool", "false", + "Annotate invariants to assist k-inductive proofs">, + Option<"skipAnnotateProperties", "skip-annotate-properties", "bool", "false", + "Do not annotate properties for optimizations"> + ]; } #endif // EXPERIMENTAL_ANALYSIS_PASSES_TD diff --git a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp index 25bb9275a8..faf01e4d32 100644 --- a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp +++ b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp @@ -156,10 +156,12 @@ HandshakeAnnotatePropertiesPass::annotateEagerForkNotAllOutputSent( void HandshakeAnnotatePropertiesPass::runDynamaticPass() { ModuleOp modOp = getOperation(); - if (failed(annotateAbsenceOfBackpressure(modOp))) - return signalPassFailure(); - if (failed(annotateValidEquivalence(modOp))) - return signalPassFailure(); + if (!skipAnnotateProperties) { + if (failed(annotateAbsenceOfBackpressure(modOp))) + return signalPassFailure(); + if (failed(annotateValidEquivalence(modOp))) + return signalPassFailure(); + } if (annotateInvariants) { if (failed(annotateEagerForkNotAllOutputSent(modOp))) return signalPassFailure(); diff --git a/experimental/tools/rigidification/rigidification.sh b/experimental/tools/rigidification/rigidification.sh index 153fee7443..7b5e52dc62 100644 --- a/experimental/tools/rigidification/rigidification.sh +++ b/experimental/tools/rigidification/rigidification.sh @@ -5,6 +5,8 @@ OUTPUT_DIR=$2 KERNEL_NAME=$3 F_HANDSHAKE_EXPORT=$4 F_HANDSHAKE_RIGIDIFIED=$5 +bash "$DYNAMATIC_DIR/experimental/tools/rigidification/verify_invariant_annotation.sh" $1 $2 $3 $4 $5 +exit $? source "$DYNAMATIC_DIR/tools/dynamatic/scripts/utils.sh" diff --git a/experimental/tools/rigidification/verify_invariant_annotation.sh b/experimental/tools/rigidification/verify_invariant_annotation.sh new file mode 100644 index 0000000000..94946e4c21 --- /dev/null +++ b/experimental/tools/rigidification/verify_invariant_annotation.sh @@ -0,0 +1,87 @@ +#!/bin/bash + +echo "bas" + +DYNAMATIC_DIR=$1 +OUTPUT_DIR=$2 +KERNEL_NAME=$3 +F_HANDSHAKE_EXPORT=$4 +F_HANDSHAKE_RIGIDIFIED=$5 + +source "$DYNAMATIC_DIR/tools/dynamatic/scripts/utils.sh" + +FORMAL_DIR="$OUTPUT_DIR/formal" +MODEL_DIR="$FORMAL_DIR/model" + +DYNAMATIC_OPT_BIN="$DYNAMATIC_DIR/bin/dynamatic-opt" +DYNAMATIC_EXPORT_RTL_BIN="$DYNAMATIC_DIR/bin/export-rtl" + +F_FORMAL_HW="$FORMAL_DIR/hw.mlir" +F_FORMAL_PROP="$FORMAL_DIR/formal_properties.json" +F_NUXMV_PROP="$FORMAL_DIR/property.rpt" +F_NUXMV_CMD="$FORMAL_DIR/prove.cmd" + +NUSMV_BINARY="$DYNAMATIC_DIR/ext/NuSMV" +NUXMV_BINARY="$DYNAMATIC_DIR/ext/nuXmv/bin/nuXmv" + +FORMAL_TESTBENCH_GEN="$DYNAMATIC_DIR/build/bin/rigidification-testbench" + +RTL_CONFIG_SMV="$DYNAMATIC_DIR/data/rtl-config-smv.json" + +SMV_RESULT_PARSER="$DYNAMATIC_DIR/experimental/tools/rigidification/parse_nuxmv_results.py" + + +rm -rf "$FORMAL_DIR" && mkdir -p "$FORMAL_DIR" + + +# Annotate properties +"$DYNAMATIC_OPT_BIN" "$F_HANDSHAKE_EXPORT" \ + --handshake-annotate-properties="json-path=$F_FORMAL_PROP annotate-invariants skip-annotate-properties" \ + > /dev/null + +# handshake level -> hw level +"$DYNAMATIC_OPT_BIN" "$F_HANDSHAKE_EXPORT" --lower-handshake-to-hw \ + > "$F_FORMAL_HW" + +# generate SMV +"$DYNAMATIC_EXPORT_RTL_BIN" \ + "$F_FORMAL_HW" \ + "$MODEL_DIR" \ + "$RTL_CONFIG_SMV" \ + --hdl smv \ + --property-database "$F_FORMAL_PROP" \ + --dynamatic-path "$DYNAMATIC_DIR" + +# create the testbench +"$FORMAL_TESTBENCH_GEN" \ + -i $MODEL_DIR \ + --name $KERNEL_NAME \ + --mlir $F_FORMAL_HW +exit_on_fail "Created formal testbench" \ + "Failed to create formal testbench" + +# use the modelcheker +echo "set verbose_level 0; +set pp_list cpp; +set counter_examples 0; +set dynamic_reorder 1; +set on_failure_script_quits; +set reorder_method sift; +set enable_sexp2bdd_caching 0; +set bdd_static_order_heuristics basic; +set cone_of_influence; +set use_coi_size_sorting 1; +read_model -i $MODEL_DIR/main.smv; +go_bmc; +check_invar_bmc -a classic; +show_property -o $F_NUXMV_PROP; +time; +quit" > $F_NUXMV_CMD +exit_on_fail "Created SMV script" \ + "Failed to create SMV script" + +# run nuXmv and increase the counter everytime it completes the check of a property +echo "[INFO] Running nuXmv" >&2 +$NUXMV_BINARY -source $F_NUXMV_CMD +exit_on_fail "Performed model checking to verify the formal property" \ + "Failed to check formal properties" diff --git a/tools/export-rtl/export-rtl.cpp b/tools/export-rtl/export-rtl.cpp index 61ae489367..bde84549eb 100644 --- a/tools/export-rtl/export-rtl.cpp +++ b/tools/export-rtl/export-rtl.cpp @@ -87,6 +87,11 @@ static cl::opt clEnumValN(HDL::SMV, "smv", "SMV")), cl::cat(mainCategory)); +static cl::opt verifyInvariants( + "verify-invariants", cl::Optional, + cl::desc("generate INVARs as INVARSPEC to verify if they are correct"), + cl::init(false), cl::cat(mainCategory)); + static cl::list rtlConfigs(cl::Positional, cl::OneOrMore, cl::desc(""), cl::cat(mainCategory)); @@ -1131,6 +1136,8 @@ struct SMVWriter : public RTLWriter { /// For example if val is mux0.outs and it is connected to buffer0 thorugh /// the ins port getUserSignal will return buffer0.ins. std::optional getUserSignal(Value val) const; + + bool verifyInvariants = true; }; } // namespace @@ -1386,11 +1393,17 @@ LogicalResult SMVWriter::write(hw::HWModuleOp modOp, os << "\n-- properties\n"; data.writeProperties([](const unsigned long &id, const std::string &property, FormalProperty::TAG tag, raw_indented_ostream &os) { - if (tag == FormalProperty::TAG::OPT) - os << "INVARSPEC NAME p" << id << " := " << property << ";\n"; - else if (tag == FormalProperty::TAG::INVAR) { - os << "-- " << id << "\n"; - os << "INVAR " << property << ";\n"; + if (true) { + if (tag == FormalProperty::TAG::INVAR) { + os << "INVARSPEC NAME p" << id << " := " << property << ";\n"; + } + } else { + if (tag == FormalProperty::TAG::OPT) + os << "INVARSPEC NAME p" << id << " := " << property << ";\n"; + else if (tag == FormalProperty::TAG::INVAR) { + os << "-- " << id << "\n"; + os << "INVAR " << property << ";\n"; + } } }); From 26baa83f0aa70cdac538a9dd965af7992032dd29 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Fri, 9 Jan 2026 15:41:06 +0100 Subject: [PATCH 2/9] added test for verify-annotation --- .../tools/rigidification/rigidification.sh | 12 +++--- .../verify_invariant_annotation.sh | 28 ++++++++----- tools/dynamatic/dynamatic.cpp | 29 +++++++++++-- tools/export-rtl/export-rtl.cpp | 4 +- tools/integration/TEST_SUITE.cpp | 41 +++++++++++++++++++ 5 files changed, 91 insertions(+), 23 deletions(-) mode change 100644 => 100755 experimental/tools/rigidification/verify_invariant_annotation.sh diff --git a/experimental/tools/rigidification/rigidification.sh b/experimental/tools/rigidification/rigidification.sh index 7b5e52dc62..c726916ce9 100644 --- a/experimental/tools/rigidification/rigidification.sh +++ b/experimental/tools/rigidification/rigidification.sh @@ -57,8 +57,8 @@ rm -rf "$FORMAL_DIR" && mkdir -p "$FORMAL_DIR" -i $MODEL_DIR \ --name $KERNEL_NAME \ --mlir $F_FORMAL_HW -exit_on_fail "Created formal testbench" \ - "Failed to create formal testbench" +exit_on_fail "Failed to create formal testbench" \ + "Created formal testbench" # use the modelcheker echo "set verbose_level 0; @@ -81,14 +81,14 @@ check_ctlspec; show_property -o $F_NUXMV_PROP; time; quit" > $F_NUXMV_CMD -exit_on_fail "Created SMV script" \ - "Failed to create SMV script" +exit_on_fail "Failed to create SMV script" \ + "Created SMV script" # run nuXmv and increase the counter everytime it completes the check of a property echo "[INFO] Running nuXmv" >&2 $NUXMV_BINARY -source $F_NUXMV_CMD -exit_on_fail "Performed model checking to verify the formal property" \ - "Failed to check formal properties" +exit_on_fail "Failed to check formal properties" \ + "Performed model checking to verify the formal property" # parse the results printf "\n[INFO] Saving formal verification results\n" >&2 diff --git a/experimental/tools/rigidification/verify_invariant_annotation.sh b/experimental/tools/rigidification/verify_invariant_annotation.sh old mode 100644 new mode 100755 index 94946e4c21..33a3952248 --- a/experimental/tools/rigidification/verify_invariant_annotation.sh +++ b/experimental/tools/rigidification/verify_invariant_annotation.sh @@ -1,12 +1,10 @@ #!/bin/bash -echo "bas" - DYNAMATIC_DIR=$1 OUTPUT_DIR=$2 KERNEL_NAME=$3 -F_HANDSHAKE_EXPORT=$4 -F_HANDSHAKE_RIGIDIFIED=$5 +# F_HANDSHAKE_EXPORT=$4 +F_HANDSHAKE_EXPORT="$OUTPUT_DIR/comp/handshake_export.mlir" source "$DYNAMATIC_DIR/tools/dynamatic/scripts/utils.sh" @@ -50,6 +48,7 @@ rm -rf "$FORMAL_DIR" && mkdir -p "$FORMAL_DIR" "$RTL_CONFIG_SMV" \ --hdl smv \ --property-database "$F_FORMAL_PROP" \ + --verify-invariants \ --dynamatic-path "$DYNAMATIC_DIR" # create the testbench @@ -57,8 +56,8 @@ rm -rf "$FORMAL_DIR" && mkdir -p "$FORMAL_DIR" -i $MODEL_DIR \ --name $KERNEL_NAME \ --mlir $F_FORMAL_HW -exit_on_fail "Created formal testbench" \ - "Failed to create formal testbench" +exit_on_fail "Failed to create formal testbench" \ + "Created formal testbench" # use the modelcheker echo "set verbose_level 0; @@ -77,11 +76,18 @@ check_invar_bmc -a classic; show_property -o $F_NUXMV_PROP; time; quit" > $F_NUXMV_CMD -exit_on_fail "Created SMV script" \ - "Failed to create SMV script" +exit_on_fail "Failed to create SMV script" \ + "Created SMV script" +NUXMV_OUT="$FORMAL_DIR/nuxmv.txt" # run nuXmv and increase the counter everytime it completes the check of a property echo "[INFO] Running nuXmv" >&2 -$NUXMV_BINARY -source $F_NUXMV_CMD -exit_on_fail "Performed model checking to verify the formal property" \ - "Failed to check formal properties" +$NUXMV_BINARY -source $F_NUXMV_CMD > $NUXMV_OUT +exit_on_fail "Failed to check formal properties" \ + "Performed model checking to verify the invariants" \ + +# parse the results +NUM_FAILED=$(cat $NUXMV_OUT | grep -c "^-- .*the induction fails$") +test $NUM_FAILED == 0 +exit_on_fail "At least one invariant was not verifiable" \ + "All properties provable by 1-induction" diff --git a/tools/dynamatic/dynamatic.cpp b/tools/dynamatic/dynamatic.cpp index eee7b726a2..92f14c3f37 100644 --- a/tools/dynamatic/dynamatic.cpp +++ b/tools/dynamatic/dynamatic.cpp @@ -97,7 +97,6 @@ struct FrontendState { std::optional sourcePath = std::nullopt; std::string outputDir = "out"; - FrontendState(StringRef cwd) : cwd(cwd), dynamaticPath(cwd) {}; bool sourcePathIsSet(StringRef keyword); @@ -268,13 +267,24 @@ class SetCP : public Command { class SetOutputDir : public Command { public: SetOutputDir(FrontendState &state) - : Command("set-output-dir", "Sets the name of the dir to perform HLS in. If not set, defaults to 'out'", state) { + : Command("set-output-dir", + "Sets the name of the dir to perform HLS in. If not set, " + "defaults to 'out'", + state) { addPositionalArg({"out_dir", "out dir name"}); } CommandResult execute(CommandArguments &args) override; }; +class VerifyInvariants : public Command { +public: + VerifyInvariants(FrontendState &state) + : Command("verify-invariants", + "Verifies the correctness of invariants generated", state) {} + + CommandResult execute(CommandArguments &args) override; +}; class Compile : public Command { public: @@ -646,7 +656,8 @@ CommandResult SetOutputDir::execute(CommandArguments &args) { llvm::StringRef outputDir = args.positionals.front(); // reject trivial bad cases - if (outputDir.empty() || outputDir == "." || outputDir == ".." || outputDir.endswith("/")) + if (outputDir.empty() || outputDir == "." || outputDir == ".." || + outputDir.endswith("/")) return CommandResult::FAIL; // reject illegal chars @@ -671,6 +682,17 @@ CommandResult SetCP::execute(CommandArguments &args) { return CommandResult::FAIL; } +CommandResult VerifyInvariants::execute(CommandArguments &args) { + if (!state.sourcePathIsSet(keyword)) + return CommandResult::FAIL; + + std::string script = + state.dynamaticPath + getSeparator() + + "experimental/tools/rigidification/verify_invariant_annotation.sh"; + + return execCmd(script, state.dynamaticPath, state.getOutputDir(), state.getKernelName()); +} + CommandResult Compile::execute(CommandArguments &args) { // We need the source path to be set if (!state.sourcePathIsSet(keyword)) @@ -871,6 +893,7 @@ int main(int argc, char **argv) { commands.add(state); commands.add(state); commands.add(state); + commands.add(state); commands.add(state); commands.add(state); commands.add(state); diff --git a/tools/export-rtl/export-rtl.cpp b/tools/export-rtl/export-rtl.cpp index bde84549eb..171491ecb6 100644 --- a/tools/export-rtl/export-rtl.cpp +++ b/tools/export-rtl/export-rtl.cpp @@ -1136,8 +1136,6 @@ struct SMVWriter : public RTLWriter { /// For example if val is mux0.outs and it is connected to buffer0 thorugh /// the ins port getUserSignal will return buffer0.ins. std::optional getUserSignal(Value val) const; - - bool verifyInvariants = true; }; } // namespace @@ -1393,7 +1391,7 @@ LogicalResult SMVWriter::write(hw::HWModuleOp modOp, os << "\n-- properties\n"; data.writeProperties([](const unsigned long &id, const std::string &property, FormalProperty::TAG tag, raw_indented_ostream &os) { - if (true) { + if (verifyInvariants) { if (tag == FormalProperty::TAG::INVAR) { os << "INVARSPEC NAME p" << id << " := " << property << ";\n"; } diff --git a/tools/integration/TEST_SUITE.cpp b/tools/integration/TEST_SUITE.cpp index cbafa8021a..f4f13ec87a 100644 --- a/tools/integration/TEST_SUITE.cpp +++ b/tools/integration/TEST_SUITE.cpp @@ -386,6 +386,47 @@ INSTANTIATE_TEST_SUITE_P(SpecBenchmarks, SpecFixture, ), [](const auto &info) { return "spec_" + info.param; }); +INSTANTIATE_TEST_SUITE_P(Tiny, RigidificationFixture, + testing::Values( + "fir", + "iir", + "matvec" + ), + [](const auto &info) { return info.param; }); + +TEST_P(RigidificationFixture, basic) { + std::string name = GetParam(); + fs::path cSourcePath = + fs::path(DYNAMATIC_ROOT) / "integration-test" / name / (name + ".c"); + std::string tmpFilename = "tmp_" + GetParam() + ".dyn"; + std::ofstream scriptFile(tmpFilename); + if (!scriptFile.is_open()) { + std::cout << "[ERROR] Failed to create .dyn script file" << std::endl; + EXPECT_EQ(0, -1); + } + scriptFile << "set-dynamatic-path " << DYNAMATIC_ROOT << std::endl + << "set-src " << cSourcePath.string() << std::endl + << "compile" << std::endl + << "verify-invariants" << std::endl + << "exit" << std::endl; + scriptFile.close(); + + fs::path dynamaticPath = fs::path(DYNAMATIC_ROOT) / "bin" / "dynamatic"; + fs::path dynamaticOutPath = + cSourcePath.parent_path() / "out" / "dynamatic_out.txt"; + fs::path dynamaticErrPath = + cSourcePath.parent_path() / "out" / "dynamatic_err.txt"; + std::string cmd = dynamaticPath.string() + " --exit-on-failure --run "; + cmd += tmpFilename; + cmd += " 1> "; + cmd += dynamaticOutPath; + cmd += " 2> "; + cmd += dynamaticErrPath; + + int status = system(cmd.c_str()); + EXPECT_EQ(status, 0); +} + // Smoke test: Using the CBC MILP solver to optimize some simple benchmarks // clang-format on From bc0f8e6051570e7f704415cb870316e2b7c8d38b Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Fri, 9 Jan 2026 16:08:30 +0100 Subject: [PATCH 3/9] formatting --- tools/dynamatic/dynamatic.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/tools/dynamatic/dynamatic.cpp b/tools/dynamatic/dynamatic.cpp index 92f14c3f37..5244bfb88a 100644 --- a/tools/dynamatic/dynamatic.cpp +++ b/tools/dynamatic/dynamatic.cpp @@ -690,7 +690,8 @@ CommandResult VerifyInvariants::execute(CommandArguments &args) { state.dynamaticPath + getSeparator() + "experimental/tools/rigidification/verify_invariant_annotation.sh"; - return execCmd(script, state.dynamaticPath, state.getOutputDir(), state.getKernelName()); + return execCmd(script, state.dynamaticPath, state.getOutputDir(), + state.getKernelName()); } CommandResult Compile::execute(CommandArguments &args) { From 6dbd0ce21513ff0c74ff44037bdd2249019a6a20 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Wed, 14 Jan 2026 13:39:57 +0100 Subject: [PATCH 4/9] gave the verify-invariants test a name, and moved it into ENABLE-LEQ-BINARIES --- .../include/experimental/Analysis/Passes.td | 2 +- .../HandshakeAnnotateProperties.cpp | 2 +- .../tools/rigidification/rigidification.sh | 2 -- tools/integration/TEST_SUITE.cpp | 29 +++++++++---------- 4 files changed, 15 insertions(+), 20 deletions(-) diff --git a/experimental/include/experimental/Analysis/Passes.td b/experimental/include/experimental/Analysis/Passes.td index 4997ede72a..5d99e5c4c4 100644 --- a/experimental/include/experimental/Analysis/Passes.td +++ b/experimental/include/experimental/Analysis/Passes.td @@ -28,7 +28,7 @@ def HandshakeAnnotateProperties : DynamaticPass< "handshake-annotate-properties" "Path to JSON-formatted file where the properties' information is stored.">, Option<"annotateInvariants", "annotate-invariants", "bool", "false", "Annotate invariants to assist k-inductive proofs">, - Option<"skipAnnotateProperties", "skip-annotate-properties", "bool", "false", + Option<"annotateProperties", "annotate-properties", "bool", "true", "Do not annotate properties for optimizations"> ]; } diff --git a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp index faf01e4d32..2d3a911cab 100644 --- a/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp +++ b/experimental/lib/Analysis/FormalPropertyAnnotation/HandshakeAnnotateProperties.cpp @@ -156,7 +156,7 @@ HandshakeAnnotatePropertiesPass::annotateEagerForkNotAllOutputSent( void HandshakeAnnotatePropertiesPass::runDynamaticPass() { ModuleOp modOp = getOperation(); - if (!skipAnnotateProperties) { + if (annotateProperties) { if (failed(annotateAbsenceOfBackpressure(modOp))) return signalPassFailure(); if (failed(annotateValidEquivalence(modOp))) diff --git a/experimental/tools/rigidification/rigidification.sh b/experimental/tools/rigidification/rigidification.sh index c726916ce9..33ba4b161f 100644 --- a/experimental/tools/rigidification/rigidification.sh +++ b/experimental/tools/rigidification/rigidification.sh @@ -5,8 +5,6 @@ OUTPUT_DIR=$2 KERNEL_NAME=$3 F_HANDSHAKE_EXPORT=$4 F_HANDSHAKE_RIGIDIFIED=$5 -bash "$DYNAMATIC_DIR/experimental/tools/rigidification/verify_invariant_annotation.sh" $1 $2 $3 $4 $5 -exit $? source "$DYNAMATIC_DIR/tools/dynamatic/scripts/utils.sh" diff --git a/tools/integration/TEST_SUITE.cpp b/tools/integration/TEST_SUITE.cpp index f4f13ec87a..ff6dae28aa 100644 --- a/tools/integration/TEST_SUITE.cpp +++ b/tools/integration/TEST_SUITE.cpp @@ -50,6 +50,7 @@ class SharingUnitTestFixture : public BaseFixture {}; class SpecFixture : public BaseFixture {}; class RigidificationFixture : public BaseFixture {}; +class VerifyInvariantsFixture : public BaseFixture {}; TEST_P(BasicFixture, basic) { IntegrationTestData config{ @@ -386,18 +387,19 @@ INSTANTIATE_TEST_SUITE_P(SpecBenchmarks, SpecFixture, ), [](const auto &info) { return "spec_" + info.param; }); -INSTANTIATE_TEST_SUITE_P(Tiny, RigidificationFixture, - testing::Values( - "fir", - "iir", - "matvec" - ), - [](const auto &info) { return info.param; }); +// Smoke test: Using the CBC MILP solver to optimize some simple benchmarks +// clang-format on -TEST_P(RigidificationFixture, basic) { +#ifdef DYNAMATIC_ENABLE_LEQ_BINARIES + +INSTANTIATE_TEST_SUITE_P(Tiny, VerifyInvariantsFixture, + testing::Values("fir", "iir", "matvec"), + [](const auto &info) { return info.param; }); + +TEST_P(VerifyInvariantsFixture, basic) { std::string name = GetParam(); fs::path cSourcePath = - fs::path(DYNAMATIC_ROOT) / "integration-test" / name / (name + ".c"); + fs::path(DYNAMATIC_ROOT) / "integration-test" / name / (name + ".c"); std::string tmpFilename = "tmp_" + GetParam() + ".dyn"; std::ofstream scriptFile(tmpFilename); if (!scriptFile.is_open()) { @@ -413,9 +415,9 @@ TEST_P(RigidificationFixture, basic) { fs::path dynamaticPath = fs::path(DYNAMATIC_ROOT) / "bin" / "dynamatic"; fs::path dynamaticOutPath = - cSourcePath.parent_path() / "out" / "dynamatic_out.txt"; + cSourcePath.parent_path() / "out" / "dynamatic_out.txt"; fs::path dynamaticErrPath = - cSourcePath.parent_path() / "out" / "dynamatic_err.txt"; + cSourcePath.parent_path() / "out" / "dynamatic_err.txt"; std::string cmd = dynamaticPath.string() + " --exit-on-failure --run "; cmd += tmpFilename; cmd += " 1> "; @@ -427,11 +429,6 @@ TEST_P(RigidificationFixture, basic) { EXPECT_EQ(status, 0); } -// Smoke test: Using the CBC MILP solver to optimize some simple benchmarks -// clang-format on - -#ifdef DYNAMATIC_ENABLE_LEQ_BINARIES - TEST_P(RigidificationFixture, basic) { IntegrationTestData config{ // clang-format off From 00c844a2924d0f0567ef806fd364970feb478da1 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Wed, 14 Jan 2026 14:37:38 +0100 Subject: [PATCH 5/9] parse nuXmv output using python --- .../rigidification/parse_nuxmv_results.py | 18 ++++++++++++++---- .../verify_invariant_annotation.sh | 10 +++++----- 2 files changed, 19 insertions(+), 9 deletions(-) diff --git a/experimental/tools/rigidification/parse_nuxmv_results.py b/experimental/tools/rigidification/parse_nuxmv_results.py index 4a3a05ea41..0b9792d31b 100644 --- a/experimental/tools/rigidification/parse_nuxmv_results.py +++ b/experimental/tools/rigidification/parse_nuxmv_results.py @@ -11,7 +11,7 @@ def to_bool(val: str): return None -def parse_nuxmv(json_file, nuxmv_file): +def parse_nuxmv(json_file, nuxmv_file, detect_unproven): with open(json_file, 'r') as f: json_data = json.load(f) @@ -31,9 +31,17 @@ def parse_nuxmv(json_file, nuxmv_file): for line in nuXmv_lines: if re.search(id_pattern, line): status_match = re.search(result_pattern, line) + if not status_match: + continue + result = to_bool(status_match.group(1)) + + # if a match is found and we only want to detect unproven properties, exit when the property is unproven + if detect_unproven and result != True: + exit(1) + # if a match is found update the object only if needed (the new value is different from the old one) - if status_match and obj["check"] != to_bool(status_match.group(1)): - obj["check"] = to_bool(status_match.group(1)) + if obj["check"] != result: + obj["check"] = result updated = True break @@ -48,6 +56,8 @@ def parse_nuxmv(json_file, nuxmv_file): parser.add_argument("json_file", help="Path to the JSON file to update.") parser.add_argument( "nuxmv_file", help="Path to the file generated by nuXmv.") + parser.add_argument("-d", "--detect-unproven", dest="detect_unproven", + action="store_true", help="Exit when a property has not been checked.") args = parser.parse_args() - parse_nuxmv(args.json_file, args.nuxmv_file) + parse_nuxmv(args.json_file, args.nuxmv_file, args.detect_unproven) diff --git a/experimental/tools/rigidification/verify_invariant_annotation.sh b/experimental/tools/rigidification/verify_invariant_annotation.sh index 33a3952248..d493d71793 100755 --- a/experimental/tools/rigidification/verify_invariant_annotation.sh +++ b/experimental/tools/rigidification/verify_invariant_annotation.sh @@ -34,7 +34,7 @@ rm -rf "$FORMAL_DIR" && mkdir -p "$FORMAL_DIR" # Annotate properties "$DYNAMATIC_OPT_BIN" "$F_HANDSHAKE_EXPORT" \ - --handshake-annotate-properties="json-path=$F_FORMAL_PROP annotate-invariants skip-annotate-properties" \ + --handshake-annotate-properties="json-path=$F_FORMAL_PROP annotate-invariants annotate-properties=false" \ > /dev/null # handshake level -> hw level @@ -86,8 +86,8 @@ $NUXMV_BINARY -source $F_NUXMV_CMD > $NUXMV_OUT exit_on_fail "Failed to check formal properties" \ "Performed model checking to verify the invariants" \ -# parse the results -NUM_FAILED=$(cat $NUXMV_OUT | grep -c "^-- .*the induction fails$") -test $NUM_FAILED == 0 +# parse and check the results +printf "\n[INFO] Saving formal verification results\n" >&2 +python "$SMV_RESULT_PARSER" "$F_FORMAL_PROP" "$F_NUXMV_PROP" exit_on_fail "At least one invariant was not verifiable" \ - "All properties provable by 1-induction" + "All properties proven by 1-induction" From 9fed41399f5dcf37542eab85d3078c664b0aa228 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Wed, 14 Jan 2026 16:57:07 +0100 Subject: [PATCH 6/9] combined verify-invariants into rigidification script --- .../tools/rigidification/rigidification.sh | 88 +++++++++++++------ .../verify_invariant_annotation.sh | 67 +++++++++----- tools/dynamatic/dynamatic.cpp | 10 ++- 3 files changed, 115 insertions(+), 50 deletions(-) mode change 100644 => 100755 experimental/tools/rigidification/rigidification.sh diff --git a/experimental/tools/rigidification/rigidification.sh b/experimental/tools/rigidification/rigidification.sh old mode 100644 new mode 100755 index 33ba4b161f..3847547c8e --- a/experimental/tools/rigidification/rigidification.sh +++ b/experimental/tools/rigidification/rigidification.sh @@ -28,13 +28,62 @@ RTL_CONFIG_SMV="$DYNAMATIC_DIR/data/rtl-config-smv.json" SMV_RESULT_PARSER="$DYNAMATIC_DIR/experimental/tools/rigidification/parse_nuxmv_results.py" +for i in $@; do + if [ "$i" = "--verify-invariants" ]; then + VERIFY_INVARIANTS="true" + fi +done + +if [ ! -z $VERIFY_INVARIANTS ]; then + ANNOTATE_FLAGS="annotate-invariants annotate-properties=false" + SMV_GENERATION_FLAGS="--verify-invariants" + RESULT_PARSE_FLAGS="--detect-unproven" + NUXMV_SCRIPT="set verbose_level 0; +set pp_list cpp; +set counter_examples 0; +set dynamic_reorder 1; +set on_failure_script_quits; +set reorder_method sift; +set enable_sexp2bdd_caching 0; +set bdd_static_order_heuristics basic; +set cone_of_influence; +set use_coi_size_sorting 1; +read_model -i $MODEL_DIR/main.smv; +go_bmc; +check_invar_bmc -a classic; +show_property -o $F_NUXMV_PROP; +time; +quit" +else + NUXMV_SCRIPT="set verbose_level 0; +set pp_list cpp; +set counter_examples 0; +set dynamic_reorder 1; +set on_failure_script_quits; +set reorder_method sift; +set enable_sexp2bdd_caching 0; +set bdd_static_order_heuristics basic; +set cone_of_influence; +set use_coi_size_sorting 1; +read_model -i $MODEL_DIR/main.smv; +flatten_hierarchy; +encode_variables; +build_flat_model; +build_model -f; +check_invar -s forward; +check_ctlspec; +show_property -o $F_NUXMV_PROP; +time; +quit" +fi + rm -rf "$FORMAL_DIR" && mkdir -p "$FORMAL_DIR" # Annotate properties "$DYNAMATIC_OPT_BIN" "$F_HANDSHAKE_EXPORT" \ - --handshake-annotate-properties=json-path=$F_FORMAL_PROP \ + --handshake-annotate-properties="json-path=$F_FORMAL_PROP $ANNOTATE_FLAGS" \ > /dev/null # handshake level -> hw level @@ -48,6 +97,7 @@ rm -rf "$FORMAL_DIR" && mkdir -p "$FORMAL_DIR" "$RTL_CONFIG_SMV" \ --hdl smv \ --property-database "$F_FORMAL_PROP" \ + $SMV_GENERATION_FLAGS \ --dynamatic-path "$DYNAMATIC_DIR" # create the testbench @@ -59,26 +109,7 @@ exit_on_fail "Failed to create formal testbench" \ "Created formal testbench" # use the modelcheker -echo "set verbose_level 0; -set pp_list cpp; -set counter_examples 0; -set dynamic_reorder 1; -set on_failure_script_quits; -set reorder_method sift; -set enable_sexp2bdd_caching 0; -set bdd_static_order_heuristics basic; -set cone_of_influence; -set use_coi_size_sorting 1; -read_model -i $MODEL_DIR/main.smv; -flatten_hierarchy; -encode_variables; -build_flat_model; -build_model -f; -check_invar -s forward; -check_ctlspec; -show_property -o $F_NUXMV_PROP; -time; -quit" > $F_NUXMV_CMD +echo $NUXMV_SCRIPT > $F_NUXMV_CMD exit_on_fail "Failed to create SMV script" \ "Created SMV script" @@ -89,11 +120,16 @@ exit_on_fail "Failed to check formal properties" \ "Performed model checking to verify the formal property" # parse the results -printf "\n[INFO] Saving formal verification results\n" >&2 -python "$SMV_RESULT_PARSER" "$F_FORMAL_PROP" "$F_NUXMV_PROP" +printf "\n[INFO] Parsing and saving formal verification results\n" >&2 +python "$SMV_RESULT_PARSER" "$F_FORMAL_PROP" "$F_NUXMV_PROP" $RESULT_PARSE_FLAGS +if [ ! -z $VERIFY_INVARIANTS ]; then + # exit if failed to verify + exit_on_fail "At least one invariant was not verifiable" \ + "All properties proven by 1-induction" + exit 0 +fi # apply rigidification "$DYNAMATIC_OPT_BIN" "$F_HANDSHAKE_EXPORT" --handshake-rigidification=json-path=$F_FORMAL_PROP > "$F_HANDSHAKE_RIGIDIFIED" -exit_on_fail "Applied formal properties to simplify the circuit" \ - "Failed to apply formal properties to simplify the circuit" - + exit_on_fail "Failed to apply formal properties to simplify the circuit" \ + "Applied formal properties to simplify the circuit" diff --git a/experimental/tools/rigidification/verify_invariant_annotation.sh b/experimental/tools/rigidification/verify_invariant_annotation.sh index d493d71793..ddd051a527 100755 --- a/experimental/tools/rigidification/verify_invariant_annotation.sh +++ b/experimental/tools/rigidification/verify_invariant_annotation.sh @@ -28,13 +28,56 @@ RTL_CONFIG_SMV="$DYNAMATIC_DIR/data/rtl-config-smv.json" SMV_RESULT_PARSER="$DYNAMATIC_DIR/experimental/tools/rigidification/parse_nuxmv_results.py" +ONLY_VERIFY=true + +if $ONLY_VERIFY; then + SMV_GENERATION_FLAGS="--verify-invariants" + ANNOTATE_FLAGS="annotate-invariants annotate-properties=false" + NUXMV_SCRIPT="set verbose_level 0; +set pp_list cpp; +set counter_examples 0; +set dynamic_reorder 1; +set on_failure_script_quits; +set reorder_method sift; +set enable_sexp2bdd_caching 0; +set bdd_static_order_heuristics basic; +set cone_of_influence; +set use_coi_size_sorting 1; +read_model -i $MODEL_DIR/main.smv; +go_bmc; +check_invar_bmc -a classic; +show_property -o $F_NUXMV_PROP; +time; +quit" +else + NUXMV_SCRIPT="set verbose_level 0; +set pp_list cpp; +set counter_examples 0; +set dynamic_reorder 1; +set on_failure_script_quits; +set reorder_method sift; +set enable_sexp2bdd_caching 0; +set bdd_static_order_heuristics basic; +set cone_of_influence; +set use_coi_size_sorting 1; +read_model -i $MODEL_DIR/main.smv; +flatten_hierarchy; +encode_variables; +build_flat_model; +build_model -f; +check_invar -s forward; +check_ctlspec; +show_property -o $F_NUXMV_PROP; +time; +quit" +fi rm -rf "$FORMAL_DIR" && mkdir -p "$FORMAL_DIR" # Annotate properties "$DYNAMATIC_OPT_BIN" "$F_HANDSHAKE_EXPORT" \ - --handshake-annotate-properties="json-path=$F_FORMAL_PROP annotate-invariants annotate-properties=false" \ + --handshake-annotate-properties="json-path=$F_FORMAL_PROP $ANNOTATE_FLAGS" \ > /dev/null # handshake level -> hw level @@ -48,7 +91,7 @@ rm -rf "$FORMAL_DIR" && mkdir -p "$FORMAL_DIR" "$RTL_CONFIG_SMV" \ --hdl smv \ --property-database "$F_FORMAL_PROP" \ - --verify-invariants \ + $SMV_GENERATION_FLAGS \ --dynamatic-path "$DYNAMATIC_DIR" # create the testbench @@ -60,29 +103,13 @@ exit_on_fail "Failed to create formal testbench" \ "Created formal testbench" # use the modelcheker -echo "set verbose_level 0; -set pp_list cpp; -set counter_examples 0; -set dynamic_reorder 1; -set on_failure_script_quits; -set reorder_method sift; -set enable_sexp2bdd_caching 0; -set bdd_static_order_heuristics basic; -set cone_of_influence; -set use_coi_size_sorting 1; -read_model -i $MODEL_DIR/main.smv; -go_bmc; -check_invar_bmc -a classic; -show_property -o $F_NUXMV_PROP; -time; -quit" > $F_NUXMV_CMD +echo "$NUXMV_SCRIPT" > $F_NUXMV_CMD exit_on_fail "Failed to create SMV script" \ "Created SMV script" -NUXMV_OUT="$FORMAL_DIR/nuxmv.txt" # run nuXmv and increase the counter everytime it completes the check of a property echo "[INFO] Running nuXmv" >&2 -$NUXMV_BINARY -source $F_NUXMV_CMD > $NUXMV_OUT +$NUXMV_BINARY -source $F_NUXMV_CMD > /dev/null exit_on_fail "Failed to check formal properties" \ "Performed model checking to verify the invariants" \ diff --git a/tools/dynamatic/dynamatic.cpp b/tools/dynamatic/dynamatic.cpp index 5244bfb88a..18f7503911 100644 --- a/tools/dynamatic/dynamatic.cpp +++ b/tools/dynamatic/dynamatic.cpp @@ -686,12 +686,14 @@ CommandResult VerifyInvariants::execute(CommandArguments &args) { if (!state.sourcePathIsSet(keyword)) return CommandResult::FAIL; - std::string script = - state.dynamaticPath + getSeparator() + - "experimental/tools/rigidification/verify_invariant_annotation.sh"; + std::string script = state.dynamaticPath + getSeparator() + + "experimental/tools/rigidification/rigidification.sh"; + + std::string handshakeExport = state.getOutputDir() + getSeparator() + "comp" + + getSeparator() + "handshake_export.mlir"; return execCmd(script, state.dynamaticPath, state.getOutputDir(), - state.getKernelName()); + state.getKernelName(), handshakeExport, "--verify-invariants"); } CommandResult Compile::execute(CommandArguments &args) { From 35e4930e7a141eb7ac2fa530cc3b0d826786ddfd Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Wed, 14 Jan 2026 16:57:30 +0100 Subject: [PATCH 7/9] removed unused script --- .../verify_invariant_annotation.sh | 120 ------------------ 1 file changed, 120 deletions(-) delete mode 100755 experimental/tools/rigidification/verify_invariant_annotation.sh diff --git a/experimental/tools/rigidification/verify_invariant_annotation.sh b/experimental/tools/rigidification/verify_invariant_annotation.sh deleted file mode 100755 index ddd051a527..0000000000 --- a/experimental/tools/rigidification/verify_invariant_annotation.sh +++ /dev/null @@ -1,120 +0,0 @@ -#!/bin/bash - -DYNAMATIC_DIR=$1 -OUTPUT_DIR=$2 -KERNEL_NAME=$3 -# F_HANDSHAKE_EXPORT=$4 -F_HANDSHAKE_EXPORT="$OUTPUT_DIR/comp/handshake_export.mlir" - -source "$DYNAMATIC_DIR/tools/dynamatic/scripts/utils.sh" - -FORMAL_DIR="$OUTPUT_DIR/formal" -MODEL_DIR="$FORMAL_DIR/model" - -DYNAMATIC_OPT_BIN="$DYNAMATIC_DIR/bin/dynamatic-opt" -DYNAMATIC_EXPORT_RTL_BIN="$DYNAMATIC_DIR/bin/export-rtl" - -F_FORMAL_HW="$FORMAL_DIR/hw.mlir" -F_FORMAL_PROP="$FORMAL_DIR/formal_properties.json" -F_NUXMV_PROP="$FORMAL_DIR/property.rpt" -F_NUXMV_CMD="$FORMAL_DIR/prove.cmd" - -NUSMV_BINARY="$DYNAMATIC_DIR/ext/NuSMV" -NUXMV_BINARY="$DYNAMATIC_DIR/ext/nuXmv/bin/nuXmv" - -FORMAL_TESTBENCH_GEN="$DYNAMATIC_DIR/build/bin/rigidification-testbench" - -RTL_CONFIG_SMV="$DYNAMATIC_DIR/data/rtl-config-smv.json" - -SMV_RESULT_PARSER="$DYNAMATIC_DIR/experimental/tools/rigidification/parse_nuxmv_results.py" - -ONLY_VERIFY=true - -if $ONLY_VERIFY; then - SMV_GENERATION_FLAGS="--verify-invariants" - ANNOTATE_FLAGS="annotate-invariants annotate-properties=false" - NUXMV_SCRIPT="set verbose_level 0; -set pp_list cpp; -set counter_examples 0; -set dynamic_reorder 1; -set on_failure_script_quits; -set reorder_method sift; -set enable_sexp2bdd_caching 0; -set bdd_static_order_heuristics basic; -set cone_of_influence; -set use_coi_size_sorting 1; -read_model -i $MODEL_DIR/main.smv; -go_bmc; -check_invar_bmc -a classic; -show_property -o $F_NUXMV_PROP; -time; -quit" -else - NUXMV_SCRIPT="set verbose_level 0; -set pp_list cpp; -set counter_examples 0; -set dynamic_reorder 1; -set on_failure_script_quits; -set reorder_method sift; -set enable_sexp2bdd_caching 0; -set bdd_static_order_heuristics basic; -set cone_of_influence; -set use_coi_size_sorting 1; -read_model -i $MODEL_DIR/main.smv; -flatten_hierarchy; -encode_variables; -build_flat_model; -build_model -f; -check_invar -s forward; -check_ctlspec; -show_property -o $F_NUXMV_PROP; -time; -quit" -fi - -rm -rf "$FORMAL_DIR" && mkdir -p "$FORMAL_DIR" - - -# Annotate properties -"$DYNAMATIC_OPT_BIN" "$F_HANDSHAKE_EXPORT" \ - --handshake-annotate-properties="json-path=$F_FORMAL_PROP $ANNOTATE_FLAGS" \ - > /dev/null - -# handshake level -> hw level -"$DYNAMATIC_OPT_BIN" "$F_HANDSHAKE_EXPORT" --lower-handshake-to-hw \ - > "$F_FORMAL_HW" - -# generate SMV -"$DYNAMATIC_EXPORT_RTL_BIN" \ - "$F_FORMAL_HW" \ - "$MODEL_DIR" \ - "$RTL_CONFIG_SMV" \ - --hdl smv \ - --property-database "$F_FORMAL_PROP" \ - $SMV_GENERATION_FLAGS \ - --dynamatic-path "$DYNAMATIC_DIR" - -# create the testbench -"$FORMAL_TESTBENCH_GEN" \ - -i $MODEL_DIR \ - --name $KERNEL_NAME \ - --mlir $F_FORMAL_HW -exit_on_fail "Failed to create formal testbench" \ - "Created formal testbench" - -# use the modelcheker -echo "$NUXMV_SCRIPT" > $F_NUXMV_CMD -exit_on_fail "Failed to create SMV script" \ - "Created SMV script" - -# run nuXmv and increase the counter everytime it completes the check of a property -echo "[INFO] Running nuXmv" >&2 -$NUXMV_BINARY -source $F_NUXMV_CMD > /dev/null -exit_on_fail "Failed to check formal properties" \ - "Performed model checking to verify the invariants" \ - -# parse and check the results -printf "\n[INFO] Saving formal verification results\n" >&2 -python "$SMV_RESULT_PARSER" "$F_FORMAL_PROP" "$F_NUXMV_PROP" -exit_on_fail "At least one invariant was not verifiable" \ - "All properties proven by 1-induction" From 1b31c7b23f507c1f21e8759fb6123a5d23634683 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Wed, 14 Jan 2026 17:22:42 +0100 Subject: [PATCH 8/9] added some documentation for the verify-invariants command --- docs/UserGuide/CommandReference.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/docs/UserGuide/CommandReference.md b/docs/UserGuide/CommandReference.md index 8b95d3e36e..3f02814daa 100644 --- a/docs/UserGuide/CommandReference.md +++ b/docs/UserGuide/CommandReference.md @@ -28,6 +28,10 @@ The `--fast-token-delivery` flag enables the *Fast Token Delivery (FTD)* algorit > [!NOTE] > Requires a Vivado installation! +- `verify-invariants`: Verify that automatically-generated invariants during rigidification are provably correct. +> [!NOTE] +> Requires nuXmv installation! + - `visualize`: Visualizes the execution of the circuit simulated by `ModelSim`/`Questa`. > [!NOTE] > Requires Godot Engine and [the visualizer component must be built!](AdvancedBuild.md#4-interactive-dataflow-circuit-visualizer) From 07f84881604584d4f07b0fc45d5a384e58c9ca06 Mon Sep 17 00:00:00 2001 From: Bas Niekel Date: Wed, 14 Jan 2026 17:29:59 +0100 Subject: [PATCH 9/9] added enable-leq-binaries flag to CI build command --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 533c485084..9eeed74848 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -80,7 +80,7 @@ jobs: repository: ${{github.event.pull_request.head.repo.full_name}} - name: build - run: ./build.sh --release --force + run: ./build.sh --release --enable-leq-binaries --force - name: check-dynamatic if: steps.build.outputs.exit_code == 0