Jasper connectivity check

hi Sharan,

 How can you tell that the tool is taking condition from 2 lines above? Can you expand? I just ran a simple example of  the following connections

CONNECTION,c_1,,t2,,out2
,COND_EXPR,~(sel)
CONNECTION,c_2,,t1,,out2
,COND_EXPR,sel
CONNECTION,c_0,,t1,,out1
,LATENCIES,0,0,1,1,0
,DISABLE_EXPR,~(rstn)

in which the last one is a simple latency connection. It worked just fine. I'm guessing you may need to change your LATENCY settings such that the check_latency setting is  1.

Chris

Hello Chris,

I have tried to explain full details of the example I have created and the issue I am talking about.

Design details:

This is a typical pin mux module.

Inputs: pin1, pin2, pin3, pin4, propogate_s1, sel

outputs: opin, opropogate_s1

All inputs and outputs are single bit except sel, which is 2 bits.

Function of the block:

muxes pin1/pin2/pin3/pin4 to opin depending on sel

opropogate_s1 is just 1 cycle delayed version of propogate_s1

Connection specification is as follows:

,NAME,SRC BLOCK,SRC SIGNAL,DEST BLOCK,DEST SIGNAL
CONNECTION,pin1_mux,,pin1,,opin
CONDITION,,sel,2'b00
#
CONNECTION,pin2_mux,,pin2,,opin
CONDITION,,sel,2'b01
#
CONNECTION,pin3_mux,,pin3,,opin
CONDITION,,sel,2'b10
#
CONNECTION,pin4_mux,,pin4,,opin
CONDITION,,sel,2'b11
#
CONNECTION,propogate_delay,,propogate_s1,,opropogate_s1
LATENCIES,,0,0,1,0

The last two rules basically deal with propogate_s1 signal and opropogate_s1

The first rule describes that connection of opropogate_s1 to propogate_s1

The second rule describes that opropogate is one cycle delayed version of propogate_s1

 Observations after running Jasper:

1) all connection rules are passing except propogate_delay.

2) I am looking at the view property in the GUI. It shows - ($past(propogate_s1, 1) = opropogate_s1)

3) I am also looking at view violation trace. It shows just one clock cycle waveform.

opropogate_s1 and propogate_s1 are both 0 during this 1 cycle.

4) **this is the interesting part**

I open schematic viewer for propogate_delay rule.

The schematic shows 2 stages for connection.
first stage shows propogate_s1 passing through a 2-1 mux.
The first input is 'a' which is left open; second input to mux is propogate_s1. Mux select is "s".

The second stage is flop, which is as expected.

Now I am not sure where jasper is inferring a mux for the propogate_delay rule.

Also, I have several questions on Jasper Gold connectivity checker. I would be thankful to get clarifications on these.

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

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?

3) I have read Jasper user guide. The connectivity part of the user guide deals more with the syntax of the tool but lacks description about

the application part of this. For example, there is hardly any explanation or examples about how each of these connectivity directives can be used by users.

I will also look into your example.

Regards,

Sharan

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

CrazyForFormal,

Thanks a lot for detailed explanation. I think I understand where I was going wrong.

I already have rules for the following case. So, I am good on these two cases. You can probably help me with the other 3 cases.

1) input to a block is simply output

2) input to a block is simply output with a fixed delay

Now that I have started implementing rules for a real project, I do have some additional questions.

1) Is a rule as follows allowed:

CONNECTION, id_1, ,~inp,,op

Please notice the ~ operator at the source signal. I ask this as I have seen most of the description for connectivity talk about input to output propagation with a lot of conditions. But in the above case, there is an change in signal value (inverted output).

if this is not acceptable then is there an alternate way to describe this?

2) I want to use constants while writing the rules

   a) can I use alias to do this?

   b) can I use `define from Verilog/SystemVerilog

  For example, is the following allowed:

  e.g. 1  (t_mode == `TRUE)

 TRUE is a define in my Verilog file

 e.g. 2 (t_mode = TRUE)

 TRUE is defined as 1'b1 Alias in the rule file

3) One main use-case of Connectivity checker is for pin muxing logic.

Normally, these modules don't have clock. So, how to specify to tool that there is no reset or clock to the module?

4) When I have to write rules for a 2-1 mux function of DUT, do I have to write 2 connection rules or there is a way to compress this description using a single connection rule?

For example,

CONNECTION, id_1, ,inp_1,,op

COND_EXPR, sel == 1'b0

CONNECTION, id_2, ,inp_2,,op

COND_EXPR, sel == 1'b1

 5) The pin mux design I am trying to verify has technology components for mux logic.

I have simulation models for these technology components. These are behavioral codes.

Is there any guideline for handling tech. components in Jasper?

Thanks a lot ... 

Unknown said:

<snip>

Now that I have started implementing rules for a real project, I do have some additional questions.

1) Is a rule as follows allowed:

 

CONNECTION, id_1, ,~inp,,op

Jose> Yes this is allowed.

Please notice the ~ operator at the source signal. I ask this as I have seen most of the description for connectivity talk about input to output propagation with a lot of conditions. But in the above case, there is an change in signal value (inverted output).

if this is not acceptable then is there an alternate way to describe this?

2) I want to use constants while writing the rules

   a) can I use alias to do this?

   b) can I use `define from Verilog/SystemVerilog

 

  For example, is the following allowed:

  e.g. 1  (t_mode == `TRUE)

 TRUE is a define in my Verilog file

 

 e.g. 2 (t_mode = TRUE)

 TRUE is defined as 1'b1 Alias in the rule file

 Jose> I need to research this.  I believe an ALIAS will work as we simply do a search and replace in connectivity spec. Give it try.  Not sure about Verilog defines.

3) One main use-case of Connectivity checker is for pin muxing logic.

Normally, these modules don't have clock. So, how to specify to tool that there is no reset or clock to the module?

 Jose> For clock simply issue:  "clock -none" in tcl file. If you do not have any pipeline connection then you can simply issue:  "reset -none" command in tcl file.

4) When I have to write rules for a 2-1 mux function of DUT, do I have to write 2 connection rules or there is a way to compress this description using a single connection rule?

 Jose> You need to specify 2 rules. One for each connection you want to describe.  If you are familiar with the IFV spreadsheet you can specify the mux connection in a single line but if you are starting with Jasper csv file format then simply specify a line per mux connection. Your example below is correct.

For example,

CONNECTION, id_1, ,inp_1,,op

COND_EXPR, sel == 1'b0

CONNECTION, id_2, ,inp_2,,op

COND_EXPR, sel == 1'b1

 5) The pin mux design I am trying to verify has technology components for mux logic.

I have simulation models for these technology components. These are behavioral codes.

Is there any guideline for handling tech. components in Jasper?

Jose> Jasper and formal tools consume only synthesizable rtl only.  Sorry.

Thanks a lot ... 

CrazyForFormal,

I actually read CDNS article. It shows an example as follows:

In fact, my question where is Alias allowed and not allowed. Where is SV/Verilog Macros allowed and not allowed.

If Jasper simply in verbatim replicates certain portion of the rule as SVA then I guess Veriog/SV macros should be ok.

I need further information on this.