[sv-ac] my strawpoll votes


Subject: [sv-ac] my strawpoll votes
From: John Havlicek (john.havlicek@motorola.com)
Date: Sun Nov 16 2003 - 13:44:56 PST


All:

Below are my strawpoll votes together with some comments.

Best regards,

John H.

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

[Y] 0 change formal semantics of negated boolean

        This is the proposal for semantic alignment with PSL.
        It changes the clock rewrite rule for negated booleans
        so that the negated boolean is treated the same as a
        negated sequence. I think this is important to get
        full semantic alignment with PSL. I'm not sure why it
        didn't make it on the list.

[Y] 1 assume property directive.

        We had a lot of discussion about this that didn't seem to
        affect the proposal.

        I think it is important to have a syntactic way to distinguish
        the assumptions from the obligations.

        The proposal doesn't specify how tools will decide which
        assumptions will be used to govern constrained random
        simulation. We discussed the fact that assumptions that are
        not on "free" signals should not be used to generate random
        stimulus. This is o.k. with me, since I would rather not say
        anything than to get it wrong.

        I am not entirely thrilled about the mechanism for specifying
        the distribution, but I don't have enough bandwidth to offer
        a better alternative in the 3.1a timeframe. I think that it
        is not easy to understand what overall distribution is specified
        when "dist" clauses are deep inside the assumption property.

[Y] 2 immediate assume

        I think immediate assume may be useful. Since I want to be
        able to distinguish assumptions from obligations, I support
        it in the absence of evidence that it is bad.

        I don't know if a tool can use an immediate assumption for
        generating random stimulus.

[Y] 3 assume synchronization

        I am confused about where the properties that are instantiated
        in a constraint block will be declared. Why is it not allowed
        to have anonymouse, inlined property expressions in the
        constraint block?

[Y] 4 local variable extensions

        This has been split up below.

[Y] 5 non-blocking clocked assignment

        I support both the original and the alternative. I like
        the fact that the original makes it more convenient for
        the user who needs to write simple state machines. I like
        the alternative for writing complicated state machines that
        may benefit from procedural constructs that are not allowed
        in the assertion clocking block.

[Y] 6 access to sampled values

        I support this, although I've indicated that it doesn't
        solve the error message problem. For multi-clock properties,
        you may not know which sampling clock is in force at the
        time of failure.

[Y] 7 parameter in properties

        I want us to support doing the kinds of things Joseph shows
        in the proposal. I am confused about whether 3.1 already
        supports these things through sequence and property
        arguments. Joseph says "no" because of restrictions on
        the range expressions. But if that is true, then
        how are we supposed to pass "$" as a symbolic constant
        through the arguments (number 9 below)?

        Can someone explain?

        Should we fix the LRM restrictions on range expressions?
        This might be an easier way to address the need. Since we
        don't have any types on these arguments, they should be
        able to handle parameters as well.

[?] 8 sequence passing

        This sounds like a good idea, but I don't know where the text
        of the proposal is. The proposal attached on the website is
        for the importing of assertions to modports.

[Y] 9 pass $ (infinite) through property arguments.
[Y] 10 enhance implication

        This has been split up below.

[Y] 11 recursive properties
[Y] 12 boolean property connectives

        This has been split up below.

[Y] 13 assertions in functions
[Y] 14 gated clock support
 
        I would also like to see an optional event_expression in
        $past.

[Y] 16 modports importing assertions

        I agree with Adam that we should not drop the ball with SV-BC.

[?] 17 event created from sequence/property for reactive functionality.

        I don't know where the text of this proposal is.

[?] 18 extend wait to work on sequence/property

        I don't know where the text of this proposal is.

[?] 19 embed assertions in structures.

        I don't know where the text of this proposal is.

We have discussed this, but still have not found a working solution.
[Y] Proposal for action blocks using sampled variable values.
     Proposal for error message having access to local variables.

Split up proposals:

[Y] accessing local variables
[Y] sampling local variables
[Y] clock flow
[Y] generalized implication
[Y] property conjunction
[Y] property disjunction
[Y] property if else
[Y] property instances
[Y] property negation



This archive was generated by hypermail 2b28 : Sun Nov 16 2003 - 13:45:32 PST