SV-ACMinutes2011_03_04 < P1800

P1800 Web>SystemVerilogAssertionCommittee>SVACMeetingMinutes>SV-ACMinutes2011_03_04 (2011-03-10, ErikSeligman) (raw view)EditAttach
     Notes from the SV-AC Face-to-Face Meeting, March 3,4, 2011

     ----------------------------------------------------------

I. Present:

     Tom Thatcher, Dmitry Korchemny, Scott Little, Anupam Prabhakar

     Erik Seligman

     Gordon Vreugdenhil, Dave Rich

    Attending by Phone:

    Tapan Kapoor, Manisha Kulshrestha

II. Dmitry gave a presentation which outlined the SV-AC's wants/needs.

     The presentation covered the following topics: Some discussion

     is presented inline

    - Checker output arguments

     Needed for exporting status from a checker

    - Continuous assignments, and blocking assignments.

    - Procedural control and looping constructs within checkers

    - Functions in checkers

    Gord: Are you talking about automatic or static functions?

    - Calling tasks from checkers

     Need to limit this to $display

    - Allow calling checkers from functions

    - Would have to avoid output connections for checkers appearing

      in functions.

     - Would need to avoid static variables

     - An alternative would be to use a macro in a package.

    - Allow checker instances to appear in classes.

     - Use checkers in a way consistent with UVM

     - Gord: Classes have a defined point of creation, but no defined

        point of destruction.

     - Only the simplest checkers would work in a class.

    - Allow forcing of design variables from checkers.

     - Would allow formal verification to do pruning of design.

     - Currently done by tool command.

     - Why wouldn't you simply drive from checker output?

    - Allow interfaces as checker arguments.

    - Gord: Should be straightforward. Nothing new here.

III. Discussions of topics in Dmitry's presentation

    - Sampling:

    Dmitry had proposed a "more flexible" form of sampling.

     For some types of variables, $sampled would mean the current value.

     Gord: Don't mess with the definition of sampling. Rather, have very

     clear semantics which define what types of variables are sampled.

     To keep things concise, define the rules once and refer to them.

    - Continous Assignmnets

    Dmitry's slide had an example of how a a simulator could produce

     inconsistent results because of the different regions that different

     variables are updated. The slide said, "This should Pass"

     Gord: I disagree, this should NOT pass.

    - Deferred Assertions

     Gord: Could move the deferred assertion reporting to the postponed

           region. However, if an action block performs any signal

           assignment, the update will not occur until the next

           simulation time-step.

IV.  Scott's Presentation

    - Scott Little presented a proposal for the semantics of adding

      concurrent assignments

      - Goal: Keep checker rules consistent with the reset of

SystemVerilog.

      - i.e continuous assignments would use current values of RHS

         variables, and would update in the Reactive region.

      - Rather than sampling at checker boundary, each construct within a

        checker would have its sampling semantics

     - assertions would sample all inputs.

     - Non-blocking assignments would sample RHS variables

     - Random checker: These would be solved asynchronously

V. Gord: Language Future

    - It seems that there are two different worlds which use the language:

     - The formal world, relies on a flattened, synthesized design

     - The simulation world can't assume a flattened design.

     - How do we bridge the gap?

    - Should there be more of a split between formal verification and

      simulation?

      - Assertions as generators is a big problem.

      - Action blocks that generate data

      - Powerful constructs for formal verification may not work well in

        simulation.

    - One precedent is the synthesis sub-set.

      Many simulation constructs were dis-allowed for synthesis.

    - Perhaps we should create a formal super-set.

     Would allow powerful formal constructs, while maintaining clean

     simulation semantics.

    - But don't know if the working group would agree to this direction

      in the language.

    - Dave Rich: But synthesis subset had problems. For example the

      simulation/synthesis mismatch.

