Hmm ... I had intended the initial value 2'b00 for global bit v in property hmm. J.H. -----Original Message----- From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of John Havlicek Sent: Tuesday, January 06, 2015 8:24 AM To: sv-ac@eda.org Subject: RE: [sv-ac] Recommended Items to Work and Study on the Next P1800 Revision 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 06:28:34 2015
This archive was generated by hypermail 2.1.8 : Tue Jan 06 2015 - 06:28:38 PST