LEMA User's Manual

Chris J. Myers, Satish Batchu, Kevin Jones, Scott Little, Nicholas Seegmiller, Robert Thacker, David Walter, Zhen Zhang

1  Introduction

LEMA has been developed for the formal verification of analog and mixed-signal (AMS) circuits. LEMA includes the following tools:

2  Project Management

A project is a collection of models, analysis views, learn views, and graphs. As shown below, LEMA displays all project files on the left, the open models, views, and graphs on the right, and a log of all external commands on the bottom. The menu bar is located on the top of the window in the Windows and Linux versions. It is located on the top of the screen in the MacOS version.
screenshots/LEMA.png

2.1  Creating and Opening Projects

To create a new project, select New → Project from the File menu as shown below. You will then be prompted to browse to a desired location and to give a name to the project directory. After you do this, click the new button and a new project directory will be created. To open a project, select Open → Project from the File menu. You will then be prompted to browse to a project directory to open, and clicking open will open the project. You may also open a project by selecting one of your five most recently opened projects by selecting the project name shown in the File drop down menu shown below.
screenshots/projectLema.png

2.2  Creating Models and Graphs

After you have created or opened a project, you can create a new model or graph to add to the project. To create a new VHDL-AMS model, select New → VHDL-AMS Model from the File menu as shown below. You will then be prompted to give a model id. At this point, a simple text editor will open in a new tab. To create a new LHPN model (see Section ), select New → Labeled Hybrid Petri Net from the File menu. You will then be prompted to give a model id. At this point, an LHPN editor (see Section ) will open in a new tab. To create a new Spice model, select New → Spice Circuit from the File menu. You will then be prompted to give a model id. At this point, a simple text editor will open in a new tab. To create a new TSD graph, select New → TSD Graph from the File menu. You will then be prompted to give a name to the TSD graph. At this point, a TSD graph editor (see Section ) will open in a new tab. Once a model or graph is created, it can be opened again later by right clicking on the object in the project window and selecting "Edit", or alternatively double-clicking on the object.
screenshots/newModelLema.png

2.3  Importing Models

You can import into the current working project VHDL-AMS models or LHPNs created by other programs or stored in other projects. To import a VHDL-AMS model, select Import → VHDL-AMS Model from the File menu as shown below. You will then be able to browse to find a model to import. After selecting the desired model, click the import button to bring the model into the project. To import an LHPN, the procedure is the same except use the Import → LHPN Model option. Before bringing the model into the project, it will be edited to a format consistent with this tool.
screenshots/importLema.png

2.4  Editing Project Objects

All project objects can be modified by highlighting the object and using a right mouse click to open a menu of options as shown below. Using this menu, every type of object can be copied, renamed, or deleted. For an LHPN, the "View/Edit" option opens the model in an LHPN editor (see Section ). For a VHDL-AMS model, the "View/Edit" option opens the model in a simple text editor. For a TSD graph, the "View/Edit" option opens the TSD graph in a TSD graph editor (see Section ). For a probability graph, the "View/Edit" option opens the probability graph in a histogram editor (see Section ). For a verification view, the "Open Verification View" option opens the verification view (see Section ). For a learn view, the "Open Learn View" option opens the learn view (see Section ).
screenshots/modLHPN.png screenshots/modVHDL.png
screenshots/modVerify.png screenshots/modLearnLema.png

2.5  Viewing Project Objects

An LHPN can also be viewed using GraphViz's dotty program by right clicking on the model you want to view and selecting the "View Model" option. A VHDL-AMS model may be converted into an LHPN and viewed using the same "View Model" option.
screenshots/modLHPN.png screenshots/modVHDL.png
screenshots/modVerify.png screenshots/modLearnLema.png

2.6  Creating Tool Views

To perform verification or learning, right click on a model and select "Create Verification View" (see Section )to perform analysis or "Create Learn View" (see Section ) to perform learning. A verification or learn view may also be opened by selecting the model in the file tree and selecting Learn or Verification from the Tools menu. You will then be prompted to give a name to your verification or learn view. After a name is entered, a tab with the newly created view will open. Once a view is created, it can be opened again later by right clicking on an analysis directory and selecting "Open Verification/Learn View" or alternatively double-clicking on the view.
screenshots/createVerification.png screenshots/createLearnLema.png
When you create a verification view from a VHDL model, an LHPN is automatically created for verification.

