`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