// ************************************************************************** // // // // eses eses // // eses eses // // eses eseses esesese eses Embedded Systems Group // // ese ese ese ese ese // // ese eseseses eseseses ese Department of Computer Science // // eses eses ese eses // // eses eseses eseseses eses University of Kaiserslautern // // eses eses // // // // ************************************************************************** // // This module implements the following SIGNAL program: // // // // +-----------------------+ // // | +-----+ | // // +->| Buf |--+ | // // +-----+ | | x1 // // | +-----+ | // // +-----------o->| | | // // x2 | +-----+ | Add | | // // +->| Buf |---->| |--o--> y // // +-----+ x3 +-----+ // // // // // // This SIGNAL program generates the sequence of Fibonacci numbers. It is a // // nice example for compositional verification. // // ************************************************************************** // import BasicNodes.*; macro val(x) = x.0; macro clk(x) = x.1; module Fibonacci(event ?clk_y,event int !val_y) { event(int * bool) x1,x2,x3; Buf(x1,x2,1); || Buf(x2,x3,1); || Add(x2,x3,x1); || CpyOut(clk(x1),clk_y,val(x1),val_y); } // ************************************************************************** // // This input trace is not clock consistent and will lead to val(x2)=⊤ in the // // second macro step of the Quartz program. // // ************************************************************************** // drivenby t1 { int i; while(i<100) { clk_y = true; next(i) = i+1; pause; } }