A data path verifier for register transfer level using temporal logic language Tokio
説明
A data path verifier for register transfer level is presented in this paper. The verifier checks if all the operations and the data transfers in a behavioral description can be realized on a given data path without any scheduling conflicts. Temporal logic based language Tokio is adopted as a behavioral description language in this verifier. In Tokio, designers can directly describe concurrent behaviors controlled by more than one finite state machine without unfolding parallelism. The verifier checks for the consistency between a behavior and a structure automatically and lightens the load of designers. The actual LSI chip which consists of 18,000 gates on CMOS gate array has been successfully verified. This verifier is concluded to have the ability to verify practical hardware design.
