We highly reccommend reading through this User's Guide before working in ernest with X-Amin. But, for those who cannot wait to get started, we offer this Quick Start Guide to get you going in a minimum amount of time. In this section, detail is kept to a minimum - just the essentials are presented. Also, the steps in this guide make minimal use of GUI dialogs using the command interface in X-Amin instead.
Analysis Process Overview
To perform basic analysis on a design, the following steps need to be performed:
- Start X-Amin
- Read the HDL code
- Optionally generate code diagrams
- Link
- Perform logic analysis
These steps are detailed in the following sections.
Start X-Amin
From the command-line, X-Amin is invoked with the command:
% xamin
If a license hasn't been installed for X-Amin, the licensing wizard will appear. Follow the prompts to obtain and install a license.
Read HDL code
To read an HDL file into X-Amin, execute the following command in the Command Entry box (at the bottom of the X-Amin window):
> read <filename>
This will read the specified design into X-Amin without performing any lint or synthesis checks and will place the module into the default design space. You can read additional HDL files in if needed by repeating the read command.
See the command reference for further details on the read command.
Once a module is read in, you can display the HDL code:
> hdl <module name>
Generate code diagrams
Once an HDL file is read, diagrams can be generated which show the code structure of the code. This is an optional step and is not needed to perform logic analysis. Code diagrams can be created for an entire module, a block of HDL code, or a signal. The code diagrams currently supported by X-Amin are a flow diagram, flowchart diagram, and hierarchy diagram.
The flow diagram shows the statement flow of the HDL code and is useful for getting an overall view of the code structure as well as for determining signal dependencies.
To generate a flow diagram:
> flow <signal or module_name>
See the command reference for further details on the flow command.
The flowchart diagram shows the logical paths within the HDL code. Flowcharts can be generated for a module or a concurrent code block.
To generate a flowchart diagram:
> flowchart <module_name or block_#>
See the command reference for further details on the flowchart command.
The hierarchy diagram depicts the hierarchical structure of a design. Obviously, it is only useful if the design contains instantiated components.
To generate a hierarchy diagram:
> hier <module_name>
See the command reference for further details on the hier command.
Link
Linking is the process of converting HDL code into a database of information suitable for analysis. Linking must be performed before any analysis functions can be executed. A design must be error free before linking can be performed. Linking can be performed at any level in a design. To link a design:
> link <module_name>
See the command reference for further details on the link command.
Perform logic analysis
X-Amin provides several logic analysis functions. Each will be briefly outlined in this section.
The first, and most often used, analysis function is logic evaluation, or eval, for short. Eval produces a truth table for a specified signal. The eval function contains many options to filter and control the truth table generation process, but just the basic eval command will be described here. To perform logic evaluation on a signal:
> eval <signal>
The output of the eval command is table showing the inputs of the signal in the lef columns and the signal state in the rightmost column as shown below:
See the command reference for further details on the eval command.
For clocked logic, X-Amin can automatically perform reachability and deadlock analysis. Reachability analysis determines if any states are not reachable from a specified start state. Deadlock analysis determines if any reachable state cannot be exited. Typically, reachability and deadlock analysis is performed on state-machine registers, but X-Amin places no restrictions on what registers can be analyzed for reachability and deadlock. To perform reachability and deadlock analysis:
> reach <signal>
Note that signal must be a clocked signal. The output of the reach command is shown below:
[reach output]
See the command reference for further details on the reach command.
X-Amin can perform logic equivalency checking between two different designs or between two signals within a design. When performing equivalency checking, X-Amin models all clocked signals as inputs and only compares the combinational path driving the two signals. Therefore, when comparing two different designs, it is necessary for X-Amin to match input and register names between the designs. X-Amin will automatically match together inputs, outputs and registers that have the same name. For all other cases, it is necessary for the user to create a mapping file that specifies how inputs, outputs and registers are to be matched.
Given the following code:
module test (clk, a, b, c); input clk; input a, b, c; wire [1:0] zwire; assign zwire = (a) ? 0 : (b) ? 2 : (c) ? 3 : 0; reg [1:0] zcomb; always @(a or b or c) if (a) zcomb <= 1; else if (b) zcomb <= 2; else if (c) zcomb <= 3; else zcomb <= 0;
reg [1:0] zreg; always @(posedge clk) if (a) zreg <= 1; else if (b) zreg <= 2; else if (c) zreg <= 3; else zreg <= 0; endmodule
We can use compare to see if zwire, zcomb and zreg are equivalent:
> compare zwire zcomb
Comparing: zwire with zcomb
ERROR: zwire and zcomb are not identical
---------------------------- compare errors ----------------------------
-- inputs
a = 1
b = 0
c = 0
-- outputs zwire evaluates to: 00 zcomb evaluates to: 01 ------------------------------------------------------------------------
> compare zcomb zreg
Comparing: zcomb with zreg
zcomb and zreg are identical
To compare two designs they must both be linked at the same time.
> link moda modb Namespace ':moda' linked Namespace ':modb' linked
To compare all outputs and register inputs (assumes same input and register names as would be expected in different revs of the same module):
> compare moda modb
Comparing: moda.zcomb with modb.zcomb
ERROR: moda.zcomb and modb.zcomb are not identical
---------------------------- compare errors ----------------------------
-- inputs
a = 1
b = 0
c = 0
-- outputs moda.zcomb evaluates to: 00 modb.zcomb evaluates to: 01 ------------------------------------------------------------------------ Comparing: moda.zreg with modb.zreg moda.zreg and modb.zreg are identical
See the command reference for further details on the compare command.
The final analysis function that will be discussed in this section is Temporal Proofs. Temporal Proofs are a method a testing state transitions for correct operation. Temporal Proofs are an extension of reachability analysis in that paths between states transitions can be analyzed. For example, using Temporal Proofs it is easy to determine if the initial state can be reached from every other state.
Temporal Proofs are specified using logic expressions with temporal operators. X-Amin contains 10 temporal operators:
- EX(A): Next state after condition A is true along some state-sequence path
- AX(A): Next state after condition A is true along all state-sequence paths
- EF(A): Some state in the future after condition A is true along some state-sequence path
- AF(A): Some state in the future after condition A is true along all state-sequence paths
- EG(A): All states in the future after condition A is true along some state-sequence path
- AG(A): All states in the future after condition A is true along all state-sequence paths
- EU(A, B): Along some state-sequence path, condition A is true until condition B is true
- AU(A, B): Along all state-sequence paths, condition A is true until condition B is true
- ER(A, B): Along some state-sequence path, condition B is true until condition A releases B
- AR(A, B): Along all state-sequence paths, condition B is true until condition A releases B
Example: A simple mod 4 counter.
reg [1:0] cnt;
always @(posedge clk)
cnt <= cnt + 1;
Prove that the next value of cnt is 1 when cnt starts at 0. Also prove that the next value is not 2, but will become 2 at some future time.
> init cnt 0 Signal 'cnt' initialized to 0b0
> prove cnt EX(cnt==1) The rule is true
> prove cnt EX(cnt==2) The rule is false
> prove cnt EF(cnt==2) The rule is true
See the command reference for further details on the prove command.