xref: /linux/tools/verification/rvgen/tests/specs/test_ha.dot (revision 55ee4b931a7ffedc886175d265dd6e6d08fd4151)
1*655d4809SGabriele Monacodigraph state_automaton {
2*655d4809SGabriele Monaco	center = true;
3*655d4809SGabriele Monaco	size = "7,11";
4*655d4809SGabriele Monaco	{node [shape = circle] "S1"};
5*655d4809SGabriele Monaco	{node [shape = plaintext, style=invis, label=""] "__init_S0"};
6*655d4809SGabriele Monaco	{node [shape = doublecircle] "S0"};
7*655d4809SGabriele Monaco	{node [shape = circle] "S0"};
8*655d4809SGabriele Monaco	{node [shape = circle] "S2"};
9*655d4809SGabriele Monaco	{node [shape = circle] "S3"};
10*655d4809SGabriele Monaco	"__init_S0" -> "S0";
11*655d4809SGabriele Monaco	"S0" [label = "S0\nclk < bar_ns()", color = green3];
12*655d4809SGabriele Monaco	"S1" [label = "S1"];
13*655d4809SGabriele Monaco	"S2" [label = "S2\nclk < BAR_NS()"];
14*655d4809SGabriele Monaco	"S3" [label = "S3"];
15*655d4809SGabriele Monaco	"S1" -> "S0" [ label = "event0;reset(clk)" ];
16*655d4809SGabriele Monaco	"S0" -> "S1" [ label = "event1;reset(clk)" ];
17*655d4809SGabriele Monaco	"S0" -> "S0" [ label = "event0;reset(clk)" ];
18*655d4809SGabriele Monaco	"S1" -> "S2" [ label = "event2;env1 == 0;reset(clk)" ];
19*655d4809SGabriele Monaco	"S2" -> "S3" [ label = "event2" ];
20*655d4809SGabriele Monaco	"S2" -> "S2" [ label = "event1;clk < foo_ns" ];
21*655d4809SGabriele Monaco	"S3" -> "S0" [ label = "event0;clk < FOO_NS && env2 == 0" ];
22*655d4809SGabriele Monaco	"S3" -> "S1" [ label = "event1;clk < 5us && env1 == 1;reset(clk)" ];
23*655d4809SGabriele Monaco	{ rank = min ;
24*655d4809SGabriele Monaco		"__init_S0";
25*655d4809SGabriele Monaco		"S0";
26*655d4809SGabriele Monaco	}
27*655d4809SGabriele Monaco}
28