[CI] Invariant Verification Test Cases

.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

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)

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<"annotateProperties", "annotate-properties", "bool", "true",
+    "Do not annotate properties for optimizations">
+    ];
 }
 
 #endif // EXPERIMENTAL_ANALYSIS_PASSES_TD

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 (annotateProperties) {
+    if (failed(annotateAbsenceOfBackpressure(modOp)))
+      return signalPassFailure();
+    if (failed(annotateValidEquivalence(modOp)))
+      return signalPassFailure();
+  }
   if (annotateInvariants) {
     if (failed(annotateEagerForkNotAllOutputSent(modOp)))
       return signalPassFailure();

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)

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,52 +97,39 @@ 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
 "$FORMAL_TESTBENCH_GEN" \
   -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;
-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
-exit_on_fail "Created SMV script" \
-  "Failed to create SMV script"
+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 
-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
-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"

tools/dynamatic/dynamatic.cpp

@@ -97,7 +97,6 @@ struct FrontendState {
   std::optional<std::string> 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,20 @@ 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/rigidification.sh";
+
+  std::string handshakeExport = state.getOutputDir() + getSeparator() + "comp" +
+                                getSeparator() + "handshake_export.mlir";
+
+  return execCmd(script, state.dynamaticPath, state.getOutputDir(),
+                 state.getKernelName(), handshakeExport, "--verify-invariants");
+}
+
 CommandResult Compile::execute(CommandArguments &args) {
   // We need the source path to be set
   if (!state.sourcePathIsSet(keyword))
@@ -871,6 +896,7 @@ int main(int argc, char **argv) {
   commands.add<SetSrc>(state);
   commands.add<SetCP>(state);
   commands.add<SetOutputDir>(state);
+  commands.add<VerifyInvariants>(state);
   commands.add<Compile>(state);
   commands.add<WriteHDL>(state);
   commands.add<Simulate>(state);

tools/export-rtl/export-rtl.cpp

@@ -87,6 +87,11 @@ static cl::opt<HDL>
                    clEnumValN(HDL::SMV, "smv", "SMV")),
         cl::cat(mainCategory));
 
+static cl::opt<bool> 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<std::string>
     rtlConfigs(cl::Positional, cl::OneOrMore,
                cl::desc("<RTL configuration files...>"), cl::cat(mainCategory));
@@ -1386,11 +1391,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 (verifyInvariants) {
+      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";
+      }
     }
   });
 

tools/integration/TEST_SUITE.cpp

 run: ./build.sh --release --force 
 run: ./build.sh --release --force 
@@ -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{
@@ -391,6 +392,43 @@ INSTANTIATE_TEST_SUITE_P(SpecBenchmarks, SpecFixture,
 
 #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");
+  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);
+}
+
 TEST_P(RigidificationFixture, basic) {
   IntegrationTestData config{
       // clang-format off