Module Circuit


module Circuit: sig .. end
Intermediate circuit representation.


type circuit =
| Circuit of id * string * circuit list * signal list
* sink list
type width = int 
type id = int 

type signal =
| Signal_input of id * string * width
| Signal_signal of id * string * width * signal Pervasives.ref
| Signal_const of id * string (*TODO: support 123, b1100, habcd*)
| Signal_empty of id (*0 width signal.*)
| Signal_select of id * int * int * signal (*msb, lsb: msb must be greater than lsb*)
| Signal_concat of id * signal * signal
| Signal_not of id * signal
| Signal_and of id * signal * signal
| Signal_xor of id * signal * signal
| Signal_or of id * signal * signal
| Signal_eq of id * signal * signal
| Signal_lt of id * signal * signal
| Signal_add of id * signal * signal
| Signal_sub of id * signal * signal
| Signal_mul_u of id * signal * signal
| Signal_mul_s of id * signal * signal
| Signal_mux of id * signal * signal * signal (*sel, high, low*)
| Signal_reg of id * signal * signal (*enable, data*)

type sink =
| Sink_output of id * string * signal
| Sink_assert of id * string * property
| Sink_assume of id * string * property
| Sink_cover of id * string * sequence

type sequence =
| Sequence_signal of signal
| Sequence_and of sequence * sequence
| Sequence_concat of sequence * sequence
| Sequence_infuse of sequence * sequence
| Sequence_altern of sequence * sequence
| Sequence_repeat of sequence
| Sequence_null

type property =
| Property_signal of signal
| Property_not of property
| Property_and of (property * property)
| Property_imply of (property * property)
| Property_always of property
| Property_sequence of sequence
| Property_sequence_weak of sequence
| Property_until_weak of (property * property)
| Property_if_sequence of sequence * property
module Signal_set: Set.S  with type elt = signal
Signal sets.
module Signal_map: Map.S  with type key = signal
Maps with signals for keys.
module Sink_map: Map.S  with type key = sink
Maps with sink for keys.
val string_of_signal : signal -> string
String of a signal.
val id_of_circuit : circuit -> id
ID of a circuit.
val id_of_signal : signal -> id
ID of a signal.
val id_of_sink : sink -> id
ID of a sink.
val width : signal -> int
Width of a signal.
val all_signals : circuit -> signal list
A list of all signals in a circuit.
val order_signals_sequential : circuit -> signal list
Topologically orders all signals. Fails if design contains a combinational loop.
val order_signals_description : circuit -> signal list
Topologically ordered based on description. Signal_signal takes precedent.
val all_sinks : circuit -> sink list
A list of all sinks in a circuit.
val psl_of_sequence : (signal -> string) -> sequence -> string
PSL code of a sequence.
val psl_of_property : (signal -> string) -> property -> string
PSL code of a property.