22 June 2015 at ACSD-2015, Brussels, Belgium

In this tutorial we will present an up-to-date vision of and approach to applying Petri nets and related concurrency models to modelling, verification and synthesis of electronic circuits. Petri nets are seen here as a unifying modelling language for reasoning about the behaviour of digital circuits and systems, where various application-specific and engineering-specific modelling notations can be used as front-end notations. In the first half of the tutorial we will introduce theoretical aspects of our methodology, while the second half will be devoted to the familiarisation with the toolkit Workcraft, which supports (and is constantly in the process of expansion!) a range of front-end notations for digital hardware, captured at different levels of abstraction and granularity. The examples of the front end notation we will be presenting include both structurally oriented models, such as data-flow structures and logic circuit net-lists, as well a behavioural formalisms, such as state-graphs and conditional partial order graphs.

While the spectrum of hardware that can be modelled and designed includes both synchronous (aka globally clocked) and asynchronous (aka self-timed) circuits, our main focus is on the support for designing asynchronous logic. Why? The reason for that is that self-timed circuits are inherently concurrent and the role played by Petri nets for them is as fundamental as the role played by finite-state machines in traditional synchronous design. Thus, the hardware whose behavioural semantics is conveniently underpinned by Petri nets includes digital processors, pipelines, arbiters, interfaces and controllers, and most notably digital control for analog electronics, such as power converters.

• Lectures (3 hours)
  • Overview of Petri nets and Hardware Design
  • Basics of Asynchronous Circuit Design
  • Modeling of Asynchronous Circuits (High level and Low level)
  • Petri net Synthesis for Hardware
  • Verification of Asynchronous Circuits
  • Synthesis of Asynchronous Circuits using Signal Transition Graphs
  • Examples: processor, data-flow structures, arbiters, interface

• Practicals (3 hours)
  • Introduction to Workcraft
  • Design of a simple asynchronous circuit
  • Automated circuit synthesis
  • Formal verification
  • Advanced models/tools
  • Exercises and tuition

• lecture_1-modeling_synthesis_and_verification_of_hardware.pdf (1 MiB)
• lecture_2-formal_verification_and_synthesis_of_asynchronous_circuits.pdf (753 KiB)
• lecture_3-advanced_circuit_design.pdf (2 MiB)
• lecture_appendix-hardware_synthesis_with_petri_nets.pdf (705 KiB)
• practical_preliminaries-workcraft_overview.pdf (515 KiB)
• practical_1-c_element.pdf (491 KiB)
• practical_2-distributed_mutual_exclusion.pdf (476 KiB)
• practical_3-buck_controller.pdf (567 KiB)
• practical_4-vme_bus_controller.pdf (456 KiB)