Assertion可能失败排查：is_within_expanded_limits断言失效原因及修复

Let's break down why your assertion is failing and fix it properly. The core issue here is that your current threshold expansion logic is overly complex (handling four combinations of positive/negative lower/upper thresholds), which makes it hard for static analyzers to prove the assertion holds for all valid inputs. Worse, it’s inconsistent with how you expand limits in mean_based mode—let’s fix both problems at once.

In mean_based mode, you expand the tolerance band by keeping the mean (center) fixed and scaling the deviation (half-width) by the expansion factor. For consistency, threshold_based mode should do the same: keep the center of the original threshold range fixed, and scale the range’s half-width by the expansion factor. This approach guarantees that the expanded lower threshold will always be less than the expanded upper threshold, and aligns the behavior across both monitoring modes.

Here’s the revised threshold_based branch for your is_within_expanded_limits function:

when threshold_based =>
    declare
        center : Float_Signed10000 := (monitor.config.lower_threshold + monitor.config.upper_threshold) / 2.0;
        half_width : Float_Signed10000 := (monitor.config.upper_threshold - monitor.config.lower_threshold) / 2.0;
        expanded_half_width : Float_Signed10000 := half_width * monitor.config.settling_tolerance_expansion;
    begin
        expanded_lower_threshold := center - expanded_half_width;
        expanded_upper_threshold := center + expanded_half_width;
        
        -- This assertion will now always hold, as expanded_half_width is positive
        pragma Assert (expanded_lower_threshold < expanded_upper_threshold);
        
        if signal_value >= expanded_lower_threshold and signal_value <= expanded_upper_threshold then
            within_expanded_limits := True;
        end if;
    end;

Why this works: #

• half_width is guaranteed to be positive because your precondition enforces lower_threshold < upper_threshold.
• expanded_half_width is half_width * settling_tolerance_expansion, and since settling_tolerance_expansion > 1.0, this remains positive.
• Subtracting a positive value from the center will always give a smaller number than adding that same positive value to the center—so expanded_lower_threshold < expanded_upper_threshold is mathematically guaranteed, and static analyzers will easily prove this assertion.

Bonus: Consistent behavior across modes #

Your original logic adjusted each threshold independently (dividing positive thresholds by the expansion factor, multiplying negative ones), which led to inconsistent expansion behavior compared to mean_based mode. For example:

• Original range [5, 10] with expansion factor 1.2 would become [~4.17, 12] (width ~7.83)
• The new logic turns it into [4.5, 10.5] (width 6, exactly 1.2x the original width of 5)

This aligns the threshold-based expansion with the mean-based approach, making your monitor’s behavior more predictable across all modes.

内容的提问来源于stack exchange，提问作者Simon