SVA:is it possible to use input as index of an array in prop

S

samuel

Guest
Hi,

I have an 255 bit inputs , and also a 8bit control input signal to
choose one from the 255 input and drive to the one bit output port.

I want to check if the connections are correct with assertion. The
best(lazy) way is to use the 8bit control input as the index in the
property as below :

module check_assertion(
input clk,
input port_a_tpa_pad,
input port_ae_tpa_pad,

//source
input [1:255] port_a_source,

//tpa slec
input [0:7] tpa_select,

);

integer port_index ;


always @(tpa_select) begin
$cast(port_index,tpa_select);
end

a_tpa: assert property (@(posedge clk) (port_ae_tpa) |-
));
Click to expand...
);

endmodule

However, I got an error message from ncvlog :
ncvlog: *E,NULLLP (aaa.v,64|0): empty/illegal list of ports
[12.3.4(IEEE-2001)].

Does anyone know other possible way to handle this ?
 
On Thu, 22 May 2008 02:51:31 -0700 (PDT), samuel
<samuelzhng@gmail.com> wrote:

Hi,

I have an 255 bit inputs , and also a 8bit control input signal to
choose one from the 255 input and drive to the one bit output port.

I want to check if the connections are correct with assertion. The
best(lazy) way is to use the 8bit control input as the index in the
property as below :

module check_assertion(
input clk,
input port_a_tpa_pad,
input port_ae_tpa_pad,
//source
input [1:255] port_a_source,
//tpa slec
input [0:7] tpa_select, // Spurious comma here - JB
);

integer port_index ;

always @(tpa_select) begin
$cast(port_index,tpa_select);
end

a_tpa: assert property (
@(posedge clk)
(port_ae_tpa) |-
(
(ipp_do_tpa == ipp_do_source[port_index] )
); // I think this semicolon is spurious - JB
);

endmodule

However, I got an error message from ncvlog :
ncvlog: *E,NULLLP (aaa.v,64|0): empty/illegal list of ports
[12.3.4(IEEE-2001)].

Does anyone know other possible way to handle this ?
Click to expand...
Fix the silly syntax errors :) Your port list ends with
a comma, which is illegal.

Other stuff to fix:
- There's no need for the $cast. You can use tpa_select
directly as the subscript.
- Your assertion seems to have a spurious semicolon in it.
In the quote above, I've laid it out to try to clarify
the nesting of parentheses.
- Your signal names are all over the place. I don't see
any declaration of "ipp_do_source", for example. This may
be just an artefact of your cut'n'paste to the post, I suppose.

Basically your assertion looks fine to me. It may cause some
trouble in formal tools, since the selector can take the value
zero but you don't have an element zero in your input array.
Perhaps you need a second assertion checking that the
selector never goes to zero.
--
Jonathan Bromley, Consultant

DOULOS - Developing Design Know-how
VHDL * Verilog * SystemC * e * Perl * Tcl/Tk * Project Services

Doulos Ltd., 22 Market Place, Ringwood, BH24 1AW, UK
jonathan.bromley@MYCOMPANY.com
http://www.MYCOMPANY.com

The contents of this message may contain personal views which
are not the views of Doulos Ltd., unless specifically stated.
 
On 5ÔÂ22ČŐ, ĎÂÎç6Ęą04ˇÖ, Jonathan Bromley <jonathan.brom...@MYCOMPANY.com>
wrote:
On Thu, 22 May 2008 02:51:31 -0700 (PDT), samuel



samuelz...@gmail.com> wrote:

Hi,

I have an 255 bit inputs , and also a 8bit control input signal to
choose one from the 255 input and drive to the one bit output port.

I want to check if the connections are correct with assertion. The
best(lazy) way is to use the 8bit control input as the index in the
property as below :

module check_assertion(
input clk,
input port_a_tpa_pad,
input port_ae_tpa_pad,
//source
input [1:255] port_a_source,
//tpa slec
input [0:7] tpa_select, // Spurious comma here - JB
);

integer port_index ;

always @(tpa_select) begin
$cast(port_index,tpa_select);
end

a_tpa: assert property (
@(posedge clk)
(port_ae_tpa) |-
(
(ipp_do_tpa == ipp_do_source[port_index] )
); // I think this semicolon is spurious - JB
);

endmodule

However, I got an error message from ncvlog :
ncvlog: *E,NULLLP (aaa.v,64|0): empty/illegal list of ports
[12.3.4(IEEE-2001)].

Does anyone know other possible way to handle this ?

Fix the silly syntax errors :) Your port list ends with
a comma, which is illegal.

