		Search-engine friendly clone of the ACL2 documentation.

Syntax

Vl-gatestrength

Representation of strengths for a assignment statements, gate instances, and module instances.

This is a product type introduced by defprod.

Fields

zero — vl-dstrength-p: Drive strength toward logical zero.
one — vl-dstrength-p: Drive strength toward logical one.

WARNING. We have not paid much attention to strengths, and our transformations probably do not handle them properly.

See sections 7.1.2 and 7.9 of the Verilog-2005 standard for discussion of strength modelling. Every regular gate has, associated with it, two drive strengths; a "strength0" which says how strong its output is when it is a logical zero, and "strength1" which says how strong the output is when it is a logical one. Strengths also seem to be used on assignments and module instances.

There seem to be some various rules for default strengths in 7.1.2, and also in 7.13. But our parser does not try to implement these defaults, and we only associate strengths onto module items where they are explicitly specified.

Subtopics

Vl-gatestrength-fix: Fixing function for vl-gatestrength structures.
Vl-gatestrength-equiv: Basic equivalence relation for vl-gatestrength structures.
Make-vl-gatestrength: Basic constructor macro for vl-gatestrength structures.
Vl-gatestrength-p: Recognizer for vl-gatestrength structures.
Vl-gatestrength->zero: Get the zero field from a vl-gatestrength.
Vl-gatestrength->one: Get the one field from a vl-gatestrength.
Change-vl-gatestrength: Modifying constructor for vl-gatestrength structures.