How to replace a statement that has a label

This application shows how to replace a statement expression and the statement could have a label that we can keep or change with a new label.

For the following testcase it specifically replaces assert A1 and assert A2 with the following A1 and A3 in the parse tree.

     A1: assert property(a ##0 b ##0 c |=> o) ;
     A3: assert property(@(posedge clk) disable iff(rst) a ##0 b ##0 c |=> o) ;

Testcase:

module top(clk, rst, a, b, c, d, o) ;
    input clk, rst, a, b, c, d ;
    output reg o ;

    always @(posedge clk) begin
        if (rst)
            o <= 0 ;
        else begin
            A1: assert property(a |-> b |-> c |=> o) ;
        end
    end

    A2: assert property(@(posedge clk) disable iff(rst) a |-> b |-> c |=> o) ;
endmodule
 

C++:

#include "veri_file.h"
#include "VeriModule.h"
#include "VeriId.h"
#include "VeriStatement.h"
#include "VeriScope.h"
#include "VeriVisitor.h"

#include "Netlist.h"
#include "VeriWrite.h"

#include "Strings.h"

#include "Array.h"
#include "Map.h"
#include <iostream>
#include <sstream>

#ifdef VERIFIC_NAMESPACE
using namespace Verific ;
#endif

void find_replace(
    std::string& s,
    std::string const& toReplace,
    std::string const& replaceWith
) {
    std::size_t pos = s.find(toReplace);
    if (pos == std::string::npos) return;
    s.replace(pos, toReplace.length(), replaceWith);
}

class MyVisitor : public VeriVisitor
{
public:
    MyVisitor() : VeriVisitor(), _parent_stack() { }
    virtual ~MyVisitor() { }

    virtual void VERI_VISIT(VeriAssertion, node)
    {
        VeriTreeNode *parent = GetParent() ;
        VERIFIC_ASSERT(parent) ;

        char *pp_str = node.GetPrettyPrintedString() ;
        node.Info("Got assertion: %s", pp_str) ;
        Strings::free(pp_str) ;

        //pp_str = parent->GetPrettyPrintedString() ;
        //node.Info("Parent: %s", pp_str) ;
        //Strings::free(pp_str) ;

        VeriIdDef *label = node.GetOpeningLabel() ;
        if (!label) return ;

        unsigned st ;
        if (Strings::compare(label->Name(), "A1")) {
            std::stringstream stream ;
            node.PrettyPrint(stream, 0) ;
            std::string s = stream.str();
            find_replace(s, "|->", "##(0)");
            find_replace(s, "A1 : ", "");
            char *updated_rtl_code = Strings::save(s.c_str()) ;
            node.Info("UPDATED assertion: %s", updated_rtl_code) ;
            st = ReplaceAssertWith(node, *parent, "A1" /*same label*/, "assert property(a ##0 b ##0 c |=> o) ;") ;
        } else {
            st = ReplaceAssertWith(node, *parent, "A3" /*different label*/, "assert property(@(posedge clk) disable iff(rst) a ##0 b ##0 c |=> o) ;") ;
        }

        parent->Info("Assertion replacement: %s", ((st)?"succeeded":"FAILED")) ;
    }

    // Maintain a parent pointer in the visitor:
    virtual void PreAction(VeriTreeNode &node)  { _parent_stack.Insert(&node) ; }
    virtual void PostAction(VeriTreeNode &node)
    {
        VeriTreeNode *n = (VeriTreeNode *)_parent_stack.RemoveLast() ;
        VERIFIC_ASSERT(n == &node) ;
    }
    VeriTreeNode *GetParent() const
    {
        VeriTreeNode *n = (VeriTreeNode *)_parent_stack.GetLast() ;
        VERIFIC_ASSERT(n) ;
        return n ;
    }

protected:
    unsigned ReplaceAssertWith(VeriAssertion &assert, VeriTreeNode &parent, const char *new_label, const char *new_assert)
    {
        if (!new_assert) return 0 ;

        // Check for any opening label:
        VeriIdDef *label = assert.GetOpeningLabel() ;

        unsigned same_label = (label && new_label && Strings::compare(label->Name(), new_label)) ? 1 : 0 ;

        // Create the string to be parsed with label if the labels are different:
        char *rtl_code = (new_label && !same_label) ? Strings::save(new_label, ":", new_assert) : 0 ;

        // Get the scope of the parent node:
        VeriScope *parent_scope = parent.GetScope() ;
        if (!parent_scope) {
            VeriScope *scope = assert.GetScope() ;
            if (scope) parent_scope = scope->Upper() ;
        }

        // Cannot handle a label without a parent scope:
        if ((label || new_label) && !parent_scope) return 0 ;

        // Now analyze the string into assertion statement:
        VeriStatement *new_node = veri_file::AnalyzeStatement(((rtl_code)?rtl_code:new_assert), veri_file::SYSTEM_VERILOG, 0 /*may use assert.Linefile()*/, parent_scope) ;
        Strings::free(rtl_code) ;
        if (!new_node) return 0 ; // Something went wrong

        if (label && parent_scope && (!new_label || !same_label)) {
#if 0
            // Different label or the new one does not have a label:
            // If you want, you can undeclare and delete the old label;
            // but it may cause memory corruption if it is referred in the design.
            // In that case you have to traverse the whole design and reset the refs.
            // Also, keeping it around will prevent defining the same label again later.
            parent_scope->Undeclare(label) ;
            label->ClearAllBckPtrs() ;
            assert.SetOpeningLabel(0) ;
            delete label ;
#endif
        }

        unsigned st = 1 ;
        // Now, try to replace the assertion statment on the parent:
        if (!parent.ReplaceChildStmt(&assert, new_node, 1 /*delete old assert*/)) {
            // Failed to replace, it may be used as a module item - try to replace that here:
            st = parent.ReplaceChildModuleItem(&assert, new_node, 1 /*delete old assert*/) ;
        }

        if (same_label) {
            // Same label: re-use the existing label:
            new_node->SetOpeningLabel(label) ;
            label->SetScope(new_node->GetScope()) ;
        }

        return st ; // 1 = success, 0 = failure
    }

private:
    Array _parent_stack ;
} ; // class MyVisitor

int main(int argc, char **argv)
{
    Array files(1) ;
    files.Insert("test.v") ;
    if (!veri_file::AnalyzeMultipleFiles(&files, veri_file::SYSTEM_VERILOG)) return 1 ;

    veri_file::PrettyPrint("test_pp.v.golden.new", 0) ;

    MyVisitor mv ;

    MapIter mi ;
    VeriModule *mod ;
    FOREACH_VERILOG_MODULE(mi, mod) if (mod) mod->Accept(mv) ;

    veri_file::PrettyPrint("test_mod_pp.v.golden.new", 0) ;

    // Elaborate the design:
    veri_file::ElaborateAll() ;

    VeriWrite vw ;
    vw.WriteFile("test.v.golden.new", Netlist::PresentDesign()) ;

    // Synthesize assertions in the parse tree:
    //veri_file::SynthesizeConcurrentAssertions() ;
    //veri_file::PrettyPrint("test_assert_synth.v.golden.new", 0) ;

    return 0 ;
}

 

Final modified result:

module top (clk, rst, a, b, c, d, o) ;
    input clk, rst, a, b, c, d ; 
    output reg o ; 
    always
        @(posedge clk)
        begin
            if (rst) 
                o <=  0 ;
            else
                begin
                    A1 : assert property (a ##(0) b ##(0) c |=> o) ;
                end
        end
    A3 : assert property (@(posedge clk) disable iff ( rst) a ##(0) b ##(0) c |=> o) ;
endmodule