— Directive: unaliased nodes...

Usage: ‘unaliased(...)’

Error out if any of nodes are aliased to each other. Tool-independent. Useful for verifying that certain nodes are not accidentally connected.

— Directive: assert P

Usage: ‘assert<P>()’

Error out if predicate expression P is false. Note that this is a compile-time check, which is enforced during unroll/create compilation. Useful for enforcing parametric constraints. Tool-independent. For run-time invariants, see $(expr)-syntax below.

— Directive: exclhi nodes...

Usage: ‘exclhi(...)’

Emits directives to check that nodes are mutually exclusive high at run-time. (This corresponds to the old CHECK_CHANNELS method of checking for exclusivity.) In hacprsim, these form checking rings. In cflat lvs, these directives affect charge-sharing and sneak-path analysis.

— Directive: excllo nodes...

Usage: ‘excllo(...)’

Emits directives to check that nodes are mutually exclusive low at run-time. (This corresponds to the old CHECK_CHANNELS method of checking for exclusivity.) In hacprsim, these form checking rings. In cflat lvs, these directives affect charge-sharing and sneak-path analysis.

— Directive: order nodes...

For cflat lvs, specify the node checking order for BDD algorithms.

— Directive: unstaticized node

For cflat lvs, specify that node should remain unstaticized.

— Directive: cross_coupled_inverters x y

For cflat lvs, just emit the directive back out with substituted canonical node names.

— Directive: mk_exclhi nodes...

For cflat prsim and hacprsim, enforce logic-high mutual exclusion among nodes. This is often used in describing arbiters.

— Directive: mk_excllo nodes...

For cflat prsim and hacprsim, enforce logic-low mutual exclusion among nodes. This is often used in describing arbiters.

— Directive: min_sep dist nodes...
— Directive: min_sep_proc dist procs...

Usage: ‘min_sep<dist>(nodes...)’

Specify that nodes should have a miminum physical separation of distance dist. nodes can be organized into aggregate groups: for ‘min_sep({a,b},{c,d})’, a and b must be separated from c and d. Affects cflat for layout and prsim.

The min_sep_proc variation specifies a minimum distance between two groups of processes. The referenced process in each group can be of different types.

          bool x[2], y[2];
          inv1 P, A;
          inv2 Q, B;
          spec {
            min_sep<100>(x[0], y[0])
            min_sep<100>(x, y)
            min_sep<100>({x[0], y[0]}, {x[1], y[1]})
            min_sep_proc<50>(P, Q)
            min_sep_proc<50>({P,Q}, {A,B})
          }

— Directive: runmodestatic node

For cflat lvs, mark this node as one that seldom or never changes value, for the sake of netlist analysis. NOTE: eventually this directive will be deprecated in favor of applying a proper node attribute. The decision to implement this as a spec-directive is an unfortunate consequence of compatibility with another tool.

— Directive: $ PRS-expr [message]

This declares a run-time invariant expression that is emits invariant directives to back-end tools and also tells simulators to check and report violations of violations, similar to exclhi and excllo. PRS-expr is a production rule guard that should always be true. Invariants also accept an optional argument after the expression for a more informative description string. These strings can be printed by back-end tools that understand invariants.

          spec {
            $(~(x & y))
            $(~(x & y), "at least one of these should be false at all times")
          }

is equivalent to exclhi(x, y).