Yes, we'll have time to discuss this. However, when dealing dealing with properties that have concurrent threads, the current rules and restrictions on the visibility of local variables in and out of those threads are complex and restrictive. I am not proposing to change what we have. My proposition actually makes it easier, if anything, as it specifies the defintion of a special local variable that is accessible (in and out) by all concurrent threads. As such, the user need to be cautious it its usage, but with guidelines that can be controlled. It does simplify the writing of assertions. Without access to these globally local property variables, one must resort to support logic with module or checker variables with specific data structures (like queues, or maybe associative array) and functions with side effects to read and write into those module variables from within a property ... and THAT is complex. I provided 2 examples for simulation. Think about how one would write those with 1800'12. My point is that this feature gives more power the SVA. The fact that a vendor added a hint of this feature in his tools (outside of SVA) and is encouraging his customers to use this non-LRM addition (when needed) speaks of the need. However, aside from this vendor, I see many assertions that can use this visibility access of local variables across concurrent threads and siblings. Till now, I had to live with what I have, and not what I wished for. We'll have interesting discussions!!! :) Ben On Thu, Jan 1, 2015 at 11:45 AM, Eduard Cerny <Eduard.Cerny@synopsys.com> wrote: > Hello Ben, > > > > I am not contesting that one could create an application, rather whether > it can be done w/o extending/complexifying the SVA language. > > > > Anyway, I am sure we’ll have time to discuss it J later this year. > > > > Best regards > > ed > > > > > > *From:* Ben Cohen [mailto:hdlcohen@gmail.com] > *Sent:* Wednesday, December 31, 2014 5:47 PM > *To:* Eduard Cerny > *Cc:* Korchemny, Dmitry; sv-ac@eda.org; Karen Pieper; IEEE P1800 Working > Group (ieee1800@eda.org) (ieee1800@eda.org) > > *Subject:* Re: [sv-ac] Recommended Items to Work and Study on the Next > P1800 Revision > > > > Hi Ed, > > In http://www.eda-stds.org/svdb/view.php?id=4571 there is a > > WhitePaper_Operational_SVA.pdf > <http://www.eda-stds.org/svdb/file_download.php?file_id=5907&type=bug> [^ > <http://www.eda-stds.org/svdb/file_download.php?file_id=5907&type=bug>] > > It describes an application by a formal verification tool vendor for the > need to read a local variable that was set in another concurrent thread of *and, or > *operators. That particular vendor defined his own technique (not in > 1800) to do that. That makes the code non-simulatable, but only formally > verified with his tool. It was by need, and not by choice. > > The point is that there is a need for this. > > > > That particular white paper example specifies assertions using a timing > diagram as it basic input format. Thus, you specify time slots using named > sequences, where t0 is the time slot for the attempt, t1 is the next cycle, > and so on. See paper for actual examples. > > > > Below is an example I just made up. Yes, there are other ways to specify > this using current 1800, but let's leave your preferences aside for the > moment. I am demonstrating the possibilities. Perhaps some of you, who > are involved in real designs can provide practical examples where a > "global" property local variable is neat or very much needed. > > // no write to main mem if there is a cache hit and same data > > // else, if wr and a miss then write to main mem. > > // try to acquire main mem bus as early as possible, and cancel if no need > > *property *p_mem; > > *global int* v_addr, v_wrdata; > > *global bit* v_miss, v_hit; > > ((wr, v_addr=addr, v_wrdata=data) ##1 > > (cache_hit && cache_data==v_wrdata, v_hit=1)) > > *or* > > (##1 (cache_miss, v_miss=1)) > > *implies* > > (##1 req_main_mem ##1 v_hit==1 && req_main_cancel) > > *or* > > (##1 req_main_mem ##1 v_miss |-> > > ##[1:4]bus_grant ##1 gmem_addr=v_addr > ##0 gmem_data==v_wrdata ##1 req_main_cancel); > > *endproperty* > > > > *property * p_mem; // Same property with comments > > *global * int v_addr, v_wrdata; > > *global * bit v_miss, v_hit; > > // if a wr, save addr and wrdata save if is in cache or not > > ((wr, v_addr=addr, v_wrdata=data) ##1 > > (cache_hit && cache_data==v_wrdata, v_hit=1) ) *or* > > (##1 (cache_miss, v_miss=1)) > > // Concurrently @t1 (cycle after attempt) > > // try to get access to main memory > > // (like a pre-get incase if it a miss) > > // If it is a miss, then store data to main memory > > *implies * > > (##1 req_main_mem ##1 v_hit==1 && req_main_cancel) *or * > > (##1 req_main_mem ##1 v_miss |-> // write to main mem > > ##[1:4]bus_grant ##1 gmem_addr=v_addr > > ##0 gmem_data==v_wrdata ##1 req_main_cancel); > > *endproperty* > > > > Ben > > > > On Wed, Dec 31, 2014 at 1:13 PM, Eduard Cerny <Eduard.Cerny@synopsys.com> > wrote: > > Hello Ben, > > > > I would like to see one practical example that works well in formal and > simulation, one that cannot be done by using existing means. IMHO, > complexifying the language is not always good. Even as it stands now, > people have enough problems understanding the intricacies of SV (and SVA). > > > > Thanks and Happy New Year! > > > > ed > > > > *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *Ben > Cohen > *Sent:* Wednesday, December 31, 2014 1:46 PM > *To:* Korchemny, Dmitry > *Cc:* sv-ac@eda.org; Karen Pieper; IEEE P1800 Working Group ( > ieee1800@eda.org) (ieee1800@eda.org) > > > *Subject:* Re: [sv-ac] Recommended Items to Work and Study on the Next > P1800 Revision > > > > Added the following note to the mantis: > > Solutions 1, 2, 3 all lead to the conclusion the need to have a local > variable accessible to all concurrent assertions and siblings, and thus, it > must somehow be tagged or qualified as special (e.g., with the $set_freeze, > $probe, or a qualifier for the variable) . This lead to solution 4, which > provides the least impact to changes. We could tag that special local > variable with a qualifier "local" or even "global" since it is, in effect, > global to the property. > > The question arises: what happens if this "globally local" variable is > read before it is written? I believe that it is up to the user to insure > this condition. The value read if not written is the defaulted or > initialized value. Below is a potential solution as to how a user can be > sure that the variable is written before it is read; this is a coding > style, rather than something the tool must verify. > > > > module m4571_4; > > bit clk, a, b, c, d, e; > > logic[31:0] x, y, z; > > property p1; > > *local *logic[31:0] v='bX; // could also be > > // *global *logic[31:0] v='bX; > > (a ##[1:$](b, v=x)) or > > (c ##[1:$] !$isunknown(v) ##1 c ##0 y==v); > > endproperty p1; > > ... > > > > On Mon, Dec 29, 2014 at 10:43 AM, Ben Cohen <hdlcohen@gmail.com> wrote: > > Dmitry and all, > > I uploaded mantis_4571 that discussed the issues and provides 2 promising > solutions. > > Please review and comment for the next meeting. > > http://www.eda-stds.org/svdb/view.php?id=4571 > > Thanks, > > Ben > > > > On Sun, Dec 28, 2014 at 4:43 AM, Korchemny, Dmitry < > dmitry.korchemny@intel.com> wrote: > > Hi all, > > > > Per Karen request, I will call a meeting next Monday to discuss the > feasibility of 4571. > > > > Thanks and Happy Holidays, > > Dmitry > > > > *From:* Karen Pieper [mailto:karen_l_pieper@yahoo.com] > *Sent:* Saturday, December 27, 2014 00:06 > *To:* Korchemny, Dmitry; IEEE P1800 Working Group (ieee1800@eda.org) ( > ieee1800@eda.org) > *Cc:* 'sv-ac@eda.org' > *Subject:* Re: [sv-ac] Recommended Items to Work and Study on the Next > P1800 Revision > > > > Can the SV-AC please start the study on the feasibility of 4571, and > advise at the P1800 review meeting what is known, likely schedule > requirements, and suggested path forward? > > > > Thanks, > > > > Karen > > > > ------------------------------ > > *From:* "Korchemny, Dmitry" <dmitry.korchemny@intel.com> > *To:* "IEEE P1800 Working Group (ieee1800@eda.org) (ieee1800@eda.org)" < > ieee1800@eda.org> > *Cc:* "'sv-ac@eda.org'" <sv-ac@eda.org> > *Sent:* Thursday, December 25, 2014 6:30 AM > *Subject:* [sv-ac] Recommended Items to Work and Study on the Next P1800 > Revision > > > > *SV-AC: Recommended Items to Work and Study on the Next P1800 Revision* > > > > Following internal discussions, SV-AC recommends to work on the following > mantis items: > > > > · 3057: Make local variables a first class language construct in > SVA > > · 5063: Allow tools to infer assertion statement type > > · 5064: Create standard package to define constants used in > assertion-related stuff > > · 5065: Create standard package to define implementation for > commonly used properties > > · 5067: Allow variables in delays and repeat operators > > > > SV-AC recommends to study the feasibility of the proposal: > > · 4571: For next 1800: Probing property local variables for > sharing across boundaries > > > > SV-AC requests from SV-CC to address the proposal: > > · 2182: Ballot comment 56: Elaborate VPI diagrams for checkers > > > > SV-AC recommends to create a cross-P1800 group to study the following > proposal and to elaborate recommendations for the future work: > > 5068: concurrent assertions in classes > > > > Also, SV-AC recommends to work on errata and clarification items. > > > > Regards, > > 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. > > > > --------------------------------------------------------------------- > 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, and is believed to be clean.Received on Thu Jan 1 13:02:48 2015
This archive was generated by hypermail 2.1.8 : Thu Jan 01 2015 - 13:02:55 PST