In reply to ben@SystemVerilog.us:
If you insist on writing the code in SVA, then consider the following
// SVA SOLUTION THAT WILL NOT WORK !!!!
property WILL_NOT_WORK_countab;
int va=0, vb=0;
go |-> ##[1:$] (a || b, va=va+a, vb=vb+b) ##0 (done, dostats(va, vb));
endproperty
ap_LOOKS_LIKE_IT_WILL_WORK_BUT_DOES_NOT_WORK: assert property( p_countab);
The property shown below fails to work because in SVA, if the sequence makes assignments to local variables, then each of the sequence involved in the ORing carries its own individual and separate copy of the local variables.
the (##[1:$] seq) is same as (##1 seq or ##2 seq or … ##n seq)
The following will work though because the property calls a task as a match item, and pass whatever values are needed. Thus,
task do_calc(int va, vb, bit go, done);
static int cta;
static int ctb;
if(go) begin cta=0; ctb=0; end
if(done) begin
$display("t=%t, calc_cta=%d, calc_ctb=%d, stats=", $time, cta, ctb, 100*cta/ctb);
end
if(a) cta=cta+1'b1;
if(b) ctb=ctb+1'b1;
endtask
property p_countab_ok;
int va=0, vb=0;
(go, do_calc(va, vb, go, done)) |->
(##[1:$] (a || b, do_calc(va, vb, go, done)) ##0 done) or
(done[->1], do_calc(0, 0, 0, done));
endproperty
ap_countab_ok: assert property(p_countab_ok);
Simulation file is at http://SystemVerilog.us/fv/countpulses.sv
sim results
# t= 650, ctab_cta= 7, ctab_ctb= 6, stats= 116
# t= 650, calc_cta= 7, calc_ctb= 6, stats= 116
# t= 1250, ctab_cta= 12, ctab_ctb= 9, stats= 133
# t= 1250, calc_cta= 12, calc_ctb= 9, stats= 133
# t= 1850, ctab_cta= 12, ctab_ctb= 8, stats= 150
# t= 1850, calc_cta= 12, calc_ctb= 8, stats= 150
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us