SVA for VHDL state machine

[Verictor]

Hi,

I have a VHDL file in which a state machine is built. The states are
coded in enum form. Now an SVA checker is intended to check the state
machine. The SVA checker will be locating in another file so that a
"bind" is needed. Now there is a question on how VHDL enum form is
interpreted in SVA.

Here is a pseudo example to show the question:

In VHDL:
-- definition
architecture BEHV of foo is
type STATE_TYPE is (S1, S2, S3, S4); -- say we have only 4 states
signal current_state, next_state: STATE_TYPE;
-- the rest ignore

In SVA:
module SVA_rule (clk, state)
input clk;
input state; // THE PROBLEM HERE, how wide is state: is state 2-
bit or 4-bit or whatever?
....
endmodule

At top level testbench:

bind foo SV_rule foo_SV_rule(.clk(clk), .state(state), .*); // SVA
checks are not correct AS STATE WIDTH IS UNKNOWN

Anyone has encountered this kind of question? I wonder if an enum type
is defined in SVA, how does that get mapped into the VHDL definition.

Thanks

 

[Jonathan Bromley]

On Thu, 7 Oct 2010 16:02:49 -0700 (PDT), Verictor wrote:

I wonder if an enum type
is defined in SVA, how does that get mapped into the VHDL definition.

There is currently no formal definition of the cross-language
behaviour of SVA or any other part of SV (other than DPI/VPI
linkage to C, of course). So the correct answer to your
question is determined by your chosen simulator. It's a
case of "read the documentation", I'm afraid. Or ask your
friendly tool vendor support people.

Sorry to pass the buck, but it's definitely a tool-specific
question rather than a language question. It is quite likely
that you simply can't do it reliably. If so, I suggest you
temporarily redefine your VHDL enum as a bunch of vector
constants so that you can match the definition in SVA:

-----type MY_ENUM is (EA, EB, EC, ED);------
type MY_ENUM is std_Logic_vector(3 downto 0);
constant EA: MY_ENUM := "0001";
constant EB: MY_ENUM := "0010";
constant EC: MY_ENUM := "0100";
constant ED: MY_ENUM := "1000";

The rest of your VHDL code should probably work OK
with these changes, and it's now possible to map
to SVA easily:

typedef enum logic [3:0] {
EA=4'b0001,
EB=4'b0010,
EC=4'b0100,
ED=4'b1000
} MY_ENUM;

cheers
--
Jonathan Bromley

 

[hssig]

Hi,

from a SVA presentation concerning bind for VHDL. It seems that the
enumeration type should be defined again in SV:

-- VHDL
architecture RTL of interleaver_m0 …
type fsm_state is( idle, send_bypass, load0,send0, load1,send1,
load_bypass, wait_idle );
signal int_state : fsm_state;


-- SVA
module interleaver_binds;
…
bind interleaver_m0
interleaver_sva
interleaver_sva_inst (
..clk(clk), ..
..int_state_vec(int_state)
);


typedef enum {
idle, send_bypass,
load0, send0, load1,send1,
load_bypass, wait_idle} fsm_state;
module interleaver_sva (
input clk, in_hs, out_hs,
input [4:0] int_state_vec);
fsm_state int_state;
assign int_state = int_state_vec;
…
// Check for sync byte
property pkt_start_check;
@(posedge clk)
(int_state == idle && in_hs)
-> (sync_in_valid);
endproperty


Cheers,
hssig