### Profile

 1 ```------------------------------------------------------------------------------ ``` ```-- Returns true on rising edge of p ``` ```------------------------------------------------------------------------------ ``` ```node Rise(p: bool) returns (r: bool); ``` ```let ``` ``` r = false -> not pre(p) and p; ``` ```tel; ``` ```node Fall(p: bool) returns (r: bool); ``` ```let ``` ``` r = false -> (not p) and pre p ; ``` ```tel ``` ```------------------------------------------------------------------------------ ``` ```-- Returns true when p changes ``` ```------------------------------------------------------------------------------ ``` ```node Changed(p: bool) returns (r: bool); ``` ```let ``` ``` r = false -> p <> pre(p); ``` ```tel; ``` ``` ``` ```------------------------------------------------------------------------------ ``` ```-- Latches p ``` ```------------------------------------------------------------------------------ ``` ```node Latch(p: bool) returns (r: bool); ``` ```let ``` ``` r = p -> p or pre(r); ``` ```tel; ``` ``` ``` ```------------------------------------------------------------------------------ ``` ```-- Converts a Boolean to an integer ``` ```------------------------------------------------------------------------------ ``` ```node b2i(b: bool) returns (i: int); ``` ```let i = if b then 1 else 0; tel; ``` ``` ``` ```------------------------------------------------------------------------------ ``` ```-- Returns a stream true for the first n steps of clock clk ``` ```------------------------------------------------------------------------------ ``` ```node ctF(n: int; clk: bool) returns (r: bool); ``` ```var ``` ``` c: int; ``` ``` ctF_counter_positive: bool; ``` ```let ``` ``` c = b2i(clk) -> pre(c) + b2i(clk); ``` ``` r = (c <= n); ``` ``` ``` ``` ctF_counter_positive = c >= 0; ``` ``` -- PROPERTY ctF_counter_positive; ``` ```tel; ``` ``` ``` ```------------------------------------------------------------------------------ ``` ```-- Returns number of steps p has been true ``` ```------------------------------------------------------------------------------ ``` ```node Duration(p: bool) returns (r: int); ``` ```var ``` ``` value_posnat: bool; ``` ```let ``` ``` -- Counts the number of instants since p was last false ``` ``` r = if p then (1 -> pre(r) + 1) else 0; ``` ``` ``` ``` value_posnat = r >= 0; ``` ``` -- PROPERTY value_posnat; ``` ``` ``` ```tel; ``` ```------------------------------------------------------------------------------ ``` ```-- Returns number of steps since p has been true - zero if p never true ``` ```------------------------------------------------------------------------------ ``` ```node Since(p: bool) returns (r: int); ``` ```var ``` ``` value_posnat, zero_till_true: bool; ``` ```let ``` ``` r = b2i(p) -> if p then 1 else if pre(r) = 0 then 0 else pre(r) + 1; ``` ``` ``` ``` value_posnat = r >= 0; ``` ``` -- PROPERTY value_posnat; ``` ``` zero_till_true = not Latch(p) => (r = 0); ``` ``` -- PROPERTY zero_till_true; ``` ``` ``` ```tel; ``` ``` ``` ```------------------------------------------------------------------------------ ``` ```-- Returns whether P has been true within the last n steps ``` ```------------------------------------------------------------------------------ ``` ```node Within(p: bool; n : int) returns (r: bool); ``` ```let ``` ``` r = Since(p) > 0 and Since(p) <= n; ``` ```tel; ``` ```node OnceWithin(p: bool; n : int) returns (r: bool); ``` ```var since_p, pre_since_p : int ; ``` ```let ``` ``` since_p = Since(p) ; ``` ``` pre_since_p = ``` ``` 0 -> if p then (if pre since_p = 0 then 0 else pre since_p + 1) ``` ``` else (if pre pre_since_p > 0 then pre pre_since_p + 1 ``` ``` else 0) ; ``` ``` r = (Since(p) > 0 and since_p <= n) and (pre_since_p > n or pre_since_p = 0) ; ``` ``` -- PROPERTY (pre_since_p = 0) or (pre_since_p > since_p) ; ``` ```tel; ``` ```------------------------------------------------------------------------------ ``` ```-- Returns true if p is always true for at least n steps ``` ```------------------------------------------------------------------------------ ``` ```node True_At_Least(p: bool; n: int) returns (r: bool); ``` ```var ``` ``` c: int; ``` ``` value_posnat: bool; ``` ```let ``` ``` -- Counts the number of steps p has been true ``` ``` c = b2i(p) -> if p then pre(c) + 1 else 0; ``` ``` ``` ``` r = true -> ((pre(c) > 0 and pre(c) < n) => p); ``` ``` ``` ``` value_posnat = c >= 0; ``` ``` -- PROPERTY value_posnat; ``` ```tel; ``` ``` ``` ``` ``` ```node Initializing ``` ``` (LS_CLK, RS_CLK, LR_CLK, RL_CLK: bool) ``` ```returns ``` ``` (r: bool); ``` ```var ``` ``` LS_Initializing: bool; ``` ``` RS_Initializing: bool; ``` ``` LR_Initializing: bool; ``` ``` RL_Initializing: bool; ``` ``` ``` ```let ``` ``` LS_Initializing = ctF(1, LS_CLK); ``` ``` RS_Initializing = ctF(1, RS_CLK); ``` ``` LR_Initializing = ctF(1, LR_CLK); ``` ``` RL_Initializing = ctF(1, RL_CLK); ``` ``` r = ``` ``` (LS_Initializing or ``` ``` RS_Initializing or ``` ``` LR_Initializing or ``` ``` RL_Initializing); ``` ```tel ``` ```-- Inihibited mode constant. ``` ```-- const inhibit_count_max = 2; ``` ```node PFS_Logic ``` ``` (riseTS, riseOSPF : bool; ``` ``` Primary_Side : bool) ``` ```returns ``` ``` (PFS : bool); ``` ```-- const St_Inhibited : int = 1 ; ``` ```-- const St_Listening : int = 2 ; ``` ```-- const St_Flying : int = 3 ; ``` ```var ``` ``` -- state : subrange [1, 3] of int; ``` ``` State: int; ``` ``` fly_to_inh, inh_to_lis, lis_to_fly: bool; ``` ``` inhibit_count: int; ``` ```let ``` ``` -- 3 -> 1 ``` ``` fly_to_inh = false -> (pre(State) = 3) and riseOSPF ; ``` ``` -- 1 -> 2 ``` ``` inh_to_lis = false -> ``` ``` (pre(State) = 1) and pre(inhibit_count) >= 2 ; ``` ``` -- T6: 2 -> 3 ``` ``` lis_to_fly = (false -> (pre(State) = 2) and riseTS) ; ``` ``` State = ( ``` ``` if Primary_Side then 3 else 1 ``` ``` ) -> ( ``` ``` if fly_to_inh then 1 else ``` ``` if inh_to_lis then 2 else ``` ``` if lis_to_fly then 3 else ``` ``` pre State ``` ``` ) ; ``` ``` -- PROPERTY (state = 3) or (state = 1) or (state = 2) ; ``` ``` PFS = Primary_Side -> ( ``` ``` if State = 1 then false else ``` ``` if State = 2 then false else ``` ``` if State = 3 then true else ``` ``` -- Unreachable. ``` ``` pre PFS ``` ``` ) ; ``` ``` inhibit_count = 0 -> ( ``` ``` if State = 1 then pre inhibit_count + 1 else 0 ``` ``` ) ; ``` ``` -- %PROPERTY inhibit_count <= 2 ; ``` ```tel; ``` ```node PFS_Side ``` ``` (TS, OSPF : bool; ``` ``` Primary_Side : bool) ``` ```returns ``` ``` (PFS : bool); ``` ```var ``` ``` PFSL_PFS : bool; ``` ``` riseTS_O : bool; ``` ``` riseOSPF_O : bool; ``` ``` ``` ```let ``` ``` PFSL_PFS = ``` ``` PFS_Logic(riseTS_O, riseOSPF_O, Primary_Side); ``` ``` ``` ``` riseTS_O = Rise(TS); ``` ``` riseOSPF_O = Rise(OSPF); ``` ``` PFS = PFSL_PFS; ``` ```tel; ``` ```node Cross_Channel_Bus ``` ``` (I : bool; ``` ``` Init_Bool : bool) ``` ```returns ``` ``` (O : bool); ``` ```let ``` ``` O = Init_Bool -> pre I ; ``` ```tel; ``` ```node qs_dfa (p, q : bool) returns (ok : bool); ``` ```var ``` ``` r : int; ``` ```let ``` ``` ok = not (((0 -> pre r) = 2 and p) or ((0 -> pre r) = -2 and q)); ``` ``` ``` ``` r = if p and q then 0 ``` ``` else if p then ``` ``` (if (0 -> pre r) < 0 then 1 else ((0 -> pre r)) + 1) ``` ``` else if q then ``` ``` (if (0 -> pre r) > 0 then -1 else ((0 -> pre r)) - 1) ``` ``` else (0 -> pre r); ``` ```tel; ``` ```node qs_calendar ``` ``` (CLK1: bool; CLK2: bool; CLK3: bool; CLK4: bool) ``` ```returns ``` ``` (ok : bool); ``` ```let ``` ``` ok = ``` ``` (qs_dfa(CLK1, CLK2) and ``` ``` qs_dfa(CLK1, CLK3) and ``` ``` qs_dfa(CLK1, CLK4) and ``` ``` qs_dfa(CLK2, CLK3) and ``` ``` qs_dfa(CLK2, CLK4) and ``` ``` qs_dfa(CLK3, CLK4) and ``` ``` (CLK1 or CLK2 or CLK3 or CLK4)); ``` ```tel; ``` ```node SinceGTOrZero(in: bool ; min: int) returns (out: bool) ; ``` ```let ``` ``` out = (Since(in) > min) or (Since(in) = 0) ; ``` ```tel ``` ```node SinceLENotZero(in: bool ; max: int) returns (out: bool) ; ``` ```let ``` ``` out = (Since(in) <= max) and (Since(in) > 0) ; ``` ```tel ``` ```-- const all_ticked_max = 7 ; ``` ```-- const both_stabilization_max = ``` ```-- (2 + 2) * (7 + 1) + 7 ; ``` ```-- const 28 = ``` ```-- (2 + 2) * 7 ; ``` ```-- const side_comm_stabilization_max = ``` ```-- (2 + 2) * 7 + 7 ; ``` ```node PFS ``` ``` (TS : bool) ``` ```returns ``` ``` (LPFS, RPFS, LS_PFS, RS_PFS, RL_O, LR_O : bool) ; ``` ```var ``` ``` global_req, global_ens, ``` ``` inhibited_R2_R3_req, inhibited_R2_R3_ens, ``` ``` unchanged_nop_R5_req, unchanged_nop_R5_ens, ``` ``` change_R3_rise_req, change_R3_rise_ens, ``` ``` change_R3_fall_req, change_R3_fall_ens, ``` ``` assume, guarantee: bool ; ``` ```let ``` ``` LS_PFS = ``` ``` PFS_Side(TS, RL_O, true); ``` ``` RS_PFS = ``` ``` PFS_Side(TS, LR_O, false); ``` ``` LR_O = ``` ``` Cross_Channel_Bus (LS_PFS, true); ``` ``` RL_O = ``` ``` ((*! /inlining/: true;*)Cross_Channel_Bus (RS_PFS, false)); ``` ``` LPFS = LS_PFS ; ``` ``` RPFS = RS_PFS ; ``` ``` global_req = Duration(true) <= 2 + 2 => not Rise(TS) ; ``` ``` global_ens = ( ``` ``` ( (LPFS and (not RPFS)) -> true ) and ``` ``` ( LPFS or RPFS ) and ``` ``` ( SinceGTOrZero(Rise(TS), 1) => LPFS = not RPFS ) ``` ``` ) ; ``` ``` inhibited_R2_R3_req = false -> ``` ``` SinceLENotZero(Fall(pre LPFS) or Fall(pre RPFS), 2) ; ``` ``` inhibited_R2_R3_ens = not (Changed(RPFS) or Changed(LPFS)) ; ``` ``` unchanged_nop_R5_req = SinceGTOrZero(Rise(TS), 2 + 1) ; ``` ``` unchanged_nop_R5_ens = not (Changed(RPFS) or Changed(LPFS)) ; ``` ``` change_R3_rise_req = Rise(TS) and ( ``` ``` SinceGTOrZero( ``` ``` Fall(false -> pre RPFS) or Fall(true -> pre LPFS), ``` ``` 2 + 2 ``` ``` ) ``` ``` ) ; ``` ``` change_R3_rise_ens = ``` ``` Rise(RPFS) or Rise(LPFS) and not (Rise(RPFS) and Rise(LPFS)) ; ``` ``` change_R3_fall_req = Since( ``` ``` Rise(true -> pre LPFS) or Rise(false -> pre RPFS) ``` ``` ) = 1 ; ``` ``` change_R3_fall_ens = ``` ``` Fall(RPFS) or Fall(LPFS) and not (Fall(RPFS) and Fall(LPFS)) ; ``` ``` assume = global_req and ( ``` ``` inhibited_R2_R3_req or ``` ``` unchanged_nop_R5_req or ``` ``` change_R3_rise_req or ``` ``` change_R3_fall_req ``` ``` ) ; ``` ``` guarantee = global_ens and ( ``` ``` (inhibited_R2_R3_req => inhibited_R2_R3_ens) and ``` ``` (unchanged_nop_R5_req => unchanged_nop_R5_ens) and ``` ``` (change_R3_rise_req => change_R3_rise_ens) and ``` ``` (change_R3_fall_req => change_R3_fall_ens) ``` ``` ) ; ``` ``` --!PROPERTY : ( Duration(assume) = Duration(true) ) => guarantee ; ``` ``` ``` ```tel; ```