!
FLUENT Verification ProjectHere is a
tracking forecast memory model in PRISM. A TFM is basically a low-pass filter that estimates the statistic of a bit-stream. This is a little cleaner in PRISM and I'm able to verify some properties.
dtmc
const double epsilon0;// = 0.75;
const double beta = 0.0625;
//------------------
// Signal Sources
//------------------
module Source0
x0 : [0..1] init 0;
[event] (x0=0 | x0=1) -> epsilon0:(x0'=1) + (1-epsilon0):(x0'=0);
endmodule
// ...
module someModule
q : [0..1] init 0;
[event] (c0>0) -> (c0/127):(q' = 1) + (1-c0/127):(q'=0);
[event] (c0=0) -> (q'=0);
endmodule
module TFM0
c0: [0..127] init 0;
[event] (c0 >= 0) & (c0 <= 127) -> (c0' = round(c0[i](1-beta)) + round(127[/i]x0*beta));
endmodule
Here are a couple of properties I tested. The second one checks the probability of <10% error during the window of 500--510 clock cycles.
P=? [ F[110,110] q=1 ]
P=? [ F[500,510] c0<epsilon0[i]1.1[/i]127 & c0>epsilon0[i]0.9[/i]127 ]
I was able to do an experiment sweeping the input bit-stream statistic, showing that the output precision improves with higher density of 1's in the input stream. This is the expected result (ignoring the little glitch in the low values).
#
PRISM #
stochasticComputing
