Binding Multiclock Domain Assertion

///////////////////////////////////////////////////////////
/////////////////// DFF module/////////////////////
///////////////////////////////////////////////////////////
module dff(
           input wire din,clk,rstn,
           output reg qout
          );
         
always@(posedge clk,negedge rstn)
  begin
    if(~rstn)
      qout<=0;
    else
      qout<=din;
  end
endmodule

///////////////////////////////////////////////////////////
/////////////////// DUT module////////////////////
///////////////////////////////////////////////////////////
module DUT (
            input rst1,rst2,clk1,clk2,in1,in2,in3,
            output  out
           );  

  wire qout1,qout2,and_out;

  dff dff1(.din(in1),.clk(clk1),.rstn(rst1),.qout(qout1));  
  assign and_out=qout1 & in2;

  dff dff2(.din(and_out),.clk(clk2),.rstn(rst2),.qout(qout2));  
  assign out=qout2 | in3;          

endmodule

///////////////////////////////////////////////////////////
/////////////////// ASSERTION Module////////
///////////////////////////////////////////////////////////
module dut_assertions(
                      input  wire rst1,rst2,clk1,clk2,in1,in2,in3,out
            );
reg val1,val2,val3;
 
 //sequence seq1(val1,val2); 
  //@(posedge clk1)
  //(1'b1,val1=in1) ##0(1'b1,val2=in2);
 //endsequence

  sequence seq1;
   (1,assign12_t);
  endsequence

 //sequence seq2(val3);
  //@(posedge clk2)
  //(1'b1,val3=in3);
 //endsequence

  sequence seq2;
   (1,assign3_t);
  endsequence

//property p(val1,val2,val3);
 //(@(posedge clk1) disable iff (!rst1) (rst1 throughout seq1(val1,val2))) |->  (@(posedge clk2) disable iff (!rst2) (rst2 throughout seq2(val3)));
//endproperty

  property p;
    (@(posedge clk1)  (rst1 throughout seq1)) ##1  (@(posedge clk2) (rst2 throughout seq2));
  endproperty

//assert property (p(val1,val2,val3))  begin
  assert property (p)  begin
///////////////////////////////////////////////////////////
//// Assertion Action Block Verifying DUT functionality////
///////////////////////////////////////////////////////////
  case({val1,val2,val3})
    3'b000,3'b010,3'b100 :
       begin
         if(!out)
           $display("DUT check passed for %b Out1=%b",{val1,val2,val3},out);
         else
           $error("DUT check failed for %b Out1=%b",{val1,val2,val3},out);    
       end
    3'b001,3'b011,3'b101,3'b110,3'b111 :
       begin
         if(out)
           $display("DUT check passed for %b Out2=%b",{val1,val2,val3},out);
         else
           $error("DUT check failed for %b Out2=%b",{val1,val2,val3},out);    
        end
   endcase
end
else  begin
  $error("Assertion failed");    
end
/////////////////////////////////////////////////////////////
////// Task holding values of in1 and in2////
/////////////////////////////////////////////////////////////
 task assign12_t;
   $display($time,"val1:%b ,val2:%b ,val3:%b",in1,in2,in3);
   val1=in1;
   val2=in2;  
 endtask
/////////////////////////////////////////////////////////////////
//////// Task holding values of in3 /////////////////
//////////////////////////////////////////////////////////////////
 task assign3_t;
   $display($time,"val1:%b, val2:%b ,val3:%b",in1,in2,in3);
   val3=in3;  
 endtask
   
endmodule
 
/////////////////////////////////////////////////////////////////////////
/////Binding DUT and ASSERTION Module//////////
//////////////////////////////////////////////////////////////////////////
module bind_assertion ();
  //bind DUT dut_assertions DUT_ASSERT(.rst1(rst1),.rst2(rst2),.clk1(clk1),.clk2(clk2),.in1(in1),.in2(in2),.in3(in3),.out(out));
  bind DUT dut_assertions DUT_ASSERT(.*);

endmodule


///////////////////////////////////////////////////////////////////////////
////////////////// DUT TEST MODULE ////////////////////////
///////////////////////////////////////////////////////////////////////////
module test;
  reg rst1,rst2,clk1,clk2,in1,in2,in3;
  wire out;              

  DUT dut_inst(.rst1(rst1),.rst2(rst2),.clk1(clk1),.clk2(clk2),.in1(in1),.in2(in2),.in3(in3),.out(out));
  //DUT dut_inst(.*);

always #5 clk1=~clk1;
always #10 clk2=~clk2;

initial begin
  clk1=0;clk2=0;
  rst1=1;rst2=1;
  in1=0;in2=1;in3=1;
  #10 rst2=0;

  #15 rst2=1;
  #10 rst1=0;
  #15 rst1=1;
  in1=0;in2=0;in3=0;
  #50 $finish;
end    
endmodule