SVA Simple challenge: Write design and SVA for a down counter

Another version of RTL

NOTE: Feedback’s are welcome



module dncounter  #(WIDTH = 4) (
  output logic[WIDTH-1:0] count_out,  // counter ouput
  output logic termcount,  // terminal cont when counter==0
  input logic[WIDTH-1:0] data_in, // initial count, loaded with ld_enb
  input logic ld_enb, count_enb, rst_n, clk // active lo reset
  );

  // Assumption
  // 1 -> termcount should be ZERO post power on rest 
  //  	  (i.e. counter should initialized with WIDTH'b1 duruing reset)
  // 2 -> counter should not be over-run once it's triggered termcount (even count_enb HIGH)
  //      (i.e. counter should re-initialized via ld_enb (or) reset once it's triggered termcount)


  logic [WIDTH-1:0] 	dncounter;
  logic [WIDTH-1:0]  	dncounter_nxt;
  logic 		dncounter_at_zero, dncounter_at_zero_flag;

  // Output Generation
  assign count_out 	= dncounter;
  assign termcount 	= dncounter_at_zero;


  // Check whether counter reached ZERO or not
  assign dncounter_at_zero= (|dncouter) ? 1'b0 : 1'b1;
  
  // Initialize the counter when ld_enb is HIGH
  // Decrement the counter when " count_enb is HIGH and counter does not reached ZERO (i.e. after ld_enb HIGH)"
  assign dncounter_nxt  = (ld_enb) ? data_in : ((count_enb && ~dncounter_at_zero_flag) ? (dncounter - 1'b1) : dncounter);


  always @ (posedge clk or negedge rst_n)
  begin
	if(~rst_n)
		dncounter <= WIDTH'b1;  // To avoid termcount assertion immediately after power on reset
	else
		dncounter <= dncounter_nxt;
  end
 
 always @ (posedge clk or negedge rst_n)
 begin
	if(~rst_n)
		dncounter_at_zero_flag <= 1'b0;		 
	else if(ld_en) // clearing the flag 
		dncounter_at_zero_flag <= 1'b0;
	else  // registering the termcount assertion. it's used along with count_enb to avoid counter over-runnig
		dncounter_at_zero_flag <= dncounter_at_zero;
 end 

 endmodule