SVA signal stability check between 2 events

SystemVerilog
,
1

Hello,
my goal is to write some SVA code in order to detect whether a given signal ‘sig’ changes between 2 events, ‘start_ev’ and ‘end_ev’, that in general will be asynchronous with sig clock.
The idea is that the signal and the events should be part of a SV interface, but the events may be controlled by a UVM testbench. For example, end_ev could be triggered by a timeout (from here the necessity of asynchronicity).
A similar question had been asked before in:

https://verificationacademy.com/forums/systemverilog/assertion-check-if-does-not-rise-between-pulse-b-and-pulse-c#reply-42989

    
    logic a[1:0];
    event start_ev, end_ev;

    property p_stable(logic sig,  event start_ev, event end_ev);
           (reject_on (sig)
		  @(start_ev) 1'b1 |-> @(end_ev) 1'b1); 
    endproperty

    property p_stable_spec;
        p_stable(a[1], posedge(a[0]), negedge(a[0]));
    endproperty

but the solution requires to hardwire, in the property, the expected value of sig, while that may change in different phases of the test.

I then ran into a paper by Doulos’s Doug Smith (http://www.doulos.com/knowhow/sysverilog/DVCon10_sva_paper/DVCon2010_AsyncSVA_paper.pdf), dealing with asynchronous SVAs, where this property is shown.


    property p_stable(logic sig,  event start_ev, event end_ev);
        bit loc_sig;

        @(start_ev) (1'b1, loc_sig = sig) ##1 @(end_ev or sig) (loc_sig == sig);
    endproperty

The problem (highlighted in the paper) is that this solution does not work, because the value of sig in


@(end_ev or sig) (loc_sig == sig);

is sampled in the Preponed region, and not in the Reactive one (it’s essentially the value of sig before it changes).
Possible workarounds (listed in the paper) require to hardwire the name of the checked signal somewhere in the code.

I am asking here if someone knows a solution that does not require to duplicate much code if one has many properties of the same kind involving different signals.
Thanks in advance,

Lanfranco

2

Would this solution work for you?


 always begin
    	automatic bit loc_sig;
    	@(start_ev)	loc_sig =sig; 
    	fork 
    		@(end_ev) 
    			if (loc_sig != sig) $display("a t=%t, error in sig @end_ev", $time);
    		@(sig) 
    		    if (loc_sig != sig) $display("at t=%t, error in sig @sig", $time); 
    	join_any 
    	
    end

Note: Could use immediate assertions instead of the “if” statements.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

  • SystemVerilog Assertions 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
3

In reply to lanfranco.salinari:

Hello Ben,
I, too, thought about a procedural solution in alternative to the SVA one.
I don’t like very much the fact that I have to replicate the code for each signal (a macro can help here) but it may be manageable.
By the way, I don’t think that loc_sig is necessary: if end_ev occurs first, sig has not changed, in the other case, sig has certainly toggled.
Besides this a “disable fork” at the end is necessary, in my opinion, to avoid giving errors every time sig changes.
stable_ev and not_stable_ev are simply events to pass information to the testbench.


always begin
    	@(start_ev); 
    	fork 
            begin
    		@(end_ev);
                -> stable_ev;
            end
            begin    			
    		@(sig); 
    		-> not_stable_ev; 
            end
    	join_any 
        disable fork
end

What do you think about this variation?
Thanks and regards,

Lanfranco

4

In reply to lanfranco.salinari:
Doesn’t the join_any terminate the fork?
Can the generate statement provide help?
Ben SystemVerilog,us

5

In reply to ben@SystemVerilog.us:

No, the join_any does not automatically kill the processes spawned by the fork (see SV 2012 std, par.9.6.3).
About the generate, well maybe it can help, I have never used it extensively.
Thanks,

Lanfranco

6

In reply to lanfranco.salinari:
OK, thanks.