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, 58 guest(s) and 1 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  Specifying properties in Verilog vs Temporal Language Goto page 1, 2, 3  Next          Verification Guild Forum Index -> Assertions View previous topic :: View next topic   Author Message vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1238 Location: Los Angeles, CA Posted: Wed Jan 28, 2004 11:44 am    Post subject: Specifying properties in Verilog vs Temporal Language Note from the editor: this topic was split from this posting Quote: This new technology allows you to write constraints and properties in Verilog so that you can also reuse constraints and properties in your normal testbenches. When the constraints and properties get very compex, you can use your normal debugging tools/methodologies to debug them! How do you write temporal constraints and properties in Verilog? Do you create FSMs? Can you provide an example? _________________ 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 jeffli Senior Joined: Jan 09, 2004 Posts: 32 Posted: Wed Jan 28, 2004 3:32 pm    Post subject: vhdlcohen wrote: Quote: This new technology allows you to write constraints and properties in Verilog so that you can also reuse constraints and properties in your normal testbenches. When the constraints and properties get very compex, you can use your normal debugging tools/methodologies to debug them! How do you write temporal constraints and properties in Verilog? Do you create FSMs? Can you provide an example? When writing testbenches in Verilog, people use "@ (posedge clk)" or similar statements to get to the next clock cycle. vhdlcohen wrote: Quote: A request shall be acknowledge within 1 to 5 cycles. property ReqAck = always {rose(req)} |=> {[*0:4]; ack}; assert ReqAck; A Verilog way to describe the above property: Code: @ (posedge req) repeat (5) begin @ (posedge clk) if (ack) ReqAck = ack; end When getting output values of Sun’s 2 floating point units for an experiment in the paper, the following code is used in an initial block: Code:         sparc_v <= 1'b0; java_v <= 1'b0;         sparc <= 32'b0; java <= 32'b0;         repeat (7) @(posedge ss_clock);         repeat (17) begin                 if (rdy && !java_v)                         {java_v,java} <= {1'b1,data};                 if (!FpBusy && !sparc_v) begin                         @(posedge ss_clock);                         sparc_v <= 1'b1;                         sparc[31] <= SignResult;                         sparc[30:23] <= ExpResult[7:0];                         sparc[22:0] <= FracResult[54:32]};                 end                 else @(posedge ss_clock);                 if (sparc_v & java_v) $finish;         end More testbench examples can be found at www.opencores.org. All project source files are available there to the public. Most of projects there have testbenches. See http://verificationguild.com/modules.php?name=Forums&file=viewtopic&p=1194#1194 for a pointer to a research paper reporting that Verilog was easier for some property checking experts to describe certain properties than a property language (which they were supposed to use). Last edited by jeffli on Thu Jan 29, 2004 9:06 am; edited 1 time in total Back to top confused Senior Joined: Jan 09, 2004 Posts: 185 Posted: Wed Jan 28, 2004 3:56 pm    Post subject: jeffli wrote: vhdlcohen wrote: Quote: A request shall be acknowledge within 1 to 5 cycles. property ReqAck = always {rose(req)} |=> {[*0:4]; ack}; assert ReqAck; A Verilog way to describe the above property: Code: @ (posedge req) repeat (5) begin @ (posedge clk) if (ack) ReqAck = ack; end This reminds me the discussion about "if (a) b = c; else b = d;" vs. "b = a ? c : d;" Back to top vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1238 Location: Los Angeles, CA Posted: Wed Jan 28, 2004 4:11 pm    Post subject: 1. I would NOT call Verilog a good language to write properties. HDLs are currently used for verification of designs using what's called "verification module". The code you displayed is a verification code, but is not a property language. You always make the point that verification checks properties of the design, but an HDL module is not a property language. By the way your Verilog code Code: A request shall be acknowledge within 1 to 5 cycles. property ReqAck = always {rose(req)} |=> {[*0:4]; ack}; assert ReqAck; A Verilog way to describe the above property: Code: @ (posedge req) repeat (5) begin @ (posedge clk) if (ack) ReqAck = ack; end  is not the same as tha PSL code. FIrst of all, the PSL code has a "rose". Also, it is more challenging to write readable property specification that is also verifiable in an HDL. I have done it for several years, and I have included such codes in my previous books. Today, I would definitely chose an ABV language, like PSL or SVA to document the requirements and to perform formal and dynamic verification with tools that understand those ABV languages. Ben _________________ 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 confused Senior Joined: Jan 09, 2004 Posts: 185 Posted: Wed Jan 28, 2004 8:14 pm    Post subject: vhdlcohen wrote: By the way your Verilog code Code: A request shall be acknowledge within 1 to 5 cycles. property ReqAck = always {rose(req)} |=> {[*0:4]; ack}; assert ReqAck; A Verilog way to describe the above property: Code: @ (posedge req) repeat (5) begin @ (posedge clk) if (ack) ReqAck = ack; end  is not the same as tha PSL code. FIrst of all, the PSL code has a "rose". Also, it is more challenging to write readable property specification that is also verifiable in an HDL. I have done it for several years, and I have included such codes in my previous books. Today, I would definitely chose an ABV language, like PSL or SVA to document the requirements and to perform formal and dynamic verification with tools that understand those ABV languages. Ben The Verilog statement is confusing. If req's rising edge and clk's rising edge are at the same time, does the checking of ack start at this edge or the next rising edge of clk? Depending on how req is generated, the answer can be different (see http://www.deepchip.com/items/0347-01.html). If the clock is not too fast, I prefer Code: @ (posedge req) #1 repeat (5) begin @ (posedge clk) if (ack) ReqAck <= ack; end When does this checking start for Ben's PSL version? Does it depend on how req is generated? According to IBM's Sugar 2.0 specification, "The built-in function rose() is another way of saying posedge in Verilog-flavored Sugar." What is rose() in PSL? Back to top vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1238 Location: Los Angeles, CA Posted: Wed Jan 28, 2004 8:42 pm    Post subject: Quote: @ (posedge req) #1 repeat (5) begin @ (posedge clk) if (ack) ReqAck <= ack; end When does this checking start for Ben's PSL version? Does it depend on how req is generated? According to IBM's Sugar 2.0 specification, "The built-in function rose() is another way of saying posedge in Verilog-flavored Sugar." What is rose() in PSL? Per LRM, rose is true if signal is true at the current cycle and false in the previous cycle. With a default clock, the check is done at the test edge of the clock (e.g., posedge). If req is generated in an always block with nonblocking assignment, req will effectively be after all the blocking assignments. I like to think of it as a delta time (even though Verilog does not view the simulation timing as VHDL). Thus, if posedge of clock occurs at time 100, 200, 300 and req rises at 100 + 1 delta, rose (req) will be true at time 200 (+ 0 delta). In "(posedge req) repeat (5) begin @ (posedge clk) if (ack) ReqAck <= ack; end" if good coding styles are used (see CLiff Cummings guidelines on blocking/nonblocking), then posedge req occurs at 100 + 1 delta,, and the first "if (ack) " would occur at time 200 (+ 0 delta). Thus, teh result is the same as the PSL rose. However, "I know PSL, and Verilog code is NO PSL" Actually, the Verilog code is nothing more than a verification module, and is not a property language. More complex sequences and properties would require more complex HDL code. PSL is more expressive. Ben _________________ 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 confused Senior Joined: Jan 09, 2004 Posts: 185 Posted: Wed Jan 28, 2004 11:42 pm    Post subject: vhdlcohen wrote: Quote: @ (posedge req) #1 repeat (5) begin @ (posedge clk) if (ack) ReqAck <= ack; end When does this checking start for Ben's PSL version? Does it depend on how req is generated? According to IBM's Sugar 2.0 specification, "The built-in function rose() is another way of saying posedge in Verilog-flavored Sugar." What is rose() in PSL? Per LRM, rose is true if signal is true at the current cycle and false in the previous cycle. With a default clock, the check is done at the test edge of the clock (e.g., posedge). If req is generated in an always block with nonblocking assignment, req will effectively be after all the blocking assignments. I like to think of it as a delta time (even though Verilog does not view the simulation timing as VHDL). Thus, if posedge of clock occurs at time 100, 200, 300 and req rises at 100 + 1 delta, rose (req) will be true at time 200 (+ 0 delta). Thanks for the education, Ben! So, the Verilog code equivalent to the PSL property might be Code: while (req) @ (posedge clk); // look for false while (!req) @ (posedge clk); // look for true repeat (5) begin @ (posedge clk) if (ack) ReqAck <= ack; end It is not as good looking as the earlier 2 Verilog versions, but it will miss narrow req pulses that do not cross clk's rising edges. It seems unfair to ask a PSL property to cover such unlikely pulses. Back to top vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1238 Location: Los Angeles, CA Posted: Thu Jan 29, 2004 11:24 am    Post subject: Quote: while (req) @ (posedge clk); // look for false while (!req) @ (posedge clk); // look for true repeat (5) begin @ (posedge clk) if (ack) ReqAck <= ack; end I would rather say that Code:  // A request shall be acknowledge within 1 to 5 cycles. property ReqAck = always {rose(req)} |=> {[*0:4]; ack}; assert ReqAck; is more in Verilog like: @ (posedge req) repeat (5) begin @ (posedge clk) if (ack) ReqAck <= ack; end If req rises at time 100 + 1 delta, then in PSL rose(req) will be true at time 200 + 0 delta (assuming a default clock). In above code, if req rises at time 100 + 1 delta, then at next posedge, at time 200 + 0 delta the "if (ack) .." statement will be executed. In any case, the Verilog solution is not as elegant as PSL, nor does it provide the verification (unless more code is added). _________________ 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 confused Senior Joined: Jan 09, 2004 Posts: 185 Posted: Thu Jan 29, 2004 6:21 pm    Post subject: In the version with 2 while loops, if req rises at time 100 + 1 delta, the first loop finishes before 100 + 1 delta, and the second loop finishs at 200 + 0 delta. Then the last line should be "repeat (5) begin if (ack) ReqAck <= ack; @ (posedge clk); end " so that at time 200 + 0 delta the "if (ack) .." statement will be executed. I do not like Verilog, either. It is too flexible, and you have to think like a simulator when reading unsynthesizable code. Any language (or coding style) with cycle-based semantics is easier to understand to people like me. vhdlcohen wrote: I would NOT call Verilog a good language to write properties. HDLs are currently used for verification of designs using what's called "verification module". In addition to coding style differences between a property and a verification module, is there any conclusion that certain bugs can be caught by only one of them but not by the other? Back to top vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1238 Location: Los Angeles, CA Posted: Fri Jan 30, 2004 2:15 pm    Post subject: Quote: In addition to coding style differences between a property and a verification module, is there any conclusion that certain bugs can be caught by only one of them but not by the other? Good question! 1. Properties defined in a language like PSL can be formally verified with a model checking tool, thus proving that the design meets the properties. If it does not, then counterexample are provided by the tool. In our book, I used a traffic light controller design with side and emergency traffic. I was "sloppy" in the coupling of the two FSMs, and interestingly enough model checking showed my design had all kinds of problems, including a case, whic under certain circumstances, would cause all lights to go GREEN at the same time. Another design with more closely coupled FSMs was later on proven to work OK. 2. You need enough meaningful properties to prove the design. 3. Simulation relies on the test vectors and on the design of the verfier module (or checker). It is not as complete of a proof as model checking. However, simulation was proven to work. 4. Properties with a language like PSL provide additional benefits of verification with a verifier. These inlcude easier to write code; easier to express a range of arrival of events, which can occur as a result of tuning the RTL for timing; easier review; documation tagged with the design / interface / requirements. Bottom line, with properties, verification depends on teh qulaity of the properties and the tool used. Model Checking does an excellent job using exhaustive proof, but works best on control driven logic verses arithmetic logic. Simulation depends on the quality of the testbench (vectors and verifier). _________________ 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 alexg Senior Joined: Jan 07, 2004 Posts: 586 Location: Ottawa Posted: Sat Jan 31, 2004 11:40 pm    Post subject: Ben, Here is my opinion about the properties and language choises. Before starting to write any verification component such as checker or scoreboard, we decide about the set of properties this component must verify. Once decided, it is really good idea to divide properties implementation from each other, if it's possible. In these case, debugging / enhancement / shutdown of specific property will not have influence to the rest of them, and complexity of the whole system will be beaten by "divide and conquer" approach. Now, these properties can be implemented in many ways. My personal experience shows, that language choise is not as important as an ability to architect verification environment in "modular" way, identifying the propeties, their priorities and dividing them from each other in implementation. Speaking about language choises, I believe that Verilog is good enough for specifying properties, once verilog code is clear and easy to understand. Another good choise is OVL and OVL-like enhancements for specific needs of the system. Myself, I prefer to write 3-5 lines of clear verilog code which does not require comments rather than writing one line of PSL code followed by 3-5 lines of comments. In my opinion, now Verilog is still more reusable than the other languages because of 3 reasons: 1. Everybody in R&D may be able to understand and modify the code 2. Debugging is easier and not tools-specific 3. Verification code remains tools-independent, which is always good, once thinking about potential ability to share the code with another company. Regards, Alexander Gnusin Back to top vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1238 Location: Los Angeles, CA Posted: Sun Feb 01, 2004 9:06 pm    Post subject: Quote: Before starting to write any verification component such as checker or scoreboard, we decide about the set of properties this component must verify. Once decided, it is really good idea to divide properties implementation from each other, if it's possible. In these case, debugging / enhancement / shutdown of specific property will not have influence to the rest of them, and complexity of the whole system will be beaten by "divide and conquer" approach. Hats off on deciding to go with ABV approach. You would be surprised as to the opposition in using such a beneficial approach. Quote: Now, these properties can be implemented in many ways. My personal experience shows, that language choice is not as important as an ability to architect verification environment in "modular" way, identifying the propeties, their priorities and dividing them from each other in implementation. Partitioning the verification envirnoment and the properties is important. Language is a part of expression and is important though. Otherwise, why not write ALL programs in assembly or microcode? Quote: Speaking about language choices, I believe that Verilog is good enough for specifying properties, once verilog code is clear and easy to understand. Another good choise is OVL and OVL-like enhancements for specific needs of the system. Myself, I prefer to write 3-5 lines of clear verilog code which does not require comments rather than writing one line of PSL code followed by 3-5 lines of comments. In my opinion, now Verilog is still more reusable than the other languages because of 3 reasons: 1. Everybody in R&D may be able to understand and modify the code 2. Debugging is easier and not tools-specific 3. Verification code remains tools-independent, which is always good, once thinking about potential ability to share the code with another company. I have several comments here: PSL evaluates expresssions with the "always" and "never" at every cycle in a mutli-thread manner. Thus, given property P = always {rose(a); b; [*0:5]; c} |=> {[*0:3]; d}; the 'cause' sequence is tested at every cycle in a multi-threaded manner. However, a single occurrence of 'd' can terminate the property. The PSL implementation implies a linked list, something that cannot be done in Verilog PSL is more than just a property specification because tools support the verification aspect thru simulation and formal verification. I agree that simple properties, like the ones expressed in OVL, can be done in an HDL. In fact OVL does that. However: The HDL modeling is not that trivial and not that easy to read as PSL Complex properties require complex FSMs The multithreading aspect of the properties cannot be expressed. All verification thru simulation need to have verification code embedded in the HDL. That diffused the purpose of the property. You can't do formal verification with HDL properties with current tools If HDL (e.g., Verilog) were a better property specification language, then Accellera really wasted their time in specifying PSL and SVA (SystemVerilog Assertion) in SystemVerilog. Vendors also would be blowing away a lot of investment money in developping tools that support property specification languages. Same comments goes for companies that are adopting ABV with PSL. Of course that goes for authors of books who addressed PSL . Bottom line, I disagree that a few Quote: write 3-5 lines of clear verilog code which does not require comments rather than writing one line of PSL code followed by 3-5 lines of comments. ... 1. Everybody in R&D may be able to understand and modify the code 2. Debugging is easier and not tools-specific That because, it would take a lot more thatn a 3-5 lines of clear Verilog code to express complex assertions, that can be expressed in 3 lines of PSL code. Also, once you get used to an ABV language, it is not that difficult to read. In fact it is a lot easier to read that Verilog which includes several FSMs, and multiple always blocks. PSL tool also collect statics on the properties, and coverage properties can easily be written to determine functional coverage. If I had less than a dozen properties, I can live with HDL written properties. However, a real design may have hundreds of properties, and that can be extremely burdensome with Verilog as a property specification and verification language. Sorry!!! I do agree with the rest of your statements though Quote: Verification code remains tools-independent, which is always good, once thinking about potential ability to share the code with another company. Sure, you already have the simulator. But is what about the cost in developping and debugging the Verilog propertiies? How does that balance witht he cost of the tools? PSL is an Accellera standard supported by many tools today. I wouold not be surprised if PSL and SVA would be a requirement imposed by the contracting agency onto the subcontractors, just like Verilog or VHDL with synthesis is imposed today as the HDL of choice. In fact, I doubt that contracting agency would accept digital designs in schematic capture, even though I heard several arguments that schematics are definitely far better than HDL to capture designs ... but that's another story. If we start taling about this, Janick will relabel the topic! _________________ 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 confused Senior Joined: Jan 09, 2004 Posts: 185 Posted: Mon Feb 02, 2004 10:41 pm    Post subject: vhdlcohen wrote: The multithreading aspect of the properties cannot be expressed If multithreading is a kind of concurrency, what concurrency cannot be expressed in Verilog? Or why is multithreading not concurrency? Why cannot a linked list be done in Verilog? I can understand something is easy or hard, but ... vhdlcohen wrote: You can't do formal verification with HDL properties with current tools It is hard to understand why the current tools have trouble with HDL properties. All of them read the designs in HDL. If they do not like the syntax of HDL properties, we can use HDL to generate A and B. Then just use "property P = always A |=> B;" for each HDL property. Actually, we can do this for every testbench. After generating 2 signals START_CHECKING and TEST_FAILING to each testbench and making the simplest property based on these 2 signals, all testbenches should satisfy the syntax requirement of all formal property checking tools. What am I missing? Back to top vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1238 Location: Los Angeles, CA Posted: Tue Feb 03, 2004 6:40 pm    Post subject: Quote: If multithreading is a kind of concurrency, what concurrency cannot be expressed in Verilog? Or why is multithreading not concurrency? Why cannot a linked list be done in Verilog? I can understand something is easy or hard, but ... Whay I mean by multithreading is that in PSL, every sequence in a thread is handled independently. Thus, property P = {rose(a); b; c; d} |=> [*0:4]; e; f}; every rose(a) starts the sequence test, and if that sequence on the left is all true, then the sequence on the right is checked. Verilog does not support pointers. Quote: It is hard to understand why the current tools have trouble with HDL properties. All of them read the designs in HDL. If they do not like the syntax of HDL properties, we can use HDL to generate A and B. Then just use "property P = always A |=> B;" for each HDL property Actually, I spoke too fast. A search on the web showed that some tools do support Verilog as a property language. Synopsys Magellan is one of them. Quote: "Magellan can be used to verify design RTL written in Verilog or VHDL. For maximum flexibility, properties and assumptions can be specified in OpenVera™ Assertions, Verilog or VHDL. Magellan can also use the predefined checks from the Open Verification Library. In addition, Magellan is architected to work with the emerging SystemVerilog standard." HOWEVER, usign Verilog as a property language is very cumbersome when expressing complex properties, as it is required to also write FSMs to keep track of sequences. Also, there were too many properties languages, and there was a need to standardize. This is why Accellera wen through a study to select a language. Quote: Actually, we can do this for every testbench. After generating 2 signals START_CHECKING and TEST_FAILING to each testbench and making the simplest property based on these 2 signals, all testbenches should satisfy the syntax requirement of all formal property checking tools. What am I missing? For simple assertions, one can une OVL, or as you said Verilog. In fact VHDL has the "assert" statement. For fomal model checking, you'll find a lot of support by vendors in the use of Accellera stamdards for property definition, including PSL, SVA, and OVL. Again, OVL is limitied. There currently are no vendors that support SVA (exept possibly for beta). PSL is however well supported in both simulation and formal verification. _________________ 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 confused Senior Joined: Jan 09, 2004 Posts: 185 Posted: Fri Feb 06, 2004 11:28 pm    Post subject: alexg wrote: Once decided, it is really good idea to divide properties implementation from each other, if it's possible. In these case, debugging / enhancement / shutdown of specific property will not have influence to the rest of them, and complexity of the whole system will be beaten by "divide and conquer" approach. What properties to verify certainly is more fundamental than the language selection, but it might not be easier. Traditionally, most projects divide the verification task by classifying input sequences. The classification is often based on what internal structures are used. ABV seems different. Ignoring the automatically generated properties, how to decide what properties to verify? Properties seem not made to classify input sequences while testbenches are. Properties are often about internal states while testbenches are mostly about external behavior. I am not sure whether they are supposed to be different in these ways. Can properties be similar to testbenches (ignoring the language differences)? How do they support different "divide and conquer" choices that testbenches do not? 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, 3  Next Page 1 of 3   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: 9.340 Seconds