Write the assertions to verify the functionality of D flip-flop with asynchronous reset

Write the assertions to verify the functionality of D flip-flop with asynchronous reset.

Please help me out with this answer.

In reply to @jpk4pj:

Give it a first cut for your homework; I’ll check it out for you, or better yet, write a testbench and check it out yourself.
:)
Ben

In reply to @jpk4pj:
HINT : Just remember the basic thing that Q(output) will always be one cycle delayed version of D (input captured at posedge of clk ) ,you can use non overlapping implication operator for this