0002483: Some small changes required for LRM to be self-consistent after proposal 2398

EDA.org Mantis

Viewing Issue Simple Details [ Jump to Notes ] [ Wiki ]

[ View Advanced ] [ Issue History ] [ Print ]

Category

Severity

Date Submitted

Last Update

0002483

[SystemVerilog P1800] SV-SC

major

2008-09-23 09:54

2008-10-08 16:05

Reporter

Erik_Seligman

View Status

public

Assigned To

Priority

urgent

Resolution

fixed

Status

closed

Product Version

P1800-2009/D7

Summary

0002483: Some small changes required for LRM to be self-consistent after proposal 2398

Description

Two issues were identified during Draft 7 reviews, where small parts of the LRM no longer make sense in light of 2398.

1. 16.5, p.315, top: The paragraph at the top, "The values of variables... (RTL) description", has an editorial note "Is this cross reference correct?" In fact it isn't-- it's referring to proposal 1995, our original proposal to enable looped concurrent assertions, which was superseded by the more general 2398. Furthermore, since this paragraph is redundant with the following one ("All variables in a concurrent assertion...") which was introduced by 2398, only the one in 2398 should be kept. Thus, we should delete this top paragraph on p.315.

2. SV-AC noticed a part at the end of section 16.16 (p. 417 of Draft 7) that reads:

-------------------------
// Only enable condition and clocking event are inferred from an always
// block always procedure. Assertion a8 is equivalent to
// assert property (@(posedge clk) !bit'(rst!='b0) |-> (a |=> b));
always @(posedge clk or posedge rst)
if (rst)
...
else begin
a8 : assert property (a |=> b);
...
end
endmodule
In assertion a8 the inferred enabling condition is from the else clause of the if-else statement, and thus it has to represent the complementary interpretation of the four-valued expression in the if condition. One such form is as indicated in the comment above a8. Other equivalent forms may be used, such as ((rst !='b0) !== 1'b1).
-------------------------------

Since this proposal eliminated the inferred enabling condition, all the text quoted above (the final section of the example + the paragraph below) needs to be removed, and replaced with a simple 'endmodule' to end the example.

Additional Information

Tags

No tags attached.

Type

Errata

Attached Files

svsc2483.pdf [^] (30,216 bytes) 2008-09-23 13:22

Relationships

related to	0001995	closed	Erik_Seligman	Allow concurrent assertions in for loops
related to	0002398	closed	Erik_Seligman	More consistent semantics for concurrent assertions in procedural code

Notes
(0007594) Erik_Seligman (developer) 2008-10-06 09:41	Passed by sv-sc email vote ending 10/6/08: 6y, 0n.

(0007595) Erik_Seligman (developer) 2008-10-06 09:42	Passed by sv-sc email vote ending 10/6/08: 6y, 0n.

(0007607) Neil Korpusik (administrator) 2008-10-08 16:04	The Editor has already made this set of changes as part of Editorial changes for 2398. Closing this mantis item.

Issue History
Date Modified	Username	Field	Change
2008-09-23 09:54	Erik_Seligman	New Issue
2008-09-23 09:54	Erik_Seligman	Type	=> Errata
2008-09-23 13:22	Erik_Seligman	File Added: svsc2483.pdf
2008-09-26 03:03	shalom	Issue Monitored: shalom
2008-09-26 03:03	shalom	Relationship added	related to 0001995
2008-09-26 03:04	shalom	Relationship added	related to 0002398
2008-10-06 09:41	Erik_Seligman	Note Added: 0007594
2008-10-06 09:42	Erik_Seligman	Note Added: 0007595
2008-10-06 09:42	Erik_Seligman	Status	new => resolved
2008-10-06 09:42	Erik_Seligman	Resolution	open => fixed
2008-10-08 16:04	Neil Korpusik	Status	resolved => closed
2008-10-08 16:04	Neil Korpusik	Note Added: 0007607

Mantis 1.1.7[^]