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?