HOME       UP       PREV       NEXT (ABD - PSL Temporal Layer Operators)  

ABD - SERES Pattern Matching Example

Suppose four events are supposed to always happen in sequence:

Consider always { true[*]; A; B; C; D }

Basic pattern matcher applied to { A;B;C;D } generates:

  DFF(g0, A, clk);
  AND2(g1, g0, B);
  DFF(g2, g1, clk);
  AND2(g3, g2, C);
  DFF(g4, g3, clk);
  AND2(g5, g4, D);
> val it = x_net "g5" : hexp_t

Although correct, distributive laws mean that all four signals must hold constantly (ignoring start up).

Hence SERES on their own are not much use. Need to embed in temporal layer.

Also, let's create an output that holds when a safety predicate fails.

(C) 2008-10, DJ Greaves, University of Cambridge, Computer Laboratory.