!
FLUENT Verification ProjectProblem:
Translate (automatically) a synchronous sequential logic netlist into a useful PRISM model
Motivation
- Analyze effects of transient faults in combinational gates and/or registers.
- Predict characteristics of stochastic logic circuits.
Summary
I previously modeled some stochastic computing circuits in PRISM. This led me to a more basic problem: how to describe sequential logic, where modules’ events are triggered by changes on their inputs. In PRISM, the update behavior is probabilistic (if I understand properly). So a module may update prior to any changes on its input (resulting in no changes). If there is a “pipeline” configuration, e.g. M1->M2->M3, then M3 may update before M2 or M1, since the order is random. This update model is not appropriate for digital circuits with combinational logic situated between synchronous registers.
Up to now, I have devised two paradigms with analogies in Verilog:
Continuous Assignment with formulas
A simple example in Verilog:
input I1, I2, clk;
output reg Z;
reg Q1, Q2;
wire Y;
assign Y = Q1 & Q2;
always @(posedge clk) begin
Q1 <= I1; Q2 <= I2; Z <= Y;
end
In this model, the
assign statement is continuous, so it consumes no time (or minimum time). It could be viewed as a shorthand for
Z=Q1 & Q2. This is analogous to the formula syntax in PRISM. We could therefore use
formula statements to model combinational logic and synchronous guards for register assignments.
formula Y=(Q1=1 & Q2=1);
module REG
Q1 : [0..1] init 0;
Q2 : [0..1] init 0;
Z : [0..1] init 0;
[event] (true) -> (Q1’ = I1);
[event] (true) -> (Q2’ = I2);
[event] (Y) -> (Z’ = 1);
[event] (!Y) -> (Z’ = 0);
endmodule
Pros/Cons for this paradigm:
- Pro: efficient DTMC model. There is only one “event” and the system state is equivalent to the register states.
- Con: Cannot directly model combinational faults or random delays, e.g. timing faults.
Two-phase clocked events
A more complicated paradigm uses an explicit “clock” signal, where the high and low phases are considered distinct events. In a pipeline, modules are successively associated to the high or low phase to maintain synchronization. For the AND example, we could model it this way:
//-----------------------------------
// Clock
//-----------------------------------
// Always toggles
//-----------------------------------
module CLK0
clk : [0..1] init 0;
[event] (true) -> (clk' = 1-clk);
endmodule
module AND
Y : [0..1] init 0;
[event] (clk=0) -> (Y’ = Q1*Q2);
[event] (clk=1) -> (Y’=Y);
endmodule
module REG
Q1 : [0..1] init 0;
Q2 : [0..1] init 0;
Z : [0..1] init 0;
[event] (clk=1) -> (Q1’ = I1);
[event] (clk=0) -> (Q1’ = Q1);
[event] (clk=1) -> (Q2’ = I2);
[event] (clk=0) -> (Q2’ = Q2);
[event] (clk=1) -> (Z’ = Y);
[event] (clk=1) -> (Z’ = Z);
endmodule
Pros/Cons for this paradigm:
- Pro: more flexible than formulas, could model a wider range of behavior
- Con: more complicated, larger state space
- Con: still can’t capture something like a random setup violation
Example: Stochastic TFF Adder
For a more complicated example, I’ve implemented a stochastic adder model based on a toggle flip-flop (TFF). The source files, property lists and results are available in my files at the link below. The figures below show the circuit schematic, the (correct) steady-state results, and the convergence behavior.
The convergence behavior is different between the two models, and I don’t immediately have a satisfactory explanation.
https://left.engr.usu.edu/cloud/winstead/Stochastic_Computing_Models/TFF_adderSchematic:
Convergence figures:
#
PRISM #
stochasticComputing
