!!
FLUENT Verification ProjectRegular Team Meeting
Present: Chris M, Chris W, Jet, Pedro, Zhen
Agenda
- Discussed outreach plans, logistics of recruiting high-school students, school district IRB required for promoting in schools. Costs to $80k for ~60 students. Major costs included (in this order) personnel, housing, transportation. Probably should focus on newly admitted or first-year college students, we can avoid the high costs and complex IRB process.
- Discussed modeling stochastic AND gate in PRISM with counter-output. Need to model the random-walk characteristics of the counter across different time windows.
- Discussed student recruitment. Chris M has a student with some background in neural interfacing and will rotate into the group. Zhen has a possible international student but it will be probably one year before that student can join USU.
- Checkin on progress with models from Jet and Pedro.
- Has @Curtis Madsen made progress with hazard circuit in STORM?
Here's the AND-gate model:
//------------------------------
// Stochastic AND gate model
// Bipolar representation
//------------------------------
dtmc
const double epsilon0=0.25;
const double epsilon1=0.75;
//------------------
// Signal Sources
//------------------
module Source0
x0 : [-1..1] init -1;
[] (x0=-1 | x0=1) -> epsilon0:(x0'=1) + (1-epsilon0):(x0'=-1);
endmodule
// Duplicate signal source:
module Source1 = Source0 [ x0=x1, epsilon0=epsilon1 ] endmodule
//------------------
// AND gate
//------------------
module AND0
a0 : [-1..1] init -1;
[] (x0=1 & x1=1) -> (a0'=1);
[] (x0=-1 | x1=-1) -> (a0'=-1);
endmodule
module Counter0
c0: [-127..127] init 0;
[] (c0>-127) & (c0<127) -> (c0' = c0+a0);
[] (c0 = 127) & (a0=1) -> (c0' = c0);
[] (c0 = 127) & (a0=-1) -> (c0' = c0-1);
[] (c0 = -127) & (a0=-1) -> (c0' = c0);
[] (c0 = -127) & (a0=1) -> (c0' = c0+1);
endmodule
#
meetings #
PRISM #
stochasticComputing #
AND #
STORM
