5
\$\begingroup\$

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.

\$\endgroup\$
2

3 Answers 3

1
\$\begingroup\$

Your comparator should be able to answer whether x"47XXXXXX" is less, greater or equal to x"48XXXXXX", because the answer does not depend on one of the undefined bits (if you assume that the bit vectors represent binary numbers, which seems to be implied in the question, otherwise the notion of "greater" and "less" becomes meaningless.

If this code also fails for x"47000000" and x"48000000", then there is a bug in the evaluation of the "leading" digits, if that testcase succeeds, then there is a bug in the order of operations, because your code looks at bits that are irrelevant for the output.

It is often the best thing to pass through undefined values through combinatorial blocks, to allow tracing in simulation, i.e. for x"4X000000" and x"4Xffffff" I'd expect your three outputs to go to 'X'. Explicitly comparing inputs against 'X' works in simulation, but cannot be replicated in synthesis.

\$\endgroup\$
0
\$\begingroup\$

I think, initial value of comp_in1 and comp_in2 signals must be defined.

Ex:

...
comp_in1                    : in    std_logic_vector(31 downto 0):= (OTHERS => '0');
...
\$\endgroup\$
1
  • \$\begingroup\$ ıt is not up to me to change anything in the design even a simple definition of the signals. \$\endgroup\$
    – mariam
    Commented Dec 13, 2018 at 7:01
0
\$\begingroup\$

You are using the case-equality comparisons in the antecedents of your assertions. If both inputs are 'bx then they will compare "equal".

Typically, having metavalues in your design is a problem in itself, so you should add assertions to check for that.

\$\endgroup\$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.