Re: Proposal for Group O (Issue 44), SystemC Flavor of PSL - second detailed draft

Hi Erich,

Regarding the following change in your proposal:
"1. Changed RANGE_SYM to ':' rather than ',' to avoid problems with forall
Value_Sets that use commas."

I think I understand the problem: if we leave ',' as the range_sym then in
an expression such as "forall i in {2,4}" we would not know whether the
value set was {2,4} or {2,3,4}.

However, it seems a pity that SystemC users will not be able to write the
ranges in their native syntax.
Could this be solved by requiring parenthesis around the range, e.g.,
"forall i in {(2,4)}" ?

If the Verilog range syntax is used, then the last sentence of this section
needs to be changed:
"4.1.2.4 SystemC flavor
  In this flavor, all expressions of the Boolean layer, as well as modeling
layer code, are written
  in SystemC syntax (see OSCI Std SystemC). The SystemC flavor also has
limited influence on
  the syntax of the temporal layer. For example, ranges of the temporal
layer are specified using
  the SystemC-style syntax i,j. "

Regards,
Avigail
_______________________________________________________
Avigail Orni
Verification and Testing Solutions Group
IBM Haifa Research Laboratory
Phone: 972-4-829-6396 email: ornia@il.ibm.com

owner-ieee-1850-extensions@eda.org wrote on 01/02/2005 03:11:21:

