A Community of Verification Professionals

Create an Account	Home | Calendar | Downloads | FAQ | Links | Site Admin | Your Account
Login Nickname Password Security Code: Type Security Code BACKWARD Don't have an account yet? You can create one. As a registered user you have some advantages like theme manager, comments configuration and post comments with your name. Modules · Home · Downloads · FAQ · Feedback · Recommend Us · Web Links · Your Account Advertising Who's Online There are currently, 65 guest(s) and 2 member(s) that are online. You are Anonymous user. You can register for free by clicking here    Verification Guild: Forums  Forum FAQ   Search   Usergroups   Profile  Digest    Log in  Type-Checking SVA Parameters Goto page 1, 2  Next          Verification Guild Forum Index -> Assertions View previous topic :: View next topic   Author Message MikeP Junior Joined: Jun 15, 2004 Posts: 5 Location: Waltham, MA Posted: Tue Jun 15, 2004 3:31 pm    Post subject: Type-Checking SVA Parameters Hey all, Long-time listener; first-time caller. I've been wading through the System Verilog 3.1A LRM and I've got some questions regarding System Verilog Assertions. The sequences and properties allow parameters to be passed in - seems like a handy feature. IE Code: sequence rot3(a, b, c)   a == b ##1 b == c##1 c == a; endsequence However, there seem to be no types associated with arguments (a, b, c). As far as I can tell, the LRM specifies nothing about type-checking or guaranteeing the safety of the expression. Are tools expected to do this, or if a and b have different types should this result in some kind of weird run-time error? Well, I guess compile-time type checking seems reasonable, but what about type inference? IE Code: sequence foo(a,b)  x == a ##1 x == b; //x is declared as int endsequence property bar  int j,k;  real l, m;  y |=> foo(j,k) |=> foo(l,m) endproperty Does the tool have to infer that (a,b) should be ints, or is it up to the user to not shoot themselves in the foot? This seems to get especially weird when combined with the local-variables-as-parameters feature. Really I'm just wondering if anyone out there with more experience with this sort of thing can clarify what the burden on the compiler is intended to be? Thanks, MikeP BlueSpec, Inc Back to top edcerny Senior Joined: Jan 12, 2004 Posts: 55 Location: Marlborough, MA Posted: Tue Jun 15, 2004 9:52 pm    Post subject: Type-Checking SVA Parameters The type is checked when the sequence / property is expanded with the actual parameters in the place of instantiation. ed Back to top bdeadman Senior Joined: Jan 06, 2004 Posts: 204 Location: Austin, TX Posted: Tue Jun 15, 2004 10:16 pm    Post subject: Since SVA and PSL are supposed to have been aligned semantically (thanks to Cindy, John etc.), I believe Ed's correct that the type checking is done after expansion. My understanding is also that after expansion, the boolean expressions must be legal Verilog booleans, as extended in whatever way SystemVerilog extended Verilog 1364, and that the booleans must be resolveable to true or false, that is to say, in your example, if SV supports the comparison of mis-matched types in, say, an if .. else construct, then SVA ought to support it, and if it doesn't, then SVA shouldn't. In summary I think everything is therefore checkable at compile time. Because of this I can't for the moment envisage any circusmtances where "weird runtime errors" might occur. Can you suggest examples? Regards Bernard Back to top MikeP Junior Joined: Jun 15, 2004 Posts: 5 Location: Waltham, MA Posted: Wed Jun 16, 2004 10:53 am    Post subject: Thanks for your prompt responses. It seems we're getting into some of the subtleties of the spec. It seems reasonable to perform type checking after expansion to avoid some of these issues. However, it still seems strange to me that the parameters to SVA sequences do not have their types explicitly specified by the user. I guess that's because the type may not be known, but SV has no support for general polymorphic types outside of the class system. One thing that's not so clear in the spec is if local variables can be used in array indices or bounds of temporal expressions. If so, you could definitely generate run-time errors. Two quick examples: Code: sequence array_var   int x;   (data_in && !data_out, x = data_in) ##1 array[x] //uh-oh endsequence sequence temp_var   int x;   (data_in &&& !data_out, x = data_in) ##[5:x] data_out //x < 5??? endsequence Anyone have any thoughts on whether or not this is intended to be a legal use of SVA local variables? In the first example we can use normal SV behavior as an example, but the temporal notation occurs only in SVA. Thanks, MikeP Bluespec Back to top bdeadman Senior Joined: Jan 06, 2004 Posts: 204 Location: Austin, TX Posted: Wed Jun 16, 2004 11:35 am    Post subject: Mike, My first reaction is this is yet another good reason why it's a bad idea to make assignments from within properties! There are a ton of others related to the use of properties within Formal tools. There is also another problem you may not have seen yet. Suppose the temporal expression contains multiple OR'd sub terms. One of the problems we face when creating master / slave verification IP from temporal expressions is the assignments in ALL of the sub terms must be identical until the time that all but one of the sub terms is eliminated. The issues with AND'd terms are even worse, and take a lot of awkward checking. I'm afraid I don't know the answer to your specific question about polymorphism, though I'll try to read the LRM again when I get a moment. Have you tried to contact one of the semantics experts directly? Regards, Bernard Back to top vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1238 Location: Los Angeles, CA Posted: Thu Jun 17, 2004 11:36 am    Post subject: Quote: Code: sequence array_var   int x;   (data_in && !data_out, x = data_in) ##1 array[x] //uh-oh endsequence sequence temp_var   int x;   (data_in &&& !data_out, x = data_in) ##[5:x] data_out //x < 5??? endsequence 1. With regards to your statement "no types associated with arguments (a, b, c).", you are correct. Thee are benefits and issues: * BENEFITS: You can pass as arguments objects of any type, and you can also pass sequences. FOr example: Code:   sequence s1(a, b, c); a ##1 b ##[0:5] c; endsequence    sequence s2; x ##1 y; endsequence   property p; a |=> s1(w, s2, z); // note that s2 is a sequence passed to s1   endproperty Thus p is equivalent to:   a|=> w ##1 x ##1 y ##[0:5] z; *PROBLEMS The problems occur when doing comparisons. Above example works if all objects are single bits. The following sequence is problamatic if a, b, c are of different types of vectors of different lengths. sequence s3(a, b, c); a==b ##1 c; endsequence Another problem would occur is a call to s3 passes sequences as arguments. Can't compare sequences! 2. local variables can lead to unexpected errors. If someone has a solution for the followwing property please pass it on. Code: // data is passed into a synchronous FIFO and is sent out up to 100 cycles later. property datain2dataout;   logic [31:0] vdata; // store incoming data   (load, vdata=datain) |=> ##[0:100] dout && dataout==vdata;   // when load, store input data to local variable   // when fifo spits out data (dout control),   //check that the output data is same as what was stored. endproperty SO far, property looks very good. Now suppose that I get the following stream: @cycle 2, load==1, datain== 1 // starts check for thread 1 // and later, dataout== vdata == 1 @cycle 15, load==1, datain==15 // starts check for thread 2 @cycle 50, dout==1 and dataout==1 PROBLEM!!! Thread 1 checks OK and passes Thread 2 FAILS, it expected dataout to equal 15 (vdata for thread 2) This is a very common problem, and I am baffled at finding a good solution. _________________ Ben Cohen http://www.systemverilog.us/ * SystemVerilog Assertions Handbook, 3rd Edition, 2013 * A Pragmatic Approach to VMM Adoption * Using PSL/SUGAR ... 2nd Edition * Real Chip Design and Verification * Cmpt Design by Example * VHDL books Back to top vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1238 Location: Los Angeles, CA Posted: Thu Jun 17, 2004 11:58 am    Post subject: Code: sequence array_var   int x;   (data_in && !data_out, x = data_in) ##1 array[x] //uh-oh endsequence sequence temp_var   int x;   (data_in &&& !data_out, x = data_in) ##[5:x] data_out //x < 5??? endsequence I forgot to comment on this code. Below is what I believe is true. I am not sure if the LRM really clarifies those point. Anyone with info or clarification on this please reply; Question 1: Can a local variable be used as an index, like array[x]? My thoughts: Probably yes. From SV3.1a LRM Quote: 17.4.1 Operand types ...— dynamic arrays Fixed size arrays, packed or unpacked, can be used as a whole or as part selects or as indexed bit or part selects. The indices can be constants, parameters, or variables. Question2: Can the delay range be dynamic using a variable, like ##[5:w] My thoughts: NO. The range must be known at compile time, like ##[0:5], or ##[0:$] With an SV compiler, I tried defining a range using a formal paramater, but that failed the compilation. Following is illegal sequence illegal (size) a ##[0:size] b; endsequence .. OK, this is not the same thing.. but I thought I would add it. _________________ Ben Cohen http://www.systemverilog.us/ * SystemVerilog Assertions Handbook, 3rd Edition, 2013 * A Pragmatic Approach to VMM Adoption * Using PSL/SUGAR ... 2nd Edition * Real Chip Design and Verification * Cmpt Design by Example * VHDL books Back to top Ajeetha Senior Joined: Mar 29, 2004 Posts: 424 Location: Bengaluru, India Posted: Thu Jun 17, 2004 2:01 pm    Post subject: vhdlcohen wrote: Question2: Can the delay range be dynamic using a variable, like ##[5:w] My thoughts: NO. The range must be known at compile time, like ##[0:5], or ##[0:$] LRM seems to be very clear on this, it allows either: 1. Constant expressions or 2. " $ " to indciate a finite, but unbounded maximum. Ref: 17.7.2 of 3.1a LRM. So a variable is not allowed for "repetition count in sequences". Thanks, Ajeetha _________________ Ajeetha Kumari, CVC Pvt Ltd. http://www.cvcblr.com * A Pragmatic Approach to VMM Adoption http://www.systemverilog.us/ * SystemVerilog Assertions Handbook * Using PSL/Sugar Back to top Ajeetha Senior Joined: Mar 29, 2004 Posts: 424 Location: Bengaluru, India Posted: Thu Jun 17, 2004 2:22 pm    Post subject: Quote: I forgot to comment on this code. Below is what I believe is true. I am not sure if the LRM really clarifies those point. Anyone with info or clarification on this please reply; Question 1: Can a local variable be used as an index, like array[x]? My thoughts: Probably yes. From SV3.1a LRM 17.4.1 Operand types ...— dynamic arrays Fixed size arrays, packed or unpacked, can be used as a whole or as part selects or as indexed bit or part selects. The indices can be constants, parameters, or variables. Ben, reading 17.4.2, variables used in expressions must be "static", so I am not clear whether "assertion local variables" are allowed in this context? Does your compiler allow this? Can any one please clarify? TIA, Ajeetha _________________ Ajeetha Kumari, CVC Pvt Ltd. http://www.cvcblr.com * A Pragmatic Approach to VMM Adoption http://www.systemverilog.us/ * SystemVerilog Assertions Handbook * Using PSL/Sugar Back to top vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1238 Location: Los Angeles, CA Posted: Thu Jun 17, 2004 2:27 pm    Post subject: Quote: Ben, reading 17.4.2, variables used in expressions must be "static", so I am not clear whether "assertion local variables" are allowed in this context? Does your compiler allow this? It would be nice to have a compiler that fully supports SystemVerilog and SystemVerilog Assertion!!! Does anywone know of a compiler (without a simulator) that checks compliance of code to LRM? _________________ Ben Cohen http://www.systemverilog.us/ * SystemVerilog Assertions Handbook, 3rd Edition, 2013 * A Pragmatic Approach to VMM Adoption * Using PSL/SUGAR ... 2nd Edition * Real Chip Design and Verification * Cmpt Design by Example * VHDL books Back to top bdeadman Senior Joined: Jan 06, 2004 Posts: 204 Location: Austin, TX Posted: Thu Jun 17, 2004 3:12 pm    Post subject: Ben Cohen wrote: Quote: local variables can lead to unexpected errors. If someone has a solution for the followwing property please pass it on Sorry to disagree, but I don't think this has anything to do with whether the variable is local, static or anything else - it seems to me the *REAL* problem is the property has no way to distinguish which output of the FIFO is the one it should be checking! What would happen if there are already three entries in the FIFO? How does the property know it should verify the FOURTH output data value? This leads me to the observation that for all that Property (aka Assertion) based verification is proclaimed, there are some things that one would think ought to be easy but which are actually EXTREMELY difficult to define. Amongst these I would include over-run / under-run on FIFO's & pipelines, CRC's, checksums etc. My guess Ben is the only way you can handle your FIFO problem is as a white box test - I think you have to have access to the counter(s) that tells you the number of items in the FIFO at any time. Regards, Bernard Back to top bdeadman Senior Joined: Jan 06, 2004 Posts: 204 Location: Austin, TX Posted: Thu Jun 17, 2004 3:23 pm    Post subject: Mike wrote: Quote: However, it still seems strange to me that the parameters to SVA sequences do not have their types explicitly specified by the user. I guess that's because the type may not be known, but SV has no support for general polymorphic types outside of the class system. One thing that's not so clear in the spec is if local variables can be used in array indices or bounds of temporal expressions. If so, you could definitely generate run-time errors. having looked at this again I realize that section 17.4.1 of the LRM says : Quote: The following [operand] types are not allowed: — non-integer types (time, shortreal, real and realtime) — string — event — chandle — class — associative arrays — dynamic arrays Since they've excluded "class", doesn't this therefore disallow polymorphism? Regards Bernard Back to top vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1238 Location: Los Angeles, CA Posted: Thu Jun 17, 2004 3:43 pm    Post subject: Quote: Sorry to disagree, but I don't think this has anything to do with whether the variable is local, static or anything else - it seems to me the *REAL* problem is the property has no way to distinguish which output of the FIFO is the one it should be checking! What would happen if there are already three entries in the FIFO? How does the property know it should verify the FOURTH output data value? The only thing though is that local assertion variables maintain their own copy with each threa. Quote: This leads me to the observation that for all that Property (aka Assertion) based verification is proclaimed, there are some things that one would think ought to be easy but which are actually EXTREMELY difficult to define. Amongst these I would include over-run / under-run on FIFO's & pipelines, CRC's, checksums etc. My guess Ben is the only way you can handle your FIFO problem is as a white box test - I think you have to have access to the counter(s) that tells you the number of items in the FIFO at any time. Bernard, I like your idea. The following would then work Code: / data is passed into a synchronous FIFO and is sent out up to 100 cycles later. property datain2dataout;   logic [31:0] vdata; // store incoming data   int vfifo_write_addr; // write fifo address   (load, vdata=datain, vfifo_write_addr= fifo_wr_addr) |=>     ##[0:100] dout && fifo_read_addr==vfifo_write_addr |->      dataout==vdata;   // when load, store input data to local variable   // when fifo spits out data (dout control) and the fifo read addr   // is same as what was written then   //check that the output data is same as what was stored. endproperty Notice the 2 implication operators _________________ Ben Cohen http://www.systemverilog.us/ * SystemVerilog Assertions Handbook, 3rd Edition, 2013 * A Pragmatic Approach to VMM Adoption * Using PSL/SUGAR ... 2nd Edition * Real Chip Design and Verification * Cmpt Design by Example * VHDL books Back to top bdeadman Senior Joined: Jan 06, 2004 Posts: 204 Location: Austin, TX Posted: Thu Jun 17, 2004 4:29 pm    Post subject: Ben, That's basically what I was thinking of, though it's incomplete as a test of a FIFO, because you also need to check that data is output in the order in which it was input - a LIFO buffer would satisfy your property I think. One way to do this is, if the position is maintained by a counter (I guess that's the address is your example?) is to check that "counter" other outputs take place before the output you're interested in. The problem is I'm not sure if it's possible in SVA to write a repeated sequence where the repeat count is a variable local to the instance? If that's not possible, I think a property that checks the output counter increments by one for every read, and wraps correctly, might be adequate. Extending this, my guess if the full property set for a FIFO is probably about 6-8 requirements, though I've never tried to code the whole thing. And at least it's doable this way - it's a nightmare as a black box test! Regards Bernard Back to top MikeP Junior Joined: Jun 15, 2004 Posts: 5 Location: Waltham, MA Posted: Thu Jun 17, 2004 6:00 pm    Post subject: Sorry I was away for a bit. Time to jump back in to the can of worms I opened. Ajeetha, & vhdlcohen: Quote: Question2: Can the delay range be dynamic using a variable, like ##[5:w] My thoughts: NO. The range must be known at compile time, like ##[0:5], or ##[0:$] After posting I found this in the 3.1A LRM: Quote: Section 17.6 Declaring Sequences ...A sequence can be declared with optional formal arguments... An actual argument can replace an: -Identifier -Expression -Event control expression -upper range as $ This actually seems to be saying that you the answer is YES, since I could have written a $ for the upper range in my example. These two issues in general seem to break the ability to compile assertions into hardware for co-evaluation purposes. But perhaps I'm missing something and they can be expanded statically? For example, there supposedly exist methods to translate SVA into PSL. If so, then they must have to transform away cases like this somehow, or are local variables not translated? Bernard: Quote: There is also another problem you may not have seen yet. Suppose the temporal expression contains multiple OR'd sub terms. One of the problems we face when creating master / slave verification IP from temporal expressions is the assignments in ALL of the sub terms must be identical until the time that all but one of the sub terms is eliminated. The issues with AND'd terms are even worse, and take a lot of awkward checking. Hmm, I thought they tried to deal with that by restricting the variable flow rules to handle this in some nice way. I'll have to take a look again at Appendix H again. Bernard, part 2: Quote: Since they've excluded "class", doesn't this therefore disallow polymorphism? Sorry, I wasn't being clear. Without thinking I was using polymorphism in the programming-language-research sense of being able to pass multiple types to the same function, not the Java-C++ sense of subclasses overloading virtual methods. I guess I should have said "parametric polymorphism" Here's a Wikipedia link for anyone who cares about such things: http://en.wikipedia.org/wiki/Polymorphism_(computer_science) Thanks to everyone for their help and insights thus far. MikeP Bluespec Back to top Display posts from previous: All Posts1 Day7 Days2 Weeks1 Month3 Months6 Months1 Year Oldest FirstNewest First         Verification Guild Forum Index -> Assertions All times are GMT - 5 Hours Goto page 1, 2  Next Page 1 of 2   Jump to: Select a forum Main----------------MainEDA NewsCommunity Services Networking----------------Looking for a jobLooking for candidates Archives----------------AssertionsCoverageFormalSimulationDesignMiscellaneous Test----------------Test  You can post new topics in this forum You can reply to topics in this forum You cannot edit your posts in this forum You cannot delete your posts in this forum You cannot vote in polls in this forum Forums ©

Verification Guild © 2006 Janick Bergeron
Web site engine's code is Copyright © 2003 by PHP-Nuke. All Rights Reserved. PHP-Nuke is Free Software released under the GNU/GPL license.
Page Generation: 1.514 Seconds