!!
FLUENT Verification ProjectZhen and I met today and took a close look at the stochastic AND gate problem. We came up with a workable counter model. Quick background: one of the main functions in a stochastic computing system is regeneration, where we sample the probability from one stream in order to produce a new, uncorrelated stream with the same statistic. An example application is the unipolar stochastic divider, where a feedback signal is used to force [tex] $p_Q = p_Ap_B$[/tex].
To model stochastic regeneration, we can use bounded counters that reset every 128 clock cycles. During the reset, a register is updated to reflect the input stream's bit frequency. This approach prevents the state space from exploding, and is also a better hardware model.
dtmc
const double epsilon0=0.25;
//------------------
// 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] (t0>0) -> (c1/127):(q' = 1) + (1-c1/127):(q'=0);
[event] (t0=0) -> (q'=0);
endmodule
module Counter0
c0: [0..127] init 0;
[event] (t0 < 127) & (c0 < 127) -> 1.0:(c0'=c0+x0);
[event] (t0 = 127) -> (c0' = 0);
endmodule
module register0
c1: [0..127] init 64;
[event] (t0 = 127) -> (c1' = c0);
[event] (t0 < 127) -> (c1' = c1);
endmodule
module elapsedTime
t0: [0..127] init 0;
[event] (t0 < 127) -> (t0' = t0 + 1);
[event] (t0 = 127) -> (t0' = 0);
endmodule
#
models #
PRISM #
stochasticComputing
