Write an assertion where in if a signal A goes high in one cycle, signals B and C should go low in the same cycle

SystemVerilog
1

Hello, I am trying to write an assertion for the following scenario
If signal A goes high in one cycle, signals B and C should go low in the same cycle

I tried doing something as follows:


 property A_high_B_and_C_low;
   disable iff(rst)
   A |-> (B == 0) && (C == 0);
 endproperty

assert property(A_high_B_and_C_low) else $error("Assertion failed");

But in the above case the implication operator makes it such that B and C should go low a cycle after A goes high. How do I change this so that I ensure B and C go low the same cycle A goes high?

2

In reply to vk7715:

Could you share the entire code along with the waveform? I want to analyze the output you are getting.

3

In reply to vk7715:

You have used overlapping implication operator(|->). It should evaluate antecedent and consequent on same clock cycle only.

Success/failure of concurrent assertions are not executed immediately, but in the reactive region.

  • Values of variables used in assertions are sampled in Preponed region.
  • Evaluation of property expressions in Observed region.
  • Execution of pass/fail code from property expressions in Reactive region.

Check this code: assertion - EDA Playground
Here value of A is changing at 45ns and assertion fail message is printed at 55ns.

Your requirement is - If signal A goes high in one cycle, signals B and C should go low in the same cycle.
For this you can write like this-


 property A_high_B_and_C_low;
   @(posedge clk) disable iff(rst)
    $rose(A) |-> ($fell(B) & $fell(C));
 endproperty
 assert property(A_high_B_and_C_low) else $error("Assertion failed");