MODELLING LAYER : Create state properties using RTL.
assign tempok = temperature < 99;
BOOLEAN LAYER
not (rd and wr); -- rd, wr are design signals in the RTL.
TEMPORAL LAYER
-- Sequence definition sequence s1 is {pkt_sop; (not pkt_xfer_en_n [*1 to 100]); pkt_eop}; sequence s2 is {pkt_sop; (not pkt_xfer_en_n [*1 to 100]); pkt_aborted}; -- Property definition property p1 is reset_cycle_ended |=> {s1; s2}; -- Property p1 uses previously defined sequences s1 and s2.
VERIFICATION LAYER
assert always p1 @(posedge clk);
11: (C) 2008-13, DJ Greaves, University of Cambridge, Computer Laboratory. |