[sv-ac] Feedback on Mantis 2005 Proposal

Have not seen this show up on reflector yet, so I'm re-sending.

Tom

-------- Original Message --------
Subject: Feedback on Mantis 2005 Proposal
Date: Mon, 17 Sep 2007 10:43:04 -0700
From: Thomas Thatcher <thomas.thatcher@sun.com>
Reply-To: Thomas.Thatcher@Sun.COM
To: sv-ac@eda-stds.org

Hello Everyone,

I have read through the proposal.  Here are my comments.

First of all, the changes to unique and priority would have to be approved by
BC.  But even so, the proposed change will not be backward compatible, and
will create confusion.  I read the proposal as "if the unique/priority occurs
in a place where concurrent assertions are illegal, then it behaves like an
immediate assertion.  Otherwise, it behaves as a concurrent assertion."  This
creates too much confusion for a small amount of benefit.


Next, I don't see the necessity of the first change in 16.14.5.  The new text:

"If the clock is explicity specified with a property, it can be different from
the inferred clock as shown below:"

To me this seems like giving users rope to hang themselves with.


Next, On the case statement example

	reg [1:0] a = 2'b00;
	always @(posedge clk) begin
	    a = 2'b00;
	    a1: assert property(a == 2'b00);
	    a = 2'b11;
	    a2: assert property(a == 2'b11);
	end

I don't see how this is going to work.  Concurrent assertions always use the
sampled value of the signal.  Thus one or both of the two assertions above
should fail, regardless of the enabling conditions, because they are going to
get the previous value of a, before the assignment takes place.  Even after
the shadow variable explanation, the code still doesn't work.

	reg [1:0] a = 2'b00;
	bit shadow_a1;
	bit shadow_a2;
	always @(posedge clk) begin
	    a = 2'b00;
	    shadow_a1 = ((a == 2'b00) != 'b0);
	    a = 2'b11;
	    shadow_a2 = ((a == 2'b11) != 'b0);
	end
	    a1: assert property(@(posedge clk) shadow_a1);
	    a2: assert property(@(posedge clk) shadow_a2);

The assert properties get the values of shadow_a1 and shadow_a2 from the
preponed region, before they are ever assigned.

If you are proposing a change to the scheduling semantics for concurrent
assertions, then I am completely opposed.  We want to avoid at all costs
having things work one way in one context and a different way in a different
context.

I think that this mantis item should be indefinitely postponed, until we can
come up with a proposal that doesn't cause worse problems than it solves.

Tom
-- 
------------------
Thomas J. Thatcher
Sun Microsystems
408-616-5589
------------------


-- 
------------------
Thomas J. Thatcher
Sun Microsystems
408-616-5589
------------------

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.