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 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) diff --git a/experimental/include/experimental/Analysis/Passes.td b/experimental/include/experimental/Analysis/Passes.td index c49af6cc2b..5d99e5c4c4 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<"annotateProperties", "annotate-properties", "bool", "true", + "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..2d3a911cab 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 (annotateProperties) { + 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/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/rigidification.sh b/experimental/tools/rigidification/rigidification.sh old mode 100644 new mode 100755 index 153fee7443..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 @@ -55,45 +105,31 @@ 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; -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" diff --git a/tools/dynamatic/dynamatic.cpp b/tools/dynamatic/dynamatic.cpp index eee7b726a2..18f7503911 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,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(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 61ae489367..171491ecb6 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)); @@ -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"; + } } }); diff --git a/tools/integration/TEST_SUITE.cpp b/tools/integration/TEST_SUITE.cpp index cbafa8021a..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{ @@ -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