Simple PRISM cause/effect example: inverter

Winstead via FLUENT Verification Project

Fri, 13 Dec 2019 15:18:12 -0700

!FLUENT Verification Project

@Chris Myers, @Zhen Zhang:
This model represents an inverter situated between two input D registers. The signal names are shown in red. The bit source and registers are synchronized using action label clk_edge (indicated in blue).

The PRISM model file for this circuit is attached. The bit-source generates a random sequence with Pr(1)=0.5. The problem is that it is possible for multiple clk_edge events to occur, inducing changes in inA and dA, without any INV events. Here's an example from a simulation trace:

event	time step	inA	dA	Q	not_dA
[clk_edge]	10	0	0	0	0
[clk_edge]	11	1	0	0	0
INV	12	1	0	0	1
[clk_edge]	13	0	1	1	1
[clk_edge]	14	0	0	1	1
[clk_edge]	20	1	0	1	1
[clk_edge]	21	0	1	1	1
INV	22	0	1	1	0

Here we see that the input inA undergoes a transition 1001, throughout which the output Q remains constant 1111. But this model is purely deterministic apart from the Bit Source and the update schedule.

Desired behavior: force INV event whenever dA changes.

#PRISM

Chris Myers

Wed, 18 Dec 2019 13:26:43 -0700

I see your problem now I think. The problem is that INV is not a clocked device, so it seems odd to synchronize it on clk_edge, it should happen asynchronously. However, that is not strictly true. It actually does update on each clk_edge because that is when it gets new input. So, I think the solution is to synchronize INV on clk_edge to ensure it updates on each clk_edge event. The only other solution would be to introduce fixed delays somehow into your model. You could do this by having clk_edge produce a delay event, which then is used to fire the INV event, essentially one delay event after clk_edge.

Winstead

Wed, 18 Dec 2019 14:56:54 -0700

The "delay" event might be the best approach. If I sync INV on clk_edge, then it will behave like an inverting register, so the total latency from inA to Q becomes 3 clk_edge periods instead of 2. What it needs to do is definitely update after each clk_edge event, before another clk_edge event happens.

Chris Myers

Wed, 18 Dec 2019 15:54:52 -0700

Good point. The Delay event would essentially create a sort-of 2-phase clocking, which granted is kinda strange. I wonder if you can do something where it creates an event whenever there is a change on dA. Kinda like a sensitivity list in Verilog.