>
> Following is the second detailed draft of the changes required for a
> SystemC flavor. Two points remain to be resolved; these are marked
> with *****. One other possible issue is similarly marked.
>
> Proposal for Group O (Issue 44), SystemC Flavor of PSL
> ===========================================
>
> Changes in the second draft
> ======================
> 1. Changed RANGE_SYM to ':' rather than ',' to avoid problems with
> forall Value_Sets that use commas.
> 2. Changed LEFT_SYM, RIGHT_SYM to '[', ']' to be consistent with
> (System)Verilog (since we are using (S)V ':' for ranges)
> 3. Detailed the additions to the definitions of True and False.
> 4. Detailed the additions to define the SystemC modeling layer.
> 5. Corrected the SystemC entry for flavor macro HDL_EXPR (to
> *conditional*_expression)
> 6. Corrected the SystemC entry for flavor macro HDL_CLOCK_EXPR and
> added a semantic restriction
> 7. Removed questions about SystemC entries for flavor macros
> HDL_DECL and HDL_STMT
> 8. Corrected the statement about interpretation of -> in the SystemC
flavor
>
> Detailed Changes
> ==============
> 31 Jan 2005
>
> Section 2 - References
>
> Add a reference to the OSCI SystemC standard, and perhaps also one
> to IEEE 1666 SystemC (which is currently under development). ******
>
> Section 3 - Definitions
>
> 3.1.20 False - add the following sentence, after the sentence about
> VHDL, and before the sentence about GDL:
> "In the SystemC flavor, the value 'false' of type bool is
> interpreted as the logical value /False/."
>
> 3.1.51 True - add the following sentence, after the sentence about
> VHDL, and before the sentence about GDL:
> "In the SystemC flavor, the value 'true' of type bool is
> interpreted as the logical value /True/."
>
> 4.1, Abstract Structure; first paragraph - change "four flavors" to
> "five flavors"
>
> 4.1.2 Flavors; first paragraph
> - change "four /flavors/" to "five /flavors/"
> - add SystemC to the list of HDLs, after VHDL
>
> 4.1.2.4 GDL flavor - just before this, insert
>
> 4.1.2.4 SystemC flavor
> In this flavor, all expressions of the Boolean layer, as well as
> modeling layer code, are written
> in SystemC syntax (see OSCI Std SystemC). The SystemC flavor also
> has limited influence on
> the syntax of the temporal layer. For example, ranges of the
> temporal layer are specified using
> the SystemC-style syntax i,j.
>
> 4.2.1 Identifiers - second paragraph
> - change "SystemVerilog and Verilog" to "SystemVerilog, Verilog,
> and SystemC"
>
> 4.3.2.1 HDL_UNIT - after the VHDL entry, add alternative
> / SystemC: /SystemC_class/_sc_module
>
> 4.3.2.2 HDL_MOD_NAME - after the VHDL entry, add alternative
> / SystemC: /SystemC_class/_sc_module_name
>
> 4.3.2.3 HDL_DECL and HDL_STMT
> - in the definition of HDL_DECL, after the VHDL entry, add alternative
> / SystemC: /SystemC/_declaration
>
> - in the definition of HDL_STMT, after the VHDL entry, add alternative
> / SystemC: /SystemC/_statement
>
> 4.3.2.4 HDL_EXPR
> - change the title to HDL_EXPR and HDL_CLOCK_EXPR (to fix an
> oversight in the PSL v1.1 LRM)
> - change the first paragraph to read
>
> "Expressions shall be valid expressions in the underlying HDL
> description. This
> applies to expressions appearing directly within a temporal
> layer property,
> including those that appear within clock expressions, as well
> as to any sub-expressions
> of those expressions. The definitions of HDL_EXPR and
> HDL_CLOCK_EXPR capture
> this requirement, as shown in Box 5."
>
> - after the VHDL entry, add alternative
> / SystemC: /C++/_Conditional_Expression
>
> - add the following to Box 5
>
> Flavor Macro HDL_CLK_EXPR =
> SystemVerilog: /SystemVerilog/_Event_Expression
> / Verilog: /Verilog/_Event_Expression
> / VHDL: /VHDL/_Expression
> / SystemC: /SystemC/_Conditional_Expression
> / GDL: /GDL/_Expression
>
> - add the following paragraph after Box 5:
> "In the SystemC flavor, a SystemC conditional expression used
> as a clock expression must be of one of the following types:
> sc_event, sc_event *, sc_event_finder, sc_event_finder *,
> sc_event_and_list, sc_event_and_list *, sc_event_or_list,
> sc_event_or_list *, sc_signal, or sc_port."
>
> 4.3.2.5 HDL_RANGE - no change (not applicable to SystemC)
>
> 4.3.2.6 AND_OP, OR_OP, and NOT_OP
> - in the definition of AND_OP, after the VHDL entry, add alternative
> / SystemC: '&&'
>
> - in the definition of OR_OP, after the VHDL entry, add alternative
> / SystemC: '||'
>
> - in the definition of NOT_OP, after the VHDL entry, add alternative
> / SystemC: '!'
>
> 4.3.2.7 RANGE_SYM, MIN_VAL, MAX_VAL
> - in the definition of RANGE_SYM, after the VHDL entry, add alternative
> / SystemC: ':'
>
> - in the definition of MIN_VAL, after the VHDL entry, add alternative
> / SystemC: '0'
>
> - in the definition of MAX_VAL, after the VHDL entry, add alternative
> / SystemC: 'inf'
>
> 4.3.2.8 LEFT_SYM and RIGHT_SYM
> - in the definition of LEFT_SYM, after the VHDL entry, add alternative
> / SystemC: '['
>
> - in the definition of RIGHT_SYM, after the VHDL entry, add alternative
> / SystemC: ']'
>
> 4.3.2.9 DEF_SYM - after the VHDL entry, add alternative
> / SystemC: '='
>
> 5.1.1 Bit expressions - add the following statement as a new
> paragraph after the VHDL statement:
>
> "In SystemC, types sc_bit and sc_logic are Bit types."
>
> 5.1.2 Boolean expressions
> - add the following statement as a new paragraph after the VHDL
statement:
> "In SystemC, type bool is a Boolean type."
>
> - in the paragraph starting "Any Bit type is interpretable as a
> Boolean type", in the second sentence, change both occurrences of
> "Verilog and SystemVerilog" to "Verilog, SystemVerilog, and SystemC".
>
> - in the paragraph starting "The return value from a PSL
> expressions ...", change the last sentence to read
> "For Verilog, the return value is of the built-in logic type;
> for SystemVerilog,
> the return value is of the built-in type logic; for VHDL, the
> return value is of
> type /STD.Standard.Boolean/; for SystemC, the return value is
> of type bool."
>
> (Note the correction of ',' => ';' before "for VHDL", as well
> as the addition of the clause for SystemC.)
>
> 5.1.3 BitVector expressions
> - add the following statement as a new paragraph after the VHDL
statement:
> "In SystemC, each of the types sc_bv, sc_lv, sc_int, sc_uint,
> sc_bigint, and
> sc_biguint is interpretable as a BitVector type."
>
> - delete the paragraph starting "The return value from a PSL
> built-in function ...", because there are no built-in functions that
> return BitVector values (except for those that return AnyType
> values, which is more general, and there are already rules
> explaining that such functions return the same type as the input type).
>
> 5.1.4 Numeric expressions
> - in the first paragraph after Box 15 ("In Verilog, any BitVector
> expression ..."), add the following final sentence:
> "In SystemC, any expression of type bool, char, short, int,
> long, or long long,
> or of types sc_bit, sc_logic, sc_int, sc_uint, sc_bigint, or
> sc_biguint, is interpretable
> as a Numeric expression."
>
> <what is the SystemCreturn type of a built-in function that returns
> a Numeric type (e.g., countones)?> ******
>
> 5.1.5 String expressions
> - in the first paragraph after Box 16, add the following sentence
> after the sentence about VHDL:
> "In SystemC, any expression of type std::string or char * is a
> String expression."
>
> 5.2.1 HDL expressions
> - update Box 18 to reflect the change to HDL_EXPR in 4.3.2.4
> - in the paragraph starting "For each operator symbol in the HDL
> expression, ..." in the first bullet, add "SystemC" after Verilog
> and before GDL.
>
> 5.2.2 PSL expressions
> - under Informal Semantics, in the second paragraph, change
> "Verilog or SystemVerilog" to "Verilog, SystemVerilog, or SystemC".
>
> 5.3 Clock expressions
> - update Box 22 to reflect the changes to HDL_CLOCK_EXPR in 4.3.2.4
> - add the following new paragraph after the paragraph starting "In
> the VHDL flavor, ..."
>
> "In the SystemC flavor, any expression that SystemC allows to be
> used as the condition in an if statement can be used as a clock
> expression. In addition, any SystemC event expression can be used as
> a clock expression. Such a clock expression is considered to hold in
> a given cycle /iff/ it generates an event in that cycle."
>
> 6.2.1.7.1 Logical implication
> - under Restrictions, add a new paragraph that reads:
>
> "In the SystemC flavor, if the operator '->' appears in an
> expression and it's left operand is the name of a pointer to an
> object that has a member whose name is the right operand, then the
> '->' operator is interpreted as the SystemC member operator, not as
> the logical implication operator."
>
> 8. Modeling layer
> - in the first paragraph, change the last sentence to include
> SystemC after VHDL.
>
> - add the following paragraph after the paragraph for VHDL:
>
> The SystemC flavor of the modeling layer consists of SystemC
> declarations that are allowed in the context of a SystemC module,
> and SystemC statements that are allowed in the constructor of a
> SystemC module.
>
> *****
> We may want to disallow use of modeling layer statements in vunits
> that are bound to SystemC instances, due to the difficulty of
> incrementally adding statements to instances of a class in SystemC.
> This may indicate also that we need to think carefully about what is
> allowed in the SystemVerilog modeling layer, for similar reasons.
> *****
>
> A.3 HDL dependencies
> - after the paragraph for VHDL (starting "For VHDL, ..."), add the
> following new paragraph:
>
> "For SystemC, the PSL syntax refers to the following
> nonterminals of the OSCI SystemC syntax:
>
> - expression
> - sc_module
> - sc_module_name
> - declaration
> - statement
>
> [The reference above may be able to change to IEEE 1666 SystemC, if
> there is at least a draft IEEE SystemC LRM available to reference by
> the time we go to ballot.]
>
> A.3.2 Flavor macros
>
> Reflect the changes mentioned above, in 4.3.2.*, in this section
>
>
> ====================================================================
>
> Original Sketch
> ============
> 28 Dec 2004
>
> The following proposal presents a sketch of the definition of a
> SystemC flavor of PSL.
>
> 1. Flavor macros
>
> The flavor macros would be extended with the following definitions,
> which follow the Verilog flavor for the most part, but also include
> references to a C++ nonterminal (constant_expression) and to SystemC
> class names:
>
> DEF_SYM: '='
> RANGE_SYM: ','
> AND_OP: '&&'
> OR_OP: '||'
> NOT_OP: '!'
> MIN_VAL: '0'
> MAX_VAL: 'inf'
> HDL_EXPR: /C++/_constant_expression
> HDL_CLK_EXPR: SystemC_Event_Expr
> HDL_UNIT: /SystemC_class/_sc_module
> HDL_MOD_NAME: /SystemC_class/_sc_module_name
> HDL_DECL: /SystemC/_declaration (needs further definition)
> HDL_STMT: /SystemC/_statement (needs further definition)
> HDL_RANGE: N/A
> LEFT_SYM: '('
> RIGHT_SYM: ')'
>
> SystemC_Event_Expr would include the following:
> sc_event, sc_event *,
> sc_event_finder, sc_event_finder *,
> sc_event_and_list, sc_event_and_list *,
> sc_event_or_list, sc_event_or_list *,
> sc_signal, sc_port
>
> 2. Data types
>
> In the SystemC flavor, PSL type classes Bit, Boolean, BitVector,
> Numeric, and String would include the set of SystemC types shown in each
case:
>
> Bit:
> bool,
> sc_bit,
> sc_logic
>
> Boolean:
> built in data types:
> bool,
> char,
> unsigned char,
> signed char,
> short,
> unsigned short,
> int,
> unsigned int,
> long,
> unsigned long,
> long long,
> unsigned long long
> SystemC data types:
> sc_bit,
> sc_int,
> sc_uint,
> sc_bigint,
> sc_biguint
> sc_logic
>
> BitVector:
> sc_bv,
> sc_lv,
> sc_int,
> sc_uint,
> sc_bigint,
> sc_biguint
>
> Note that in SystemC, sc_bv and sc_lv do not have an implicit
> conversion to bool, which means that they can't be interpreted as
> true or false.
>
> Numeric:
> Same as Boolean
>
> 3. Event expression forms that can be used as clock expressions:
>
> HDL_CLK_EXPR (above)
> rose, fell (where the argument is a port or signal of bool or sc_logic)
>
> 4. SystemC types returned by endpoints and built-in functions:
>
> bool (with the exception of prev()).
>
>
> Possible Issues
> ============
>
> There is a grammar conflict between PSL and C++. The following
> PSL/SystemC boolean expression is ambiguous:
>
> a -> b
>
> It could mean either "a implies b" or "member b of object pointed to
> by a". This conflict can only arise if someone writes a boolean
> expression using a pointer to a data structure that contains a
> member with the same name as another identifier in scope. In such a
> case, the "HDL" interpretation (member reference) should take
> precedence over the PSL interpretation (implication) to resolve the
> conflict. The user can rename their variables to avoid the conflict
> if it ever arises.
>
> ==================================================================
>
>
>
Received on Tue Feb 1 07:18:14 2005