Specification and Verification of Synchronous Hardware using LOTOS

Abstract

This paper investigates specification and verification of synchronous circuits using Dill (Digital Logic in Lotos). After an overview of the Dill approach, the paper focuses on the characteristics of synchronous circuits. A more constrained model is presented for specifying digital components and verifying them. Two standard benchmark circuits are specified using this new model, and analysed by the Cadp toolset (Cæsar/Aldébaran Development Package).