| Safe Haskell | None |
|---|---|
| Language | GHC2024 |
Proarrow.Category.Instance.Circuit
Description
Synchronous digital circuits. The tensor preserves the grouping of bit bundles; copying is
fan-out, and tracing connects wires without adding a delay. register delays a bit by one
clock cycle. prepare rejects observable combinational cycles before simulation.
>>>simulate notGate [False, True]Right [True,False]>>>simulate (register False) [True, False, True]Right [False,True,False]
Synopsis
- data Wires
- class Is 'Sim (Value @ 'Ready a) => KnownWires (a :: Wires)
- data family Value :: PREPARED +-> SIMULATOR
- type Sample (a :: Wires) = UN 'Sim (Value @ 'Ready a)
- data PREPARED = Ready Wires
- data Prepared (a :: PREPARED) (b :: PREPARED)
- data Circuit (a :: Wires) (b :: Wires)
- constant :: Bool -> 'Empty ~> 'Bit
- notGate :: 'Bit ~> 'Bit
- andGate :: ('Bit ** 'Bit) ~> 'Bit
- orGate :: ('Bit ** 'Bit) ~> 'Bit
- xorGate :: ('Bit ** 'Bit) ~> 'Bit
- mux :: (('Bit ** 'Bit) ** 'Bit) ~> 'Bit
- register :: Bool -> 'Bit ~> 'Bit
- data Netlist (a :: Wires) (b :: Wires)
- netlist :: forall (a :: Wires) (b :: Wires). Circuit a b -> Netlist a b
- renderNetlist :: forall (a :: Wires) (b :: Wires). Netlist a b -> String
- toDot :: forall (a :: Wires) (b :: Wires). Netlist a b -> String
- toVerilog :: forall (a :: Wires) (b :: Wires). String -> Netlist a b -> Either CircuitError String
- newtype CircuitError = CombinationalCycle [Int]
- data Simulator (a :: SIMULATOR) (b :: SIMULATOR)
- prepare :: forall (a :: Wires) (b :: Wires). Netlist a b -> Either CircuitError (Prepared ('Ready a) ('Ready b))
- step :: Simulator ('Sim a) ('Sim b) -> a -> (b, Simulator ('Sim a) ('Sim b))
- simulate :: forall (a :: Wires) (b :: Wires). Circuit a b -> [Sample a] -> Either CircuitError [Sample b]
Documentation
A bit, no wires, or two bundles. Tensor grouping is retained in the type.
Instances
class Is 'Sim (Value @ 'Ready a) => KnownWires (a :: Wires) Source Github #
Minimal complete definition
shape
Instances
| KnownWires 'Bit Source Github # | |
Defined in Proarrow.Category.Instance.Circuit | |
| KnownWires 'Empty Source Github # | |
Defined in Proarrow.Category.Instance.Circuit | |
| (KnownWires a, KnownWires b) => KnownWires ('Pair a b) Source Github # | |
Defined in Proarrow.Category.Instance.Circuit | |
data family Value :: PREPARED +-> SIMULATOR Source Github #
Interpret validated circuits as state machines. Bits become Bool, the unit becomes (),
and a tensor becomes a pair, all in the SIMULATOR category.
Instances
| FunctorForRep Value Source Github # | |
| MonoidalProfunctor (Rep Value) Source Github # | |
| type Value @ ('Ready 'Bit) Source Github # | |
| type Value @ ('Ready 'Empty) Source Github # | |
| type Value @ ('Ready ('Pair a b) :: PREPARED) Source Github # | |
type Sample (a :: Wires) = UN 'Sim (Value @ 'Ready a) Source Github #
The Haskell value for one clock cycle at a wire shape.
Objects of validated circuits, with the same wire shapes as Wires.
Instances
| Monoidal PREPARED Source Github # | |||||||||
Defined in Proarrow.Category.Instance.Circuit Associated Types
Methods withOb2 :: forall (a :: PREPARED) (b :: PREPARED) r. (Ob a, Ob b) => (Ob (a ** b) => r) -> r Source Github # leftUnitor :: forall (a :: PREPARED). Ob a => ((Unit :: PREPARED) ** a) ~> a Source Github # leftUnitorInv :: forall (a :: PREPARED). Ob a => a ~> ((Unit :: PREPARED) ** a) Source Github # rightUnitor :: forall (a :: PREPARED). Ob a => (a ** (Unit :: PREPARED)) ~> a Source Github # rightUnitorInv :: forall (a :: PREPARED). Ob a => a ~> (a ** (Unit :: PREPARED)) Source Github # associator :: forall (a :: PREPARED) (b :: PREPARED) (c :: PREPARED). (Ob a, Ob b, Ob c) => ((a ** b) ** c) ~> (a ** (b ** c)) Source Github # associatorInv :: forall (a :: PREPARED) (b :: PREPARED) (c :: PREPARED). (Ob a, Ob b, Ob c) => (a ** (b ** c)) ~> ((a ** b) ** c) Source Github # | |||||||||
| SymMonoidal PREPARED Source Github # | |||||||||
| CopyDiscard PREPARED Source Github # | |||||||||
| CategoryOf PREPARED Source Github # | |||||||||
Defined in Proarrow.Category.Instance.Circuit Associated Types
| |||||||||
| Promonad Prepared Source Github # | |||||||||
| Ob a => CocommutativeComonoid (a :: PREPARED) Source Github # | |||||||||
Defined in Proarrow.Category.Instance.Circuit | |||||||||
| Ob a => Comonoid (a :: PREPARED) Source Github # | |||||||||
| MonoidalProfunctor Prepared Source Github # | |||||||||
| Profunctor Prepared Source Github # | |||||||||
Defined in Proarrow.Category.Instance.Circuit Methods dimap :: forall (c :: PREPARED) (a :: PREPARED) (b :: PREPARED) (d :: PREPARED). (c ~> a) -> (b ~> d) -> Prepared a b -> Prepared c d Source Github # lmap :: forall (c :: PREPARED) (a :: PREPARED) (b :: PREPARED). (c ~> a) -> Prepared a b -> Prepared c b Source Github # rmap :: forall (b :: PREPARED) (d :: PREPARED) (a :: PREPARED). (b ~> d) -> Prepared a b -> Prepared a d Source Github # (\\) :: forall (a :: PREPARED) (b :: PREPARED) r. ((Ob a, Ob b) => r) -> Prepared a b -> r Source Github # | |||||||||
| FunctorForRep Value Source Github # | |||||||||
| MonoidalProfunctor (Rep Value) Source Github # | |||||||||
| type Unit Source Github # | |||||||||
Defined in Proarrow.Category.Instance.Circuit | |||||||||
| type (~>) Source Github # | |||||||||
Defined in Proarrow.Category.Instance.Circuit | |||||||||
| type Ob (a :: PREPARED) Source Github # | |||||||||
Defined in Proarrow.Category.Instance.Circuit | |||||||||
| type (a :: PREPARED) ** (b :: PREPARED) Source Github # | |||||||||
| type Value @ ('Ready 'Bit) Source Github # | |||||||||
| type Value @ ('Ready 'Empty) Source Github # | |||||||||
| type Value @ ('Ready ('Pair a b) :: PREPARED) Source Github # | |||||||||
data Prepared (a :: PREPARED) (b :: PREPARED) Source Github #
A circuit that passed combinational-cycle validation, carrying its current simulation state. Composition and tensor preserve validity; unrestricted trace is available only before validation.
Instances
| Promonad Prepared Source Github # | |
| MonoidalProfunctor Prepared Source Github # | |
| Profunctor Prepared Source Github # | |
Defined in Proarrow.Category.Instance.Circuit Methods dimap :: forall (c :: PREPARED) (a :: PREPARED) (b :: PREPARED) (d :: PREPARED). (c ~> a) -> (b ~> d) -> Prepared a b -> Prepared c d Source Github # lmap :: forall (c :: PREPARED) (a :: PREPARED) (b :: PREPARED). (c ~> a) -> Prepared a b -> Prepared c b Source Github # rmap :: forall (b :: PREPARED) (d :: PREPARED) (a :: PREPARED). (b ~> d) -> Prepared a b -> Prepared a d Source Github # (\\) :: forall (a :: PREPARED) (b :: PREPARED) r. ((Ob a, Ob b) => r) -> Prepared a b -> r Source Github # | |
data Circuit (a :: Wires) (b :: Wires) Source Github #
A typed circuit builder. Constructors are hidden so every output bit has one driver.
Instances
| Promonad Circuit Source Github # | |
| MonoidalProfunctor Circuit Source Github # | |
| Profunctor Circuit Source Github # | |
Defined in Proarrow.Category.Instance.Circuit Methods dimap :: forall (c :: Wires) (a :: Wires) (b :: Wires) (d :: Wires). (c ~> a) -> (b ~> d) -> Circuit a b -> Circuit c d Source Github # lmap :: forall (c :: Wires) (a :: Wires) (b :: Wires). (c ~> a) -> Circuit a b -> Circuit c b Source Github # rmap :: forall (b :: Wires) (d :: Wires) (a :: Wires). (b ~> d) -> Circuit a b -> Circuit a d Source Github # (\\) :: forall (a :: Wires) (b :: Wires) r. ((Ob a, Ob b) => r) -> Circuit a b -> r Source Github # | |
| Costrong (Tensor :: Wires -> (Wires, Wires) -> Type) Circuit Source Github # | |
mux :: (('Bit ** 'Bit) ** 'Bit) ~> 'Bit Source Github #
Select the second input when the first is true, and the third when it is false.
register :: Bool -> 'Bit ~> 'Bit Source Github #
A register's output starts at the given value. Each clock edge replaces it with its input from the preceding cycle. All registers update simultaneously.
data Netlist (a :: Wires) (b :: Wires) Source Github #
A netlist with typed boundaries. Disconnected components are omitted.
netlist :: forall (a :: Wires) (b :: Wires). Circuit a b -> Netlist a b Source Github #
Build a netlist, retaining precisely the components that can influence an output, including through a register on a later cycle.
renderNetlist :: forall (a :: Wires) (b :: Wires). Netlist a b -> String Source Github #
A text netlist. Bit numbers are local to this netlist; bundle ports are ordered left to right.
toDot :: forall (a :: Wires) (b :: Wires). Netlist a b -> String Source Github #
A Graphviz graph of the same netlist used by the simulator. Register nodes show their initial value. Copying is fan-out of an edge, and feedback aliases are small connection points.
toVerilog :: forall (a :: Wires) (b :: Wires). String -> Netlist a b -> Either CircuitError String Source Github #
Verilog with scalar ports in0, in1, ... and out0, out1, ... in bundle order,
and a shared rising-edge clock clk. The caller supplies a valid Verilog module name.
Combinational cycles are rejected, and disconnected components are omitted.
Registers use initial assignments to preserve their starting values in simulation;
synthesis support for initialization depends on the hardware target.
newtype CircuitError Source Github #
Bits participating in a combinational cycle. Every observable cycle must cross a register.
Constructors
| CombinationalCycle [Int] |
Instances
| Show CircuitError Source Github # | |
Defined in Proarrow.Category.Instance.Circuit | |
| Eq CircuitError Source Github # | |
Defined in Proarrow.Category.Instance.Circuit Methods (==) :: CircuitError -> CircuitError -> Bool Github # (/=) :: CircuitError -> CircuitError -> Bool Github # | |
data Simulator (a :: SIMULATOR) (b :: SIMULATOR) Source Github #
A machine and its current state, represented by its next step.
Instances
| Promonad Simulator Source Github # | |
| MonoidalProfunctor Simulator Source Github # | |
Defined in Proarrow.Category.Instance.Simulator | |
| Profunctor Simulator Source Github # | |
Defined in Proarrow.Category.Instance.Simulator Methods dimap :: forall (c :: SIMULATOR) (a :: SIMULATOR) (b :: SIMULATOR) (d :: SIMULATOR). (c ~> a) -> (b ~> d) -> Simulator a b -> Simulator c d Source Github # lmap :: forall (c :: SIMULATOR) (a :: SIMULATOR) (b :: SIMULATOR). (c ~> a) -> Simulator a b -> Simulator c b Source Github # rmap :: forall (b :: SIMULATOR) (d :: SIMULATOR) (a :: SIMULATOR). (b ~> d) -> Simulator a b -> Simulator a d Source Github # (\\) :: forall (a :: SIMULATOR) (b :: SIMULATOR) r. ((Ob a, Ob b) => r) -> Simulator a b -> r Source Github # | |
prepare :: forall (a :: Wires) (b :: Wires). Netlist a b -> Either CircuitError (Prepared ('Ready a) ('Ready b)) Source Github #
Cut the dependencies through registers and topologically order the combinational nodes. Multiplexers depend on both data inputs, even when their selector is constant.