Реферат: Тестирование и верификация HDL-моделей компонентов SOC

reg[7:0] d;

(!RST,d=a)

##7 (b==d);

endsequence

property f(a,b);

@(posedge CLK)

// disable iff(RST||$isunknown(a)) first(a,b);

!RST |=> first(a,b);

endproperty

odin:assert property (f(xin,xa7_in))

// $display("Very good");

else $error("The end, xin =%b,xa7_in=%b", $past(xin, 7),xa7_in);

В результате проведенной верификации дискретного косинусного преобразования в среде Questa, Mentor Graphics были найдены неточности в восьми строках исходного кода HDL-модели:

// add_sub1a <= xa7_reg + xa0_reg;//

Последующее исправление ошибок привело к появлению исправленного фрагмента кода, который показан в листинге 4.

Листинг 4.

add_sub1a <= ({xa7_reg[8],xa7_reg} + {xa0_reg[8],xa0_reg});

add_sub2a <= ({xa6_reg[8],xa6_reg} +{xa1_reg[8],xa1_reg});

add_sub3a <= ({xa5_reg[8],xa5_reg} +{xa2_reg[8],xa2_reg});

add_sub4a <= ({xa4_reg[8],xa4_reg} + {xa3_reg[8],xa3_reg});

end

else if (toggleA == 1'b0)

begin

add_sub1a <= ({xa7_reg[8],xa7_reg} - {xa0_reg[8],xa0_reg});

add_sub2a <= ({xa6_reg[8],xa6_reg} - {xa1_reg[8],xa1_reg});

add_sub3a <= ({xa5_reg[8],xa5_reg} - {xa2_reg[8],xa2_reg});

add_sub4a <= ({xa4_reg[8],xa4_reg} - {xa3_reg[8],xa3_reg});