changelog:v3.0.6

Workcraft v3.0.6 (2015-11-02)

Usability improvements

Frequently used Tools→Conversion menu is promoted to the main menu bar.
Support for read-arcs in Petri net and STG plugins. Tools for conversion between read-arcs and pairs of producing/consuming arcs.
Support for replica places in Petri net and STG plugin. A replica place is created if Shift is held while creating a connection to/from a place.
In simulation mode of Petri nets and STGs the consuming arcs from marked places are highlighted.
A generic tool for merging selected nodes of the same type. This tool is accessible under Transformations menu as follows: Merge selected vertices for Graph model, Merge selected states for FSM and FST models, Merge selected places for Petri net and STG models, and Merge selected components for Dataflow Structures.
User documentation is added for Dataflow Structures plugin.

Model and tool plugins

Digital Circuit plugin
- Automated conversion of MPSat synthesis results into a Digital Circuit work.
  - Complex gate synthesis – the self-dependencies of signals are interpreted as self-loops on combinational gates.
  - Generalised C-element synthesis – the self-dependencies result in sequential gates.
  - Standard C-element synthesis – the set and reset functions are extracted from the assign statement.
  - Technology mapping - zero delay inverters are taken into account.
- Verilog parser is extended to read assign statements and interpret them as unmapped gates.
- Improved handling of self-loops in circuit layout tool.
- Support for zero delay gates – visualised as a gate with a pass-through dotted wire when its Zero delay property is true. Note that only buffers and inverters can be set as zero delay. Also zero delay gates cannot be connected to other zero delay gates or primary outputs. A suggested use for zero delay buffers and inverters is as follows:
  - Zero delay inverters mimic input bubbles on the gates and should be placed close to those gates. The information about zero delay inverters is read from technology mapping results of Petrify and MPSat.
  - Buffers can be used to test the need for isochronic fork timing assumptions. Insert a buffer in each branch of a fork. If it causes a hazard, then tag the fork buffers as zero delay one by one, until a hazard-free operation is achieved. The remaining buffers will suggest the timing assumptions associated with the fork.

Signal Transition Graph plugin
- Visualisation of encoding conflicts: Verification→Unique State Coding (all cores) [MPSat] for USC conflicts or for Verification→Complete State Coding (all cores) [MPSat] for CSC conflicts. A user can choose between two visualisation schemes in the Tool controls panel:
  - Show selected core – individual cores in a selected sets of cores are highlighted in distinct colours. This feature can be useful for detailed analysis of the encoding conflicts to make an informed decision on how to manually resolve them.
  - Show core density map – the darker shades denote the higher density of the overlapping cores. Usually it is advantageous to insert new signals in the areas where most cores overlap, thus eliminating more conflicts by a single signal. Note that the number of density map levels can be configured in the Maximum number of core density map levels property of Signal Transition Graph model under Edit→Preferences… menu (5 levels by default).
- Tools for visualisation of state graphs by write_sg and draw_astg are (temporary) restored. Commands for generation of basic and binary-encoded state graphs can be found under Tools→External visualiser menu. Note that a better alternative is to convert an STG to an FSM via Conversion→Finite State Transducer [Petrify] as it allows better visualisation of CSC conflicts now (in different colors).

Conditional Partial Order Graph plugin
- Converter of Petri nets into Partial Order Graphs using JBPT library for untanglings.
- Vertices can be visualised either as a circle, a box or a label (to match the view of Petri nets and STGs).
- Improved algorithm for removal of transitive arcs.
- Performance optimisations for process mining of large data sets.

XMAS Circuit plugin
- Conversion of standard XMAS components into clocked STG. Note that Sync and Credit components are not supported yet.
- Tool for interactive simulation of xMAS based on generated STG model.
- Rotation and flipping of xMAS components.

Structured Occurrence Net plugin
- Time analysis and verification of SONs.
- Tool for automated generation and analysis of execution scenarios.
- Support for reverse simulation.

Fixes and technical stuff

MpsatPlugin is split into 4 plugins: MpsatVerificationPlugin, MpsatSynthesisPlugin, PunfPlugin and PcomPlugin.
MPSat is updated (backend tool for synthesis and verification of speed-independent circuits).
PGMiner is updated (backend tool for process mining).
ScEnco is updated (backend tool for scenario encoding of CPOGs).
VXM is included in the distribution (a backend tool for verification of xMAS circuits).