Subject: Re: [sv-ac] The case for retaining check
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Sun Feb 16 2003 - 07:11:16 PST
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
This archive was generated by hypermail 2b28 : Sun Feb 16 2003 - 07:08:26 PST