VI. More discussions

    - Continuous Assignments: Do we need them in checkers?

     - Dave: Can't we just fix let?

     - Dmitry: example:

        let a = b[15:0]; How can we reference a[5]

     - Gord: Instead, define like this:

        let a = {b[15:0]};  Now, the reference a[5] becomes legal

     - Dmitry: example:

        struct {

           bit a;

           bit b;

        } s

        Without assign, how can you set the struc elements?

     - Gord & Dave:

        typedef struct {

           bit a;

           bit b;

        } s_t;

        let s = s_t'{ . . ., . . .}

     - Assignments needed for checker outputs:

        Gord: Agree, outputs are the one compelling reason why

           continous assignments are needed.

           For a let, there is no process

        Gord: Continuous assignments updating in the Reactive region should

           be OK.

           - In simulation, assigns could only target outputs of checker.

        - Allow continuous assigns in checkers: needed for outputs.

        - Can't expect assigns to update in time for assertion in the same

          cycle.

        - Can't expect that updated values will be seen by assertions.

           i.e. Dmitry's example will still not work.

    - Checkers appearing in tasks/functions

     - Gord: In simulation - would need to limit to checkers containing

        only deferred assertions.

     - This would require the compiler to elaborate the statement.

     - Essentially the same support requires as a generate block.

     - Could different calls to the function result in different

      elaborations of the checker?

     - If the checker contains only deferred assertions, it should be OK.

     - Can't allow anything which would require function inlining.

        examples: $inferred_clk

     - Alternative idea: treat checker as a parameterized type

        example: checker check(. . ., p)

                checker ck1 = check(. . ., 1)

     - Note that in SystemVerilog, the whole universe of types is known

        after elaboration.

    - Checker argument Sampling:

     - We got to checker input argument sampling because we wanted the

        non-blocking assignments to sample their arguments.

     - Manisha: What about checker inputs that have a const cast?

        The const cast means the checker input is not sampled. it gets

        the current value.

     - Dave:    Any place where a variable triggers a process should not

        be sampled.

     - Scott: Free checker variables are never sampled.

    - Checker output arguments

     - May be assigned only from a continous assignment.

     - Should it be typed?

     - Dave: It will have to be typed.

     - Major use case supported:

        Driving result indication to other parts of the model

     - Dmitry: What about having action block drive assertion output.

     - Anupam: Currently deferred assert may only have single subroutine

        call.

     - Why is deferred assertion action block limited to single subroutine

        call?

        Text mentions "no begin-end block" -- Seems arbitrary

        Concurrent assertions don't have this restriction.

    - Forcing in checkers

     - Use cases:

        1. Substituting module with abstract model in a system.

        2. Pruning the design

    - Checkers in classes

     - Use case:

        OVM/UVM allows monitors in classes. Why couldn't these be

        implemented as checkers?

     - Note: Only expect, and immediate assertions allowed in classes

     - Dave: Note that immediate assertions are turned off by $assertoff

        and other assertion control tasks. Thus, a monitor implemented

        with assertions could also be turned off.

        - He recommended against using assertions in the monitor

           implementation.

     - No defined destruction point for a class: A checker/assertion

        could fail long after it is useful.

     - Scott: Checkers might make sense in some static classes.

     - Dave: Problem with clocking blocks: #1 sampling semantics.

    - Vacuity

     - Scott: We had discussed vacuity before.

        However, research is not mature in this area.

        We should just fix implies and leave the rest for later.

Day 2

=====

