-- 1 ####################################################################### -- 2 ############################CPU_TRIGGER.CSP############################ -- 3 ####################################################################### -- CopyRight(r) CURUPIRA Inc, 12/2000, version 2 -- Adolfo Duran - aad@cin.ufpe.br -- Leonardo Freitas - ljsf@cin.ufpe.br -- THIS FILE IS BEST VIEWED WITH TABSTOPS = 4 -- 10 %%%%%%%%%%%%%%%%%%%%%%%%INCLUDE SECTION%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -- Channels define core channels (always need to be included). include "channels.csp" -- 16 %%%%%%%%%%%%%%%%%%%%%%%DOCUMENTATION SECTION%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -- CPU Trigger Timmer. -- This is just a timmer abstraction for the CPU clock tic used exclusively -- by the TC_CLASSIFIER process. -- -- It has been made a separate file since we describe it as an individual -- specification to not mix the state of the TC_CLASSIFIER and CPU_TRIGGER -- specifications -- -- You can also note that this can be an generic specification as defined by -- Fischer (in PhD. thesis) parametrized with the CYCLES variable, but this -- was not well defined in the semantic conversion to FDR, and is avoided here -- but with simple duplication and adjustments we solve this problem -- -- 27 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%ZED DOC SECTION%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -- Attention should be given to the fact that we do not put any input nor outputs -- in the CSP part of the spec's, instead in the declaration part of the channels -- we define the kind of information that will be used by the channel. -- -- At the com function definitions, the commented versions are the those that was -- less optimized than the uncommented one. -- -- spec CPU_TRIGGER -- -- channel cpu_trigger [tic!: CPU_CYCLES] -- -- main = cpu_trigger -> main -- -- 43 %%%%%%%%%%%%%%%%%%%%%%%%%IMPLEMENTATION SECTION%%%%%%%%%%%%%%%%%%%%%%%%% CPU_TRIGGER = let -- The Interface Channels = {| cpu_trigger |} lChannels = {} Interface = union( Channels, lChannels ) -- The CSP Part main = cpu_trigger?n -> main -- The Z Part (specific) State = { clock | clock <- CPU_CYCLES } Init = { 0 } -- { clock' | clock' <- CPU_CYCLES, clock' == 0 } by optimization ? -- com( clock, cpu_trigger.tic ) = { clock' | clock' <- CPU_CYCLES, -- ( not ( clock >= CPU_CYCLE ) or ( clock' == 0 ) ), -- ( not ( clock < CPU_CYCLE ) or ( clock' == clock+1 ) ), -- ( tic == clock' ) } -- -- com( clock, cpu_trigger.tic ) = -- if ( clock >= CPU_CYCLE ) then -- { clock' | clock' <- CPU_CYCLES, ( clock' == 0 ), ( tic == clock' ) } -- else -- { clock' | clock' <- CPU_CYCLES, ( clock' == clock + 1 ), ( tic == clock' ) } com( clock, cpu_trigger.tic ) = if ( clock >= CPU_CYCLE ) and ( tic == 0 ) then { 0 } else if ( tic == ( clock + 1 ) ) then { tic } else {} -- The Z Part (common) Z_CSP = let Z(State) = [] (States,Comm) : {(com(State,c),c) | c <- Interface} @ States != {} & |~| State': States @ Comm -> Z(State') within |~| iState: Init @ Z(iState) within (main [|Interface|] Z_CSP)\lChannels -- END OF SPEC -- 89 %%%%%%%%%%%%%%%%%%%%%%%%%%ASSERTION SECTION%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -- assert CPU_TRIGGER :[ deterministic [FD] ] -- assert CPU_TRIGGER :[ deadlock free [F] ] -- assert CPU_TRIGGER :[ divergence free ] -- 95 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%