A Framework for Automated HW/SW Co-Verification of SystemC Designs Using Timed Automata
In this dissertation, we present a systematic, comprehensive, and formally founded quality assurance process, which allows automated co-verification of digital hardware/software systems that are modeled in SystemC. The main idea is to apply model checking to verify that an abstract design meets a requirements specification and to generate conformance tests to check whether refined designs conform to this abstract design. As formal foundation, we define a formal semantics of SystemC by a transformation into the well-defined semantics of UPPAAL timed automata. The automatically generated timed automata model can be verified using the UPPAAL model checker and it can be used to generate conformance tests. With that, we obtain guarantees about liveness, safety, and timing properties of the abstract design, which serves as a specification, and we can ensure the consistency of each refined design to that. The result is a HW/SW co-verification flow that supports the HW/SW co-development process continuously from abstract design down to the implementation. The complete verification flow is implemented in our Framework for the Verification of SystemC designs using Timed Automata (VeriSTA) and its applicability and performance are shown by experimental results.
What people are saying - Write a review
We haven't found any reviews in the usual places.
abstract design algorithm Anti-lock Braking System ANTLR approach ATENA automata model automata template automaton behavior clock zone co-simulation committed location communication computational eﬀort compute all possible conformance tests counter-examples coverage deﬁned deﬁnition delay delta-cycle design ﬂow diﬀerent edges eﬀect eﬃcient embedded systems error detecting capability FIFO ﬁnal implementation ﬁrst formal semantics formal veriﬁcation given input trace given SystemC design hardware and software HW/SW co-design HW/SW co-veriﬁcation inﬁnite input selection instantiated interface Kripke structure labeled transition systems loop model checking modules non-deterministic notiﬁcation optimizations packet switch possible output traces possible successor primitive channels producer-consumer example properties ready_procs reﬁned design reﬁnement satisﬁed semantic step semantics of SystemC shown in Figure speciﬁcation structure symbolic semantics synchronization SystemC language SystemC test benches SystemC to Uppaal test suite test verdict thread process transaction level modeling transition update Uppaal model checker Uppaal timed automata variables veriﬁcation techniques Verilog VeriSTA framework wait