Subject: Re: [sv-ac] The case for retaining check
From: Stephen Meier (Stephen.Meier@synopsys.com)
Date: Sun Feb 16 2003 - 15:10:20 PST
Cindy:
Yes agreed that getting rid of check leaves a hole in immediate checking.
Your proposal of using unclocked assert statements has been discussed in
DWG previously and discarded.
The reason is that when unclocked assertions appear in procedural
context then their sampling clock is inferred from context. Thus when
you write assert without an explicit clock it would be ambiguous between
an inferred clock and an unclocked assertion. The check vs. assert
distinction is required in order to explicitly declare an unclocked assertion.
Additionally it was our goal to clearly distinguish and have clear partition
between concurrent assertions and immediate assertions. A clear distinction
is needed as the scheduling and sampling are quite distinct. I would expect
that most cycle based tools (testbench, formal) would not implement the
immediate assertion. If they had the same keyword there could easily be
confusion between scheduling mechansim and tool support.
Regards,
Steve
=====
At 05:11 PM 2/16/2003 +0200, Cindy Eisner 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
Steve Meier (stephen.meier@synopsys.com) W: 650-584-4476, Cell: 408-393-8246
This archive was generated by hypermail 2b28 : Sun Feb 16 2003 - 15:11:05 PST