Disclaimer: I am writing this post while recovering from 3-day covid-y fever. So, there is a chance that memes to technical details ratio is alarmingly high. If you want the boring technical stuff, read the paper :^)

This post is about dvcon paper titled SAWD: Systemverilog Assertions waveform based development tool which was a weekend project that escalated quickly.

Problem statement Link to heading

Starting with problem statement, I will just use this xkcd joke that I am big fan of :)

This is problem is not about regex but i find my problem very similar. let me explain, I have one problem to verify this design, so i decide to write an assertion, now i have 2 problems. right?! right!?

we all agree that writing SVA is a problem on it’s own because SVA are complicated and it takes long time to write, test and debug assertion expressions.

Usually i start by creating handcrafted directed test with many assignments and delays. Just to make sure sequences and properties compile and have a heartbeat. Then start running the assertion in the bigger design env. Usually the design env takes 3-4 hours to compile/run. So, if i find a problem in my assertion i have to turn to wait these 3-4 hours.

well, One can’t simply write an assertion

The back story Link to heading

anyway, I was bored one weekend last Feb and was looking for something to do. so, i went to a pub in the city to kill some time. While i was doodling on coaster, I had the idea.

if WAL can evaluate expressions on waveform, why can’t i evaluate assertions on VCD?

So, i wrote down the architecture and data structures(mainly time-aware expression tree) on cocktail napkin :)

I started writing each BNF line from LRM into Lark EBNF. Honestly,this was most boring part and it took all night to get all the basic BNF for basic assertion.

once i have that implemented, the engine came next on Sunday. It was hacky and literally quick-and-dirty code that only understands the delay ##1 but it worked. And then supporting the rest of sequence and property operators became about shaping the syntax tree and supporting that operator in evaluation engine.

SAWD Link to heading

at this point, i am planning to open-source the SAWD but until then, this is high level explanation of architecture. Please, enjoy the ASCII art!

SVA -> SVA Frontend -> |
                       | -> evaluation engine -> | (reports and diagrams)
VCD ->VCD Frontend  -> | 

the SVA front is basically the front end of compiler. I used Lark to generate syntax tree and cool feature from lark, is that i can transformations to convert the syntax tree to AST(abstract syntax tree)

This is snippet of SVA_GRAMMER variable that is fed to lark. I copied a lot of SV LRM BNF into lark EBNF for this work.

SVA_GRAMMAR = r"""
    //
    // body
    //
    ?body: (checker_or_generate_item)*
    checker_or_generate_item:   concurrent_assertion_item
                                | assertion_item_declaration
    //
    // Assertion declarations
    //
    concurrent_assertion_item: [ block_identifier ":" ] concurrent_assertion_statement
    concurrent_assertion_statement: assert_property_statement
    assert_property_statement: "assert" "property" "(" property_spec ")" action_block
    property_instance: ps_or_hierarchical_property_identifier [ "(" [ property_list_of_arguments ] ")" ]
    property_list_of_arguments: [ property_actual_arg ] ( "," [ property_actual_arg ] )*
    property_actual_arg: property_expr
                         | sequence_actual_arg
    assertion_item_declaration: property_declaration
                                | sequence_declaration

once that’s done, transformations kick in to transform the syntax tree into nodes

    def property_expr_implication1_rule(self,args):
        seq, prop = args
        nodes = [seq,prop]
        ast = Node(NodeType.AST_IMPLICATION1, *nodes)
        return 

well, here is part of AST node for reference

class NodeType(Enum):
    AST_NONE            = ""
    AST_LOGIC_AND       = "&&"
    AST_LOGIC_OR        = "||"
    AST_LOGIC_NOT       = "!"
    AST_BIT_AND         = "&"
    AST_BIT_OR          = "|"
    AST_BIT_NOT         = "~"

On the other side, I also wrote vcd frontend as wrapper around vcdvcd.I had fun implementing edge, Posedge, Negedge API so that the engine can call these API and not vcdvcd low-level API

class Signal(vcdvcd.Signal):
    """ Custom Signal class """

    def __init__(self,*args):
        super().__init__(self, *args)
        self.marker = 0

    def __call__(self, time):
        return self[time]

    @property
    def timestamps(self):
	....

    @property
    def values(self):
	....

    @property
    def edges(self):
	....

The third big component is the engine. Although the engine is the most interesting part. It’s very consistent and systemic code. I talked about time-aware expression tree a lot. It’s time we see it. it’s very simple rooted tree with timestamps for start and end of an expression.

class Node:
    """ """
    def __init__(self, type_,  *args, **kargs):
        self.type_      : NodeType  = type_
        self.children   :[Node]     = list(args)
        self.ts         : Result    = None
        self.evaluated : Result    = None
        self.tag        : str       = ''.join(random.choices(string.ascii_letters + string.digits, k=8))

Finally, here is the output of the tool for each evaluation. The diagram uses the time-aware expression tree to show how each expression (and children expressions) are evaluated.