(* always_ready, always_enabled *)
interface TopIfc;
  method Action   sw  (Bit#(4) val);
  method Bit#(4)  led ();
endinterface

(* synthesize *)
module hello_world (TopIfc);
  Reg#(Bit#(26)) counter <- mkRegU;

  Wire#(Bit#(4)) w_sw <- mkBypassWire;

  (* fire_when_enabled, no_implicit_conditions *)
  rule incr_counter;
    counter <= counter + 1;
  endrule

  method Action sw (Bit#(4) val);
    w_sw <= val;
  endmethod

  method Bit#(4) led();
    return { w_sw[3:1], counter[25] };
  endmethod
endmodule

package HelloWorld where

interface TopIfc {-# always_enabled , always_ready  #-} =
    sw :: Bit 4 -> Prelude.Action {-# arg_names = [val] #-};
    led :: Bit 4

{-# properties hello_world = { synthesize } #-}

hello_world :: Module TopIfc
hello_world =
  module
    counter :: Reg (Bit 26) <- mkRegU
    w_sw :: Wire (Bit 4) <- mkBypassWire

    rules
      {-# ASSERT fire when enabled #-}
      {-# ASSERT no implicit conditions #-}
      "incr_counter":
        when True ==> counter := counter + 1

    interface
      sw val = w_sw := val
      led = w_sw[3:1] ++ counter[25:25]