16737 latest Fairness/Ethics + ML/AI papersVerifying Non-friendly Formal Verification Designs: Can We Start Earlier?
Bryan Olmos, Daniel Gerl, Aman Kumar, Djones Lettnin
arXiv:2410.18454v1 »Full PDF »Published in DVCon Europe 2024
The design of Systems on Chips (SoCs) is becoming more and more complex due
to technological advancements. Missed bugs can cause drastic failures in
safety-critical environments leading to the endangerment of lives. To overcome
these drastic failures, formal property verification (FPV) has been applied in
the industry. However, there exist multiple hardware designs where the results
of FPV are not conclusive even for long runtimes of model-checking tools. For
this reason, the use of High-level Equivalence Checking (HLEC) tools has been
proposed in the last few years. However, the procedure for how to use it inside
an industrial toolchain has not been defined. For this reason, we proposed an
automated methodology based on metamodeling techniques which consist of two
main steps. First, an untimed algorithmic description written in C++ is
verified in an early stage using generated assertions; the advantage of this
step is that the assertions at the software level run in seconds and we can
start our analysis with conclusive results about our algorithm before starting
to write the RTL (Register Transfer Level) design. Second, this algorithmic
description is verified against its sequential design using HLEC and the
respective metamodel parameters. The results show that the presented
methodology can find bugs early related to the algorithmic description and
prepare the setup for the HLEC verification. This helps to reduce the
verification efforts to set up the tool and write the properties manually which
is always error-prone. The proposed framework can help teams working on
datapaths to verify and make decisions in an early stage of the verification
flow.