Formal Verification SVA assume signal to NOT toggle at negedge

SystemVerilog
, ,
1

Hi,

I have a bit as a primary input to the DUT.
The only specification for this signal is that the value cannot change at the negative edge of the clock.

However, without additional constraints, the formal tool would toggle the signal at the negative edge.

I tried the following assume property but it is not working:


ASSUME_SIGNAL_IS_FULL_CYCLE: assume property (@(posedge clk)
    sig
        |->
    strong(sig[*1:$])
);

Is there a construct / statement that would constrain such bit to NOT toggle at the negative edge?

2

In reply to erictaur:
If FV can handle multi locking, you can write something like:


property p; 
 bit v; 
  @(posedge clk) (1, v=sig) ##0 @(negedge clk) sig==v; 
endproperty 
ap_p: assert property(p);

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  2. Free books:
  3. Papers:
    Understanding the SVA Engine,
    Verification Horizons
    Reflections on Users’ Experiences with SVA, part 1 and part 2
    Reflections on Users’ Experiences with SVA

SUPPORT LOGIC AND THE ALWAYS PROPERTY
http://systemverilog.us/vf/support_logic_always.pdf
SVA Alternative for Complex Assertions
https://verificationacademy.com/news/verification-horizons-march-2018-issue
SVA in a UVM Class-based Environment
https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment
SVA for statistical analysis of a weighted work-conserving prioritized round-robin arbiter.
https://verificationacademy.com/forums/coverage/sva-statistical-analysis-weighted-work-conserving-prioritized-round-robin-arbiter.

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/

3

In reply to ben@SystemVerilog.us:

I checked, Yes, multiclocking should be supported in general.
Ben

4

In reply to ben@SystemVerilog.us:

In reply to ben@SystemVerilog.us:
I checked, Yes, multiclocking should be supported in general.
Ben

Hi Ben,

Thanks for your reply!

I have to add a -lca option to the elaborate command for this syntax to work but in the attached waveform, the signal is still toggling at the negative edge (as seen in marker intervals).

Link to screenshot

5

In reply to erictaur:

I have a bit as a primary input to the DUT.
The only specification for this signal is that the value cannot change at the negative edge of the clock.

Sorry, you should have used the assume instead of the assert.
I still don’t understand why the signal toggles in mid-bit.
Do you have things toggling at both edges of the clock?
Why do you have this need to make this assumption?

6

In reply to ben@SystemVerilog.us:

Hi Ben,

Thank you for responding!

Yes I did modify your snippet to be an assume property.
The signal in question, though being a primary input to the DUT, is actually flopped outside of the DUT – hence constraining that it should only be toggling / changing values at the posedge.

As far as I know, the DUT and the submodules within are operating on the posedge of the clock.
The behavior of the signal toggling at the negedge is most likely a result of the formal tool (VC-Formal to be exact)

7

In reply to erictaur:
Does it really matter if sig** is toggling at the negedge as long as setup time is abided by? Besides, Formal verification does not handle setup and hold as this is done by a static timing analyzer tool. Thus, going back to the original question: Why the need for this assumption of the sig not toggling at the midway point?
Perhaps your intend if for the signal to be stable for 2 consecutive cycles, something like:


@(posedge clk) $changed(sig) |=> $stable(sig);

Ben

8

In reply to ben@SystemVerilog.us:

Hi Ben,

The reason for constraining this signal is because it is messing with my helper FSMs. The next_state (being driven by combinational logic) would jump all over the place if this signal is not stable at the negedge.

For now indeed I am forcing the signal (with the following) to be high for 2 or more cycles but that snips out a portion of the valid state space.


ASSUME_FullCycle: assume property (@(posedge CCLK)
  sig
    |->
  sig[*2:$]
);
9

In reply to erictaur:

The reason for constraining this signal is because it is messing with my helper FSMs. The next_state (being driven by combinational logic) would jump all over the place if this signal is not stable at the negedge.

I must be missing something here because support-logic driven with proper SV guidelines and synchronous to the DUT should not be dependent on setup times. Are you using nonblocking assignments? Are you using the edge of the clock in your logic?
I may be wrong, but it seems to me that something is wrong with the way you are using SystemVerilog. Typical good SystemVerilog Example:
Again, I fail to understand your need for the assume.
If I were a reviewer of your code then you better give me a good explanation.


module top;
  bit clk, a, b, c, e, f; 
  typedef enum {A,B} AB_t;  
  AB_t fsm;  
  initial forever #10 clk = !clk; 
  always @(posedge clk) begin
    if(a) fsm <= A; 
    else  fsm <= B;     
  end 
  always_comb begin
    if(fsm==A) c=e && f; 
    else c=0; 
  end

...
endmodule
10

Resolved with set_change_at command in VC-Formal
Check section 4.4 Stabilizing Constraints in Multi-Clock Designs in VC-Formal User Guide

Thanks Ben for providing feedback

1 Like