User Tools
Log In
Search
Site Tools
Log In
start
What is Workcraft?
framework for
interpreted graph models
elaborate cross-platform GUI
for modelling
established tools
for verification and synthesis
source code
•
latest news
•
training events
Download Workcraft v3.1.9
for Windows
(34 MiB)
for Linux
(42 MiB)
for OS X
(38 MiB)
download mirror
•
release notes
•
distribution
Modelling and verification of concurrent algorithms with Petri Nets
Synthesis of instruction decoder using Conditional Partial Order Graphs
Specification and synthesis of speed-independent controllers from Signal Transition Graphs
Modelling self-timed pipelines using Dataflow Structures
Tutorials
Modelling causality and concurrency
Modelling with Finite State Machines: Vending machine
Petri net synthesis: Concurrent vending machine
Modelling with Petri nets: Dining philosophers
Modelling with Signal Transition Graphs: Distributed Mutual Exclusion
Modelling with STGs: Writer-biased read/write lock
Modelling Genetic Regulatory Networks with STGs: Lysis-Lysogeny Switch in Phage λ
Optimising Asynchronous Pipelines Using Wagging
Analysis and Verification of Communication Fabrics
Modelling with Structured Occurrence Nets: Crime and Accident Scenes
Synthesis and verification of asynchronous circuits
Synthesis and verification of C-element
(basic circuit, detail explanation)
Synthesis and verification of buck controller
(medium complexity with some hints)
Synthesis and verification of VME bus controller
(medium complexity, for individual work)
Hierarchical design of a realistic buck controller
(advanced material for individual work)
Initialisation of speed-independent circuits
(advanced material for individual work)
Resolution of encoding (CSC) conflicts
(advanced material for individual work)
Help
Generic information
Main window
Property editor
Tool controls
Main menu
Global settings
Tips and tricks
Model plugins
Petri Net
Structured Occurrence Net
Signal Transition Graph
Conditional Partial Order Graph
Digital Circuit
Dataflow Structure
xMAS Circuit
Advanced topics
SCENCO toolsuite
Plato toolsuite
Boolean expressions
Reach language
Assertion language
Verification properties
Circuit synthesis
Scripting interface
Async arbitration primitives
Development
Building from source
Preparing the documentation
Notes about backend tools
Notes about models
Notes about DokuWiki setup
Analysis of code with ObjectAID UML Explorer
Concept of Expressions
Naming of model components
Mathematical and visual models
Hierarchy observers
Compatibility manager
Acknowledgements