[sv-cc] Feedback for VPI extension (assertions)


Subject: [sv-cc] Feedback for VPI extension (assertions)
From: Bassam Tabbara (bassam@novas.com)
Date: Mon Jan 12 2004 - 09:19:14 PST


Hi Joao,
 
The following list of issues is related to draft3 of LRM with the
changes/extensions to the Assertion chapter (17). I think the easiest way is
to refer to the Annex A with the formal BNF.
 
** Can you please review these issues with Surrendra if need be, I'll be
glad to give it a once over after your changes.
 
%%%%%%
 

1) concurrent assertions (start page 26):

 

ok, my mistake (see 7 and 8 for where the fixes should go).

 

2) property spec on p. 28

 

- needs multi_clock_property_expr

 

3) Add new multi_clock_property_expr

 

4) property expr on p. 28

 

- needs another "property expr (detail)" that one is similar to sequence
expr (but more restricted)

   (now (draft3) there is property composition as well, properties do not
just necessarily reference a sequence only).

 

5) multi_clock_seq added (not just expr, there can also be a clocking_event
decl inside), this is a minor addition

 

6) p. 31, sequence expr need to add "dist" as well.

 

expression_or_dist::=

expression

| expression dist { dist_list }

LRM 133

 

7) p. 33 where "immediate assert" is used add also the following (the
assume below)

 

A.6.10 Assertion statements

procedural_assertion_item ::=

assert_property_statement

| cover_property_statement

| immediate_assert_statement

| assume_property_statement

 

8) Add "expect_property_statement" (see A.2.10 Assertion declarations) I
think also p. 33 (same as assume above)

 

A.6.4 Statements

statement_or_null ::=

statement

| { attribute_instance } ;

statement ::= [ block_identifier : ] { attribute_instance } statement_item

statement_item ::=

{ attribute_instance } blocking_assignment ;

| { attribute_instance } nonblocking_assignment ;

| { attribute_instance } procedural_continuous_assignments ;

| { attribute_instance } case_statement

| { attribute_instance } conditional_statement

| { attribute_instance } inc_or_dec_expression ;

| { attribute_instance } function_call ;

| function_call_statement

| { attribute_instance } disable_statement

| { attribute_instance } event_trigger

| { attribute_instance } loop_statement

| { attribute_instance } jump_statement

| { attribute_instance } par_block

| { attribute_instance } procedural_timing_control_statement

| { attribute_instance } seq_block

| { attribute_instance } system_task_enable task_enable_statement

| { attribute_instance } task_enable

| { attribute_instance } wait_statement

| { attribute_instance } procedural_assertion_item

| { attribute_instance } clocking_drive

| void ' ( function_call )

| randsequence

| scope_randomize

| randcase_statement

| expect ( property_spec ) [ action_block ]

| expect ( property_instance ) [ action_block ]

| expect_property_statement

LRM 66

LRM 39

LRM 41

LRM 62

LRM 63

LRM 66

LRM 73

LRM 113

LRM 136

 

%%%%%%%

--
Dr. Bassam Tabbara
Technical Manager, R&D
Novas Software, Inc.

http://www.novas.com <http://www.novas.com/> (408) 467-7893



This archive was generated by hypermail 2b28 : Mon Jan 12 2004 - 09:20:27 PST