CISPA
Browse
cispa_all_3072.pdf (4.58 MB)

Syntroids: Synthesizing a Game for FPGAs using Temporal Logic Specifications

Download (4.58 MB)
conference contribution
posted on 2023-11-29, 18:11 authored by Gideon Geier, Philippe HeimPhilippe Heim, Felix Klein, Bernd FinkbeinerBernd Finkbeiner
We present Syntroids, a case study for the automatic synthesis of hardware from a temporal logic specification. Syntroids is a space shooter acarde game realized on an FPGA, where the control flow architecture has been completely specified in Temporal Stream Logic (TSL) and implemented using reactive synthesis. TSL is a recently introduced temporal logic that separates control and data. This leads to scalable synthesis, because the cost of the synthesis process is independent of the complexity of the handled data. In this case study, we report on our experience with the TSL-based development of the Syntroids game and on the implementation quality obtained with synthesis in comparison to manual programming. We also discuss solved and open challenges with respect to currently available synthesis tools.

History

Preferred Citation

Gideon Geier, Philippe Heim, Felix Klein and Bernd Finkbeiner. Syntroids: Synthesizing a Game for FPGAs using Temporal Logic Specifications. In: Formal Methods in Computer-Aided Design (FMCAD). 2019.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

Formal Methods in Computer-Aided Design (FMCAD)

Legacy Posted Date

2020-05-25

Open Access Type

  • Unknown

BibTeX

@inproceedings{cispa_all_3072, title = "Syntroids: Synthesizing a Game for FPGAs using Temporal Logic Specifications", author = "Geier, Gideon and Heim, Philippe and Klein, Felix and Finkbeiner, Bernd", booktitle="{Formal Methods in Computer-Aided Design (FMCAD)}", year="2019", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC