ABD - PSL Four-Level Syntax Structure

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