I am trying to verify a design written in VHDL using SystemVerilog's assertions.
I have a problem when I have a non-defined signal'X.'
Just for example here is the code of a comparator:
entity FP_comparator_V2 is
port (
comp_in1 : in std_logic_vector(31 downto 0);
comp_in2 : in std_logic_vector(31 downto 0);
less : out std_logic;
equal : out std_logic;
greater : out std_logic
);
end FP_comparator_V2;
architecture behav of FP_comparator_V2 is
-- signal, component etc. declarations
begin
-- architecture body
process(comp_in1, comp_in2)
begin
if comp_in1 = comp_in2 then
equal <= '1';
less <= '0';
greater <= '0';
else
equal <= '0';
...
end if;
end process;
end behav;
and the assertions
property FP_Comparator_V2_1_1;
@(posedge `assertion_check_clk29M4912 or negedge `assertion_check_clk29M4912)
(fp_comp_intf.Comp_in1 === fp_comp_intf.Comp_in2) |-> (fp_comp_intf.equal);
endproperty
DS_3_4_69_1_1:
assert property(FP_Comparator_V2_1_1);
cover property(FP_Comparator_V2_1_1);
property FP_Comparator_V2_1_2;
@(posedge `assertion_check_clk29M4912 or negedge `assertion_check_clk29M4912)
(fp_comp_intf.Comp_in1 !== fp_comp_intf.Comp_in2) |-> (!fp_comp_intf.equal);
endproperty
DS_3_4_69_1_2:
assert property(FP_Comparator_V2_1_2);
cover property(FP_Comparator_V2_1_2);
When Comp_int1 and Comp_int2 have defined values the simulation works fine.
If one of them have an undefined value also works fine.
When both signals have an undefined value it gives an error.
For example:
Comp_int1= 48xx_xxxx; Comp_int2=47xx_xxxx ==>Equal = 1
I suppose it compares bit by bit so Equal should be '0.' Please if you know a book or a website explaining the behavior of signals after synthesis or the logic behind undefined signals I would be thankful if you put it in a comment.