More comments on 4571 *4571 For next 1800: Probing property local variables for sharing across boundaries* http://www.eda-stds.org/svdb/view.php?id=4571 *Summary*: There would be a need to put restrictions in the usage of the *$probe*(local_variable_name) function to read a local variable that was set in thread that belongs to a multithreaded set of sequences ORed or ANDed together. *Restrictions*: 1) The local variable accessed with the *$probe* can only be written once, and only by one of the multithreaded sequences (i.e., if we have multithreaded sequences connected by OR or AND sequence operators, then that local variable can only be written one in one and only one of those threads). 2) Like any local variable, it must be set before it is read. In addition, it can only be read in cycles following the cycle in which it was set (thus, if the local variable is set in cycle 2, it can be read in cycles 3, 4, ...etc). 3) If read in a cycle in which it was not read then ??? - assertion is vacuous? - assertion fails ? - assertion considers the default or initialized value of the local variable? (what do we do now? Is tis specified in 1800?) *Examples: * *module* m4571; *bit* clk, a, b, c, d, e; *int* x, y, z; *property* p1; *int* v; (a ##1 (b, v=x)) *or* (c ##3 y==$probe(v)); *endproperty* p1; *property* p2; *int* v; (a ##1 (b, v=x)) *and* (c ##3 y==$probe(v)) implies (1'b1 ##3 d ##1 z==$probe(v)); *endproperty* p2; *endmodule* On Fri, Nov 28, 2014 at 4:03 PM, Ben Cohen <hdlcohen@gmail.com> wrote: > > *4571 For next 1800: Probing property local variables for sharing > across boundaries* > http://www.eda-stds.org/svdb/view.php?id=4571 > [Ben] I updated the notes for above mantis. Specifically: > Currently, local variables do not flow across the "and" property operator. > There are applications where is is desired to access a local variables set > once in an antecedent. I recommend that we add the > $probe(local_variable_name) function to read a local variable that was set > in an antecedent of a sequence. That antecedent can belong to a property > of the form (sequence |-> property) or (sequence implies property). > Example: > int data; > property p; > int v; > (a, v=data) implies (c ##2 d==$probe(v); > endproperty: p > > This is an important feature. > > *3195 Local Variables Flow Out Issue in and/or/intersect/implies* > [Ben] Child of 4571 > > >> >> > > *4081 Checking for nonvacuity of ORed properties* > http://www.eda-stds.org/svdb/view.php?id=04081 > [Ben] Nice to have, but I am concerned about adding more complexity. > The existing solution of writing separate small assertions without the > *or* operator works OK, and is probably a better overall recommendation > from a style standpoint. > Users need to be made aware of vacuity with the *or *operator. > > http://www.eda-stds.org/svdb/view.php?id=04060 > *4060 Soft assumptions should provide functionality similar to soft > constraints in next PAR* > [Ben] Nice to have > > > >> ** >> *5068 concurrent assertions in classes* >> >> > *3718 Need to define concept of sampling in classes* > > > http://www.eda-stds.org/svdb/view.php?id=03718 > [Ben] This is a child of 5068 > > ** > *3057 Make local variables a first class language construct in SVA.* > [Ben] This is a child of 5068 > > *3060 Allow class instantiation in checkers* > [Ben] This is a child of 5068 > > > > *3120 expect construct to refer to virtual interfaces* > [Ben] This is a child of 5068 > > *3559 Implication example explanation is not accurate* > [Ben] IF not clear, clarifications must be made. That can easily be done. > > > > ** > > *3057 Make local variables a first class language construct in SVA.* > http://www.eda-stds.org/svdb/view.php?id=3057 > [Ben] Nice to have to important > > > *2944 concurrent assertions in tasks/functions* > [Ben] Maybe is a child of 5068 since tasks uses tasks rather than always > statements. > Also important for modules and checkers > > ---------------------------------------- > >> 5066 Allow variables in delays and repeat operators >> >> 5065 Create standard package to define implementation for commonly >> used properties >> >> 5064 Create standard package to define constants used in >> assertion-related stuff >> >> 5063 Automatic inference of assertion statement type >> >> 5038 Grammar changes for Mantis 3525 appear to have unintended >> effects >> >> ** >> *4571 For next 1800: Probing property local variables for sharing >> across boundaries* >> >> 4156 17.2 checker syntax does not support use of $display ß >> irrelevant? (DK) >> >> 4084 Issue with coverage // need for a "full_paths" coverage? >> >> >> *4081 Checking for nonvacuity of ORed properties* >> >> >> *4060 Soft assumptions should provide functionality similar to >> soft constraints in next PAR* >> >> *3718 Need to define concept of sampling in classes* >> >> >> 3672 hierarchical access to named block in assertion action blocks >> >> 3614 Free variable randomization with assumptions with various clock >> domains >> >> 3610 Sequence methods with sequences admitting empty match >> >> ** >> *3559 Implication example explanation is not accurate* >> >> 3555 Use let in implication example >> >> 3552 16.14.6 Sequence methods // .triggered need further >> clarification >> >> 3478 Make drivers of inout ports accessible >> >> 3217 Definition for referring to an assertion as a relative >> hierarchical name is missing in Section 23.6 >> >> >> *3195 Local Variables Flow Out Issue in and/or/intersect/implies* >> >> 3157 Identifier usage before declaration in assertions >> >> >> >> *3120 expect construct to refer to virtual interfaces* >> >> 3117 make it clear that rewriting algorithm (F.4.1) applies to >> checker and let >> >> 3099 action block triggering is not well defined >> >> ** >> *3060 Allow class instantiation in checkers* >> >> 3059 Study PSL local variables and determine if any alignment is >> warranted. >> >> 3058 Add support for real variables and continuous time, which are >> necessary for mixed-signal assertions. >> >> ** >> *3057 Make local variables a first class language construct in SVA.* >> >> 3038 Tighter integration between SVA constructs and covergroups >> >> 3032 2012 Ballot comment 44: Allow forcing in checkers >> >> ** >> *3031 Allow checker instantiation in classes* >> >> 3030 2012 Ballot comment 45: Allow checker instantiation in >> functions and tasks >> >> 3029 Remove limitation regarding passing dynamic arrays to >> sequences, properties and checkers >> >> 3024 Introduce generic integral type >> >> 2980 semantic inconsistency between expect and procedural concurrent >> assertions >> >> 2958 provide same syntax variants for agrument passing at >> sequence/property instances (16.8, 16.13) as for port connections at module >> >> 2947 Module variables from within function or task not sampled, LRM >> and practice contradictory >> > > >> ** >> *2944 concurrent assertions in tasks/functions* >> >> 2939 Hierarchical reference of checker variable should be disallowed >> completely >> >> 2858 Clarify the rules for assigning a value to a non-checker >> variable from within a checker >> >> 2842 Checker variable randomization with deferred assumptions is not >> defined >> >> 2751 P1800-2009: checker formal arguments may not be connected to >> interfaces // WHY? >> >> 2560 Inconsistent description of conditional property operators >> >> 2555 Clarify relationships of different local variable binding >> mechanisms >> >> 2546 'empty match' and 'vacuous success' are not clearly defined in >> LRM >> >> 2413 Allow inferred value functions in let >> >> 2341 should scope of assert control tasks be finer than a module >> >> 2297 Case construct for sequences >> >> 2248 leading clock - Champions feedback - items related to Mantis >> item 1683 >> >> 2172 Add sequence if...else. >> >> 2151 Referencing assertions in functions >> >> 2111 Allow parameters in checkers >> >> 1853 BNF for calls to $rose and other sample value system functions >> >> 1647 Type query functions >> >> 1547 need to be able to assert assertions in a clocking block >> >> 1531 Allow static local variables in properties and sequences >> >> 1502 Decision point definition >> >> 1296 Annex E does not cover all clocked derived forms >> >> 1147 find way to embed PSL >> >> 1036 Incorporate by reference Accellera PSL >> >> >> >> I suggest to allow working on minor enhancements (like mantis 3555), and >> on any mantis item if the resolution is to close it. For example, there are >> several enhancements that are not relevant anymore. >> >> >> >> Thanks, >> >> Dmitry >> >> --------------------------------------------------------------------- >> 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, and is believed to be clean.Received on Sun Nov 30 11:58:34 2014
This archive was generated by hypermail 2.1.8 : Sun Nov 30 2014 - 11:58:38 PST