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

ABD - Sequence Constraint as a Suffix Implication

Earlier example: try phrasing using suffix implication:

Perhaps this will serve as a good always assertion?

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

  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.

PSL has a onehot operator: can use it to stop more than one of these values at once.

Data conservation: At an interface we commonly want to assert that data is not lost or duplicated. Is PSL any help?

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