Skip to content

mathworks/formal-functional-equivalence

Repository files navigation

Formal Functional Equivalence

Functional equivalence testing is a workflow which involves simulating two models, or a model and its generated code, and ensuring their outputs are equivalent. This is a common workflow in standards such as ISO26262, however this technique does not formally prove functional equivalence in all cases.

This project provides a set of utilities for performing "formal functional equivalence," which is a static analysis-based technique to prove that two Simulink® models are functionally equivalent. These utilities use Property Proving in Simulink Design Verifier™. If the two models are not formally functionally equivalent, Simulink Design Verifier will generate a counterexample for debugging.

Consider using formal functional equivalence when refactoring a model to improve its maintainability, standards compliance, clarity, code generation performance, or for other considerations, while maintaining the expected behavior.

Get Started

To Run:

  1. Open Formal_functional_equivalence.prj in MATLAB®.
  2. Run funcEquivExample.m to see an example

MathWorks Products

Requires MATLAB® release R2022a or newer

License

The license for is available in the license.txt file in this repository.

Copyright 2022 The MathWorks, Inc.