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

ABD - SERES Pattern Matching Example

Suppose four events are supposed to always happen in sequence:

Desired behaviour of the four nets.
Desired behaviour of the four nets.

 

First attempt, we write 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);  
 // Hmmm D must always hold then ? 
 // Not what we wanted!
> val it = x_net "g5" : hexp_t
images/pslcct1.png

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.


17: (C) 2012-18, DJ Greaves, University of Cambridge, Computer Laboratory.