Familiarise yourself with Workcraft interface to learn its common features that are available for all plugins.
This plugin is intended for capturing, simulation and verification of xMAS Circuits. It supports all the conventional xMAS components and also a specialised Sync component. For simulation an xMAS model is automatically translated into a Signal Transition Graph (STG) that allows re-using the features of the STG plugin. The verification tool supports different levels of analysis including deadlock analysis of the xMAS circuits and a relational level focussed on querying.
In order to create an xMAS Circuit model choose File→Create work… menu item and in the New work dialogue select xMAS Circuit as the model type.
The xMAS plugin supports the following different types of primitive component:
Select the corresponding generator tool to create components of a needed type.
The following tools are used to create the components of the xMAS circuits:
The following is used to describe the synchronisation component of the xMAS model and its generator:
When the connection tool is active you can connect xMAS components. Only connections from the output ports to the input ports of the xMAS components are allowed.
For model editing, activate the selection tool . All the standard editing features (select, drag-and-drop, delete, copy, undo, group, etc.) work the same – see generic help on Selection controls and Property editor for details.
Similar to all the other models, textual comments can be created by activating the tool and clicking the editor panel in the position you want to put the text. Double-click on the note box to edit its text label in-place or do it through the property editor panel when the note is selected.
The Sync selection tool is selected from the Tools menu. For xMAS circuits that contain synchroniser components the Sync selection tool must be used for configuration of the synchronisers prior to verification. For GALS circuits synchronisers must be present in the design model and groupings must first have been made around all the basic primitive components in the design using the Selection controls prior to configuration.
The configuration menu is used for the sync settings. When it is selected a popup window appears which lists all of the synchronisers that are present in the design. Each of these is listed with its own configuration settings.
The configuration popup supports the following options:
Details are accepted by clicking on the OK button. The clocking frequencies are used subsequently in the verification.
For exporting to Json an Export Tool can be selected from the Tools menu. Json is a language independent data interchange format. The Export tool translates the xMAS circuits consisting of basic primitives into the Json format. For GALS designs clock frequencies set using the Sync Tool are assigned to the queues in the local modules respectively. The Export tool is used prior to verification.
For translating from Json to Circuit Petri nets a Generate CPN Tool is selected from the Tools menu. The Generate CPN tool translates the Json format into Control Circuit Petri nets which are subsequently used in the verification tool.
For simulation of an xMAS Circuit model activate the simulation tool . The enabled components are highlighted and can be executed by clicking them. The simulation tool controls provide the means for analysis and navigation through the simulation trace, see generic help on Simulation controls for details.
Note that simulation of an xMAS Circuit model is just an abstraction over the simulation of an automatically generated STG representation of the xMAS components.
In order to introduce priority execution of the xMAS components the following protocol with two distinct stages is adopted:
Verification can be conducted on any type of xMAS circuit constructed from the primitives. For GALS circuits synchronisers must be present in the xMAS model and the synchroniser settings must also be configured first using the Sync tool. Once the CPNs are generated verification of an xMAS Circuit model is carried out by selecting the verification tool [vxm] from the Tools menu. The verification tool has various submenus for configuring and executing different levels of verification. These are outlined below.
The configuration menu is used for applying various verification settings. Once it is selected a popup window appears listing various options.
The configuration menu supports the following options:
The verification submenu is used for initiating a verification. The output from the verification is dependent on the configuration settings that have been selected. Verification occurs by unfolding the net model to occurence nets followed by deadlock analysis. In advanced mode relational details are provided about the analysis in a verification report. An output screen showing verification in advanced mode for a GALS design is shown below.
This is accompanied with a popup screen highlighting relational details concerning the queues. An accompanying verification report is provided in the console.
The analysis submenu is used for analysing the solutions after an advanced level verification has been made. Following an advanced level verification a number of possible unique solutions is listed. Each solution lists details of the contents of the queues occuring in the particular deadlock state.
Options exist to select one of the unique solutions that are listed. By clicking the OK button the selected solution is processed by the analyser and from a detailed analysis specific feedback is given to the user based on the configuration settings.
The query submenu is used for selecting a specific type of query after an advanced level of verification has been made.
The query popup window supports the following options:
An example of the results of a query popup window relating to a Source query is shown below: