verilog - Why are "if..else" statements not encouraged within systemverilog assertion property?

Question

I am writing an assertion check for the following structure

Basically, I want to check that output is equal to d1 when select signal is 0 and output is equal to d2 when select signal is 1.

I did something like this:

property check_mux_out (clk, rst, en, d1, output, d2, select);
   @(posedge clk)
   if (select)
      (rst==0) && (en==1) |-> (output === d2);
   else
      (rst==0) && (en==1) |-> (output === d1);
endproperty

a1: assert property (check_mux_out(inst1_clk, inst1_rst, latch_en, signal1, inst_out, signal2, inst_select)) else $error("ERROR: output not equal input");

However I came across some posts from https://verificationacademy.com/forums/systemverilog/conditional-statement-assertion-property and https://verificationacademy.com/forums/systemverilog/clock-period-checker-sva that seem to suggest that if..else statements should not be used within systemverilog properties. Why is it so? Is what I did wrong and why?

question from:https://stackoverflow.com/questions/65856569/why-are-if-else-statements-not-encouraged-within-systemverilog-assertion-prop

Answer 1

I guess, the only advise is to avoid writing big properties. It is very easy to mess up the code. if/else just add to size and have a potential to further obfuscate it.

Your code has syntactic errors. You cannot use the keyword outptut as a variable name. there is also an extra ; in your code, after the if clause.

property check_mux_out (clk, rst, en, d1, out, d2, select);
   @(posedge clk)
   if (select)
      (rst==0) && (en==1) |-> (out === d2) // << no ';'
   else
      (rst==0) && (en==1) |-> (out === d1);
endproperty

You can re-write it in a different way as well:

property check_mux_out (clk, rst, en, d1, out, d2, select);
   @(posedge clk)
     (rst==0) && (en==1) |-> if (select) (out === d2) else (out === d1);
endproperty

or even without if/else

property check_mux_out (clk, rst, en, d1, out, d2, select);
   @(posedge clk)
  (rst==0) && (en==1) |-> (select) ? (out === d2) : (out === d1);
endproperty