How to Perform Formal Functional Equivalence - MATLAB & Simulink
Video Player is loading.
Current Time 0:00
Duration 3:27
Loaded: 4.77%
Stream Type LIVE
Remaining Time 3:27
 
1x
  • Chapters
  • descriptions off, selected
  • en (Main), selected
    Video length is 3:27

    How to Perform Formal Functional Equivalence

    Functional equivalence testing is a workflow that involves simulating two models, or a model and its generated code, and ensuring their outputs are equivalent. This technique does not formally prove functional equivalence in all cases. Formal functional equivalence is a static analysis–based technique to formally prove that two Simulink® models are functionally equivalent. You can use formal functional equivalence when refactoring a model to improve its verifiability, maintainability, standards compliance, and code generation performance, or for other considerations, while maintaining the expected behavior.

    Published: 4 Nov 2022

    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 technique does not formally prove functional equivalence in all cases.

    Formal functional equivalence is a static analysis-based technique to formally prove that to Simulink models are functionally equivalent. You can use formal functional equivalence when refactoring a model to improve its verifiability, maintainability, standards compliance, code generation performance, or for other considerations, while maintaining the expected behavior.

    This MATLAB project includes a set of utilities for performing formal functional equivalence using property proving from Simulink Design Verifier. If the two models are not formally functionally equivalent, Simulink Design Verifier will generate a counterexample test case for debugging. Let's see it in action.

    In this scenario, I am an engineer working on a new version of control system software in a vehicle. I have been tasked with implementing the following requirement in Simulink. The control system shall select the median value among triplex redundant vehicle speed sensors when all three sensors are providing valid data.

    I would like to save time when implementing this requirement in Simulink. So I have started with a model from a legacy vehicle program. My team has strict design for verifiability standards for our designs, meaning that the designs should be free of dead logic and relatively easy to completely test. The model from the legacy vehicle program includes a saturation block on the selected signal due to an older, defensive programming approach. If a signal's value cannot be greater than or less than the upper and lower saturation values, then the saturation block is dead logic.

    First, I will use Simulink Design Verifier to check for dead logic. The saturation block is indeed dead and can be removed from the design. The design now complies with my team's standards. I still need to perform requirements-based testing to ensure the design correctly implements the requirement. I can save additional time and budget by reusing the test suite from the legacy vehicle program on the new design.

    Before doing so, I can use formal functional equivalence to prove that the new design is equivalent to the design from the legacy vehicle program. I can use the function formalEquivalence with the names of the two models as arguments. Let's run the function.

    The models are equivalent. Formal functional equivalence has provided me with an additional check to improve my confidence in using the design from the legacy vehicle program while meeting my team's standards. Click on the link below to access the GitHub repository for the formal functional equivalence utilities.

    View more related videos