Questa formal tool giving error for SVA sequences with ports

SystemVerilog
, ,
1

I added following sequence in my tb module

// sequence send byte
sequence seq_send_byte (input logic s_data, input logic [7:0] data_to_send);
s_data == data_to_send[0] ##1
s_data == data_to_send[1] ##1
s_data == data_to_send[2] ##1
s_data == data_to_send[3] ##1
s_data == data_to_send[4] ##1
s_data == data_to_send[5] ##1
s_data == data_to_send[6] ##1
s_data == data_to_send[7] ;
endsequence

using Questa formal version 10.3d_3

Getting following error
Error near “input”: syntax error, unexpected input, expecting ‘)’

can someone help !
Thank you

2

In reply to hemum_p:
Note that in this forum we do NOT address specific tools, but rather the language and its application. Thus, my response is targeted to the language and style.
from 1800,
sequence_declaration ::=
sequence sequence_identifier [ ( [ sequence_port_list ] ) ] ;
sequence_port_list ::=
sequence_port_item {, sequence_port_item}
sequence_port_item ::=
{ attribute_instance } [ local [ sequence_lvar_port_direction ] ] sequence_formal_type
formal_port_identifier {variable_dimension} [ = sequence_actual_arg ]
sequence_lvar_port_direction ::= input | inout | output

16.8.2 Local variable formal arguments in sequence declarations

A formal argument of a named sequence may be designated as a local variable argument by specifying the keyword local in the port item, followed optionally by one of the directions input, inout, or output. If no direction is specified explicitly, then the direction input shall be inferred.

Thus, to use use the direction input, you also need local. The following compiles OK in the compiler I have:


sequence seq_send_byte (local logic s_data, local input logic [7:0] data_to_send);
...
endsequence 
// But do you want the argument to be local? 
// can this work for you? 
sequence seq_send_byte (logic s_data, logic [7:0] data_to_send);
  s_data == data_to_send[0] ##1 
  s_data == data_to_send[1] ##1 
  s_data == data_to_send[2] ##1 
  s_data == data_to_send[3] ##1 
  s_data == data_to_send[4] ##1
  s_data == data_to_send[5] ##1 
  s_data == data_to_send[6] ##1 
  s_data == data_to_send[7] ;
endsequence
// A more compact and generic approach to write the above is: 
sequence seq_send_byte2 (logic s_data, logic [7:0] data_to_send);
	int v=0;
	(s_data == data_to_send[v], v=v+1'b1)[*8] ;
endsequence

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

  • SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
  • A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
  • Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
  • Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
  • Component Design by Example ", 2001 ISBN 0-9705394-0-1
  • VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
  • VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115