// アサーション
// synthesis translate_off
always @ (posedge clk_ddr2) begin
if (reset_ddr2) begin
camc_addr_1d <= 0;
vgadc_addr_1d <= 0;
addr_assertion_valid <= 1'b0;
end else begin
if (ddr2_addr_we) begin
camc_addr_1d <= camc_addr;
end
if (vgadc_addr_we) begin
vgadc_addr_1d <= vgadc_addr;
end
if (ddr2_addr_we || vgadc_addr_we) begin
addr_assertion_valid <= 1'b1;
end
end
end
// Camera_Controller が有効の時にVGA_Display_Controller がライトしないことをチェックするOVLアサーション
ovl_never #(`OVL_ERROR, `OVL_ASSERT, "ERROR : Camera_Controller が有効の時にVGA_Display_Controller がライトした", `OVL_COVER_DEFAULT, `OVL_POSEDGE, `OVL_ACTIVE_HIGH, `OVL_GATE_CLOCK) camc_vga_we_assertion (clk_ddr2, reset_ddr2, 1'b1, (cs_abt==CAMC_Grant || cs_abt==VGADC_Wait) && vgadc_addr_we, fire_camc_vgac);
// 現在のCamera_Controller からのWrite Addressが以前のWrite Addressの+4かどうかをチェックするOVLアサーション
ovl_always #(`OVL_ERROR, `OVL_ASSERT, "ERROR : 以前のcamc_addr から+4されていない", `OVL_COVER_ALL, `OVL_POSEDGE, `OVL_ACTIVE_HIGH, `OVL_GATE_CLOCK) camc_addr_assertion (clk_ddr2, reset_ddr2, camc_addr>=4 && (cs_abt==CAMC_Grant || cs_abt==VGADC_Wait) && ddr2_addr_we , camc_addr_1d+4==camc_addr, fire_camc_addr);
// VGA_Display_Controller が有効の時にCamera_Controller がライトしないことをチェックするOVLアサーション
ovl_never #(`OVL_ERROR, `OVL_ASSERT, "ERROR : VGA_Display_Controller が有効の時に、camc_addr_ena, camc_data_ena が1になった", `OVL_COVER_DEFAULT, `OVL_POSEDGE, `OVL_ACTIVE_HIGH, `OVL_GATE_CLOCK) vgac_camc_we_assertion (clk_ddr2, reset_ddr2, 1'b1, (cs_abt==VGADC_Grant || cs_abt==CAMC_Wait) && (ddr2_addr_we || ddr2_addr_we), fire_vgac_camc);
// 現在のVGA_Display_Controller からのRead Addressが以前のRead Addressの+4かどうかをチェックするOVLアサーション
ovl_always #(`OVL_ERROR, `OVL_ASSERT, "ERROR : 以前のvgadc_addr から+4されていない", `OVL_COVER_ALL, `OVL_POSEDGE, `OVL_ACTIVE_HIGH, `OVL_GATE_CLOCK) vgadc_addr_assertion (clk_ddr2, reset_ddr2, vgadc_addr>=4 && (cs_abt==CAMC_Grant || cs_abt==VGADC_Wait) && ddr2_addr_we , vgadc_addr_1d+4==vgadc_addr, fire_vgac_addr);
// Camera_Controller がFIFOがフルの時に書き込んでいるか？をチェックするアサーション
ovl_never #(`OVL_ERROR, `OVL_ASSERT, "ERROR : アドレスFIFOがフルの時にCamera_Controller が書き込んだ", `OVL_COVER_DEFAULT, `OVL_POSEDGE, `OVL_ACTIVE_HIGH, `OVL_GATE_CLOCK) camc_addr_full_we_assertion (clk_ddr2, reset_ddr2, 1'b1, ddr2_addr_we && ddr2_addr_fifo_full, fire_camc_addr_overflow);
ovl_never #(`OVL_ERROR, `OVL_ASSERT, "ERROR : データFIFOがフルの時にCamera_Controller が書き込んだ", `OVL_COVER_DEFAULT, `OVL_POSEDGE, `OVL_ACTIVE_HIGH, `OVL_GATE_CLOCK) camc_data_full_we_assertion (clk_ddr2, reset_ddr2, 1'b1, ddr2_data_we && ddr2_wrdata_fifo_full, fire_camc_data_overflow);
// VGA_Display_Controller がFIFOがフルの時に書き込んでいるか？をチェックするアサーション
ovl_never #(`OVL_ERROR, `OVL_ASSERT, "ERROR : アドレスFIFOがフルの時にVGA_Display_Controller が書き込んだ", `OVL_COVER_DEFAULT, `OVL_POSEDGE, `OVL_ACTIVE_HIGH, `OVL_GATE_CLOCK) vgadc_data_full_we_assertion (clk_ddr2, reset_ddr2, 1'b1, vgadc_addr_we && ddr2_addr_fifo_full, fire_vgadc_addr_overflow);
// synthesis translate_on
// アサーション
// synthesis translate_off
always @ (posedge clk_ddr2) begin
if (reset_ddr2)
;
else begin
if (afifo_overflow) begin
$display("%m: at time %t ERROR : FIFOがフルなのにライトした",$time);
$stop;
end
end
end
always @(posedge clk_cam) begin
if (reset_cam)
;
else begin
if (afifo_underflow) begin
$display("%m: at time %t ERROR : FIFOが空なのにリードした",$time);
$stop;
end
end
end
// synthesis translate_on
// synthesis translate_off
`include "std_ovl_defines.h" // std_ovl_defines.hをインクルード
// synthesis translate_on
...............
// synthesis translate_off
wire [`OVL_FIRE_WIDTH-1:0] fire_overflow, fire_underflow; // fire用の信号を定義
// synthesis translate_on
...............
// synthesis translate_off
ovl_never #(
`OVL_ERROR, // severity_level
`OVL_ASSERT, // property_type
"ERROR : FIFOがフルなのにライトした", // msg
`OVL_COVER_DEFAULT, // coverage_level
`OVL_POSEDGE, // clock_edge
`OVL_ACTIVE_HIGH, // reset_polarity
`OVL_GATE_CLOCK // gating_type
) afifo_overflow_assertion (
clk_ddr2,
reset_ddr2,
1'b1,
afifo_overflow,
fire_overflow
);
ovl_never #(
`OVL_ERROR, // severity_level
`OVL_ASSERT, // property_type
"ERROR : FIFOが空なのにリードした", // msg
`OVL_COVER_DEFAULT, // coverage_level
`OVL_POSEDGE, // clock_edge
`OVL_ACTIVE_HIGH, // reset_polarity
`OVL_GATE_CLOCK // gating_type
) afifo_underflow_assertion (
clk_cam,
reset_cam,
1'b1,
afifo_underflow,
fire_underflow
);
// synthesis translate_on
ovl_never : test_exprが決して真にならないことをチェックする。例えば、サイコロの値をdice_cntとすると、test_exprはdice_cnt>6と表される。dice_cntが7以上になればアサーション・エラーとなる
-Define OVL_VERILOG
-Define OVL_INIT_MSG
-Define OVL_COVER_ON
-Define OVL_ASSERT_ON
-Define OVL_MAX_REPORT_ERROR=1
-include_dir ../../../../OVL/std_ovl
-lib_dir ../../../../OVL/std_ovl
は必要ない。-lib_ext vlib
-- tb_req_ack.vhd
-- OVL_Verilogアサーションを使用する
-- tb_req_ack.vhd本体
library ieee;
use ieee.std_logic_1164.all;
use ieee.std_logic_unsigned.all;
use ieee.std_logic_arith.all;
library accellera_ovl_vhdl;
use accellera_ovl_vhdl.std_ovl.all;
use accellera_ovl_vhdl.std_ovl_procs.all;
-- use accellera_ovl_vhdl.std_ovl_components.all;
library accellera_ovl_vlog;
use accellera_ovl_vlog.all; -- ovl_frameをuse
library work;
use work.proj_pkg.all;
entity tb_req_ack is
end tb_req_ack;
architecture testbench_arch of tb_req_ack is
component ack_sm
port(
clk : in std_logic;
reset : in std_logic;
req0 : in std_logic;
req1 : in std_logic;
ta0 : in std_logic; -- Transfer Acknowledge
ta1 : in std_logic; -- Transfer Acknowledge
ack0 : out std_logic;
ack1 : out std_logic
);
end component;
component req_sm
port(
clk : in std_logic;
reset : in std_logic;
req_start : in std_logic;
ack : in std_logic;
req : out std_logic
);
end component;
component ovl_next
generic (
severity_level : ovl_severity_level := OVL_SEVERITY_LEVEL_NOT_SET;
num_cks : positive := 1;
check_overlapping : ovl_chk_overlap := OVL_CHK_OVERLAP_OFF;
check_missing_start : ovl_ctrl := OVL_OFF;
property_type : ovl_property_type := OVL_PROPERTY_TYPE_NOT_SET;
msg : string := OVL_MSG_NOT_SET;
coverage_level : ovl_coverage_level := OVL_COVERAGE_LEVEL_NOT_SET;
clock_edge : ovl_active_edges := OVL_ACTIVE_EDGES_NOT_SET;
reset_polarity : ovl_reset_polarity := OVL_RESET_POLARITY_NOT_SET;
gating_type : ovl_gating_type := OVL_GATING_TYPE_NOT_SET;
controls : ovl_ctrl_record := OVL_CTRL_DEFAULTS
);
port (
clock : in std_logic;
reset : in std_logic;
enable : in std_logic;
start_event : in std_logic;
test_expr : in std_logic;
fire : out std_logic_vector(OVL_FIRE_WIDTH - 1 downto 0)
);
end component ovl_next;
component ovl_frame
generic (
severity_level : ovl_severity_level := OVL_SEVERITY_DEFAULT;
min_cks : natural := 0;
max_cks : natural := 0;
action_on_new_start : natural := OVL_ACTION_ON_NEW_START_DEFAULT;
property_type : ovl_property_type := OVL_PROPERTY_DEFAULT;
msg : string := OVL_MSG_DEFAULT;
coverage_level : ovl_coverage_level := OVL_COVER_DEFAULT;
clock_edge : ovl_active_edges := OVL_CLOCK_EDGE_DEFAULT;
reset_polarity : ovl_reset_polarity := OVL_RESET_POLARITY_DEFAULT;
gating_type : ovl_gating_type := OVL_GATING_TYPE_DEFAULT;
controls : ovl_ctrl_record := OVL_CTRL_DEFAULTS
);
port (
clock : in std_logic;
reset : in std_logic;
enable : in std_logic;
start_event : in std_logic;
test_expr : in std_logic;
fire : out std_logic_vector(OVL_FIRE_WIDTH - 1 downto 0)
);
end component ovl_frame;
signal clk : std_logic := '1';
signal reset : std_logic := '1';
signal req_start0 : std_logic := '0';
signal req_start1 : std_logic := '0';
signal req0 : std_logic := '0';
signal req1 : std_logic := '0';
signal ta0 : std_logic := '0';
signal ta1 : std_logic := '0';
signal ack0 : std_logic := '0';
signal ack1 : std_logic := '0';
signal fire_ta0_ack0_as, fire_ta1_ack1_as : std_logic_vector(OVL_FIRE_WIDTH - 1 downto 0);
signal fire_req0_ack0_as, fire_req1_ack1_as : std_logic_vector(OVL_FIRE_WIDTH - 1 downto 0);
constant PERIOD : time := 20 ns;
constant DUTY_CYCLE : real := 0.5;
-- req_startとtaを出力するprocedure
procedure REQ_START_TA(
signal clk : in std_logic;
loop_count : in integer;
signal req_start : out std_logic;
signal ta : out std_logic
) is
begin
wait until clk'event and clk='1'; -- clkの立ち上がりまでwait
wait for 1 ns; -- 遅延を挟んで
req_start <= '1';
wait until clk'event and clk='1'; -- clkの立ち上がりまでwait
wait for 1 ns; -- 遅延を挟んで
req_start <= '0';
for n in loop_count to 1 loop
wait until clk'event and clk='1'; -- clkの立ち上がりまでwait
wait for 1 ns; -- 遅延を挟んで
end loop;
ta <= '1';
wait until clk'event and clk='1'; -- clkの立ち上がりまでwait
wait for 1 ns; -- 遅延を挟んで
ta <= '0';
end REQ_START_TA;
begin
-- clkの生成（50MHz）
clk_generate : process begin
clock_loop : loop
clk <= '1';
wait for (PERIOD * DUTY_CYCLE);
clk <= '0';
wait for (PERIOD - (PERIOD * DUTY_CYCLE));
end loop clock_loop;
end process clk_generate;
-- シミュレーション時にOVLチェッカの初期化数を表示
ovl_print_init_count_p : process begin
wait for 0 ns;
ovl_print_init_count_proc(ovl_proj_controls);
wait; -- forever
end process ovl_print_init_count_p;
-- resetの生成
reset_generate : process begin
reset <= '1';
wait for 100 ns;
reset <= '0';
wait; -- forever
end process reset_generate;
ack_sm_inst : ack_sm port map(
clk => clk,
reset => reset,
req0 => req0,
req1 => req1,
ta0 => ta0,
ta1 => ta1,
ack0 => ack0,
ack1 => ack1
);
req_am_inst0 : req_sm port map(
clk => clk,
reset => reset,
req_start => req_start0,
ack => ack0,
req => req0
);
req_am_inst1 : req_sm port map(
clk => clk,
reset => reset,
req_start => req_start1,
ack => ack1,
req => req1
);
-- req_start0 とta0 の関係を生成する
process begin
req_start0 <= '0';
ta0 <= '0';
wait until reset'event and reset='0'; -- resetの立ち下がりまでwait
wait for 100 ns;
REQ_START_TA(clk, 1, req_start0, ta0);
REQ_START_TA(clk, 2, req_start0, ta0);
REQ_START_TA(clk, 3, req_start0, ta0);
REQ_START_TA(clk, 2, req_start0, ta0);
REQ_START_TA(clk, 1, req_start0, ta0);
REQ_START_TA(clk, 3, req_start0, ta0);
REQ_START_TA(clk, 2, req_start0, ta0);
wait for 200 ns;
assert (false) report "Simulation End!" severity failure;
end process;
-- req_start1 とta1 の関係を生成する
process begin
req_start1 <= '0';
ta1 <= '0';
wait until reset'event and reset='0'; -- resetの立ち下がりまでwait
wait for 100 ns;
REQ_START_TA(clk, 2, req_start1, ta1);
REQ_START_TA(clk, 1, req_start1, ta1);
REQ_START_TA(clk, 2, req_start1, ta1);
REQ_START_TA(clk, 3, req_start1, ta1);
REQ_START_TA(clk, 3, req_start1, ta1);
REQ_START_TA(clk, 1, req_start1, ta1);
REQ_START_TA(clk, 2, req_start1, ta1);
wait; -- forever
end process;
-- OVLアサーション
ovl_gen : if (ovl_proj_controls.assert_ctrl = OVL_ON) generate
ta0_ack0_assertion : ovl_next generic map (
severity_level => OVL_ERROR,
num_cks => 1,
check_overlapping => OVL_CHK_OVERLAP_OFF,
check_missing_start => OVL_ON,
property_type => OVL_ASSERT,
msg =>"ERROR: ack0 isn't asserted of with the next clock that ta0 was asserted.",
coverage_level => OVL_COVER_BASIC,
clock_edge => OVL_POSEDGE,
reset_polarity => OVL_ACTIVE_HIGH,
gating_type => OVL_GATE_CLOCK,
controls => OVL_CTRL_DEFAULTS
)port map (
clock => clk,
reset => reset,
enable => '1',
start_event => ta0,
test_expr => ack0,
fire => fire_ta0_ack0_as
);
ta1_ack1_assertion : ovl_next generic map (
severity_level => OVL_ERROR,
num_cks => 1,
check_overlapping => OVL_CHK_OVERLAP_OFF,
check_missing_start => OVL_ON,
property_type => OVL_ASSERT,
msg =>"ERROR: ack1 isn't asserted of with the next clock that ta1 was asserted.",
coverage_level => OVL_COVER_BASIC,
clock_edge => OVL_POSEDGE,
reset_polarity => OVL_ACTIVE_HIGH,
gating_type => OVL_GATE_CLOCK,
controls => OVL_CTRL_DEFAULTS
)port map (
clock => clk,
reset => reset,
enable => '1',
start_event => ta1,
test_expr => ack1,
fire => fire_ta1_ack1_as
);
req0_ack0_assertion : ovl_frame generic map(
severity_level => OVL_ERROR,
min_cks => 2,
max_cks => 4,
action_on_new_start => OVL_IGNORE_NEW_START,
property_type => OVL_ASSERT,
msg => "ERROR: ack0 isn't asserted after 2-4 clocks after req0 was asserted.",
coverage_level => OVL_COVER_BASIC,
clock_edge => OVL_POSEDGE,
reset_polarity => OVL_ACTIVE_HIGH,
gating_type => OVL_GATE_CLOCK,
controls => OVL_CTRL_DEFAULTS
) port map(
clock => clk,
reset => reset,
enable => '1',
start_event => req0,
test_expr => ack0,
fire => fire_req0_ack0_as
);
req1_ack1_assertion : ovl_frame generic map(
severity_level => OVL_ERROR,
min_cks => 2,
max_cks => 4,
action_on_new_start => OVL_IGNORE_NEW_START,
property_type => OVL_ASSERT,
msg => "ERROR: ack1 isn't asserted after 2-4 clocks after req1 was asserted.",
coverage_level => OVL_COVER_BASIC,
clock_edge => OVL_POSEDGE,
reset_polarity => OVL_ACTIVE_HIGH,
gating_type => OVL_GATE_CLOCK,
controls => OVL_CTRL_DEFAULTS
) port map(
clock => clk,
reset => reset,
enable => '1',
start_event => req1,
test_expr => ack1,
fire => fire_req1_ack1_as
);
end generate ovl_gen;
end testbench_arch;
# OVL_ERROR : OVL_NEXT : ERROR: ack1 isn't asserted of with the next clock that ta1 was asserted. : Test expression is not asserted after elapse of num_cks cycles from start event : severity 1 : time 260000 : tb_req_ack.ovl_gen.ta1_ack1_assertion.ovl_error_t
# OVL_ERROR : OVL_NEXT : ERROR: ack0 isn't asserted of with the next clock that ta0 was asserted. : Test expression is not asserted after elapse of num_cks cycles from start event : severity 1 : time 280000 : tb_req_ack.ovl_gen.ta0_ack0_assertion.ovl_error_t
# OVL_ERROR : OVL_FRAME : ERROR: ack0 isn't asserted after 2-4 clocks after req0 was asserted. : Test expression is not TRUE within specified maximum max_cks cycles from start event : severity 1 : time 300000 : tb_req_ack.ovl_gen.req0_ack0_assertion.ovl_error_t
# OVL_ERROR : OVL_FRAME : ERROR: ack1 isn't asserted after 2-4 clocks after req1 was asserted. : Test expression is not TRUE within specified maximum max_cks cycles from start event : severity 1 : time 300000 : tb_req_ack.ovl_gen.req1_ack1_assertion.ovl_error_t
# OVL_ERROR : OVL_NEXT : ERROR: ack0 isn't asserted of with the next clock that ta0 was asserted. : Test expresson is asserted without a corresponding start_event : severity 1 : time 320000 :
tb_req_ack.ovl_gen.ta0_ack0_assertion.ovl_error_t
# OVL_ERROR : OVL_NEXT : ERROR: ack1 isn't asserted of with the next clock that ta1 was asserted. : Test expresson is asserted without a corresponding start_event : severity 1 : time 320000 :
tb_req_ack.ovl_gen.ta1_ack1_assertion.ovl_error_t
# OVL_ERROR : OVL_NEXT : ERROR: ack0 isn't asserted of with the next clock that ta0 was asserted. : Test expression is not asserted after elapse of num_cks cycles from start event : severity 1 : time 340000 : tb_req_ack.ovl_gen.ta0_ack0_assertion.ovl_error_t
# OVL_ERROR : OVL_NEXT : ERROR: ack1 isn't asserted of with the next clock that ta1 was asserted. : Test expression is not asserted after elapse of num_cks cycles from start event : severity 1 : time 340000 : tb_req_ack.ovl_gen.ta1_ack1_assertion.ovl_error_t
# OVL_ERROR : OVL_NEXT : ERROR: ack0 isn't asserted of with the next clock that ta0 was asserted. : Test expression is not asserted after elapse of num_cks cycles from start event : severity 1 : time 400000 : tb_req_ack.ovl_gen.ta0_ack0_assertion.ovl_error_t
# OVL_ERROR : OVL_NEXT : ERROR: ack1 isn't asserted of with the next clock that ta1 was asserted. : Test expression is not asserted after elapse of num_cks cycles from start event : severity 1 : time 400000 : tb_req_ack.ovl_gen.ta1_ack1_assertion.ovl_error_t
# OVL_ERROR : OVL_NEXT : ERROR: ack0 isn't asserted of with the next clock that ta0 was asserted. : Test expresson is asserted without a corresponding start_event : severity 1 : time 440000 :
tb_req_ack.ovl_gen.ta0_ack0_assertion.ovl_error_t
# OVL_ERROR : OVL_NEXT : ERROR: ack1 isn't asserted of with the next clock that ta1 was asserted. : Test expresson is asserted without a corresponding start_event : severity 1 : time 440000 :
tb_req_ack.ovl_gen.ta1_ack1_assertion.ovl_error_t
# OVL_ERROR : OVL_NEXT : ERROR: ack0 isn't asserted of with the next clock that ta0 was asserted. : Test expression is not asserted after elapse of num_cks cycles from start event : severity 1 : time 460000 : tb_req_ack.ovl_gen.ta0_ack0_assertion.ovl_error_t
# OVL_ERROR : OVL_NEXT : ERROR: ack1 isn't asserted of with the next clock that ta1 was asserted. : Test expression is not asserted after elapse of num_cks cycles from start event : severity 1 : time 460000 : tb_req_ack.ovl_gen.ta1_ack1_assertion.ovl_error_t
# OVL_ERROR : OVL_NEXT : ERROR: ack1 isn't asserted of with the next clock that ta1 was asserted. : Test expression is not asserted after elapse of num_cks cycles from start event : severity 1 : time 520000 : tb_req_ack.ovl_gen.ta1_ack1_assertion.ovl_error_t
# OVL_ERROR : OVL_NEXT : ERROR: ack0 isn't asserted of with the next clock that ta0 was asserted. : Test expression is not asserted after elapse of num_cks cycles from start event : severity 1 : time 540000 : tb_req_ack.ovl_gen.ta0_ack0_assertion.ovl_error_t
# OVL_ERROR : OVL_FRAME : ERROR: ack0 isn't asserted after 2-4 clocks after req0 was asserted. : Test expression is not TRUE within specified maximum max_cks cycles from start event : severity 1 : time 560000 : tb_req_ack.ovl_gen.req0_ack0_assertion.ovl_error_t
# OVL_ERROR : OVL_FRAME : ERROR: ack1 isn't asserted after 2-4 clocks after req1 was asserted. : Test expression is not TRUE within specified maximum max_cks cycles from start event : severity 1 : time 560000 : tb_req_ack.ovl_gen.req1_ack1_assertion.ovl_error_t
# OVL_ERROR : OVL_NEXT : ERROR: ack0 isn't asserted of with the next clock that ta0 was asserted. : Test expresson is asserted without a corresponding start_event : severity 1 : time 580000 :
tb_req_ack.ovl_gen.ta0_ack0_assertion.ovl_error_t
# OVL_ERROR : OVL_NEXT : ERROR: ack1 isn't asserted of with the next clock that ta1 was asserted. : Test expresson is asserted without a corresponding start_event : severity 1 : time 580000 :
tb_req_ack.ovl_gen.ta1_ack1_assertion.ovl_error_t
# OVL_ERROR : OVL_NEXT : ERROR: ack0 isn't asserted of with the next clock that ta0 was asserted. : Test expression is not asserted after elapse of num_cks cycles from start event : severity 1 : time 600000 : tb_req_ack.ovl_gen.ta0_ack0_assertion.ovl_error_t
# OVL_ERROR : OVL_NEXT : ERROR: ack1 isn't asserted of with the next clock that ta1 was asserted. : Test expression is not asserted after elapse of num_cks cycles from start event : severity 1 : time 600000 : tb_req_ack.ovl_gen.ta1_ack1_assertion.ovl_error_t
# OVL_ERROR : OVL_NEXT : ERROR: ack0 isn't asserted of with the next clock that ta0 was asserted. : Test expression is not asserted after elapse of num_cks cycles from start event : severity 1 : time 660000 : tb_req_ack.ovl_gen.ta0_ack0_assertion.ovl_error_t
# OVL_ERROR : OVL_NEXT : ERROR: ack1 isn't asserted of with the next clock that ta1 was asserted. : Test expression is not asserted after elapse of num_cks cycles from start event : severity 1 : time 660000 : tb_req_ack.ovl_gen.ta1_ack1_assertion.ovl_error_t
# OVL_ERROR : OVL_FRAME : ERROR: ack0 isn't asserted after 2-4 clocks after req0 was asserted. : Test expression is not TRUE within specified maximum max_cks cycles from start event : severity 1 : time 700000 : tb_req_ack.ovl_gen.req0_ack0_assertion.ovl_error_t
# OVL_ERROR : OVL_FRAME : ERROR: ack1 isn't asserted after 2-4 clocks after req1 was asserted. : Test expression is not TRUE within specified maximum max_cks cycles from start event : severity 1 : time 700000 : tb_req_ack.ovl_gen.req1_ack1_assertion.ovl_error_t
# ** Failure: Simulation End!
# Time: 841 ns Iteration: 0 Process: /tb_req_ack/line__183 File: C:/HDL/OVL/examples/req_ack_test_vhdl_vlog/tb_req_ack.vhd
# Break at C:/HDL/OVL/examples/req_ack_test_vhdl_vlog/tb_req_ack.vhd line 196
-- proj_pkg.vhd
library accellera_ovl_vhdl;
use accellera_ovl_vhdl.std_ovl.all;
use accellera_ovl_vhdl.std_ovl_procs.all;
package proj_pkg is
-- OVL configuration
constant ovl_proj_controls : ovl_ctrl_record := (
-- generate statement controls
xcheck_ctrl => OVL_ON,
implicit_xcheck_ctrl => OVL_ON,
init_msg_ctrl => OVL_ON,
init_count_ctrl => OVL_OFF,
assert_ctrl => OVL_ON,
cover_ctrl => OVL_ON,
global_reset_ctrl => OVL_OFF,
finish_ctrl => OVL_ON,
gating_ctrl => OVL_ON,
-- user configurable library constants
max_report_error => 4,
max_report_cover_point => 15,
runtime_after_fatal => "150 ns ",
-- default values for common generics
severity_level_default => OVL_SEVERITY_DEFAULT,
property_type_default => OVL_PROPERTY_DEFAULT,
--msg_default => OVL_MSG_DEFAULT,
msg_default => ovl_set_msg("Assertion Error"),
coverage_level_default => OVL_COVER_DEFAULT,
clock_edge_default => OVL_CLOCK_EDGE_DEFAULT,
reset_polarity_default => OVL_RESET_POLARITY_DEFAULT,
gating_type_default => OVL_GATING_TYPE_DEFAULT
);
end package proj_pkg;
-- OVLテスト用 req_sm.vhd
-- req_start 信号を受けると、reqを1にアサートする。ackを受け取るとreqを0にディアサートする
library ieee;
use ieee.std_logic_1164.all;
use ieee.std_logic_unsigned.all;
use ieee.std_logic_arith.all;
entity req_sm is
port(
clk : in std_logic;
reset : in std_logic;
req_start : in std_logic;
ack : in std_logic;
req : out std_logic
);
end req_sm;
architecture RTL of req_sm is
type cs_req_state is (idle_req, assert_req);
signal cs_req : cs_req_state;
begin
process(clk) begin
if clk'event and clk='1' then
if reset='1' then
cs_req <= idle_req;
req <= '0';
else
case cs_req is
when idle_req =>
if req_start='1' then
cs_req <= assert_req;
req <= '1';
end if;
when assert_req =>
if ack='1' then
cs_req <= idle_req;
req <= '0';
end if;
end case;
end if;
end if;
end process;
end RTL;
-- OVLテスト用 ack_sm.vhd
-- 2つのreqを管理して、reqがアサートされている状態で、taがアサートされるとackを返す
library ieee;
use ieee.std_logic_1164.all;
use ieee.std_logic_unsigned.all;
use ieee.std_logic_arith.all;
entity ack_sm is
port(
clk : in std_logic;
reset : in std_logic;
req0 : in std_logic;
req1 : in std_logic;
ta0 : in std_logic; -- Transfer Acknowledge
ta1 : in std_logic; -- Transfer Acknowledge
ack0 : out std_logic;
ack1 : out std_logic
);
end ack_sm;
architecture RTL of ack_sm is
type cs_main_state is (idle_req, assert_req0, assert_req1, assert_req01, req0_ack, req1_ack, req01_ack);
signal cs_main : cs_main_state;
begin
process(clk) begin
if clk'event and clk='1' then
if reset='1' then
cs_main <= idle_req;
ack0 <= '0'; ack1 <= '0';
else
case cs_main is
when idle_req =>
if req0='1' then
cs_main <= assert_req0;
ack0 <= '0'; ack1 <= '0';
elsif req1='1' then
cs_main <= assert_req1;
ack0 <= '0'; ack1 <= '0';
end if;
when assert_req0 =>
if req1='1' then
cs_main <= assert_req01;
ack0 <= '0'; ack1 <= '0';
elsif ta0='1' then
cs_main <= req0_ack;
ack0 <= '1'; ack1 <= '0';
end if;
when assert_req1 =>
if req0='1' then
cs_main <= assert_req01;
ack0 <= '0'; ack1 <= '0';
elsif ta1='1' then
cs_main <= req1_ack;
ack0 <= '0'; ack1 <= '1';
end if;
when assert_req01 =>
if ta0='1' and ta1='0' then
cs_main <= req0_ack;
ack0 <= '1'; ack1 <= '0';
elsif ta0='0' and ta1='1' then
cs_main <= req1_ack;
ack0 <= '0'; ack1 <= '1';
elsif ta0='1' and ta1='1' then
cs_main <= req01_ack;
ack0 <= '1'; ack1 <= '1';
end if;
when req0_ack =>
if req1='1' then
cs_main <= assert_req1;
ack0 <= '0'; ack1 <= '0';
else
cs_main <= idle_req;
ack0 <= '0'; ack1 <= '0';
end if;
when req1_ack =>
if req0='1' then
cs_main <= assert_req0;
ack0 <= '0'; ack1 <= '0';
else
cs_main <= idle_req;
ack0 <= '0'; ack1 <= '0';
end if;
when req01_ack =>
cs_main <= idle_req;
ack0 <= '0'; ack1 <= '0';
end case;
end if;
end if;
end process;
end RTL;
-- tb_req_ack.vhd
-- tb_req_ack.vhd本体
library ieee;
use ieee.std_logic_1164.all;
use ieee.std_logic_unsigned.all;
use ieee.std_logic_arith.all;
library accellera_ovl_vhdl;
use accellera_ovl_vhdl.std_ovl.all;
use accellera_ovl_vhdl.std_ovl_components.all;
use accellera_ovl_vhdl.std_ovl_procs.all;
library work;
use work.proj_pkg.all;
entity tb_req_ack is
end tb_req_ack;
architecture testbench_arch of tb_req_ack is
component ack_sm
port(
clk : in std_logic;
reset : in std_logic;
req0 : in std_logic;
req1 : in std_logic;
ta0 : in std_logic; -- Transfer Acknowledge
ta1 : in std_logic; -- Transfer Acknowledge
ack0 : out std_logic;
ack1 : out std_logic
);
end component;
component req_sm
port(
clk : in std_logic;
reset : in std_logic;
req_start : in std_logic;
ack : in std_logic;
req : out std_logic
);
end component;
signal clk : std_logic := '1';
signal reset : std_logic := '1';
signal req_start0 : std_logic := '0';
signal req_start1 : std_logic := '0';
signal req0 : std_logic := '0';
signal req1 : std_logic := '0';
signal ta0 : std_logic := '0';
signal ta1 : std_logic := '0';
signal ack0 : std_logic := '0';
signal ack1 : std_logic := '0';
signal fire_ta0_ack0_as, fire_ta1_ack1_as : std_logic_vector(OVL_FIRE_WIDTH - 1 downto 0);
signal fire_req0_ack0_as, fire_req1_ack1_as : std_logic_vector(OVL_FIRE_WIDTH - 1 downto 0);
constant PERIOD : time := 20 ns;
constant DUTY_CYCLE : real := 0.5;
-- req_startとtaを出力するprocedure
procedure REQ_START_TA(
signal clk : in std_logic;
loop_count : in integer;
signal req_start : out std_logic;
signal ta : out std_logic
) is
begin
wait until clk'event and clk='1'; -- clkの立ち上がりまでwait
wait for 1 ns; -- 遅延を挟んで
req_start <= '1';
wait until clk'event and clk='1'; -- clkの立ち上がりまでwait
wait for 1 ns; -- 遅延を挟んで
req_start <= '0';
for n in loop_count to 1 loop
wait until clk'event and clk='1'; -- clkの立ち上がりまでwait
wait for 1 ns; -- 遅延を挟んで
end loop;
ta <= '1';
wait until clk'event and clk='1'; -- clkの立ち上がりまでwait
wait for 1 ns; -- 遅延を挟んで
ta <= '0';
end REQ_START_TA;
begin
-- clkの生成（50MHz）
clk_generate : process begin
clock_loop : loop
clk <= '1';
wait for (PERIOD * DUTY_CYCLE);
clk <= '0';
wait for (PERIOD - (PERIOD * DUTY_CYCLE));
end loop clock_loop;
end process clk_generate;
-- シミュレーション時にOVLチェッカの初期化数を表示
ovl_print_init_count_p : process begin
wait for 0 ns;
ovl_print_init_count_proc(ovl_proj_controls);
wait; -- forever
end process ovl_print_init_count_p;
-- resetの生成
reset_generate : process begin
reset <= '1';
wait for 100 ns;
reset <= '0';
wait; -- forever
end process reset_generate;
ack_sm_inst : ack_sm port map(
clk => clk,
reset => reset,
req0 => req0,
req1 => req1,
ta0 => ta0,
ta1 => ta1,
ack0 => ack0,
ack1 => ack1
);
req_am_inst0 : req_sm port map(
clk => clk,
reset => reset,
req_start => req_start0,
ack => ack0,
req => req0
);
req_am_inst1 : req_sm port map(
clk => clk,
reset => reset,
req_start => req_start1,
ack => ack1,
req => req1
);
-- req_start0 とta0 の関係を生成する
process begin
req_start0 <= '0';
ta0 <= '0';
wait until reset'event and reset='0'; -- resetの立ち下がりまでwait
wait for 100 ns;
REQ_START_TA(clk, 1, req_start0, ta0);
REQ_START_TA(clk, 2, req_start0, ta0);
REQ_START_TA(clk, 3, req_start0, ta0);
REQ_START_TA(clk, 2, req_start0, ta0);
REQ_START_TA(clk, 1, req_start0, ta0);
REQ_START_TA(clk, 3, req_start0, ta0);
REQ_START_TA(clk, 2, req_start0, ta0);
wait for 200 ns;
assert (false) report "Simulation End!" severity failure;
end process;
-- req_start1 とta1 の関係を生成する
process begin
req_start1 <= '0';
ta1 <= '0';
wait until reset'event and reset='0'; -- resetの立ち下がりまでwait
wait for 100 ns;
REQ_START_TA(clk, 2, req_start1, ta1);
REQ_START_TA(clk, 1, req_start1, ta1);
REQ_START_TA(clk, 2, req_start1, ta1);
REQ_START_TA(clk, 3, req_start1, ta1);
REQ_START_TA(clk, 3, req_start1, ta1);
REQ_START_TA(clk, 1, req_start1, ta1);
REQ_START_TA(clk, 2, req_start1, ta1);
wait; -- forever
end process;
-- OVLアサーション
ovl_gen : if (ovl_proj_controls.assert_ctrl = OVL_ON) generate
ta0_ack0_assertion : ovl_next generic map (
severity_level => OVL_ERROR,
num_cks => 1,
check_overlapping => OVL_CHK_OVERLAP_OFF,
check_missing_start => OVL_ON,
property_type => OVL_ASSERT,
msg =>"ERROR: ack0 isn't asserted of with the next clock that ta0 was asserted.",
coverage_level => OVL_COVER_BASIC,
clock_edge => OVL_POSEDGE,
reset_polarity => OVL_ACTIVE_HIGH,
gating_type => OVL_GATE_CLOCK,
controls => OVL_CTRL_DEFAULTS
)port map (
clock => clk,
reset => reset,
enable => '1',
start_event => ta0,
test_expr => ack0,
fire => fire_ta0_ack0_as
);
ta1_ack1_assertion : ovl_next generic map (
severity_level => OVL_ERROR,
num_cks => 1,
check_overlapping => OVL_CHK_OVERLAP_OFF,
check_missing_start => OVL_ON,
property_type => OVL_ASSERT,
msg =>"ERROR: ack1 isn't asserted of with the next clock that ta1 was asserted.",
coverage_level => OVL_COVER_BASIC,
clock_edge => OVL_POSEDGE,
reset_polarity => OVL_ACTIVE_HIGH,
gating_type => OVL_GATE_CLOCK,
controls => OVL_CTRL_DEFAULTS
)port map (
clock => clk,
reset => reset,
enable => '1',
start_event => ta1,
test_expr => ack1,
fire => fire_ta1_ack1_as
);
end generate ovl_gen;
end testbench_arch;
# OVL_ERROR : OVL_NEXT : ERROR: ack1 isn't asserted of with the next clock that ta1 was asserted. : Test expression is not asserted after elapse of num_cks cycles from start event : severity 1 : time 260000 ps :tb_req_ack:ovl_gen:ta1_ack1_assertion:
# OVL_ERROR : OVL_NEXT : ERROR: ack0 isn't asserted of with the next clock that ta0 was asserted. : Test expression is not asserted after elapse of num_cks cycles from start event : severity 1 : time 280000 ps :tb_req_ack:ovl_gen:ta0_ack0_assertion:
# OVL_ERROR : OVL_NEXT : ERROR: ack0 isn't asserted of with the next clock that ta0 was asserted. : Test expression is not asserted after elapse of num_cks cycles from start event : severity 1 : time 400000 ps :tb_req_ack:ovl_gen:ta0_ack0_assertion:
# OVL_ERROR : OVL_NEXT : ERROR: ack1 isn't asserted of with the next clock that ta1 was asserted. : Test expression is not asserted after elapse of num_cks cycles from start event : severity 1 : time 400000 ps :tb_req_ack:ovl_gen:ta1_ack1_assertion:
# OVL_ERROR : OVL_NEXT : ERROR: ack1 isn't asserted of with the next clock that ta1 was asserted. : Test expression is not asserted after elapse of num_cks cycles from start event : severity 1 : time 520000 ps :tb_req_ack:ovl_gen:ta1_ack1_assertion:
# OVL_ERROR : OVL_NEXT : ERROR: ack0 isn't asserted of with the next clock that ta0 was asserted. : Test expression is not asserted after elapse of num_cks cycles from start event : severity 1 : time 540000 ps :tb_req_ack:ovl_gen:ta0_ack0_assertion:
# OVL_ERROR : OVL_NEXT : ERROR: ack0 isn't asserted of with the next clock that ta0 was asserted. : Test expression is not asserted after elapse of num_cks cycles from start event : severity 1 : time 660000 ps :tb_req_ack:ovl_gen:ta0_ack0_assertion:
# OVL_ERROR : OVL_NEXT : ERROR: ack1 isn't asserted of with the next clock that ta1 was asserted. : Test expression is not asserted after elapse of num_cks cycles from start event : severity 1 : time 660000 ps :tb_req_ack:ovl_gen:ta1_ack1_assertion:
# ** Failure: Simulation End!
# Time: 841 ns Iteration: 0 Process: /tb_req_ack/line__133 File: H:/HDL/OVL/example/req_ack_test_vhdl/tb_req_ack.vhd
# Break in Process line__133 at H:/HDL/OVL/example/req_ack_test_vhdl/tb_req_ack.vhd line 146
cd H:/HDL/OVL/std_ovl
vlib accellera_ovl_vlog
vlog -work accellera_ovl_vlog +define+OVL_VERILOG +define+OVL_ASSERT_ON +define+OVL_FINISH_OFF +incdir+H:/HDL/OVL/std_ovl ovl_*.v
vlib accellera_ovl_vhdl
vcom -93 -work accellera_ovl_vhdl std_ovl.vhd
vcom -93 -work accellera_ovl_vhdl std_ovl_procs.vhd
vcom -93 -work accellera_ovl_vhdl std_ovl_components_vlog.vhd
vcom -93 -work accellera_ovl_vhdl std_ovl_clock_gating.vhd
vcom -93 -work accellera_ovl_vhdl std_ovl_reset_gating.vhd
vcom -93 -work accellera_ovl_vhdl ovl_*.vhd
vcom -93 -work accellera_ovl_vhdl vhdl93/ovl_*_rtl.vhd
ovl_always : 常に式が成り立つかを見ている(val1 < val2)
ovl_always_on_edge : サンプリングイベントの時に式が成り立つかを見ている（サンプリングイベント=ack, 式=(MAIN_STATE==ACK_STATE))(VHDLは無し)
ovl_change : start_eventが起こった時から、num_cksで示されたクロック以内に出力値が変化すことを保証する(VHDLは無し)
ovl_cycle_sequence : ステートマシンの遷移条件をテストできる。WR→WAIT→(WRまたはDONE)
ovl_decrement : ある値で減算するカウンタ等をテストできる（VHDLは無し）
ovl_delta : 信号がある一定の範囲で変化することをテストできる（VHDLは無し）
ovl_even_parity : 偶数パリティをチェックする（VHDLは無し）
ovl_fifo_index : FIFOのオーバーフローとアンダーフローをチェックする。push,pop条件を監視しdepthを設定することでチェックすることができる（VHDLは無し）
ovl_frame : start_eventとあるtest_exprの関係をテストできる。start_eventが変化してからtest_exprが変化するまでのクロック数を最小値、最大値で表する（VHDLは無し）
ovl_handshake : requestとacknowledgeの関係をovl_frame等よりも詳細にチェックすることができる。req, ackの厳密な関係を記述したい場合はこれを使うべきだと思う（VHDLは無し）
ovl_implication : 原因と結果の関係をテストする。antecedent_exprがアサートされている時に、consequent_exprもアサートされているかをチェックする
ovl_increment：ある値で加算するカウンタ等をテストできる（VHDLは無し）
ovl_never : test_exprが決して真にならないことをチェックする。例えば、サイコロの値をdice_cntとすると、test_exprはdice_cnt>6と表される。dice_cntが7以上になればアサーション・エラーとなる
ovl_never_unkown : qualifierがTRUEの時に、test_exprに不定値を含むかどうかをチェックする
ovl_never_unkown_async : 非同期（クロックイベントがない）のovl_never_unkown
ovl_next : start_eventとtest_expr間のアサートのクロックのタイミングをチェックする。ovl_frameと異なるのは、クロックのタイミングが固定されていること
ovl_no_overflow : test_exprがminとmaxの間にあるかどうかをチェックする(VHDLは無し)
ovl_no_transition : start_stateを指定して、次のステートがnext_stateに遷移しないことをチェックする(VHDLは無し)
ovl_no_underflow : test_exprがminとmaxの間にあるかどうかをチェックする(VHDLは無し)
ovl_odd_parity : test_exprが奇数パリティであることをチェックする(VHDLは無し)
ovl_one_cold : test_exprのステート値などのどれか1ビットが0であることをチェックする(VHDLは無し)
ovl_one_hot : test_exprのどれか1ビットだけが1であることをチェックする
ovl_proposition : test_exprが成立することをチェックする。組み合わせ回路(VHDLは無し)
ovl_quiescent_state : sample_eventがTRUEの時に、state_exprがcheck_valueと同一になっているかをチェックする(VHDLは無し)
ovl_range : test_exprの値がmin値とmax値の間にあることをチェックする
ovl_time : start_eventがTRUEになった次のクロックからnum_cksクロック間、test_exprの条件が成り立つことをチェックする(VHDLは無し)
ovl_transition : test_exprの信号がstart_stateの次のステートがnext_stateであることをチェックする(VHDLは無し)（注：必ずしもステートマシンのステートチェックだけではなく、1つ前の状態と次の状態のチェックをする。enableを使うとクロックが離れていても使える）
ovl_unchange : start_eventがTRUEになってから、test_exprの信号がnum_cksクロック間、変化しないことをチェックする(VHDLは無し)
ovl_width : パルス幅をチェックする。test_exprがTRUEの幅が、min_cksとmax_cksのクロックの間に入っていることをチェックする(VHDLは無し)
ovl_win_change : start_eventがTRUEになってから、end_eventがTRUEになるまでの間(event window)に、test_exprが変化することをチェックする(VHDLは無し)
ovl_win_unchange : start_eventがTRUEになってから、end_eventがTRUEになるまでの間(event window)に、test_exprが変化しないことをチェックする(VHDLは無し)
ovl_window : start_eventがTRUEになってから、end_eventがTRUEになるまでの間(event window)に、test_exprが常にTRUEであることをチェックする(VHDLは無し)
ovl_zero_one_hot : test_exprのどれか1ビットだけが1かまたは、オール0であることをチェックする
ovl_always, ovl_cycle_sequence, ovl_implication, ovl_never, ovl_never_unkown, ovl_next, ovl_one_hot, ovl_range, ovl_win_unchange, ovl_zero_one_hot
| 日 | 月 | 火 | 水 | 木 | 金 | 土 |
|---|---|---|---|---|---|---|
| - | - | - | - | 1 | 2 | 3 |
| 4 | 5 | 6 | 7 | 8 | 9 | 10 |
| 11 | 12 | 13 | 14 | 15 | 16 | 17 |
| 18 | 19 | 20 | 21 | 22 | 23 | 24 |
| 25 | 26 | 27 | 28 | 29 | 30 | - |