0001995: Allow concurrent assertions in for loops

(0004188)
Erik_Seligman (developer)
2007-08-27 14:52

After some discussion, we decided to make this proposal just for the assertions-- a separate proposal (or an edit to 1900) will add this for checkers.

(0004304)
Steven Sharp (developer)
2007-09-07 21:21

The phrase "statically computable set of iterations" is not sufficiently restrictive or precise.

Many things could be theoretically possible to compute, but completely impractical in practice. If you want to allow this, you should require iterations that are straightforward to compute. You should have the same kind of limitations that generate loops have (e.g. the loop bounds and increment being constant expressions).

Note that there are a lot of constructs possible in Verilog procedural code that are not possible in generate loops, and you would need to account for these also. For example, a procedural loop can modify the loop counter inside the loop. The loop counter could be forced from elsewhere (including PLI), which would prevent the loop from operating normally. There are constructs which could cause early exit from the loop, such as break, return and disable.

(0004313)
Erik_Seligman (developer)
2007-09-10 08:58

I just uploaded a new version that attempts to address Steven's concerns.

(0005636)
John Havlicek (manager)
2007-12-25 09:41

2007-12-24: Passed by e-mail vote, 8y/0n/2a. There were no friendly amendments. There were comments from Shalom Bresticker.

(0005715)
John Havlicek (manager)
2008-01-15 17:40

Updated to address editorial comments from Shalom Bresticker. The updated version was approved by voice vote on 2008-01-15, 9y/0n/0a.

(0005831)
John Havlicek (manager)
2008-01-29 06:44

2008-01-28: e-mail ballot passed minor revisions based on comments from Manisha Kulshrestha, 8y/0n/2a.

(0005922)
shalom (manager)
2008-02-05 06:43

Uploaded new version from Erik responding to comments from John and from me as comments to email Champions' vote.

(0005956)
Neil Korpusik (administrator)
2008-02-08 19:03

The proposal failed in the Champions email vote
which ended on Feb 4th, 2008.

         Failed with 1 no-vote
         - Dave - This proposal is essentially creating a generate block within
           a procedural context. I'm fine with limiting this to assertion
           statements for now, but that does alleviate addressing all the
           issues surrounding generated code. For example each assertion
           statement is replicated in the loop (including nested loops) and a
           generate block label needs to be created for every instance of each.
           The loop iterator should be treated as a genvar constant within each
           instance of the assertion statement.

         - Shalom - note to the Editor:
           In "For loop control variable value 1, the assertion will pass, and
           the pass action block will be generated," change the last word
           to "executed".

         - John - friendly amendments:
            - Editorial: I think that the parenthetical exception in the
              change to 16.4 should be at the end of the sentence.

            - In the change to 16.14.3, I'm not sure that

                 shall count each possible set of loop control variable values
                 as one attempt

              is really clear. Based on the sentence that follows, I think
              that what is intended is something like

                 shall count distinct valuations of loop control variable
                 values as separate attempts

            - Editorial: At the bottom of p. 2, the comma following the bold
              courier "continue" should be in non-bold roman.

            - Editorial: Do not use smart quotes in the courier examples.

            - p. 3, change "generated" to "executed" in "the pass action block
              will be generated".

            - p. 4.
                 In the example above, ac1 will always be checking the sampled
                 value of variable ok. Since this will be equal to
                 (my_bits[3] == 0) by the end of any time step, it will always
                 pass

              The declaration and initialization of "ok" are not shown, so we
              do not know its sampled value in timesteps prior to and including
              the first timestep in which posedge clk occurs. Similar comments
              apply to other statements in this paragraph.

(0005963)
Neil Korpusik (administrator)
2008-02-09 19:03
edited on: 2008-02-09 19:09

Placing into the Feedback state.
Mantis items in the Resolved state are ready for the Champions.
The latest proposal doesn't seem to have been approved by
the Technical Committee.

I am requesting that the Champions review the latest proposal
so that any additional feedback can be provided in a timely
fashion.

(0005987)
John Havlicek (manager)
2008-02-13 03:15

2008-02-12: Voice vote approved changes to address Champions friendly amendments, 8y/0n/0a.

(0006018)
Neil Korpusik (administrator)
2008-02-16 18:43

