Subject: [sv-ac] nested implication example
From: dudani@us04.synopsys.com
Date: Wed Feb 12 2003 - 19:21:01 PST
Below is an example of the use of nested implication and dynamic data. The
example is taken from the list of examples distributed to the vfv committee.
Property 15
English description:
Two consecutive writes cannot be to the same address. Address appears one
cycle after the write_valid.(design 6)
System Verilog:
sequence next_event(e) = ((!e * [0:inf]) ; e);
property p15 = ((write_valid ; true) =>
((int addr = addr_bus[0:7])
(true ; next_event(write_valid)) =>
(true;(addr != addr_bus[0:7]))));
The address need to be stored away in the middle of the overall sequence.
Surrendra
**********************************************
Surrendra A. Dudani
Synopsys, Inc.
377 Simarano Drive
Suite 300
Marlboro, MA 01752
Tel: 508-263-8072
Fax: 508-263-8123
email: dudani@synopsys.com
**********************************************
This archive was generated by hypermail 2b28 : Wed Feb 12 2003 - 19:23:29 PST