IEEE Transactions on Computers · 2008 · 39 citations · 12 references
ComputingComputer ScienceComputer SystemsFormal MethodsReal-time SystemsSystems ModelingAssertion-based VerificationModel CheckingSpecification LanguagesSystem SimulationTemporal LogicVerificationAssertion VerificationChannelsReal-time System VerificationReal-time Systems VerificationSimulation-based VerificationSystemc ModelingTemporal Logic AssertionsTemporal Verification
The TLM modeling level of the systemC language emphasizes the transactions in a complex system, considered at a very high level of abstraction. This level of specification considerably improves simulation performance and is therefore increasingly being adopted. We address assertion-based verification (ABV) of TLM systemC models. We propose a framework for supervising during simulation the verification of temporal properties expressed in PSL. Very few modifications are needed in the original systemC code. The TLM specification can be timed or not. The properties can involve several channels, of different types.
12
Combining System Level Modeling with Assertion Based Verification
A. Dahan, Daniel Geist, L. Gluhovsky et al. · 2005 · 60 citations
Formal verification of LTL formulas for SystemC designs
Rolf Drechsler · 2003 · 54 citations
Proven correct monitors from PSL specifications
Katell Morin-Allory, D. Borrione · 2006 · 53 citations