diff --git a/counter/Makefile b/counter/Makefile index 8634882..f7c4eba 100644 --- a/counter/Makefile +++ b/counter/Makefile @@ -1,6 +1,7 @@ -alu: counter.vhd counter_t.sv counter_f.sby +.PHONY: counter +counter: counter.vhd counter_t.sv counter_f.sby sby -f -d work counter_f.sby - +.PHONY: clean clean: rm -rf work diff --git a/counter/counter.vhd b/counter/counter.vhd index 70d9bfa..b0537f6 100644 --- a/counter/counter.vhd +++ b/counter/counter.vhd @@ -5,6 +5,9 @@ use ieee.numeric_std.all; entity counter is + generic ( + Init : natural := 8 + ); port ( Reset_n_i : in std_logic; Clk_i : in std_logic; @@ -23,7 +26,7 @@ begin process (Reset_n_i, Clk_i) is begin if (Reset_n_i = '0') then - Data_o <= 32x"8"; + Data_o <= std_logic_vector(to_unsigned(Init, Data_o'length)); elsif (rising_edge(Clk_i)) then if (unsigned(Data_o) <= 64) then Data_o <= std_logic_vector(unsigned(Data_o) + 1); @@ -33,3 +36,4 @@ begin end architecture rtl; + diff --git a/counter/counter_t.sv b/counter/counter_t.sv index 19b1bad..79a18cb 100644 --- a/counter/counter_t.sv +++ b/counter/counter_t.sv @@ -1,27 +1,29 @@ module counter_t ( - inout Reset_n_i, + input Reset_n_i, input Clk_i, input [31:0] Data_i, output [31:0] Data_o ); - counter counter_i ( + `define INIT_VALUE 8 + + + counter #(.Init(`INIT_VALUE)) counter_i ( .Reset_n_i(Reset_n_i), .Clk_i(Clk_i), .Data_o(Data_o) ); - reg init_state; + reg init_state = 1; - initial init_state = 1; + always @(*) + if (init_state) assume (!Reset_n_i); always @(posedge Clk_i) init_state = 0; - always @(*) - assume (Reset_n_i == ~init_state); /* // Don't works with Verific at the moment @@ -32,8 +34,9 @@ module counter_t ( // Proves fail, counterexample hasn't initial reset active - assert property (@(posedge Clk_i) Data_o >= 8 && Data_o <= 64); + assert property (@(posedge Clk_i) Data_o >= `INIT_VALUE && Data_o <= 64); assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Data_o < 64 |=> Data_o == $past(Data_o) + 1); endmodule +