Subject: RE: [sv-ac] nested implication example
From: Erich Marschner (erichm@cadence.com)
Date: Wed Feb 12 2003 - 20:13:13 PST
Surrendra,
| 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]))));
For comparison, and in the interest of alignment, here's how PSL would express this, using the 'forall' construct:
PSL:
property p15 = forall addr[0:7]: boolean:
always {write_valid; addr_bus[0:7]==addr[0:7]; write_valid[->]} |=>
{addr_bus[0:7] != addr[0:7]};
Regards,
Erich
-------------------------------------------
Erich Marschner, Cadence Design Systems
Senior Architect, Advanced Verification
Phone: +1 410 750 6995 Email: erichm@cadence.com
Vmail: +1 410 872 4369 Email: erichm@comcast.net
-----Original Message-----
From: dudani@us04.synopsys.com [mailto:Surrendra.Dudani@synopsys.com]
Sent: Wednesday, February 12, 2003 10:21 PM
To: sv-ac@eda.org
Subject: [sv-ac] nested implication example
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 - 20:13:48 PST