		Search-engine friendly clone of the ACL2 documentation.

Def-override-transparent

For a given FSM and set of keys (internal signal names), prove that the FSM is override-transparent with respect to those keys.

This utility tries to prove that the given FSM is override-transparent with respect to a set of keys, using a syntactic check and, if necessary and the :fgl-semantic-check keyword argument is provided, a semantic check using FGL and equivalence checking.

Usage:

(def-override-transparent name-of-theorem-to-prove
   :fsm (my-fsm) :keys (my-keys)
   ;; optional:
   :fgl-semantic-check t                ;; default: nil
   :use-default-aignet-transforms nil)  ;; default: t