1



2

 Returns true on rising edge of p

3



4

node Rise(p: bool) returns (r: bool);

5

let

6

r = false > not pre(p) and p;

7

tel;

8


9

node Fall(p: bool) returns (r: bool);

10

let

11

r = false > (not p) and pre p ;

12

tel

13


14


15



16

 Returns true when p changes

17



18

node Changed(p: bool) returns (r: bool);

19

let

20

r = false > p <> pre(p);

21

tel;

22


23


24



25

 Latches p

26



27

node Latch(p: bool) returns (r: bool);

28

let

29

r = p > p or pre(r);

30

tel;

31


32


33



34

 Converts a Boolean to an integer

35



36

node b2i(b: bool) returns (i: int);

37

let i = if b then 1 else 0; tel;

38


39


40



41

 Returns a stream true for the first n steps of clock clk

42



43

node ctF(n: int; clk: bool) returns (r: bool);

44

var

45

c: int;

46

ctF_counter_positive: bool;

47

let

48

c = b2i(clk) > pre(c) + b2i(clk);

49

r = (c <= n);

50


51

ctF_counter_positive = c >= 0;

52

 PROPERTY ctF_counter_positive;

53

tel;

54


55


56



57

 Returns number of steps p has been true

58



59

node Duration(p: bool) returns (r: int);

60

var

61

value_posnat: bool;

62

let

63

 Counts the number of instants since p was last false

64

r = if p then (1 > pre(r) + 1) else 0;

65


66

value_posnat = r >= 0;

67

 PROPERTY value_posnat;

68


69

tel;

70


71


72



73

 Returns number of steps since p has been true  zero if p never true

74



75

node Since(p: bool) returns (r: int);

76

var

77

value_posnat, zero_till_true: bool;

78

let

79

r = b2i(p) > if p then 1 else if pre(r) = 0 then 0 else pre(r) + 1;

80


81

value_posnat = r >= 0;

82

 PROPERTY value_posnat;

83


84

zero_till_true = not Latch(p) => (r = 0);

85

 PROPERTY zero_till_true;

86


87

tel;

88


89



90

 Returns whether P has been true within the last n steps

91



92

node Within(p: bool; n : int) returns (r: bool);

93

let

94

r = Since(p) > 0 and Since(p) <= n;

95

tel;

96


97

node OnceWithin(p: bool; n : int) returns (r: bool);

98

var since_p, pre_since_p : int ;

99

let

100

since_p = Since(p) ;

101

pre_since_p =

102

0 > if p then (if pre since_p = 0 then 0 else pre since_p + 1)

103

else (if pre pre_since_p > 0 then pre pre_since_p + 1

104

else 0) ;

105

r = (Since(p) > 0 and since_p <= n) and (pre_since_p > n or pre_since_p = 0) ;

106

 PROPERTY (pre_since_p = 0) or (pre_since_p > since_p) ;

107

tel;

108


109



110

 Returns true if p is always true for at least n steps

111



112

node True_At_Least(p: bool; n: int) returns (r: bool);

113

var

114

c: int;

115

value_posnat: bool;

116

let

117

 Counts the number of steps p has been true

118

c = b2i(p) > if p then pre(c) + 1 else 0;

119


120

r = true > ((pre(c) > 0 and pre(c) < n) => p);

121


122

value_posnat = c >= 0;

123

 PROPERTY value_posnat;

124


125

tel;

126


127


128


129

node Initializing

130

(LS_CLK, RS_CLK, LR_CLK, RL_CLK: bool)

131

returns

132

(r: bool);

133

var

134

LS_Initializing: bool;

135

RS_Initializing: bool;

136

LR_Initializing: bool;

137

RL_Initializing: bool;

138


139

let

140

LS_Initializing = ctF(1, LS_CLK);

141

RS_Initializing = ctF(1, RS_CLK);

142

LR_Initializing = ctF(1, LR_CLK);

143

RL_Initializing = ctF(1, RL_CLK);

144


145

r =

146

(LS_Initializing or

147

RS_Initializing or

148

LR_Initializing or

149

RL_Initializing);

150


151

tel

152


153

 Inihibited mode constant.

154

 const inhibit_count_max = 2;

155


156

node PFS_Logic

157

(riseTS, riseOSPF : bool;

158

Primary_Side : bool)

159


160

returns

161

(PFS : bool);

162


163

 const St_Inhibited : int = 1 ;

164

 const St_Listening : int = 2 ;

165

 const St_Flying : int = 3 ;

166


167

var

168

 state : subrange [1, 3] of int;

169

State: int;

170

fly_to_inh, inh_to_lis, lis_to_fly: bool;

171

inhibit_count: int;

172

let

173


174

 3 > 1

175

fly_to_inh = false > (pre(State) = 3) and riseOSPF ;

176

 1 > 2

177

inh_to_lis = false >

178

(pre(State) = 1) and pre(inhibit_count) >= 2 ;

179

 T6: 2 > 3

180

lis_to_fly = (false > (pre(State) = 2) and riseTS) ;

181


182

State = (

183

if Primary_Side then 3 else 1

184

) > (

185

if fly_to_inh then 1 else

186

if inh_to_lis then 2 else

187

if lis_to_fly then 3 else

188

pre State

189

) ;

190


191

 PROPERTY (state = 3) or (state = 1) or (state = 2) ;

192


193

PFS = Primary_Side > (

194

if State = 1 then false else

195

if State = 2 then false else

196

if State = 3 then true else

197

 Unreachable.

198

pre PFS

199

) ;

200


201

inhibit_count = 0 > (

202

if State = 1 then pre inhibit_count + 1 else 0

203

) ;

204

 %PROPERTY inhibit_count <= 2 ;

205


206

tel;

207


208


209

node PFS_Side

210

(TS, OSPF : bool;

211

Primary_Side : bool)

212


213

returns

214

(PFS : bool);

215


216

var

217

PFSL_PFS : bool;

218

riseTS_O : bool;

219

riseOSPF_O : bool;

220


221

let

222


223

PFSL_PFS =

224

PFS_Logic(riseTS_O, riseOSPF_O, Primary_Side);

225


226

riseTS_O = Rise(TS);

227


228

riseOSPF_O = Rise(OSPF);

229


230

PFS = PFSL_PFS;

231


232

tel;

233


234


235

node Cross_Channel_Bus

236

(I : bool;

237

Init_Bool : bool)

238


239

returns

240

(O : bool);

241


242

let

243

O = Init_Bool > pre I ;

244

tel;

245


246

node qs_dfa (p, q : bool) returns (ok : bool);

247


248

var

249

r : int;

250


251

let

252


253

ok = not (((0 > pre r) = 2 and p) or ((0 > pre r) = 2 and q));

254


255

r = if p and q then 0

256

else if p then

257

(if (0 > pre r) < 0 then 1 else ((0 > pre r)) + 1)

258

else if q then

259

(if (0 > pre r) > 0 then 1 else ((0 > pre r))  1)

260

else (0 > pre r);

261


262

tel;

263


264

node qs_calendar

265

(CLK1: bool; CLK2: bool; CLK3: bool; CLK4: bool)

266

returns

267

(ok : bool);

268

let

269

ok =

270

(qs_dfa(CLK1, CLK2) and

271

qs_dfa(CLK1, CLK3) and

272

qs_dfa(CLK1, CLK4) and

273

qs_dfa(CLK2, CLK3) and

274

qs_dfa(CLK2, CLK4) and

275

qs_dfa(CLK3, CLK4) and

276

(CLK1 or CLK2 or CLK3 or CLK4));

277

tel;

278


279


280


281


282


283


284

node SinceGTOrZero(in: bool ; min: int) returns (out: bool) ;

285

let

286

out = (Since(in) > min) or (Since(in) = 0) ;

287

tel

288


289

node SinceLENotZero(in: bool ; max: int) returns (out: bool) ;

290

let

291

out = (Since(in) <= max) and (Since(in) > 0) ;

292

tel

293


294


295


296

 const all_ticked_max = 7 ;

297


298

 const both_stabilization_max =

299

 (2 + 2) * (7 + 1) + 7 ;

300


301

 const 28 =

302

 (2 + 2) * 7 ;

303

 const side_comm_stabilization_max =

304

 (2 + 2) * 7 + 7 ;

305


306


307


308


309


310


311

node PFS

312

(TS : bool)

313

returns

314

(LPFS, RPFS, LS_PFS, RS_PFS, RL_O, LR_O : bool) ;

315

var

316

global_req, global_ens,

317

inhibited_R2_R3_req, inhibited_R2_R3_ens,

318

unchanged_nop_R5_req, unchanged_nop_R5_ens,

319

change_R3_rise_req, change_R3_rise_ens,

320

change_R3_fall_req, change_R3_fall_ens,

321

assume, guarantee: bool ;

322

let

323


324

LS_PFS =

325

PFS_Side(TS, RL_O, true);

326


327

RS_PFS =

328

PFS_Side(TS, LR_O, false);

329


330

LR_O =

331

Cross_Channel_Bus (LS_PFS, true);

332


333

RL_O =

334

((*! /inlining/: true;*)Cross_Channel_Bus (RS_PFS, false));

335


336

LPFS = LS_PFS ;

337

RPFS = RS_PFS ;

338


339

global_req = Duration(true) <= 2 + 2 => not Rise(TS) ;

340

global_ens = (

341

( (LPFS and (not RPFS)) > true ) and

342

( LPFS or RPFS ) and

343

( SinceGTOrZero(Rise(TS), 1) => LPFS = not RPFS )

344

) ;

345


346

inhibited_R2_R3_req = false >

347

SinceLENotZero(Fall(pre LPFS) or Fall(pre RPFS), 2) ;

348

inhibited_R2_R3_ens = not (Changed(RPFS) or Changed(LPFS)) ;

349


350

unchanged_nop_R5_req = SinceGTOrZero(Rise(TS), 2 + 1) ;

351

unchanged_nop_R5_ens = not (Changed(RPFS) or Changed(LPFS)) ;

352


353

change_R3_rise_req = Rise(TS) and (

354

SinceGTOrZero(

355

Fall(false > pre RPFS) or Fall(true > pre LPFS),

356

2 + 2

357

)

358

) ;

359

change_R3_rise_ens =

360

Rise(RPFS) or Rise(LPFS) and not (Rise(RPFS) and Rise(LPFS)) ;

361


362

change_R3_fall_req = Since(

363

Rise(true > pre LPFS) or Rise(false > pre RPFS)

364

) = 1 ;

365

change_R3_fall_ens =

366

Fall(RPFS) or Fall(LPFS) and not (Fall(RPFS) and Fall(LPFS)) ;

367


368

assume = global_req and (

369

inhibited_R2_R3_req or

370

unchanged_nop_R5_req or

371

change_R3_rise_req or

372

change_R3_fall_req

373

) ;

374


375

guarantee = global_ens and (

376

(inhibited_R2_R3_req => inhibited_R2_R3_ens) and

377

(unchanged_nop_R5_req => unchanged_nop_R5_ens) and

378

(change_R3_rise_req => change_R3_rise_ens) and

379

(change_R3_fall_req => change_R3_fall_ens)

380

) ;

381


382


383

!PROPERTY : ( Duration(assume) = Duration(true) ) => guarantee ;

384


385

tel;

386


387

