WaveDrom is really great tool to generate timing diagram. It provide nice features to annotate the diagrams with arrows to link between edges. So, it was fun to invent simple convention using WaveDrom to generate simple SVA expressions.

I thought to start with 2 assertions:

  • -~> Horizontal arrow between nodes
  • -|> Vertical arrow between nodes

The first step is defining the nodes to anchor the arrows(Horizontal and Vertical).

The horizontal specifies delayed between the events.

$rise(req) |-> ##[1:N] $rise(ack);

The vertical specifies zero-delay between the events.

$rise(req) |-> ($stable(ack); && ack == 0

{
"signal": [
  {"name": "clk", "wave": "P.......", "node":"........"},
  {"name": "req", "wave": "01...0..", "node":".a.B.c.D"},
  {"name": "ack", "wave": "0..1...0", "node":".A.b.C.d"}
],
  "edge"   : ["a-~>b 1:N",
  				"b-~>c 2",
                "c-~>d 2",

  				"a-~>c 1:$",
  				"b-~>d 1:$",

  		  		"a-|>A",
  				"b-|>B",
  				"c-|>C",
  				"d-|>D"

   ],
 "config": {"hscale":2,"scale":2}
}

The generated diagram should something like the following:

Example image

And the generated SVA expressions:

$rise(req) |-> ##[1:N] $rise(ack);
$rise(ack) |-> ##[2] $fell(req);
$fell(req) |-> ##[2] $fell(ack);
$rise(req) |-> ##[1:$] $fell(req);
$rise(ack) |-> ##[1:$] $fell(ack);
$rise(req) |-> ($stable(ack); && ack == 0
$rise(ack) |-> ($stable(req); && req == 1
$fell(req) |-> ($stable(ack); && ack == 1
$fell(ack) |-> ($stable(req); && req == 0

well, Not my proudest moment but it’s Saturday and I will probably rewrite the whole thing again.

        for i, n in enumerate(node):
            # Parse labels
            if n != ".":
                edge = mapping[wave[i]]

                assert (edge in mapping.values())

                """
                in case of 1 or 0, that is the correct value
                in case of ".", i need to get the last non-"." value
                """
                value = None
                if wave[i] != ".":
                    value = wave[i]
                else:
                    value = get_last_value(wave[0:i])
                assert(value is not None)

                nn = Node(n, sig_name, i , wave[i], value, edge)
                nodes.append(nn)

    # Parse edges for assertions
    edges = []
    for e in wd["edge"]:
        ed = None

        # a-~>b DELAY
        # a |-> ##[DELAY] b
        result = re.match("([a-zA-Z])-~>([a-zA-Z]) (.*)", e)
        if result:
            tokens = result.groups()