Contract Specification of Pipelined Designs: Application to Testbench Automation
Alexander Kamkin · Proceedings of the Spring/Summer young researchers' colloquium on software engineering · 2007
In this paper we introduce a novel approach to formal specification of pipelined designs.The approach is based on contract specifications of pipe stages extended by a mechanism of temporal binding.Contract specifications describe the pipeline behavior in the form of preconditions and postconditions of pipe stages, while temporal binding combines specifications of separated stages into a co-operative specification.Such specifications are suitable for automatic generation of test oracles which check design correctness.The approach was integrated into the CTESK test development tool from the UniTESK toolkit.The methodology was successfully applied to several modules of the industrial microprocessor.