Automata-Theoretic Approach to Hardware/Software Co-Verification

Executive Statement

This project develops an automata-theoretic approach to HW/SW co-verification. Major research tasks include: (1) developing a co-specification scheme for hardware and software, (2) developing an automata-theoretic model for co-verification and its model checking algorithms, (3) developing abstraction/refinement algorithms for co-verification, (4) developing a co-verification toolkit supporting this approach, and (5) evaluating this approach and the toolkit on device-driver co-verification.

Project Members

Funding

Software Packages

We are developing a toolkit, namely CoVer, to support the complete  abstraction-check-refinement loop for co-verification. This toolkit includes: (1) a co-specification tool that supports inclusion of hardware designs and software programs and specification of HW/SW interfaces; (2) an abstraction engine that takes the co-specification and creates a Büchi-pushdown system which abstracts the whole system; (3) a model checking engine for the Büchi-pushdown system which produces an error trace when the verification fails; (4) a refinement engine which takes the error trace, the Büchi-pushdown system, and the original co-specification as inputs, validates the error trace on the co-specification, and generates refinement hints if the error trace is spurious.

CoVer is currently available for download here.

Publications