3   LHPN Editor

The LHPN editor as shown below allows the user to create or modify an LHPN model of an analog or mixed-signal circuit. An LHPN model includes places (see Section ), transitions (see Section ), variables (see Section ), and control flow (see Section ). Each of these items can be added, removed, or edited. To add a new item, click on the appropriate add button. You will then be prompted to provide a unique id and some properties for this new item (as described below). After you have filled out all of the required fields, click add and the new item will be added to the LHPN. To remove an item from the model, select that item and click the remove button. The item will then be removed from the model. However, if you try to remove an item that is being used (for example, a variable that is assigned in a transition), you will first have to remove its use. To edit an existing item, select that item from the list and click the edit button. An editing window will open and you will be able to change the properties of that item. When you are done editing this item, click save to save the changes to the item. After the model is complete, press the Save LHPN button to store the model. The Save As button can also be used to store the model, but in this case, a new model ID will be requested and the model will be saved using that ID.
screenshots/LHPNedit.png

3.1   Places

Places define a certain characteristic of a circuit, according to the definition of Petri nets. It may be noted that the LEMA tool does not support implicit places in its LHPNs. If an LHPN with implicit places is imported into the tool, the implicit places are automatically explicitly declared in the imported net. As shown below, a place has the following fields:
screenshots/place.png

3.2   Transitions

Transitions define events in the petri nets. In the case of LHPNs, they are elaborated by labels attached to the transitions, which are defined by included fields. As shown below, a transition has the following fields:
screenshots/transition.png

3.2.1   Assignments

When an assignment is added to the labeling function of a transition, the user is prompted to define the assignment that is to take place. An assignment may be made to the value of any variable or to the rate of a continuous variable. An assignment consists of the following fields:
screenshots/assignment.png

3.3   Variables

Variables represent the continuous, boolean, or integer signals used in an LHPN. When a variable is created, the user will be prompted to input which type of variable is being created. As shown below, a variable contains the following fields: To change a variable from one type to another, the user must remove the initial variable and then add a new variable with the same id of the desired type.
screenshots/contVariable.png screenshots/boolVariable.png screenshots/intVariable.png

3.4   Control Flow

The control flow describes the edges in the LPN, or the connections between places and transitions. The edges in the net are referred to as "movements" within the tool and describe a directional edge between nodes of the graph. As shown below, a movement includes the following fields:
screenshots/movement.png

4   Text Editor

A simple text editor is available for viewing VHDL-AMS models and spice decks. This editor does not have many features, so the user may desire to use a more robust external text editor. To do so, select the Preferences option from the Edit menu, click on the "Use External Viewer" option and enter the name of the desired external text editor in the space provided. Every time that a VHDL-AMS or Spice model is opened, it will be opened in the external text editor.
screenshots/VHDLedit.png

5   Verification View

The verification view is used to verify the property stated in the LHPN model. The verification view as shown below includes tabs for basic options (see Section ), and advanced options (see Section ).
screenshots/verificationView.png

5.1   Basic Options

This tab includes the model being verified, basic timing options, and other basic user options. <ADD CITATION?>
The first line on the basic options panel is the filename of the LHPN being verified. The LHPN verified is the one saved in the file location at the time of verification.
The first set of radio buttons in this tab specifies the timing method to be used in the verification.
The other options refer to miscellaneous ATACS options.

5.2   Advanced Options

This tab includes compilation options, advanced timing options, other advanced options and a user specification for a BDD Linkspace size. The first set of check boxes enables or disables compilations options.
The next set of check boxes allows the user acces to more advanced timing options.
The other advanced options include
screenshots/advOptions.png

6   Learn View

The learn view is used to generate an LHPN from time series data. The learn view includes tabs for a data manager (see Section ), a learn tool (see Section ), and a TSD graph editor (see Section ).

6.1   Data Manager

