Implementation status (TBD)¶
Most of Pyrope is implemented in LiveHD
and exercised by its test suite. This page lists the documented features that
are not implemented yet; each is also marked "TBD" where it is described.
A feature on this list may parse (lhd elaborate is permissive) but does not
lower to working hardware.
Each feature has a matching task page (with a failing example) in the LiveHD
repo under todo/.
| Feature | Documented in | Task | Notes |
|---|---|---|---|
fluid lambdas, valid/retry/fire elastic handshakes |
Fluid Blocks | 2f-fluid |
syntax parses; no lowering |
Temporal library: past(x, n), rose, fell, stable, changed, eventually(x, w), always(x, w) |
Extended Verification | 2f-temporal |
positional args only — there is no f[N](x) bracket form. The pipelining past[N](x) DOES work (design body only) and is a different operator. No edge attributes: .[rising]/.[falling]/.[changed]/.[stable] are not recognized. lhd formal verify must reject these calls with an explicit "not implemented" diagnostic |
Testbench extras: string sigref (arbitrary-path), force/release, cpp(...) external models, unbounded tick { } |
Extended Verification | 2f-testbench |
the instance/step/poke-peek model + if/continue waiting + if-block monitors run via lhd sim; string peek/poke work; waitfor/spawn/join/cancel are dropped (replaced by that idiom) |
regref (register reference through the instance hierarchy) |
Verification, Type system | 2f-testbench |
not needed for assert/assume: verification code reaches signals through the ordinary instance hierarchy |
Statements rejected inside a test block: for loops, .[rand]/.[crand], past[N], positional instantiation-by-call |
Testing | 2f-test_syntax |
dotted names, runtime (...) params, tick/step/break/continue, and field + string poke/peek all work |
Standard library (import("prp")) |
Standard Library | 2f-stdlib |
wish-list chapter |
macro= memory-compiler binding |
Memories | 2f-macro |
|
cover, covercase, in-language lec()/lec_valid() |
Assertions | 2f-verif_extras |
assert/cassert/assume/assert_always work; cover does NOT exist in any context |
.[rand] / .[crand] random generation |
Random | 2f-verif_extras |
rejected in test blocks and design bodies; survives only where it constant-folds |
assert.[failed] (read/clear the accumulated failure flag in a test) |
Test | 2f-verif_extras |
|
always_assert / always_cassert / always_assume / always_cover / always_covercase; valid-based (.[valid]) gating of checks |
Reset and verification | 2f-verif_extras |
the implemented spelling is assert_always; no valid-based gating exists |
Generics: body references of a generic name (T(a), mut tmp:T, a + N, F(v=a)), constant/lambda-valued generics, defaults <T, N=4>, named <T=…> bindings |
Functions | 3g |
signature :T binding works: explicit f<u8>(…), inference, mod/pipe specialization |
Input default values (comb f(in1:u4, in2=3), tuple-scope b:signed=a+5) |
Functions, Variables | 3g |
omitting a defaulted input errors fcall-missing-arg today |
Notes:
requires/ensureswere removed from the language. They parse today only to emit a "no obligation generated" warning; write anassumefor a precondition and anassertfor a postcondition.- A design-body
assertis checked bypass.formaland emitted into the Verilog netlist, but is not executed bylhd sim— the simulation runtime fallback is pending. Only assertions written inside atestblock are checked at simulation time. - A verification statement does not inherit an enclosing
ifguard:if c { assert(x) }is lowered as an unconditionalassert(x). Useassert(c implies x). - A refutable
assumeover free inputs is a hard build error at the top module and a deferred runtime check in an instantiated one. - Runtime
wrap/satlowering and enum-typed register resets are implemented (earlier limitations, since fixed). - Glob import patterns were removed from the language: the import string is
"file"or"file.pub_name"only (see import). - The comptime
[...]test-parameter sweep (one test instance per swept value, the planned replacement for thefor { test ... }fan-out idiom) is reserved but not yet specified.