The proposal was approved by the Champions in the
February 14th, 2008 conference call with 3 abstains.

        Abstain: Dave - see his original email for his reasons
                 Francoise - seems problematic - extra rules being added
                 Stu - concerned that spec is not clear enough -
                             implementations could diverge.
        Passed with 3 abstain (4 approved)

(0006162)
Neil Korpusik (administrator)
2008-03-08 19:07

Steven Sharp made a request for this Mantis item to be sent back to the
sv-bc for review. The Champions considered this request at the Feb 25, 2008
Champions conference call.

         Move: Stu - Withdraw approval for Mantis item 1995 and send it to the
                     svbc for approval.
       Second: Dave
      Abstain: Shalom, John, Surrendra
       Oppose: Brad,
          For: Stu, Dave
       Motion failed - the proposal will be sent to the Working Group.

(0006208)
Neil Korpusik (administrator)
2008-03-08 20:26

The proposal was approved by the Working Group in the conference call
of February 28, 2008 with one opposed.

Dave (Mentor) - opposed

(0006594)
Neil Korpusik (administrator)
2008-04-23 11:10

Moving to the sv-sc.

(0006595)
Neil Korpusik (administrator)
2008-04-23 11:13

Mantis was unwilling to allow me to put this back into the feedback state.
I am moving it to the review state so that it doesn't end up in the next
draft of the LRM.

This is one of the Mantis items being reviewed by the sv-sc.

(0007234)
Neil Korpusik (administrator)
2008-07-19 09:13

Attempting to get this mantis item into the resolved state.

(0007235)
Neil Korpusik (administrator)
2008-07-19 09:16

Leaving in the Review state.
The sv-sc voted as follows:

Vote to close as duplicate, assuming 2398 passes, PASSED. 10y/0n/3a

We need to wait for the results of mantis 2398 before taking further action
on this mantis item.

(0007819)
Neil Korpusik (administrator)
2009-01-08 07:28

0002398 has been approved and added to draft 7a.
This is a duplicate of 2398.

Changing status to closed.

