In reply to Avinash:
Lets take a counter design which output a count value. The counter update happen on many input conditions. As inputs are many I cannot use assertions
You’re underestimating the powers of assertions. For complex problems, like the ones you are referring to, you need to write multiple small assertions. Since you’re addressing a counter, below is something I wrote for a class on assertions. It’s a very funky type of counter!!!
Requirements
- Loadable synchronous up-counter
- reset to MIN_COUNT if rst_n==0
- Min load value == MIN_COUNT (default ==2)
- Max count value == MAX_COUNT (default ==9)
- holds the count when it reaches the maximum value
- Must change value at least every 9 clocks
- Increments If ld==1’b0 and the counter != MAX_COUNT
The Model with assertions:
package counter_pkg;
timeunit 1ns; timeprecision 100ps;
`define TOP counter_tb
const int MAX_COUNT=6, MIN_COUNT=3;
typedef enum {CT_LOAD, CT_RESET, CT_WAIT, CT_DONE} ct_scen_e;
endpackage : counter_pkg
module counter_max (
input logic[3:0] data_in,
input logic ld,
output logic[3:0] counter,
input logic clk, rst_n) ;
import counter_pkg::*;
int cover_count=0;
int fail_count=0;
// ap_P: assert property(@ (posedge clk) P )
// parameter MIN_COUNT=2; // module item parameter
// If use of parameter port list, then can't use defparam
default disable iff !rst_n;
property p_load;
logic[3:0] v_data_in; // local variable to property
(ld && (data_in>= MIN_COUNT && data_in <= MAX_COUNT), v_data_in=data_in) |=>
counter==v_data_in;
endproperty : p_load
ap_load: assert property ( @(posedge clk) p_load);
property p_hold_on_load;
ld && (data_in< MIN_COUNT || data_in > MAX_COUNT) |=>
$stable(counter);
endproperty : p_hold_on_load
ap_hold_on_load: assert property ( @(posedge clk) p_hold_on_load);
ap_count: assert property(@(posedge clk)
!ld && (counter!=MAX_COUNT) |=> counter==$past(counter)+1'b1);
ap_hold: assert property(@(posedge clk)
!ld && counter==MAX_COUNT |=> counter==$past(counter));
mp_min_load: assume property(@(posedge clk)
ld |-> not(data_in<MIN_COUNT));
mp_max_load: assume property(@ (posedge clk)
ld |-> not(data_in > MAX_COUNT))
cover_count++; else fail_count++ ;
ap_statble8: assume property(@(posedge clk)
$stable(counter)|-> ##[1:8] !$stable(counter));
ap_reset: assert property(@ (posedge clk) disable iff (1'b0)
!rst_n |=> counter==MIN_COUNT);
always @(posedge clk) begin : counter1
if(!rst_n) counter <= MIN_COUNT;
else if (ld && data_in >= MIN_COUNT && data_in <= MAX_COUNT)
counter <= data_in;
else if (!ld && counter!=MAX_COUNT) begin : counter2
counter <= counter + 1'b1;
end : counter2
end : counter1
endmodule : counter_max
Notice the many small assertions that cover the different cases; thus, your statement that “As inputs are many I cannot use assertions” is not true.
Question : While building the scorboard(checker) I end up modelling the design.
Sometime it gets complex and my checkers wont be stable for all the possible scenarios ,
dont know if my approach is right. Any thoughts on it ?
The scoreboard may indeed possess a lot of the modeling feature of the original design, and this is why the checker with scoreboarding may not necessarily prove that the design is OK. Below is code from by testbench scoreboard (used as demo for the class)
virtual function void counter_scoreboard ();
//forever begin : f_ever
$display("counter_scoreboard started @ %t", $time);
// @(this.m_vif.driver_cb)
if (this.m_vif.mon_cb.rst_n==1'b0) begin
$display("counter_scoreboard reset @ %t", $time);
this.counter =MIN_COUNT;
end
else if (this.m_vif.mon_cb.ld) begin : load
if (this.m_vif.mon_cb.data_in >= MIN_COUNT &&
this.m_vif.mon_cb.data_in <= MAX_COUNT) begin : if2
this.counter = this.m_vif.mon_cb.data_in;
$display("this.counter in checker=%d", this.counter);
end : if2
end : load
else if(this.counter==MAX_COUNT)
this.counter = this.counter + 1'b0;
else this.counter = this.counter + 1'b1;
// end : f_ever
endfunction : counter_scoreboard
Do you suggest any other way?
I like assertions because they get into the individual requirements.
Scoreboarding works too, but you have to be careful.
Another approach is through the use of signatures generated with LFSRs with one signature from a known good model exercised over several (e.g., thousands) of cycles, and the other from the DUT. This is indeed the model used for acceptance tests for an ASIC in production. Wayback Machine
is a VHDL package of LFSRs that I wrote several years ago.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
- SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6
- 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