Jasper connectivity check

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

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