Issue History
Date Modified	Username	Field	Change
2007-08-24 12:58	Erik_Seligman	New Issue
2007-08-24 12:58	Erik_Seligman	File Added: assertinloop.pdf
2007-08-24 12:58	Erik_Seligman	Type	=> Enhancement
2007-08-26 03:05	shalom	Issue Monitored: shalom
2007-08-26 03:05	shalom	Status	new => assigned
2007-08-26 03:05	shalom	Assigned To	=> Erik_Seligman
2007-08-27 14:50	Erik_Seligman	File Deleted: assertinloop.pdf
2007-08-27 14:51	Erik_Seligman	File Added: assertinloop.pdf
2007-08-27 14:52	Erik_Seligman	Note Added: 0004188
2007-08-30 14:31	Erik_Seligman	Relationship added	related to 0002005
2007-09-07 21:21	Steven Sharp	Note Added: 0004304
2007-09-10 08:57	Erik_Seligman	File Deleted: assertinloop.pdf
2007-09-10 08:57	Erik_Seligman	File Added: assertinloop.pdf
2007-09-10 08:58	Erik_Seligman	Note Added: 0004313
2007-09-10 23:42	shalom	Relationship added	related to 0002008
2007-09-24 10:21	Erik_Seligman	File Deleted: assertinloop.pdf
2007-09-24 10:21	Erik_Seligman	File Added: assertinloop_0924es.pdf
2007-09-27 11:12	Erik_Seligman	File Deleted: assertinloop_0924es.pdf
2007-09-27 11:13	Erik_Seligman	File Added: assertinloop_0927es.pdf
2007-09-28 08:00	Erik_Seligman	File Deleted: assertinloop_0927es.pdf
2007-09-28 08:00	Erik_Seligman	File Added: assertinloop_0927es.pdf
2007-10-16 00:58	shalom	Relationship added	related to 0002110
2007-10-26 08:06	Erik_Seligman	File Deleted: assertinloop_0927es.pdf
2007-10-26 08:06	Erik_Seligman	File Added: assertinloop_1026es.pdf
2007-10-26 08:08	Erik_Seligman	File Deleted: assertinloop_1026es.pdf
2007-10-26 08:08	Erik_Seligman	File Added: assertinloop_1026es.pdf
2007-10-28 00:53	shalom	Relationship added	related to 0002163
2007-11-19 12:43	Erik_Seligman	File Deleted: assertinloop_1026es.pdf
2007-11-19 12:44	Erik_Seligman	File Added: assertinloop_1117es.pdf
2007-11-27 10:28	Erik_Seligman	File Deleted: assertinloop_1117es.pdf
2007-11-27 10:29	Erik_Seligman	File Added: assertinloop_1127es.pdf
2007-12-07 09:10	Erik_Seligman	File Deleted: assertinloop_1127es.pdf
2007-12-07 09:10	Erik_Seligman	File Added: assertinloop_1206es.pdf
2007-12-07 14:38	Erik_Seligman	File Deleted: assertinloop_1206es.pdf
2007-12-07 14:38	Erik_Seligman	File Added: assertinloop_1207es.pdf
2007-12-10 09:03	Erik_Seligman	File Deleted: assertinloop_1207es.pdf
2007-12-10 09:03	Erik_Seligman	File Added: assertinloop_1210es.pdf
2007-12-10 09:03	Erik_Seligman	File Added: assertinloop_1210es.doc
2007-12-17 08:38	Erik_Seligman	File Deleted: assertinloop_1210es.pdf
2007-12-17 08:38	Erik_Seligman	File Deleted: assertinloop_1210es.doc
2007-12-17 08:39	Erik_Seligman	File Added: assertinloop1217es.pdf
2007-12-17 08:39	Erik_Seligman	File Added: assertinloop_1217es.doc
2007-12-17 09:06	Erik_Seligman	File Deleted: assertinloop1217es.pdf
2007-12-17 09:07	Erik_Seligman	File Deleted: assertinloop_1217es.doc
2007-12-17 09:07	Erik_Seligman	File Added: assertinloop1217es.pdf
2007-12-17 09:07	Erik_Seligman	File Added: assertinloop_1217es.doc
2007-12-18 09:20	Erik_Seligman	File Added: assertinloop_071218es.doc
2007-12-18 09:20	Erik_Seligman	File Added: assertinloop_071218es.pdf
2007-12-18 09:38	Erik_Seligman	File Deleted: assertinloop_071218es.doc
2007-12-18 09:40	Erik_Seligman	File Deleted: assertinloop_071218es.pdf
2007-12-18 09:41	Erik_Seligman	File Added: assertinloop_071218es.doc
2007-12-18 09:41	Erik_Seligman	File Added: assertinloop_071218es.pdf
2007-12-18 10:39	Erik_Seligman	File Deleted: assertinloop_071218es.pdf
2007-12-18 10:40	Erik_Seligman	File Deleted: assertinloop_071218es.doc
2007-12-18 10:40	Erik_Seligman	File Added: assertinloop_071218es.doc
2007-12-18 10:40	Erik_Seligman	File Added: assertinloop_071218es.pdf
2007-12-25 09:41	John Havlicek	Note Added: 0005636
2007-12-25 09:45	John Havlicek	Note Added: 0005637
2007-12-25 09:46	John Havlicek	Note Deleted: 0005637
2008-01-14 09:07	Erik_Seligman	File Added: assertinloop_080114es.doc
2008-01-14 09:07	Erik_Seligman	File Added: assertinloop_080114es.pdf
2008-01-15 17:37	John Havlicek	File Deleted: assertinloop1217es.pdf
2008-01-15 17:37	John Havlicek	File Deleted: assertinloop_1217es.doc
2008-01-15 17:38	John Havlicek	File Deleted: assertinloop_071218es.doc
2008-01-15 17:38	John Havlicek	File Deleted: assertinloop_071218es.pdf
2008-01-15 17:40	John Havlicek	Note Added: 0005715
2008-01-15 17:40	John Havlicek	Status	assigned => resolved
2008-01-15 17:40	John Havlicek	Resolution	open => fixed
2008-01-23 08:22	shalom	File Added: assertinloop_080123es.doc
2008-01-23 08:23	shalom	File Added: assertinloop_080123es.pdf
2008-01-25 09:02	Dave Rich	Relationship added	related to 0002150
2008-01-29 06:44	John Havlicek	Note Added: 0005831
2008-02-05 06:41	shalom	File Added: assertinloop_080204es.doc
2008-02-05 06:42	shalom	File Added: assertinloop_080204es.pdf
2008-02-05 06:43	shalom	Note Added: 0005922
2008-02-08 19:03	Neil Korpusik	Note Added: 0005956
2008-02-09 19:03	Neil Korpusik	Status	resolved => feedback
2008-02-09 19:03	Neil Korpusik	Resolution	fixed => reopened
2008-02-09 19:03	Neil Korpusik	Note Added: 0005963
2008-02-09 19:09	Neil Korpusik	Note Edited: 0005963
2008-02-13 03:15	John Havlicek	Note Added: 0005987
2008-02-13 03:16	John Havlicek	Status	feedback => resolved
2008-02-13 03:16	John Havlicek	Resolution	reopened => fixed
2008-02-16 18:43	Neil Korpusik	Note Added: 0006018
2008-02-25 08:23	John Havlicek	Summary	Allow concurrent assertions and checkers in for loops => Allow concurrent assertions in for loops
2008-03-08 19:07	Neil Korpusik	Note Added: 0006162
2008-03-08 20:26	Neil Korpusik	Note Added: 0006208
2008-03-08 20:26	Neil Korpusik	Status	resolved => approved
2008-04-23 11:10	Neil Korpusik	Note Added: 0006594
2008-04-23 11:10	Neil Korpusik	Status	approved => review
2008-04-23 11:11	Neil Korpusik	Status	review => editor
2008-04-23 11:13	Neil Korpusik	Note Added: 0006595
2008-04-23 11:13	Neil Korpusik	Status	editor => review
2008-04-23 11:14	Neil Korpusik	Category	SV-AC => SV-SC
2008-05-27 16:09	Erik_Seligman	Relationship added	related to 0002398
2008-07-19 09:13	Neil Korpusik	Note Added: 0007234
2008-07-19 09:13	Neil Korpusik	Status	review => editor
2008-07-19 09:16	Neil Korpusik	Note Added: 0007235
2008-07-19 09:16	Neil Korpusik	Status	editor => review
2008-09-26 03:03	shalom	Relationship added	related to 0002483
2009-01-08 07:28	Neil Korpusik	Status	review => closed
2009-01-08 07:28	Neil Korpusik	Note Added: 0007819
2009-01-08 07:29	Neil Korpusik	Relationship replaced	duplicate of 0002398

