Thanks John. I can now see cases that can be problematic. BTW, on your model, global bit [1:0] v = 2'b11; should be global bit [1:0] v = 2'b00; I need to note that your use case, "v" is a controlling element vs a storage of a module variable (e.g., a data element) for later comparisons. In the model used by that formal verification vendor (and my intended usage), the globally-local variable is used to store bus data, and that is set only once before it is read. Also, in a timing type of modeling, there is a sequence of events (e.g., addr, data on bus, data store, data read, etc). That vendor used a different modeling style in his SVA, modified to handle the storage elements. I understand that we're looking for a generalized solution, rather than specific cases. Thus, your point is well taken. Thanks for the examples. Ben On Tue, Jan 6, 2015 at 6:24 AM, John Havlicek <johnh@cadence.com> wrote: > Consider this sequence, where I'm using "global" to signify the global > local variable. What should it mean? > > sequence unsure (byte B, C, D); > global byte V = 8'b0; > ( > // writer thread > (B[0][->1], V[0] = D[0]) > ##0 (B[1][->1], V[1] = D[1]) > ##0 (B[2][->1], V[2] = D[2]) > ##0 (B[3][->1], V[3] = D[3]) > ##0 (B[4][->1], V[4] = D[4]) > ##0 (B[5][->1], V[5] = D[5]) > ##0 (B[6][->1], V[6] = D[6]) > ##0 (B[7][->1], V[7] = D[7]) > ) > and > ( > // reader thread > (C[0][->1], $display("V[0] == %b", V[0])) > ##0 (C[1][->1], $display("V[1] == %b", V[1])) > ##0 (C[2][->1], $display("V[2] == %b", V[2])) > ##0 (C[3][->1], $display("V[3] == %b", V[3])) > ##0 (C[4][->1], $display("V[4] == %b", V[4])) > ##0 (C[5][->1], $display("V[5] == %b", V[5])) > ##0 (C[6][->1], $display("V[6] == %b", V[6])) > ##0 (C[7][->1], $display("V[7] == %b", V[7])) > ) > ; > endsequence : unsure > > Depending on when the B bits turn on, the V bits get written, some may be > in the same time step, others not. Depending on when the C bits turn on, > the V bits get read, some concurrent, some not. One can try to reduce the > chaos by saying that in a given timestep, writes to V should occur before > reads from V. > > But such an ordering rule may be foiled when there are circular > dependencies between reads and writes: > > property hmm (bit [1:0] a, b); > global bit [1:0] v = 2'b11; > > > ( > a[0] ##1 b[0][->1] > |-> > !v[1] > |-> > (1'b1, v[0] = 1'b1, $display("thread 0 wins!")) > ) > and > ( > a[1] ##1 b[1][->1] > |-> > !v[0] > |-> > (1'b1, v[1] = 1'b1, $display("thread 1 wins!")) > ) > endproperty : hmm > > > J.H. > > -----Original Message----- > From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of > Eduard Cerny > Sent: Monday, January 05, 2015 9:16 AM > To: hdlcohen@gmail.com; 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 > > Hello Ben, > > > > The same can be achieved by writing to a global variable in a match item > task call, at least in that case the user is aware that if another attempt > could start in parallel (not in this example) the data could be > overwritten. In other words, your notation of global would / could be a > short hand for a task call assignment. Should there be a required check > that no other attempt is started while one is in progress? > > > > I’d suggest that the property as you wrote it be modified to avoid false > failures and successes by dropping |-> in both the antecedent and > consequent as follows: > > property p_packet2mem; > > global int v_block[0:1023]; > > global int v_addr, v_i, v_i2; > > @(posedge clk_fast) (sop, v_done=0) ##1 (1, v_addr=addr, v_i=0) > > // at start of packet addr info, do setups > > ##1 (1, v_block[v_i]=pkt_data, v_i++)[*1024] // save > packet data > > ##0 (1, check_signature(checksum, v_block)) // check > signatures with function call > > implies > > @(posedge clk_slow) ##[0:2] (start_wr2mem, v_i2=0) > > // when logic detects its ready to write to mem > > // start writing data into mem > > ##1 (wr && mem_data==v_block[v_i2] && mem_addr==v_addr, > v_i2++, v_addr++)[*1024]; > > endproperty > > > > Best regards > > ed > > > > From: Ben Cohen [mailto:hdlcohen@gmail.com] > Sent: Sunday, January 04, 2015 7:10 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 > > > > Below is an updated model for your consideration. The requirements and > explanations are documented below. Hopefully, I got the model correct, but > this is a model to demonstrate the concepts in using globally local > variables. > > > > bit start_wr2mem, wr; > > // A packet transmit 1024 data over a bus at a clock rate of 20MHz. > > // Packet includes a sop, addr, 1024 data set, signature > > // DUT does the following: > > // 1) When the sop and the 1st word of a packet is received, > > // the DUT saves this addr and data into a local buffer (like > a fifo) > > // 2) The DUT initiates a "start_wr2mem" command to initiate the > memory transfer > > // when the fifo starts to fill. > > // 3) When "start_wr2mem", DUT starts the transfer of that > buffered data into a memory > > // at a clock rate of 7MHz. > > // > > // ASSERTION does the following: > > // In antecedent: > > // 1) at fast_clk, it detects the sop, and stores the addr. > > // 2) It saves the addr into a globally local > variable v_addr > > // 3) It saves the 1024 data into a globally local > variable v_block > > // 4) At end of transfer, it checks the signature using a > function. > > // Function returns true to avoid vacuity, but flags an > error message. > > // Function could use an immediate assertion. > > // > > // Concurrently with step 1 (above) and at the slow clock rate, > > // in consequent: > > // a) It waits for the start_wr2mem command > > // b) It then checks that the wr signal of the mem is true, > > // and the data is what was sent, > > // and the address to mem is wahta was > in the packet > > // It repeats step b for all 1024 words, taking the info from > the > // globally local variables > > // > > property p_packet2mem; > > global int v_block[0:1023]; > > global int v_addr, v_i, v_i2; > > @(posedge clk_fast) (sop, v_done=0) ##1 (1, v_addr=addr, v_i=0) |-> > > // at start of packet addr info, do setups > > (##1 (1, v_block[v_i]=pkt_data, v_i++))[*1024] // save packet > data > > ##1 (1, check_signature(checksum, v_block)) > // check signatures with function call > > implies > > @(posedge clk_slow) ##[0:2] (start_wr2mem, v_i2=0) |-> > // when logic detects its ready to write to mem > > // start the writing data into mem > > (##1 (wr, mem_data==v_block[v_i2], mem_addr==v_addr, v_i2++, > v_addr++))[*1024]; > > endproperty > > Ben > > > > On Sun, Jan 4, 2015 at 9:53 AM, Ben Cohen <hdlcohen@gmail.com <mailto: > hdlcohen@gmail.com> > wrote: > > What if the copying occurs as soon as 1 word is received instead of at end > of packet? In that case you would need the implies instead of the > implication operator since, with the implies, the antecedent and consequent > start at same time and are concurrent. With the implication, antecedent > must end before consequent starts. Btw, the copying requirement could be > changed to writing into a dut memory. The point I am making is that having > a globally accessible local variable gives you more freedom to write > models. I see it as a tool. > > If you were to build the pyramids, can it be done without cranes? Would > cranes make it easier? > > Ben > > > > On Sunday, January 4, 2015, Eduard Cerny <Eduard.Cerny@synopsys.com > <mailto:Eduard.Cerny@synopsys.com> > wrote: > > Hello Ben, > > > > regarding the example of copying a packet, why do you need to use implies” > at all? The delay on the consequent may be costly in performance or memory. > Is it not simpler to use the more common suffix implication and the usual > local variables? For example: > > > > // Upon receipt of a successful packet with 1024 data transfers, > > // that data is then transferred (i.e., copied) into another bus, > using the proper protocol. > > // IOW, it's a relay. > > property p_packet2bus; > > int v_block[0:1023]; // for storage of packet data > > int v_i1, v_i2; > > (sop) ##1 (1, v_i1=0) ##1 // at start of packet (sop), do > setups > > (##1 (1, v_block[v_i1]=pkt_data, v_i1++))[*1024] // save > packet data into local variable > > ##1 (1, check_signature(checksum, v_block)) > // > check_signature is a function > > // when done packet xfr > > bus_req[->1] > > |=> // start the copying into the other bus … checking > > (ack, v_i2 = 0) ##1 (1, bus_data==v_block[v_i2], > v_i2++)[*1024]; > // data on bus is > what was initially received > > endproperty > > > > This could also eliminate the need for v_i2 because v_i1 could be reused. > > > > Best regards > > ed > > > > From: Ben Cohen [mailto:hdlcohen@gmail.com] > Sent: Thursday, January 01, 2015 2:10 AM > To: Eduard Cerny > Cc: Korchemny, Dmitry; sv-ac@eda.org <mailto:sv-ac@eda.org> ; Karen > Pieper; IEEE P1800 Working Group (ieee1800@eda.org <mailto: > ieee1800@eda.org> ) (ieee1800@eda.org <mailto:ieee1800@eda.org> ) > Subject: Re: [sv-ac] Recommended Items to Work and Study on the Next P1800 > Revision > > > > Ed, > > Another example that uses the implies, which is of course of the form > > property_expr implies property_expr > > Being able to access sibling local variables between antecedent and > consequent of the implies gives the writer of assertions a lot more > flexibility. I see lots of models that can benefit from being able to > share globally local variables across concurrent threads and siblings. > > > > // Upon receipt of a successful packet with 1024 data transfers, > > // that data is then transferred (i.e., copied) into another bus, > using the proper protocol. > > // IOW, it's a relay. > > property p_packet2bus; > > global int v_block[0:1023]; // for storage of packet data > > global int v_i, v_i2; > > global bit v_done; > > (sop, v_done=0) ##1 (1, v_index=0) |-> // at start of packet > (sop), do setups > > (##1 (1, v_block[v_i]=pkt_data, v_i++))[*1024] // save > packet data into local variable > > ##1 (1, check_signature(checksum, v_block)) ##0(1, > v_done=1) > // > check_signature is a function > > implies > > ##1027 (v_done, v_i2=0) |=> // when done packet xfr > > bus_req |=> // start the copying into the other bus > > ack (##1 (1, bus_data==v_block[v_i2], > v_i2++))[*1024]; > // data on bus is > what was initially received > > endproperty > > > > I strongly believe that having this feature simplifies the language, > rather than complicates it. > > I found that the flow-out rules are complex, and in any case, there is no > flow-in, meaning that it is illegal to read within a concurrent thread > local variables set in another thread. For example, > > ((a, v=1) ##2 b) or (c ##1 v==d) // is illegal > > ((a, v=1) ##2 b) and (c ##1 v==d) // is illegal > > > > In this group, I would like to see the addition of useful features that > users and industry have found necessary to simplify the definition of > assertions. This should be done in a neutral position. We saw this in many > situations where vendors added their own specific additions or flags or > pragmas that eventually made their way (maybe modified or tuned) into > SystemVerilog, of course because of need. > > Ben > > > > On Wed, Dec 31, 2014 at 2:46 PM, Ben Cohen <hdlcohen@gmail.com <mailto: > hdlcohen@gmail.com> > wrote: > > 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 > <mailto: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> [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 <mailto:sv-ac@eda.org> ; Karen Pieper; IEEE P1800 > Working Group (ieee1800@eda.org <mailto:ieee1800@eda.org> ) ( > ieee1800@eda.org <mailto: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 <mailto: > 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 <mailto: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 <mailto: > ieee1800@eda.org> ) (ieee1800@eda.org <mailto: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 <mailto: > dmitry.korchemny@intel.com> > > To: "IEEE P1800 Working Group (ieee1800@eda.org <mailto: > ieee1800@eda.org> ) (ieee1800@eda.org <mailto:ieee1800@eda.org> )" < > ieee1800@eda.org <mailto:ieee1800@eda.org> > > Cc: "'sv-ac@eda.org'" <sv-ac@eda.org <mailto: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 <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. > > > > -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Tue Jan 6 08:47:37 2015
This archive was generated by hypermail 2.1.8 : Tue Jan 06 2015 - 08:47:43 PST