Concurrent assertion checking the condition even when clk is not high

SystemVerilog
,
1

Hi Everyone, I’m trying to write an assertion to check that input1 and input2 shouldn’t be equal at posedge of clk. But, i’m encountering an issue: the assertion is getting triggered even when the clock is not going high(also when clk is not even stabilised,x->0) .

This is my initial assertion: I’m passing disable condition instead of using reset to disable the assertion. Value of dis_cond will alway be '0.

assign dis_cond=0;
property vld_inp(reg clk, logic dis_cond, logic input1, logic input2);
 @(posedge clk) disable iff (dis_cond==1)
   input1 !=  input2;
endproperty
assert_valid_inp_check : assert property(vld_inp(clk,dis_cond,input1,input2)) else $error("Assertion vld_inp_chk failed");

Later i modified it to check only when both inputs are stabilised but still the assertion is failing as it is getting triggered when clk is 'x. Can you help me understand why it is getting triggered when clk is not valid?

property vld_inp(reg clk, logic reset, logic input1, logic input2);
 @(posedge clk) disable iff (disable_con==1)
   (!$isunknown(input1) && !$isunknown(input2)) |-> (input1 !=  input2);
endproperty
assert_valid_inp_check : assert property(vld_inp(clk,dis_cond,input1,input2)) else $error("Assertion vld_inp_chk failed");
2

A posedge event is

  • 0 → 1, 0 → x, 0 → z
  • x → 1, z → 1

x → 0 is supposed to be a negedge, so I don’t know how that would have triggered any assertions. We need a minimal, complete reproducible example.

I don’t understand what you are doing with dis_cond. There are much simpler mechanisms to disable assertions with $assertoff/on

Note that an x value does not mean unstabilized–it just means its value is unknown.

3

See SystemVerilog and Verilog X Optimism - Verilog Pro

SystemVerilog and Verilog X Optimism – You May Not Be Simulating What You Think

August 19, 2015 by Jason Yu
The issue I see is your requirements:

  1. check that input1 and input2 shouldn’t be equal at posedge of clk.
  2. Check to be done when clk is stable
  3. Check to occur “n” cycles after reset is inactive.

Fix your requirements first, then write the assertions.

4

Hi Dave, apologies for the delayed response. I have changed my property and added reset condition in disable like you suggested. Thanks for the help.

5

@ben2 I have added reset condition in my assertion to disable the assertion when reset is active and it worked. Thanks for your inputs.

6

Forbidding property needed here, sometimes we need to check some property should not occur.
I tried using below assertion, it will also work.


AST : assert property (@(posedge clk) not(input1 != input2));
7

Hi,
I’m confused why you’re using not(expression). Doesn’t it change it the requirement altogether? not(inp1 != inp2) but i want to check that at every posedge of clk, input != input2 should become true.

8

Yes I was wrong.
Correct code are below

AST: assert property (@(posedge clk && !$isunknown(clk)) not(input1 == input2));