Notes
(0004188) Erik_Seligman (developer) 2007-08-27 14:52	After some discussion, we decided to make this proposal just for the assertions-- a separate proposal (or an edit to 1900) will add this for checkers.

(0004304) Steven Sharp (developer) 2007-09-07 21:21	The phrase "statically computable set of iterations" is not sufficiently restrictive or precise. Many things could be theoretically possible to compute, but completely impractical in practice. If you want to allow this, you should require iterations that are straightforward to compute. You should have the same kind of limitations that generate loops have (e.g. the loop bounds and increment being constant expressions). Note that there are a lot of constructs possible in Verilog procedural code that are not possible in generate loops, and you would need to account for these also. For example, a procedural loop can modify the loop counter inside the loop. The loop counter could be forced from elsewhere (including PLI), which would prevent the loop from operating normally. There are constructs which could cause early exit from the loop, such as break, return and disable.

(0004313) Erik_Seligman (developer) 2007-09-10 08:58	I just uploaded a new version that attempts to address Steven's concerns.

(0005636) John Havlicek (manager) 2007-12-25 09:41	2007-12-24: Passed by e-mail vote, 8y/0n/2a. There were no friendly amendments. There were comments from Shalom Bresticker.

(0005715) John Havlicek (manager) 2008-01-15 17:40	Updated to address editorial comments from Shalom Bresticker. The updated version was approved by voice vote on 2008-01-15, 9y/0n/0a.

(0005831) John Havlicek (manager) 2008-01-29 06:44	2008-01-28: e-mail ballot passed minor revisions based on comments from Manisha Kulshrestha, 8y/0n/2a.

