Hi Lisa, I would like to clarify the motivation of this proposal. ABV users usually don't write verification entities (I want to avoid abusing the term "checker" here) from scratch, but instantiate the ready ones from a verification library. OVL is a classic example of such a library. A verification entity in a library may contain one or several assertions, assumptions, coverage statements and also some modeling code. When the verification entity consists of a single assertion, SVA has appropriate constructs to express it. Consider the verification entity "implication": when an antecedent happens then the consequent must also happen. Here a plain property may be used as a verification entity: property implication(sequence antecedent, property consequent, context clk = $inferred_clock, rst = $inferred_disable); @clk disable iff (rst) antecedent |-> consequent; endproperty I can instantiate this property (almost) everywhere and benefit from the context inference: wire a, b, c; bit clk, d, e; ... assign a = b && c; p1: assert property (implication(a, b, clk)); always @(posedge clk) begin c <= a; d <= b; p2: assert property (implication(c, d)); end I can also easily extend my property by passing sequences or properties to it: p3: assert property(implication(c ##1 c, ##1 d, clk)); The situation changes when the verification entity consists from several properties or contains also some modeling code. I will use the OVL "checker" (=verification entity) assert_implication for illustration purposes since it is simple, but you can easily imagine more sophisticated OVL "checkers" in place of it (e.g., assert_window, etc.). (Modified) OVL assert_implication verification entity consists of an assertion and of a cover statement: assert property (@(posedge clk) disable iff (rst) antecedent |-> consequent); cover property (@(posedge clk) !rst throughout antecedent); Actually in OVL the reset is active low, but I am using an active high reset for convenience. Now we need to package these assert and cover statements together. The property construct cannot be used for this purpose. The only thing you can do is to package these statements into a module (or into an interface): module implication (bit antecedent, consequent, clk, rst); assert property (@(posedge clk) disable iff (rst) antecedent |-> consequent); cover property (@(posedge clk) !rst throughout antecedent); endmodule Now you lose the locality, the context sensitivity and the extendibility. Returning to our example: wire a, b, c; bit clk, d, e; ... assign a = b && c; implication p1(a, b, clk, 1'b0); // OK. Note explicit reset here, and posedge clk instead of clk always @(posedge clk) begin c <= a; d <= b; implication p2 (c, d); // Module instantiation illegal here, let alone the context inference end implication p3 (c ##1 c, ##1 d, clk); // Cannot pass sequences as arguments. Note also the issue with @clk Unfortunately, there is no SV construct that could solve this packaging problem unless you introduce the concept of checker. Using it, our task becomes easy: checker implication (sequence antecedent, property consequent, context, clk = $inferred_clock, rst = $inferred_disable); assert property (@clk disable iff (rst) antecedent |-> consequent); cover property (@clk !rst throughout antecedent); endmodule Now the above example can be rewritten as: wire a, b, c; bit clk, d, e; ... assign a = b && c; implication p1(a, b, clk); always @(posedge clk) begin c <= a; d <= b; implication p2(c, d); end implication p3 (c ##1 c, ##1 d, clk); I would like to stress that the HW designer is not expected to write new checkers, but to use the existing ones. The checkers would be normally written by EDA vendors, CAD people and the formal verification people. Therefore all the "wisdom" of this proposal belongs to the checker implementation. Checker instantiation is very intuitive and straightforward. Thanks, Dmitry ________________________________ From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Behalf Of Lisa Piper Sent: Monday, July 23, 2007 10:23 PM To: Seligman, Erik; sv-ac@server.eda-stds.org Subject: RE: [sv-ac] Feedback on 1900 (new 'checker' construct) Erik, I have reviewed the checker proposal. The application and use model for this is still not clear to me. How does this compare with using parametized properties in a package? My biggest concern is that this is yet another way that things could be done. The average user is going to become overwhelmed with trying to understand the alternatives. More specific questions: 1. You state that it is similar to a PSL vunit, A PSL vunit is essentially an extension of the module scope. It has the advantage over SVA bind that you do not have to bundle the code into a module with a complete port list. The signals in the vunit connect to the signals of the same name in the associated module. But you still need to know the names of the signals in the design, which resticts re-use. And it does not allow for instantiating a checker in procedural code as you have shown in these examples. (Note that PSL is adding parameter lists to vunits to address the reuse issue.) 2. How will checkers be documented to make the use easy? Is it only the clock and disable that can be inferred from context? How does the user know what will be inferred? It would be very confusing from a debug perspective if some properties do infer and some do not, as shown in example 3. My fear is that it will be as difficult to learn libraries as it is to just learn the underlying language. 3. To debug a failure, won't the user need to be able to understand SVA? Is the goal of the user not needing to understand SVA realistic or desired? 4. This will allow always blocks within always blocks, where the top level always block has what effect? 5. Instantiation of a 'checker' inside an 'always' block makes this equivalent to a kind of module inside an always block. This is against the Verilog language in general. It also allows user to put things inside an always block which are not otherwise legal in Verilog (e.g assign statements). This will make things confusing without any real benefit. 6. There is a statement that checkers may not include module, interface, or cell declarations or instantiations. What is a "cell"? 7. In example 4, is this PSL? Will PSL be allowed in a checker? ovl_width_a1: assert always ((checking & !test_sig) |-> (t >= width)) 8. How is a free variable different from a local variable? The bottom line is that I do not see any compelling reason for this new construct. Lisa -----Original Message----- From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Seligman, Erik Sent: Monday, July 23, 2007 2:54 PM To: sv-ac@eda-stds.org Subject: [sv-ac] Feedback on 1900 (new 'checker' construct) Hi guys-- I'm going to start working on the 'real' proposal (manual format) for item 1900. Please try to send any feedback you have at this point. Thanks! -- 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 <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 Tue Jul 24 08:26:47 2007
This archive was generated by hypermail 2.1.8 : Tue Jul 24 2007 - 08:26:54 PDT