The data manager as shown below is used to both enter time series experimental data as well as bring data into the learn view. The Add button is used to create a new data file. After pressing this button, enter the name of the new data file, and then enter the data for this file using the data editor to the right. The Remove button deletes all highlighted files. Note that after highlighting one file, you can use the ctrl key to highlight additional files or the shift key to highlight a range of files. The Rename button is used to change the name of a data file. The Copy button copies a data file. The Copy From View button brings up a list of all analysis and learn views in the current project, and data from the selected view will be copied into this learn view. Finally, the Import button brings up a file browser, and it allows you to import a data file from outside this project. These files can be in time series data (TSD) format (see Section ), comma separated value (CSV) format, or tab delimited format (DAT).
The contents of the data file highlighted on the left appear in the data editor on the right. Individual data entries can be modified, new data points can be added using the Add Data Point button, data points can be removed using the Remove Data Point button, and data points can be copied using the Copy Data Point button. When you are satisfied with all your changes, you should press the Save button to record your changes.
screenshots/dataManagerLema.png

6.2   Learn Tool

The learn tool is used to generate abstract models from the simulation data entered through the data manager described above. To use this learn tool, adjust the basic options(see Section  ) and advanced options(see Section  ), if desired, then press the Save and Learn button. The resulting abstract models in the form of Labeled Hybrid Petri Net (see Section ),VHDL-AMS and Verilog-AMS can be viewed by clicking appropriate options in the View Menu. The resulting circuit is specified using our Labeled Hybrid Petri Net Format (see Section ) and is shown graphically using GraphViz's Dotty tool. There are also menu options to save the parameters without learning, view the last learned models, save the generated models into the project, and view the last run log.

6.2.1   Basic Options

The learning options shown below are as follows:
screenshots/learnBasicLema.png

6.2.2   Advanced Options

The following parameters which are used to configure the model generation process can be specified through the advanced options tab.
screenshots/learnAdvLema.png

7   TSD Graph Editor

The TSD graph editor appears as a tab in the learn view. TSD graphs can also be created at the top-level of the project to allow you to integrate results from several learn views. These graphs can be created using the New → TSD Graph menu option. Once created, they can be viewed and edited by double clicking on the graph in the project window. An example graph is shown below.
screenshots/TSDgraphLema.png
In the TSD graph editor shown below, a graph is created by double clicking on the graph. You can then set various parameters and select what values you would like to have graphed. The parameters that you can select for a graph include:
screenshots/editGraphLema.png
The data selection menu on the left displays all of the available sets of data that can be graphed. In particular, one can graph the average, variance, standard deviation, or results from individual simulation runs. For a top-level graph, these data sets will be organized hierarchically. Hierarchy is also introduced when simulations in an analysis view are given simulation IDs or after performing an analysis while sweeping parameter values. After selecting a data set, one can select individual species to graph and how they are to be displayed. In other words, for each species, there are the following options: Note that a check mark appears on a data set to indicate that some variables have been selected in that data set. Also, all variables can be deselected by pressing the Deselect All button.
The "Save Graph" button saves the settings for the graph to a file, so when you re-open the graph, it will reload this data and display in the same way as before. The "Save As" button prompts for a filename and creates a new top-level graph with that name. Finally, the "Export" button prompts for a filename and exports the data to the given name. The extension provided for the filename is used to determine how the graph is to be exported. The supported file types are: If no extension is given, then the file type is the one specified in the file filter (default is pdf). For image (i.e., not data) file types, you will be prompted to give a desired pixel height and width for the file before the file is exported.

8   Preferences

User preferences can be set by selecting the Preferences option under the File menu on Linux and Windows or the LEMA menu on MacOS. As shown below, the user can decided whether they wish to use an external editor for VHDL-AMS models, and which editor to use.
screenshots/preferenceLema.png

9   Labeled Hybrid Petri Net Format

Our labeled hybrid Petri net (LHPN) format specifies a system according to an extended version of Petri nets. The graph is specified as a set of places and transitions. Each transition is described with a set of labels described in a format specific to LHPNs. The places, transitions, and boolean signals that are general to Petri nets are described in a generalized .g file format, as follows. Each space-delineated string on the lines ".inputs" and ".outputs" declares a boolean input or output signal. Each space-delineated string on the ".dummy" line declares a "dummy" transition to be used in the net. Beginning with the ".graph" line, each line with two space-delineated strings represents a movement between a place and a transition. The ".marking" line ennumerates the initially marked places in the graph, and the ".end" line specifies the end of the file.
.inputs a b
.outputs x y z
.dummy yP xM yM xP zP zM
.graph
ip0 yP
xM ip2
ip5 xM
etc.
.marking {ip4 ip5}
.end

