[fpv/script] add script to parse FPV result This PR creates a script to parse fpv.log results. It will output a results.hjson file. This script is primarily used for dvsim Signed-off-by: Cindy Chen <chencindy@google.com>
diff --git a/hw/formal/tools/jaspergold/parse-fpv-report.py b/hw/formal/tools/jaspergold/parse-fpv-report.py new file mode 100644 index 0000000..8ae8226 --- /dev/null +++ b/hw/formal/tools/jaspergold/parse-fpv-report.py
@@ -0,0 +1,207 @@ +#!/usr/bin/env python3 +# Copyright lowRISC contributors. +# Licensed under the Apache License, Version 2.0, see LICENSE for details. +# SPDX-License-Identifier: Apache-2.0 + +import argparse +import logging as log +import re +from pathlib import Path +from collections import OrderedDict +import sys + +import hjson + + +def extract_messages(str_buffer, patterns): + '''Extract messages matching patterns from str_buffer as a dictionary. + + The patterns argument is a list of pairs, (key, pattern). Each pattern is a regex + and all matches in str_buffer are stored in a dictionary under the paired key. + ''' + results = OrderedDict() + for key, pattern in patterns: + val = results.setdefault(key, []) + val += re.findall(pattern, str_buffer, flags=re.MULTILINE) + + return results + + +def extract_messages_count(str_buffer, patterns): + '''Extract messages matching patterns from full_file as a dictionary. + + The patterns argument is a list of pairs, (key, pattern). Each pattern is a regex + and the total count of all matches in str_buffer are stored in a dictionary under + the paired key. + ''' + results = OrderedDict() + for key, pattern in patterns: + results.setdefault(key, 0) + results[key] += len(re.findall(pattern, str_buffer, flags=re.MULTILINE)) + + return results + + +def format_percentage(good, bad): + '''Return a percetange of good / (good + bad) with a format `100.00 %`.''' + denom = good + bad + pc = 100 * good / denom if denom else 0 + + return '{0:.2f} %'.format(round(pc, 2)) + + +def parse_fpv_message(str_buffer): + '''Parse error, warnings, and failed properties from the log file''' + err_warn_patterns = [("errors", r"^ERROR: .*"), + ("errors", r"^\[ERROR.*"), + ("warnings", r"^WARNING: .*"), + ("warnings", r"^\[WARN.*"), + ("cex", r"^\[\d+\]\s+(\S*)\s+cex.*"), + ("undetermined", r"^\[\d+\]\s+(\S*)\s+undetermined.*"), + ("unreachable", r"^\[\d+\]\s+(\S*)\s+unreachable.*")] + return extract_messages(str_buffer, err_warn_patterns) + + +def parse_fpv_summary(str_buffer): + '''Count errors, warnings, and property status from the log file''' + message_patterns = [("errors", r"^ERROR: .*"), + ("errors", r"^\[ERROR.*"), + ("warnings", r"^WARNING: .*"), + ("warnings", r"^\[WARN.*"), + ("proven", r"^\[\d+\].*proven.*"), + ("cex", r"^\[\d+\].*cex.*"), + ("covered", r"^\[\d+\].*covered.*"), + ("undetermined", r"^\[\d+\].*undetermined.*"), + ("unreachable", r"^\[\d+\].*unreachable.*")] + fpv_summary = extract_messages_count(str_buffer, message_patterns) + + fpv_summary["pass_rate"] = format_percentage(fpv_summary["proven"], + fpv_summary["cex"] + fpv_summary["undetermined"]) + fpv_summary["cov_rate"] = format_percentage(fpv_summary["covered"], fpv_summary["unreachable"]) + + return fpv_summary + + +def get_results(logpath): + '''Parse FPV log file and extract info to a dictionary''' + try: + with Path(logpath).open() as f: + results = OrderedDict() + full_file = f.read() + results["messages"] = parse_fpv_message(full_file) + fpv_summary = parse_fpv_summary(full_file) + if fpv_summary: + results["fpv_summary"] = fpv_summary + return results + + except IOError as err: + err_msg = 'IOError {}'.format(err) + log.error("[get_results] IOError %s", err) + return {'messages': {'errors': err_msg}} + + return results + + +def get_cov_results(logpath): + '''Parse FPV coverage information from the log file''' + try: + with Path(logpath).open() as f: + full_file = f.read() + coverage_patterns = [("stimuli", r"^\|\w+.*\|(\d*.\d\d)%.*\|\d*.\d\d%.*\|\d*.\d\d%.*"), + ("coi", r"^\|\w+.*\|\d*.\d\d%.*\|(\d*.\d\d)%.*\|\d*.\d\d%.*"), + ("proof", r"^\|\w+.*\|\d*.\d\d%.*\|\d*.\d\d%.*\|(\d*.\d\d)%.*")] + cov_results = extract_messages(full_file, coverage_patterns) + for key, item in cov_results.items(): + if len(item) == 1: + cov_results[key] = item[0] + " %" + else: + cov_results[key] = "N/A" + log.error("Parse %s coverage error. Expect one matching value, get %s", + key, item) + return cov_results + + except IOError as err: + log.error("[get_cov_results] IOError %s", err) + return None + + +def main(): + parser = argparse.ArgumentParser( + description= + '''This script parses the JasperGold FPV log to extract below information. + + "messages": { + "errors" : [] + "warnings" : [] + "cex" : ["property1", "property2"...], + "undetermined": [], + "unreachable" : [], + }, + "fpv_summary": { + "errors" : 0 + "warnings" : 2 + "proven" : 20, + "cex" : 5, + "covered" : 18, + "undetermined": 7, + "unreachable" : 2, + "pass_rate" : "90 %", + "cover_rate" : "90 %" + }, + If coverage is enabled, this script will also parse the coverage result: + "fpv_coverage": { + stimuli: "90 %", + coi : "90 %", + proof : "80 %" + } + The script returns nonzero status if any errors or property failures including + "cex, undetermined, unreachable" are presented. + ''') + parser.add_argument('--logpath', + type=str, + default="fpv.log", + help=('FPV log file path. Defaults to `fpv.log` ' + 'under the current script directory.')) + + parser.add_argument('--reppath', + type=str, + default="results.hjson", + help=('Parsed output hjson file path. Defaults to ' + '`results.hjson` under the current script directory.')) + + parser.add_argument('--cov', + type=int, + default=0, + help=('Enable parsing coverage data. ' + 'By default, coerage parsing is disabled.')) + + args = parser.parse_args() + + results = get_results(args.logpath) + + if args.cov: + results["fpv_coverage"] = get_cov_results(args.logpath) + + with Path(args.reppath).open("w") as results_file: + hjson.dump(results, + results_file, + ensure_ascii=False, + for_json=True, + use_decimal=True) + + # return nonzero status if any errors or property failures are present + # TODO: currently allow FPV warnings + err_msgs = results["messages"] + n_errors = len(err_msgs["errors"]) + n_failures = (len(err_msgs.get("cex")) + len(err_msgs.get("undetermined")) + + len(err_msgs.get("unreachable"))) + if n_errors > 0 or n_failures > 0: + log.info("Found %d FPV errors, %d FPV property failures", n_errors, n_failures) + return 1 + + log.info("FPV logfile parsed succesfully") + return 0 + + +if __name__ == "__main__": + sys.exit(main())