Olika typer av allmänna programmeringsspråk, som SystemC, används i allt högre grad för att specificera systemkonstruktioner som har både hårdvara och programvarudelar. Språken på systemnivå möjliggör en flexibel partitionering i utformningen av hårdvaran och programvaran. Dessutom är många egenskaper beroende av kombinationen av hårdvara och programvara och kan inte verifieras av någondera parten ensam. Befintliga verktyg tillämpar antingen icke-formella metoder eller hanterar endast språkets lågnivådelar. Detta dokument presenterar en ny teknik som hanterar både hårdvara och programvarudelar i en systembeskrivning. Detta görs genom att automatiskt partitionera den enhetliga systembeskrivningen till synkrona (hårdvara) och asynkrona (programvara) delar. Denna teknik har implementerats och tillämpats på systemnivåbeskrivningar av flera industriella exempel. Partitioneringen av maskinvara/programvara förbättrar verifieringens prestanda jämfört med den monolitiska metoden.
En formell verifiering av partitionering av maskinvara/programvara med SystemC finns i REF.
Formal verification of SystemC by automatic hardware/software partitioning
{'venue': "Proceedings. Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2005. MEMOCODE '05.", 'journal': "Proceedings. Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2005. MEMOCODE '05.", 'mag_field_of_study': ['Computer Science']}