ABD - PSL Four-Level Syntax Structure

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);