Other stuff to fix:
- There's no need for the $cast. You can use tpa_select
directly as the subscript.
- Your assertion seems to have a spurious semicolon in it.
In the quote above, I've laid it out to try to clarify
the nesting of parentheses.
- Your signal names are all over the place. I don't see
any declaration of "ipp_do_source", for example. This may
be just an artefact of your cut'n'paste to the post, I suppose.

Basically your assertion looks fine to me. It may cause some
trouble in formal tools, since the selector can take the value
zero but you don't have an element zero in your input array.
Perhaps you need a second assertion checking that the
selector never goes to zero.
--
Jonathan Bromley, Consultant

DOULOS - Developing Design Know-how
VHDL * Verilog * SystemC * e * Perl * Tcl/Tk * Project Services

Doulos Ltd., 22 Market Place, Ringwood, BH24 1AW, UK
jonathan.brom...@MYCOMPANY.comhttp://www.MYCOMPANY.com

The contents of this message may contain personal views which
are not the views of Doulos Ltd., unless specifically stated.
Click to expand...
Thanks Jonathan,

After removing the $cast part and without other sily syntax issues:
(,now the code ncvlog saw is as below :

module tpa_check_assertion(
input clk,
input ipp_do_tpa_pad,
input ipp_obe_tpa_pad,

//source
input [1:255] ipp_do_source,

//tpa slec
input [0:7] tpa_select,

);

a_tpa: assert property (@(posedge clk)
(ipp_obe_tpa_pad) |-> ( (ipp_do_tpa_pad =ipp_do_source[tpa_select] )));

endmodule


However, unfortunately I still can't get ncvlog parse it successfully:
ncvlog: *E,NULLLP (sva/asserts.v,64|0): empty/illegal list of ports
[12.3.4(IEEE-2001)].

Do you know or does anyone know anything might be wrong ?

Regarding the element zero issue, the design the assertion bound to
probably will ensure no zero generated to tpa_select, otherwise , a
design issue will be found.

I am trying to use decode tpa_select to 255 assertions
seperately ,which probably can work, but not so nice :( ....

Best regards,

Samuel
 
On 5ÔÂ22ČŐ, ĎÂÎç6Ęą04ˇÖ, Jonathan Bromley <jonathan.brom...@MYCOMPANY.com>
wrote:
On Thu, 22 May 2008 02:51:31 -0700 (PDT), samuel



samuelz...@gmail.com> wrote:

Hi,

I have an 255 bit inputs , and also a 8bit control input signal to
choose one from the 255 input and drive to the one bit output port.

I want to check if the connections are correct with assertion. The
best(lazy) way is to use the 8bit control input as the index in the
property as below :

module check_assertion(
input clk,
input port_a_tpa_pad,
input port_ae_tpa_pad,
//source
input [1:255] port_a_source,
//tpa slec
input [0:7] tpa_select, // Spurious comma here - JB
);

integer port_index ;

always @(tpa_select) begin
$cast(port_index,tpa_select);
end

a_tpa: assert property (
@(posedge clk)
(port_ae_tpa) |-
(
(ipp_do_tpa == ipp_do_source[port_index] )
); // I think this semicolon is spurious - JB
);

endmodule

However, I got an error message from ncvlog :
ncvlog: *E,NULLLP (aaa.v,64|0): empty/illegal list of ports
[12.3.4(IEEE-2001)].

Does anyone know other possible way to handle this ?

Fix the silly syntax errors :) Your port list ends with
a comma, which is illegal.

Other stuff to fix:
- There's no need for the $cast. You can use tpa_select
directly as the subscript.
- Your assertion seems to have a spurious semicolon in it.
In the quote above, I've laid it out to try to clarify
the nesting of parentheses.
- Your signal names are all over the place. I don't see
any declaration of "ipp_do_source", for example. This may
be just an artefact of your cut'n'paste to the post, I suppose.

Basically your assertion looks fine to me. It may cause some
trouble in formal tools, since the selector can take the value
zero but you don't have an element zero in your input array.
Perhaps you need a second assertion checking that the
selector never goes to zero.
--
Jonathan Bromley, Consultant

DOULOS - Developing Design Know-how
VHDL * Verilog * SystemC * e * Perl * Tcl/Tk * Project Services

Doulos Ltd., 22 Market Place, Ringwood, BH24 1AW, UK
jonathan.brom...@MYCOMPANY.comhttp://www.MYCOMPANY.com

The contents of this message may contain personal views which
are not the views of Doulos Ltd., unless specifically stated.
Click to expand...
Thanks Jonathan,

You are right. I was just mislead by those silly syntax mistakes ....

Regarding the element zero issue, the design the assertion bound to
probably will ensure no zero generated to tpa_select, otherwise , a
design issue will be found.

Best regards,

Samuel
 
You must log in or register to reply here.

Welcome to EDABoard.com

Sponsor

Back
Top