interface t_if(input logic clk); 
  logic a, b, c;
  wire f,g; 
  modport slave_mp (output c,   
                    input a, b);
//   modport master_mp (
//     output a, b, f, g, 
//     input c);

  initial $display("within interface %b", c);
  assign  f=!a;
  assign  g= a && b;
  ap_abc_if: assert property(@ (posedge clk) a && b |=> c);

  task randomize_ab(input logic x, y, // demo
					output logic a, b);
	logic w, z;
	w=x; z=y;
	ap_rdnmz2: assert(randomize(w, z));
	a=w; b=z;
  endtask : randomize_ab
endinterface : t_if

module dut(input logic clk, t_if.slave_mp slv_if);
  always @ (posedge clk)
	slv_if.c <= slv_if.a && slv_if.b;
  ap_abc_dut: assert property(@ (posedge clk) 
         slv_if.a && slv_if.b |=> slv_if.c);
  
endmodule : dut 

// ** USING A MODULE TO EMULATE A CHECKER 
//checker  chk_m(input event e, t_if.mavlog ster_mp  k_if);
module  chk_m(input event e, t_if  k_if);  // replace "module" with "checker" 
  logic a=0, b=0, c;
  logic r=0, s=0;
  always @ (e) k_if.a <= a;   
  always @ (e) k_if.b <= b;
  always @ (e) begin : always1
    // ap_rdnmz: assert(randomize(a, b));
	k_if.randomize_ab( r, s, 
					     a, b);
  end : always1
  ap_abc_OK: assert property(@e k_if.a && k_if.b |=> k_if.c);   
endmodule  : chk_m


module top;
  logic clk =1'b1;
  t_if t_if1(clk);
  event  e1;                          // Needed for simulation when "checker" is "module"
  always @ (posedge clk)  -> e1;      // ""
  initial forever #10 clk=!clk;
  dut dut1(.clk(clk), .slv_if(t_if1));
  chk_m chk_m1(.e(e1), .k_if(t_if1));   // <-- checker instantiation 

endmodule : top