In reply to Rocketfingers:
You need a supporting logic for the never cases that you identified.
I added the “started” flag that gets set when started, and reset when stop or done (end is a reserved word). For the never sequences, here is an example
ap_start_start: assert property(not(start ##1 (start && started[->1])) );
That states that there should never be sequence start followed by an occurrence of start and the started flag. Come to think of it, could that be replaced with just:
ap_start_start: assert property(not( (start && started)) );
Below is my code with a testbench
/* I want assertions that check
1 - every start ( // 1 cycle)is followed by an end or a stop (start to start back to back cannot occur)
2 - every stop ( // 1 cycle ) or end (done // 1 cycle)is followed by a start ( no back to back stops or ends)
So valid sequences are
Start stop start
Start end start
Examples of invalid sequences are
Start start
Start end end
Start stop stop
Start stop end */
import uvm_pkg::*; `include "uvm_macros.svh"
module top;
timeunit 1ns; timeprecision 100ps;
bit clk,start, stop, done, started;
default clocking @(posedge clk);
endclocking
initial forever #10 clk=!clk;
function void set_started(bit a);
started = a;
endfunction : set_started
// 1 - every start is followed by an end or a stop (start to start back to back cannot occur)
ap_start_stopr_or_done: assert property(
(start, set_started(1)) |=> stop[->1] or done[->1])
set_started(0); else set_started(0);
// every stop ( // 1 cycle ) or end (done // 1 cycle)is followed by a start ( no back to back stops or ends)
ap_stop_done_to_start: assert property((stop || done) |=> start[->1] );
//Start .. start with NO done or stop, i.e, when in the started state
ap_start_start: assert property(not(start ##1 (start && started[->1])) );
// Start end end
ap_start_end_end: assert property(not(done && started==1'b0));
// Start stop stop
ap_start_stop_stop: assert property(not(stop && started==1'b0));
// Start stop end
ap_start_stop_end: assert property(not(done && started==1'b0) );
initial begin
bit va, vb, vc;
repeat(200) begin
@(posedge clk);
if (!randomize(va, vb, vc) with
{ va dist {1'b1:=1, 1'b0:=3};
vb dist {1'b1:=1, 1'b0:=2};
vc dist {1'b1:=1, 1'b0:=2};
}) `uvm_error("MYERR", "This is a randomize error")
start <= va;
stop <= vb;
done <= vc;
end
$stop;
end
endmodule
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
- 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 978-1539769712
- 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
- SVA Alternative for Complex Assertions
Verification Horizons - March 2018 Issue | Verification Academy - SVA: Package for dynamic and range delays and repeats | Verification Academy
- SVA in a UVM Class-based Environment
SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy