Sockets

Sockets are a way for Virdant modules to expose a set of ports as a named group. You may connect all the ports together in a single bidirectional assignment, rather than wiring each port individually.

Socket Definitions

A socket definition is a top-level declaration that names a group of ports with their types and directions.

SocketDef :=
    DocString? Annotations "pub"? "socket" Ident Generics? "{" SocketDefStmt* "}"

SocketDefStmt :=
    DocString? Annotations "cosi" Ident ":" Type
    | DocString? Annotations "soci" Ident ":" Type

socket Mem {
    cosi addr : Word[16]
    soci data : Word[8]
}

The direction keywords have the following meanings, from the perspective of a client socket instance:

cosi: Client-Out, Server-In. For a client instance, this port is an output. For a server instance, this port is an input.
soci: Server-Out, Client-In. For a client instance, this port is an input. For a server instance, this port is an output.

Thus cosi ports are driven by the client and received by the server, while soci ports are driven by the server and received by the client.

Generic Socket Definitions

A socket definition may declare generic parameters, exactly like type and module definitions (see Types). The parameters are a comma-separated name : kind list in square brackets after the socket name, and the parameter names are in scope in the channel types of the body:

socket Bus[T : Type] {
    cosi req : T
    soci rsp : T
}

Both channels of Bus have type T. The definition is analyzed once, generically, with the parameters unbound; concrete channel types exist only per instantiation, which supplies the actual types (see Type Arguments below).

Socket Instances

Socket instances are declared inside module bodies. Each instance must specify its role: client or server.

ModDefStmtSocket :=
    DocString? Annotations "client" "socket" Ident "of" Ofness GenericsParams? ItBlock?
    | DocString? Annotations "server" "socket" Ident "of" Ofness GenericsParams? ItBlock?

mod Core {
    client socket mem of Mem
    unused mem.data
    mem.addr := 0
}

mod Memory {
    server socket mem of Mem
    unused mem.addr
    mem.data := 10
}

A client socket instance uses cosi ports as outputs (driven by the client) and soci ports as inputs (received by the client). A server socket instance reverses these directions.

Type Arguments

An instance of a generic socket supplies type arguments after the socket definition name, in square brackets and in the same order as the declared parameters:

mod Master {
    incoming d : Word[8]
    client socket bus of Bus[Word[8]] {
        it.req := d
    }
    unused bus.rsp
}

mod Slave {
    server socket bus of Bus[Word[8]] {
        it.rsp := it.req
    }
}

The channel types of the instance are the definition’s channel types with the arguments substituted: both bus.req and bus.rsp have type Word[8] in the examples above, so Slave may assign it.rsp straight from it.req.

The arguments are checked at the instantiation site: a Type parameter takes a type expression and a Nat parameter a number literal, in exactly the number declared. Instantiating the builtin Pipe with no arguments:

client socket p of Pipe

reports Type builtin::Pipe takes 1 type argument, but 0 were given. Instantiating Bus at a number:

client socket bus of Bus[8]

reports Type argument mismatch: parameter T of Bus expects a type, but found a Nat literal.

Bidirectional Connections

A pair of socket instances (one client, one server) may be connected bidirectionally using the :=: operator. This connects every port in the socket at once, with the appropriate direction for each instance.

mod Top {
    mod core of Core
    mod memsrv of Memory

    memsrv.mem :=: core.mem
}

The :=: operator connects every port in the Mem socket between the core and memsrv instances. The addr port is driven by core and received by memsrv. The data port is driven by memsrv and received by core.

This is equivalent to manually wiring each port:

memsrv.mem.addr := core.mem.addr
core.mem.data := memsrv.mem.data

Mono-Socket Matching

When the connected sockets are generic, :=: matches on the mono socket: the socket definition together with its type arguments. A connection joins two instances of the same socket definition instantiated at the same type arguments. Two instances of the same socket definition at different arguments are different mono sockets and do not connect.

The arguments written at a socket instantiation inside a generic module compose with the arguments of the enclosing module instances:

mod Master[W : Type] {
    incoming d : W
    client socket bus of Bus[W] {
        it.req := d
    }
    unused bus.rsp
}

mod Slave[W : Type] {
    server socket bus of Bus[W] {
        it.rsp := it.req
    }
}

pub mod Top {
    incoming inp : Word[8]

    mod master of Master[Word[8]] {
        it.d := inp
    }
    mod slave of Slave[Word[8]] {
        master.bus :=: it.bus
    }

    outgoing out : Word[8]
    out := slave.bus.rsp
}

master.bus instantiates Bus at W, and the instance master supplies Word[8] for W, so master.bus is the mono socket Bus[Word[8]] — and so is it.bus inside slave’s it-block. The connection therefore checks. Connections written inside a module instance’s it-block are checked the same way: it resolves to the instance, and the instance’s arguments compose with the socket’s.

A mismatch is an error whose diagnostic names both instantiations and points at the connection. If master’s socket instantiates Link[Word[8]] while slave’s instantiates Link[Word[9]]:

slave.pipe :=: master.pipe

reports:

Cannot connect Link[Word[9]] to Link[Word[8]]: mismatched socket instantiations

Accessing Socket Ports

Individual ports on a socket instance are accessed through a two-level path:

<instance>.<socket_instance>.<port>

core.mem.addr := 0
result := memsrv.mem.data

The first component is the module instance name, the second is the socket instance name, and the third is the port name within the socket definition.

Sockets as Interfaces

Sockets are useful for defining standard bus interfaces that can be reused across multiple modules.

For example, a TileLink UL interface or a Wishbone bus can be defined as a socket and then instantiated by any module that speaks that protocol.

socket TileLinkUL {
    cosi a_address  : Word[32]
    cosi a_opcode   : Word[3]
    cosi a_size     : Word[2]
    cosi a_data     : Word[32]
    cosi a_mask     : Word[4]
    soci d_data     : Word[32]
    soci d_opcode   : Word[3]
    soci d_size     : Word[2]
}

By defining the interface as a socket, the compiler can verify that all connections are complete and correctly oriented.

Builtin Sockets

Virdant ships a single builtin socket, in the builtin package of the standard library (lib/builtin.vir): Pipe[T], a ready/valid handshake channel.

pub socket Pipe[T : Type] {
    cosi data  : Valid[T]
    soci ready : Bit
}

The two ports form a handshake pair:

cosi data : Valid[T] — the payload. @Valid(v) carries a value v of type T, while @Invalid() marks the pipe as empty. The client drives data and the server receives it.
soci ready : Bit — readiness. The server drives ready and the client receives it.

A client socket instance of Pipe[T] therefore drives data and reads ready, while a server socket instance reads data and drives ready.

Like any generic socket, Pipe[T] is instantiated with explicit type arguments, e.g. of Pipe[Word[8]]. And like everything in the builtin package, it is loaded implicitly by every design: no import is needed, and builtin items are referenced unqualified. The name builtin is a keyword, so it cannot be written as a package qualifier: builtin::Pipe[...] is not valid Virdant.

A Producer/Consumer Pair

The example below is a compact end-to-end pair over Pipe[Word[8]]: a producer drives a Valid payload into its end of the pipe, a consumer asserts readiness, and a top module connects the two with :=:.

// A producer: pushes a Valid payload into its end of the pipe.
mod Producer {
    // The payload the producer pushes into the pipe.
    incoming d : Word[8]

    client socket pipe of Pipe[Word[8]] {
        it.data := @Valid(d)
    }

    // The consumer's readiness, received back through the pipe.
    outgoing ready : Bit
    ready := pipe.ready
}

// A consumer: asserts readiness and forwards the received payload.
mod Consumer {
    server socket pipe of Pipe[Word[8]] {
        it.ready := true
    }

    // The payload received from the producer.
    outgoing data : Valid[Word[8]]
    data := pipe.data
}

pub mod Top {
    incoming d : Word[8]

    mod producer of Producer {
        it.d := d
    }
    mod consumer of Consumer

    consumer.pipe :=: producer.pipe

    // The consumer's readiness flows back to the producer through the pipe.
    outgoing ready : Bit
    ready := producer.ready

    // The producer's payload, unwrapped where the argument is concrete.
    outgoing valid : Bit
    outgoing data : Word[8]
    valid := match consumer.data {
        with @Valid(dontcare) => true
        with @Invalid() => false
    }
    data := match consumer.data {
        with @Valid(payload) => payload
        with @Invalid() => 0
    }
}

The :=: connection joins the two socket instances port by port: the producer’s @Valid(d) payload appears on the consumer’s pipe.data, and the consumer’s readiness flows back to the producer’s pipe.ready.

The dependson List on Channels

A socket channel may carry a dependson list, naming channels of the opposite direction word of the same socket:

socket Wishbone {
    cosi cyc : Bit
    cosi stb : Bit
    soci ack : Bit dependson cyc, stb
}

When the socket is instantiated in the channel’s driving role (client for cosi channels, server for soci channels), the list places the same obligation on the containing module as if the dependson were declared on the resulting port: the module’s drive on that channel may combinationally depend on its reads of the listed channels. In the receiving role the list is inert.

Unlike dependson on module ports, a socket channel’s list never produces an unused warning when the drive does not exercise it: protocols such as Wishbone and TileLink support same-cycle responses but also arbitrary delays, so the declared potential may legitimately stay dormant. It is still part of the contract: the containing module must not drive the channel with anything outside the declared set, and cycles in the composed dependson relation (for example, both sides of a link declaring same-cycle responses) are errors. See Modules.