Vl-time
Representation of time amounts like 45.12ns.
This is a product type, introduced by deftagsum in support of vl-value.
Fields
- quantity — stringp
- An ACL2 string with the amount. In practice, the amount should
match either unsigned_number or fixed_point_number,
e.g., "3" or "45.617". We don't try to process
this further because (1) we don't expect it to matter for much,
and (2) ACL2 doesn't really support fixed point numbers.
- units — vl-timeunit-p
- The kind of time unit this is, e.g., seconds, milliseconds,
microseconds, ...
We barely support this. You should probably not rely on our
current representation, since we will almost certainly want to change
it as soon as we do anything with time units.
Subtopics
- Vl-time->units
- Get the units field from a vl-time.
- Vl-time->quantity
- Get the quantity field from a vl-time.
- Make-vl-time
- Basic constructor macro for vl-time structures.
- Change-vl-time
- Modifying constructor for vl-time structures.
- Vl-timeunit
- Representation for SystemVerilog time units (s, ms, ps, ...).
