MODELLING LAYER : Create state properties using RTL.
assign pkt_sop = state == 0 && !reset && running; assign pkt_eop = state > 0 && !reset && eop_in ... assign tempok = temperature < 99;
BOOLEAN LAYER
!(rd && tempok); // rd, tempok are RTL/modelling layer signals.
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
foo_22: assert always p1 @(posedge clk);
12: (C) 2008-16, DJ Greaves, University of Cambridge, Computer Laboratory. |