Jacob,
Do we have time to address the concurrent assertions in procedural code.
That needs to be addressed as it is unclear now.
For the record, I changed the always_comb to always @ (a or b or c or clk)
to see the results.
Am curious as to why I got 3 action block messages instead of one. Any
idea?
module try();
logic clk=0, a=0, b=0, c=0;
initial #400 $finish;
initial forever #20 clk = ~clk;
always @ (posedge clk) begin
$display("INFO_clk: time=%t, current a=%b, sampled a=%b, \
current b=%b, sampled b=%b",
$time, a, $sampled(a), b, $sampled(b));
#2 b <= !b;
end
initial begin
#20;
#40 a = 0;
#40 a = 1;
end
always @ (a or b or c or clk) begin
if (a)
a1: assert property (@(posedge clk) b == c)
$display("a1_PASS: time=%t, current a=%b, sampled a=%b, \
current b=%b, sampled b=%b",
$time, a, $sampled(a), b, $sampled(b));
else
$display("a1_FAIL: time=%t, current a=%b, sampled a=%b, \
current b=%b, sampled b=%b",
$time, a, $sampled(a), b, $sampled(b));
end
endmodule
run 300ns
# INFO_clk: time= 20, current a=0, sampled a=0,
current b=0, sampled b=0
# INFO_clk: time= 60, current a=0, sampled a=0,
current b=1, sampled b=1
# INFO_clk: time= 100, current a=1, sampled a=0,
current b=0, sampled b=0
# a1_PASS: time= 100, current a=1, sampled a=0,
current b=0, sampled b=0
# INFO_clk: time= 140, current a=1, sampled a=1,
current b=1, sampled b=1
*# a1_FAIL: time= 140, current a=1, sampled a=1,
current b=1, sampled b=1*
*# a1_FAIL: time= 140, current a=1, sampled a=1,
current b=1, sampled b=1*
*# a1_FAIL: time= 140, current a=1, sampled a=1,
current b=1, sampled b=1*
# INFO_clk: time= 180, current a=1, sampled a=1,
current b=0, sampled b=0
# a1_PASS: time= 180, current a=1, sampled a=1,
current b=0, sampled b=0
# a1_PASS: time= 180, current a=1, sampled a=1,
current b=0, sampled b=0
# a1_PASS: time= 180, current a=1, sampled a=1,
current b=0, sampled b=0
# INFO_clk: time= 220, current a=1, sampled a=1,
current b=1, sampled b=1
# a1_FAIL: time= 220, current a=1, sampled a=1,
current b=1, sampled b=1
# a1_FAIL: time= 220, current a=1, sampled a=1,
current b=1, sampled b=1
# a1_FAIL: time= 220, current a=1, sampled a=1,
current b=1, sampled b=1
# INFO_clk: time= 260, current a=1, sampled a=1,
current b=0, sampled b=0
# a1_PASS: time= 260, current a=1, sampled a=1,
current b=0, sampled b=0
# a1_PASS: time= 260, current a=1, sampled a=1,
current b=0, sampled b=0
# a1_PASS: time= 260, current a=1, sampled a=1,
current b=0, sampled b=0
# INFO_clk: time= 300, current a=1, sampled a=1,
current b=1, sampled b=1
# a1_FAIL: time= 300, current a=1, sampled a=1,
current b=1, sampled b=1
# a1_FAIL: time= 300, current a=1, sampled a=1,
current b=1, sampled b=1
# a1_FAIL: time= 300, current a=1, sampled a=1,
current b=1, sampled b=1
On Mon, Sep 26, 2011 at 11:09 AM, Katz, Jacob <jacob.katz@intel.com> wrote:
> I think that one certain outcome of this discussion is that the current
> proposal for 3564 should only talk about immediate assertions and say
> nothing about concurrent. Scheduling semantics of concurrent assertions in
> procedural code (not only always_comb) should probably be addressed
> separately…****
>
> ** **
>
> --------------------------------****
>
> *Jacob M. Katz* | jacob.katz@intel.com | *Work:* +972-4-865-5726 | *iNet:
> *(8)-465-5726****
>
> ** **
>
> *From:* owner-sv-bc@eda.org [mailto:owner-sv-bc@eda.org] *On Behalf Of *ben
> cohen
> *Sent:* Monday, September 26, 2011 21:01
>
> *To:* Prabhakar, Anupam
> *Cc:* Korchemny, Dmitry; Steven Sharp; sv-ac@eda.org; sv-bc@eda.org;
> stuart@sutherland-hdl.com; Cliff Cummings; mills@lcdm-eng.com; Seligman,
> Erik
> *Subject:* {Disarmed} [sv-bc] {Disarmed} Re: [sv-ac] RE: Call to vote: Due
> September 26****
>
> ** **
>
> One more note because I tried something else, and the tool did not seem to
> respond the the leading clocking event sensitivity list. ****
>
> module try();****
>
> logic clk=0, a=0, b=0, c=0;****
>
> initial #400 $finish; ****
>
> initial forever #20 clk = ~clk;****
>
> always @ (posedge clk) begin ****
>
> $display("INFO_clk: time=%t, current a=%b, sampled a=%b, \****
>
> current b=%b, sampled b=%b", ****
>
> $time, a, $sampled(a), b, $sampled(b));****
>
> #2 b <= !b; ****
>
> end ****
>
> initial begin****
>
> #20;****
>
> #40 a = 0;****
>
> #40 a = 1;****
>
> end****
>
> always_comb begin****
>
> if (a)****
>
> a1: assert property (@(posedge clk) b == c) ****
>
> $display("a1_PASS: time=%t, current a=%b, sampled a=%b, \*
> ***
>
> current b=%b, sampled b=%b", ****
>
> $time, a, $sampled(a), b, $sampled(b));****
>
> else ****
>
> $display("a1_FAIL: time=%t, current a=%b, sampled a=%b, \*
> ***
>
> current b=%b, sampled b=%b", ****
>
> $time, a, $sampled(a), b, $sampled(b));****
>
> end****
>
> endmodule****
>
> // remember that* c==0 all the time. *****
>
> un 300ns****
>
> # INFO_clk: time= 20, current a=0, sampled a=0,
> current b=0, sampled b=0****
>
> # INFO_clk: time= 60, current a=0, sampled a=0,
> current b=1, sampled b=1****
>
> #* INFO_clk: time= 100, current a=1, sampled a=0,
> current b=0, sampled b=0*****
>
> # a1_PASS: time= 100, current a=1, sampled a=0,
> current b=0, sampled b=0****
>
> #* INFO_clk: time= 140, current a=1, sampled a=1,
> current b=1, sampled b=1*****
>
> *// [Ben] Should have failed here, a==1, b==1, c==0 TOOL DID NOT
> TRIGGER *****
>
> *# INFO_clk: time= 180, current a=1, sampled a=1,
> current b=0, sampled b=0*****
>
> *// [Ben] should have passed here, a==1, b==0, c==0 **TOOL DID NOT
> TRIGGER *****
>
> # INFO_clk: time= 220, current a=1, sampled a=1,
> current b=1, sampled b=1****
>
> # INFO_clk: time= 260, current a=1, sampled a=1,
> current b=0, sampled b=0****
>
> # INFO_clk: time= ****
>
> How about something like the following: ****
>
> Expressions used in immediate assertions (see 16.3), within the block or
> within any function called within the block, also contribute to the implicit
> sensitivity list of an always_comb. Expressions used in concurrent
> assertions (see 16.5) do not contribute to the implicit sensitivity list of
> an always_comb, *with the exception of the leading clocking event
> specified in the concurrent assertions. Note that caution need to be
> exercised because the the triggering condition for the concurrent assertions
> are evaluated in the Active region, whereas the variables used in the
> concurrent assertions are sampled in the Preponed region. *****
>
> *[Ben] This is a change to whatever the current tool I a using is doing.
> The current tool fires only when the always_comb triggers, then uses the
> current triggering conditions, and if a pass, then used the sampled values
> of the properties to evaluate the assertion. *****
>
> *A big mess. we need to clarify this, one way or the other. *****
>
> Ben ****
>
> ** **
>
> ** **
>
> On Mon, Sep 26, 2011 at 10:40 AM, ben cohen <hdlcohen@gmail.com> wrote:***
> *
>
> Jacob, I modified your code as follows and I have some concerns. ****
>
> module try();****
>
> logic clk=0, a=0, b=1, c=0;****
>
> initial #200 $finish;****
>
> initial forever #20 clk = ~clk;****
>
> initial begin****
>
> #20;****
>
> #40 a = 0;****
>
> #40 a = 1;****
>
> end****
>
> always_comb begin****
>
> if (a)****
>
> a1: assert property (@(posedge clk) b == c) else ****
>
> $display("a1 FAIL: time=%t, current a=%b, sampled a=%b", *
> ***
>
> $time, a, $sampled(a));****
>
> end****
>
> endmodule****
>
> Simulation results with one tool: ****
>
> run 150ns****
>
> # a1 FAIL: time= 100, current a=1, sampled a=0****
>
> In this example, "a" is evaluated to true in the active region, and the
> assertion takes the current value of "a" to evaluate its properties. ****
>
> ** **
>
> I then tried the following example to determine if the tool takes
> the sampled or current value of "b" ****
>
> module try2();****
>
> logic clk=0, a=0, b=0, c=0;****
>
> initial #200 $finish;****
>
> initial forever #20 clk = ~clk;****
>
> always @ (posedge clk) b <= !b; ****
>
> initial begin****
>
> #20;****
>
> #40 a = 0;****
>
> #40 a = 1;****
>
> end****
>
> always_comb begin****
>
> if (a)****
>
> a1: assert property (@(posedge clk) b == c) ****
>
> $display("a1_PASS: time=%t, current a=%b, sampled a=%b, \****
>
> current b=%b, sampled b=%b", ****
>
> $time, a, $sampled(a), b, $sampled(b));****
>
> else ****
>
> $display("a1_FAIL: time=%t, current a=%b, sampled a=%b, \*
> ***
>
> current b=%b, sampled b=%b", ****
>
> $time, a, $sampled(a), b, $sampled(b));****
>
> end****
>
> endmodule****
>
> Sim results: run 150ns****
>
> # a1_PASS: time= 100, current a=1, sampled a=0,
> current b=1, sampled b=0****
>
> ** **
>
> *Bottom line: This tool takes the "actual" values evaluated in the Active
> region ("a" in this case), and uses that new result along with the sampled
> values of the property variables ("b" and "c" in the Preponed region). ***
> **
>
> Thus, it is NOT correct to say that ****
>
> always_comb begin****
>
> if (a)****
>
> a1: assert property (@(posedge clk) b == c); ****
>
> is same as ****
>
> a1b: assert property(@ (posedge clk) a |-> b==c);****
>
> *They ARE NOT the same because in a1b the the property variables are
> sampled in the Preponed region, whereas in the always_comb,
> the triggering conditions that enable the assertion are evaluated in the
> Active region. *****
>
> ** **
>
> So where do we go from here? How about something like the following: ***
> *
>
> Expressions used in immediate assertions (see 16.3), within the block or
> within any function called within the block, also contribute to the implicit
> sensitivity list of an always_comb. Expressions used in concurrent
> assertions (see 16.5) do not contribute to the implicit sensitivity list of
> an always_comb, *with the exception of the leading clocking event
> specified in the concurrent assertions. Note that caution need to be
> exercised because the the triggering condition for the concurrent assertions
> are evaluated in the Active region, whereas the variables used in the
> concurrent assertions are sampled in the Preponed region. *****
>
> Ben Cohen ****
>
> ** **
>
> In the example below, the always_comb shall trigger whenever b,c or e
> change.****
>
> ** **
>
> ** **
>
> On Mon, Sep 26, 2011 at 9:27 AM, Prabhakar, Anupam <
> anupam_prabhakar@mentor.com> wrote:****
>
> Hi Dmitry,****
>
> ****
>
> I disagree with your requirement to write deferred assertions outside the
> process.****
>
> AP: Absolutely – a deferred assertion should be embedded in the process in
> normal cases. I was only referring to the ones which reference a variable,
> let’s say, ‘x’ which is not otherwise used in that process. My argument is
> that you probably will have a similar assertion written in the other process
> which modifies ‘x’ also. The other option is to pull the assertion out and
> write it separately and I agree that this might not be convenient. ****
>
> ****
>
> The nesting of the code where a deferred assertion is written may be very
> deep (as I tried to emulate in my example), and an attempt to write the
> assertion outside the process will require huge code duplication and
> rewriting of procedural code in the form of generate blocks. I saw many such
> examples of nested deferred assertions in real life designs.****
>
> AP: Are you are saying that you find assertions that refer to variables not
> otherwise used in that process very common in real life designs ?****
>
> The reason you want that immediate assertion should contribute to the
> sensitivity of always_comb is only to evaluate the assertion itself and
> ‘hope’ there is no side-effect of the whole always_comb getting evaluated
> again. This might be true in most of the cases but I will be very careful
> when making this assumption. What about simple cases where there is a
> $display. You turn off assertions using $assertoff and your output
> references change.****
>
> There will be trade-offs no matter what we decide here – we will need to
> decide which problem we want to solve.****
>
> ****
>
> Anupam****
>
> ****
>
> *From:* Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com]
> *Sent:* Sunday, September 25, 2011 11:52 PM****
>
>
> *To:* Prabhakar, Anupam; Steven Sharp; sv-ac@eda.org; sv-bc@eda.org
> *Cc:* stuart@sutherland-hdl.com; Cliff Cummings; mills@lcdm-eng.com;
> Seligman, Erik
> *Subject:* RE: [sv-ac] RE: Call to vote: Due September 26****
>
> ****
>
> Hi Anupam,****
>
> ****
>
> I agree with your first comment and with your statement that in the normal
> case there is no side effect introduced by an immediate assertion. The
> behavior of the code snippet in 3564 is nondeterministic even in the
> absence of the assertion since it depends on the number of the block
> relaxations in a timestep:****
>
> ****
>
> always_comb****
>
> begin****
>
> if (a == 1)****
>
> ahigh++;****
>
> assert(b == 0);****
>
> end****
>
> ****
>
> Such pathological constructs are ruled out by the vague LRM statement
> “Software tools should perform additional checks to warn if the behavior
> within an always_comb procedure does not represent combinational logic, such
> as if latched behavior can be inferred.” (9.2.2.2).****
>
> ****
>
> I disagree with your requirement to write deferred assertions outside the
> process. The nesting of the code where a deferred assertion is written may
> be very deep (as I tried to emulate in my example), and an attempt to write
> the assertion outside the process will require huge code duplication and
> rewriting of procedural code in the form of generate blocks. I saw many such
> examples of nested deferred assertions in real life designs.****
>
> ****
>
> Thanks,****
>
> Dmitry****
>
> ****
>
> *From:* Prabhakar, Anupam [mailto:anupam_prabhakar@mentor.com]
> *Sent:* Sunday, September 25, 2011 23:45
> *To:* Korchemny, Dmitry; Steven Sharp; sv-ac@eda.org; sv-bc@eda.org
> *Cc:* stuart@sutherland-hdl.com; Cliff Cummings; mills@lcdm-eng.com;
> Seligman, Erik
> *Subject:* RE: [sv-ac] RE: Call to vote: Due September 26****
>
> ****
>
> Hi Dmitry,****
>
> ****
>
> Please see my comments below.****
>
> ****
>
> Anupam****
>
> ****
>
> *From:* Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com]
> *Sent:* Sunday, September 25, 2011 12:16 PM
> *To:* Prabhakar, Anupam; Steven Sharp; sv-ac@eda.org; sv-bc@eda.org
> *Cc:* stuart@sutherland-hdl.com; Cliff Cummings; mills@lcdm-eng.com;
> Seligman, Erik
> *Subject:* RE: [sv-ac] RE: Call to vote: Due September 26****
>
> ****
>
> Hi Anupam,****
>
> ****
>
> Please, ignore my previous answer to this mail, I missed the point that you
> were talking about immediate assertions and sent an answer about concurrent
> ones.****
>
> ****
>
> One simple example is the definition of a standalone deferred assertion: an
> immediate assertion incorporated into an always_comb block. Had always_comb
> been non-sensitive to the assertion expression, this definition would be
> meaningless.****
>
> AP : I think this definition can simply be re-worded without any change in
> functionality.****
>
> ****
>
> Another example is the case when an embedded assertion depends on some
> external signal that may change independently. E.g.,****
>
> ****
>
> always_comb begin****
>
> if (a) begin****
>
> for (int i = 0; i < 8: i++) begin****
>
> en[i] = …;****
>
> assert #0 (en[i] -> x[i]);
> // x is assigned in a different process; This assertion should be checked
> also when x changes****
>
> AP : Even if we make always_comb sensitive to ‘x’ the assert is still gated
> by ‘a’. Would you also put another assert #0 (en[i] -> x[i]) in the process
> that assigns ‘x’ ? For such dependencies it might be best to keep the
> deferred assert outside the processes which assign ‘en’ and ‘x’, especially
> since the LRM does not limit writing a deferred only in procedural blocks.
> In any case what I was looking for was an example where not including the
> immediate assert expression causes undesired behavior other than evaluation
> of the assertion itself. ****
>
> ****
>
> …****
>
> ****
>
> Thanks,****
>
> Dmitry****
>
> ****
>
> *From:* Prabhakar, Anupam [mailto:anupam_prabhakar@mentor.com]
> *Sent:* Saturday, September 24, 2011 07:34
> *To:* Steven Sharp; sv-ac@eda.org; sv-bc@eda.org
> *Cc:* stuart@sutherland-hdl.com; Cliff Cummings; mills@lcdm-eng.com;
> Korchemny, Dmitry; Seligman, Erik
> *Subject:* RE: [sv-ac] RE: Call to vote: Due September 26****
>
> ****
>
> One reasoning to not add the expression in an immediate assertion to
> always_comb sensitivity is that an assertion should be considered as an
> observer (rather than a contributor. At the same time the result of an
> always_comb should not depend on whether immediate assertion expression
> participates on not – except in some weird cases (like the example I wrote
> in mantis 3564). I would be interested to see a case where not including
> immediate assertion expression can lead to undesired behavior – maybe
> Dmitry/Eric can provide one.****
>
> ****
>
> Anupam****
>
> ****
>
> *From:* Steven Sharp [mailto:sharp@cadence.com]
> *Sent:* Friday, September 23, 2011 5:33 PM
> *To:* Prabhakar, Anupam; sv-ac@eda.org; sv-bc@eda.org
> *Subject:* RE: [sv-ac] RE: Call to vote: Due September 26****
>
> ****
>
> If I understand procedural concurrent assertions correctly, the always_comb
> doesn’t evaluate them, but rather launches a concurrent subprocess that goes
> off and check them. As a result, I would not expect them to add anything to
> the sensitivity of the always_comb. If fork..join_none were allowed in
> always_comb, I would expect the same thing for any subprocesses that it
> launched. Or taking the example of fork..join_none, perhaps concurrent
> assertions should be illegal in always_comb. I don’t see what reasonable
> purpose they serve there, and I suspect that they would lead to other
> problems besides the issue of the sensitivity list.****
>
> ****
>
> However, I disagree with Stu about immediate assertions. These are
> evaluated by the always_comb process itself. They are equivalent to an
> if-statement that produces an error and/or executes some code if the
> condition is not met. If such a construct were coded directly, it would add
> to the sensitivity list, so why shouldn’t the immediate assertion? Stu has
> acknowledged that not adding it to the sensitivity list would create a
> problem, for which he suggests that a cautionary note would be adequate.
> However, he has not pointed out any situation where adding it to the
> sensitivity list creates a problem. This might cause extra evaluations
> which serve only to check the immediate assertion without any possibility of
> changing an output, but this doesn’t appear to cause any problem other than
> some simulation cost. I don’t see how this could lead to mismatches between
> RTL simulation and synthesized hardware (for things other than the
> assertions themselves, which are not synthesizable).****
>
> ****
>
> ****
>
> *From:* owner-sv-bc@eda.org [mailto:owner-sv-bc@eda.org] *On Behalf Of *Prabhakar,
> Anupam
> *Sent:* Friday, September 23, 2011 5:46 PM
> *To:* sv-ac@eda.org; sv-bc@eda.org
> *Subject:* [sv-bc] FW: [sv-ac] RE: Call to vote: Due September 26****
>
> ****
>
> Including SV-BC for a wider audience ….****
>
>
> -----------------------------------------------------------------------------------------------------------------
> ****
>
> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *Stuart
> Sutherland
> *Sent:* Friday, September 23, 2011 2:26 PM
> *To:* 'Samik Sengupta'; 'Seligman, Erik'; sv-ac@eda-stds.org
> *Cc:* Cliff Cummings; mills@lcdm-eng.com
> *Subject:* RE: [sv-ac] RE: Call to vote: Due September 26 (resend with the
> correct Mantis number)****
>
> ****
>
> In my opinion, even adding the condition(s) of an immediate assertion to
> the always_comb (or always_latch) sensistivity list is a BAD IDEA! It will
> force engineers to go back to the old days of having to deal with simulation
> and synthesis seeing very different things in the same block of code, and
> will lead to mismatches in RTL simulation and synthesized hardware. It is
> nasty, dangerous, and can risk expensive re-spins of a chip. Don’t mess
> with the rules of inferred sensivity!!!!****
>
> ****
>
> I would much rather see a rule in the standard that any type of assertion
> in always_comb and always_latch does not affect the inferred sensitivity
> list in any way. A cautionary note would be appropriate that if the
> immediate assertion reads an expression that are not read elsewhere in the
> procedure, the immediate assertion will not be evaluated when that
> expression changes value.****
>
> ****
>
> Again, I am copying Cliff and Don, in case fellow real designers think I am
> off base.****
>
> ****
>
> Stu****
>
> ****
>
> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *Stuart
> Sutherland
> *Sent:* Friday, September 23, 2011 2:10 PM
> *To:* sv-ac@eda-stds.org
> *Cc:* Cliff Cummings; mills@lcdm-eng.com
> *Subject:* RE: [sv-ac] RE: Call to vote: Due September 26****
>
> ****
>
> From both a SystemVerilog and SVA user and an SVA instructor point of view…
> ****
>
> ****
>
> Adding the clock event to the sensitivity list of an always_comb would be a
> likely source of simulation and synthesis and real hardware mismatches. It
> is a horrible idea. The goal when always_comb was added to the language –
> in the days of Superlog, long before Verilog++ or SystemVerilog, and long
> before the AC committee got involved with the language – was to make
> simulation and synthesis as closely aligned as reasonable. ****
>
> ****
>
> Please do no mangle the rules of always_comb for purposes that are not in
> line with the intent of the construct! ****
>
> ****
>
> If you need to add special rules for concurrent assertion behavior in an
> always_comb block, specify those rules on the assert property statement, not
> on always_comb. For example, you could define rules that an assert property
> in any type of always block will run as a parallel background task with its
> own sensitivity list, where perhaps __some__ of the assertion’s sensitivity
> was inferred from the always procedure context but is totally independent of
> the always procedure sensitivity list.****
>
> ****
>
> I am copying Cliff Cummings and Don Mills on this message, two former SV
> committee members and engineers with a good understanding of the purpose of
> always_comb, always_latch, and always_ff and why we wanted them in
> SystemVerilog. I hope they will respond and let me know if I am off base on
> my adamant opposition to concurrent assertions affecting the inferred
> sensitivity list.****
>
> ****
>
> Stu
> ~~~~~~~~~~~~~~~~~~~~~~~~~~~
> Stuart Sutherland****
>
> Sutherland HDL, Inc.****
>
> *MailScanner has detected a possible fraud attempt from
> "stuart@sutherland-hdl.com" claiming to be* *MailScanner has detected a
> possible fraud attempt from "stuart@sutherland-hdl.com" claiming to be*stuart@sutherland-hdl.com<http://stuart@sutherland-hdl.com>
> ****
>
> 503-692-0898
> www.sutherland-hdl.com ****
>
> ****
>
> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *Korchemny,
> Dmitry
> *Sent:* Friday, September 23, 2011 4:27 AM
> *To:* ben@systemverilog.us; Eduard Cerny
> *Cc:* Seligman, Erik; sv-ac@eda-stds.org
> *Subject:* RE: [sv-ac] RE: Call to vote: Due September 26****
>
> ****
>
> Hi Ben,****
>
> ****
>
> Your example does not agree with the position of Ed, Anupam and Manisha.**
> **
>
> ****
>
> IMO a procedural concurrent assertion should be evaluated at each clock
> tick when its enabling condition is active. In Ben’s example I would expect
> that the new attempt of b |=> d is checked each time when its enabling
> condition a is asserted. Therefore, if a is always 1 this assertion should
> be equivalent to assert property(@ (posedge clk) b|=> d);****
>
> ****
>
> If we adopt the opposite point of view that the clocking event of the
> concurrent assertion does not belong to the sensitivity list then we will
> have the embedded assertion roughly equivalent to:****
>
> ****
>
> assert property(@ (posedge clk) $rose(a) |-> b|=> d);****
>
> ****
>
> which does not seem to be very useful.****
>
> ****
>
> Inserting the clocking event into the sensitivity list of the procedure
> should not be very expensive in simulation. The simulator may cache the
> latest value of the context of the concurrent assertion and not to
> reevaluate the entire procedure on the rising edge of the clock, i.e.
> actually not to include the clocking event into the sensitivity list.****
>
> ****
>
> Thanks,****
>
> Dmitry****
>
> ****
>
> *From:* ben cohen [mailto:hdlcohen@gmail.com]
> *Sent:* Wednesday, September 21, 2011 20:13
> *To:* Eduard Cerny
> *Cc:* Seligman, Erik; Korchemny, Dmitry; sv-ac@eda-stds.org
> *Subject:* Re: [sv-ac] RE: Call to vote: Due September 26****
>
> ****
>
> I agree with Ed and Anupam. Below is code that I tested with a simulator.
> In the always_comb, I have: ****
>
> if(a) ****
>
> ap_conc: assert property(@ (posedge clk) b|=> d) else
> $display("ap_coc error");****
>
> The simulator behaved as the following ****
>
> ****
>
> ap_conc_equivalent: assert property(@ (posedge clk) *if(a)* b|=> d) else
> $display("ap_coc error");****
>
> ****
>
> module test_abcde; ****
>
> logic clk=0, a=0, b=1, c=1, d=0, e=0; ****
>
> initial forever #10 clk=!clk; ****
>
> ****
>
> // always @ (posedge clk) b <= !b; ****
>
> initial begin ****
>
> #2 e=1'b1; ****
>
> #3 e=1'b0; ****
>
> #7 e=1'b1; ****
>
> #23 b=1'b0;****
>
> #40 b=1'b1; ****
>
> #27 c=1'b0; ****
>
> end ****
>
> ****
>
> always_comb****
>
> begin****
>
> a = b & c;****
>
> ap: assert (a != e) else $display("ap error");****
>
> if(a) ****
>
> ap_conc: assert property(@ (posedge clk) b|=> d) else
> $display("ap_coc error");****
>
> end****
>
> endmodule ****
>
> ****
>
> Ben Cohen ****
>
> ****
>
> On Wed, Sep 21, 2011 at 8:46 AM, Eduard Cerny <Eduard.Cerny@synopsys.com>
> wrote:****
>
> I am also a little confused what we are voting on, 2093 or 3564. Regarding
> 3564, my thought is as follows:****
>
> for immediate, deferred and final assertions, only variables in the
> condition of the assertion should contribute to the sensitivity list, not
> those appearing in the action blocks. For concurrent assertions, IMHO they
> should not contribute in any way to the sensitivity list. An attempt is
> enabled when control reaches the location of the assertion in the
> always_comb procedure and then they run totally independently of the always,
> on their own clock. None of the variables in the assertion has anything to
> do with the actual evaluation of the always_comb. ****
>
> ****
>
> Best regards,****
>
> ed****
>
> ****
>
> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *Seligman,
> Erik
> *Sent:* Wednesday, September 21, 2011 11:34 AM
> *To:* Korchemny, Dmitry; sv-ac@eda-stds.org
> *Subject:* [sv-ac] RE: Call to vote: Due September 26****
>
> ****
>
> I assume we’re really voting on 3564, not 2093?****
>
> ****
>
> I vote NO on 3564. Reasoning: The current proposal explicitly states
> that expressions in concurrent assertions do not wake up the always_comb,
> but I don’t believe this is a correct solution. As an RTL author, I would
> want the always_comb to wake up at some point soon after any changes to the
> sampled expression, as well as any time a const’ expression changes. ***
> *
>
> ****
>
> Since we agreed that more time is needed for a clean definition of behavior
> under concurrent assertions, we should just talk about immediate assertions
> in this proposal, and leave the concurrent case undefined (which we will fix
> in the next PAR). So I would rewrite the proposal as:****
>
> ****
>
> Expressions used in immediate assertions (see 16.3), within the block or
> within any function called within the block, also contribute to the implicit
> sensitivity list of an *always_comb**. * In the example below, the *always_comb
> *shall trigger whenever b,c or e change.****
>
> ****
>
> *always_comb *****
>
> *begin *****
>
> a = b & c; ****
>
> * assert *(a != e); ****
>
> *end*****
>
> ****
>
> ****
>
> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *Korchemny,
> Dmitry
> *Sent:* Tuesday, September 20, 2011 11:55 PM
> *To:* sv-ac@eda-stds.org
> *Subject:* [sv-ac] Call to vote: Due September 26****
>
> ****
>
> -You have until 11:59 pm PDT, Monday, September 26, 2011 to respond****
>
> -An issue passes if there are zero NO votes and half of the eligible voters
> respond with a YES vote.****
>
> -If you vote NO on any issue, your vote must be accompanied by a reason. *
> ***
>
> The issue will then be up for discussion during a future conference call.*
> ***
>
> ****
>
> As of the September 20, 2011 meeting, the eligible voters are****
>
> ****
>
> Ashok Bhatt****
>
> Eduard Cerny****
>
> Ben Cohen****
>
> Dana Fisman****
>
> Tapan Kapoor****
>
> Jacob Katz****
>
> Scott Little****
>
> Manisha Kulshrestha****
>
> Anupam Prabhakar****
>
> Erik Seligman****
>
> Samik Sengupta****
>
> Tom Thatcher****
>
> ****
>
> Mantis 2093 ____ Yes ____ No****
>
> http://www.eda-stds.org/mantis/view.php?id=3564 <http://www.eda-stds.org/mantis/view.php?id=2093%20>
> ****
>
> http://www.eda-stds.org/mantis/file_download.php?file_id=5462&type=bug****
>
> ****
>
> ---------------------------------------------------------------------
> Intel Israel (74) Limited
>
> This e-mail and any attachments may contain confidential material for
> the sole use of the intended recipient(s). Any review or distribution
> by others is strictly prohibited. If you are not the intended
> recipient, please contact the sender and delete all copies.
> --
> This message has been scanned for viruses and
> dangerous content by *MailScanner* <http://www.mailscanner.info/>, and is
> believed to be clean. ****
>
>
> --
> This message has been scanned for viruses and
> dangerous content by *MailScanner* <http://www.mailscanner.info/>, and is
> believed to be clean. ****
>
>
> --
> This message has been scanned for viruses and
> dangerous content by *MailScanner* <http://www.mailscanner.info/>, and is
> believed to be clean. ****
>
> ****
>
> ---------------------------------------------------------------------
> Intel Israel (74) Limited
>
> This e-mail and any attachments may contain confidential material for
> the sole use of the intended recipient(s). Any review or distribution
> by others is strictly prohibited. If you are not the intended
> recipient, please contact the sender and delete all copies.
> --
> This message has been scanned for viruses and
> dangerous content by *MailScanner* <http://www.mailscanner.info/>, and is
> believed to be clean. ****
>
>
> --
> This message has been scanned for viruses and
> dangerous content by *MailScanner* <http://www.mailscanner.info/>, and is
> believed to be clean. ****
>
>
> --
> This message has been scanned for viruses and
> dangerous content by *MailScanner* <http://www.mailscanner.info/>, and is
> believed to be clean. ****
>
> ---------------------------------------------------------------------
> Intel Israel (74) Limited
>
> This e-mail and any attachments may contain confidential material for
> the sole use of the intended recipient(s). Any review or distribution
> by others is strictly prohibited. If you are not the intended
> recipient, please contact the sender and delete all copies.****
>
> ---------------------------------------------------------------------
> Intel Israel (74) Limited
>
> This e-mail and any attachments may contain confidential material for
> the sole use of the intended recipient(s). Any review or distribution
> by others is strictly prohibited. If you are not the intended
> recipient, please contact the sender and delete all copies.****
>
>
> --
> This message has been scanned for viruses and
> dangerous content by *MailScanner* <http://www.mailscanner.info/>, and is
> believed to be clean. ****
>
> ** **
>
> ** **
>
>
> --
> This message has been scanned for viruses and
> dangerous content by *MailScanner* <http://www.mailscanner.info/>, and is
> believed to be clean. ****
> ---------------------------------------------------------------------
> Intel Israel (74) Limited
>
> This e-mail and any attachments may contain confidential material for
> the sole use of the intended recipient(s). Any review or distribution
> by others is strictly prohibited. If you are not the intended
> recipient, please contact the sender and delete all copies.
>
-- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Mon Sep 26 11:17:38 2011
This archive was generated by hypermail 2.1.8 : Mon Sep 26 2011 - 11:17:47 PDT