		Search-engine friendly clone of the ACL2 documentation.

Defmodules

Vl-simplify

Top level interface for simplifying Verilog modules for use in formal verification with esim.

Signature
(vl-simplify design config) → (mv good bad)
Arguments: design — Parsed Verilog design, typically from vl-load.
Guard (vl-design-p design).; config — Various options that govern how to simplify the modules.
Guard (vl-simpconfig-p config).
Returns: good — Portion of the design that was simplified successfully.
Type (vl-design-p good).; bad — Portion of the design that was thrown out due to errors or unsupported constructs.
Type (vl-design-p bad).

Definitions and Theorems

Function: vl-simplify

(defun vl-simplify (design config)
 (declare (xargs :guard (and (vl-design-p design)
                             (vl-simpconfig-p config))))
 (let ((__function__ 'vl-simplify))
  (declare (ignorable __function__))
  (mbe
   :logic
   (b* (((mv good bad)
         (vl-simplify-main (vl-annotate-design design)
                           config)))
     (mv good bad))
   :exec
   (b* (((vl-simpconfig config) config)
        (design (vl-annotate-design design))
        (design (if config.compress-p (xf-cwtime (hons-copy design))
                  design))
        ((mv good bad)
         (vl-simplify-main design config))
        (good (if config.compress-p (xf-cwtime (hons-copy good))
                good))
        (bad (if config.compress-p (xf-cwtime (hons-copy bad))
               bad)))
     (vl-gc)
     (mv good bad)))))

Theorem: vl-design-p-of-vl-simplify.good

(defthm vl-design-p-of-vl-simplify.good
  (b* (((mv ?good ?bad)
        (vl-simplify design config)))
    (vl-design-p good))
  :rule-classes :rewrite)

Theorem: vl-design-p-of-vl-simplify.bad

(defthm vl-design-p-of-vl-simplify.bad
  (b* (((mv ?good ?bad)
        (vl-simplify design config)))
    (vl-design-p bad))
  :rule-classes :rewrite)

Subtopics

Vl-warn-problem-modulelist: Extend vl-warn-problem-modulelist to a list of modules.
Propagating-errors: The error handling strategy used by vl-simplify.
Vl-simpconfig: Options for how to simplify Verilog modules.
Vl-simplify-main: Core transformation sequence for using VL to generate E modules.
Vl-warn-problem-module: Add a fatal warning if this is a problem module.
Vl-design-problem-mods: Remove user-specified problem modules from the design.