(0005922) shalom (manager) 2008-02-05 06:43	Uploaded new version from Erik responding to comments from John and from me as comments to email Champions' vote.

(0005956) Neil Korpusik (administrator) 2008-02-08 19:03	The proposal failed in the Champions email vote which ended on Feb 4th, 2008. Failed with 1 no-vote - Dave - This proposal is essentially creating a generate block within a procedural context. I'm fine with limiting this to assertion statements for now, but that does alleviate addressing all the issues surrounding generated code. For example each assertion statement is replicated in the loop (including nested loops) and a generate block label needs to be created for every instance of each. The loop iterator should be treated as a genvar constant within each instance of the assertion statement. - Shalom - note to the Editor: In "For loop control variable value 1, the assertion will pass, and the pass action block will be generated," change the last word to "executed". - John - friendly amendments: - Editorial: I think that the parenthetical exception in the change to 16.4 should be at the end of the sentence. - In the change to 16.14.3, I'm not sure that shall count each possible set of loop control variable values as one attempt is really clear. Based on the sentence that follows, I think that what is intended is something like shall count distinct valuations of loop control variable values as separate attempts - Editorial: At the bottom of p. 2, the comma following the bold courier "continue" should be in non-bold roman. - Editorial: Do not use smart quotes in the courier examples. - p. 3, change "generated" to "executed" in "the pass action block will be generated". - p. 4. In the example above, ac1 will always be checking the sampled value of variable ok. Since this will be equal to (my_bits[3] == 0) by the end of any time step, it will always pass The declaration and initialization of "ok" are not shown, so we do not know its sampled value in timesteps prior to and including the first timestep in which posedge clk occurs. Similar comments apply to other statements in this paragraph.

(0005963) Neil Korpusik (administrator) 2008-02-09 19:03 edited on: 2008-02-09 19:09	Placing into the Feedback state. Mantis items in the Resolved state are ready for the Champions. The latest proposal doesn't seem to have been approved by the Technical Committee. I am requesting that the Champions review the latest proposal so that any additional feedback can be provided in a timely fashion.

(0005987) John Havlicek (manager) 2008-02-13 03:15	2008-02-12: Voice vote approved changes to address Champions friendly amendments, 8y/0n/0a.

(0006018) Neil Korpusik (administrator) 2008-02-16 18:43	The proposal was approved by the Champions in the February 14th, 2008 conference call with 3 abstains. Abstain: Dave - see his original email for his reasons Francoise - seems problematic - extra rules being added Stu - concerned that spec is not clear enough - implementations could diverge. Passed with 3 abstain (4 approved)

(0006162) Neil Korpusik (administrator) 2008-03-08 19:07	Steven Sharp made a request for this Mantis item to be sent back to the sv-bc for review. The Champions considered this request at the Feb 25, 2008 Champions conference call. Move: Stu - Withdraw approval for Mantis item 1995 and send it to the svbc for approval. Second: Dave Abstain: Shalom, John, Surrendra Oppose: Brad, For: Stu, Dave Motion failed - the proposal will be sent to the Working Group.

(0006208) Neil Korpusik (administrator) 2008-03-08 20:26	The proposal was approved by the Working Group in the conference call of February 28, 2008 with one opposed. Dave (Mentor) - opposed

(0006594) Neil Korpusik (administrator) 2008-04-23 11:10	Moving to the sv-sc.

(0006595) Neil Korpusik (administrator) 2008-04-23 11:13	Mantis was unwilling to allow me to put this back into the feedback state. I am moving it to the review state so that it doesn't end up in the next draft of the LRM. This is one of the Mantis items being reviewed by the sv-sc.

(0007234) Neil Korpusik (administrator) 2008-07-19 09:13	Attempting to get this mantis item into the resolved state.

(0007235) Neil Korpusik (administrator) 2008-07-19 09:16	Leaving in the Review state. The sv-sc voted as follows: Vote to close as duplicate, assuming 2398 passes, PASSED. 10y/0n/3a We need to wait for the results of mantis 2398 before taking further action on this mantis item.

(0007819) Neil Korpusik (administrator) 2009-01-08 07:28	0002398 has been approved and added to draft 7a. This is a duplicate of 2398. Changing status to closed.