HOME       UP       PREV       NEXT (ABD - A Simple Model Checker)  

ABD - Sequence Constraint as a Suffix Implication

Earlier example: add a onehot assertion - that will constrain the state space.

Also, consider some phrasing using suffix implications to constrain the state trajectory:
// (Verilog concatenation braces, not a PSL sequence).
always onehot ({A,B,C,D});
// expands to
>val it = // holds on error
  (((A<<3)|(B<<2)|(C<<1)|D) != 8) &&
  (((A<<3)|(B<<2)|(C<<1)|D) != 4) &&
  (((A<<3)|(B<<2)|(C<<1)|D) != 2) &&
  (((A<<3)|(B<<2)|(C<<1)|D) != 1);

//(ML for expanding above macro not in notes)

// A feasible-looking suffix implication:

always { A;B } |=> { C;D };

// It expands to:
  DFF(g0, A, clk);
  AND2(g1, g0, B);
  DFF(g2, g1, clk);
  INV(g3, C);
  AND2(g4, g3, g2);  // Holds if C missing
  DFF(g5, g2, clk);
  INV(g6, D);
  AND2(g7, g5, g6);  // Holds if D missing
  OR2(g8, g7, g4);
> val it = x_net "g8" : hexp_t   // Holds on error

Even this is not very specific: C and D might occur at other times.

It is a good idea to write protocol rules as suffix implications that range over SERES.

Use a separate temporal implication for each sequential step.

What about asserting a requirement of data conservation ? At an interface we commonly want to assert that data is not lost or duplicated. Is PSL any help?

18: (C) 2008-13, DJ Greaves, University of Cambridge, Computer Laboratory.