		Search-engine friendly clone of the ACL2 documentation.

Def-pipeline-thm

Prove that an SVTV pipeline is an unrolling of the FSM that it's based on

When computing an SVTV pipeline using defsvtv$ or defsvtv$-phasewise, a FSM is first created and the pipeline is then a composition (unrolling) of FSM phases. This is an invariant of the svtv-data stobj; if the pipeline-valid bit of the svtv-data stobj is set, then it is known that the pipeline field is an unrolling of the cycle-fsm field, with unrolling parameters specified in the pipeline-setup field.

The def-pipeline-thm event uses this invariant of the svtv-data stobj to prove that property, given an SVTV that was created using defsvtv$. This event requires that the svtv-data stobj was not changed since the creation of the defsvtv$. It proves a theorem of the following form:

(b* ((fsm (svtv-cycle))
     (rename-fsm (make-svtv-fsm :fsm fsm
                                :namemap (svtv-namemap)))
     (renamed-fsm (svtv-fsm->renamed-fsm rename-fsm))
     ((pipeline-setup pipe) (svtv-pipeline-setup))
     (outvars  (svtv-probealist-outvars pipe.probes))
     (run (fsm-run
           (svex-alistlist-eval
            (svtv-fsm-to-fsm-inputsubsts
             (take (len outvars) pipe.inputs)
             pipe.override-vals pipe.override-tests
             (svtv-namemap))
            env)
           (svex-alist-eval pipe.initst env)
           renamed-fsm
           outvars)))
  (svex-envs-equivalent
   (svex-alist-eval (svtv->outexprs (svtv)) env)
   (svtv-probealist-extract pipe.probes run)))

Here (svtv) is the SVTV created by defsvtv$. The other constant functions (svtv-cycle), (svtv-namemap), and (svtv-pipeline-setup) are introduced by the def-pipeline-thm event. (The cycle function doesn't need to be created if a previous def-pipeline-thm event already introduced it.)

The options for def-pipeline-thm are as follows:

(def-pipeline-thm svtv-name
                  ;; optional, in case cycle was introduced previously
                  :cycle-name cycle-name)