In reply to Tudor Timi:
See embedded comments
*In reply to ben@SystemVerilog.us:*I’m curious where you want to go with this, so I’ll bite.
Thanks for providing a substantial reply.
My goals for asking for these challenges include:
- Demonstrate how assertions provide several benefits, besides verification.
- Assertions challenge ambiguous requirements, and force the clarification of issues, even if minute (more on that below).
- Demonstrate the need for reviews, and that includes assertions, code, and verification methodologies.
- Provide my reviews and comments, perhaps for the benefits of the community.
- Promote the use of assertions.
I don’t have a testbench to submit, but I do have assertions. I used a formal tool to prove them:
Good approach. BTW, I did provide a testbench (see my original post above). I found that the quickest way to build a testbench to verify assertions is to use the SV randomize with weighted distributions. Example:
initial begin
rst_n <= 1'b0;
@(posedge clk) #2 rst_n <= 1'b1;
repeat(200) begin
@(posedge clk);
#2if (!randomize(data_in, ld_enb, count_enb, rst_n) with
{ ld_enb dist {1'b1:=1, 1'b0:=8};
count_enb dist {1'b1:=1, 1'b0:=2};
rst_n dist {1'b1:=12, 1'b0:=1};
}) `uvm_error("MYERR", "This is a randomize error")
end
$finish;
end
// Your code
...
count_out_reset_val : assert property (
$rose(rst_n) |-> count_out == 0 );
// Not specified, but I think it's ok to say that before preloading we've
// finished counting.
term_count_reset_val : assert property (
$rose(rst_n) |-> term_count == 1 );
[Ben] Is is really a good idea, from an operation viewpoint, to have
term_count==1 upon a reset? If this was my design, I would have preferred a count_out to be '1.
[Ben] Why the $rose(rst_n)? Though the $rose if often used because the interest is indeed on just the rose(signal), in this case, we’re talking about a reset, thus, the assertion should be true for every cycle rst_n is asserted. Since rst_n is active low, the !rst_n or the rst_n==1’b1 should be used instead.
load : assert property (
load_en |=> count_out == $past(data_in)
);
The rst_n is ignored here.
No default disable iff defined.
// Not specified, but I'll define load as having priority over count.
count : assert property (
count_en && !load_en |=> count_out == $past(count_out) - 1
); // [Ben] Good assumption
term_count_tracks_count_out : assert property (
//term_count iff count_out == 0
(count_out == 0 |-> term_count) and
(term_count |-> count_out == 0)
);
[Ben] Interesting corollary; I like it. Again, no default disable iff
Some things weren’t fully specified so I chose what to implement. I said that when coming out of reset, we start in the terminal state. This means that pre-loading is mandatory. It would have also probably been valid to start in the full value state to be able to count down immediately. I also said that loading has priority over counting.
I also added a constraint to disallow counting from the terminal state:
no_count_when_term : assume property (
term_count |-> !count_en );
[Ben] Good that you wrote assumptions to clarify your design, and for use by formal verification.
I wrote some simple coverage points for some cases I deemed interesting:
load_0 : cover property (
load_en && data_in == 0 );
load_0_after_non_zero_count : cover property (
load_en && data_in == 0 && count_out != 0
);
decrement_to_0 : cover property (
count_out != 0 && count_en && !load_en
);
[Ben] Good idea to add coverage.
Here’s the RTL code I ended up with:
module dncounter #(WIDTH = 4) (
input bit rst_n,
input bit clk,
input logic count_en,
input logic load_en,
input logic [WIDTH-1:0] data_in,
output logic [WIDTH-1:0] count_out,
output logic term_count
);
always @(posedge clk or negedge rst_n)
if (rst_n == 0) begin
count_out <= 0;
end
else begin
if (load_en) begin
count_out <= data_in;
end
else if (count_en) begin
count_out <= count_out - 1;
end
end
// I implemented 'term_count' as a registered output, but it coult also be
// implemented combinatorially (with some area savings, but output delay).
always @(posedge clk or negedge rst_n)
if (rst_n == 0) begin
term_count <= 1;
end
else begin
if (load_en) begin
if (data_in == 0)
term_count <= 1;
else
term_count <= 0;
end
else if (count_en) begin
if (count_out == 1)
term_count <= 1;
else
term_count <= 0;
end
end
endmodule
I chose to implement term_count sequentially, but I could have just as well implemented it combinatorially. I would have probably saved on logic (comparators), but I would have had output delay on the signal.
Now that I think about it a bit more, maybe it would have made more sense to define that in the terminal state, even when count comes, count_out stays 0. This way an integrator can just tie the count signal to 1 and play with loading.
[Ben] Yes.
Ben’s solution
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