Re: [sv-ac] multi-clock seq implications

Subject: Re: [sv-ac] multi-clock seq implications
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Thu Feb 13 2003 - 01:24:33 PST

• Next message: Cindy Eisner: "[sv-ac] and, or, intersect"
• Previous message: Cindy Eisner: "Re: [sv-ac] First match example and match of past."
• Maybe in reply to: Joseph Lu: "[sv-ac] multi-clock seq implications"
• Next in thread: Erich Marschner: "RE: [sv-ac] multi-clock seq implications"
• Maybe reply: Cindy Eisner: "Re: [sv-ac] multi-clock seq implications"
• Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

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

• Next message: Cindy Eisner: "[sv-ac] and, or, intersect"
• Previous message: Cindy Eisner: "Re: [sv-ac] First match example and match of past."
• Maybe in reply to: Joseph Lu: "[sv-ac] multi-clock seq implications"
• Next in thread: Erich Marschner: "RE: [sv-ac] multi-clock seq implications"
• Maybe reply: Cindy Eisner: "Re: [sv-ac] multi-clock seq implications"
• Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

This archive was generated by hypermail 2b28 : Thu Feb 13 2003 - 01:21:27 PST