!
FLUENT Verification ProjectFYI, I've started refining a schema for making stochastic computing models and properties in PRISM. As I develop these, I'm dropping the beta-versions into my files on Hubzilla, and you can view them here:
https://left.engr.usu.edu/cloud/winstead/Stochastic_Computing_Models.
Up to now, I have the TFM model, a divider (DIV), and a divide-by-two (DIV2) circuit. The DIV2 circuit is probably the most mature representation. The basic schema for a stochastic gate model is as follows:
- DTMC model type
- Input stream probabilities given by
const double epsilon0, epsilon1, ... - Time unit given by
const int Tstep - Each input requires a signal source module, which creates a Bernoulli-style random bit-stream. The source modules are named
Source0, Source1, and so on. The bit-streams are named x0, x1, and so on.
//------------------
// Signal Sources
//------------------
module Source0
x0 : [0..1] init 0;
[event] (x0=0 | x0=1) -> epsilon0:(x0'=1) + (1-epsilon0):(x0'=0);
endmodule
- Additional sources are instantiated using the module renaming syntax:
module Source1 = Source0 [ x0=x1, epsilon0=epsilon1 ] endmodule
- All events are synchronized using the
[event] identifier. - The output signal is named
Q.
With these conventions, some convenient properties can be defined:
- Steady-state:
S=? [ Q=1 ] - Transient:
P=? [ F[Tstep,Tstep] Q=1 ] - Convergence:
(P=? [ F[Tstep,Tstep] Q=1 ]) - (S=? [ Q=1 ])- This specification allows performing experiments simultaneously sweeping epsilon and Tstep, to visualize convergence properties.
- The image below shows transient and steady-state probabilities for the DIV2 model.
- The image below shows convergence for the DIV2 model:
I plan to continue building these models and then create a GitHub repo for them once they have a consistent design.
#
models #
PRISM #
stochasticComputing
