EngineeringComputer EngineeringComputer ScienceEmbedded SystemsHardware Description LanguagesSystems ModelingConcurrency VerificationConcurrent ModelingFinite State Machine ModelingHardware Modeling For Digital SystemsModel CheckingReal-time Systems DesignConcurrency RepresentationDeterministic CommunicationDeterministic ConcurrencyEmbedded System ModelingHardware-software IntegrationNondeterministic SpecificationReal-time Systems VerificationRendezvous Communication
Typical embedded hardware/software systems are implemented using a combination of C and an hdl such as Verilog. While each is well-behaved in isolation, combining the two gives a nondeterministic model whose ultimate behavior must be validated through expensive (cycle-accurate) simulation.We propose an alternative for describing such systems. Our shim (software/hardware integration medium) model, effectively Kahn networks with rendezvous communication, provides deterministic concurrency. We present the Tiny-shim language for such systems and its semantics, demonstrate how to implement it in hardware and software, and discuss how it can be used to model a real-world system.By providing a powerful, deterministic formalism for expressing systems, designing systems and verifying their correctness will become easier.
30
Petri nets: Properties, analysis and applications
T. Murata · Proceedings of the IEEE · 1989 · 10.5K citations
The Semantics of a Simple Language for Parallel Programming.
Gilles Kahn · IFIP Congress · 1974 · 2.1K citations
Communicating sequential processes
Roger Boyle · Data Processing · 1985 · 2K citations
A Structural Approach to Operational Semantics
Gordon Plotkin · 2004 · 2K citations