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> 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> > 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; 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 >> >> >> >> 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> 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> >> 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 Sun Jan 4 16:11:08 2015
This archive was generated by hypermail 2.1.8 : Sun Jan 04 2015 - 16:11:16 PST