The labels and analog behavior of LHPNs is specified using a file format specific to LHPNs. These lines will be interpreted as comments by other .g parsers. Each line used in the ATACS tool begins with a "#@." (citation for ATACS?), while each line specific to the LEMA tool begins with a "# - .". Most of these lines are easily understood according to their beginning comments. Each of the continuous and integer variables are declared in a space-delineated "#@.variables" line included near the top of the file. Following the variable declaration, the places are explicitly declared in a "# - .places" line, which follows the format of the ".inputs" line. The inital values of the boolean signals are given in a boolean vector in a "#@.init_state" line of the following format. The signals are given in the order that they are declared, input signals coming before output signals.
#@.init_state [boolean vector]

Each integer and continuous variable is given an initial value in a "#@.init_vals" line, and each continuous variable is given an initial rate value in a "#@.init_rates" line. The syntax of these lines is as follows, the example being given for a ".#@init_vals" line.
#@.init_vals {<variable1=initial value1><variable2...>}

The enabling condition for each transition is given in a "#@.enablings" line in the following format.
#@.enablings {<transition1=[enabling condition1]><transition2...>}

The delay for each transition is specified in the "#@.delay_assignments" line according to the following format, where each lower and upper bound of the delay is written as an expression parseable by ATACS. Likewise, the delays may be of a single value for deterministic behavior, as seen on the second transition.
#@.delay_assignments {<transition1=[lower bound, upper bound]><transition2=delay>}

The assignments to boolean variables on each transition are specified in the following format, where each lower and upper bound, or each deterministic assignment, is also written as an expression.
#@.boolean_assigments {<transition1=[boolean1:=[lower bound, upper bound]][boolean2:=value]><transition2...>}

Assignments to continuous variables and integers are combined onto a single "#@.assignments" line and written in the same format as boolean assignments. It may be noted that the only explicit difference between the declaration of continuous and integer variables in the inclusion of a "#@.continuous" line of the same format as the ".input" and ".output" lines.
Below is a simple, but complete example of an LHPN, including each of the options mentioned above.
.inputs w x
.ouputs y z
.dummy t0 t1 t2
#@.variables a b c
#|.places p0 p1
#@.init_state [0011]
.graph
p0 t0
t0 p1
p1 t2
t2 p0
.marking {p0}
#@.init_vals {<a=0><b=3><c=[1,2]>}
#@.init_rates {<a=-2><b=1>}
#@.enablings {<t0=[~x&~y]><t1=[x&(a>=5)]><t2=[c>=4]>}
#@.assignments {<t1=[a:=5][c:=4]><t2=[c:=1]>}
#@.rate_assignments {<t0=[a:=1]><t2=[a:=0][b:=1]>}
#@.delay_assignments {<t0=2><t1=[0,inf]><t2=[0,5]>}
#@.boolean_assignments {<t0=[y:=TRUE]><t1=[y:=FALSE][z:=TRUE]><t2=[y:=~w]>}
#@.continuous a b
.end

10   Time Series Data Format

The time series data (tsd) format is composed of a parenthesized and comma-separated set of time points. Each time point is composed of a parenthesized and comma-separated set of data for that time point. This first time point is composed of a set of strings that are the labels for the data entries. The first entry in each time point is by convention the time for that time point. Below is an example simulation of the species CI and CII from 0 to 1000 seconds with time points separated by 100 seconds.
(("time","CI","CII"), (0,0,0), (100,0,19), (200,20,25), (300,19,18), (400,17,20), (500,17,46),
(600,26,40), (700,43,43), (800,63,28), (900,72,34), (1000,72,28))

11   List of Hot Keys

Below is a list of the hot keys used in Windows and Linux with the MacOS equilvalents in parantheses.

12  Reporting Bugs and Feature Requests

In order to report a bug or to request a change or feature, please send an email to:
atacs-bugs@vlsigroup.ece.utah.edu.
The subject line must begin with one of the following keywords or the mail will be filtered by our spam filters:

13  Credits

The LEMA tool is being developed at the University of Utah by Chris Myers,   Satish Batchu   Kevin Jones,   Scott Little,   Nicholas Seegmiller,   Robert Thacker,   David Walter, and Zhen Zhang. Scott Little is now with Freescale in Austin, Texas, Nicholas Seegmiller is now with Backcountry.com in Park City, Utah, and David Walter is now with the Virginia State University.



File translated from TEX by TTH, version 3.81.
On 11 Sep 2017, 09:31.