interface t_if(input logic clk); 
  wire a, b, c;
  bit f,g; // temps 

  clocking slv_cb @ (posedge clk);
    inout c;  // clocking block outputs can't be "read", must use inout 
    input a, b;
  endclocking : slv_cb
  modport slave_mp (clocking slv_cb);
  
  clocking mstr_cb @ (posedge clk);
    inout a, b, f, g;  // clocking block outputs can't be "read", must use inout 
    input c;
  endclocking : mstr_cb
  modport master_mp (clocking mstr_cb);

  initial $display("within interface %b", c);
  // always @ (posedge clk)  $display("within always @ (posedge clk) interface %b", c);
//   task tk();
// 	ap_rdnmz2: assert(randomize(f, g));
//   endtask : tk

  ap_abc_if: assert property(@ (posedge clk) a && b |=> c);
endinterface : t_if

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

// ** USING A MODULE TO EMULATE A CHECKER 
//checker  chk_m(input event e, t_if.master_mp  k_if);
module  chk_m(input event e, t_if.master_mp  k_if);  // replace "module" with "checker" 
  logic a=0, b=0, c;
  always @ (e) k_if.mstr_cb.a <= a;   // line 31 
  always @ (e) k_if.mstr_cb.b <= b;
  // always @ (e) k_if.mstr_cb.b <= k_if.g;
  always @ (e) begin : always1
    ap_rdnmz: assert(randomize(a, b));
	// k_if.tk();
  end : always1
  ap_abc_INCORRECT: assert property(@e a && b |=> k_if.mstr_cb.c);
  ap_abc_OK: assert property(@e k_if.mstr_cb.a && k_if.mstr_cb.b |=> k_if.mstr_cb.c);   // line 36 
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