User Tools

Site Tools


changelog:v3.2.5

Workcraft v3.2.5 (2019-11-21)

Usability improvements

  • Show shortcuts in Create work dialog for quickly creating new models
  • Configurable font size via global preferences (Edit→Preferences…):
    • In Common→Visual the properties Label font size (cm) and Name font size (cm).
    • In Models→Digital Circuit the properties Contact font size (cm) and Function font size (cm)
    • In Models→Signal Transition Graph the property Transition font size (cm)
  • Auto-save of last edited Custom properties and Custom assertions
  • Menu item for combined verification of all basic properties (in Digital Circuit, Signal Transition Graph, and Dataflow Structures) is renamed to All of the above (reuse unfolding) [MPSat]

Model and tool plugins

  • Digital Circuit plugin
    • Tool for reducing the number of zero delay inverters (available via Transformation→Optimise zero delay of buffers and inverters (selected or all)).
    • Verification of circuit implementation for binate functions (via Verification→Binate consensus [MPSat]).
    • Names and pins of gates for synthesis of reset logic (BUF, AND2, OR2, NAND2B, NOR2B) are now automatically extracted from Genlib gate library.
    • In global preferences use of separators to create subsections for import/export, reset, and testing.
    • Undo/redo functionality in Initialisation analyser and Cycle analyser tools
  • Signal Transition Graph plugin
    • Handshake verification wizard (Verification→Handshake wizard [MPSat]…)
    • Search of signal events by the signal name directly from the Property editor of the model
  • eXtended Burst Mode plugin
    • Model capturing functionality
    • Auto-calculation of signal changes in input and output bursts
    • Verification for unique state encoding and inclusion of conditionals
    • Conversion into STGs and Petri nets
    • Export into Minimalist burst mode file format
    • Simulation tool

Fixes and technical stuff

  • Integration of BDD library (https://bitbucket.org/vahidi/jdd) for complex operations on Boolean functions (e.g. checks for functions isomorphism, implication, binatness).
  • Update of UnfoldingTools
    • Bugfix for threshold operator (not used in built-in verification properties, but could affect custom Reach properties using this operator)
    • Syntax sugar to refer to transition or signal enabledness in LTL-X verification in Punf
  • Refactoring of the properties API and improvements of Property editor
    • Action properties rendered as a buttons (can be an array of actions associated with one property).
    • Span properties that occupy both columns.
    • Separator to structure properties into subsections.
    • Textual properties with associated action (e.g. create or search for a node with the specified name)
  • Rework of the build system updating Gradle and its plugins
  • Refactoring of Boolean formula API
  • When reading .g files recognise split STG places with @NUMBER suffix. These can be produced in the intermediate .g files when calling Punf with -r option.