Regarding system verilog assertions

The ~ and ! operators are clearly described in the SystemVerilog LRM with examples. See section 11.4 Operator Descriptions. Do you have a copy?

There are no examples of $fell on its own in the LRM; it is usually used in the context of an assertion where there is a reference clock cycle. $fell(X) returns true if the LSB of X is 0 in the current cycle when it was not 0 in the previous cycle.

There is no $rise() in SystemVerilog, only the past tense $rose(). Since this is digital logic simulation, not analog, you can only know that a signal rises after it has already risen.

So you can write

assert property(@posedge clk !b |-> !$rose(a));

But it is easier to understand this property by simplifying it using DeMorgan’s Law.

assert property(@posedge clk !$rose(a) |-> b);