Subject: Re: [sv-ac] The case for retaining check
From: dudani@us04.synopsys.com
Date: Sun Feb 16 2003 - 10:52:00 PST
Hi Cindy and Prakash,
Your proposal is reasonable. It is not an immediate assertion, but
strobed(from DAS) assertion, where sampling takes place at(rosync time) at
the end of simulation step.
In immediate assertion, one would catch all glitches, including the ones
that happen during a time step.
In strobed assertion, there would be no glitches during a time step, but
the glitches between two clock(hardware) ticks, assuming we are dealing
with synchronous logic, would be detected.
It also makes sense to restrict such assertions to combinational logic.
However, I'm not so sure about the requirement, whether event based
combinational assertion, or strobed based combinational assertion is needed.
Surrendra
At 05:11 PM 2/16/2003 +0200, you wrote:
>prakash,
>
>i agree that getting rid of check will leave a hole. i have the following
>proposal:
>
>get rid of the keyword "check", but not the idea of immediate assertions.
>define that a clocked property is sampled, as described in section 11.3 of
>revision 0.79. an unclocked property must be a boolean expression, and
>works like an immediate assertion (like check does currently).
>
>justification:
>
>getting rid of check will leave a hole, but the current definition makes
>"check" look like something other than an assertion, which might be what
>bothers lots of people (it bothers me a lot, at least).
>
>the above proposal allows you to code: "assert (e)" when you mean an
>immediate assertion, "assert @(posedge clk) (e)" when you mean a sampled
>assertion, and "assert @(posedge clk) (e ; f ; g)" when you mean a sampled
>assertion that lives for more than one clock cycle. note that under this
>proposal, "assert (e ; f ; g)", where the sequence is unclocked, is not
>allowed.
>
>since revision 0.79 does not seem to describe what an unclocked sequence
>means, this does not conflict with anything now defined.
>
>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
>
>
>Prakash Narain <prakash@realintent.com>@eda.org on 13/02/2003 23:45:22
>
>Sent by: owner-sv-ac@eda.org
>
>
>To: sv-ac <sv-ac@eda.org>
>cc:
>Subject: [sv-ac] The case for retaining check
>
>
>
>I want to challenge that we can't get rid of check without
>leaving a permanent hole in the specification capability of
>assertions. I am also challenging that a better scheduling
>of procedural assertions can't be designed.
>
>Let me elaborate on the issue I was trying to raise in the
>meeting today. I want to say (A=>B in the current cycle). I
>want to say this as the first element of the sequence in a
>procedural assertion. I can't do that with the proposed
>scheduling/evaluation semantics when the procedural block
>is a sequential block. An example is given below.
>
>always @(posedge clk)
> case(sig1)
> junk1:
> if (sig2) begin
> .
> .
> .
> if (sig3) begin
> check(foo) ;
> //desired behavior if (!foo) $display("assertion failed");
> //simulation solution if (!foo) $error("assertion
>failed") ;
> .
> end
> end
> endcase
>
>In our experience, such specification has been encountered numerous
>times.
>
>If we change the evaluation semantics such that the first element of a
>sequence in a procedural assertion is evaluated right away, we can get
>rid of this limitation. However, that can cause false firing of assertions
>in combinational blocks. The way around that will be to employ the
>methodology that procedural assertions in combinational blocks begin
>with true. The user has to code that explicitly.
>
>However, this will cause serious mismatch between cycle based and
>event driven evaluation semantics. Cycle based semantics can't
>schedule an intra-cycle evaluation.
>
>If we get rid of check, we will leave a permanent hole. This is a
>corner case situation.
>
>Best Regards,
>
>Prakash
**********************************************
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 : Sun Feb 16 2003 - 11:12:44 PST