User manual MATLAB SIMULINK DESIGN VERIFIER RELEASE NOTES

[. . . ] Other product or brand names may be trademarks or registered trademarks of their respective holders. Patents The MathWorks products are protected by one or more U. S. Please see www. mathworks. com/patents for more information. Contents Summary by Version . Version 1. 6 (R2010a) Simulink® Design Verifier Software . Version 1. 5 (R2009b) Simulink® Design Verifier Software . [. . . ] This allows the software to generate test cases for parts of your model that are hard to analyze. If you enable the Extend existing test cases parameter in the Configuration Parameters dialog box, the software imports the logged test cases from a MAT-file. If you also enable the Ignore objectives satisfied by existing test cases parameter, the analysis generates results, ignoring the coverage objectives satisfied by the logged test cases. Otherwise, the analysis efficiently creates a complete test suite. Demo Library and Models to Support Temporal Properties Specification The Simulink Design Verifier software includes a new Temporal Property Specification demo category that includes: · A Temporal Operator Blocks demo library that contains the following blocks and examples: 5 Simulink® Design VerifierTM Release Notes - Detector -- Detects a user-specified length of true duration on the input signal and constructs an output true duration of length based on the output type. Extender -- Extends the true duration of the input signal by a fixed number of time steps or indefinitely. Within Implies -- Captures the within implication by observing whether the second input is true for at least one time step within each true duration of the first input. Temporal Property Specification examples -- A library model that includes examples that use the Detector, Extender, and Within Implies blocks Debounce Temporal Properties Power Window Controller Temporal Properties · Two demo models that contains these blocks: - Support for Stateflow Absolute-Time Temporal Logic Operators The Simulink Design Verifier software now supports the Stateflow® absolute-time temporal logic operators. For more information, see "Operators for Absolute-Time Temporal Logic" in the Stateflow and Stateflow® CoderTM User's Guide. Support for Simulink Blocks The Simulink Design Verifier software now fully supports the following blocks: · Backlash · Cosine · Discrete Derivative · Sine The Simulink Design Verifier software now provides improved support for the following blocks: · Interpolation Using Prelookup 6 Version 1. 6 (R2010a) Simulink® Design VerifierTM Software · Lookup Table (n-D) For more information, see "Simulink Block Support". 7 Simulink® Design VerifierTM Release Notes Version 1. 5 (R2009b) Simulink Design Verifier Software This table summarizes what's new in V1. 5 (R2009b): New Features and Changes Yes Details below Version Compatibility Considerations Yes Summary Fixed Bugs and Known Problems Bug Reports Related Documentation at Web Site Printable Release Notes: PDF Current product documentation · "New Functions for Verification Objectives and Constraints" on page 8 · "Support for Enumerated Signals and Parameters" on page 9 · "New Option to Stop Simulation on Proof Violation" on page 9 · "New sldvmakeharness Function" on page 10 · "New sldvreport Function" on page 10 · "New Support for Simulink Blocks" on page 10 · "Support for New Blocks" on page 10 New Functions for Verification Objectives and Constraints Use these four new functions to specify objectives and constraints within an Embedded MATLAB® script. You can use these functions instead of the corresponding Simulink Design Verifier blocks. By default, this feature is unavailable. To enable automatic stubbing before running an analysis, on the Configuration Parameters Design Verifier main pane, select Automatic stubbing of unsupported blocks and functions. 12 Version 1. 4 (R2009a) Simulink® Design VerifierTM Software In addition, if the compatibility check finds unsupported blocks that automatic stubbing can handle, you can enable automatic stubbing at that time. Long Test Case Optimization Long test cases is a new option for the Test suite optimization parameter. The Long test cases option instructs the Simulink Design Verifier software to create fewer but longer test cases that each satisfy multiple test objectives. With this option, you can customize the analysis results, run a more efficient analysis, and create easier-to-review results, in both Signal Builder and in the HTML report that the software generates. New Support for Blocks The Simulink Design Verifier software now supports models containing the following blocks: · Combinatorial Logic · Decrement Time To Zero · Discrete Filter · Fixed-Point State-Space · Integer Delay · Model blocks that reference other models · Prelookup · Relay Analyzing External Functions for Embedded MATLAB Function Blocks If your model contains an Embedded MATLAB Function block that calls any external functions, the Simulink Design Verifier software can now accumulate coverage results for those functions. 13 Simulink® Design VerifierTM Release Notes Enhanced Block Replacement Capability for Subsystems and Model Blocks You can write your own replacement rules to replace subsystem or Model blocks that reference another model with the Simulink Design Verifier block replacement capability. The software replaces a subsystem or Model block with a different subsystem or with a built-in block as defined in the block replacement rules. New Implies Block The new Implies block simplifies property specification. You can now specify conditions that produce a given response. For example, you can quickly create expressions indicating that pressing the break pedal implies the cruise control must be inactive. You can use the Implies block in any model, not just when running the Simulink Design Verifier software. New Property-Proving Examples and Demos The Simulink Design Verifier block library includes four new example models that demonstrate how to define complex properties for property-proving analysis. In addition, the following demo models are shipping with R2009a: · sldvdemo_sbr_design. mdl -- Finding property violations · sldvdemo_sbr_verification. mdl -- Proving that properties are valid · sldvdemo_thrustrvs_verification. mdl -- Analyzing model and properties to prove correctness or to identify counterexamples · sldvdemo_cruise_control_fxp_verification. mdl -- Proving properties for fixed-point arithmetic with block replacements · sldvdemo_cruise_control_verification. mdl -- Supporting model reference and verification subsystems 14 Version 1. 4 (R2009a) Simulink® Design VerifierTM Software sldvisactive Function The sldvisactive function checks whether the Simulink Design Verifier software is actively translating the model. This function is called from the masked initialization of masked subsystems and other model or block callbacks to configure the model, as needed, for Simulink Design Verifier analysis. For example, the mask initialization of the Environment Controller block invokes the sldvisactive function to output the signal at its Sim port when you start analyzing a model that contains the block. 15 Simulink® Design VerifierTM Release Notes Version 1. 3 (R2008b) Simulink Design Verifier Software This table summarizes what's new in V1. 3 (R2008b): New Features and Changes Yes Details below Version Compatibility Considerations Yes Summary Fixed Bugs and Known Problems Bug Reports Related Documentation at Web Site Printable Release Notes: PDF Current product documentation New features and changes introduced in this version are: · "Simulink Bus Signals and Bus Objects Support " on page 16 · "Fixed-Point Data Support" on page 17 · "Generating Test Harness Model with Model Reference" on page 17 · "Generating SystemTest TEST-File" on page 17 · "Improved Search Algorithms" on page 17 · "New Data File Format" on page 18 · "New HTML Report" on page 18 · "Blocks with No Input Ports Limitation" on page 19 Simulink Bus Signals and Bus Objects Support Simulink Design Verifier now supports Simulink buses and bus objects: · The root Inport and Outport blocks accept bus signals. · Nonvirtual buses are propagated through the model elements. · The test harness model reconstructs the needed bus signals from the underlying bus elements. 16 Version 1. 3 (R2008b) Simulink® Design VerifierTM Software Fixed-Point Data Support Simulink Design Verifier blocks now support fixed-point parameters and inputs. [. . . ] · Prove Properties The Simulink Design Verifier software can prove that signals in your model attain particular values or ranges. Use Simulink Design Verifier blocks to specify values and ranges that you desire signals to attain, or to constrain the values of other signals. If the software disproves any of the values or ranges given the constraints you specify, it produces a test 23 Simulink® Design VerifierTM Release Notes harness model with a Signal Builder block that contains signals comprising counterexamples. Simply simulate the test harness model to confirm that the counterexamples falsify your model's properties. [. . . ]