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.