Subject: RE: [sv-ac] multi-clock seq implications
From: Erich Marschner (erichm@cadence.com)
Date: Thu Feb 13 2003 - 05:12:37 PST
Cindy, Joseph,
I can confirm that the DWG decided not to include support for multiply-clocked assertions in the first release. This decision was taken because there are fundamental differences between the semantics of PSL and OVA in this area, and it was clear that we could not come to agreement in the DWG. In general, we tried to avoid including features that would lead to long, drawn-out arguments, and this is one of the features that would clearly have done so.
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: Cindy Eisner [mailto:EISNER@il.ibm.com]
| Sent: Thursday, February 13, 2003 4:25 AM
| To: Joseph Lu
| Cc: sv-ac@eda.org; dudani@us04.synopsys.com
| Subject: Re: [sv-ac] multi-clock seq implications
|
|
| joseph,
|
| i see that no one has answered this yet. as far as i
| understand it, it was
| decided not to support multi-clocked assertions for this version.
|
| regards,
|
| cindy.
|
| Cindy Eisner
| Formal Methods Group Tel:
| +972-4-8296-266
| IBM Haifa Research Laboratory Fax: +972-4-8296-114
| Haifa 31905, Israel e-mail:
| eisner@il.ibm.com
|
|
| Joseph Lu <Juin-Yeu.Lu@sun.com>@eda.org on 10/02/2003 22:59:14
|
| Please respond to Joseph Lu <Juin-Yeu.Lu@sun.com>
|
| Sent by: owner-sv-ac@eda.org
|
|
| To: sv-ac@eda.org, "dudani@us04.synopsys.com"
| <Surrendra.Dudani@synopsys.com>
| cc:
| Subject: [sv-ac] multi-clock seq implications
|
|
|
| Hi,
|
|
| Have anyone thought about how multi-clock seq implication can be
| handled using existing proposals for seq implication?
| I haven't seen any operational semantics been defined.
| Am i missing anything?
|
|
| For example,
|
| given a multi-clock system that clocks are necessarily synchronous,
| there groups of events need to be observed in partial oder fashion.
|
| My intent is that
|
| 1) if I see {a1; a2; a3} followed by {b1; b2; b3}, then
| I expect to see {c1; c2; c3}
|
| 2) if I see {a1; a2; a3} followed by {b4; b5; b6}, then
| I expect to see {c4; c5; c6}; otherwise,
|
| 3) if I see {a1; a2; a3} is followed neither by {b1; b2;
| b3} nor {b4;
| b5; b6},
| but followed by a timeout,{[100] TRUE} @clk_a, then
| I expect to see a trap sequence {trap_start;trap_handle}
|
|
| {a1; a2; a3} @clk_a
|
| {a4; a5; a6} @clk_a
|
| {b1; b2; b3} @clk_b
|
| {b4; b5; b6} @clk_b
|
| {c1; c2; c3} @clk_c
|
| {c4; c5; c6} @clk_c
|
| {trap_start;trap_handle} @clk_sp
|
|
| Seq IMP:
|
| {a1; a2; a3} @clk_a => {b1; b2; b3} @clk_b or {b4; b5; b6} @clk_b
|
| {b1; b2; b3} @clk_b => {c1; c2; c3} @clk_c
| {b4; b5; b6} @clk_b => {c4; c5; c6} @clk_c
|
| {a1; a2; a3} @clk_a => {[100] TRUE} @clk_a =>
| {trap_start;trap_handle}
| @clk_sp
|
|
|
| Thanks,
|
| --Joseph
|
|
| --------------------------------------------------
| Joseph Lu
| Global Validation, Processor Product Group
| Sun Microsystems
| M/S USUN 03-202, 430 N. Mary Ave.,
| Sunnyvale, CA 94086
| 408-616-5887
| joseph@eng.sun.com
| --------------------------------------------------
|
|
|
|
|
|
|
This archive was generated by hypermail 2b28 : Thu Feb 13 2003 - 05:14:11 PST