forked from tanchou/Verilog
71 lines
1.6 KiB
Verilog
71 lines
1.6 KiB
Verilog
`timescale 1ns/1ps
|
|
`default_nettype none
|
|
|
|
// Simple counter_reg with synchronous reset (and no load)
|
|
//
|
|
|
|
module counter #(
|
|
parameter WIDTH = 8,
|
|
parameter INITIAL_VALUE = 8'h0f
|
|
) (
|
|
input wire clk, // global clock
|
|
input wire reset, // synchronous reset signal
|
|
input wire en, // enable signal
|
|
output reg strobe // output strobe
|
|
);
|
|
|
|
initial strobe = 0;
|
|
|
|
reg[WIDTH-1:0] counter_reg = INITIAL_VALUE;
|
|
|
|
always @(posedge clk) begin
|
|
if (reset) begin
|
|
counter_reg <= INITIAL_VALUE;
|
|
end
|
|
else if (en) begin
|
|
strobe <= 0;
|
|
if (counter_reg == 0)
|
|
counter_reg <= INITIAL_VALUE;
|
|
else begin
|
|
if (counter_reg == 1)
|
|
strobe <= 1;
|
|
counter_reg <= counter_reg - 1;
|
|
end
|
|
end
|
|
|
|
end
|
|
|
|
`ifdef FORMAL
|
|
|
|
reg f_past_valid = 0;
|
|
|
|
always @* f_past_valid = !$initstate;
|
|
|
|
always @* begin
|
|
assume (counter_reg <= INITIAL_VALUE);
|
|
end
|
|
|
|
always @(posedge clk) begin
|
|
// if ($initstate) begin
|
|
// assume(counter_reg==INITIAL_VALUE);
|
|
// end
|
|
// if (!$initstate && $past(en)==1 && !$past(reset)) begin
|
|
if (f_past_valid && $past(en)==1 && !$past(reset)) begin
|
|
if (counter_reg < INITIAL_VALUE)
|
|
assert (counter_reg == $past(counter_reg) - 1);
|
|
else begin
|
|
assert(counter_reg == INITIAL_VALUE && $past(counter_reg)==0);
|
|
end
|
|
end
|
|
end
|
|
|
|
`endif
|
|
|
|
|
|
`ifdef VERIFIC
|
|
//internal_check: assert property (@(posedge clk)(counter_reg==11)|=>(counter_reg==10));
|
|
//assert property (@(posedge clk)(counter_reg==11 && en && !reset)|=>(counter_reg==10));
|
|
`endif
|
|
|
|
|
|
endmodule |