V. Discussions

    - Local Variables:  3 Mantis items open

     - 2555 is just a clarification

     - 3057 Allows first-class local variables

        - Would allow declaration within any parenthesized scope

        - Annex F would already support this

        - Manisha: Would conflicting definitions be well defined?

         (local variables with same name defined in different scopes)

     - 3195     Ben Cohen's proposal on local variable flow-out

        - Ask Ben if he wants to write the proposal.

    - AMS Assertions:

     - Scott: Details of AMS Group

        - Freescale developed realtime sequence syntax

        - They just don't know how to implement it.

        - Definition for non-overlapping implication needs work.

        - Did a realtime LTL implementation

     - Scott: Application to P1800

        - Annex F does have unclocked support

        - Published work on extending PSL for unclocked use.

        - PSL has unclocked support.

           However, nobody implements it because it would mean evaluating

           every time step.

     - Dmitry: It would be good to have a notion of stability.

        (even for regular assertions: could use it to check for glitches)

    - Dynamic data types in assertions

     - Existing use: Inside procedural code, an automatic variable can

        be considered an example of how this might work.

        The value of the variable is captured and preserved throughout

        the assertion attempt.

     - Erik:    Would similar mechanism work for dynamic data types?

     - Scott: Might not want ot capture the value right away. What abou

        a temporal assertion?

     - Erik: But the object might be destroyed before the temporal

        assertion attempt completes.

     - What's the difference between these examples?

        string s;

         always @ (posedge clk)

           if (s == "yes") . . .

        and

        string s;

        assert property ( @(posedge clk) s == "yes" );

        - One difference is sampling.

           Sampling captures the value in the Preponed region

           It doesn't refer to the original object.

     - Could we sample dynamic types?

        - If the index is not constant, we would have to sample the

           entire array.

                 e.g.  assert property ( myqueue[i] == 4 );

        - Manisha: Same problem if we use a local variable for the index.

     - Dmitry: Example

        Would like to do something like this:

        property p (x, set);

           x inside set;

        endproperty

        assert property p(y, '{1,3,7});

     - Dave: for this, you would need to declare the type of "set".

        Can't have it untyped.

     - Tom: What is the motivation for allowing dynamic types in

        assertions?

     - Scott: Would like to put assertions in test bench to catch

        test bench bugs.

    - Adding real types to assertions

     - Dave: Language in other parts of the LRM say, "The expression

        must return an integral type" Using language like this would

        easily permit the referencing of real types in assertions.

     - Dmitry: Displayed presentation slide, which proposed adding

        an "integral" type. A formal argument typed "ingegral" would

        accept any integral type, but would not accept arguments of

        sequence & property, for example.

     - Dave: But then what about real types?

     - Dave: Note that you can already type an expression like this:

           if ( type(x) == int )

     - Dave: There is already the type "packed" Any packed type can

        be interpreted as an integral type.

        Probably need to discuss this more with the SV-BC.

    - What about variables of type time

     - Problem: If you use $time direcly in an assertion, you will get

        the current value.

        If you capture $time in a variable in a process, then try to

        use that variable in an assertion, you will instead get the

        sampled value of the variable, not the current time.

     - Don't try to fix this. Variables of type time should be sampled

        just as any other variable appearing in assertions. The user

        will have to know that this is a problem. You can't capture

        time in a variable, and refer to it in an assertion and expect

        to get the correct time.

    - Global Clocking

     - Dmitry: Want to allow multiple global clocks.

     - Tom:     Doesn't this mean that global clock is now essentially the

        same as default clocking?

     - Anupam: This proposal requires that the global clock appears at

        the very top level of the model. Before, global clock could

        appear anywhere in the model, and it would affect the entire

        design.

     - Dave: Now the global clocking must be in a higher level of

        hierarchy than the call to $global_clock

     - Backward incompatibilities:

        - Modules could get different global clock than they did before

        - Modules which used to have a valid global clock might not have

           one with this proposal.

        - Assertions could get different values for future value functions

           if the effective global clock changes.

    - Assertionns and Covergroups

     - Dmitry: Proposed temporal coverage

        covergroup

           A : coverpoint a { bins a[] = {1,2}; }

           B : coverpoint b { bins b[] = {[1:3]}; }

              cover property ( trig #-# A[*2] ##1 B[*2] );

        endcovergroup

        This cover property would report coverage for sequences where

        coverpoint A matches 2 cycles in a row, and coverpoint B matches

        in the following two cycles. In addition it would create a cross

        over the different possible bins of coverpoints A and B.

     - Tom: It's not really clear from the syntax that the cover

        property is crossing the bins of A and B.

     - Dave: There is already existing syntax for transition bins.

        But the syntax only allows for transitions between one coverpoint

        bin, and another bin in that same coverpoint.

     - Dave: Maybe you need to include the cross somehow in the syntax.

     - Dave: If this type of thing is needed, you should write up a

        detailes spec of requirements, ignoring syntax.

     - Dave: One other enhancement: it might be desireable to specify

        that illegal bins in a cover point will act like an assertion,

        and fire if they are hit.
Topic revision: r1 - 2011-03-10 - 19:31:31 - ErikSeligman
P1800