Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- //design example
- module design_module(
- input logic enable,
- input logic reset,
- input logic clk,
- output logic active);
- logic [1:0] fsm_cs;//current state
- logic [1:0] fsm_ns;//next state
- always @(posedge clk or posedge reset)
- begin
- if(reset)
- fsm_cs <= 2'b0;
- else
- fsm_cs <= fsm_ns;
- end
- always_comb
- case(fsm_cs)
- 2'b00: if(enable==1'b1 && reset==1'b0)
- fsm_ns=2'b1;
- 2'b01: if(enable==1'b0 || reset==1'b1)
- fsm_ns=2'b0;
- default: fsm_ns=2'b0;
- endcase
- assign active = (fsm_ns==2'b01) ? 1'b1:1'b0;
- endmodule
- //assertion module
- module assertion_module(input logic fsm_state,input logic enable,input logic reset,input logic clk);
- property fsm_check();
- @(posedge clk)
- disable iff(reset) $rose(enable)|=> (fsm_state==2'b1);
- endproperty
- FSM_ASSERT:assert property(fsm_check) else `uvm_error("assertion_module", $sformatf("fsm assertion failed");
- endmodule
- //testbench top
- module top();
- logic en,reset,tester_clk,active_out;
- initial
- begin
- tester_clk=1'b0;
- forever #10 tester_clk=~tester_clk;
- end
- design_module mydut(.enable(en),.reset(reset),.clk(tester_clk),.active(active_out));
- //binding assertion module(assertion_module) to design module(design_module)
- bind design_module assertion_module assert_instance(.fsm_state(fsm_cs),.enable(enable),.reset(reset),.clk(clk));
- initial
- begin
- #5;
- reset=1'b1;
- #10;
- reset=1'b0;
- #10
- en=1'b1;
- #100;
- $finish;
- end
- endmodule
Add Comment
Please, Sign In to add comment