Jasper connectivity check

Sharan,

I believe I recreated what you described for the delayed connectivity through a flop in the following design.

module top ();

wire src, dest, cond, middle, out_mux,clk,rst;
reg flop;

always @(posedge clk or posedge rst)
if (rst)
  flop <=0;
else
  begin
    flop <= src;
  end

assign dest = flop;

endmodule // top

Corresponding connectivity specification:

CONNECTION,test,,src,,dest
LATENCIES,0,0,1,1,0
CLOCK,,clk,posedge

TCL file:

analyze -sv top.sv
elaborate
reset rst
clock -none
check_conn -load conn.csv
check_conn -prove

As Chris noted in his response you need to make the LATENCIES pattern, 0,0,1,1,0 to push to create the property:

@(posedge clk) ( ##1 ($past(src, 1) == dest))

Without the ##1 above you would get a single cycle CEX because the $past(src,1) would return either one or zero because it is asking for the value of src before the formal proof starts. 

Another key piece of information, is that you need to specify the CLOCK specification so there is no ambiguity regarding the sample clock.  You can avoid this by defining the clock but it is better to explicitly specify the sampling clock so there  is not need to define the clock (clock -none) in the tcl commands.

See if this clears up your issue with the delayed connection. 

Regarding the mux.  If it is in the schematic it is in the design.  The connection specification does not influence the schematic. Only the design can impact the schematic.

If you have a mux, then you need to modify the connectivity specification to specify the mux condition. I modified the code and connectivity file to mimic what I believe you are describing.

======== Design ==============

module top ();

wire src, dest, cond, middle, out_mux,clk,rst,s;
reg flop;

// Mux before flop
assign out_mux = s ? src : 1'bz;

always @(posedge clk or posedge rst)
if (rst)
  flop <=0;
else
  begin
    flop <= out_mux;
  end

assign dest = flop;

endmodule // top

========= Connectivity specification - conn.csv ==========

CONNECTION,test,,src,,dest
LATENCIES,0,0,1,1,0
CONDITION,,s,1
CLOCK,,clk,posedge

=========== End of connectivity specification =========

Regarding questions above:

2) I am also interested to understand if a signal from block A is connected to block B using just a wire, what does Jasper try to prove in this case?

Does it just check that fanout of A block is fanin to block B or it runs test to prove that block A to block B signal is toggled properly?

Jasper does validate that fanout of A block is in fanin of B if you issue the tcl command:  "check_conn -validate" in the tcl file. You will see the status marked in the connectivity gui.

Jasper also verifies source signals can toggle by automatically extracting toggle covers for all inputs of the connectivity specification.

Insert the tcl command: "check_conn -generate_toggle_checks" before you issue "check_conn -prove" and you will prove these toggle assertions along with each check.

Let me work on the response to the following and respond tomorrow with the information:

1) The design I would like to verify has mostly 3-4 types of connections

- input to a block is simply output

- input to a block is simply output with a fixed delay

- input to a block is simply output with variable delay (within a fixed range, say 8-16 clock cycles)

- multiple inputs are connected to one output based on a signal condition (sort of many to one mux)

- multiple inputs are connected to one output based on a signal condition (sort of many to one mux) with a delay

Sharan,

I believe I recreated what you described for the delayed connectivity through a flop in the following design.

module top ();

wire src, dest, cond, middle, out_mux,clk,rst;
reg flop;

always @(posedge clk or posedge rst)
if (rst)
  flop <=0;
else
  begin
    flop <= src;
  end

assign dest = flop;

endmodule // top

Corresponding connectivity specification:

CONNECTION,test,,src,,dest
LATENCIES,0,0,1,1,0
CLOCK,,clk,posedge

TCL file:

analyze -sv top.sv
elaborate
reset rst
clock -none
check_conn -load conn.csv
check_conn -prove

As Chris noted in his response you need to make the LATENCIES pattern, 0,0,1,1,0 to push to create the property:

@(posedge clk) ( ##1 ($past(src, 1) == dest))

Without the ##1 above you would get a single cycle CEX because the $past(src,1) would return either one or zero because it is asking for the value of src before the formal proof starts. 

Another key piece of information, is that you need to specify the CLOCK specification so there is no ambiguity regarding the sample clock.  You can avoid this by defining the clock but it is better to explicitly specify the sampling clock so there  is not need to define the clock (clock -none) in the tcl commands.

See if this clears up your issue with the delayed connection. 

Regarding the mux.  If it is in the schematic it is in the design.  The connection specification does not influence the schematic. Only the design can impact the schematic.

If you have a mux, then you need to modify the connectivity specification to specify the mux condition. I modified the code and connectivity file to mimic what I believe you are describing.

======== Design ==============

module top ();

wire src, dest, cond, middle, out_mux,clk,rst,s;
reg flop;

// Mux before flop
assign out_mux = s ? src : 1'bz;

always @(posedge clk or posedge rst)
if (rst)
  flop <=0;
else
  begin
    flop <= out_mux;
  end

assign dest = flop;

endmodule // top

========= Connectivity specification - conn.csv ==========

CONNECTION,test,,src,,dest
LATENCIES,0,0,1,1,0
CONDITION,,s,1
CLOCK,,clk,posedge

=========== End of connectivity specification =========

Regarding questions above:

2) I am also interested to understand if a signal from block A is connected to block B using just a wire, what does Jasper try to prove in this case?

Does it just check that fanout of A block is fanin to block B or it runs test to prove that block A to block B signal is toggled properly?

Jasper does validate that fanout of A block is in fanin of B if you issue the tcl command:  "check_conn -validate" in the tcl file. You will see the status marked in the connectivity gui.

Jasper also verifies source signals can toggle by automatically extracting toggle covers for all inputs of the connectivity specification.

Insert the tcl command: "check_conn -generate_toggle_checks" before you issue "check_conn -prove" and you will prove these toggle assertions along with each check.

Let me work on the response to the following and respond tomorrow with the information:

1) The design I would like to verify has mostly 3-4 types of connections

- input to a block is simply output

- input to a block is simply output with a fixed delay

- input to a block is simply output with variable delay (within a fixed range, say 8-16 clock cycles)

- multiple inputs are connected to one output based on a signal condition (sort of many to one mux)

- multiple inputs are connected to one output based on a signal condition (sort of many to one mux) with a delay