In reply to Prabhu Kamalanathan:
Thanks for providing a reply with code and assertions. From my reply above, you can most likely appreicate the need for assertions, even for sch a trivial design.
Another version of RTL
...
// Assumption
// 1 -> termcount should be ZERO post power on rest
// (i.e. counter should initialized with WIDTH'b1 during 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)
[Ben] Those were also my assumptions.
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);
[Ben] You seem to have taken a “gate-level” rather than an RTL approach in your coding. I say this because you use temporary variables to compute the computational logic prior to loading it into the registers. That is more gate-level, and have done that in the past with drawing tools that picked gates and drew lines for interconnects. Actually, I would date myself if I also admit that I used velum paper and peeled primitives (FF, gates) off a sheet of pre-printed primitives. These were then pasted onto the paper, and I used a drafting ruler to make the interconnects. Do they still teach drafting in engineering school? :)
IMHO, this make the code more difficult to follow, and adds line to the code. See my code below, which is more RTL.
always @ (posedge clk or negedge rst_n)
begin
if(~rst_n)
dncounter <= WIDTH'b1; // To avoid termcount assertion immediately after power on reset
[Ben] WIDTH’b1 is illegal, should be '1. See code below
module top; // [Ben]
parameter WIDTH=4;
bit[WIDTH-1 : 0] a, b;
initial begin
b= WIDTH'b1; // syntax error, unexpected BASE, expecting ';'.
a='1;
end
endmodule
[your code]
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
[/quote]
My code
module dncounter #(WIDTH = 4) (
output logic[WIDTH-1:0] count_out,
output logic termcount,
input logic[WIDTH-1:0] data_in,
input logic ld_enb, count_enb, rst_n, clk
);
always_ff @ (posedge clk or negedge rst_n)
begin
if (!rst_n) count_out <= '1;
else if (ld_enb) count_out <= data_in;
else if (count_enb)
if (count_out != 0) count_out <= count_out - 1'b1;
end
assign termcount = (count_out == 0) ? 1'b1 : 1'b0;
// assertions
default clocking @(posedge clk); endclocking
default disable iff !rst_n;
ap_load: assert property(##1 ld_enb |=> count_out==$past(data_in));
ap_count: assert property(##1 !ld_enb && count_enb && count_out!=0 |=> count_out==$past(count_out) - 1'b1);
ap_nocount: assert property(##1 !ld_enb && count_out==0 |=> $stable(count_out) );
ap_termcount0: assert property(count_out !='0 |-> !termcount);
ap_termcount1: assert property(count_out =='0 |-> termcount);
ap_reset: assert property(disable iff(1'b0) !rst_n |=> count_out=='1);
endmodule // dncounter
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
- SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
- A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
- Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
- Component Design by Example ", 2001 ISBN 0-9705394-0-1
- VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
- VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115