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?