| Login | | Don't have an account yet? You can create one. As a registered user you have some advantages like theme manager, comments configuration and post comments with your name. | |
| Who's Online | There are currently, 54 guest(s) and 0 member(s) that are online.
You are Anonymous user. You can register for free by clicking here | |
 | |
|
Verification Guild: Forums |
|
| View previous topic :: View next topic |
| Author |
Message |
Janick
Site Admin
Joined: Nov 29, 2003
Posts: 1382
Location: Ottawa, ON Canada
|
 Posted: Thu May 13, 2004 6:59 am Post subject: |
 |
|
| romi wrote: | | but it sure seems like being able to not hardcode a reset value sure has many advantages. It allows us to programmatically change the operations of our ASIC by just changing the initialized state. |
You can have both scan AND resets. Most chips with auto-inserted scan chains do.
| Quote: | | As verification becomes more complex, a design would want much more programability to workaround problems. |
But more programmability also makes verification more complex. It is a trade-off.
You currently have a problem that appears to make FV impractical for your design. It could be fixed by making the FV tools work with your usage model (long term, must be a large $$$ customer) - or you could adapt your usage model to the tool. This, however,
You mentionned you had a script that replaced flip-flops with master/slave latches later on in the design. You could code your RTL with async reset but have to resettable flip-flop taken out and replaced by non-resettable master/slave latches later on. |
|
| Back to top |
|
 |
romi
Senior
Joined: Feb 28, 2004
Posts: 88
Location: Minnesota
|
| Posted: Thu May 13, 2004 7:14 am Post subject: |
|
|
| Quote: | | You can have both scan AND resets. Most chips with auto-inserted scan chains do. |
Ok. Makes sense.
| Quote: | | But more programmability also makes verification more complex. It is a trade-off. |
Agreed. We struggle with this all the time.
| Quote: | | You mentionned you had a script that replaced flip-flops with master/slave latches later on in the design. You could code your RTL with async reset but have to resettable flip-flop taken out and replaced by non-resettable master/slave latches later on. |
Got to somehow get rid of the reset port too.
I'm working with one vendor that allows you to set initial values for registers. Seems like other vendors, if they don't already, will/should have a way to do this. |
|
| Back to top |
|
|
bdeadman
Senior
Joined: Jan 06, 2004
Posts: 204
Location: Austin, TX
|
| Posted: Thu May 13, 2004 8:59 am Post subject: |
|
|
My observation on the reset issue is I've always had a reset. In the systems I've been working on I want to make absolutely sure the circuit doesn't come up in some stupid or illegal state and start doing things before the registers get set. A reset signal normally gets me to a safe condition in just a couple of clock cycles, though the rest of the initialization can take a long time.
On the more specific problem. First, I'm a little confused about whether the objective is to establish constraints on your btrack module, or if it's to check the module works correctly in all conditions? If it's the latter and the btrack module is generating the allocate, set & deallocate signals, I'm beginning to wonder if the model checker isn't telling you there's a problem, even if it's a problem you don't care about?
If the signals are being generated by the btrack module, then I'm also concerned by the code in your 'always' block
| Quote: |
always @(negedge clk) begin
if(~reset)begin
allocate_out <= allocate;
set_out <= set;
deallocate_out <= deallocate;
end else begin
allocate_out <= 0;
set_out <= 0;
deallocate_out <= 0;
end
end
|
Is this actually setting the signals inside the module in the way your scan register would? It seems to me it's setting the output signals without modifying the state inside the module. Also, I'm a little concerned about the use of negedge clock to copy the outputs. I would have tried:
always @(negedge clk) begin
if(reset) begin
btrack0.allocate <= 0;
btrack0.set <= 0;
btrack0.deallocate <= 0;
end
end
then simply connected (or worst case continuously assigned) the btrack0 outputs to the btrack_tb module outputs.
Regards
Bernard |
|
| Back to top |
|
|
romi
Senior
Joined: Feb 28, 2004
Posts: 88
Location: Minnesota
|
| Posted: Thu May 13, 2004 9:13 am Post subject: |
|
|
So now you are indicating the I should use OOMRs to initialize the design. I have a feeling the tool won't like that.
Also, you have some misinterpretations about what I did do.
The btrack module has only inputs. The wrapper module, btrack_tb, was just making these inputs come up in a know state. I thought that's what you were suggesting.
I obviously have some problems with the code too. For instance, there is no need to make the *_out signals outputs. They just drive the instantiated module.
Also, I'm really not seeing the need for the wrapper module any longer. I should be able to make the inputs to btrack come up in the correct order by just saying this, right?
| Code: | property start_with_allocate =
(!set && !deallocate) until_ allocate;
|
So, here's where I'm at now.
| Code: | module btrack (clk,allocate,deallocate,set);
input clk; // 1/4 cycle low active clock. ie. high for 3, low for 1, high for 3, low for 1...
input allocate; // Allocates the data buffer. Changes on the negedge of clk.
input set; // Makes the allocated data buffer valid. Changes on the negedge of clk.
input deallocate; // Deallocates the data buffer. Changes on the negedge of clk.
// The inputs never occur on the same cycle and must always occur in order. That is, allocate, set, deallocate.
reg active_r, valid_r;
wire active_s, valid_s, active_in, valid_in;
// psl default clock = negedge (clk);
// psl property never_allocate_when_active =
// never (allocate & active_s);
// psl assert never_allocate_when_active;
// psl property never_deallocate_when_not_active =
// never (deallocate & ~active_s);
// psl assert never_deallocate_when_not_active;
// psl property eventually_valid_if_active =
// always ( active_s -> eventually! valid_s);
// psl assert eventually_valid_if_active;
assign active_in = ((allocate | active_s) & ~deallocate);
always @(negedge clk) begin
active_r <= active_in;
end
assign active_s = active_r;
assign valid_in = (active_s & (set | valid_s));
always @(negedge clk) begin
valid_r <= valid_in;
end
assign valid_s = valid_r;
endmodule |
| Code: | vunit btrack_assume (btrack) {
clock sequence clk_seq = {clk[*3];~clk};
default clock = (negedge clk);
property allocate_to_set =
always (allocate -> next ((!allocate && !deallocate) until_ set));
assume allocate_to_set;
property set_to_deallocate =
always (set -> next ((!set && !allocate) until_ deallocate));
assume set_to_deallocate;
property dallocate_to_allocate =
always (deallocate -> next ((!deallocate && !set) until_ allocate));
assume dallocate_to_allocate;
property start_with_allocate =
(!set && !deallocate) until_ allocate;
assume start_with_allocate;
} |
Fails similarly with both Cadence's staticcheck (LDV5.1) and RealInent's Verix (4.3.1a).
Both the never_allocate_when_active and never_deallocate_when_not_active fail.
-----------------------------------------
I just editted the code slightly taking out some wires I had that were uneccessary and potentially confusing.
Last edited by romi on Thu May 13, 2004 2:48 pm; edited 3 times in total |
|
| Back to top |
|
|
bdeadman
Senior
Joined: Jan 06, 2004
Posts: 204
Location: Austin, TX
|
| Posted: Thu May 13, 2004 9:50 am Post subject: |
|
|
That's better - you threw me completely when you said the three signals were outputs! This is much closer to what I was expecting! I'll try to look at it again.
Bernard |
|
| Back to top |
|
|
|
|
You can post new topics in this forum
You can reply to topics in this forum
You cannot edit your posts in this forum
You cannot delete your posts in this forum
You cannot vote in polls in this forum
|
| |
|
|
Forum FAQ
Search
Usergroups
Profile
Digest
Log in
