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 0 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 Previous  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: Sat Feb 07, 2004 12:25 am    Post subject: Quote: Traditionally, most projects divide the verification task by classifying input sequences. The classification is often based on what internal structures are used. Given a requirement specification (English or PSL end-to-end properties), the internal structure of the design should NOT play a role in the verification task. I am not clear on what you mean here. Quote: 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. As explained and demonstrated in our 2nd edition PSL book, properties can be classifed as: 1. System -- end-to-end For example property PiToPCIxyz = always {xaction.send256to_pi} |-> {[*100:499]; pci_start_xfr}; // given a command to transfer 256 words from PI bus to PCI bus, the pci start of data transfer should occur with 100 to 500 cycles Another system level requiement example: When the CPU commands a FilterX operation, the image processing subsystem shall perform the FilterX operation, as described by the function FilterX. The FilterX operation on a scene image of size 100 x 100 pixels shall be formed in less than 1000 cycles. property FilterXProcessing = always {xaction.do_FilterX_cmd && image_processor.scene_loaded} |-> {[*700:999]; image_processor.done_FilterX }; property FilterXProcessingCheck = always image_processor.done_FilterX -> image_processor.FilterX_scene == FilterX(xaction.sent_scene); 2. Interface - like a PCI bus properties 3. RTL design -- properties within the RTL for white-box verification. 4. coverage -- interesting issue, also addressed in our book. Your question: Which properties to verify? Answer: All of them. The 'cause - effect' nature of typical properties facilitate the definition of tests in a test plan. In the image processing example, there is a need to load an image. In transaction-based testbench, the loading of the image is the transaction. The verification is definitely eased because of a user-defined verifier with scoreboard and FSMs and counters, the HDL with PSL simulator with verify the properties. The inline (in the RTL) properties verify the lower level design characteristics and report errors. Quote: 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. Properties are thus about characteristics of the requirements and design, and not necessarily the internal states. Testbenches are really about providing the stimulus vectors and verifying the behavior. Typically, the observed behavior is, as you said, from the interfaces (black-box) level. However, it is possible in HDL to access intennal signals of a design, and more gray or white-box verification is possible. Quote: Can properties be similar to testbenches (ignoring the language differences)? How do they support different "divide and conquer" choices that testbenches do not? Properties are NEAT because they define the design from its onset, from teh requirement level. They also are used for the definition of the interfaces, and by the designer to specify, document, and provide verification of characteristics of the interanal design. PSL is great in that aspect. Aside from verification thru simulation or model checking, the abbreviated syntax enables the authors to write more assertions. It also facilitates code reviews because it becomes clearer as to the direction the the design is taking. Take for example this inline property written by a designer: property FirePyro = always {rose(Fire_PyroX_CMD==FIRE)} |=> {[*0:4]; PyroX_relay==ACTIVATED}; At code review, a system engineer can look at this and say: Hey, wait a minute! should you check that the FPGA is charged ant that the clock is running, and the CPU armed the system? I think the property should be: property FirePyroSafe = always {Fire_PyroX_CMD==FIRE &&  power_stable && fpga_charged && reset_cycle== DONE && armed == OK} |=> {[*0:5]; PyroX_relay==ACTIVATED}; For those who still doubt the value of PSL and the notion of properties written in a readable manner, I would like to inform you that the Wide-Field Infrared Explorer (WIRE) satellite was lost in space in March, 1999 Lost due to misfiring of pyros @ powerup because of that VERY problem discussed above. If the review committee had thoroughly reviewed the functional requirements, and those additional safety properties were recognized, the hardware could have been designed to protect from early firing of the relays. For whatever it is worth, the rest of the satellite electronics probably worked OK. It's just that the satellite was lost! Note from the editor: this article spawned the following 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: Sat Feb 07, 2004 12:32 am    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? At least, what are the interesting "divide and conquer" choices? Back to top srini Senior Joined: Jan 23, 2004 Posts: 430 Location: Bengaluru, India Posted: Tue Feb 10, 2004 3:37 pm    Post subject: Quote: 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. Here is where I tend to think of differntiating Properties from the conventional term "assertions". Assertions, as has been known for over a decade now, can be as simple as Verilog's $display, VHDL's assert, 0-in directives, OVL etc. And I tend to agree with the OP that these are more close to the "internal states" than extrenal. In my view, Properties are more "external", i.e. as Ben has elaborated end-to-end/System behavior, any expected latency requirement (saying I should get an ack within 100 clocks, no matter what happens). Properties, along with formal methods can be of EXTREME use in "Performance measurement" of digital systems - some thing that our latest book elaborates on. This is something that's fundamentally different from Simulation based verification, a testcase can say whether we are meeting a 4-cycle latency in a pipelined design for "this particular stream/sequence of inputs", while a formal tool + PSL Property can tell you when you will NOT be able to meet it!! Having said this, let's be aware that the tools are not yet matured enought to completely handle a huge design for performance measurement formally. Back to top srini Senior Joined: Jan 23, 2004 Posts: 430 Location: Bengaluru, India Posted: Tue Feb 10, 2004 3:51 pm    Post subject: Quote: Can properties be similar to testbenches (ignoring the language differences)? How do they support different "divide and conquer" choices that testbenches do not? Let me add my 2 cents worth. Properties are just that - "Properties of your design/system/environment". Properties about the design (and hence its implementation/internal structure) are often known as "assertions". Properties about the "system" being built - are the "system requirements, specifications, interface properties" etc. Properties about the env - constraints & assumptions. IMO PSL is made to fit all the 3. In fact I personally prefer to use the term "PBV - Property Based Verification" than ABV Now, coming to your "property vs testbenches" - some properties can find way into the TB as additional checkers/monitors, either through inherent support of PSL (tools such as NCSIM, Modelsim etc.), or through "PLI - such as Safelogic's Monitor" or via a PSL-2-HDL conversion such as IBM's FoCs (supports Sugar 2.0). Recently, tools are being developed to "extract test sequences" automatically from your properties - properties about your environment, constraints/assumptions. Also, any formal tool, when used with PSL - if it finds a possible failure of a property, can generate a "sequence" that could be a VCD/a rwa testbench code. What would be more interesting is to be able to generate "Functional coverage points" automatically for failing properties in a HVL such as E/VERA through a formal tool. I am not aware of any EDA tool doing this as of now. Needless to say - all these are addressed with examples in our book! Srini & Aji Back to top srini Senior Joined: Jan 23, 2004 Posts: 430 Location: Bengaluru, India Posted: Tue Feb 10, 2004 4:12 pm    Post subject: Quote: 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. Not intended to be negative, but a quick look at the recent bugs found in OVL (Please don't take it in the -ve sense, I have GREAT respect to OVL) - walk through the mailing list archive - "Debuuing a HDL property" can be heavily time consuming - primarily b'cos of any HDL's "programming nature". What we really need for a good Property language is a "formal, mathematically precise, un-ambiguous" specification language - one that doesn't worry too much about type declarations, size of vectors etc. Agreed - PSL/SVA is not the easiest thing on earth - especialy for many engineers, who are, for so long used to the "programming nature" of HDLs and HVLs. But once you get used to it, it becomes extremely easier to "abstract" the intention at such a high level that would be close to impossible using HDL/HVL. I am NOT talking about simple assertions such as one hot check, rather more end-to-end properties (as Ben has shown in other replies). IMHO - PBV/ABV is a paradigm shift and it has to overcome the hurdle of being so precise/abstract(at times vague ). I believe that PSL adoption has to come from both bottom-up and top-down, i.e. using assertions/coverage is some thing designers can do immedietly, hopefully there will soon be "library" of commonly used PSL assertions available to aid here. Architects should start thinking about "executable specification" - in PRACTICE - I have been hearing this term for almost 6 years and am yet to see it in practice. Also, for standard protocols, readlily available PSL/SVA complicance checks would be GREAT! Cadence came up with one for AHB + PSL. (Our book has an improved version with a real life, completely worked out example). Debugging - you have touched upon some thing which is a really realy HOT stuff, but the LEAST researched one - especially in HW domain. Interested readers should go through Bassam's papers on "HW Debugging" Yu-Chin Hsu, Bassam Tabbara, Yirng-An Chen, Furshing Tsai, "Advanced Techniques for RTL Debugging", DAC, June 2003. Bassam Tabbara, Yu-Chin Hsu, George Bakewell, Scott Sandler, "Assertion-Based Hardware Debugging", DVCon, February 2003. We address "temporal debugging" with a small example in Section 7.2 in our book. Regards, Srini Back to top confused Senior Joined: Jan 09, 2004 Posts: 185 Posted: Tue Feb 10, 2004 10:21 pm    Post subject: srini wrote: Architects should start thinking about "executable specification" Behavioral models in C, C++, SystemC, behavioral HDL, etc. seem to be used as executable specifications. Are properties good replacements of behavioral models? When I looked last time, tools need models when taking properties. When people use properties as executable specifications, they also have to provide models. Will this always be true? Back to top vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1238 Location: Los Angeles, CA Posted: Thu Feb 12, 2004 1:08 pm    Post subject: Quote: Behavioral models in C, C++, SystemC, behavioral HDL, etc. seem to be used as executable specifications. Are properties good replacements of behavioral models? Every language expresses different notions. When addressing "executable specifications", C, C++, SstemC do a go job on the definition of data processing algorithms, like filters. Behavioral models in some way do express "properties" since by defintion, a property represent the characteristic of the design. The question though is "which language is best"? PSL is best for defining properties that deal with FSMs, controllers, etc. Basically properties that are Boolean intensive, rather than data intensive. However, one can use data intensive properties with PSL by having the data properties or characteristics processed by another layer (e.g., in Verilog or SystemC with results in files or memories at LUTs), and having the latenties and Boolean comparisons done in PSL. FOr example: property TargetDetected = always {image_loaded} |=> {700:790}; array_compare(image, expected_results)}; Array_compare is a function returning Boolean. Quote: When I looked last time, tools need models when taking properties. When people use properties as executable specifications, they also have to provide models. Will this always be true? Not necessarily. One needs a structure, like the interface signals (or entity in VHDL). However, properties can specify the expected or required defintion of the design. These definitions can be used in a specification to clarify the real intent. There are case where a "modeling layer", meaning some HDL processing is required, and PSL can tap onto those signals or registers to specify the requirements. For example, in a UART, the parallel data can be stored in a register "XMT_REG", and the serialization can be speficied in terms of bits (sequence) off this reg. e.g., {1'b0; xmt_reg[0]; xmt_reg[1]; ....; 1'b1} , thus showing the START, LSB to MSB, and a STOP. _________________ 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: Sat Feb 14, 2004 2:28 pm    Post subject: vhdlcohen wrote: Basically properties that are Boolean intensive, rather than data intensive. However, one can use data intensive properties with PSL by having the data properties or characteristics processed by another layer (e.g., in Verilog or SystemC with results in files or memories at LUTs), and having the latenties and Boolean comparisons done in PSL. Good point! Behavioral models generally do well at mapping input sequences to output sequences, but they are not good at expressing the flexibilities in the outputs. For example, a behavioral model can clearly define the output of A+B where A and B are floating point numbers. However, it is tough to indicate the timing restriction of this output in behavioral models. As Ben pointed out, properties can easily express such restrictions or flexibilities, though a behavioral language may also be able to define such properties. However, a property language may not be the best choice to define the floating point A+B. The basic assumption in verification is that everybody can make mistakes. Mistakes in behavioral models are generally uncovered with simulation. Due to the nature of properties, I do not know how simulation can show the flexibilities and restrictions in the requirements. My guess is that the mistakes in the properties are not uncovered until a model is available to run simulation. Can formal verification uncover mistakes in properties without a model (behavoral, RTL or gate level)? I am not sure what kinds of mistakes are likely in properties. Typos are certainly possible. When the number of properties is big, some properties can be redundant, incomplete/missing, or conflicting with each other. It is often desirable to get verification code debugged before getting the design under verification. Back to top confused Senior Joined: Jan 09, 2004 Posts: 185 Posted: Sun Feb 22, 2004 4:36 pm    Post subject: The original question is related to creating FSM in Verilog for a temporal property. It sounded like that FSM is a bad name because of its poor readability. FSM is the only coding style for any sequential behavior if you want to use certain tools. However, There are other Verilog coding styles for the same thing if your tool is not causing trouble. I see that OVL uses FSM whenever possible. The following is some representative OVL assertions coded in a different Verilog style.This style seems more similar to PSL. If we have PSL versions of these assertions, probably we can come up with an even closer style. Then people can make their own decisions on what is more natural to them. Code: module assert_window (clk, reset_n, start_event, test_expr, end_event);    parameter severity_level=0;    parameter msg="VIOLATION";    input clk, reset_n;    input start_event, test_expr, end_event;    always begin       wait (start_event == 1'b1 && reset_n != 0);       @(posedge clk);       while (end_event != 1'b1 && reset_n != 0) begin          if (test_expr != 1'b1)             $display(msg);          @(posedge clk);       end       @(posedge clk);    end endmodule Code: module assert_win_unchange (clk, reset_n, start_event, test_expr, end_event);    parameter severity_level=0;    parameter width=1;    parameter msg="VIOLATION";    input clk, reset_n;    input start_event;    input [width-1:0] test_expr;    input end_event;    reg [width-1:0] r_check_value;    always begin       wait (start_event == 1'b1 && reset_n != 0);       r_check_value <= test_expr;       @(posedge clk);       while (end_event != 1'b1 && reset_n != 0) begin          if (test_expr != r_check_value)             $display(msg);          @(posedge clk);       end       @(posedge clk);    end endmodule Code: module assert_transition (clk, reset_n, test_expr, start_state, next_state);    parameter severity_level=0;    parameter width=1;    parameter msg="VIOLATION";    input clk, reset_n;    input [width-1:0] test_expr, start_state, next_state;    always begin       wait (test_expr == start_state && reset_n != 0);       wait (test_expr != start_state && reset_n != 0);       if (test_expr != next_state && reset_n != 0)          $display(msg);    end endmodule Code: module assert_time (clk, reset_n, start_event, test_expr);    parameter severity_level=0;    parameter num_cks=1;    parameter flag=2'b00;    parameter msg="VIOLATION";    input clk, reset_n;    input start_event, test_expr;    parameter FLAG_IGNORE_NEW_START=2'b00;    parameter FLAG_RESET_ON_START=2'b01;    parameter FLAG_ERR_ON_START=2'b10;    always begin: checking       wait (start_event == 1'b1 && reset_n != 0);       @(posedge clk);       repeat (num_cks) begin          if (start_event == 1'b1 && reset_n != 0)             if (flag == FLAG_RESET_ON_START)                disable checking;             else if (flag == FLAG_ERR_ON_START)                $display("illegal start event");             else if (flag != FLAG_IGNORE_NEW_START)                $display("illegal flag value");          if (test_expr != 1'b1 && reset_n != 0)             $display(msg);          @(posedge clk);       end       end endmodule Code: module assert_no_overflow (clk, reset_n, test_expr);    parameter severity_level=0;    parameter width=1;    parameter min=0;    parameter max=((1<<width)-1);    parameter msg="VIOLATION";    input clk, reset_n;    input [width-1:0] test_expr;    always begin       wait (test_expr == max && reset_n != 0);       wait (test_expr != max && reset_n != 0);       if ((test_expr <= min || test_expr > max) && reset_n != 0)          $display(msg);    end endmodule Code: module assert_handshake (clk, reset_n, req, ack);    parameter severity_level=0;    parameter min_ack_cycle=0;    parameter max_ack_cycle=0;    parameter req_drop=0;    parameter deassert_count=0;    parameter max_ack_length=0;    parameter msg="VIOLATION";    input clk, reset_n;    input req, ack;    always begin : checking       // Both req and ack must go inactive prior to starting       wait (req == 1'b0 && ack == 1'b0 && reset_n != 0);       wait ((req == 1'b1 || ack == 1'b1) && reset_n != 0);       if (ack == 1'b1 && reset_n != 0) begin          $display("ack without req");          disable checking;       end       // go on if req active and ack inactive       repeat (min_ack_cycle) begin          if (ack == 1'b1 && reset_n != 0) begin             $display("ack too early");             disable checking;          end          if (req_drop != 1'b0 && req != 1'b1 && reset_n !=0)             $display("req drop");          @(posedge clk);       end       // expect ack any cycle       if (max_ack_cycle == 1'b0)          // wait forever          while (ack == 1'b0 && reset_n != 0) begin             if (req_drop != 1'b0 && req != 1'b1 && reset_n !=0)                $display("req drop");             @(posedge clk);          end       else begin : wait_for_ack          repeat (max_ack_cycle - min_ack_cycle) begin             if (req_drop != 1'b0 && req != 1'b1 && reset_n !=0)                $display("req drop");             if (ack == 1'b1 || reset_n == 0)                disable wait_for_ack;             @(posedge clk);          end          $display("ack too late");          disable checking;       end       // just get ack       if (max_ack_length != 0) begin: ack_active          repeat (max_ack_length) begin             @(posedge clk);             if (ack == 1'b0 || reset_n == 0)                disable ack_active;          end          $display("ack too long");          disable checking;       end       // ack just complete       if (deassert_count != 0) begin: finish_req          repeat(deassert_count+1) begin             if (req != 1'b1 || reset_n == 0)                disable finish_req;             (@posedge clk);             if (ack == 1'b1 && reset_n != 0)                $display("multiple ack");          end          $display("req too long");       end    end endmodule Code: module assert_change (clk, reset_n, start_event, test_expr);    parameter severity_level=0;    parameter width=1;    parameter num_cks=1;    parameter flag=0;    parameter msg="VIOLATION";    input clk, reset_n;    input start_event;    input [width-1:0] test_expr;    parameter FLAG_IGNORE_NEW_START=2'b00;    parameter FLAG_RESET_ON_START=2'b01;    parameter FLAG_ERR_ON_START=2'b10;    reg [width-1:0] r_check_value;    always begin : checking       wait (start_event == 1'b1 && reset_n != 0);       r_check_value <= test_expr;       @(posedge clk);       repeat (num_cks) begin          if (start_event == 1'b1 && reset_n != 0)             if (flag == FLAG_RESET_ON_START)                disable checking;             else if (flag == FLAG_ERR_ON_START)                $display("illegal start event");             else if (flag != FLAG_IGNORE_NEW_START)                $display("illegal flag value");          if (test_expr != r_check_value && reset_n != 0)             disable checking; // done          @(posedge clk);       end       if (reset_n != 0)          $display(msg);    end endmodule These are only for showing the coding style. Not all optional features of these OVL assertions are coded. There can also be various bugs in the code. Back to top confused Senior Joined: Jan 09, 2004 Posts: 185 Posted: Sat Mar 06, 2004 7:51 pm    Post subject: vhdlcohen wrote: 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. This feature of PSL seems assuming a pipelined implementation. With the above property, if the sequence {rose(a); b; c; d} occurs twice before the first {e; f} occurs, it requires 2 occurrences of {e; f}. Frequently, the pipelined style is not required in the implementation. I wonder how to express this flexibility in PSL. Without a pipelined implementation, if 2 occurrences of {rose(a); b; c; d} are too close, either the 1st or the 2nd is ignored and normally a response is needed to indicate such a situation. PSL should be able to express all these variations, but it is interesting to see how these properties should look like. One possible variation is that {rose(a); b; c; d} should never occur again before the last expected {e; f}. Back to top bdeadman Senior Joined: Jan 06, 2004 Posts: 204 Location: Austin, TX Posted: Sun Mar 07, 2004 9:27 am    Post subject: Quote: This feature of PSL seems assuming a pipelined implementation One of the major differences between PSL and OVL is that the former assumes unlimited concurrency of properties while the latter generally only supported a single instance of a property. Multiple concurrency is central to the reasoning behind Formal Model checkers, and is also relatively easy to support if you build an assertion capability into the core of a simulator, but hard to achieve if you either write a Verilog FSM or generate an FSM using, for example, FoCs. It is however feasible in Verilog to support a number of concurent instances, however the coding of this is complex and you have to know at the outset the worst case number of instances you need to support. Here's an interesting puzzle. How do you write a simple, elegant property to check the number outstanding requests on a pipelined bus never exceeds some limit? Or for that matter that it is never less than the number of responses? I can figure it out if if the request and response are tagged so they can be compared, but few buses work in this way, and there's no effective notion of a counter in PSL. Regards Bernard Back to top alexg Senior Joined: Jan 07, 2004 Posts: 586 Location: Ottawa Posted: Sun Mar 07, 2004 10:46 pm    Post subject: Quote: Here's an interesting puzzle. How do you write a simple, elegant property to check the number outstanding requests on a pipelined bus never exceeds some limit? Or for that matter that it is never less than the number of responses? I can figure it out if if the request and response are tagged so they can be compared, but few buses work in this way, and there's no effective notion of a counter in PSL. Instead of thinking about stand-alone properties verification with either OVL or PSL, I would rather recommend to write transaction-based monitor for such a bus. Once this monitor is written, many properties like quoted ones will be already implemented as the key part of monitor functionality. Before writing monitor, we have to think carefully which transactions we need to extract with it. Since transaction is defined as the data structure passed from one place to another in specific simulation time, it may be represented in verilog as an event (simulation time) and set of registers (data structure). When event "fires", all transaction registers will contain valid information about transaction. For pipelined buses, we may naturally think about transactions organized in hierarchical fashion: Level 1: Indepedent request or response transaction extracted from the bus. For example, we may have such transactions to be defined: Code: event request; reg ....      rq_address; reg           rq_read_write; reg ....      rq_data; event response; reg .....     rs_status; reg           rs_read_write; reg .....     rs_data; Level 2: Request - response level 1 transaction pairs, which defines the following: - successfully completed bus transactions - error / retry / etc bus transactions Successfully completed bus transactions may be defined like this: Code: event trx_ok; reg  ...   txr_address; reg  ...   txr_data; reg        txr_read_write; This transaction states that operation was not only happened on the bus, but was successfully completed by both initiating and receiving devices. This is exactly what checker / scoreboard is looking for. Implementation ------------------ Assuming, that we already have Level 1 transactions implemented, we may think how to implement level 2 transactions for the pipelined bus. The easiest solution is to use fifo with the same depth as maximum number of outstanding transactions and built-in overflow/underflow indication events. It is preferable to build such a FIFO as parametric module with tasks such as push and pull. 1. Insantiate FIFO module for outstanding requests, for example: fifo #(depth) rq_fifo (); 2. Push request transactions into fifo: Code:   always (request)       rq_fifo.push(request_transaction) 3. Upon reception of response transaction, get corresponding request from fifo and build level 2 transactions: Code:   always (response) begin      matching_req_data = rq_fifo.pull;      build trx_ok or txr_err transactions from responce & request data and        fire either   -> trx_ok  or   -> trx_err   events    end 4. Monitor overflow/underflow errors: Code:    always (rq_fifo.overflow)   <do_something....>    always (rq_fifo.underflow)   <do_something....> 5. Create "remainders reporting" task which will be called at the end of simulation. It will check that total number of requests matches the total number of responses. In my opinion, such approach is the most effective one. It combines powerful data extraction capabilites with the checking properties in the natural way and results in the most compact and easy-to-debug code. Functional coverage (which is mostly coverage for defined transaction data) may be added easily as well. Regards, Alexander Gnusin Back to top vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1238 Location: Los Angeles, CA Posted: Sun Mar 07, 2004 11:48 pm    Post subject: I attended a DvCon session where one company used SystemC to compute expected responses, and in zero sim time, pushed those signal processing results into a FIFO. In a manner similar to what you're describing, an RTL signal throttled the reading of the FIFO for comparison of RTL signal processing results against the SystemC results. The FIFO was use to iron out synchronization issues. Is your transaction-based solution workable? Yes! However, you're missing the main purpose of property verification: to infuse the requirements / interfaces / and RTL design with concise, easy to define and read properties to both clarify intent and to verify the design through simulation and formal verification. To achieve that infusion, the mechanism (i.e., language) must be concise, yet effective. Otherwise, there is less incentive to add assertions. Note that the assertions make use of some additional RTL constructs (e.g., reg, FIFO, etc) to collect the transactions (such as de-serialize data). To you, building Verilog verification code with FSM, FIFOs, and counters is easy and readable and is really not an issue. However, this is not the general feeling of the community. Acceptance of property assertion languages like OVL, PSL and SystemVerilog Assertion (SVA) is spreading because of the benefits provided by the concise nature of the languages. OVL is fairly constrained in its library. PSL is definitely more flexible. SVA and PSL have many regions of overlaps. PSL addresses several languages ( Verilog, VHDL, GDL, and it is anticipated that it will support SystemVerilog and SystemC). SVA is closely linked to SystemVerilog, and offers some very interesting constructs, in addition to those similar to PSL. Bottom line, assertion-based verification is now the new “buzz” word, very much like “reuse” was the word a few years back. ABV is a methodology, irrelevant of the language. Thus, if you implement ABV with Verilog, VHDL, OVL, PSL, GDL, SVA, SUGAR, VERA, etc.. more power to you, and you’re definitely adopting the new paradigm in verification. There are other paradigms, like constrained random testing (with functional coverage), and formal verification. What’s we discussing is choice of language for ABV. My preferences are, whenever possible, the languages that are concise, easy to read, and expressive because they are easier to use, and engineers would write assertions. If the task of writing assertions is difficult, those assertions would be delayed (or never written). Point-in-case: how many engineers really write meaningful comments? With assertion languages, one could write assertions instead of comments. Of course assertions are executable. _________________ 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: Mon Mar 08, 2004 9:22 am    Post subject: Quote: I would rather recommend to write transaction-based monitor for such a bus. Once this monitor is written, many properties like quoted ones will be already implemented as the key part of monitor functionality Alexander, I agree this is one approach, and one that I personally support because our company produces tools that generate monitors automatically from formal protocol descriptions. You can find background to this in a tutorial I co-presented at DVCon last year (2003). This is available at www.sdvinc.com/PSL-Sugar_tutorial_pt5.pdf . It is not, incidentally, the SystemC presentation Ben mentions, though all the master, slave, and monitor code we generate does inherently perform "overflow" and "underflow" checks as you describe. On a more general note, the compactness of PSL properties is very attractive, however there are some tasks for which I find it difficult to write properties as I highlighted yesterday. It seems there is no way to sample in the middle of a stream of transactions and figure out the pipeline status, therefore overflow and underflow conditions require counting from the last reset. If the language supported it, I could imagine properties like: req && !response -> increment_counter; !req && response -> decrement_counter; assert never { ((counter > MAX_PIPELINE_LENGTH) || (counter<0)) } ; Another area I find difficult is checksum & CRC calculation. At first sight I would have expected them to be easy because they are both performed over long sequences, which is were regular expressions excel, however.... Does anyone see simple solutions to expressing these requirements in PSL? Regards Bernard Back to top vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1238 Location: Los Angeles, CA Posted: Mon Mar 08, 2004 5:09 pm    Post subject: Quote: On a more general note, the compactness of PSL properties is very attractive, however there are some tasks for which I find it difficult to write properties as I highlighted yesterday. It seems there is no way to sample in the middle of a stream of transactions and figure out the pipeline status, therefore overflow and underflow conditions require counting from the last reset. I As you know the language supports the modeling layer, which represents all the synthesizable constructs allowed in the HDL of interest. The modeling layer applies to the vunit. For modules, all of VHDL or Verilog constructs are allowed (part of the module). Thus typically, one would add enough HDL constructs to support PSL. For example, serial data can be stored into a register or a FIFO for later comparison of the received value against the transmitted value. Quote: If the language supported it, I could imagine properties like: req && !response -> increment_counter; !req && response -> decrement_counter; assert never { ((counter > MAX_PIPELINE_LENGTH) || (counter<0)) } ; What you're addressing is the action-block feature available in SVA. PSL 1.1 does not support the action-block, basically an action (task, function call, etc) when the property passes or fails. PSL 1.1 clarifies several issues, and provides something close, but not identical to the action block. The idea is to use endpoints (Boolean that identifies the end of a sequence). Code can then test the value of tht endpoint and take an action. Below is an application example: Code: sequence transaction_q = {breq[*]; back; [*1:3]; drdy; !breq; !back};     endpoint transaction_e = {transaction_q};     cover transaction_q;     always @ (posedge clk)          if (transaction_e)  top.sig <= 1’b1 else                                     top.sig <= 1’b0; Thus, in your example, a set of endpoints can detect the end of the sequences "req && ! response" and "!req && response" (sequences can be more complex than the Boolean above). Based on the value of the endpoints, the counters can be modified. Of course, one can always do that in HDL., by addition logic to detect the triggering condition. Quote: Another area I find difficult is checksum & CRC calculation. At first sight I would have expected them to be easy because they are both performed over long sequences, which is were regular expressions excel, however.... PSL is not an HDL. Those functions need to be defined at the modeling layer or in the HDL. The results of those caluculations can however be used in PSL. _________________ 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 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 Previous  1, 2, 3  Next Page 2 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: 2.036 Seconds