How to replace a statement that has a label
From Verific Design Automation FAQ
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